ITL
© 1996-2018







2.8 Properties of Halt

halt w ; f if w then f else (halt w ; f) HaltChopEqv

Proof:

1
halt w if w then empty else halt w
2
halt w ; f if w then empty ; f else ( halt w) ; f
3
empty ; f f
4
( halt w) ; f (halt w ; f)
5
halt w ; f if w then f else (halt w ; f)
2, 3, 4,Prop

qed

w (halt w ; f) f AndHaltChopImp

Proof:

1
halt w ; f if w then f else (halt w ; f)
2
w (halt w ; f) f
1,Prop

qed

¬w (halt w ; f) (halt w ; f) NotAndHaltChopImpNext

Proof:

1
halt w ; f if w then f else (halt w ; f)
2
⊢ ¬w (halt w ; f) (halt w ; f)
1,Prop

qed

¬w (halt w ; f) skip (halt w ; f) NotAndHaltChopImpSkipYields

Proof:

1
⊢ ¬w (halt w ; f) (halt w ; f)
2
(halt w ; f) skip (halt w ; f)
3
⊢ ¬w (halt w ; f) skip (halt w ; f)
1, 2,ImpChain

qed

halt w ; f ¬(halt w ; ¬f) HaltChopImpNotHaltChopNot

Proof:

1
halt w ; f if w then f else (halt w ; f)
2
if w then f else (halt w ; f) ((w f) (¬w (halt w ; f)))
3
halt w ; ¬f if w then ¬f else (halt w ; ¬f)
4
if w then ¬f else (halt w ; ¬f) ((w ¬f) (¬w (halt w ; ¬f)))
5
(halt w ; f) (halt w ; ¬f)
  (w f) (¬w (halt w ; f)) (w ¬f) (¬w (halt w ; ¬f))
1, 2, 3, 4,Prop
6
(halt w ; f) (halt w ; ¬f) (halt w ; f) (halt w ; ¬f)
6,Prop
7
(halt w ; f) (halt w ; ¬f) ((halt w ; f) (halt w ; ¬f))
8
(halt w ; f) (halt w ; ¬f) ((halt w ; f) (halt w ; ¬f))
6, 7,Prop
9
⊢ ¬((halt w ; f) (halt w ; ¬f))
10
halt w ; f ¬(halt w ; ¬f)
9,Prop

qed

halt w ; f (halt w) f HaltChopImpHaltYields

Proof:

1
halt w ; f ¬(halt w ; ¬f)
2
halt w ; f (halt w) f
1, def. of 

qed

(halt w) ; f (halt w) ; g (halt w) ; (f g) HaltChopAnd

Proof:

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

qed

(halt w f) ; f1 (halt w ; g) (halt w f) ; (f1 g) HaltAndChopAndHaltChopImpHaltAndChopAnd

Proof:

1
f1 ¬g (f1 g)
2
(halt w f) ; f1
(halt w f) ; ¬g) ((halt w f) ; (f1 g))
3
(halt w f) ; ¬g halt w ; ¬g
4
halt w ; g ¬(halt w ; ¬g)
5
(halt w f) ; f1 (halt w ; g) (halt w f) ; (f1 g)
2, 3, 4,Prop

qed

(halt w) ; f ( ¬w) ((halt w) ; f) HaltImpBoxYields

Proof:

1
( ¬w) ; ¬(halt w ; f) ( ¬w)
2
¬w ¬w
3
( ¬w) ¬w
4
¬w ≡¬w
5
( ¬w) ; ¬(halt w ; f) ¬w
1, 2, 4,Prop
6
halt w ; f if w then f else (halt w ; f)
7
(halt w ; f) ( ¬w) ; ¬(halt w ; f) ((halt w) ; f)
5, 6,Prop
8
¬w empty ¬w
9
( ¬w) ; ¬(halt w ; f)
¬(halt w ; f) (( ¬w) ; ¬(halt w ; f))
10
(halt w) ; f ( ¬w) ; ¬(halt w ; f)
(( ¬w) ; ¬(halt w ; f))
9,Prop
11
(halt w) ; f ( ¬w) ; ¬(halt w ; f)
((halt w) ; f) (( ¬w) ; ¬(halt w ; f))
7, 10,Prop
12
((halt w) ; f) (( ¬w) ; ¬(halt w ; f))
(((halt w) ; f) (( ¬w) ; ¬(halt w ; f)))
13
(halt w) ; f ( ¬w) ; ¬(halt w ; f)
(((halt w) ; f) (( ¬w) ; ¬(halt w ; f)))
11, 12,ImpChain
14
⊢ ¬((halt w) ; f ( ¬w) ; ¬(halt w ; f))
15
(halt w) ; f ¬(( ¬w) ; ¬(halt w ; f))
14,Prop
16
(halt w) ; f ( ¬w) ((halt w) ; f)
15, def. of 

qed







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