let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let bb, cc be Int-Location; :: thesis: for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let k be Nat; :: thesis: for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let p be Instruction-Sequence of SCM+FSA; :: thesis: for Ig being really-closed good MacroInstruction of SCM+FSA st ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
let Ig be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 & Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) implies ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1 )
set I = Ig;
assume that
A1: ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (intloc 0) = 1 and
A2: Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) ; :: thesis: ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) . (intloc 0) = 1
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig));
set IB = (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)));
set SW2 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))));
A3: (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))) = Ig ";" ((AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) by SCMFSA6A:28;