let w be Element of Inf_seq AtomicFamily; :: thesis: for v being neg-inner-most LTL-formula
for U being Choice_Function of (BOOL (Subformulae v)) st w |= v holds
for n being Nat holds
( CastNode (((chosen_run (w,v,U)) . (n + 1)),v) is_next_of CastNode (((chosen_run (w,v,U)) . n),v) & Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) )
let v be neg-inner-most LTL-formula; :: thesis: for U being Choice_Function of (BOOL (Subformulae v)) st w |= v holds
for n being Nat holds
( CastNode (((chosen_run (w,v,U)) . (n + 1)),v) is_next_of CastNode (((chosen_run (w,v,U)) . n),v) & Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) )
let U be Choice_Function of (BOOL (Subformulae v)); :: thesis: ( w |= v implies for n being Nat holds
( CastNode (((chosen_run (w,v,U)) . (n + 1)),v) is_next_of CastNode (((chosen_run (w,v,U)) . n),v) & Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) ) )
set s = init v;
deffunc H₁( Nat) -> strict LTLnode over v = CastNode (((chosen_run (w,v,U)) . $1),v);
defpred S₁[ Nat] means ( H₁($1 + 1) is_next_of H₁($1) & Shift (w,$1) |= * ('X' H₁($1)) );
assume w |= v ; :: thesis: for n being Nat holds
( CastNode (((chosen_run (w,v,U)) . (n + 1)),v) is_next_of CastNode (((chosen_run (w,v,U)) . n),v) & Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) )
then A1: w |= * ('X' (init v)) by Th72;
A2: CastNode (((chosen_run (w,v,U)) . 0),v) = CastNode ((init v),v) by Def50
.= init v by Def16 ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set s1 = H₁(n);
H₁(n) is strict elementary LTLnode over v

proof

now :: thesis: H₁(n) is strict elementary LTLnode over v

per cases ( n = 0 or 0 < n ) ;

suppose n = 0 ; :: thesis: H₁(n) is strict elementary LTLnode over v

then H₁(n) = CastNode ((init v),v) by Def50
.= init v by Def16 ;
hence H₁(n) is strict elementary LTLnode over v ; :: thesis: verum

end;

suppose A4: 0 < n ; :: thesis: H₁(n) is strict elementary LTLnode over v

set m = n - 1;
reconsider m = n - 1 as Nat by A4, NAT_1:20;
n = m + 1 ;
then H₁(n) = CastNode ((chosen_next ((Shift (w,m)),v,U,(CastNode (((chosen_run (w,v,U)) . m),v)))),v) by Def50
.= chosen_next ((Shift (w,m)),v,U,(CastNode (((chosen_run (w,v,U)) . m),v))) by Def16 ;
hence H₁(n) is strict elementary LTLnode over v ; :: thesis: verum

end;

end;

end;

hence H₁(n) is strict elementary LTLnode over v ; :: thesis: verum

end;

then reconsider s1 = H₁(n) as strict elementary LTLnode over v ;
set n1 = n + 1;
set w1 = Shift (w,n);
set w2 = Shift (w,(n + 1));
set s2 = H₁(n + 1);
set s3 = H₁((n + 1) + 1);
A5: H₁(n + 1) = CastNode ((chosen_next ((Shift (w,n)),v,U,(CastNode (((chosen_run (w,v,U)) . n),v)))),v) by Def50
.= chosen_next ((Shift (w,n)),v,U,s1) by Def16 ;
then reconsider s2 = H₁(n + 1) as strict elementary LTLnode over v ;
A6: H₁((n + 1) + 1) = CastNode ((chosen_next ((Shift (w,(n + 1))),v,U,(CastNode (((chosen_run (w,v,U)) . (n + 1)),v)))),v) by Def50
.= chosen_next ((Shift (w,(n + 1))),v,U,s2) by Def16 ;
assume S₁[n] ; :: thesis: S₁[n + 1]
then ( Shift (w,(n + 1)) = Shift ((Shift (w,n)),1) & Shift (w,n) |= * (chosen_next ((Shift (w,n)),v,U,s1)) ) by Th69, MODELC_2:80;
then Shift (w,(n + 1)) |= * ('X' s2) by A5, Th70;
hence S₁[n + 1] by A6, Th69; :: thesis: verum

end;

H₁(0 + 1) = CastNode ((chosen_next ((Shift (w,0)),v,U,(CastNode (((chosen_run (w,v,U)) . 0),v)))),v) by Def50
.= CastNode ((chosen_next (w,v,U,(init v))),v) by A2, MODELC_2:79
.= chosen_next (w,v,U,(init v)) by Def16 ;
then A7: S₁[ 0 ] by A1, A2, Th69, MODELC_2:79;
for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A3);
hence for n being Nat holds
( CastNode (((chosen_run (w,v,U)) . (n + 1)),v) is_next_of CastNode (((chosen_run (w,v,U)) . n),v) & Shift (w,n) |= * ('X' (CastNode (((chosen_run (w,v,U)) . n),v))) ) ; :: thesis: verum