| ⊢ | (f1 ; … ; fm) ; (g1 ; … ; gn) ≡ f1 ; … ; fm ; g1 ; … ; gn | ChopGroupMerge |
We prove this by induction on m.
Proof for m=1:
1 | ⊢ f1 ; (g1 ; … ; gn) ≡ f1 ; g1 ; … ; gn | def. of < chop > |
qed
Proof for m > 1:
1 | ⊢ (f1 ; f2 ; … ; fm) ; (g1 ; … ; gn) ≡ |
|
f1 ; ((f2 ; … ; fm) ; (g1 ; … ; gn)) | ||
2 | ⊢ (f2 ; … ; fm) ; (g1 ; … ; gn) ≡ |
|
f2 ; … ; fm ; g1 ; … ; gn | induction hypothesis |
|
3 | ⊢ f1 ; ((f2 ; … ; fm) ; (g1 ; … ; gn)) ≡ |
|
f1 ; (f2 ; … ; fm ; g1 ; … ; gn) | ||
4 | ⊢ (f1 ; f2 ; … ; fm) ; (g1 ; … ; gn) ≡ |
|
f1 ; f2 ; … ; fm ; g1 ; … ; gn |
qed