let p, q, r, s be Element of LTLB_WFF ; ('not' (p '&&' s)) => ('not' ((r '&&' s) '&&' (p '&&' q))) is ctaut
let g be Function of LTLB_WFF,BOOLEAN; LTLAXIO1:def 16 (VAL g) . (('not' (p '&&' s)) => ('not' ((r '&&' s) '&&' (p '&&' q)))) = 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) . ('not' ((r '&&' s) '&&' (p '&&' q))) =
((VAL g) . ((r '&&' s) '&&' (p '&&' q))) => ((VAL g) . TFALSUM)
by LTLAXIO1:def 15
.=
(((VAL g) . (r '&&' s)) '&' ((VAL g) . (p '&&' q))) => ((VAL g) . TFALSUM)
by LTLAXIO1:31
.=
((((VAL g) . r) '&' ((VAL g) . s)) '&' ((VAL g) . (p '&&' q))) => ((VAL g) . TFALSUM)
by LTLAXIO1:31
.=
((((VAL g) . r) '&' ((VAL g) . s)) '&' (((VAL g) . p) '&' ((VAL g) . q))) => ((VAL g) . TFALSUM)
by LTLAXIO1:31
;
A4:
( (VAL g) . s = 1 or (VAL g) . s = 0 )
by XBOOLEAN:def 3;
(VAL g) . ('not' (p '&&' s)) =
((VAL g) . (p '&&' s)) => ((VAL g) . TFALSUM)
by LTLAXIO1:def 15
.=
(((VAL g) . p) '&' ((VAL g) . s)) => ((VAL g) . TFALSUM)
by LTLAXIO1:31
;
hence (VAL g) . (('not' (p '&&' s)) => ('not' ((r '&&' s) '&&' (p '&&' q)))) =
((((VAL g) . p) '&' ((VAL g) . s)) => ((VAL g) . TFALSUM)) => (((((VAL g) . r) '&' ((VAL g) . s)) '&' (((VAL g) . p) '&' ((VAL g) . q))) => ((VAL g) . TFALSUM))
by LTLAXIO1:def 15, A3
.=
1
by A2, A4, A1
;
verum