ITL
© 1996-2018







9 Properties of While


while w do f if w then f ; (while w do f) else empty WhileEqvIf


Proof:

1
while w do f (w f) fin ¬w
def. of  while
2
(w f) empty ((w f) ; (w f))
3
empty fin ¬w ≡¬w empty
4
(w f) ; (w f)w f ; (w f)
5
(f ; (w f)) fin ¬w f ; ((w f) fin ¬w)
6
f ; ((w f) fin ¬w) f ; while w do f
def. of  while
7
while w do f
1, 2, 3, 4, 5, 6,Prop
(¬w empty) (w (f ; while w do f))
8
while w do f if w then f ; (while w do f) else empty
7,Prop


(while w do f) ; g if w then f ; (while w do f) ; g else g WhileChopEqvIf


Proof:

1
while w do f if w then f ; (while w do f) else empty
2
(while w do f) ; g
if w then (f ; while w do f) ; g else empty ; g
3
(f ; while w do f) ; g f ; (while w do f) ; g
4
empty ; g g
5
(while w do f) ; g if w then f ; (while w do f) ; g else g
2, 3, 4,Prop


f (while w do g) ; h f if w then g ; f else h WhileChopEqvIfRule


Proof:

1
f (while w do g) ; h
given
2
(while w do g) ; h if w then g ; (while w do g) ; h else h
3
g ; f g ; (while w do g) ; h
4
f if w then g ; f else h
1, 2, 3,Prop


while w do f fin ¬w WhileImpFin


Proof:

1
(w f) fin ¬w fin ¬w
2
while w do f fin ¬w
1, def. of  while


while w do f (¬w empty) (w (f more) ; while w do f) WhileEqvEmptyOrChopWhile


Proof:

1
(w f) empty ((w f) more) ; (w f)
2
(w f) more w (f more)
3
((w f) more) ; (w f)(w f more) ; (w f)
4
(w f) empty (w f more) ; (w f)
1, 3,Prop
5
(w f) fin ¬w
(empty fin ¬w) ((w f more) ; (w f) fin ¬w)
1,Prop
6
empty fin ¬w ≡¬w empty
7
(w f more) ; (w f)w (f more) ; (w f)
8
(f more) ; (w f) fin ¬w
(f more) ; ((w f) fin ¬w)
9
(w f) fin ¬w
(¬w empty) (w (f more) ; ((w f) fin ¬w))
5, 6, 7, 8,Prop
10
while w do f
(¬w empty) (w (f more) ; while w do f)
9, def. of  while


¬w f empty WhileIntro
w f (g more) ; f
⇒ ⊢ f while w do g


Proof:

1
⊢ ¬w f empty
given
2
w f (g more) ; f
given
3
while w do g
(¬w empty) (w (g more) ; while w do g)
4
f ¬ while w do g
(g more) ; f ¬((g more) ; while w do g)
1, 2, 3,Prop
5
g more more
6
f while w do g


¬w empty g WhileElim
w (f more) ; g g
⇒ ⊢ while w do f g


Proof:

1
while w do f
(¬w empty) (w (f more) ; while w do f)
2
⊢ ¬w empty g
given
3
w (f more) ; g g
given
4
while w do f ¬g
(f more) ; while w do f ¬((f more) ; g)
1, 2, 3,Prop
5
f more more
6
while w do f g


(f g) (while w do f) (while w do g) BaWhileImpWhile


Proof:

1
(f g) ((w f) (w g)
2
(f g) ((w f) (w g))
3
((w f) (w g)) ((w f)(w g))
4
(f g) ((w f) fin ¬w (w g) fin ¬w)
2, 3,Prop
5
(f g) (while w do f) (while w do g)
4, def. of  while


f g ⇒ ⊢ (while w do f) (while w do g) WhileImpWhile


Proof:

1
f g
given
2
(f g)
3
(f g) (while w do f) (while w do g)
4
(while w do f) (while w do g)
2, 3,MP







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL