| ⊢ T until f ≡ f ∨ (T ∧ (T until f)) | UntilEqv |
Proof:
1 | skip ∧ T ⊃ more | |
2 | (skip ∧ T)⋆ ⌢ f ≡ f ∨ ((skip ∧ T) ⌢ ((skip ∧ T)⋆ ⌢ f)) | |
3 | T until f ≡ f ∨ ((skip ∧ T) ⌢ (T until f)) | 2, def. of until |
4 | (skip ∧ T) ⌢ (T until f) ≡ T ∧ (T until f) | |
5 | T until f ≡ f ∨ (T ∧ (T until f)) |
qed