%
% examples from the practical session
% Tallinn, 10.9.03

proof ex1 : ((A | B) => C) <=> (A => C) & (B => C) =
begin
[(A => C) & (B => C);
 [A | B;
  A => C;
  B => C;
  [ A;
    C ];
  [ B;
    C ];
  C];
 (A | B) => C];
(A => C) & (B => C) => ((A | B) => C);
[(A | B) => C;
 [ B;
   A | B;
   C ];
 B => C; 
 [ A;
   A | B;
   C ];
 A => C;
 (A => C) & (B => C)];
((A | B) => C) => (A => C) & (B => C);
((A | B) => C) <=> (A => C) & (B => C)
end;

proof tarmo : ~~ (A | ~A) =
begin
[ ~ (A | ~A);
  [ A;
    A | ~A;
    F ];
  ~A;
  A | ~A;
  F];
~~ (A | ~A)
end;

proof expred : ((! x:t . (P x) & (Q x)) <=> (!x:t.P x) & (!x:t.Q x)) =
begin
[ (!x:t.P x) &(!x:t.Q x);
  [ x0 : t;
    !x:t.P x;   
    P x0;  
    !x:t.Q x;
    Q x0;
    (P x0) & (Q x0)];
  ! x:t . (P x) & (Q x)];
(!x:t.P x) &(!x:t.Q x) => (! x:t . (P x) & (Q x));
[ ! x:t . (P x) & (Q x);
  [ x1 : t;
    (P x1) & (Q x1);
    P x1];
  !x:t.P x;
  [ x2 : t;
    (P x2) & (Q x2);     
    Q x2];
  !x:t.Q x;
  (!x:t.P x) & (!x:t.Q x)];
(! x:t . (P x) & (Q x)) => (!x:t.P x) &(!x:t.Q x);
(! x:t . (P x) & (Q x)) <=> (!x:t.P x) &(!x:t.Q x);
end;

proof tarmopred : (!x:t.?y:t.R x y)
               => (!x:t.!y:t.!z:t.(R x y) => (R y z) => (R x z))
               => (!x:t.!y:t.(R x y) => (R y x))
	       => (!x:t.R x x) =
begin 
[!x:t.?y:t.R x y;
 [ (!x:t.!y:t.!z:t.(R x y) => (R y z) => (R x z));
   [ (!x:t.!y:t.(R x y) => (R y x));
     [ x0 : t;
       ? y:t.R x0 y;
       [ y0:t, R x0 y0;
         !y:t.(R x0 y) => (R y x0);
         (R x0 y0) => (R y0 x0);
	 R y0 x0;
         !y:t.!z:t.(R x0 y) => (R y z) => (R x0 z);
         !z:t.(R x0 y0) => (R y0 z) => (R x0 z);	
         (R x0 y0) => (R y0 x0) => (R x0 x0);
	 (R y0 x0) => (R x0 x0);
         R x0 x0];
       R x0 x0];
     !x:t.R x x];
   (!x:t.!y:t.(R x y) => (R y x))
	       => (!x:t.R x x)];
 (!x:t.!y:t.!z:t.(R x y) => (R y z) => (R x z))
               => (!x:t.!y:t.(R x y) => (R y x))
	       => (!x:t.R x x)];
 (!x:t.?y:t.R x y)
               => (!x:t.!y:t.!z:t.(R x y) => (R y z) => (R x z))
               => (!x:t.!y:t.(R x y) => (R y x))
	       => (!x:t.R x x)
end;