let P be consistent PNPair; :: thesis: for f being FinSequence of LTLB_WFF st rng f = (comp P) ^ holds
{} LTLB_WFF |- (P ^) => ('not' ((con (nega f)) /. (len (con (nega f)))))
let f be FinSequence of LTLB_WFF ; :: thesis: ( rng f = (comp P) ^ implies {} LTLB_WFF |- (P ^) => ('not' ((con (nega f)) /. (len (con (nega f))))) )
set c = comp (rng P);
defpred S₁[ PNPair] means ( rng (P `1) c= rng ($1 `1) & rng (P `2) c= rng ($1 `2) );
defpred S₂[ PNPair] means ( $1 is consistent & S₁[$1] );
defpred S₃[ PNPair] means ( not rng (P `1) misses rng ($1 `2) or not rng (P `2) misses rng ($1 `1) );
set c1 = { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ;
set c2 = (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ;
A1: { Pg where Pg is Element of comp (rng P) : S₂[Pg] } c= comp (rng P) from FRAENKEL:sch 10();
A2: { Pg where Pg is Element of comp (rng P) : S₂[Pg] } = comp P

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: comp P c= { Pg where Pg is Element of comp (rng P) : S₂[Pg] }

let x be object ; :: thesis: ( x in { Pg where Pg is Element of comp (rng P) : S₂[Pg] } implies x in comp P )
assume x in { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ; :: thesis: x in comp P
then consider Pg being Element of comp (rng P) such that
A3: Pg = x and
A4: S₂[Pg] ;
reconsider Pg = Pg as consistent PNPair by A4;
Pg in comp (rng P) ;
then ex Q being PNPair st
( Q = Pg & rng Q = tau (rng P) & rng (Q `1) misses rng (Q `2) ) ;
then Pg is_completion_of P by A4;
hence x in comp P by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in comp P or x in { Pg where Pg is Element of comp (rng P) : S₂[Pg] } )
assume x in comp P ; :: thesis: x in { Pg where Pg is Element of comp (rng P) : S₂[Pg] }
then consider Q being consistent PNPair such that
A5: Q = x and
A6: Q is_completion_of P ;
( rng (Q `1) misses rng (Q `2) & rng Q = tau (rng P) ) by LTLAXIO3:30, A6;
then Q in comp (rng P) ;
then reconsider Q = Q as Element of comp (rng P) ;
S₂[Q] by A6;
hence x in { Pg where Pg is Element of comp (rng P) : S₂[Pg] } by A5; :: thesis: verum

end;

reconsider c1 = { Pg where Pg is Element of comp (rng P) : S₂[Pg] } as finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] by A1, XBOOLE_1:1;
A7: comp (rng P) = c1 \/ ((comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ) by XBOOLE_1:45, A1;
consider f2 being FinSequence such that
A8: rng f2 = ((comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ) ^ and
f2 is one-to-one by FINSEQ_4:58;
reconsider f2 = f2 as FinSequence of LTLB_WFF by A8, FINSEQ_1:def 4;
set r = H₂( nega (f ^ f2));
set s = H₂( nega f);
set t = H₂( nega f2);
assume A9: rng f = (comp P) ^ ; :: thesis: {} LTLB_WFF |- (P ^) => ('not' ((con (nega f)) /. (len (con (nega f)))))

A10: now :: thesis: for x being PNPair st x in (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } holds
not S₂[x]

let x be PNPair; :: thesis: ( x in (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } implies not S₂[x] )
assume A11: x in (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ; :: thesis: not S₂[x]
then reconsider x1 = x as Element of comp (rng P) by XBOOLE_0:def 5;
assume S₂[x] ; :: thesis: contradiction
then x1 in c1 ;
hence contradiction by A11, XBOOLE_0:def 5; :: thesis: verum

end;

A12: now :: thesis: for pi being PNPair st pi in (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } holds
{} LTLB_WFF |- (P ^) => ('not' (pi ^))

let pi be PNPair; :: thesis: ( pi in (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } implies {} LTLB_WFF |- (P ^) => ('not' (b₁ ^)) )
assume A13: pi in (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ; :: thesis: {} LTLB_WFF |- (P ^) => ('not' (b₁ ^))
then pi in comp (rng P) by XBOOLE_0:def 5;
then A14: ex Q being PNPair st
( Q = pi & rng Q = tau (rng P) & rng (Q `1) misses rng (Q `2) ) ;

per cases ( pi is Inconsistent or not S₁[pi] ) by A10, A13;

suppose A15: pi is Inconsistent ; :: thesis: {} LTLB_WFF |- (P ^) => ('not' (b₁ ^))

('not' (pi ^)) => ((P ^) => ('not' (pi ^))) is ctaut by LTLAXIO2:33;
then ('not' (pi ^)) => ((P ^) => ('not' (pi ^))) in LTL_axioms by LTLAXIO1:def 17;
then A16: {} LTLB_WFF |- ('not' (pi ^)) => ((P ^) => ('not' (pi ^))) by LTLAXIO1:42;
{} LTLB_WFF |- 'not' (pi ^) by A15;
hence {} LTLB_WFF |- (P ^) => ('not' (pi ^)) by A16, LTLAXIO1:43; :: thesis: verum

end;

suppose A17: not S₁[pi] ; :: thesis: {} LTLB_WFF |- (P ^) => ('not' (b₁ ^))

A18: now :: thesis: S₃[pi]

per cases ( not rng (P `1) c= rng (pi `1) or not rng (P `2) c= rng (pi `2) ) by A17;

suppose not rng (P `1) c= rng (pi `1) ; :: thesis: S₃[pi]

then consider x being object such that
A19: x in rng (P `1) and
A20: not x in rng (pi `1) ;
rng (P `1) c= rng P by XBOOLE_1:7;
then ( rng P c= tau (rng P) & x in rng P ) by LTLAXIO3:16, A19;
then x in rng (pi `2) by A14, XBOOLE_0:def 3, A20;
then x in (rng (P `1)) /\ (rng (pi `2)) by XBOOLE_0:def 4, A19;
hence S₃[pi] by XBOOLE_0:def 7; :: thesis: verum

end;

suppose not rng (P `2) c= rng (pi `2) ; :: thesis: S₃[pi]

then consider x being object such that
A21: x in rng (P `2) and
A22: not x in rng (pi `2) ;
rng (P `2) c= rng P by XBOOLE_1:7;
then ( rng P c= tau (rng P) & x in rng P ) by LTLAXIO3:16, A21;
then x in rng (pi `1) by A14, XBOOLE_0:def 3, A22;
then x in (rng (P `2)) /\ (rng (pi `1)) by XBOOLE_0:def 4, A21;
hence S₃[pi] by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

A23: now :: thesis: {} LTLB_WFF |- 'not' ((P ^) '&&' (pi ^))

per cases ( not rng (P `1) misses rng (pi `2) or not rng (P `2) misses rng (pi `1) ) by A18;

suppose A24: not rng (P `1) misses rng (pi `2) ; :: thesis: {} LTLB_WFF |- 'not' ((P ^) '&&' (pi ^))

set Q1 = [(P `1),(pi `2)];
set p = H₂([(P `1),(pi `2)] `1 );
set q = H<sub>2</sub>( nega ([(P `1),(pi `2)] `2));
not rng ([(P `1),(pi `2)] `1) misses rng ([(P `1),(pi `2)] `2) by A24;
then [(P `1),(pi `2)] is Inconsistent by LTLAXIO3:30;
then A25: {} LTLB_WFF |- 'not' ([(P `1),(pi `2)] ^) ;
A26: ('not' (H₂(P `1 ) '&&' H<sub>2</sub>( nega (pi `2)))) => ('not' ((P ^) '&&' (pi ^))) is ctaut by LTLAXIO2:42;
('not' ([(P `1),(pi `2)] ^)) => ('not' ((P ^) '&&' (pi ^))) in LTL_axioms by A26, LTLAXIO1:def 17;
then {} LTLB_WFF |- ('not' ([(P `1),(pi `2)] ^)) => ('not' ((P ^) '&&' (pi ^))) by LTLAXIO1:42;
hence {} LTLB_WFF |- 'not' ((P ^) '&&' (pi ^)) by LTLAXIO1:43, A25; :: thesis: verum

end;

suppose A27: not rng (P `2) misses rng (pi `1) ; :: thesis: {} LTLB_WFF |- 'not' ((P ^) '&&' (pi ^))

set Q2 = [(pi `1),(P `2)];
set p = H₂([(pi `1),(P `2)] `1 );
set q = H<sub>2</sub>( nega ([(pi `1),(P `2)] `2));
not rng ([(pi `1),(P `2)] `2) misses rng ([(pi `1),(P `2)] `1) by A27;
then [(pi `1),(P `2)] is Inconsistent by LTLAXIO3:30;
then A28: {} LTLB_WFF |- 'not' ([(pi `1),(P `2)] ^) ;
A29: ('not' (H₂(pi `1 ) '&&' H<sub>2</sub>( nega (P `2)))) => ('not' ((P ^) '&&' (pi ^))) is ctaut by LTLAXIO2:41;
('not' ([(pi `1),(P `2)] ^)) => ('not' ((P ^) '&&' (pi ^))) in LTL_axioms by A29, LTLAXIO1:def 17;
then {} LTLB_WFF |- ('not' ([(pi `1),(P `2)] ^)) => ('not' ((P ^) '&&' (pi ^))) by LTLAXIO1:42;
hence {} LTLB_WFF |- 'not' ((P ^) '&&' (pi ^)) by LTLAXIO1:43, A28; :: thesis: verum

end;

end;

end;

('not' ((P ^) '&&' (pi ^))) => ((P ^) => ('not' (pi ^))) is ctaut by LTLAXIO2:37;
then ('not' ((P ^) '&&' (pi ^))) => ((P ^) => ('not' (pi ^))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- ('not' ((P ^) '&&' (pi ^))) => ((P ^) => ('not' (pi ^))) by LTLAXIO1:42;
hence {} LTLB_WFF |- (P ^) => ('not' (pi ^)) by LTLAXIO1:43, A23; :: thesis: verum

end;

end;

end;

A30: for p being Element of LTLB_WFF st p in ((comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ) ^ holds
{} LTLB_WFF |- (P ^) => ('not' p)

proof

let p be Element of LTLB_WFF ; :: thesis: ( p in ((comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ) ^ implies {} LTLB_WFF |- (P ^) => ('not' p) )
assume p in ((comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ) ^ ; :: thesis: {} LTLB_WFF |- (P ^) => ('not' p)
then ex Q being PNPair st
( p = Q ^ & Q in (comp (rng P)) \ { Pg where Pg is Element of comp (rng P) : S₂[Pg] } ) ;
hence {} LTLB_WFF |- (P ^) => ('not' p) by A12; :: thesis: verum

end;

A31: now :: thesis: {} LTLB_WFF |- (P ^) => H₂( nega f2)

per cases ( len f2 = 0 or len f2 > 0 ) ;

suppose A32: len f2 = 0 ; :: thesis: {} LTLB_WFF |- (P ^) => H₂( nega f2)

(P ^) => TVERUM is ctaut

proof

let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . ((P ^) => TVERUM) = 1
set v = VAL g;
thus (VAL g) . ((P ^) => TVERUM) = ((VAL g) . (P ^)) => ((VAL g) . TVERUM) by LTLAXIO1:def 15
.= ((VAL g) . (P ^)) => TRUE by LTLAXIO2:4
.= 1 ; :: thesis: verum

end;

then A33: (P ^) => TVERUM in LTL_axioms by LTLAXIO1:def 17;
len (nega f2) = 0 by A32, LTLAXIO2:def 4;
then nega f2 = {} ;
hence {} LTLB_WFF |- (P ^) => H₂( nega f2) by A33, LTLAXIO1:42, LTLAXIO2:10; :: thesis: verum

end;

suppose A34: len f2 > 0 ; :: thesis: {} LTLB_WFF |- (P ^) => H₂( nega f2)

set t1 = con (nega f2);
A35: len (nega f2) > 0 by A34, LTLAXIO2:def 4;
then reconsider lt1 = len (con (nega f2)) as non zero Nat by LTLAXIO2:def 2;
defpred S₄[ Nat] means ( $1 <= len (con (nega f2)) implies {} LTLB_WFF |- (P ^) => ((con (nega f2)) /. $1) );

A36: now :: thesis: for k being non zero Nat st S₄[k] holds
S₄[k + 1]

let k be non zero Nat; :: thesis: ( S₄[k] implies S₄[k + 1] )
assume A37: S₄[k] ; :: thesis: S₄[k + 1]
thus S₄[k + 1] :: thesis: verum

proof

set a = (con (nega f2)) /. k;
set b = (nega f2) /. (k + 1);
reconsider k1 = k as non empty Element of NAT by ORDINAL1:def 12;
assume A38: k + 1 <= len (con (nega f2)) ; :: thesis: {} LTLB_WFF |- (P ^) => ((con (nega f2)) /. (k + 1))
((P ^) => ((con (nega f2)) /. k)) => (((P ^) => ((nega f2) /. (k + 1))) => ((P ^) => (((con (nega f2)) /. k) '&&' ((nega f2) /. (k + 1))))) is ctaut by LTLAXIO2:40;
then ((P ^) => ((con (nega f2)) /. k)) => (((P ^) => ((nega f2) /. (k + 1))) => ((P ^) => (((con (nega f2)) /. k) '&&' ((nega f2) /. (k + 1))))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- ((P ^) => ((con (nega f2)) /. k)) => (((P ^) => ((nega f2) /. (k + 1))) => ((P ^) => (((con (nega f2)) /. k) '&&' ((nega f2) /. (k + 1))))) by LTLAXIO1:42;
then A39: {} LTLB_WFF |- ((P ^) => ((nega f2) /. (k + 1))) => ((P ^) => (((con (nega f2)) /. k) '&&' ((nega f2) /. (k + 1)))) by LTLAXIO1:43, A38, NAT_1:13, A37;
A40: k + 1 <= len (nega f2) by A38, LTLAXIO2:def 2, A35;
then k + 1 <= len f2 by LTLAXIO2:def 4;
then A41: k1 + 1 in dom f2 by NAT_1:12, FINSEQ_3:25;
then {} LTLB_WFF |- (P ^) => ('not' (f2 /. (k + 1))) by PARTFUN2:2, A8, A30;
then {} LTLB_WFF |- (P ^) => ((nega f2) /. (k + 1)) by LTLAXIO2:8, A41;
then ( 1 <= k1 & {} LTLB_WFF |- (P ^) => (((con (nega f2)) /. k) '&&' ((nega f2) /. (k + 1))) ) by NAT_1:25, A39, LTLAXIO1:43;
hence {} LTLB_WFF |- (P ^) => ((con (nega f2)) /. (k + 1)) by LTLAXIO2:7, NAT_1:13, A40; :: thesis: verum

end;

end;

A42: S₄[1]

proof

assume 1 <= len (con (nega f2)) ; :: thesis: {} LTLB_WFF |- (P ^) => ((con (nega f2)) /. 1)
1 <= len f2 by A34, NAT_1:25;
then A43: 1 in dom f2 by FINSEQ_3:25;
(con (nega f2)) /. 1 = (nega f2) /. 1 by A35, LTLAXIO2:6
.= 'not' (f2 /. 1) by LTLAXIO2:8, A43 ;
hence {} LTLB_WFF |- (P ^) => ((con (nega f2)) /. 1) by PARTFUN2:2, A43, A8, A30; :: thesis: verum

end;

for k being non zero Nat holds S₄[k] from NAT_1:sch 10(A42, A36);
then {} LTLB_WFF |- (P ^) => ((con (nega f2)) /. lt1) ;
hence {} LTLB_WFF |- (P ^) => H₂( nega f2) ; :: thesis: verum

end;

end;

end;

A44: nega (f ^ f2) = (nega f) ^ (nega f2) by LTLAXIO2:16;

now :: thesis: for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . (('not' H₂( nega (f ^ f2))) => ('not' (H₂( nega f) '&&' H₂( nega f2)))) = 1

let g be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL g) . (('not' H₂( nega (f ^ f2))) => ('not' (H₂( nega f) '&&' H₂( nega f2)))) = 1
set v = VAL g;
A45: ( (VAL g) . H₂( nega (f ^ f2)) = FALSE or (VAL g) . H₂( nega (f ^ f2)) = TRUE ) by XBOOLEAN:def 3;
A46: (VAL g) . H₂( nega (f ^ f2)) = ((VAL g) . H₂( nega f)) '&' ((VAL g) . H₂( nega f2)) by LTLAXIO2:17, A44;
thus (VAL g) . (('not' H₂( nega (f ^ f2))) => ('not' (H₂( nega f) '&&' H₂( nega f2)))) = ((VAL g) . ('not' H₂( nega (f ^ f2)))) => ((VAL g) . ('not' (H₂( nega f) '&&' H₂( nega f2)))) by LTLAXIO1:def 15
.= (((VAL g) . H₂( nega (f ^ f2))) => ((VAL g) . TFALSUM)) => ((VAL g) . ('not' (H₂( nega f) '&&' H₂( nega f2)))) by LTLAXIO1:def 15
.= (((VAL g) . H₂( nega (f ^ f2))) => FALSE) => ((VAL g) . ('not' (H₂( nega f) '&&' H₂( nega f2)))) by LTLAXIO1:def 15
.= (((VAL g) . H₂( nega (f ^ f2))) => FALSE) => (((VAL g) . (H₂( nega f) '&&' H₂( nega f2))) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15
.= (((VAL g) . H₂( nega (f ^ f2))) => FALSE) => (((VAL g) . (H₂( nega f) '&&' H₂( nega f2))) => FALSE) by LTLAXIO1:def 15
.= 1 by A45, A46, LTLAXIO1:31 ; :: thesis: verum

end;

then ('not' H₂( nega (f ^ f2))) => ('not' (H₂( nega f) '&&' H₂( nega f2))) is ctaut ;
then ('not' H₂( nega (f ^ f2))) => ('not' (H₂( nega f) '&&' H₂( nega f2))) in LTL_axioms by LTLAXIO1:def 17;
then A47: {} LTLB_WFF |- ('not' H₂( nega (f ^ f2))) => ('not' (H₂( nega f) '&&' H₂( nega f2))) by LTLAXIO1:42;
('not' (H₂( nega f) '&&' H₂( nega f2))) => (((P ^) => H₂( nega f2)) => ((P ^) => ('not' H₂( nega f)))) is ctaut by LTLAXIO2:39;
then ('not' (H₂( nega f) '&&' H₂( nega f2))) => (((P ^) => H₂( nega f2)) => ((P ^) => ('not' H₂( nega f)))) in LTL_axioms by LTLAXIO1:def 17;
then A48: {} LTLB_WFF |- ('not' (H₂( nega f) '&&' H₂( nega f2))) => (((P ^) => H₂( nega f2)) => ((P ^) => ('not' H₂( nega f)))) by LTLAXIO1:42;
rng (f ^ f2) = (rng f) \/ (rng f2) by FINSEQ_1:31
.= (comp (rng P)) ^ by A7, Th10, A9, A2, A8 ;
then {} LTLB_WFF |- 'not' H₂( nega (f ^ f2)) by Th16;
then {} LTLB_WFF |- 'not' (H₂( nega f) '&&' H₂( nega f2)) by A47, LTLAXIO1:43;
then {} LTLB_WFF |- ((P ^) => H₂( nega f2)) => ((P ^) => ('not' H₂( nega f))) by A48, LTLAXIO1:43;
hence {} LTLB_WFF |- (P ^) => ('not' H₂( nega f)) by LTLAXIO1:43, A31; :: thesis: verum