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 H1( Nat) -> strict LTLnode over v = CastNode (((chosen_run (w,v,U)) . $1),v);
defpred S1[ Nat] means ( H1($1 + 1) is_next_of H1($1) & Shift (w,$1) |= * ('X' H1($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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set s1 = H1(n);
H1(n) is strict elementary LTLnode over v
proof
now :: thesis: H1(n) is strict elementary LTLnode over v
per cases ( n = 0 or 0 < n ) ;
suppose n = 0 ; :: thesis: H1(n) is strict elementary LTLnode over v
then H1(n) = CastNode ((init v),v) by Def50
.= init v by Def16 ;
hence H1(n) is strict elementary LTLnode over v ; :: thesis: verum
end;
suppose A4: 0 < n ; :: thesis: H1(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 H1(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 H1(n) is strict elementary LTLnode over v ; :: thesis: verum
end;
end;
end;
hence H1(n) is strict elementary LTLnode over v ; :: thesis: verum
end;
then reconsider s1 = H1(n) as strict elementary LTLnode over v ;
set n1 = n + 1;
set w1 = Shift (w,n);
set w2 = Shift (w,(n + 1));
set s2 = H1(n + 1);
set s3 = H1((n + 1) + 1);
A5: H1(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 = H1(n + 1) as strict elementary LTLnode over v ;
A6: H1((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 S1[n] ; :: thesis: S1[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 S1[n + 1] by A6, Th69; :: thesis: verum
end;
H1(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: S1[ 0 ] by A1, A2, Th69, MODELC_2:79;
for n being Nat holds S1[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