ITL
© 1996-2018







10 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


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


¬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


¬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


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


Proof:

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


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 


(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


(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


(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 







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