Properties of groups of chops

ITL

© 1996-2018

11 Properties of groups of chops

⊢

(f₁ ; … ; f_m) ; (g₁ ; … ; g_n) ≡ f₁ ; … ; f_m ; g₁ ; … ; g_n

ChopGroupMerge

We prove this by induction on m.
Proof for m=1:

1

⊢ f₁ ; (g₁ ; … ; g_n) ≡ f₁ ; g₁ ; … ; g_n

def. of < chop >

Proof for m > 1:

1	⊢ (f₁ ; f₂ ; … ; f_m) ; (g₁ ; … ; g_n) ≡
	f₁ ; ((f₂ ; … ; f_m) ; (g₁ ; … ; g_n))	ChopAssoc
2	⊢ (f₂ ; … ; f_m) ; (g₁ ; … ; g_n) ≡
	f₂ ; … ; f_m ; g₁ ; … ; g_n	induction hypothesis
3	⊢ f₁ ; ((f₂ ; … ; f_m) ; (g₁ ; … ; g_n)) ≡
	f₁ ; (f₂ ; … ; f_m ; g₁ ; … ; g_n)	2,RightChopEqvChop
4	⊢ (f₁ ; f₂ ; … ; f_m) ; (g₁ ; … ; g_n) ≡
	f₁ ; f₂ ; … ; f_m ; g₁ ; … ; g_n	1, 3,EqvChain

⊢	(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₁

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

⊢

f ; f ; … ; f ⊃ f^∗

ChopGroupImpCS

The proof is by induction on the number of <chops>.
Proof when no <chops>:

1

⊢ f ⊃ f^∗

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^∗	1,LeftChopImpChop
3	⊢ f ; f^∗⊃ f^∗	ChopCSImpCS
4	⊢ f ; f ; … ; f ⊃ f^∗	2, 3,ImpChain

⊢

f₁ ⊃g, …, ⊢ f_n ⊃g ⇒ ⊢ (f₁ ; … ; f_n) ⊃ g^∗

MultChopImpCS

Proof:

1	⊢ f_i ⊃ g, for 1 ≤ i ≤ n	given
2	⊢ f₁ ; … ; f_n ⊃ g ; … ; g	1,MultChopImpChop
3	⊢ g ; … ; g ⊃ g^∗	ChopGroupImpCS
4	⊢ f₁ ; … ; f_n ⊃ g^∗	2, 3,ImpChain

⊢	w ∧ f ⊃g ; (w₁ ∧ f₁), ⊢ w₁ ∧ f₁ ⊃g₁ ; (w₂ ∧ f₂)		NestedChopImpChop
	⇒ ⊢ w ∧ f ⊃g ; g₁ ; (w₂ ∧ f₂)

Proof:

1	⊢ w ∧ f ⊃ g ; (w₁ ∧ f₁)	given
2	⊢ w₁ ∧ f₁ ⊃ g₁ ; (w₂ ∧ f₂)	given
3	⊢ g ; (w₁ ∧ f₁) ⊃ g ; g₁ ; (w₂ ∧ f₂)	2,RightChopImpChop
4	⊢ w ∧ f ⊃ g ; g₁ ; (w₂ ∧ f₂)	1, 3,ImpChain

⊢	w₁ ∧ f₁ ⊃g₁ ; (w₂ ∧ f₂),…,⊢ w_n−1 ∧ f_n−1 ⊃g_n−1 ; (w_n ∧ f_n)		MultNestedChopImpChop
	⇒ ⊢ w₁ ∧ f₁ ⊃g₁ ; … ; g_n−1 ; (w_n ∧ g_n)

The proof is by induction on n.
Proof for n = 1:

1

⊢ w₁ ∧ f₁ ⊃ w₁ ∧ f₁

Proof for n > 1:

1	⊢ w₁ ∧ f₁ ⊃ g₁ ; (w₂ ∧ f₂)	given
2	⊢ w_i ∧ f_i ⊃ g_i ; (w_i+1 ∧ f_i+1), for each i: 1 < i < n	given
3	⊢ w₂ ∧ f₂ ⊃ g₂ ; … ; g_n−1 ; (w_n ∧ g_n)	2, induction hypothesis
4	⊢ w₁ ∧ f₁ ⊃ g₁ ; g₂ ; … ; g_n−1 ; (w_n ∧ g_n)	1, 3,NestedChopImpChop

2018-02-26

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