ChopGroupGroupMerge

ChopGroupGroupMerge

⊢	(f_1,1 ; … ; f_1,l₁) ; … ; (f_n,1 ; … ; f_{n,l_n}) ≡		ChopGroupGroupMerge
	f_1,1 ; … ; f_1,l₁ ; … ; f_n,1 ; … ; f_{n,l_n},

where there are n groups and for each group 1 ≤ i < n, there are l_i formulas. Proof is by induction on n.

Proof for n = 1:

1

⊢ f_1,1 ; … ; f_1,l₁ ≡ f_1,1 ; … ; f_1,l₁

qed

Proof for n > 1:

1	⊢ (f_2,1 ; … ; f_2,l₂) ; … ; (f_n,1 ; … ; f_{n,l_n}) ≡
	f_2,1 ; … ; f_2,l₂ ; … ; f_n,1 ; … ; f_{n,l_n}	induction hypothesis

2	⊢ (f_1,1 ; … ; f_1,l₁) ; (f_2,1 ; … ; f_2,l₂) ; … ; (f_n,1 ; … ; f_{n,l_n}) ≡
	(f_1,1 ; … ; f_1,l₁) ; (f_2,1 ; … ; f_2,l₂ ; … ; f_n,1 ; … ; f_{n,l_n})	1,LeftChopEqvChop
3	⊢ (f_1,1 ; … ; f_1,l₁) ; (f_2,1 ; … ; f_2,l₂ ; … ; f_n,1 ; … ; f_{n,l_n}) ≡
	f_1,1 ; … ; f_1,l₁ ; f_2,1 ; … ; f_2,l₂ ; … ; f_n,1 ; … ; f_{n,l_n}	ChopGroupMerge
4	⊢ (f_1,1 ; … ; f_1,l₁) ; (f_2,1 ; … ; f_2,l₂) ; … ; (f_n,1 ; f_n,2 ; … ; f_{n,l_n}) ≡
	f_1,1 ; … ; f_1,l₁ ; f_2,1 ; … ; f_2,l₂ ; … ; f_n,1 ; … ; f_{n,l_n}	2, 3,EqvChain

qed

2024-08-03

Contact | Home | ITL home | Course | Proofs | Algebra | FL

© 1996-2024