let p, q, r be Element of LTLB_WFF ; :: thesis: (r => (untn (p,q))) => ((r => (('not' q) '&&' ('not' (p 'U' q)))) => ('not' r)) is ctaut
let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (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 ;
:: thesis: verum