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