let s be State of SCM+FSA; :: according to SCM_HALT:def 3 :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I ';' J c= p holds
for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A2: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I ';' J c= p holds
for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1
then A3: s +* (Initialize ((intloc 0) .--> 1)) = s by FUNCT_4:103, FUNCT_4:104;
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( I ';' J c= p implies for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A4: I ';' J c= p ; :: thesis: for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1
then A5: p +* (I ';' J) = p by FUNCT_4:103, FUNCT_4:104;
A6: Initialize ((intloc 0) .--> 1) c= s by A2;
A8: I c= p +* I by FUNCT_4:26;
A9: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;

per cases ( p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) or not p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) ) ;

suppose A10: p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) ; :: thesis: for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1

let k be Element of NAT ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1
A11: s +* (Initialize ((intloc 0) .--> 1)) = s +* (Initialize ((intloc 0) .--> 1))
.= s by A6, FUNCT_4:103, FUNCT_4:104 ;

per cases ( k <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) or k > LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ) ;

suppose A12: k <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1

A13: (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) . (intloc 0) = 1 by Def3, A8, A9;
NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) = NPP (Comput (p,s,k)) by A3, A10, A12, Th24, A5;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A13, SCMFSA10:92; :: thesis: verum

end;

suppose A14: k > LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1

set LS = LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))));
consider pp being Element of NAT such that
A15: k = (LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + pp and
A16: 1 <= pp by A14, FINSEQ_4:99;
consider r being Nat such that
A17: pp = 1 + r by A16, NAT_1:10;
reconsider r = r as Element of NAT by ORDINAL1:def 13;
set Rr = Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r);
set Sr = Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA);
A18: Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
J c= (p +* I) +* J by FUNCT_4:26;
then A19: (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) . (intloc 0) = 1 by Def3, A18;
( dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by FUNCOP_1:19, SCMFSA_2:81;
then not intloc 0 in dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
then A20: ((Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA))) . (intloc 0) = (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) . (intloc 0) by FUNCT_4:12;
NPP ((Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA))) = NPP (Comput ((p +* (I ';' J)),s,(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + r))) by A2, A10, A11, Th26, A4;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A15, A17, A19, A20, A5, SCMFSA10:92; :: thesis: verum

end;

end;

end;

suppose A21: not p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) ; :: thesis: for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1

let k be Element of NAT ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1
XX: NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) = NPP (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) by A21, Th27;
(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) . (intloc 0) = 1 by Def3, A8, A9;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A3, A5, XX, SCMFSA10:92; :: thesis: verum

end;

end;