consider Q being object such that
A1: Q in comp P by XBOOLE_0:def 1;
consider Pg being consistent PNPair such that
Pg = Q and
A2: Pg is_completion_of P by A1;
A3: rng (P `1) c= rng (Pg `1) by A2;
A4: rng (P `2) c= rng (Pg `2) by A2;
reconsider Pg = Pg as consistent complete PNPair by A2, Th13;
set T = the pnptree of Pg;
set t = the complete path of the pnptree of Pg;
defpred S1[ Element of NAT , Element of bool props] means c2 = { p where p is Element of LTLB_WFF : ( p is simple & p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . P)) `1) ) } ;
A5: now :: thesis: for x being Element of NAT ex y being Element of bool props st S1[x,y]
let x be Element of NAT ; :: thesis: ex y being Element of bool props st S1[x,y]
set y = { p where p is Element of LTLB_WFF : ( p is simple & p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . x)) `1) ) } ;
{ p where p is Element of LTLB_WFF : ( p is simple & p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . x)) `1) ) } c= props
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { p where p is Element of LTLB_WFF : ( p is simple & p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . x)) `1) ) } or z in props )
assume z in { p where p is Element of LTLB_WFF : ( p is simple & p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . x)) `1) ) } ; :: thesis: z in props
then consider p being Element of LTLB_WFF such that
A6: p = z and
A7: p is simple and
p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . x)) `1) ;
ex n being Element of NAT st p = prop n by A7, HILBERT2:def 8;
hence z in props by LTLAXIO1:def 10, A6; :: thesis: verum
end;
then reconsider y = { p where p is Element of LTLB_WFF : ( p is simple & p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . x)) `1) ) } as Element of bool props ;
S1[x,y] ;
hence ex y being Element of bool props st S1[x,y] ; :: thesis: verum
end;
consider M being sequence of (bool props) such that
A8: for n being Element of NAT holds S1[n,M . n] from FUNCT_2:sch 3(A5);
 set s = SAT M;
defpred S2[ Element of LTLB_WFF ] means for i being Element of NAT st P in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) holds
( (SAT M) . [i,P] = 1 iff P in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) );
A9: now :: thesis: for i being Element of NAT
for p being Element of LTLB_WFF st p is simple holds
( ( (SAT M) . [i,p] = 1 implies p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) & ( p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) implies (SAT M) . [i,p] = 1 ) )
let i be Element of NAT ; :: thesis: for p being Element of LTLB_WFF st p is simple holds
( ( (SAT M) . [i,p] = 1 implies p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) & ( p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) implies (SAT M) . [i,p] = 1 ) )
let p be Element of LTLB_WFF ; :: thesis: ( p is simple implies ( ( (SAT M) . [i,p] = 1 implies p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) & ( p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) implies (SAT M) . [i,p] = 1 ) ) )
assume A10: p is simple ; :: thesis: ( ( (SAT M) . [i,p] = 1 implies p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) & ( p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) implies (SAT M) . [i,p] = 1 ) )
then A11: ex n being Element of NAT st p = prop n by HILBERT2:def 8;
A12: M . i = { q where q is Element of LTLB_WFF : ( q is simple & q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) } by A8;
hereby :: thesis: ( p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) implies (SAT M) . [i,p] = 1 )
assume (SAT M) . [i,p] = 1 ; :: thesis: p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1)
then p in M . i by A11, LTLAXIO1:def 11;
then ex q being Element of LTLB_WFF st
( p = q & q is simple & q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) by A12;
hence p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ; :: thesis: verum
end;
assume p in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ; :: thesis: (SAT M) . [i,p] = 1
then p in M . i by A12, A10;
hence (SAT M) . [i,p] = 1 by LTLAXIO1:def 11, A11; :: thesis: verum
end;
A13: now :: thesis: for n being Element of NAT holds S2[ prop n]
let n be Element of NAT ; :: thesis: S2[ prop n]
prop n is simple by HILBERT2:def 8;
hence S2[ prop n] by A9; :: thesis: verum
end;
A14: now :: thesis: for r, q being Element of LTLB_WFF st S2[r] & S2[q] holds
( S2[r 'U' q] & S2[r => q] )
let r, q be Element of LTLB_WFF ; :: thesis: ( S2[r] & S2[q] implies ( S2[r 'U' q] & S2[r => q] ) )
set ruq = r 'U' q;
assume that
A15: S2[r] and
A16: S2[q] ; :: thesis: ( S2[r 'U' q] & S2[r => q] )
thus S2[r 'U' q] :: thesis: S2[r => q]
proof
let i be Element of NAT ; :: thesis: ( r 'U' q in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) implies ( (SAT M) . [i,(r 'U' q)] = 1 iff r 'U' q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) )
defpred S3[ Nat] means not (SAT M) . [P,q] = 1;
set Q = the pnptree of Pg . ( the complete path of the pnptree of Pg . i);
defpred S4[ Element of NAT ] means ex k being Element of NAT st
( i < k & k < P & not (SAT M) . [k,r] = 1 );
assume A17: r 'U' q in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) ; :: thesis: ( (SAT M) . [i,(r 'U' q)] = 1 iff r 'U' q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) )
hereby :: thesis: ( r 'U' q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) implies (SAT M) . [i,(r 'U' q)] = 1 )
assume A18: (SAT M) . [i,(r 'U' q)] = 1 ; :: thesis: r 'U' q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1)
assume not r 'U' q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ; :: thesis: contradiction
then A19: r 'U' q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `2) by A17, XBOOLE_0:def 3;
consider j being Element of NAT such that
A20: ( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,r] = 1 ) ) by A18, Th5;
per cases ( q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . j)) `2) or ex k being Element of NAT st
( i < k & k < j & r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) `2) ) ) by Th30, A19, A20;
suppose q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . j)) `2) ; :: thesis: contradiction
then ( not q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . j)) `1) & q in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . j)) ) by LTLAXIO3:30, XBOOLE_0:3, XBOOLE_0:def 3;
hence contradiction by A16, A20; :: thesis: verum
end;
suppose ex k being Element of NAT st
( i < k & k < j & r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) `2) ) ; :: thesis: contradiction
then consider k being Element of NAT such that
A21: ( i < k & k < j ) and
A22: r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) `2) ;
( not r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) `1) & r in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) ) by LTLAXIO3:30, A22, XBOOLE_0:3, XBOOLE_0:def 3;
then not (SAT M) . [k,r] = 1 by A15;
hence contradiction by A21, A20; :: thesis: verum
end;
end;
end;
assume r 'U' q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ; :: thesis: (SAT M) . [i,(r 'U' q)] = 1
then consider j being Element of NAT such that
A23: j > i and
A24: q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . j)) `1) and
A25: for k being Element of NAT st i < k & k < j holds
r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) `1) by Def14;
A26: now :: thesis: for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,r] = 1
let k be Element of NAT ; :: thesis: ( i < k & k < j implies (SAT M) . [k,r] = 1 )
assume ( i < k & k < j ) ; :: thesis: (SAT M) . [k,r] = 1
then A27: r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) `1) by A25;
then r in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . k)) by XBOOLE_0:def 3;
hence (SAT M) . [k,r] = 1 by A15, A27; :: thesis: verum
end;
q in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . j)) by A24, XBOOLE_0:def 3;
then (SAT M) . [j,q] = 1 by A24, A16;
hence (SAT M) . [i,(r 'U' q)] = 1 by A26, Th5, A23; :: thesis: verum
end;
thus S2[r => q] :: thesis: verum
proof
let i be Element of NAT ; :: thesis: ( r => q in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) implies ( (SAT M) . [i,(r => q)] = 1 iff r => q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) )
set Q = the pnptree of Pg . ( the complete path of the pnptree of Pg . i);
assume A28: r => q in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) ; :: thesis: ( (SAT M) . [i,(r => q)] = 1 iff r => q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) )
A29: tau (rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i))) = rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) by LTLAXIO3:def 11;
then A30: r in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) by A28, LTLAXIO3:19;
A31: q in rng ( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) by A28, LTLAXIO3:19, A29;
A32: ( (SAT M) . [i,r] = 1 or (SAT M) . [i,r] = 0 ) by XBOOLEAN:def 3;
hereby :: thesis: ( r => q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) implies (SAT M) . [i,(r => q)] = 1 )
assume (SAT M) . [i,(r => q)] = 1 ; :: thesis: r => q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1)
then ((SAT M) . [i,r]) => ((SAT M) . [i,q]) = 1 by LTLAXIO1:def 11;
then ( not r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) or q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) by A32, A15, A16, A30, A31;
then ( r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `2) or q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) by A30, XBOOLE_0:def 3;
hence r => q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) by LTLAXIO3:33, A28, A30, A31; :: thesis: verum
end;
assume r => q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ; :: thesis: (SAT M) . [i,(r => q)] = 1
then ( r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `2) or q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) by LTLAXIO3:33, A28, A30, A31;
then ( not r in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) or q in rng (( the pnptree of Pg . ( the complete path of the pnptree of Pg . i)) `1) ) by XBOOLE_0:3, LTLAXIO3:30;
then ((SAT M) . [i,r]) => ((SAT M) . [i,q]) = 1 by A15, A16, A30, A31, A32;
hence (SAT M) . [i,(r => q)] = 1 by LTLAXIO1:def 11; :: thesis: verum
end;
end;
A33: S2[ TFALSUM ] by LTLAXIO3:32, LTLAXIO1:def 11;
A34: for A being Element of LTLB_WFF holds S2[A] from HILBERT2:sch 2(A33, A13, A14);
 A35: the pnptree of Pg . ( the complete path of the pnptree of Pg . 0) = the pnptree of Pg . {} by Def13
.= Pg by Def11 ;
now :: thesis: for i being Nat st i in dom (nega (P `2)) holds
(SAT M) . [0,((nega (P `2)) /. i)] = 1
let i be Nat; :: thesis: ( i in dom (nega (P `2)) implies (SAT M) . [0,((nega (P `2)) /. i)] = 1 )
set nA = (nega (P `2)) /. i;
set A = (P `2) /. i;
assume A36: i in dom (nega (P `2)) ; :: thesis: (SAT M) . [0,((nega (P `2)) /. i)] = 1
len (nega (P `2)) = len (P `2) by LTLAXIO2:def 4;
then A37: i in dom (P `2) by A36, FINSEQ_3:29;
then (P `2) . i in rng (P `2) by FUNCT_1:3;
then (P `2) /. i in rng (P `2) by PARTFUN1:def 6, A37;
then A38: ( (P `2) /. i in rng (Pg `2) & not (P `2) /. i in rng (Pg `1) ) by A4, LTLAXIO3:30, XBOOLE_0:3;
rng (Pg `2) c= rng Pg by XBOOLE_1:7;
then A39: not (SAT M) . [0,((P `2) /. i)] = 1 by A38, A35, A34;
thus (SAT M) . [0,((nega (P `2)) /. i)] = (SAT M) . [0,('not' ((P `2) /. i))] by LTLAXIO2:8, A37
.= 1 by A39, XBOOLEAN:def 3, LTLAXIO1:5 ; :: thesis: verum
end;
then A40: (SAT M) . [0,H2( nega (P `2))] = 1 by Th6;
now :: thesis: for i being Nat st i in dom (P `1) holds
(SAT M) . [0,((P `1) /. i)] = 1
let i be Nat; :: thesis: ( i in dom (P `1) implies (SAT M) . [0,((P `1) /. i)] = 1 )
set A = (P `1) /. i;
assume i in dom (P `1) ; :: thesis: (SAT M) . [0,((P `1) /. i)] = 1
then (P `1) /. i in rng (P `1) by PARTFUN2:2;
then ( rng (Pg `1) c= rng Pg & (P `1) /. i in rng (Pg `1) ) by XBOOLE_1:7, A3;
hence (SAT M) . [0,((P `1) /. i)] = 1 by A35, A34; :: thesis: verum
end;
then (SAT M) . [0,H2(P `1 )] = 1 by Th6;
then (SAT M) . [0,(P ^)] = 1 by A40, LTLAXIO1:7;
hence P ^ is satisfiable ; :: thesis: verum