| ⊢ | 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) |
qed