-1-



demo 	: o  -> type.
prove 	: o -> o -> o -> type.
assume 	: o -> type.
chain  	: o -> o -> o -> o -> type.

start 	: demo A <- prove A true false.
ptrue   	: prove true true _ .
pnot		 : prove (not A) S F <- prove (A => false) S F.
pand     	 : prove (A & B) S F <- prove A (B & S) F.
porl		 : prove (A v B ) S F <- prove A S (B v F).
pimplies 	 : prove (A => B) S F <- (assume A -> prove B S F).
pinst	 : prove (some A) S F <- prove (A X) S F.
pgen		 : prove (all A) S F <- {a : i} prove (A a) S F.
patom    	 : prove A S F <- assume B <- chain B A S F.
pbtrack  	:  prove A S (F & false) <- prove F S false.

uaxiom 	 : chain A A S F <- prove S true F.
uandL   	 : chain (B1 & B2) A S F <- chain B1 A S F.
uandR   	 : chain (B1 & B2) A S F <- chain B2 A S F.
uall     	 : chain (all D) A S F <- chain (D X) A S F.
uimplies 	 : chain (B => A) A  S F <- prove B S F .