Go backward to Example: Type Correctness
Go up to Top
Go forward to General Invariance Proofs
Proof
- Prove and [A]
- and A
- and A
- and (<, >' = <,
>)
- Prove and A
- (( in Nat) and (
in Nat))'
( in Nat) and ( in Nat)
- and A in Nat
and A in Nat
- Prove and A in Nat
- and A
( in Nat) and ( = )
in Nat
Proofs "mechanically" guided by the structure of formulas.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine