ITL
© 1996-2018







17.5 Properties Involving the PTL Operator


( f) g (f g) NextChop


1
(skip f) g skip (f g)
2
( f) g (f g)
1, def. of 


(w f) g w (f g) StateAndNextChop


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


(w w) w w DfStateAndNextEqv


1
(w w) true w (w true)
2
(w w) w w
1, def. of 
3
w′≡ w
4
skip w′≡ skip w
5
w′≡w
4, def. of 
6
(w w) w w
2, 5,Prop







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