set D = Int-Locations \/ FinSeq-Locations;
set JAt = Initialized J;
let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,SCM_HALT:def 2 :: thesis: ( not Initialized (I ';' J) c= s or ProgramPart s halts_on s )
A1: Initialized (I ';' J) = (I ';' J) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15;
set s1 = s +* I;
set s3 = (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J);
set m1 = LifeSpan ((ProgramPart (s +* I)),(s +* I));
set s4 = Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1));
T4: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by AMI_1:123;
A2: ProgramPart (Relocated (J,(card I))) c= I ';' J by FUNCT_4:26;
A3: dom I misses dom (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by Th2;
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)));
A4: dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
reconsider m = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))) as Element of NAT ;
A5: dom (Directed I) = dom I by FUNCT_4:105;
assume A6: Initialized (I ';' J) c= s ; :: thesis: ProgramPart s halts_on s
then A7: s = s +* (Initialized (I ';' J)) by FUNCT_4:79;
dom (I ';' J) misses dom (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by Th2;
then A8: I ';' J c= Initialized (I ';' J) by A1, FUNCT_4:33;
then I ';' J c= s by A6, XBOOLE_1:1;
then ProgramPart (Relocated (J,(card I))) c= s by A2, XBOOLE_1:1;
then A9: ( Initialized J c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) ) by AMI_1:81, FUNCT_4:26;
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= (I ';' J) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then A10: ((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= s by A6, A1, XBOOLE_1:1;
then s +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) = s by FUNCT_4:79;
then A11: s +* I = s +* ((((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) +* I) by FUNCT_4:15
.= s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) by A3, FUNCT_4:36
.= s +* (Initialized I) by FUNCT_4:15 ;
then A12: ProgramPart (s +* I) halts_on s +* I by Th5, FUNCT_4:26;
A13: Initialized I c= s +* I by A11, FUNCT_4:26;

A14: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized J)) implies (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b₁ )
assume x in dom (DataPart (Initialized J)) ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b₁
then A15: x in (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
then A16: x in dom (Initialized J) by XBOOLE_0:def 4;
A17: x in Int-Locations \/ FinSeq-Locations by A15, XBOOLE_0:def 4;

per cases ( x in dom J or x = intloc 0 or x = IC SCM+FSA ) by A16, SCMFSA6A:44;

suppose A18: x in dom J ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b₁

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

end;

suppose A19: x = intloc 0 ; :: thesis: (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b₁ = (DataPart (Initialized J)) . b₁

then x in Int-Locations by SCMFSA_2:9;
then A20: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . x = (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) . x by FUNCT_1:72, SCMFSA_2:127
.= 1 by A13, A19, Def3
.= (Initialized J) . x by A19, SCMFSA6A:46
.= (DataPart (Initialized J)) . x by A20, FUNCT_1:72, SCMFSA_2:127 ;
:: thesis: verum

end;

suppose x = IC SCM+FSA ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b₁

hence (DataPart (Initialized J)) . x = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . x by A15, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

take m ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,m)) in proj1 (ProgramPart s) & CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = halt SCM+FSA )
IC (Comput ((ProgramPart s),s,m)) in NAT ;
hence IC (Comput ((ProgramPart s),s,m)) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = halt SCM+FSA
A21: Directed I c= I ';' J by SCMFSA6A:55;
A22: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A5, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A6, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A21, A8, LATTICE2:8, XBOOLE_1:1
.= s by A6, LATTICE2:8 ;
then A23: Directed I c= s by FUNCT_4:26;
A24: Initialized J c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
then dom (Initialized J) c= dom ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by GRFUNC_1:8;
then dom (Initialized J) c= the carrier of SCM+FSA by PARTFUN1:def 4;
then dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Int-Locations \/ FinSeq-Locations) by A4, XBOOLE_1:26;
then dom (DataPart (Initialized J)) c= (dom (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) /\ (Int-Locations \/ FinSeq-Locations) by PARTFUN1:def 4;
then dom (DataPart (Initialized J)) c= dom (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) by RELAT_1:90, SCMFSA_2:127;
then ( DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) +* (DataPart (Initialized J)) & DataPart (Initialized J) c= DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) ) by A14, FUNCT_4:75, GRFUNC_1:8;
then DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by LATTICE2:8;
then X: DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by A7, A11, A12, Th24, SCMFSA6A:39;
ProgramPart (s +* I) halts_on s +* I by A13, Th5;
then A25: DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by A10, A23, Th22, X;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by AMI_1:123;
x: Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))) by EXTPRO_1:5;
IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I by A10, A12, A22, Th21, FUNCT_4:26;
then IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))))) by A25, A9, Th12, T4;
then A26: IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))) by x, T;
ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) halts_on (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by A24, EXTPRO_1:def 10;
then CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A26, EXTPRO_1:def 14
.= halt SCM+FSA by SCMFSA_4:8 ;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = halt SCM+FSA ; :: thesis: verum