⊢ | (f1,1 ; … ; f1,l1) ; … ; (fn,1 ; … ; fn,ln) ≡ | ChopGroupGroupMerge | |
f1,1 ; … ; f1,l1 ; … ; fn,1 ; … ; fn,ln, |
where there are n groups and for each group 1 ≤ i < n, there are li formulas. Proof is by induction on n.
Proof for n = 1:
1 | ⊢ f1,1 ; … ; f1,l1 ≡ f1,1 ; … ; f1,l1 |
qed
Proof for n > 1:
1 | ⊢ (f2,1 ; … ; f2,l2) ; … ; (fn,1 ; … ; fn,ln) ≡ |
|
f2,1 ; … ; f2,l2 ; … ; fn,1 ; … ; fn,ln | induction hypothesis |
|
2 | ⊢ (f1,1 ; … ; f1,l1) ; (f2,1 ; … ; f2,l2) ; … ; (fn,1 ; … ; fn,ln) ≡ |
|
(f1,1 ; … ; f1,l1) ; (f2,1 ; … ; f2,l2 ; … ; fn,1 ; … ; fn,ln) | ||
3 | ⊢ (f1,1 ; … ; f1,l1) ; (f2,1 ; … ; f2,l2 ; … ; fn,1 ; … ; fn,ln) ≡ |
|
f1,1 ; … ; f1,l1 ; f2,1 ; … ; f2,l2 ; … ; fn,1 ; … ; fn,ln | ||
4 | ⊢ (f1,1 ; … ; f1,l1) ; (f2,1 ; … ; f2,l2) ; … ; (fn,1 ; fn,2 ; … ; fn,ln) ≡ |
|
f1,1 ; … ; f1,l1 ; f2,1 ; … ; f2,l2 ; … ; fn,1 ; … ; fn,ln | ||
qed