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 ;
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 ;
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 ;
then reconsider x = x as Element of LTLB_WFF ;
A6: 1 <= n2 by ;
A7: n2 <= len (P `2) by ;
'not' (P ^) is ctaut
proof
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 ;
n2 <= len (nega (P `2)) by ;
then A10: n2 in dom (nega (P `2)) by ;
A11: (VAL g) . ((nega (P `2)) /. n2) = (VAL g) . ('not' ((P `2) /. n2)) by
.= (VAL g) . () by
.= ((VAL g) . x) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= ((VAL g) . x) => FALSE by LTLAXIO1:def 15 ;
A12: (VAL g) . (P ^) = ((VAL g) . H2(P `1 )) '&' ((VAL g) . H2( nega (P `2))) by LTLAXIO1:31
.= ((((VAL g) . H2((P `1) | (n1 -' 1))) '&' ((VAL g) . ((P `1) /. n1))) '&' ((VAL g) . H2((P `1) /^ n1))) '&' ((VAL g) . H2( nega (P `2))) by
.= ((((VAL g) . H2((P `1) | (n1 -' 1))) '&' ((VAL g) . ((P `1) /. n1))) '&' ((VAL g) . H2((P `1) /^ n1))) '&' ((((VAL g) . H2((nega (P `2)) | (n2 -' 1))) '&' ((VAL g) . ((nega (P `2)) /. n2))) '&' ((VAL g) . H2((nega (P `2)) /^ n2))) by
.= 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;
then 'not' (P ^) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- 'not' (P ^) by LTLAXIO1:42;
hence contradiction by Def10; :: thesis: verum