set D = Data-Locations ;
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: 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 A1: 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 ;

A2: now :: thesis: for x being object st x in dom (DataPart (Start-At (0,SCM+FSA))) holds
kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x

let x be object ; :: 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 A3: x in (dom (Start-At (0,SCM+FSA))) /\ (Data-Locations ) by RELAT_1:61;
x in dom (Start-At (0,SCM+FSA)) by A3, XBOOLE_0:def 4;
then x in {(IC )} ;
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 A3, 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 A4: 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 A4, 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 A2, FUNCT_4:71, GRFUNC_1:2;
then A5: 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 by ORDINAL1:def 12;
A6: Reloc (J,(card I)) c= I ";" J by SCMFSA6A:38;
take m ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,m)) in dom P & CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA )
set s4 = Comput (P,s,((LifeSpan ((P +* I),s)) + 1));
A7: Directed I c= I ";" J by SCMFSA6A:16;
A8: P +* I halts_on s by Th1, FUNCT_4:25;
then A9: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by Th11, A7, A1, XBOOLE_1:1;
A10: P +* (I ";" J) = P by A1, FUNCT_4:98;
A11: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A5, A10, Th14, A8;
A12: 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;
A13: DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A11, Th12, A7, A8, A1, XBOOLE_1:1;
A14: J c= (P +* I) +* J by FUNCT_4:25;
A15: Reloc (J,(card I)) c= P by A6, A1, XBOOLE_1:1;
A16: 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 Th6, A14, A13, A9, A15;
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
A17: J c= (P +* I) +* J by FUNCT_4:25;
(P +* I) +* J halts_on Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) by A17, AMISTD_1:def 11;
then CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A16, A12, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
hence CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA ; :: thesis: verum