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 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 SCM+FSA ;
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