deffunc H1( set , set ) -> strict elementary LTLnode over v = chosen_next ((Shift (w,(CastNat $1))),v,U,(CastNode ($2,v)));
set LS = LTLStates v;
( ex y being set ex f being Function st
( y = f . 0 & dom f = NAT & f . 0 = init v & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . 0 & dom f = NAT & f . 0 = init v & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) & ex f being Function st
( y2 = f . 0 & dom f = NAT & f . 0 = init v & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) holds
y1 = y2 ) ) from RECDEF_1:sch 12();
 then consider IT being Function such that
A1: dom IT = NAT and
A2: IT . 0 = init v and
A3: for n being Nat holds IT . (n + 1) = H1(n,IT . n) ;
A4: for n being Nat holds IT . (n + 1) = H1(n,IT . n) by A3;
A5: for n being Nat holds IT . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((IT . n),v)))
proof
let n be Nat; :: thesis: IT . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((IT . n),v)))
IT . (n + 1) = chosen_next ((Shift (w,(CastNat n))),v,U,(CastNode ((IT . n),v))) by A4;
hence IT . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((IT . n),v))) by MODELC_2:def 1; :: thesis: verum
end;
for x being object st x in NAT holds
IT . x in LTLStates v
proof
let x be object ; :: thesis: ( x in NAT implies IT . x in LTLStates v )
assume x in NAT ; :: thesis: IT . x in LTLStates v
then reconsider x = x as Nat ;
A6: ( x = 0 or 0 < 0 + x ) ;
now :: thesis: IT . x in LTLStates v
per cases ( x = 0 or 1 <= x ) by A6, NAT_1:19;
suppose A7: x = 0 ; :: thesis: IT . x in LTLStates v
set y = IT . x;
reconsider y = IT . x as Element of LTLNodes v by A2, A7, Def30;
IT . x = y ;
hence IT . x in LTLStates v by A2, A7; :: thesis: verum
end;
suppose A8: 1 <= x ; :: thesis: IT . x in LTLStates v
set x1 = x - 1;
reconsider x1 = x - 1 as Nat by A8, NAT_1:21;
set y = IT . x;
A9: IT . x = IT . (x1 + 1)
.= H1(x1,IT . x1) by A4 ;
then reconsider y = IT . x as Element of LTLNodes v by Def30;
IT . x = y ;
hence IT . x in LTLStates v by A9; :: thesis: verum
end;
end;
end;
hence IT . x in LTLStates v ; :: thesis: verum
end;
then reconsider IT = IT as sequence of (LTLStates v) by A1, FUNCT_2:3;
take IT ; :: thesis: ( IT . 0 = init v & ( for n being Nat holds IT . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((IT . n),v))) ) )
thus ( IT . 0 = init v & ( for n being Nat holds IT . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((IT . n),v))) ) ) by A2, A5; :: thesis: verum