| ⊢ (skip ∧ T) ⌢ f ≡ T ∧ f | NLoneAndSkipChopEqvNLoneAndNext |
Proof for ⊃:
1 | (skip ∧ T) ⌢ f ⊃ (skip ∧ T) | |
2 | (skip ∧ T) ≡more ∧ T | |
3 | (skip ∧ T) ⌢ f ⊃ T | |
4 | (skip ∧ T) ⌢ f ⊃ skip ⌢ f | |
5 | (skip ∧ T) ⌢ f ⊃ f | 4, def. of |
6 | (skip ∧ T) ⌢ f ⊃ T ∧ f |
qed
Proof for ⊂:
1 | f ⊃ more | |
2 | more ∧ T ⊃ (more ⊃ T) | |
3 | T ∧ f ⊃ (more ⊃ T) | |
4 | (more ⊃ T) ∧ f ⊃ (skip ∧ T) ⌢ f | |
5 | T ∧ f ⊃ (skip ∧ T) ⌢ f |
qed