%%% Assignment 4 %%% Out: Monday 1st Oct %%% Due: Monday 8th Oct %%% Author : Brigitte Pientka annotated proof p1 : (A | ~ A) => ((A => B) => A) => A = begin [ x : (A | ~A); [y : (A => B) => A; [u : A; u : A]; [v : A => F; [z: A; v z : F; abort (v z) : B]; fn z => abort (v z) : A => B; y (fn z => abort (v z)) : A]; case x of inl u => u | inr v => y (fn z => abort (v z)) end : A]; fn y => case x of inl u => u | inr v => y (fn z => abort (v z)) end : ((A => B) => A) => A]; fn x => fn y => case x of inl u => u | inr v => y (fn z => abort (v z)) end : (A | ~ A) => ((A => B) => A) => A end; annotated proof p2 :~A | ~B => ~(A & B) = begin [x : ~A|~B; [u : ~A; [z: A & B; fst z : A; u (fst z) : F]; fn z => u (fst z) : ~(A & B)]; [v : ~B; [z : A & B; snd z : B; v (snd z) : F]; fn z => v (snd z) : ~(A & B)]; case x of inl u => (fn z => u (fst z)) | inr v => (fn z => v (snd z)) end : ~(A & B)]; fn x => case x of inl u => (fn z => u (fst z)) | inr v => (fn z => v (snd z)) end : ~A | ~B => ~(A & B) end; term M : (A => C) => ((B => C) => (A | B => C)) = fn x => fn y => fn z => case z of inl u => (x u) | inr v => (y v) end ; % what is the type of the term ... term N : (A => B => C) => (A => B) => A => C = fn x => fn y => fn z => x z (y z); term O : (A => B => C) => B => A => C = fn x => fn y => fn z => x z y; term P : ((A | B) => C) => (A => C) & (B => C) = fn x => (fn a => x (inl a), fn b => x (inr b)); % reduction 1 % N (fn x => fn y => y) (fn x => x) (fn x => fn y => x) % reduces to (fn x => fn y => y) (fn x => fn y => x) ((fn x => x) (fn x => fn y => x)) % .... fn x => fn y => x % reduction 2 % M (fn x => x) ((fn x => inl x) ((fn x => fn y => x )(fn x => fn y => x y) ())) % reduces to : fn x => fn y => x y %