let F be finite Subset of LTLB_WFF; :: thesis: for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds
{} LTLB_WFF |- 'not' ((con (nega f)) /. (len (con (nega f))))
let f be FinSequence of LTLB_WFF ; :: thesis: ( rng f = (comp F) ^ implies {} LTLB_WFF |- 'not' ((con (nega f)) /. (len (con (nega f)))) )
defpred S₁[ Nat] means for F being finite Subset of LTLB_WFF st card (tau F) = $1 holds
for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds
{} LTLB_WFF |- H₁(f);
assume A1: rng f = (comp F) ^ ; :: thesis: {} LTLB_WFF |- 'not' ((con (nega f)) /. (len (con (nega f))))
A2: card (tau F) = card (tau F) ;

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let G be finite Subset of LTLB_WFF; :: thesis: ( card (tau G) = k + 1 implies for f being FinSequence of LTLB_WFF st rng f = (comp G) ^ holds
{} LTLB_WFF |- H₁(f) )
assume A5: card (tau G) = k + 1 ; :: thesis: for f being FinSequence of LTLB_WFF st rng f = (comp G) ^ holds
{} LTLB_WFF |- H₁(f)
then reconsider H = G as non empty finite Subset of LTLB_WFF ;
let g be FinSequence of LTLB_WFF ; :: thesis: ( rng g = (comp G) ^ implies {} LTLB_WFF |- H₁(g) )
consider A being Element of LTLB_WFF such that
A6: A in tau H and
A7: tau ((tau H) \ {A}) = (tau H) \ {A} by Th15;
set Fp = (tau H) \ {A};
consider ff being FinSequence such that
A8: rng ff = comp ((tau H) \ {A}) and
ff is one-to-one by FINSEQ_4:58;
reconsider ff = ff as FinSequence of [:(LTLB_WFF **),(LTLB_WFF **):] by A8, FINSEQ_1:def 4;
deffunc H₃( Nat) -> Element of LTLB_WFF = [(((ff /. $1) `1) ^^ <*A*>),((ff /. $1) `2)] ^ ;
deffunc H₄( Nat) -> Element of LTLB_WFF = [((ff /. $1) `1),(((ff /. $1) `2) ^^ <*A*>)] ^ ;
consider ff1 being FinSequence of LTLB_WFF such that
A9: ( len ff1 = len ff & ( for i being Nat st i in dom ff1 holds
ff1 /. i = H₃(i) ) ) from FINSEQ_4:sch 2();
consider ff2 being FinSequence of LTLB_WFF such that
A10: ( len ff2 = len ff & ( for i being Nat st i in dom ff2 holds
ff2 /. i = H₄(i) ) ) from FINSEQ_4:sch 2();
set fl = ff1 ^ ff2;

A11: now :: thesis: for i being Nat st ( i in dom ff1 or i in dom ff2 ) holds
( rng (ff /. i) = tau ((tau H) \ {A}) & rng ((ff /. i) `1) misses rng ((ff /. i) `2) )

let i be Nat; :: thesis: ( ( i in dom ff1 or i in dom ff2 ) implies ( rng (ff /. i) = tau ((tau H) \ {A}) & rng ((ff /. i) `1) misses rng ((ff /. i) `2) ) )
set Q = ff /. i;
assume ( i in dom ff1 or i in dom ff2 ) ; :: thesis: ( rng (ff /. i) = tau ((tau H) \ {A}) & rng ((ff /. i) `1) misses rng ((ff /. i) `2) )
then i in dom ff by A9, A10, FINSEQ_3:29;
then ff /. i in comp ((tau H) \ {A}) by PARTFUN2:2, A8;
then ex R being PNPair st
( R = ff /. i & rng R = tau ((tau H) \ {A}) & rng (R `1) misses rng (R `2) ) ;
hence ( rng (ff /. i) = tau ((tau H) \ {A}) & rng ((ff /. i) `1) misses rng ((ff /. i) `2) ) ; :: thesis: verum

end;

tau ((tau H) \ {A}) misses {A} by XBOOLE_1:79, A7;
then A12: tau ((tau H) \ {A}) misses rng <*A*> by FINSEQ_1:38;

A13: now :: thesis: for i being Nat st i in dom ff1 holds
( rng ((ff /. i) `1) misses rng <*A*> & rng ((ff /. i) `2) misses rng <*A*> )

let i be Nat; :: thesis: ( i in dom ff1 implies ( rng ((ff /. i) `1) misses rng <*A*> & rng ((ff /. i) `2) misses rng <*A*> ) )
set Q = ff /. i;
assume i in dom ff1 ; :: thesis: ( rng ((ff /. i) `1) misses rng <*A*> & rng ((ff /. i) `2) misses rng <*A*> )
then A14: rng (ff /. i) misses rng <*A*> by A12, A11;
hence rng ((ff /. i) `1) misses rng <*A*> by XBOOLE_1:7, XBOOLE_1:63; :: thesis: rng ((ff /. i) `2) misses rng <*A*>
thus rng ((ff /. i) `2) misses rng <*A*> by XBOOLE_1:7, A14, XBOOLE_1:63; :: thesis: verum

end;

A15: now :: thesis: for i being Nat st i in dom ff2 holds
( rng ((ff /. i) `2) misses rng <*A*> & rng ((ff /. i) `1) misses rng <*A*> )

let i be Nat; :: thesis: ( i in dom ff2 implies ( rng ((ff /. i) `2) misses rng <*A*> & rng ((ff /. i) `1) misses rng <*A*> ) )
set Q = ff /. i;
assume i in dom ff2 ; :: thesis: ( rng ((ff /. i) `2) misses rng <*A*> & rng ((ff /. i) `1) misses rng <*A*> )
then A16: rng (ff /. i) misses rng <*A*> by A12, A11;
hence rng ((ff /. i) `2) misses rng <*A*> by XBOOLE_1:7, XBOOLE_1:63; :: thesis: rng ((ff /. i) `1) misses rng <*A*>
thus rng ((ff /. i) `1) misses rng <*A*> by XBOOLE_1:7, A16, XBOOLE_1:63; :: thesis: verum

end;

A17: rng (ff1 ^ ff2) c= (comp G) ^

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (ff1 ^ ff2) or x in (comp G) ^ )
assume x in rng (ff1 ^ ff2) ; :: thesis: x in (comp G) ^
then A18: x in (rng ff1) \/ (rng ff2) by FINSEQ_1:31;

per cases ( x in rng ff1 or x in rng ff2 ) by A18, XBOOLE_0:def 3;

suppose A19: x in rng ff1 ; :: thesis: x in (comp G) ^

set i = x .. ff1;
set Q = ff /. (x .. ff1);
set P1 = [(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)];
A20: x .. ff1 in dom ff1 by A19, FINSEQ_4:20;
then A21: rng ((ff /. (x .. ff1)) `1) misses rng <*A*> by A13;
rng ((ff /. (x .. ff1)) `2) misses rng <*A*> by A13, A20;
then A22: rng ([(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)] `2) misses {A} by FINSEQ_1:38;
A23: rng ([(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)] `1) = rng (((ff /. (x .. ff1)) `1) ^ <*A*>) by LTLAXIO3:def 3, A21
.= (rng ((ff /. (x .. ff1)) `1)) \/ (rng <*A*>) by FINSEQ_1:31
.= (rng ((ff /. (x .. ff1)) `1)) \/ {A} by FINSEQ_1:38 ;
rng ((ff /. (x .. ff1)) `1) misses rng ((ff /. (x .. ff1)) `2) by A11, A20;
then A24: rng ([(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)] `1) misses rng ([(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)] `2) by XBOOLE_1:70, A22, A23;
rng [(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)] = {A} \/ (rng (ff /. (x .. ff1))) by XBOOLE_1:4, A23
.= {A} \/ (tau ((tau H) \ {A})) by A11, A20
.= tau G by XBOOLE_1:45, ZFMISC_1:31, A6, A7 ;
then A25: [(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)] in comp G by A24;
x = ff1 /. (x .. ff1) by FINSEQ_5:38, A19
.= [(((ff /. (x .. ff1)) `1) ^^ <*A*>),((ff /. (x .. ff1)) `2)] ^ by A9, A19, FINSEQ_4:20 ;
hence x in (comp G) ^ by A25; :: thesis: verum

end;

suppose A26: x in rng ff2 ; :: thesis: x in (comp G) ^

set i = x .. ff2;
set Q = ff /. (x .. ff2);
set P1 = [((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)];
A27: x .. ff2 in dom ff2 by A26, FINSEQ_4:20;
then A28: rng ((ff /. (x .. ff2)) `2) misses rng <*A*> by A15;
rng ((ff /. (x .. ff2)) `1) misses rng <*A*> by A15, A27;
then A29: rng ([((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)] `1) misses {A} by FINSEQ_1:38;
A30: rng ([((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)] `2) = rng (((ff /. (x .. ff2)) `2) ^ <*A*>) by LTLAXIO3:def 3, A28
.= (rng ((ff /. (x .. ff2)) `2)) \/ (rng <*A*>) by FINSEQ_1:31
.= (rng ((ff /. (x .. ff2)) `2)) \/ {A} by FINSEQ_1:38 ;
rng ((ff /. (x .. ff2)) `2) misses rng ((ff /. (x .. ff2)) `1) by A11, A27;
then A31: rng ([((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)] `1) misses rng ([((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)] `2) by XBOOLE_1:70, A29, A30;
rng [((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)] = {A} \/ (rng (ff /. (x .. ff2))) by XBOOLE_1:4, A30
.= {A} \/ (tau ((tau H) \ {A})) by A11, A27
.= tau G by XBOOLE_1:45, ZFMISC_1:31, A6, A7 ;
then A32: [((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)] in comp G by A31;
x = ff2 /. (x .. ff2) by FINSEQ_5:38, A26
.= [((ff /. (x .. ff2)) `1),(((ff /. (x .. ff2)) `2) ^^ <*A*>)] ^ by A10, A26, FINSEQ_4:20 ;
hence x in (comp G) ^ by A32; :: thesis: verum

end;

end;

end;

assume A33: rng g = (comp G) ^ ; :: thesis: {} LTLB_WFF |- H₁(g)
H₁(ff1 ^ ff2) => H₁(g) is ctaut

proof

let h be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL h) . (H₁(ff1 ^ ff2) => H₁(g)) = 1
set v = VAL h;
A34: ( (VAL h) . H₁(g) = 1 or (VAL h) . H₁(g) = 0 ) by XBOOLEAN:def 3;

A35: now :: thesis: ( (VAL h) . H₁(ff1 ^ ff2) = 1 implies not (VAL h) . H₁(g) = 0 )

assume that
A36: (VAL h) . H₁(ff1 ^ ff2) = 1 and
A37: (VAL h) . H₁(g) = 0 ; :: thesis: contradiction

per cases ( len (ff1 ^ ff2) = 0 or len (ff1 ^ ff2) > 0 ) ;

suppose len (ff1 ^ ff2) = 0 ; :: thesis: contradiction

then len (nega (ff1 ^ ff2)) = 0 by LTLAXIO2:def 4;
then con (nega (ff1 ^ ff2)) = <*TVERUM*> by LTLAXIO2:def 2;
then H₁(ff1 ^ ff2) = 'not' (<*TVERUM*> /. 1) by FINSEQ_1:39
.= 'not' TVERUM by FINSEQ_4:16 ;
then (VAL h) . H₁(ff1 ^ ff2) = ((VAL h) . TVERUM) => ((VAL h) . TFALSUM) by LTLAXIO1:def 15
.= TRUE => ((VAL h) . TFALSUM) by LTLAXIO2:4 ;
hence contradiction by A36, LTLAXIO1:def 15; :: thesis: verum

end;

suppose len (ff1 ^ ff2) > 0 ; :: thesis: contradiction

((VAL h) . H₂( nega (ff1 ^ ff2))) => ((VAL h) . TFALSUM) = 1 by A36, LTLAXIO1:def 15;
then ((VAL h) . H₂( nega (ff1 ^ ff2))) => FALSE = 1 by LTLAXIO1:def 15;
then consider i being Nat such that
A38: i in dom (nega (ff1 ^ ff2)) and
A39: not (VAL h) . ((nega (ff1 ^ ff2)) /. i) = 1 by LTLAXIO2:19;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
len (ff1 ^ ff2) = len (nega (ff1 ^ ff2)) by LTLAXIO2:def 4;
then A40: i1 in dom (ff1 ^ ff2) by FINSEQ_3:29, A38;
then A41: not (VAL h) . ('not' ((ff1 ^ ff2) /. i1)) = 1 by LTLAXIO2:8, A39;
set j = ((ff1 ^ ff2) /. i1) .. g;
((VAL h) . H₂( nega g)) => ((VAL h) . TFALSUM) = 0 by A37, LTLAXIO1:def 15;
then A42: ((VAL h) . H₂( nega g)) => FALSE = 0 by LTLAXIO1:def 15;
A43: (ff1 ^ ff2) /. i1 in rng (ff1 ^ ff2) by PARTFUN2:2, A40;
then A44: ((ff1 ^ ff2) /. i1) .. g in dom g by A17, A33, FINSEQ_4:20;
then ((ff1 ^ ff2) /. i1) .. g <= len g by FINSEQ_3:25;
then A45: ((ff1 ^ ff2) /. i1) .. g <= len (nega g) by LTLAXIO2:def 4;
1 <= ((ff1 ^ ff2) /. i1) .. g by A44, FINSEQ_3:25;
then A46: ((ff1 ^ ff2) /. i1) .. g in dom (nega g) by A45, FINSEQ_3:25;
(nega g) /. (((ff1 ^ ff2) /. i1) .. g) = 'not' (g /. (((ff1 ^ ff2) /. i1) .. g)) by LTLAXIO2:8, A44
.= 'not' ((ff1 ^ ff2) /. i1) by FINSEQ_5:38, A43, A17, A33 ;
hence contradiction by A42, A46, LTLAXIO2:19, A41; :: thesis: verum

end;

end;

end;

thus (VAL h) . (H₁(ff1 ^ ff2) => H₁(g)) = ((VAL h) . H₁(ff1 ^ ff2)) => ((VAL h) . H₁(g)) by LTLAXIO1:def 15
.= 1 by A35, A34, XBOOLEAN:def 3 ; :: thesis: verum

end;

then H₁(ff1 ^ ff2) => H₁(g) in LTL_axioms by LTLAXIO1:def 17;
then A47: {} LTLB_WFF |- H₁(ff1 ^ ff2) => H₁(g) by LTLAXIO1:42;
deffunc H₅( Nat) -> Element of LTLB_WFF = (ff /. $1) ^ ;
consider fk being FinSequence of LTLB_WFF such that
A48: ( len fk = len ff & ( for i being Nat st i in dom fk holds
fk /. i = H₅(i) ) ) from FINSEQ_4:sch 2();

A49: now :: thesis: for g being Function of LTLB_WFF,BOOLEAN st (VAL g) . H₁(fk) = 1 holds
(VAL g) . H₁(ff1 ^ ff2) = 1

let g be Function of LTLB_WFF,BOOLEAN; :: thesis: ( (VAL g) . H₁(fk) = 1 implies (VAL g) . H₁(ff1 ^ ff2) = 1 )
set v = VAL g;
assume (VAL g) . H₁(fk) = 1 ; :: thesis: (VAL g) . H₁(ff1 ^ ff2) = 1
then ((VAL g) . H₂( nega fk)) => ((VAL g) . TFALSUM) = 1 by LTLAXIO1:def 15;
then ((VAL g) . H₂( nega fk)) => FALSE = 1 by LTLAXIO1:def 15;
then consider i being Nat such that
A50: i in dom (nega fk) and
A51: not (VAL g) . ((nega fk) /. i) = 1 by LTLAXIO2:19;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
A52: 1 <= i1 by FINSEQ_3:25, A50;
i1 <= len (nega fk) by FINSEQ_3:25, A50;
then A53: i1 <= len fk by LTLAXIO2:def 4;
(nega fk) /. i = (nega fk) . i1 by A50, PARTFUN1:def 6
.= 'not' (fk /. i1) by LTLAXIO2:def 4, A53, A52 ;
then A54: (VAL g) . ((nega fk) /. i) = ((VAL g) . (fk /. i1)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= ((VAL g) . (fk /. i1)) => FALSE by LTLAXIO1:def 15 ;
A55: (VAL g) . (fk /. i1) = (VAL g) . ((ff /. i1) ^) by A53, FINSEQ_3:25, A52, A48
.= ((VAL g) . H₂((ff /. i1) `1 )) '&' ((VAL g) . H<sub>2</sub>( nega ((ff /. i1) `2))) by LTLAXIO1:31 ;

now :: thesis: not (VAL g) . H₁(ff1 ^ ff2) = 0

dom (nega ff1) c= dom ((nega ff1) ^ (nega ff2)) by FINSEQ_1:26;
then A56: dom (nega ff1) c= dom (nega (ff1 ^ ff2)) by LTLAXIO2:16;
assume (VAL g) . H₁(ff1 ^ ff2) = 0 ; :: thesis: contradiction
then ((VAL g) . H₂( nega (ff1 ^ ff2))) => ((VAL g) . TFALSUM) = 0 by LTLAXIO1:def 15;
then A57: ((VAL g) . H₂( nega (ff1 ^ ff2))) => FALSE = 0 by LTLAXIO1:def 15;

per cases ( (VAL g) . A = 1 or (VAL g) . A = 0 ) by XBOOLEAN:def 3;

suppose A58: (VAL g) . A = 1 ; :: thesis: contradiction

i1 <= len (nega ff1) by A9, A48, A53, LTLAXIO2:def 4;
then A59: i in dom (nega ff1) by A52, FINSEQ_3:25;
set a = ((ff /. i1) `1) ^^ <*A*>;
set b = (ff /. i1) `2 ;
i1 in dom ff1 by A52, A9, A48, A53, FINSEQ_3:25;
then rng ((ff /. i1) `1) misses rng <*A*> by A13;
then A60: ((ff /. i1) `1) ^^ <*A*> = ((ff /. i1) `1) ^ <*A*> by LTLAXIO3:def 3;
A61: (nega (ff1 ^ ff2)) /. i1 = ((nega ff1) ^ (nega ff2)) /. i by LTLAXIO2:16
.= (nega ff1) /. i by FINSEQ_4:68, A59
.= (nega ff1) . i1 by PARTFUN1:def 6, A59
.= 'not' (ff1 /. i1) by LTLAXIO2:def 4, A52, A9, A48, A53 ;
A62: 1 = (VAL g) . ((nega (ff1 ^ ff2)) /. i1) by A57, A59, A56, LTLAXIO2:19
.= ((VAL g) . (ff1 /. i1)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15, A61
.= ((VAL g) . (ff1 /. i1)) => FALSE by LTLAXIO1:def 15 ;
(VAL g) . (ff1 /. i1) = (VAL g) . ([(((ff /. i1) `1) ^^ <*A*>),((ff /. i1) `2)] ^) by A9, A52, A48, A53, FINSEQ_3:25
.= ((VAL g) . H<sub>2</sub>(((ff /. i1) `1) ^^ <*A*>)) '&' ((VAL g) . H₂( nega ((ff /. i1) `2))) by LTLAXIO1:31
.= (((VAL g) . H<sub>2</sub>((ff /. i1) `1 )) '&' ((VAL g) . H₂(<*A*>))) '&' ((VAL g) . H₂( nega ((ff /. i1) `2))) by LTLAXIO2:17, A60
.= (((VAL g) . H<sub>2</sub>((ff /. i1) `1 )) '&' ((VAL g) . A)) '&' ((VAL g) . H₂( nega ((ff /. i1) `2))) by LTLAXIO2:11
.= 1 by A54, A51, XBOOLEAN:def 3, A58, A55 ;
hence contradiction by A62; :: thesis: verum

end;

suppose A63: (VAL g) . A = 0 ; :: thesis: contradiction

set b = ((ff /. i1) `2) ^^ <*A*>;
set a = (ff /. i1) `1 ;
i1 in dom ff2 by A52, A53, A10, A48, FINSEQ_3:25;
then rng ((ff /. i1) `2) misses rng <*A*> by A15;
then A64: ( nega (((ff /. i1) `2) ^ <*A*>) = (nega ((ff /. i1) `2)) ^ (nega <*A*>) & ((ff /. i1) `2) ^^ <*A*> = ((ff /. i1) `2) ^ <*A*> ) by LTLAXIO2:16, LTLAXIO3:def 3;
nega <*A*> = <*('not' A)*> by LTLAXIO2:14;
then (VAL g) . H<sub>2</sub>( nega <*A*>) = (VAL g) . ('not' A) by LTLAXIO2:11
.= ((VAL g) . A) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= 1 by A63 ;
then A65: (VAL g) . H<sub>2</sub>( nega (((ff /. i1) `2) ^^ <*A*>)) = ((VAL g) . H₂( nega ((ff /. i1) `2))) '&' TRUE by A64, LTLAXIO2:17;
reconsider j = (len ff1) + i1 as Element of NAT ;
A66: j = (len (nega ff1)) + i1 by LTLAXIO2:def 4;
i1 <= len (nega ff2) by A53, A10, A48, LTLAXIO2:def 4;
then A67: i1 in dom (nega ff2) by FINSEQ_3:25, A52;
A68: j in dom (ff1 ^ ff2) by FINSEQ_1:28, A52, A53, A10, A48, FINSEQ_3:25;
then j <= len (ff1 ^ ff2) by FINSEQ_3:25;
then A69: j <= len (nega (ff1 ^ ff2)) by LTLAXIO2:def 4;
A70: (nega (ff1 ^ ff2)) /. j = ((nega ff1) ^ (nega ff2)) /. j by LTLAXIO2:16
.= (nega ff2) /. i1 by FINSEQ_4:69, A67, A66
.= (nega ff2) . i1 by PARTFUN1:def 6, A67
.= 'not' (ff2 /. i1) by LTLAXIO2:def 4, A52, A53, A10, A48 ;
1 <= j by A68, FINSEQ_3:25;
then j in dom (nega (ff1 ^ ff2)) by A69, FINSEQ_3:25;
then A71: 1 = (VAL g) . ((nega (ff1 ^ ff2)) /. j) by A57, LTLAXIO2:19
.= ((VAL g) . (ff2 /. i1)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15, A70
.= ((VAL g) . (ff2 /. i1)) => FALSE by LTLAXIO1:def 15 ;
(VAL g) . (ff2 /. i1) = (VAL g) . ([((ff /. i1) `1),(((ff /. i1) `2) ^^ <*A*>)] ^) by A10, A52, A53, A48, FINSEQ_3:25
.= ((VAL g) . H<sub>2</sub>((ff /. i1) `1 )) '&' ((VAL g) . H₂( nega (((ff /. i1) `2) ^^ <*A*>))) by LTLAXIO1:31
.= 1 by A54, A51, XBOOLEAN:def 3, A55, A65 ;
hence contradiction by A71; :: thesis: verum

end;

end;

end;

hence (VAL g) . H₁(ff1 ^ ff2) = 1 by XBOOLEAN:def 3; :: thesis: verum

end;

H₁(fk) => H₁(ff1 ^ ff2) is ctaut

proof

let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . (H₁(fk) => H₁(ff1 ^ ff2)) = 1
set v = VAL g;

now :: thesis: not (VAL g) . (H₁(fk) => H₁(ff1 ^ ff2)) = 0

assume (VAL g) . (H₁(fk) => H₁(ff1 ^ ff2)) = 0 ; :: thesis: contradiction
then A72: ((VAL g) . H₁(fk)) => ((VAL g) . H₁(ff1 ^ ff2)) = 0 by LTLAXIO1:def 15;
( (VAL g) . H₁(ff1 ^ ff2) = 1 or (VAL g) . H₁(ff1 ^ ff2) = 0 ) by XBOOLEAN:def 3;
hence contradiction by A72, A49; :: thesis: verum

end;

hence (VAL g) . (H₁(fk) => H₁(ff1 ^ ff2)) = 1 by XBOOLEAN:def 3; :: thesis: verum

end;

then H₁(fk) => H₁(ff1 ^ ff2) in LTL_axioms by LTLAXIO1:def 17;
then A73: {} LTLB_WFF |- H₁(fk) => H₁(ff1 ^ ff2) by LTLAXIO1:42;
A74: rng fk = (comp ((tau H) \ {A})) ^

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (comp ((tau H) \ {A})) ^ c= rng fk

let x be object ; :: thesis: ( x in rng fk implies x in (comp ((tau H) \ {A})) ^ )
assume A75: x in rng fk ; :: thesis: x in (comp ((tau H) \ {A})) ^
then reconsider x1 = x as Element of LTLB_WFF ;
set i = x1 .. fk;
x1 .. fk in dom fk by A75, FINSEQ_4:20;
then x1 .. fk in dom ff by A48, FINSEQ_3:29;
then A76: ff /. (x1 .. fk) in comp ((tau H) \ {A}) by A8, PARTFUN2:2;
x1 = fk /. (x1 .. fk) by A75, FINSEQ_5:38
.= (ff /. (x1 .. fk)) ^ by A48, A75, FINSEQ_4:20 ;
hence x in (comp ((tau H) \ {A})) ^ by A76; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (comp ((tau H) \ {A})) ^ or x in rng fk )
assume x in (comp ((tau H) \ {A})) ^ ; :: thesis: x in rng fk
then consider P1 being PNPair such that
A77: x = P1 ^ and
A78: P1 in comp ((tau H) \ {A}) ;
set i = P1 .. ff;
P1 .. ff in dom ff by FINSEQ_4:20, A8, A78;
then A79: P1 .. ff in dom fk by FINSEQ_3:29, A48;
then fk /. (P1 .. ff) = (ff /. (P1 .. ff)) ^ by A48
.= x by A77, FINSEQ_5:38, A8, A78 ;
hence x in rng fk by PARTFUN2:2, A79; :: thesis: verum

end;

card (tau ((tau H) \ {A})) = k by STIRL2_1:55, A6, A7, A5;
then {} LTLB_WFF |- H₁(fk) by A74, A4;
then {} LTLB_WFF |- H₁(ff1 ^ ff2) by A73, LTLAXIO1:43;
hence {} LTLB_WFF |- H₁(g) by A47, LTLAXIO1:43; :: thesis: verum

end;

end;

A80: S₁[ 0 ]

proof

let F be finite Subset of LTLB_WFF; :: thesis: ( card (tau F) = 0 implies for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds
{} LTLB_WFF |- H₁(f) )
assume card (tau F) = 0 ; :: thesis: for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds
{} LTLB_WFF |- H₁(f)
then A81: F = {} LTLB_WFF ;
let f be FinSequence of LTLB_WFF ; :: thesis: ( rng f = (comp F) ^ implies {} LTLB_WFF |- H₁(f) )
assume A82: rng f = (comp F) ^ ; :: thesis: {} LTLB_WFF |- H₁(f)
then A83: f /. 1 in rng f by FINSEQ_6:42, RELAT_1:38;
A84: 1 in dom f by A82, FINSEQ_3:32;
H₁(f) is ctaut

proof

let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . H₁(f) = 1
set v = VAL g;
(VAL g) . (f /. 1) = (VAL g) . (TVERUM '&&' TVERUM) by TARSKI:def 1, Th11, A82, Th12, A81, A83
.= ((VAL g) . TVERUM) '&' ((VAL g) . TVERUM) by LTLAXIO1:31
.= 1 by LTLAXIO2:4 ;
hence (VAL g) . H₁(f) = 1 by XBOOLEAN:def 3, LTLAXIO2:20, A84; :: thesis: verum

end;

then H₁(f) in LTL_axioms by LTLAXIO1:def 17;
hence {} LTLB_WFF |- H₁(f) by LTLAXIO1:42; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A80, A3);
hence {} LTLB_WFF |- H₁(f) by A2, A1; :: thesis: verum