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
for p being Instruction-Sequence 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_closed_on s,p & 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 Ig being good Program of
for p being Instruction-Sequence 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_closed_on s,p & for-up (a,bb,cc,Ig) is_halting_on s,p )
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of
for p being Instruction-Sequence 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_closed_on s,p & for-up (a,bb,cc,Ig) is_halting_on s,p )
let Ig be good Program of ; :: thesis: for p being Instruction-Sequence 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_closed_on s,p & for-up (a,bb,cc,Ig) is_halting_on s,p )
let p be Instruction-Sequence 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_closed_on s,p & 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_closed_on s,p & for-up (a,bb,cc,Ig) is_halting_on s,p )
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)),p,s);
set p1 = p;
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)),p,s),p & 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)),p,s),p ) 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)),p,s),p by SCMFSA9A:27;
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 ;
set MI = for-up (a,bb,cc,Ig);
A5: ( I03 is_closed_on Initialized s,p & I03 is_halting_on Initialized s,p ) by SCMFSA7B:18, SCMFSA7B:19;
then A6: for-up (a,bb,cc,Ig) is_closed_on Initialized s,p by A4, SFMASTR1:2;
hence for-up (a,bb,cc,Ig) is_closed_on s,p by A1, SFMASTR2:4; :: thesis: for-up (a,bb,cc,Ig) is_halting_on s,p
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)),p,s),p by A3, SCMFSA9A:27;
then for-up (a,bb,cc,Ig) is_halting_on Initialized s,p by A5, A4, SFMASTR1:3;
hence for-up (a,bb,cc,Ig) is_halting_on s,p by A1, A6, SFMASTR2:5; :: thesis: verum