:: deftheorem defines -dl.constant AMI_8:def 3 :
for n being Nat
for I being Instruction of SCM holds
( I is n -dl.constant iff for P being Instruction-Sequence of SCM
for s being State of SCM
for k being Nat st CurInstr (P,(Comput (P,s,k))) = I holds
(Comput (P,s,(k + 1))) . (dl. n) = (Comput (P,s,k)) . (dl. n) );