deffunc H₁( set , set ) -> strict elementary LTLnode of v = chosen_next ((Shift (w,(CastNat $1))),v,U,(CastNode ($2,v)));
deffunc H₂( Nat, set ) -> strict elementary LTLnode of v = chosen_next ((Shift (w,$1)),v,U,(CastNode ($2,v)));
set LS = LTLStates v;
A10: for f, g being Function of NAT,(LTLStates v) st f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) holds
f = g

proof

let f, g be Function of NAT,(LTLStates v); :: thesis: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) implies f = g )
assume that
A11: f . 0 = init v and
A12: for n being Nat holds f . (n + 1) = H₁(n,f . n) and
A13: g . 0 = init v and
A14: for n being Nat holds g . (n + 1) = H₁(n,g . n) ; :: thesis: f = g
defpred S₁[ Nat] means f . $1 = g . $1;
A15: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then f . (k + 1) = H₁(k,g . k) by A12
.= g . (k + 1) by A14 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A16: S₁[ 0 ] by A11, A13;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A16, A15);
then A17: for x being set 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 Function of NAT,(LTLStates v) st f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₂(n,g . n) ) holds
f = g

proof

let f, g be Function of NAT,(LTLStates v); :: thesis: ( f . 0 = init v & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) & g . 0 = init v & ( for n being Nat holds g . (n + 1) = H₂(n,g . n) ) implies f = g )
assume that
A18: f . 0 = init v and
A19: for n being Nat holds f . (n + 1) = H₂(n,f . n) and
A20: g . 0 = init v and
A21: for n being Nat holds g . (n + 1) = H₂(n,g . n) ; :: thesis: f = g
A22: for n being Nat holds g . (n + 1) = H₁(n,g . n)

proof

let n be Nat; :: thesis: g . (n + 1) = H₁(n,g . n)
g . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((g . n),v))) by A21;
hence g . (n + 1) = H₁(n,g . n) by MODELC_2:def 1; :: thesis: verum

end;

for n being Nat holds f . (n + 1) = H₁(n,f . n)

proof

let n be Nat; :: thesis: f . (n + 1) = H₁(n,f . n)
f . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((f . n),v))) by A19;
hence f . (n + 1) = H₁(n,f . n) by MODELC_2:def 1; :: thesis: verum

end;

hence f = g by A10, A18, A20, A22; :: thesis: verum

end;

hence for b₁, b₂ being sequence of (LTLStates v) st b₁ . 0 = init v & ( for n being Nat holds b₁ . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b₁ . n),v))) ) & b₂ . 0 = init v & ( for n being Nat holds b₂ . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b₂ . n),v))) ) holds
b₁ = b₂ ; :: thesis: verum