let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_onInit s,P & I is_halting_onInit s,P & k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) & IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) )
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_onInit s,P & I is_halting_onInit s,P & k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) & IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) )
let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA
for k being Element of NAT st I is_closed_onInit s,P & I is_halting_onInit s,P & k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) & IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) )
set D = Data-Locations SCM+FSA;
let s be State of SCM+FSA; :: thesis: for k being Element of NAT st I is_closed_onInit s,P & I is_halting_onInit s,P & k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) & IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) )
let k be Element of NAT ; :: thesis: ( I is_closed_onInit s,P & I is_halting_onInit s,P & k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) & IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) implies ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) ) )
set s0 = Initialized s;
set sw = s +* (Initialize ((intloc 0) .--> 1));
set Pw = P +* (while>0 (a,I));
set sI = s +* (Initialize ((intloc 0) .--> 1));
set PI = P +* I;
set s0I = Initialize (Initialized s);
set s0w = (Initialized s) +* (Start-At (0,SCM+FSA));
set sK1 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k));
set sK2 = Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k);
set l3 = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k));
A1: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by SCMFSA8A:13;
assume I is_closed_onInit s,P ; :: thesis: ( not I is_halting_onInit s,P or not k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) or not IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 or not DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) or ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) ) )
then A3: I is_closed_on Initialized s,P by SCM_HALT:40;
assume I is_halting_onInit s,P ; :: thesis: ( not k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) or not IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 or not DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) or ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) ) )
then A4: I is_halting_on Initialized s,P by SCM_HALT:41;
assume A5: k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: ( not IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 or not DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) or ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) ) )
assume A6: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) + 4 ; :: thesis: ( not DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) or ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) ) )
assume A7: DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + k))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) )
hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + 4 by A5, A6, A3, A4, A1, SCMFSA_9:44; :: thesis: DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))
thus DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1))) by A5, A6, A7, A3, A4, A1, SCMFSA_9:44; :: thesis: verum