| ⊢ | w ∧ f ⊃ f1 ∧fin w1 | ChopRepAndFin | |
| ⊢ | w1 ∧ g ⊃ g1 ∧fin w2 | ||
| ⇒ ⊢ | w ∧ (f ; g) ⊃ (f1 ; g1) ∧fin w2 |
Proof:
1 | ⊢ w ∧ f ⊃ f1 ∧fin w1 | given |
2 | ⊢ w1 ∧ g ⊃ g1 ∧fin w2 | given |
3 | ⊢ w ∧ (f ; g) ⊃ f1 ; (g1 ∧fin w2) | |
4 | ⊢ f1 ; (g1 ∧fin w2) ⊃ f1 ; g1 | |
5 | ⊢ f1 ; (g1 ∧fin w2) ⊃ f1 ; fin w2 | |
6 | ⊢ f1 ; fin w2 ⊃fin w2 | |
7 | ⊢ w ∧ (f ; g) ⊃ (f1 ; g1) ∧fin w2 |
qed
The following lemma is used in MoreChopLoop.
| ⊢ | true ; more ≡more | TrueChopMoreEqvMore |