set D = Int-Locations \/ FinSeq-Locations;
set SAt = Start-At (0,SCM+FSA);
let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,SCMFSA6B:def 3 :: thesis: ( not (I ';' J) +* (Start-At (0,SCM+FSA)) c= s or ProgramPart s halts_on s )
set SA0 = Start-At (0,SCM+FSA);
set JAt = J +* (Start-At (0,SCM+FSA));
set s1 = s +* I;
set s3 = (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)));
set m1 = LifeSpan ((ProgramPart (s +* I)),(s +* I));
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))));
reconsider kk = DataPart (J +* (Start-At (0,SCM+FSA))) as Function ;

A1: now

let x be set ; :: thesis: ( x in dom (DataPart (J +* (Start-At (0,SCM+FSA)))) implies kk . b₁ = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b₁ )
assume x in dom (DataPart (J +* (Start-At (0,SCM+FSA)))) ; :: thesis: kk . b₁ = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . b₁
then A2: x in (dom (J +* (Start-At (0,SCM+FSA)))) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
then A3: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 4;
x in dom (J +* (Start-At (0,SCM+FSA))) by A2, 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 SCM+FSA)} by FUNCOP_1:19;
then A4: ( x in dom J or x in {(IC SCM+FSA)} ) by XBOOLE_0:def 3;

per cases ( x in dom J or x = IC SCM+FSA ) by A4, TARSKI:def 1;

suppose A5: x in dom J ; :: thesis: kk . 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 A5;
kk . l = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . l by A3, SCMFSA6A:37;
hence kk . x = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) . x ; :: thesis: verum

end;

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

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

end;

end;

end;

J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then dom (J +* (Start-At (0,SCM+FSA))) c= dom ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))) by GRFUNC_1:8;
then A6: dom (J +* (Start-At (0,SCM+FSA))) c= the carrier of SCM+FSA by PARTFUN1:def 4;
dom (DataPart (J +* (Start-At (0,SCM+FSA)))) = (dom (J +* (Start-At (0,SCM+FSA)))) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
then dom (DataPart (J +* (Start-At (0,SCM+FSA)))) c= the carrier of SCM+FSA /\ (Int-Locations \/ FinSeq-Locations) by A6, XBOOLE_1:26;
then dom (DataPart (J +* (Start-At (0,SCM+FSA)))) 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 (J +* (Start-At (0,SCM+FSA)))) c= dom (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) by RELAT_1:90, SCMFSA_2:127;
then ( ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))) | (Int-Locations \/ FinSeq-Locations) = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) +* kk & DataPart (J +* (Start-At (0,SCM+FSA))) c= DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) ) by A1, FUNCT_4:75, GRFUNC_1:8, SCMFSA_2:127;
then A7: 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))))) +* (J +* (Start-At (0,SCM+FSA)))) by LATTICE2:8, SCMFSA_2:127;
assume A8: (I ';' J) +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: ProgramPart s halts_on s
then A9: s = s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
reconsider m = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))))) as Element of NAT ;
A10: dom (Directed I) = dom I by FUNCT_4:105;
A11: ProgramPart (Relocated (J,(card I))) c= I ';' J by FUNCT_4:26;
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 )
set s4 = Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1));
A12: Directed I c= I ';' J by SCMFSA6A:55;
dom (I ';' J) misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then A13: I ';' J c= (I ';' J) +* (Start-At (0,SCM+FSA)) by FUNCT_4:33;
then I ';' J c= s by A8, XBOOLE_1:1;
then ProgramPart (Relocated (J,(card I))) c= s by A11, XBOOLE_1:1;
then A14: ( J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) ) by AMI_1:81, FUNCT_4:26;
A15: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A10, FUNCT_4:20
.= (s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Directed I) by A8, LATTICE2:8
.= s +* (((I ';' J) +* (Start-At (0,SCM+FSA))) +* (Directed I)) by FUNCT_4:15
.= s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A12, A13, LATTICE2:8, XBOOLE_1:1
.= s by A8, LATTICE2:8 ;
then A16: Directed I c= s by FUNCT_4:26;
Start-At (0,SCM+FSA) c= (I ';' J) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
then A17: Start-At (0,SCM+FSA) c= s by A8, XBOOLE_1:1;
then s +* (Start-At (0,SCM+FSA)) = 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 A18: s +* (I +* (Start-At (0,SCM+FSA))) = s +* I by FUNCT_4:36;
then A19: ProgramPart (s +* I) halts_on s +* I by Th18, FUNCT_4:26;
then A20: IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I by A17, A15, Th37, FUNCT_4:26;
s +* I = (Initialize s) +* I by A17, FUNCT_4:79
.= Initialize (s +* I) by COMPOS_1:83
.= s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:15 ;
then A21: DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))) by A9, A19, A7, Th40, SCMFSA6A:39;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by AMI_1:123;
u: 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))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))))))) = 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))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))))) by EXTPRO_1:5;
TZ: ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
TU: ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(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))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
I +* (Start-At (0,SCM+FSA)) c= s +* I by A18, FUNCT_4:26;
then ProgramPart (s +* I) halts_on s +* I by Th18;
then 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))))) +* (J +* (Start-At (0,SCM+FSA)))) by A17, A21, A16, Th38;
then IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))))))))),(card I)) = CurInstr ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(Comput ((ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))),(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))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))))))) by A20, A14, Th27, TU, TZ;
then A22: IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))))))))),(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))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))))))))) by u, T;
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
( J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))) & J +* (Start-At (0,SCM+FSA)) is halting ) by Def3, FUNCT_4:26;
then ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA)))) halts_on (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (J +* (Start-At (0,SCM+FSA))) by EXTPRO_1:def 10;
then CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A22, 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