set D = Data-Locations SCM+FSA;
set JAt = Initialized J;
let s be State of SCM+FSA; :: according to SCM_HALT:def 2 :: 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
P halts_on s )
assume A1: 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
P halts_on s
then A2: s = s +* (Initialize ((intloc 0) .--> 1)) 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 p halts_on s )
assume A3: I ';' J c= p ; :: thesis: p halts_on s
A4: p = p +* (I ';' J) by A3, FUNCT_4:103, FUNCT_4:104;
set p1 = p +* I;
set s3 = (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1));
set p3 = (p +* I) +* J;
A7: J c= (p +* I) +* J by FUNCT_4:26;
set m1 = LifeSpan ((p +* I),s);
set s4 = Comput (p,s,((LifeSpan ((p +* I),s)) + 1));
A8: I c= p +* I by FUNCT_4:26;
A9: Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))));
A11: dom (DataPart (Initialize ((intloc 0) .--> 1))) = (dom (Initialize ((intloc 0) .--> 1))) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
reconsider m = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))) as Element of NAT ;
A15: Initialize ((intloc 0) .--> 1) c= s by A1;
then B15: s +* (Initialize ((intloc 0) .--> 1)) = s by FUNCT_4:103, FUNCT_4:104;
A17: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
I c= p +* I by FUNCT_4:26;
then A18: p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th5, A17;

A19: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialize ((intloc 0) .--> 1))) implies (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . b₁ = (DataPart (Initialize ((intloc 0) .--> 1))) . b₁ )
DataPart (Initialize ((intloc 0) .--> 1)) c= Initialize ((intloc 0) .--> 1) by RELAT_1:88;
then AA: dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (Initialize ((intloc 0) .--> 1)) by RELAT_1:25;
assume ZZ: x in dom (DataPart (Initialize ((intloc 0) .--> 1))) ; :: thesis: (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . b₁ = (DataPart (Initialize ((intloc 0) .--> 1))) . b₁
then x in dom (Initialize ((intloc 0) .--> 1)) by AA;
then pc: x in {(intloc 0),(IC )} by diS, ENUMSET1:41;

per cases ( x = intloc 0 or x = IC ) by pc, TARSKI:def 2;

suppose A24: x = intloc 0 ; :: thesis: (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . b₁ = (DataPart (Initialize ((intloc 0) .--> 1))) . b₁

then x in Int-Locations by SCMFSA_2:9;
then A25: x in Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_0:def 3;
hence (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . x = (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) . x by FUNCT_1:72
.= 1 by B15, A24, Def3, A17, A8
.= (DataPart (Initialize ((intloc 0) .--> 1))) . x by A25, A24, iSint, FUNCT_1:72 ;
:: thesis: verum

end;

suppose S: x = IC ; :: thesis: (DataPart (Initialize ((intloc 0) .--> 1))) . b₁ = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . b₁

dom (DataPart (Initialize ((intloc 0) .--> 1))) c= Data-Locations SCM+FSA by RELAT_1:87;
then x in Data-Locations SCM+FSA by ZZ;
hence (DataPart (Initialize ((intloc 0) .--> 1))) . x = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . x by S, SCMFSA6A:37; :: thesis: verum

end;

end;

end;

take m ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (p,s,m)) in proj1 p & CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA )
IC (Comput (p,s,m)) in NAT ;
hence IC (Comput (p,s,m)) in dom p by PARTFUN1:def 4; :: thesis: CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA
Directed I c= I ';' J by SCMFSA6A:55;
then A27: Directed I c= p by A3, XBOOLE_1:1;
Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then dom (Initialize ((intloc 0) .--> 1)) c= dom ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by GRFUNC_1:8;
then dom (Initialize ((intloc 0) .--> 1)) c= the carrier of SCM+FSA by PARTFUN1:def 4;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= the carrier of SCM+FSA /\ (Data-Locations SCM+FSA) by A11, XBOOLE_1:26;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= (dom (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) /\ (Data-Locations SCM+FSA) by PARTFUN1:def 4;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by RELAT_1:90;
then DataPart (Initialize ((intloc 0) .--> 1)) c= DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A19, GRFUNC_1:8;
then A30: DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:104
.= DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:75 ;
NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),s)))) = NPP (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),s)))) by A18, Th24, B15;
then NPP (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = NPP (Comput (p,s,(LifeSpan ((p +* I),s)))) by A2, A4;
then A31: DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A30, COMPOS_1:138;
I c= p +* I by FUNCT_4:26;
then YY: p +* I halts_on s by A1, Th5;
then A33: DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A15, Th22, A31, A27;
A35: Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))))) by EXTPRO_1:5;
A36: Reloc (J,(card I)) c= p by A9, A3, XBOOLE_1:1;
X: Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
x: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I by YY, A27, Th21, A1;
for i being Element of NAT holds IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),i)))),(card I)) = CurInstr (p,(Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),i))) by X, A7, A36, Th12, x, A33;
then A37: IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))))),(card I)) = CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))))) by A35;
(p +* I) +* J halts_on (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by A7, Def2, X;
then CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A37, EXTPRO_1:def 14
.= halt SCM+FSA by COMPOS_1:93 ;
hence CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA ; :: thesis: verum