set D = Data-Locations SCM+FSA;
let s be State of SCM+FSA; :: according to SCMFSA6B:def 3 :: thesis: ( Start-At (0,SCM+FSA) 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: Start-At (0,SCM+FSA) 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 +* (Start-At (0,SCM+FSA)) by 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
set JAt = Start-At (0,SCM+FSA);
set s3 = (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA));
set m1 = LifeSpan ((P +* I),s);
set m3 = LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))));
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;

A5: now

let x be set ; :: thesis: ( x in dom (DataPart (Start-At (0,SCM+FSA))) implies kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x )
assume x in dom (DataPart (Start-At (0,SCM+FSA))) ; :: thesis: kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x
then A6: x in (dom (Start-At (0,SCM+FSA))) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
x in dom (Start-At (0,SCM+FSA)) by A6, XBOOLE_0:def 4;
then x in {(IC )} by FUNCOP_1:19;
then x = IC by TARSKI:def 1;
hence kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A6, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

Start-At (0,SCM+FSA) c= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
then dom (Start-At (0,SCM+FSA)) c= dom ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
then A10: dom (Start-At (0,SCM+FSA)) c= the carrier of SCM+FSA by PARTFUN1:def 4;
dom (DataPart (Start-At (0,SCM+FSA))) = (dom (Start-At (0,SCM+FSA))) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then dom (DataPart (Start-At (0,SCM+FSA))) c= the carrier of SCM+FSA /\ (Data-Locations SCM+FSA) by A10, XBOOLE_1:26;
then dom (DataPart (Start-At (0,SCM+FSA))) c= (dom (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) /\ (Data-Locations SCM+FSA) by PARTFUN1:def 4;
then dom (DataPart (Start-At (0,SCM+FSA))) c= dom (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by RELAT_1:90;
then ( ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))) | (Data-Locations SCM+FSA) = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) +* kk & DataPart (Start-At (0,SCM+FSA)) c= DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) ) by A5, FUNCT_4:75, GRFUNC_1:8;
then A11: DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))) by FUNCT_4:104;
reconsider m = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))))) as Element of NAT ;
A13: Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
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 )
set s4 = Comput (P,s,((LifeSpan ((P +* I),s)) + 1));
Directed I c= I ';' J by SCMFSA6A:55;
then A19: Directed I c= P by A3, XBOOLE_1:1;
Y2: s +* (Start-At (0,SCM+FSA)) = s by A1, FUNCT_4:104;
Start-At (0,SCM+FSA) c= s by Y2, FUNCT_4:26;
then A21: P +* I halts_on s by Th18, FUNCT_4:26;
then A22: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by A1, Th37, A19;
A24: P +* (I ';' J) = P by A3, FUNCT_4:104;
X1: P +* I halts_on s +* (Start-At (0,SCM+FSA)) by A21, A1, FUNCT_4:104;
NPP (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) = NPP (Comput (P,s,(LifeSpan ((P +* I),s)))) by A2, A24, Th40, X1;
then A25: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))) by A11, COMPOS_1:138;
A26: Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))))))) = Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA)))))) by EXTPRO_1:5;
A27: DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))) by A1, A25, Th38, A19, A21;
A28: J c= (P +* I) +* J by FUNCT_4:26;
WW1: Reloc (J,(card I)) c= P by A13, A3, XBOOLE_1:1;
WW: Start-At (0,SCM+FSA) c= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
A29: IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA))))))))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA)))))))) by Th27, A28, A27, A22, WW, WW1;
dom P = NAT by PARTFUN1:def 4;
hence IC (Comput (P,s,m)) in dom P ; :: thesis: CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA
A30: J c= (P +* I) +* J by FUNCT_4:26;
(P +* I) +* J halts_on (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Start-At (0,SCM+FSA)) by WW, Def3, A30;
then CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A29, A26, EXTPRO_1:def 14
.= halt SCM+FSA by COMPOS_1:93 ;
hence CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA ; :: thesis: verum