let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let bb, cc be Int-Location; :: thesis: for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let k be Nat; :: thesis: for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let p be Instruction-Sequence of SCM+FSA; :: thesis: for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let Ig be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) implies DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k) )
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: k = ((s . cc) - (s . bb)) + 1 and
A3: ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) ; :: thesis: DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
set scb1 = ((s . cc) - (s . bb)) + 1;
set SF = StepForUp (a,bb,cc,Ig,p,s);
A4: ProperForUpBody a,bb,cc,Ig,s,p by A3, Th15;
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));
reconsider IB = (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))) as really-closed MacroInstruction of SCM+FSA ;
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;
A5: (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)) . (intloc 0) = (Exec ((a := bb),(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)))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (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)))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((AddTo ((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))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb))),p,s)) . (intloc 0) by SCMFSA_2:64
.= (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),bb)),(Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) := cc),(Initialized s))) . (intloc 0) by SCMFSA_2:65
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA_M:9 ;
then A6: DataPart (Initialized (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))) = DataPart (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)) by SCMFSA_M:19;
set Ex1 = ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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 SW1 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))));
A7: ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)),IB, 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, A3, Lm1;
then A8: ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)),IB, Initialized (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 A6, SCMFSA9A:38;
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
set p2 = p;
set SW2 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))));
A9: DataPart (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)) = DataPart ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) by A1, Th14;
then DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) by A6, A8, SCMFSA9A:34;
then A10: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) = ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) by SCMFSA_M:2;
A11: WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)),IB, 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, A3, Lm1;
then A12: WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)),IB, Initialized (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 A5, A6, A7, SCMFSA9A:41;
consider K being Nat such that
A13: ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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)))) = K and
A14: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . K) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) <= 0 and
A15: ( ( for i being Nat st ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . i) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) <= 0 holds
K <= i ) & DataPart (Comput ((p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB))),(Initialize (Initialized (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)))),(LifeSpan ((p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB))),(Initialize (Initialized (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)))))))) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . K) ) by A12, A8, SCMFSA9A:def 6;
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . K) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . K) by A6, A8, A9, SCMFSA9A:34;
then A16: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . K) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) = ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . K) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) by SCMFSA_M:2;

A17: now :: thesis: not K < ((s . cc) - (s . bb)) + 1

assume A18: K < ((s . cc) - (s . bb)) + 1 ; :: thesis: contradiction
then (((StepForUp (a,bb,cc,Ig,p,s)) . K) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + K < 0 + (((s . cc) - (s . bb)) + 1) by A14, A16, XREAL_1:8;
hence contradiction by A1, A4, A18, Th17; :: thesis: verum

end;

(((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 by A1, A2, A4, Th17;
then K <= k by A2, A15, A10;
then A19: ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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)))) = k by A2, A13, A17, XXREAL_0:1;
set MI = for-up (a,bb,cc,Ig);
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB);
while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB) 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 A7, A11, SCMFSA9A:27;
hence DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart (IExec ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB)),p,(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)))) by SFMASTR1:9
.= DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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))))) . (ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),IB,p,(Initialized (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)))))) by A8, A12, SCMFSA9A:36
.= DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k) by A6, A8, A9, A19, SCMFSA9A:34 ;
:: thesis: verum