| ⊢ (w ∧ w′) ≡ w ∧ w′ | DfStateAndNextEqv |
Proof:
1 | (w ∧ w′) ⌢ true ≡ w ∧ (w′ ⌢ true) | |
2 | (w ∧ w′) ≡ w ∧ w′ | 1, def. of |
3 | w′≡ w′ | |
4 | skip ⌢ w′≡skip ⌢ w′ | |
5 | w′≡ w′ | 4, def. of |
6 | (w ∧ w′) ≡ w ∧ w′ |
qed