ITL
© 1996-2018







8.1 Some Basic Properties of Chop

We now consider deducing various simple properties of chop and the associated operators , , and which have a wide range of uses.

(f f1) (f g) (f1 g) BfChopImpChop

Proof:

1
g g
2
(g g)
3
(f f1) (g g) (f g) (f1 g)
4
(f f1) (f g) (f1 g)
2, 3,Prop

qed

(g g1) (f g) (f g1) BoxChopImpChop

Proof:

1
finite (f f)
2
(f f)
3
(f f) (g g1) (f g) (f g1)
4
(g g1) (f g) (f g1)
2, 3,Prop

qed

(g g1) (f g) (f g1) BoxChopEqvChop

Proof:

1
(g g1) (g g1) (g1 g)
2
(g g1) (f g) (f g1)
3
(g1 g) (f g1) (f g)
4
(g g1) (f g) (f g1)
2, 3,Prop

qed

The following derived variant of Inference Rule BfFGen omits the subformula finite:

f ⇒ ⊢ f BfGen

Proof:

1
f
Assump
2
finite f
1,Prop
3
f

qed

The derived inference rule BfGen can also be referred to as Gen (analogous to the inference rule BoxGen).

f f1 ⇒ ⊢ (f g) (f1 g) LeftChopImpChop

Proof:

1
f f1
Assump
2
(f f1)
3
(f f1) (f g) (f1 g)
4
f g f1 g
2, 3,MP

qed

f f1 ⇒ ⊢ (f g) (f1 g) LeftChopEqvChop

Proof:

1
f f1
Assump
2
f f1
1,Prop
3
f g f1 g
4
f1 f
1,Prop
5
f1 g f g
6
f g f1 g
3, 5,Prop

qed

f g ⇒ ⊢ f g DfImpDf

Proof:

1
f g
Assump
2
f true g true
3
f g
2, def. of 

qed

f g ⇒ ⊢ f g DfEqvDf

Proof:

1
f g
Assump
2
f true g true
3
f g
2, def. of 

qed

g g1 ⇒ ⊢ (f g) (f g1) RightChopImpChop

Proof:

1
g g1
Assump
2
(g g1)
3
(g g1) (f g) (f g1)
4
f g f g1
2, 3,MP

qed

g g1 ⇒ ⊢ (f g) (f g1) RightChopEqvChop

Proof:

1
g g1
Assump
2
g g1
1,Prop
3
f g f g1
4
g1 g
1,Prop
5
f g1 f g
6
f g f g1
3, 5,Prop

qed

f g ⇒ ⊢ f g DiamondEqvDiamond

Proof:

1
f g
Assump
2
true f true g
3
f g
2, def. of 

qed

f g ⇒ ⊢ f g BoxEqvBox

Proof:

1
f g
Assump
2
¬f ≡¬g
1,Prop
3
¬f ¬g
4
¬¬f ≡¬¬g
3,Prop
5
f g
4, def. of 

qed

f g ⇒ ⊢ f g BoxImpInferBoxImpBox

Proof:

1
f g
Assump
2
( f g)
3
( f g) ( f g)
4
f g
2, 3,MP

qed

(f f1) g f g AndChopA

Proof:

1
f f1 f
2
(f f1) g f g

qed

(f f1) g f1 g AndChopB

Proof:

1
f f1 f1
2
(f f1) g f1 g

qed

(f f1) g (f g) (f1 g) AndChopImpChopAndChop

Proof:

1
(f f1) g f g
2
(f f1) g f1 g
3
(f f1) g (f g) (f1 g)
1, 2,Prop

qed

(f f1) g (f1 f) g AndChopCommute

Proof:

1
f f1 f1 f
2
(f f1) g (f1 f) g

qed

(f f1) g (f g) (f1 g) OrChopEqv

The proof for is immediate from axiom OrChopImp.

Here is the proof for :

1
f f f1
2
f g (f f1) g
3
f1 f f1
4
f1 g (f f1) g
5
(f g) (f g1) (f f1) g
2, 4,Prop

qed

f g f ChopImpDf

Proof:

1
g true
2
f g f true
3
f g f
2, def. of 

qed

empty DfEmpty

Proof:

1
empty true true
2
empty true empty
3
empty
1, 2,Prop

qed

f g g ChopImpDiamond

Proof:

1
f true
2
f g true g
3
f g g
2, def. of 

qed







2018-10-21
Contact | Home | ITL home | Course | Proofs | Algebra | FL