THM	not_not_eq	x,y:. (x = y) x = y
ML	super_reduce	let BoolToProp i = RWH (bool_to_propC) i ;; let Reduce' i = Reduce i THEN RWH (bool_to_propC) i THEN Try (RW (SweepUpC (LemmaC `not_not_eq`)) i) ;;
THM	hoare_example_1	[q] = 2 {SKIP} [q] = 2
THM	hoare_example_2	True {a := 2} [a] = 2
THM	hoare_example_3	True {WHILE Bexp(tt) DO SKIP OD} False
DISP	factorial_df	(<n:nat:*>)!== (<n>)!
ML	factorial_ml	(n)!==r if n z 0 then 1 else n * (n - 1)! fi
THM	factorial_wf	n:. (n)!
THM	hoare_example_4	n: True {f := 1; i := 0; WHILE NOT i == n DO i := i + 1; f := i * f OD} [f] = (n)!
THM	gcd_sub	a,b,y:. GCD(a;b;y) GCD(a;b - a;y)
DISP	gcd_exe_df	#GCD#== #GCD#
ABS	gcd_exe	#GCD# == WHILE NOT a == b DO IF a < b THEN b := b - a ELSE a := a - b OD
THM	gcd_exe_wf	#GCD#
THM	hoare_gcd_1	n:. GCD([a];[b];n) {#GCD#} [a] ~ n
THM	hoare_gcd_2	[a] > 0 [b] > 0 {#GCD#} [a] > 0 [b] > 0
THM	hoare_gcd	n:. GCD([a];[b];n) [a] > 0 [b] > 0 {#GCD#} [a] = n

the other theories