set D = Data-Locations ;
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 11 :: thesis: for b₁ being set holds
( not I ';' J c= b₁ or b₁ halts_on s )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I ';' J c= P or P halts_on s )
assume A3: I ';' J c= P ; :: thesis: P halts_on s
set JAt = Start-At (0,SCM+FSA);
set s3 = Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
set m1 = LifeSpan ((P +* I),s);
set m3 = LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))));
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 ) by RELAT_1:61;
x in dom (Start-At (0,SCM+FSA)) by A6, XBOOLE_0:def 4;
then x in {(IC )} by FUNCOP_1:13;
then x = IC by TARSKI:def 1;
then not x in Data-Locations by STRUCT_0:3;
hence kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A6, XBOOLE_0:def 4; :: thesis: verum

end;

Start-At (0,SCM+FSA) c= Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) by FUNCT_4:25;
then dom (Start-At (0,SCM+FSA)) c= dom (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by GRFUNC_1:2;
then A10: dom (Start-At (0,SCM+FSA)) c= the carrier of SCM+FSA by PARTFUN1:def 2;
dom (DataPart (Start-At (0,SCM+FSA))) = (dom (Start-At (0,SCM+FSA))) /\ (Data-Locations ) by RELAT_1:61;
then dom (DataPart (Start-At (0,SCM+FSA))) c= the carrier of SCM+FSA /\ (Data-Locations ) 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 ) by PARTFUN1:def 2;
then dom (DataPart (Start-At (0,SCM+FSA))) c= dom (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by RELAT_1:61;
then ( (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) | (Data-Locations ) = (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:71, GRFUNC_1:2;
then A11: DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by FUNCT_4:98;
reconsider m = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))))) as Element of NAT ;
A13: Reloc (J,(card I)) c= I ';' J by FUNCT_4:25;
take m ; :: according to EXTPRO_1:def 8 :: 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));
B19: Directed I c= I ';' J by SCMFSA6A:16;
A21: P +* I halts_on s by Th18, FUNCT_4:25;
then A22: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by Th37, B19, A3, XBOOLE_1:1;
A24: P +* (I ';' J) = P by A3, FUNCT_4:98;
A25: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A11, A24, Th40, A21;
A26: Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))))))) = Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))))))) by EXTPRO_1:4;
A27: DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A25, Th38, B19, A21, A3, XBOOLE_1:1;
A28: J c= (P +* I) +* J by FUNCT_4:25;
WW1: Reloc (J,(card I)) c= P by A13, A3, XBOOLE_1:1;
A29: IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))),(LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))))))))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))))))))) by Th27, A28, A27, A22, WW1;
dom P = NAT by PARTFUN1:def 2;
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:25;
(P +* I) +* J halts_on Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) by A30, AMISTD_1:def 11;
then CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A29, A26, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_1:11 ;
hence CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA ; :: thesis: verum