Go backward to Invariant Proof
Go up to Top
Go forward to Fixed Point Proof
Fixed Point Proof
- Show (true FP):
- Know I and FP.
- Suffices to show (true ).
- Show (true ).
- Find well-founded ordering << with
(,)=(,) and not ( )
(,)<<(,).
- By induction, not ( ) cannot hold forever.
Find inductive term.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine