for N being with_zero set
for n being Nat
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for I being Program of
for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Nat st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Nat st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)