let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
( for-up (a,bb,cc,Ig) is_closed_on s & for-up (a,bb,cc,Ig) is_halting_on s )
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
( for-up (a,bb,cc,Ig) is_closed_on s & for-up (a,bb,cc,Ig) is_halting_on s )
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
( for-up (a,bb,cc,Ig) is_closed_on s & for-up (a,bb,cc,Ig) is_halting_on s )
let Ig be good Program of {INT,(INT *)}; :: thesis: ( s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) implies ( for-up (a,bb,cc,Ig) is_closed_on s & for-up (a,bb,cc,Ig) is_halting_on s ) )
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) ; :: thesis: ( for-up (a,bb,cc,Ig) is_closed_on s & for-up (a,bb,cc,Ig) is_halting_on s )
set i3 = a := bb;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc;
set i1 = SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb);
set i2 = AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0));
set IB = (Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)));
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))));
set I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb);
set s1 = IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s);
A3: ( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)),(Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))), IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)),(Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))), IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) ) by A1, A2, Lm1;
then A4: while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))) is_closed_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) by SCMFSA9A:33;
reconsider I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb) as parahalting Program of {INT,(INT *)} ;
set MI = for-up (a,bb,cc,Ig);
A5: ( I03 is_closed_on Initialized s & I03 is_halting_on Initialized s ) by SCMFSA7B:24, SCMFSA7B:25;
then A6: for-up (a,bb,cc,Ig) is_closed_on Initialized s by A4, SFMASTR1:3;
hence for-up (a,bb,cc,Ig) is_closed_on s by A1, SFMASTR2:4; :: thesis: for-up (a,bb,cc,Ig) is_halting_on s
while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))) is_halting_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) by A3, SCMFSA9A:33;
then for-up (a,bb,cc,Ig) is_halting_on Initialized s by A5, A4, SFMASTR1:4;
hence for-up (a,bb,cc,Ig) is_halting_on s by A1, A6, SFMASTR2:5; :: thesis: verum