Go backward to Fixed Point Proof
Go up to Top
Go forward to Proof of Ensure Relations

Fixed Point Proof

Let << be the lexicographic ordering.
- ( $y$ , $z$ ) << ( $m$ , $n$ ) := ( $y<m$ or ( $y=m$ and $z<n$ )).
- Show ( $y$ , $z$ )=( $m$ , $n$ ) and not ( $y<z$ $<=$ $N$ ) $|->$ ( $y<m$ or ( $y=m$ and $z<n$ )).
- General disjunction theorem for $|->$ .
Show (y,z)=(m,n) and y>=z |-> y<m.
- Suffices to show $y$ $>=$ $z$ and $y$ = $m$ ensures $y<m$ .
Show (y,z)=(m,n) and y<z and z>N |-> (y=m and z<n).
- Suffices to show ( $y$ , $z$ )=( $m$ , $n$ ) and $y<z$ and $z>N$ ensures ( $y=m$ and $z<n$ ).

Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine