| ⊢ | (fin w) ; f ≡ (w ∧ f) | FinChopEqvDiamond |
Proof for ⊃ :
1 | ⊢ (fin w) ; f ≡ (w ∧ f) ∨ ((fin w) ; f) | |
2 | ⊢ (w ∧ f) ≡ (w ∧ f) ∨ (w ∧ f) | |
3 | ⊢ (fin w) ; f ∧¬ (w ∧ f) ≡ ((fin w) ; f) ∧¬ (w ∧ f) | |
4 | ⊢ (fin w) ; f ⊃ (w ∧ f) |
qed
Proof of ⊂:
1 | ⊢ (fin w) ; f ≡ (w ∧ f) ∨ ((fin w) ; f) | |
2 | ⊢ (w ∧ f) ≡ (w ∧ f) ∨ (w ∧ f) | |
3 | ⊢ (w ∧ f) ∧¬((fin w) ; f) ≡ (w ∧ f) ∧¬ ((fin w) ; f) | |
4 | ⊢ (w ∧ f) ⊃ (fin w) ; f |
qed
The following important theorem demonstrates how to pass information from the final state of a subinterval to the starting state of a subinterval immediately following it.