deffunc H1( set , set ) -> strict elementary LTLnode over v = chosen_next ((Shift (w,(CastNat $1))),v,U,(CastNode ($2,v)));
deffunc H2( Nat, set ) -> strict elementary LTLnode over v = chosen_next ((Shift (w,$1)),v,U,(CastNode ($2,v)));
set LS = LTLStates v;
A10: for f, g being sequence of (LTLStates v) st f . 0 = init v & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) holds
f = g
proof
let f, g be sequence of (LTLStates v); :: thesis: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) implies f = g )
assume that
A11: f . 0 = init v and
A12: for n being Nat holds f . (n + 1) = H1(n,f . n) and
A13: g . 0 = init v and
A14: for n being Nat holds g . (n + 1) = H1(n,g . n) ; :: thesis: f = g
defpred S1[ Nat] means f . $1 = g . $1;
A15: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then f . (k + 1) = H1(k,g . k) by A12
.= g . (k + 1) by A14 ;
hence S1[k + 1] ; :: thesis: verum
end;
A16: S1[ 0 ] by A11, A13;
for k being Nat holds S1[k] from NAT_1:sch 2(A16, A15);
 then A17: for x being object st x in dom f holds
f . x = g . x ;
( dom f = NAT & dom g = NAT ) by FUNCT_2:def 1;
hence f = g by A17, FUNCT_1:2; :: thesis: verum
end;
for f, g being sequence of (LTLStates v) st f . 0 = init v & ( for n being Nat holds f . (n + 1) = H2(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H2(n,g . n) ) holds
f = g
proof
let f, g be sequence of (LTLStates v); :: thesis: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H2(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H2(n,g . n) ) implies f = g )
assume that
A18: f . 0 = init v and
A19: for n being Nat holds f . (n + 1) = H2(n,f . n) and
A20: g . 0 = init v and
A21: for n being Nat holds g . (n + 1) = H2(n,g . n) ; :: thesis: f = g
A22: for n being Nat holds g . (n + 1) = H1(n,g . n)
proof
let n be Nat; :: thesis: g . (n + 1) = H1(n,g . n)
g . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((g . n),v))) by A21;
hence g . (n + 1) = H1(n,g . n) by MODELC_2:def 1; :: thesis: verum
end;
for n being Nat holds f . (n + 1) = H1(n,f . n)
proof
let n be Nat; :: thesis: f . (n + 1) = H1(n,f . n)
f . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((f . n),v))) by A19;
hence f . (n + 1) = H1(n,f . n) by MODELC_2:def 1; :: thesis: verum
end;
hence f = g by A10, A18, A20, A22; :: thesis: verum
end;
hence for b1, b2 being sequence of (LTLStates v) st b1 . 0 = init v & ( for n being Nat holds b1 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b1 . n),v))) ) & b2 . 0 = init v & ( for n being Nat holds b2 . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b2 . n),v))) ) holds
b1 = b2 ; :: thesis: verum