#### 2.5 Properties of chop-plus

 ⊢ f ⊃ f+ ImpChopPlus

Proof:

 1 ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ ChopPlusEqv 2 ⊢ f ⊃ f+ 1,Prop

qed

 ⊢ f ; f+ ⊃ f+ ChopChopPlusImpChopPlus

Proof:

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

qed

 ⊢ f+ ≡ f ∨ (f ; f+) ChopPlusEqvOrChopChopPlus

Proof for :

 1 ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ ChopPlusEqv 2 ⊢ (f ∧ more) ; f+ ⊃ f ; f+ 3 ⊢ f+ ⊃ f ∨ f ; f+ 1, 2,Prop

qed

Proof for :

 1 ⊢ f ⊃ 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 ⊢ f ∨ (f ; f+) ⊃ f+ 1, 6,Prop

qed

 ⊢ f ∧¬g ⊃ (g ∧ more) ; f ⇒ ⊢ f ⊃ g+ ChopPlusIntro

Proof:

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

qed

 ⊢ f ⊃g, ⊢ (f ∧ more) ; g ⊃g ⇒ ⊢ f+ ⊃g ChopPlusElim

Proof:

 1 ⊢ f+ ≡ f ∨ (f ∧ more) ; f+ 2 ⊢ f ⊃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

 ⊢ f ⊃g, ⊢ f ; g ⊃g ⇒ ⊢ f+ ⊃g ChopPlusElimWithoutMore

Proof:

 1 ⊢ f ⊃ 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,ChopPlusElim

qed

 ⊢ f ⊃g ⇒ ⊢ f+ ⊃g+ ChopPlusImpChopPlus

Proof:

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

qed

 ⊢ f ≡ g ⇒ ⊢ f+ ≡ g+ ChopPlusEqvChopPlus

Proof:

 1 ⊢ f ≡ g given 2 ⊢ f ⊃ g 1,Prop 3 ⊢ f+ ⊃ g+ 4 ⊢ g ⊃ f 1,Prop 5 ⊢ g+ ⊃ f+ 6 ⊢ f+ ≡ g+ 3, 5,Prop

qed

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