theorem :: EXTPRO_1:20

for i, j being Nat
for N being non empty with_zero set st i <= j holds
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b₄ -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
Comput (P,s,j) = Comput (P,s,i)