for i being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
for w being FinSequence of INT st Initialized ((fsloc 0) .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm