%%% 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
%