| ⊢ | (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) | |
5 | ⊢ (f ⊃ g) ⊃ (while w do f) ⊃ (while w do g) | 4, def. of while |
qed