### 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)∗∧ ﬁn ¬w def. of  while 2 ⊢ (w ∧ f)∗≡ empty ∨ ((w ∧ f) ; (w ∧ f)∗) 3 ⊢ empty ∧ ﬁn ¬w ≡¬w ∧ empty 4 ⊢ (w ∧ f) ; (w ∧ f)∗≡ w ∧ f ; (w ∧ f)∗ 5 ⊢ (f ; (w ∧ f)∗) ∧ ﬁn ¬w ≡ f ; ((w ∧ f)∗∧ ﬁn ¬w) 6 ⊢ f ; ((w ∧ f)∗∧ ﬁn ¬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 ⊃ ﬁn ¬w WhileImpFin

Proof:

 1 ⊢ (w ∧ f)∗∧ ﬁn ¬w ⊃ ﬁn ¬w 2 ⊢ while w do f ⊃ ﬁn ¬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)∗∧ ﬁn ¬w ≡ (empty ∧ ﬁn ¬w) ∨ ((w ∧ f ∧ more) ; (w ∧ f)∗∧ ﬁn ¬w) 1,Prop 6 ⊢ empty ∧ ﬁn ¬w ≡¬w ∧ empty 7 ⊢ (w ∧ f ∧ more) ; (w ∧ f)∗≡ w ∧ (f ∧ more) ; (w ∧ f)∗ 8 ⊢ (f ∧ more) ; (w ∧ f)∗∧ ﬁn ¬w ≡ (f ∧ more) ; ((w ∧ f)∗∧ ﬁn ¬w) 9 ⊢ (w ∧ f)∗∧ ﬁn ¬w ≡ (¬w ∧ empty) ∨ (w ∧ (f ∧ more) ; ((w ∧ f)∗∧ ﬁn ¬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) WhileEqvEmptyOrChopWhile 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 4, 5,ChopContra

 ⊢ ¬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) WhileEqvEmptyOrChopWhile 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 4, 5,ChopContra

 ⊢ (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)) 1,BaImpBa 3 ⊢ ((w ∧ f) ⊃(w ∧ g)) ⊃ ((w ∧ f)∗⊃(w ∧ g)∗) 4 ⊢ (f ⊃g) ⊃ ((w ∧ f)∗∧ ﬁn ¬w ⊃(w ∧ g)∗∧ ﬁn ¬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) 1,BaGen 3 ⊢ (f ⊃g) ⊃ (while w do f) ⊃(while w do g) BaWhileImpWhile 4 ⊢ (while w do f) ⊃ (while w do g) 2, 3,MP

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