ITL
© 1996-2018







6 Properties of Fin


f fin w f ; (w empty) AndFinEqvChopStateAndEmpty


Proof for :

1
f ; empty f
2
empty (w empty) (¬w empty)
3
f ; empty f ; (w empty) f ; (¬w empty)
4
f ; (¬w empty) (¬w empty)
5
(¬w empty) ¬ fin w
6
f f ; (w empty) ¬ fin w
1, 3, 4, 5,Prop
7
f fin w f ; (w empty)
6,Prop

Proof for :

1
f ; (w empty) f ; empty
2
f ; empty f
3
f ; (w empty) (w empty)
4
(w empty) fin w
5
f ; (w empty) f fin w
1, 2, 3, 4,Prop

The following is a lemma used in the proof of theorem FinChopEqvDiamond.


(fin w) ; f (w f) ((fin w) ; f) FinChopEqvOr


Proof:

1
fin w (w empty) fin w
2
(fin w) ; f ((w empty) fin w) ; f
3
((w empty) fin w) ; f (w empty) ; f ( fin w) ; f
4
(w empty) ; f w f
5
( fin w) ; f ((fin w) ; f)
6
(fin w) ; f (w f) ((fin w) ; f)
2, 4, 5,Prop


(fin w) ; f (w f) FinChopEqvDiamond


Proof for :

1
(fin w) ; f (w f) ((fin w) ; f)
2
(w f) (w f) (w f)
3
(fin w) ; f ¬(w f) ((fin w) ; f) ¬(w f)
1, 2,Prop
4
(fin w) ; f (w f)

Proof of :

1
(fin w) ; f (w f) ((fin w) ; f)
2
(w f) (w f) (w f)
3
(w f) ¬((fin w) ; f) (w f) ¬((fin w) ; f)
1, 2,Prop
4
(w f) (fin w) ; f

The following important theorem demonstrates how to pass information from the final state of a subinterval to the starting state of a subinterval immediately following it.


(fin w) w FinYields


Proof:

1
(fin w) ; ¬w (w ¬w)
2
⊢ ¬(w ¬w)
3
⊢ ¬((fin w) ; ¬w)
1, 2,Prop
4
(fin w) w
3, def. of 

Here is a related theorem whose proof uses FinYields:


(f fin w) ; g f ; (w g) AndFinChopEqvStateAndChop


Proof for :

1
(fin w) w
2
f fin w fin w
3
(fin w) w (f fin w) w
4
(f fin w) w
1, 3,MP
5
(f fin w) ; g (f fin w) w (f fin w) ; (g w)
6
(f fin w) ; g (f fin w) ; (g w)
4, 5,Prop
7
(f fin w) ; (g w) f ; (g w)
8
g w w g
9
f ; (g w) f ; (w g)
10
(f fin w) ; g f ; (w g)
6, 7, 9,ImpChain

Prove of :

1
f (f fin w) fin ¬w
2
f ; (w g) ((f fin w) fin ¬w) ; (w g)
3
((f fin w) fin ¬w) ; (w g)
(f fin w) ; (w g) (fin ¬w) ; (w g)
4
(fin ¬w) ; (w g) (¬w (w g))
5
⊢ ¬(¬w (w g))
6
f ; (w g) (f fin w) ; (w g)
2, 3, 4, 5,Prop
7
(f fin w) ; (w g) (f fin w) ; g
8
f ; (w g) (f fin w) ; g
6, 7,ImpChain


(f fin w) f ; w DiAndFinEqvChopState


Proof:

1
(f fin w) ; true f ; (w true)
2
w true w
3
f ; (w true) f ; w
4
(f fin w) ; true f ; w
1, 3,EqvChain
5
(f fin w) f ; w
4, def. of 

Here is a corollary of DiAndFinEqvChopState:


(f fin w) f w BiImpFinEqvYieldsState


Proof:

1
(f fin ¬w) f ; ¬w
2
f fin ¬w f ¬ fin w
3
f ¬ fin w ≡¬(f fin w)
4
f fin ¬w ≡¬(f fin w)
2, 3,EqvChain
5
(f fin ¬w) ¬(f fin w)
6
¬(f fin w) ≡¬(f fin w)
7
⊢ ¬(f fin w) f ; ¬w
1, 5, 6,Prop
8
(f fin w) ≡¬(f ; ¬w)
7,Prop
9
(f fin w) f w
8, def. of 


f ; fin w fin w ChopFinImpFin


Proof:

1
f ; fin w fin w
2
fin w fin w
3
f ; fin w fin w
1, 2,ImpChain


fin w f fin w FinImpYieldsFin


Proof:

1
f ; fin ¬w fin ¬w
2
fin ¬w ≡¬ fin w
3
f ; fin ¬w f ; ¬ fin w
4
f ; ¬ fin w ¬ fin w
1, 2, 3,Prop
5
fin w ¬(f ; ¬ fin w)
4,Prop
6
fin w f fin w
5, def. of 


(f ; g) fin w f ; (g fin w) ChopAndFin


Proof for :

1
fin w true fin w
2
(f ; g) fin w (f ; g) true fin w
1,Prop
3
(f ; g) true fin w f ; (g fin w)
4
(f ; g) fin w f ; (g fin w)
2, 3,ImpChain

Proof for :

1
f ; (g fin w) f ; g
2
f ; (g fin w) f ; fin w
3
f ; fin w fin w
4
fin w fin w
5
f ; (g fin w) (f ; g) fin w
1, 2, 3, 4,Prop

Here is a corollary used in some proofs by contradiction:


f ; g ¬ fin w f ; (g ¬ fin w) ChopAndNotFin


1
f ; g fin ¬w f ; (g fin ¬w)
2
fin ¬w ≡¬ fin w
3
g fin ¬w g ¬ fin w
2,Prop
4
f ; (g fin ¬w) f ; (g ¬ fin w)
5
f ; g ¬ fin w f ; (g ¬ fin w)
1, 2, 4,Prop


(w fin w1) ; (w1 fin w2) (w fin w2) FinChopChain


Proof:

1
w   (w fin w1) ; (w1 fin w2)
(w (w fin w1)) ; (w1 fin w2))
2
w (w fin w1) fin w1
3
(w (w fin w1)) ; (w1 fin w2)
(fin w1) ; (w1 fin w2)
4
(fin w1) ; (w1 fin w2) (w1 (w1 fin w2))
5
(w1 (w1 fin w2)) fin w2
6
w   (w fin w1) ; (w1 fin w2) fin w2
1, 3, 4, 5,Prop
7
(w fin w1) ; (w1 fin w2) (w fin w2)
6,Prop


w f fin w1 ChopRule
w1 f1 fin w2
⇒ ⊢ w (f ; f1) fin w2


Proof:

1
w (f ; f1) (w f) ; f1
2
w f fin w1
given
3
(w f) ; f1 (fin w1) ; f1
4
(fin w1) ; f1 (w1 f1)
5
w1 f1 fin w2
given
6
(w1 f1) fin w2
7
fin w2 fin w2
8
w (f ; f1) fin w2
1, 3, 4, 6, 7,Prop


w f f1 fin w1 ChopRep
w1 g g1
⇒ ⊢ w (f ; g) (f1 ; g1)


Proof:

1
w f f1 fin w1
given
2
w (f ; g) (f1 fin w) ; g
3
(f1 fin w1) ; g f1 ; (w1 g)
4
w1 g g1
given
5
f1 ; (w1 g) f1 ; g1
6
w (f ; g) f1 ; g1
2, 3, 5,Prop


w f f1 fin w1 ChopRepAndFin
w1 g g1 fin w2
⇒ ⊢ w (f ; g) (f1 ; g1) fin w2


Proof:

1
w f f1 fin w1
given
2
w1 g g1 fin w2
given
3
w (f ; g) f1 ; (g1 fin w2)
1, 2,ChopRep
4
f1 ; (g1 fin w2) f1 ; g1
5
f1 ; (g1 fin w2) f1 ; fin w2
6
f1 ; fin w2 fin w2
7
w (f ; g) (f1 ; g1) fin w2
3, 4, 5, 6,Prop


f more ; f ⇒ ¬f MoreChopLoop


Proof:

1
f more ; f
given
2
more ; f f
3
f f
2,Prop
4
(f f)
5
(f f) ¬f
6
⊢ ¬f
4, 5,MP

Here is a corollary:


f ¬g (more ; (f ¬g)) ⇒ ⊢ f g MoreChopContra


Proof:

1
f ¬g (more ; (f ¬g))
given
2
⊢ ¬(f ¬g)
3
f g
2,Prop

Here is a variant of lemma MoreChopLoop that is useful in proofs:


f g ; f, g more ⇒ ¬f ChopLoop


Proof:

1
f g ; f
given
2
g more
given
3
g ; f more ; f
4
f more ; f
1, 3,ImpChain
5
⊢ ¬f

Here is a variant of lemma MoreChopContra that is useful in proofs:


f ¬g h ; f ¬(h ; g), h more ⇒ ⊢ f g ChopContra


Proof:

1
f ¬g h ; f ¬(h ; g)
given
2
h more
given
3
h ; f ¬(h ; g) h ; (f ¬g)
4
h ; (f ¬g) more ; (f ¬g)
5
f ¬g more ; (f ¬g)
1, 3, 4,ImpChain
6
f g







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL