let M be LTLModel; :: thesis: for n being Element of NAT
for f being FinSequence of LTLB_WFF holds
( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )
let n be Element of NAT ; :: thesis: for f being FinSequence of LTLB_WFF holds
( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )
let f be FinSequence of LTLB_WFF ; :: thesis: ( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )
set s = SAT M;
defpred S₁[ Nat] means for f being FinSequence of LTLB_WFF st len f = $1 holds
( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 );

A1: 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 A2: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let f be FinSequence of LTLB_WFF ; :: thesis: ( len f = k + 1 implies ( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ) )
A3: 1 <= k + 1 by NAT_1:11;
set fk = f | k;
assume A4: len f = k + 1 ; :: thesis: ( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )
A5: dom (f | k) c= dom f by RELAT_1:60;

per cases ( k > 0 or k = 0 ) ;

suppose A6: k > 0 ; :: thesis: ( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )

then A7: 1 <= k by NAT_1:25;
A8: H₂(f) = (con f) /. (k + 1) by LTLAXIO2:def 2, A4
.= ((con f) /. k) '&&' (f /. (k + 1)) by LTLAXIO2:7, A7, NAT_1:16, A4 ;
A9: k < len f by NAT_1:16, A4;
then A10: len (f | k) = k by FINSEQ_1:59;
A11: (con f) /. k = (con (f | k)) /. k by A7, A9, LTLAXIO2:13
.= H₂(f | k) by A10, LTLAXIO2:def 2, A6 ;

hereby :: thesis: ( ( for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ) implies (SAT M) . [n,H₂(f)] = 1 )

assume A12: (SAT M) . [n,H₂(f)] = 1 ; :: thesis: for i being Nat st i in dom f holds
(SAT M) . [n,(f /. b₂)] = 1
then A13: (SAT M) . [n,H₂(f | k)] = 1 by A8, LTLAXIO1:7, A11;
let i be Nat; :: thesis: ( i in dom f implies (SAT M) . [n,(f /. b₁)] = 1 )
assume A14: i in dom f ; :: thesis: (SAT M) . [n,(f /. b₁)] = 1
then A15: 1 <= i by FINSEQ_3:25;
A16: i <= len f by A14, FINSEQ_3:25;

per cases ( i < len f or i = len f ) by A16, XXREAL_0:1;

suppose i < len f ; :: thesis: (SAT M) . [n,(f /. b₁)] = 1

then i <= k by A4, NAT_1:13;
then A17: i in dom (f | k) by A10, FINSEQ_3:25, A15;
then (SAT M) . [n,((f | k) /. i)] = 1 by A2, A10, A13;
hence (SAT M) . [n,(f /. i)] = 1 by FINSEQ_4:70, A17; :: thesis: verum

end;

suppose i = len f ; :: thesis: (SAT M) . [n,(f /. b₁)] = 1

hence (SAT M) . [n,(f /. i)] = 1 by A4, A12, A8, LTLAXIO1:7; :: thesis: verum

end;

end;

end;

assume A18: for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ; :: thesis: (SAT M) . [n,H₂(f)] = 1

now :: thesis: for i being Nat st i in dom (f | k) holds
(SAT M) . [n,((f | k) /. i)] = 1

let i be Nat; :: thesis: ( i in dom (f | k) implies (SAT M) . [n,((f | k) /. i)] = 1 )
assume A19: i in dom (f | k) ; :: thesis: (SAT M) . [n,((f | k) /. i)] = 1
then (SAT M) . [n,(f /. i)] = 1 by A5, A18;
hence (SAT M) . [n,((f | k) /. i)] = 1 by FINSEQ_4:70, A19; :: thesis: verum

end;

then A20: (SAT M) . [n,((con f) /. k)] = 1 by A2, A10, A11;
(SAT M) . [n,(f /. (k + 1))] = 1 by A18, FINSEQ_3:25, A4, A3;
hence (SAT M) . [n,H₂(f)] = 1 by LTLAXIO1:7, A20, A8; :: thesis: verum

end;

suppose A21: k = 0 ; :: thesis: ( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )

then A22: H₂(f) = (con f) /. 1 by A4, LTLAXIO2:def 2
.= f /. 1 by LTLAXIO2:6, A4 ;

hereby :: thesis: ( ( for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ) implies (SAT M) . [n,H₂(f)] = 1 )

assume A23: (SAT M) . [n,H₂(f)] = 1 ; :: thesis: for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1
let i be Nat; :: thesis: ( i in dom f implies (SAT M) . [n,(f /. i)] = 1 )
assume i in dom f ; :: thesis: (SAT M) . [n,(f /. i)] = 1
then ( 1 <= i & i <= len f ) by FINSEQ_3:25;
hence (SAT M) . [n,(f /. i)] = 1 by NAT_1:25, A21, A4, A23, A22; :: thesis: verum

end;

assume for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ; :: thesis: (SAT M) . [n,H₂(f)] = 1
hence (SAT M) . [n,H₂(f)] = 1 by A21, A4, FINSEQ_3:25, A22; :: thesis: verum

end;

end;

end;

end;

A24: S₁[ 0 ]

proof

let f be FinSequence of LTLB_WFF ; :: thesis: ( len f = 0 implies ( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ) )
assume len f = 0 ; :: thesis: ( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )
then f = {} ;
hence ( (SAT M) . [n,H₂(f)] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ) by LTLAXIO1:6, LTLAXIO2:10; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A24, A1);
then S₁[ len f] ;
hence ( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 ) ; :: thesis: verum