let P be consistent PNPair; :: thesis: rng (P `1) misses rng (P `2)

assume not rng (P `1) misses rng (P `2) ; :: thesis: contradiction

then not (rng (P `1)) /\ (rng (P `2)) = {} ;

then consider x being object such that

A1: x in (rng (P `1)) /\ (rng (P `2)) by XBOOLE_0:def 1;

x in rng (P `1) by XBOOLE_0:def 4, A1;

then consider n1 being object such that

A2: n1 in dom (P `1) and

A3: (P `1) . n1 = x by FUNCT_1:def 3;

x in rng (P `2) by XBOOLE_0:def 4, A1;

then consider n2 being object such that

A4: n2 in dom (P `2) and

A5: (P `2) . n2 = x by FUNCT_1:def 3;

reconsider n1 = n1, n2 = n2 as Element of NAT by A2, A4;

x = (P `2) /. n2 by PARTFUN1:def 6, A4, A5;

then reconsider x = x as Element of LTLB_WFF ;

A6: 1 <= n2 by FINSEQ_3:25, A4;

A7: n2 <= len (P `2) by FINSEQ_3:25, A4;

'not' (P ^) is ctaut

then {} LTLB_WFF |- 'not' (P ^) by LTLAXIO1:42;

hence contradiction by Def10; :: thesis: verum

assume not rng (P `1) misses rng (P `2) ; :: thesis: contradiction

then not (rng (P `1)) /\ (rng (P `2)) = {} ;

then consider x being object such that

A1: x in (rng (P `1)) /\ (rng (P `2)) by XBOOLE_0:def 1;

x in rng (P `1) by XBOOLE_0:def 4, A1;

then consider n1 being object such that

A2: n1 in dom (P `1) and

A3: (P `1) . n1 = x by FUNCT_1:def 3;

x in rng (P `2) by XBOOLE_0:def 4, A1;

then consider n2 being object such that

A4: n2 in dom (P `2) and

A5: (P `2) . n2 = x by FUNCT_1:def 3;

reconsider n1 = n1, n2 = n2 as Element of NAT by A2, A4;

x = (P `2) /. n2 by PARTFUN1:def 6, A4, A5;

then reconsider x = x as Element of LTLB_WFF ;

A6: 1 <= n2 by FINSEQ_3:25, A4;

A7: n2 <= len (P `2) by FINSEQ_3:25, A4;

'not' (P ^) is ctaut

proof

then
'not' (P ^) in LTL_axioms
by LTLAXIO1:def 17;
let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . ('not' (P ^)) = 1

set nP2 = nega (P `2);

set v = VAL g;

A8: ( (VAL g) . x = TRUE or (VAL g) . x = FALSE ) by XBOOLEAN:def 3;

A9: (VAL g) . ((P `1) /. n1) = (VAL g) . x by PARTFUN1:def 6, A2, A3;

n2 <= len (nega (P `2)) by A7, LTLAXIO2:def 4;

then A10: n2 in dom (nega (P `2)) by FINSEQ_3:25, A6;

A11: (VAL g) . ((nega (P `2)) /. n2) = (VAL g) . ('not' ((P `2) /. n2)) by LTLAXIO2:8, A4

.= (VAL g) . ('not' x) by A4, A5, PARTFUN1:def 6

.= ((VAL g) . x) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15

.= ((VAL g) . x) => FALSE by LTLAXIO1:def 15 ;

A12: (VAL g) . (P ^) = ((VAL g) . H_{2}(P `1 )) '&' ((VAL g) . H_{2}( nega (P `2)))
by LTLAXIO1:31

.= ((((VAL g) . H_{2}((P `1) | (n1 -' 1))) '&' ((VAL g) . ((P `1) /. n1))) '&' ((VAL g) . H_{2}((P `1) /^ n1))) '&' ((VAL g) . H_{2}( nega (P `2)))
by LTLAXIO2:18, A2

.= ((((VAL g) . H_{2}((P `1) | (n1 -' 1))) '&' ((VAL g) . ((P `1) /. n1))) '&' ((VAL g) . H_{2}((P `1) /^ n1))) '&' ((((VAL g) . H_{2}((nega (P `2)) | (n2 -' 1))) '&' ((VAL g) . ((nega (P `2)) /. n2))) '&' ((VAL g) . H_{2}((nega (P `2)) /^ n2)))
by LTLAXIO2:18, A10

.= 0 by A8, A11, A9 ;

thus (VAL g) . ('not' (P ^)) = ((VAL g) . (P ^)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15

.= 1 by A12 ; :: thesis: verum

end;set nP2 = nega (P `2);

set v = VAL g;

A8: ( (VAL g) . x = TRUE or (VAL g) . x = FALSE ) by XBOOLEAN:def 3;

A9: (VAL g) . ((P `1) /. n1) = (VAL g) . x by PARTFUN1:def 6, A2, A3;

n2 <= len (nega (P `2)) by A7, LTLAXIO2:def 4;

then A10: n2 in dom (nega (P `2)) by FINSEQ_3:25, A6;

A11: (VAL g) . ((nega (P `2)) /. n2) = (VAL g) . ('not' ((P `2) /. n2)) by LTLAXIO2:8, A4

.= (VAL g) . ('not' x) by A4, A5, PARTFUN1:def 6

.= ((VAL g) . x) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15

.= ((VAL g) . x) => FALSE by LTLAXIO1:def 15 ;

A12: (VAL g) . (P ^) = ((VAL g) . H

.= ((((VAL g) . H

.= ((((VAL g) . H

.= 0 by A8, A11, A9 ;

thus (VAL g) . ('not' (P ^)) = ((VAL g) . (P ^)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15

.= 1 by A12 ; :: thesis: verum

then {} LTLB_WFF |- 'not' (P ^) by LTLAXIO1:42;

hence contradiction by Def10; :: thesis: verum