theorem :: SCMFSA9A:38

for p1, p2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1,p1 holds
ProperBodyWhile>0 a,I,s2,p2