| ⊢ | f ; f ; … ; f ⊃ f∗ | ChopGroupImpCS |
The proof is by induction on the number of ¡chops¿.
Proof when no ¡chops¿:
1 | ⊢ f ⊃ f∗ |
qed
Proof for at n occurrences of ¡chops¿ where n ≥ 1:
1 | ⊢ f ; … ; f ⊃ f∗ | induction for n − 1 ¡chops¿ |
2 | ⊢ f ; f ; … ; f ⊃ f ; f∗ | |
3 | ⊢ f ; f∗⊃ f∗ | |
4 | ⊢ f ; f ; … ; f ⊃ f∗ |
qed