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 SCM+FSA 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 SCM+FSA 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 SCM+FSA 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 SCM+FSA ; :: 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 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 i3 = a := bb;
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 MI = for-up a,bb,cc,Ig;
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;
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 SCM+FSA ;
A3: I03 is_closed_on Initialize s by SCMFSA7B:24;
A4: I03 is_halting_on Initialize s by SCMFSA7B:25;
A5: 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 by A1, A2, Lm1;
A6: 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 A7: 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 A5, SCMFSA9A:33;
A8: 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 A5, A6, SCMFSA9A:33;
A9: for-up a,bb,cc,Ig is_closed_on Initialize s by A3, A4, A7, 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
for-up a,bb,cc,Ig is_halting_on Initialize s by A3, A4, A7, A8, SFMASTR1:4;
hence for-up a,bb,cc,Ig is_halting_on s by A1, A9, SFMASTR2:5; :: thesis: verum