theorem :: SF_MASTR:65

for I being Program of
for n being Nat
for s, t being State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) holds
( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )