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 & I is_halting_onInit s & k < LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) & IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) holds
( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(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 & I is_halting_onInit s & k < LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) & IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) holds
( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) )
set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for k being Element of NAT st I is_closed_onInit s & I is_halting_onInit s & k < LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) & IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) holds
( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) )
let k be Element of NAT ; :: thesis: ( I is_closed_onInit s & I is_halting_onInit s & k < LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) & IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) implies ( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) ) )
set s0 = Initialized s;
set sw = s +* (Initialized (while>0 a,I));
set sI = s +* (Initialized I);
set s0I = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ));
set s0w = (Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ));
set sK1 = Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k);
set sK2 = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k;
set l3 = IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k);
A1: s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
A2: s +* (Initialized (while>0 a,I)) = (Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
assume I is_closed_onInit s ; :: thesis: ( not I is_halting_onInit s or not k < LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) or not IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 or not DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) or ( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) ) )
then A3: I is_closed_on Initialized s by SCM_HALT:40;
assume I is_halting_onInit s ; :: thesis: ( not k < LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) or not IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 or not DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) or ( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) ) )
then A4: I is_halting_on Initialized s by SCM_HALT:41;
assume A5: k < LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)) ; :: thesis: ( not IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 or not DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) or ( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) ) )
assume A6: IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) + 4 ; :: thesis: ( not DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) or ( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) ) )
assume A7: DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) ; :: thesis: ( IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) )
hence IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))) + 4 by A5, A6, A3, A4, A1, A2, SCMFSA_9:44; :: thesis: DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1))
thus DataPart (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(k + 1)) by A5, A6, A7, A3, A4, A1, A2, SCMFSA_9:44; :: thesis: verum