let p, q, r be Element of LTLB_WFF ; (r => (untn (p,q))) => ((r => (('not' q) '&&' ('not' (p 'U' q)))) => ('not' r)) is ctaut
let g be Function of LTLB_WFF,BOOLEAN; LTLAXIO1:def 16 (VAL g) . ((r => (untn (p,q))) => ((r => (('not' q) '&&' ('not' (p 'U' q)))) => ('not' r))) = 1
set v = VAL g;
set pq = p 'U' q;
set nq = 'not' q;
set nr = 'not' r;
A1:
(VAL g) . TFALSUM = 0
by LTLAXIO1:def 15;
A2:
( (VAL g) . r = 1 or (VAL g) . r = 0 )
by XBOOLEAN:def 3;
A3: (VAL g) . ((r => (('not' q) '&&' ('not' (p 'U' q)))) => ('not' r)) =
((VAL g) . (r => (('not' q) '&&' ('not' (p 'U' q))))) => ((VAL g) . ('not' r))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => ((VAL g) . (('not' q) '&&' ('not' (p 'U' q))))) => ((VAL g) . ('not' r))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => (((VAL g) . ('not' q)) '&' ((VAL g) . ('not' (p 'U' q))))) => ((VAL g) . ('not' r))
by LTLAXIO1:31
.=
(((VAL g) . r) => ((((VAL g) . q) => ((VAL g) . TFALSUM)) '&' ((VAL g) . ('not' (p 'U' q))))) => ((VAL g) . ('not' r))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => ((((VAL g) . q) => ((VAL g) . TFALSUM)) '&' (((VAL g) . (p 'U' q)) => ((VAL g) . TFALSUM)))) => ((VAL g) . ('not' r))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => ((((VAL g) . q) => ((VAL g) . TFALSUM)) '&' ((g . (p 'U' q)) => ((VAL g) . TFALSUM)))) => ((VAL g) . ('not' r))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => ((((VAL g) . q) => ((VAL g) . TFALSUM)) '&' ((g . (p 'U' q)) => ((VAL g) . TFALSUM)))) => (((VAL g) . r) => ((VAL g) . TFALSUM))
by LTLAXIO1:def 15
;
A4:
( g . (p 'U' q) = 1 or g . (p 'U' q) = 0 )
by XBOOLEAN:def 3;
A5:
( (VAL g) . q = 1 or (VAL g) . q = 0 )
by XBOOLEAN:def 3;
(VAL g) . (r => (untn (p,q))) =
((VAL g) . r) => ((VAL g) . (untn (p,q)))
by LTLAXIO1:def 15
.=
((VAL g) . r) => (((VAL g) . q) 'or' ((VAL g) . (p '&&' (p 'U' q))))
by Th5
.=
((VAL g) . r) => (((VAL g) . q) 'or' (((VAL g) . p) '&' ((VAL g) . (p 'U' q))))
by LTLAXIO1:31
.=
((VAL g) . r) => (((VAL g) . q) 'or' (((VAL g) . p) '&' (g . (p 'U' q))))
by LTLAXIO1:def 15
;
hence (VAL g) . ((r => (untn (p,q))) => ((r => (('not' q) '&&' ('not' (p 'U' q)))) => ('not' r))) =
(((VAL g) . r) => (((VAL g) . q) 'or' (((VAL g) . p) '&' (g . (p 'U' q))))) => ((((VAL g) . r) => ((((VAL g) . q) => ((VAL g) . TFALSUM)) '&' ((g . (p 'U' q)) => ((VAL g) . TFALSUM)))) => (((VAL g) . r) => ((VAL g) . TFALSUM)))
by LTLAXIO1:def 15, A3
.=
1
by A2, A5, A1, A4
;
verum