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 of 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 of v

proof

now

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

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

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

end;

suppose A4: 0 < n ; :: thesis: H₁(n) is strict elementary LTLnode of 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 of v ; :: thesis: verum

end;

end;

end;

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

end;

then reconsider s1 = H₁(n) as strict elementary LTLnode of 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 of 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