#### 2.6 Properties of chop-star

 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ CSEqv

Proof:

 1 ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ ChopPlusEqv 2 ⊢ empty ≡¬more 3 ⊢ empty ∨ f+ ≡ empty ∨ (f ∧ more) ∨ (f ∧ more) ; f+ 1, 2,Prop 4 ⊢ (f ∧ more) ; empty ≡ f ∧ more 5 ⊢ (f ∧ more) ; (empty ∨ f+) ≡ (f ∧ more) ; empty ∨ (f ∧ more) ; f+ 6 ⊢ empty ∨ f+ ≡ empty ∨ ((f ∧ more) ; (empty ∨ f+)) 3, 4, 5,Prop 7 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ 6, def. of ∗

qed

 ⊢ empty ⊃ f∗ EmptyImpCS

Proof:

 1 ⊢ f∗≡ empty ∨ f+ def. of ∗ 2 ⊢ empty ⊃ f∗ 1,Prop

qed

Here is an straightforward corollary:

 ⊢ ¬f∗⊃ more NotCSImpMore

 ⊢ f+ ⊃ f∗ ChopPlusImpCS

Proof:

 1 ⊢ f+ ⊃ empty ∨ f+ 2 ⊢ f+ ⊃ f∗ 1, def. of ∗

qed

 ⊢ f ⊃ f∗ ImpCS

Proof:

 1 ⊢ f ⊃ f+ ImpChopPlus 2 ⊢ f ⊃ empty ∨ f+ 1,Prop 3 ⊢ f ⊃ f∗ 2, def. of ∗

qed

 ⊢ f∗ ; g ≡ g ∨ f+ ; g CSChopEqvOrChopPlusChop

Proof:

 1 ⊢ f∗≡ empty ∨ f+ def. of ∗ 2 ⊢ f∗ ; g ≡ g ∨ f+ ; g

qed

 ⊢ f∗≡ empty ∨ (f ; f∗) CSEqvOrChopCS

Proof for :

 1 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ 2 ⊢ (f ∧ more) ; f∗⊃ f ; f∗ AndChopA 3 ⊢ f∗⊃ empty ∨ f ; f∗ 1, 2,Prop

qed

Proof for :

 1 ⊢ empty ⊃ f∗ 2 ⊢ empty ∨ more 3 ⊢ f ⊃ empty ∨ (f ∧ more) 2,Prop 4 ⊢ f ; f∗⊃ f∗∨ (f ∧ more) ; f∗ 5 ⊢ f∗≡ f ∨ (f ∧ more) ; f∗ 6 ⊢ (f ∧ more) ; f∗⊃ f∗ 5,Prop 7 ⊢ empty ∨ (f ; f∗) ⊃ f∗ 1, 6,Prop

qed

 ⊢ f ; f∗⊃ f∗ ChopCSImpCS

Proof:

 1 ⊢ f∗≡ empty ∨ (f ; f∗) CSEqvOrChopCS 2 ⊢ f ; f∗⊃ f∗ 1,Prop

qed

 ⊢ f∗∧ more ⊃ f+ CSAndMoreImpChopPlus

Proof:

 1 ⊢ f∗∧ more ⊃ f ; f∗ CSAndMoreImpChopCS 2 ⊢ f∗∧ more ⊃ f+ 1, def. of +

qed

 ⊢ f∗∧ more ≡ (f ∧ more) ; f∗ CSAndMoreEqvAndMoreChop

Proof for :

 1 ⊢ (empty ∨ (f ∧ more) ; f∗) ∧ more ⊃ (f ∧ more) ; f∗ 2 ⊢ f∗∧ more ⊃ (f ∧ more) ; f∗ 1, def. of ∗

qed

Proof for :

 1 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ 2 ⊢ (f ∧ more) ; f∗⊃ f∗ 1,Prop 3 ⊢ (f ∧ more) ; f∗⊃ more MoreChopImpMore 4 ⊢ (f ∧ more) ; f∗⊃ f∗∧ more 2, 3,Prop

qed

 ⊢ f∗∧ more ⊃ f ; f∗ CSAndMoreImpChopCS

Proof:

 1 ⊢ f∗∧ more ≡ (f ∧ more) ; f∗ CSAndMoreEqvAndMoreChop 2 ⊢ (f ∧ more) ; f∗⊃ f ; f∗ 3 ⊢ f∗∧ more ⊃ f ; f∗ 1, 2,Prop

qed

 ⊢ f∗∧ more ⊃ f∗ ; f CSAndMoreImpCSChop

Proof:

 1 ⊢ f∗∧ more ≡ (f ∧ more) ; f∗ 2 ⊢ empty ∨ more 3 ⊢ f∗⊃ empty ∨ (f∗∧ more) 2,Prop 4 ⊢ (f ∧ more) ; f∗⊃ (f ∧ more) ∨ ((f ∧ more) ; (f∗∧ more)) 5 ⊢ f∗∧ more ∧¬f ⊃ (f ∧ more) ; (f∗∧ more) CSMoreNotImpChopCSAndMore 6 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ 7 ⊢ f∗ ; f ≡ f ∨ ((f ∧ more) ; f∗) ; f 8 ⊢ ((f ∧ more) ; f∗) ; f ≡ (f ∧ more) ; (f∗ ; f) 9 ⊢ (f∗∧ more) ∧¬(f∗ ; f) ⊃ (f ∧ more) ; (f∗∧ more) ∧¬((f ∧ more) ; (f∗ ; f)) 5, 7, 8,Prop 10 ⊢ f ∧ more ⊃ more 11 ⊢ f∗∧ more ⊃ f∗ ; f 9, 10,ChopContra

qed

The following lemma is used in the proof of CSAndMoreImpCSChop:

 ⊢ f∗∧ more ∧¬f ⊃ (f ∧ more) ; (f∗∧ more) CSMoreNotImpChopCSAndMore

Proof:

 1 ⊢ f∗∧ more ≡ (f ∧ more) ; f∗ CSAndMoreEqvAndMoreChop 2 ⊢ empty ∨ more 3 ⊢ f∗⊃ empty ∨ (f∗∧ more) 2,Prop 4 ⊢ (f ∧ more) ; f∗⊃ (f ∧ more) ∨ ((f ∧ more) ; (f∗∧ more)) 5 ⊢ (f ∧ more) ; f∗∧ more ∧¬f ⊃ (f ∧ more) ; (f∗∧ more) 4,Prop 6 ⊢ f∗∧ more ∧¬f ⊃ (f ∧ more) ; (f∗∧ more) 1, 5,Prop

qed

 ⊢ f∗ ; f∗⊃ f∗ CSChopCSImpCS

Proof:

 1 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ 2 ⊢ f∗ ; f∗≡ f∗∨ ((f ∧ more) ; f∗) ; f∗ 3 ⊢ f∗ ; f∗∧¬(f∗) ⊃ ((f ∧ more) ; f∗) ; f∗∧¬((f ∧ more) ; f∗) 1, 2,Prop 4 ⊢ ((f ∧ more) ; f∗) ; f∗≡ (f ∧ more) ; f∗ ; f∗ 5 ⊢ f∗ ; f∗∧¬(f∗) ⊃ (f ∧ more) ; f∗ ; f∗∧¬((f ∧ more) ; f∗) 3, 4,Prop 6 ⊢ f ∧ more ⊃ more 7 ⊢ f∗ ; f∗⊃ f∗ 5, 6,ChopContra

qed

 ⊢ f∗ ; f ⊃ f∗ CSChopImpCS

Proof:

 1 ⊢ f ⊃ f∗ 2 ⊢ f∗ ; f ⊃ f∗ ; f∗ 3 ⊢ f∗ ; f∗⊃ f∗ 4 ⊢ f∗ ; f ⊃ f∗ 2, 3,ImpChain

qed

 ⊢ (f∗)∗⊃ f∗ CSCSImpCS

Proof:

 1 ⊢ empty ⊃ f∗ 2 ⊢ (f∗∧ more) ; f∗⊃ f∗ ; f∗ 3 ⊢ f∗ ; f∗⊃ f∗ CSChopCSImpCS 4 ⊢ (f∗∧ more) ; f∗⊃ f∗ 2, 3,ImpChain 5 ⊢ (f∗)∗⊃ f∗ 1, 4,CSElim

qed

 ⊢ f ⊃g ⇒ ⊢ f∗⊃g∗ CSImpCS

Proof:

 1 ⊢ f ⊃ g given 2 ⊢ f+ ⊃ g+ 3 ⊢ empty ∨ f+ ⊃ empty ∨ g+ 2,Prop 4 ⊢ f∗⊃ g∗ 3, def. of ∗

qed

 ⊢ f ≡ g ⇒ ⊢ f∗≡ g∗ CSEqvCS

Proof:

 1 ⊢ f ≡ g given 2 ⊢ f+ ≡ g+ 3 ⊢ empty ∨ f+ ≡ empty ∨ g+ 2,Prop 4 ⊢ f∗≡ g∗ 3, def. of ∗

qed

 ⊢ (f ∧ g)∗⊃ f∗ AndCSA

Proof:

 1 ⊢ f ∧ g ⊃ f 2 ⊢ (f ∧ g)∗⊃ f∗ 1,CSImpCS

qed

 ⊢ (f ∧ g)∗⊃ g∗ AndCSB

Proof:

 1 ⊢ f ∧ g ⊃ g 2 ⊢ (f ∧ g)∗⊃ g∗ 1,CSImpCS

qed

 ⊢ f ∧ more ⊃(g ∧ more) ; f ⇒ ⊢ f ⊃g∗ CSIntro

Proof:

 1 ⊢ f ∧ more ⊃ (g ∧ more) ; f given 2 ⊢ more ≡¬empty 3 ⊢ f ∧¬empty ⊃ (g ∧ more) ; f 1, 2,Prop 4 ⊢ g∗≡ empty ∨ (g ∧ more) ; g∗ 5 ⊢ f ∧¬g∗⊃ (g ∧ more) ; f ∧¬((g ∧ more) ; g∗) 3, 4,Prop 6 ⊢ g ∧ more ⊃ more 7 ⊢ f ⊃ g∗ 5, 6,ChopContra

qed

 ⊢ empty ⊃g, ⊢ (f ∧ more) ; g ⊃g ⇒ ⊢ f∗⊃g CSElim

Proof:

 1 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ 2 ⊢ empty ⊃g given 3 ⊢ (f ∧ more) ; g ⊃g given 4 ⊢ f∗∧¬g ⊃ (f ∧ more) ; f∗∧¬((f ∧ more) ; g) 1, 2, 3,Prop 5 ⊢ f ∧ more ⊃ more 6 ⊢ f∗⊃ g 4, 5,ChopContra

qed

 ⊢ empty ⊃g, ⊢ f ; g ⊃g ⇒ ⊢ f∗⊃g CSElimWithoutMore

Proof:

 1 ⊢ empty ⊃ g given 2 ⊢ f ; g ⊃ g given 3 ⊢ (f ∧ more) ; g ⊃ f ; g 4 ⊢ (f ∧ more) ; g ⊃ g 2, 3,ImpChain 5 ⊢ f∗⊃ g 1, 4,CSElim

qed

 ⊢ f ≡ g∗ ; h ⇒ ⊢ f ≡ (g ; f) ∨ h CSChopEqvChopOrRule

Proof:

 1 ⊢ f ≡ g∗ ; h given 2 ⊢ g∗≡ empty ∨ (g ; g∗) 3 ⊢ g∗ ; h ≡ h ∨ ((g ; g∗) ; h) 4 ⊢ (g ; g∗) ; h ≡ g ; (g∗ ; h) ChopAssoc 5 ⊢ g ; f ≡ g ; (g∗ ; h) 6 ⊢ f ≡ (g ; f) ∨ h 1, 3, 4, 5,Prop

qed

 ⊢ f ∧¬h ⊃g ; f, ⊢ g ⊃more ⇒ f ⊃g∗ ; h CSChopIntroRule

Proof:

 1 ⊢ f ∧¬h ⊃ g ; f given 2 ⊢ g ⊃ more given 3 ⊢ g ⊃ g ∧ more 2,Prop 4 ⊢ g ; f ⊃ (g ∧ more) ; f 5 ⊢ f ⊃ (g ∧ more) ; f ∨ h 1, 4,Prop 6 ⊢ g∗≡ empty ∨ (g ∧ more) ; g∗ 7 ⊢ g∗ ; h ≡ h ∨ ((g ∧ more) ; g∗) ; h 8 ⊢ ((g ∧ more) ; g∗) ; h ≡ (g ∧ more) ; (g∗ ; h) 9 ⊢ g∗ ; h ≡ h ∨ (g ∧ more) ; (g∗ ; h) 7, 8,Prop 10 ⊢ f ∧¬(g∗ ; h) ⊃ (g ∧ more) ; f ∧¬((g ∧ more) ; (g∗ ; h)) 5, 9,Prop 11 ⊢ g ∧ more ⊃ more 12 ⊢ f ⊃ g∗ ; h 10, 11,ChopContra

qed

 ⊢ f ⊃empty ∨ ( w ∧ more) ; f ⇒ ⊢ w ∧ f ⊃w CSImpBox

Proof:

 1 ⊢ f ⊃ empty ∨ ( w ∧ more) ; f given 2 ⊢ w ∧¬w ⊃¬empty 3 ⊢ w ∧ f ∧¬w ⊃ ( w ∧ more) ; f 1, 2,Prop 4 ⊢ w ∧ more ⊃ ( w ∧ more) ∧ ﬁn w 5 ⊢ ( w ∧ more) ; f ⊃ (( w ∧ more) ∧ ﬁn w) ; f 6 ⊢ (( w ∧ more) ∧ ﬁn w) ; f ≡ ( w ∧ more) ; (w ∧ f) 7 ⊢ ¬w ⊃ ( w) ¬w NotBoxStateImpBoxYieldsNotBox 8 ⊢ ( w) ¬w ⊃ ( w ∧ more) ¬w 9 ⊢ ( w ∧ more) ; (w ∧ f) ∧ ( w ∧ more) ¬w ⊃ ( w ∧ more) ; ((w ∧ f) ∧¬w) 10 ⊢ (w ∧ f) ∧¬w ⊃ ( w ∧ more) ; ((w ∧ f) ∧¬w) 3, 5, 6, 7, 8, 9,Prop 11 ⊢ ( w ∧ more) ; ((w ∧ f) ∧¬w) ⊃ more ; ((w ∧ f) ∧¬w) 12 ⊢ (w ∧ f) ∧¬w ⊃ more ; ((w ∧ f) ∧¬w) 10, 11,ImpChain 13 ⊢ w ∧ f ⊃w

qed

 ⊢ w ∧ ( w)∗≡w BoxCSEqvBox

Proof for :

 1 ⊢ ( w)∗≡ empty ∨ ( w ∧ more) ; ( w)∗ 2 ⊢ ( w)∗⊃ empty ∨ ( w ∧ more) ; ( w)∗ 1,Prop 3 ⊢ w ∧ ( w)∗⊃w 2,CSImpBox

qed

Proof for :

 1 ⊢ w ⊃ w 2 ⊢ w ⊃ ( w)∗ 3 ⊢ w ⊃ w ∧ ( w)∗ 1, 2,Prop

qed

 ⊢ w ∧ f∗≡ w ∧ ( w ∧ f)∗ BoxStateAndCSEqvCS

Proof for :

 1 ⊢ w ⊃ w 2 ⊢ f∗∧ more ≡ (f ∧ more) ; f∗ CSAndMoreEqvAndMoreChop 3 ⊢ w ∧ ((f ∧ more) ; f∗) ≡ ( w ∧ f ∧ more) ; ( w ∧ f∗) 4 ⊢ w ∧ f ∧ more ⊃ ( w ∧ f) ∧ more 5 ⊢ ( w ∧ f ∧ more) ; ( w ∧ f∗) ⊃ (( w ∧ f) ∧ more) ; ( w ∧ f∗) 6 ⊢ ( w ∧ f∗) ∧ more ⊃ (( w ∧ f) ∧ more) ; ( w ∧ f∗) 2, 3, 5,Prop 7 ⊢ w ∧ f∗⊃ ( w ∧ f)∗ 6,CSIntro 8 ⊢ w ∧ f∗⊃ w ∧ ( w ∧ f)∗ 1, 7,Prop

qed

Proof for :

 1 ⊢ ( w ∧ f)∗⊃ ( w)∗ 2 ⊢ w ∧ ( w)∗≡w BoxCSEqvBox 3 ⊢ ( w ∧ f)∗⊃ f∗ 4 ⊢ w ∧ ( w ∧ f)∗⊃w ∧ f∗ 1, 2, 3,Prop

qed

 ⊢ (f ⊃g) ⊃ f∗⊃g∗ BaCSImpCS

Proof:

 1 ⊢ f∗≡ empty ∨ (f ∧ more) ; f∗ 2 ⊢ g∗≡ empty ∨ (g ∧ more) ; g∗ 3 ⊢ f∗∧¬(g∗) ⊃ (f ∧ more) ; f∗∧¬((g ∧ more) ; g∗) 1, 2,Prop 4 ⊢ (f ⊃g) ⊃ (f ∧ more ⊃ g ∧ more) 5 ⊢ (f ⊃g) ⊃(f ∧ more ⊃ g ∧ more) 4,BaImpBa 6 ⊢ (f ∧ more ⊃ g ∧ more) ⊃ (f ∧ more) ; f∗⊃ (g ∧ more) ; f∗ 7 ⊢ (f ⊃g) ∧ (f ∧ more) ; f∗⊃ (g ∧ more) ; f∗ 5, 6,Prop 8 ⊢ (g ∧ more) ; f∗∧¬((g ∧ more) ; g∗) ⊃ (g ∧ more) ; (f∗∧¬(g∗)) ChopAndNotChopImp 9 ⊢ (g ∧ more) ; (f∗∧¬(g∗)) ⊃ more ; (f∗∧¬(g∗)) 10 ⊢ (f ⊃g) ⊃ more ; (f∗∧¬(g∗)) ⊃ more ; ((f ⊃g) ∧ f∗∧¬(g∗)) 11 ⊢ (f ⊃g) ∧ f∗∧¬(g∗) ⊃ more ; ((f ⊃g) ∧ f∗∧¬(g∗)) 3, 7, 8, 9, 10,Prop 12 ⊢ ¬((f ⊃g) ∧ f∗∧¬(g∗)) 11,MoreChopLoop 13 ⊢ (f ⊃g) ⊃ f∗⊃g∗ 12,Prop

qed

The following corollary can be readily veriﬁed:

 ⊢ (f ≡ g) ⊃ f∗≡ g∗ BaCSEqvCS

 ⊢ f ∧ g∗⊃ (f ∧ g)∗ BaAndCSImport

Proof:

 1 ⊢ f ⊃ (g ⊃f ∧ g) 2 ⊢ f ⊃(g ⊃f ∧ g) 1,BaImpBa 3 ⊢ (g ⊃f ∧ g) ⊃ g∗⊃(f ∧ g)∗ BaCSImpCS 4 ⊢ f ∧ g∗⊃ (f ∧ g)∗ 2, 3,Prop

qed

 2019-01-03 Contact | Home | ITL home | Course | Proofs | Algebra | FL