let p, q be Element of LTLB_WFF ; (p => (q '&&' ('not' q))) => ('not' p) is ctaut
let g be Function of LTLB_WFF,BOOLEAN; LTLAXIO1:def 16 (VAL g) . ((p => (q '&&' ('not' q))) => ('not' p)) = 1
set v = VAL g;
A1:
(VAL g) . TFALSUM = 0
by LTLAXIO1:def 15;
A2:
( (VAL g) . p = 1 or (VAL g) . p = 0 )
by XBOOLEAN:def 3;
A3:
( (VAL g) . q = 1 or (VAL g) . q = 0 )
by XBOOLEAN:def 3;
thus (VAL g) . ((p => (q '&&' ('not' q))) => ('not' p)) =
((VAL g) . (p => (q '&&' ('not' q)))) => ((VAL g) . ('not' p))
by LTLAXIO1:def 15
.=
(((VAL g) . p) => ((VAL g) . (q '&&' ('not' q)))) => ((VAL g) . ('not' p))
by LTLAXIO1:def 15
.=
(((VAL g) . p) => (((VAL g) . q) '&' ((VAL g) . ('not' q)))) => ((VAL g) . ('not' p))
by LTLAXIO1:31
.=
(((VAL g) . p) => (((VAL g) . q) '&' (((VAL g) . q) => ((VAL g) . TFALSUM)))) => ((VAL g) . ('not' p))
by LTLAXIO1:def 15
.=
1
by A2, A3, A1, LTLAXIO1:def 15
; verum