let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
for-up (a,bb,cc,Ig) is_halting_on s,p
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
for-up (a,bb,cc,Ig) is_halting_on s,p
let bb, cc be Int-Location; :: thesis: for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
for-up (a,bb,cc,Ig) is_halting_on s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
for-up (a,bb,cc,Ig) is_halting_on s,p
let Ig be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) implies for-up (a,bb,cc,Ig) is_halting_on s,p )
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) ; :: thesis: for-up (a,bb,cc,Ig) is_halting_on s,p
set i3 = a := bb;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig));
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc;
set i1 = SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb);
set i2 = AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0));
set IB = (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)));
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))));
set I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) ";" (a := bb);
set s1 = IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) ";" (a := bb)),p,s);
set p1 = p;
A3: ( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)),(Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))), IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) ";" (a := bb)),p,s),p & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)),(Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))), IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) ";" (a := bb)),p,s),p ) by A1, A2, Lm1;
reconsider I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) ";" (a := bb) as parahalting Program of ;
set MI = for-up (a,bb,cc,Ig);
A4: I03 is_halting_on Initialized s,p by SCMFSA7B:19;
while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))) is_halting_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) ";" (a := bb)),p,s),p by A3, SCMFSA9A:27;
then for-up (a,bb,cc,Ig) is_halting_on Initialized s,p by A4, SFMASTR1:3;
hence for-up (a,bb,cc,Ig) is_halting_on s,p by A1, SCMFSA8B:42; :: thesis: verum