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

A1: now

let x be set ; :: thesis: ( x in dom (DataPart (J +* (Start-At (insloc 0 )))) implies kk . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁ )
assume x in dom (DataPart (J +* (Start-At (insloc 0 )))) ; :: thesis: kk . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁
then A2: x in (dom (J +* (Start-At (insloc 0 )))) /\ (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 (insloc 0 ))) by A2, XBOOLE_0:def 4;
then x in (dom J) \/ (dom (Start-At (insloc 0 ))) 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 (Computation (s +* I),(LifeSpan (s +* I)))) . b₁

dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCM+FSA by A5, AMI_1:def 4;
kk . l = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . l by A3, SCMFSA6A:37;
hence kk . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x ; :: thesis: verum

end;

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

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

end;

end;

end;

J +* (Start-At (insloc 0 )) c= (Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then dom (J +* (Start-At (insloc 0 ))) c= dom ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) by GRFUNC_1:8;
then A6: dom (J +* (Start-At (insloc 0 ))) c= the carrier of SCM+FSA by AMI_1:79;
dom (DataPart (J +* (Start-At (insloc 0 )))) = (dom (J +* (Start-At (insloc 0 )))) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then dom (DataPart (J +* (Start-At (insloc 0 )))) c= the carrier of SCM+FSA /\ (Int-Locations \/ FinSeq-Locations ) by A6, XBOOLE_1:26;
then dom (DataPart (J +* (Start-At (insloc 0 )))) c= (dom (Computation (s +* I),(LifeSpan (s +* I)))) /\ (Int-Locations \/ FinSeq-Locations ) by AMI_1:79;
then dom (DataPart (J +* (Start-At (insloc 0 )))) c= dom (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) by RELAT_1:90, SCMFSA_2:127;
then ( ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) | (Int-Locations \/ FinSeq-Locations ) = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) +* kk & DataPart (J +* (Start-At (insloc 0 ))) c= DataPart (Computation (s +* I),(LifeSpan (s +* I))) ) by A1, FUNCT_4:75, GRFUNC_1:8, SCMFSA_2:127;
then A7: DataPart (Computation (s +* I),(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) by LATTICE2:8, SCMFSA_2:127;
assume A8: (I ';' J) +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
then A9: s = s +* ((I ';' J) +* (Start-At (insloc 0 ))) by FUNCT_4:79;
reconsider m = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))))) 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 AMI_1:def 20 :: thesis: CurInstr (Computation s,m) = halt SCM+FSA
set s4 = Computation s,((LifeSpan (s +* I)) + 1);
A12: Directed I c= I ';' J by SCMFSA6A:55;
dom (I ';' J) misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then A13: I ';' J c= (I ';' J) +* (Start-At (insloc 0 )) 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 (insloc 0 )) c= (Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))) & [(ProgramPart (Relocated J,(card I)))] c= Computation s,((LifeSpan (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 (insloc 0 )))) +* (Directed I) by A8, LATTICE2:8
.= s +* (((I ';' J) +* (Start-At (insloc 0 ))) +* (Directed I)) by FUNCT_4:15
.= s +* ((I ';' J) +* (Start-At (insloc 0 ))) 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 (insloc 0 ) c= (I ';' J) +* (Start-At (insloc 0 )) by FUNCT_4:26;
then A17: Start-At (insloc 0 ) c= s by A8, XBOOLE_1:1;
then s +* (Start-At (insloc 0 )) = s by FUNCT_4:79;
then ( dom I misses dom (Start-At (insloc 0 )) & s +* ((Start-At (insloc 0 )) +* I) = s +* I ) by FUNCT_4:15, SF_MASTR:64;
then A18: s +* (I +* (Start-At (insloc 0 ))) = s +* I by FUNCT_4:36;
then A19: s +* I is halting by Th18, FUNCT_4:26;
then A20: IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) by A17, A15, Th37, FUNCT_4:26;
s +* I = (s +* (Start-At (insloc 0 ))) +* I by A17, FUNCT_4:79
.= (s +* I) +* (Start-At (insloc 0 )) by Th14
.= s +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:15 ;
then A21: DataPart (Computation s,(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) by A9, A19, A7, Th40, SCMFSA6A:39;
I +* (Start-At (insloc 0 )) c= s +* I by A18, FUNCT_4:26;
then DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) by A17, A21, A16, Th18, Th38;
then IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))))))),(card I) = CurInstr (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))))) by A20, A14, Th27;
then A22: IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))))))),(card I) = CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))))))) by AMI_1:51;
( J +* (Start-At (insloc 0 )) c= (Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))) & J +* (Start-At (insloc 0 )) is halting ) by Def3, FUNCT_4:26;
then (Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))) is halting by AMI_1:def 26;
hence CurInstr (Computation s,m) = IncAddr (halt SCM+FSA ),(card I) by A22, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
:: thesis: verum