let f be FinSequence of LTLB_WFF ; :: thesis: {} LTLB_WFF |- ((con (nex f)) /. (len (con (nex f)))) => ('X' ((con f) /. (len (con f))))
set t = TVERUM ;

per cases ( len f = 0 or 0 < len f ) ;

suppose A1: len f = 0 ; :: thesis: {} LTLB_WFF |- ((con (nex f)) /. (len (con (nex f)))) => ('X' ((con f) /. (len (con f))))

then len (nex f) = 0 by Def5;
then A2: nex f = {} ;
TVERUM is ctaut by Th4;
then TVERUM in LTL_axioms by LTLAXIO1:def 17;
then A3: {} LTLB_WFF |- TVERUM by LTLAXIO1:42;
then A4: {} LTLB_WFF |- 'X' TVERUM by LTLAXIO1:44;
TVERUM => (('X' TVERUM) => (TVERUM => ('X' TVERUM))) is ctaut by Th34;
then TVERUM => (('X' TVERUM) => (TVERUM => ('X' TVERUM))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- TVERUM => (('X' TVERUM) => (TVERUM => ('X' TVERUM))) by LTLAXIO1:42;
then A5: {} LTLB_WFF |- ('X' TVERUM) => (TVERUM => ('X' TVERUM)) by LTLAXIO1:43, A3;
f = {} by A1;
hence {} LTLB_WFF |- ((con (nex f)) /. (len (con (nex f)))) => ('X' ((con f) /. (len (con f)))) by A5, LTLAXIO1:43, A4, Th10, A2; :: thesis: verum

end;

suppose A6: 0 < len f ; :: thesis: {} LTLB_WFF |- ((con (nex f)) /. (len (con (nex f)))) => ('X' ((con f) /. (len (con f))))

defpred S₁[ Nat] means ( $1 <= len f implies {} LTLB_WFF |- ((con (nex f)) /. $1) => ('X' ((con f) /. $1)) );

A7: 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] )
set p = (con (nex f)) /. k;
set q = (con (nex f)) /. (k + 1);
set r = (nex f) /. (k + 1);
set s = (con f) /. (k + 1);
set t = (con f) /. k;
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

(((con (nex f)) /. (k + 1)) => (((con (nex f)) /. k) '&&' ((nex f) /. (k + 1)))) => ((((con (nex f)) /. k) => ('X' ((con f) /. k))) => (((con (nex f)) /. (k + 1)) => (('X' ((con f) /. k)) '&&' ((nex f) /. (k + 1))))) is ctaut by Th44;
then (((con (nex f)) /. (k + 1)) => (((con (nex f)) /. k) '&&' ((nex f) /. (k + 1)))) => ((((con (nex f)) /. k) => ('X' ((con f) /. k))) => (((con (nex f)) /. (k + 1)) => (('X' ((con f) /. k)) '&&' ((nex f) /. (k + 1))))) in LTL_axioms by LTLAXIO1:def 17;
then A9: {} LTLB_WFF |- (((con (nex f)) /. (k + 1)) => (((con (nex f)) /. k) '&&' ((nex f) /. (k + 1)))) => ((((con (nex f)) /. k) => ('X' ((con f) /. k))) => (((con (nex f)) /. (k + 1)) => (('X' ((con f) /. k)) '&&' ((nex f) /. (k + 1))))) by LTLAXIO1:42;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
A10: 1 <= k1 by NAT_1:25;
assume A11: k + 1 <= len f ; :: thesis: {} LTLB_WFF |- ((con (nex f)) /. (k + 1)) => ('X' ((con f) /. (k + 1)))
then A12: k1 + 1 <= len (con f) by Def2;
A13: k1 + 1 <= len (nex f) by A11, Def5;
then (nex f) /. (k + 1) = (nex f) . (k1 + 1) by NAT_1:12, FINSEQ_4:15
.= 'X' (f /. (k + 1)) by Def5, NAT_1:12, A11 ;
then A14: {} LTLB_WFF |- (('X' ((con f) /. k)) '&&' ((nex f) /. (k + 1))) => ('X' (((con f) /. k) '&&' (f /. (k + 1)))) by LTLAXIO1:53;
A15: k < len f by A11, NAT_1:13;
then A16: k1 < len (nex f) by Def5;
k1 + 1 <= len (con (nex f)) by A13, Def2;
then (con (nex f)) /. (k + 1) = (con (nex f)) . (k1 + 1) by NAT_1:12, FINSEQ_4:15
.= ((con (nex f)) /. k) '&&' ((nex f) /. (k + 1)) by Def2, A16, A10 ;
then ((con (nex f)) /. (k + 1)) => (((con (nex f)) /. k) '&&' ((nex f) /. (k + 1))) is ctaut by Th24;
then ((con (nex f)) /. (k + 1)) => (((con (nex f)) /. k) '&&' ((nex f) /. (k + 1))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- ((con (nex f)) /. (k + 1)) => (((con (nex f)) /. k) '&&' ((nex f) /. (k + 1))) by LTLAXIO1:42;
then {} LTLB_WFF |- (((con (nex f)) /. k) => ('X' ((con f) /. k))) => (((con (nex f)) /. (k + 1)) => (('X' ((con f) /. k)) '&&' ((nex f) /. (k + 1)))) by A9, LTLAXIO1:43;
then A17: {} LTLB_WFF |- ((con (nex f)) /. (k + 1)) => (('X' ((con f) /. k)) '&&' ((nex f) /. (k + 1))) by LTLAXIO1:43, A11, NAT_1:13, A8;
((con f) /. k) '&&' (f /. (k + 1)) = (con f) . (k1 + 1) by Def2, A10, A15
.= (con f) /. (k + 1) by NAT_1:12, A12, FINSEQ_4:15 ;
hence {} LTLB_WFF |- ((con (nex f)) /. (k + 1)) => ('X' ((con f) /. (k + 1))) by A14, A17, LTLAXIO1:47; :: thesis: verum

end;

end;

A18: 0 < len (nex f) by A6, Def5;
A19: S₁[1]

proof

assume A20: 1 <= len f ; :: thesis: {} LTLB_WFF |- ((con (nex f)) /. 1) => ('X' ((con f) /. 1))
then 1 <= len (nex f) by Def5;
then 1 <= len (con (nex f)) by Def2;
then A21: (con (nex f)) /. 1 = (con (nex f)) . 1 by FINSEQ_4:15
.= (nex f) . 1 by Def2, A18
.= 'X' (f /. 1) by Def5, A20 ;
('X' (f /. 1)) => ('X' (f /. 1)) is ctaut by Th24;
then A22: ('X' (f /. 1)) => ('X' (f /. 1)) in LTL_axioms by LTLAXIO1:def 17;
'X' ((con f) /. 1) = 'X' (f /. 1) by Th6, A20;
hence {} LTLB_WFF |- ((con (nex f)) /. 1) => ('X' ((con f) /. 1)) by A22, LTLAXIO1:42, A21; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A19, A7);
then A23: {} LTLB_WFF |- ((con (nex f)) /. (len f)) => ('X' ((con f) /. (len f))) by A6;
A24: len (nex f) > 0 by A6, Def5;
len f = len (nex f) by Def5
.= len (con (nex f)) by Def2, A24 ;
hence {} LTLB_WFF |- ((con (nex f)) /. (len (con (nex f)))) => ('X' ((con f) /. (len (con f)))) by Def2, A6, A23; :: thesis: verum

end;

end;