set D = Data-Locations SCM+FSA;
let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,SCMFSA6B:def 3 :: thesis: ( not Initialize (I ';' J) c= s or for b₁ being set holds
( not ProgramPart (Initialize (I ';' J)) c= b₁ or b₁ halts_on s ) )
assume A1: Initialize (I ';' J) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialize (I ';' J)) c= b₁ or b₁ halts_on s )
then A2: s = s +* (Initialize (I ';' J)) by FUNCT_4:79;
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialize (I ';' J)) c= P or P halts_on s )
assume A3: ProgramPart (Initialize (I ';' J)) c= P ; :: thesis: P halts_on s
A4: I ';' J c= P by A3, COMPOS_1:144;
set JAt = Initialize J;
set s1 = s +* I;
set s3 = (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J);
set m1 = LifeSpan ((P +* I),(s +* I));
set m3 = LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)));
reconsider kk = DataPart (Initialize J) as Function ;

A5: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialize J)) implies kk . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁ )
assume x in dom (DataPart (Initialize J)) ; :: thesis: kk . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁
then A6: x in (dom (Initialize J)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then A7: x in Data-Locations SCM+FSA by XBOOLE_0:def 4;
x in dom (Initialize J) by A6, XBOOLE_0:def 4;
then x in (dom J) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
then x in (dom J) \/ {(IC )} by FUNCOP_1:19;
then A8: ( x in dom J or x in {(IC )} ) by XBOOLE_0:def 3;

per cases ( x in dom J or x = IC ) by A8, TARSKI:def 1;

suppose A9: x in dom J ; :: thesis: kk . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁

dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A9;
kk . l = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . l by A7, SCMFSA6A:37;
hence kk . x = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . x ; :: thesis: verum

end;

suppose x = IC ; :: thesis: kk . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁

hence kk . x = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . x by A6, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

Initialize J c= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J) by FUNCT_4:26;
then dom (Initialize J) c= dom ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)) by GRFUNC_1:8;
then A10: dom (Initialize J) c= the carrier of SCM+FSA by PARTFUN1:def 4;
dom (DataPart (Initialize J)) = (dom (Initialize J)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then dom (DataPart (Initialize J)) c= the carrier of SCM+FSA /\ (Data-Locations SCM+FSA) by A10, XBOOLE_1:26;
then dom (DataPart (Initialize J)) c= (dom (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) /\ (Data-Locations SCM+FSA) by PARTFUN1:def 4;
then dom (DataPart (Initialize J)) c= dom (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) by RELAT_1:90;
then ( ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)) | (Data-Locations SCM+FSA) = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) +* kk & DataPart (Initialize J) c= DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) ) by A5, FUNCT_4:75, GRFUNC_1:8;
then A11: DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)) by LATTICE2:8;
reconsider m = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)))) as Element of NAT ;
A12: dom (Directed I) = dom I by FUNCT_4:105;
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 +* I))) + 1));
A14: Directed I c= I ';' J by SCMFSA6A:55;
dom (I ';' J) misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then A15: I ';' J c= Initialize (I ';' J) by FUNCT_4:33;
then I ';' J c= s by A1, XBOOLE_1:1;
then Reloc (J,(card I)) c= s by A13, XBOOLE_1:1;
then A16: ( Initialize J c= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J) & Reloc (J,(card I)) c= Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1)) ) by AMI_1:81, FUNCT_4:26;
A17: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A12, FUNCT_4:20
.= (s +* (Initialize (I ';' J))) +* (Directed I) by A1, LATTICE2:8
.= s +* ((Initialize (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialize (I ';' J)) by A14, A15, LATTICE2:8, XBOOLE_1:1
.= s by A1, LATTICE2:8 ;
A18: Directed I c= I ';' J by SCMFSA6A:55;
I ';' J c= P by A3, COMPOS_1:144;
then A19: Directed I c= P by A18, XBOOLE_1:1;
Start-At (0,SCM+FSA) c= Initialize (I ';' J) by FUNCT_4:26;
then A20: Start-At (0,SCM+FSA) c= s by A1, XBOOLE_1:1;
then Initialize s = s by FUNCT_4:79;
then ( dom I misses dom (Start-At (0,SCM+FSA)) & s +* ((Start-At (0,SCM+FSA)) +* I) = s +* I ) by COMPOS_1:140, FUNCT_4:15;
then s +* (Initialize I) = s +* I by FUNCT_4:36;
then Initialize I c= s +* I by FUNCT_4:26;
then A21: P +* I halts_on s +* I by Th18, FUNCT_4:26;
then A22: IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I by A20, A17, Th37, FUNCT_4:26, A19;
A23: s +* I = (Initialize s) +* I by A20, FUNCT_4:79
.= Initialize (s +* I) by COMPOS_1:83
.= s +* (Initialize I) by FUNCT_4:15 ;
I ';' J c= P by COMPOS_1:144, A3;
then A24: P +* (I ';' J) = P by FUNCT_4:79;
Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* I)))), Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(LifeSpan ((P +* I),(s +* I)))) equal_outside NAT by Th40, A23, A21;
then A25: DataPart (Comput (P,s,(LifeSpan ((P +* I),(s +* I))))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)) by A11, A2, COMPOS_1:138, A23, A24;
A26: Comput (P,s,(((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)))))) = Comput (P,(Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J))))) by EXTPRO_1:5;
A27: DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)) by A20, A25, A17, FUNCT_4:26, Th38, A19, A21;
A28: J c= (P +* I) +* J by FUNCT_4:26;
Reloc (J,(card I)) c= P by A13, A4, XBOOLE_1:1;
then A29: IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J)))))))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J))))))) by Th27, A16, A28, A27, A22;
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
J c= (P +* I) +* J by FUNCT_4:26;
then A30: ProgramPart (Initialize J) c= (P +* I) +* J by COMPOS_1:144;
( Initialize J c= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J) & Initialize J is halting ) by Def3, FUNCT_4:26;
then (P +* I) +* J halts_on (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialize J) by EXTPRO_1:def 10, A30;
then CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A29, EXTPRO_1:def 14, A26
.= halt SCM+FSA by COMPOS_1:93 ;
hence CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA ; :: thesis: verum