theorem Th19: :: SCMPDS_4:21

for n being Nat
for I being Program of
for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Nat st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Nat st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)