Go backward to Proof of Ensure Relations
Go up to Top
Go forward to References

Proof of Unless Relations

Show y>=z and y=m unless y<m.
- Show {( $y$ $>=$ $z$ and $y$ = $m$ ) and $y$ $>=$ $m$ } $s$
  {( $y$ $>=$ $z$ and $y$ = $m$ ) or $y,m$ }
  for every $s$ .
{(y>=z and y=m) and y>=m}
z,k := 2*z, 2*k if y>=2*z ~
N,1 if y<2*z
{(y>=z and y=m) or y,m}
- { $y$ $>=$ $2*z$ and ( $y$ $>=$ $z$ and $y$ = $m$ ) and $y$ $>=$ $m$ }
  $z,k$ := $2*z, 2*k$
  {( $y$ $>=$ $z$ and $y$ = $m$ ) or $y,m$ }
- { $y<2*z$ and ( $y$ $>=$ $z$ and $y$ = $m$ ) and $y$ $>=$ $m$ }
  $z,k$ := $N, 1$
  {( $y$ $>=$ $z$ and $y$ = $m$ ) or $y,m$ }

Show that in all statements premise or conclusion holds from state where premise but not conclusion holds.

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