let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: 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
let s1, s2 be State of SCM+FSA; :: thesis: 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
let a be read-write Int-Location; :: thesis: 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
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: ( DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1,p1 implies ProperBodyWhile>0 a,I,s2,p2 )
assume that
A1: DataPart s1 = DataPart s2 and
A2: ProperBodyWhile>0 a,I,s1,p1 ; :: thesis: ProperBodyWhile>0 a,I,s2,p2
let k be Nat; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (a,I,p2,s2)) . k) . a > 0 implies I is_halting_on (StepWhile>0 (a,I,p2,s2)) . k,p2 +* (while>0 (a,I)) )
assume A3: ((StepWhile>0 (a,I,p2,s2)) . k) . a > 0 ; :: thesis: I is_halting_on (StepWhile>0 (a,I,p2,s2)) . k,p2 +* (while>0 (a,I))
A4: DataPart ((StepWhile>0 (a,I,p2,s2)) . k) = DataPart ((StepWhile>0 (a,I,p1,s1)) . k) by A1, A2, Th34;
then ((StepWhile>0 (a,I,p1,s1)) . k) . a > 0 by A3, SCMFSA_M:2;
then I is_halting_on (StepWhile>0 (a,I,p1,s1)) . k,p1 +* (while>0 (a,I)) by A2;
hence I is_halting_on (StepWhile>0 (a,I,p2,s2)) . k,p2 +* (while>0 (a,I)) by A4, SCMFSA8B:5; :: thesis: verum