let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA
for k being Nat st I is_halting_onInit s,P & k < LifeSpan ((P +* I),(Initialized s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) )
let a be Int-Location; :: thesis: for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA
for k being Nat st I is_halting_onInit s,P & k < LifeSpan ((P +* I),(Initialized s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) )
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for s being State of SCM+FSA
for k being Nat st I is_halting_onInit s,P & k < LifeSpan ((P +* I),(Initialized s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) )
set D = Data-Locations ;
let s be State of SCM+FSA; :: thesis: for k being Nat st I is_halting_onInit s,P & k < LifeSpan ((P +* I),(Initialized s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) )
let k be Nat; :: thesis: ( I is_halting_onInit s,P & k < LifeSpan ((P +* I),(Initialized s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) ) )
set s0 = Initialized s;
set Pw = P +* (while>0 (a,I));
set PI = P +* I;
set s0I = Initialize (Initialized s);
set sK1 = Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k));
set sK2 = Comput ((P +* I),(Initialized s),k);
set l3 = IC (Comput ((P +* I),(Initialized s),k));
A1: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
assume I is_halting_onInit s,P ; :: thesis: ( not k < LifeSpan ((P +* I),(Initialized s)) or not IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 or not DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) or ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) ) )
then A2: I is_halting_on Initialized s,P by SCM_HALT:31;
assume A3: k < LifeSpan ((P +* I),(Initialized s)) ; :: thesis: ( not IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 or not DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) or ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) ) )
assume A4: IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 3 ; :: thesis: ( not DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) or ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) ) )
assume A5: DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) )
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 3 by A3, A4, A2, A1, SCMFSA_9:39; :: thesis: DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1)))
thus DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) by A3, A4, A5, A2, A1, SCMFSA_9:39; :: thesis: verum