set SA0 = 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 )
assume A1: (I ';' J) +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
then A2: s = s +* ((I ';' J) +* (Start-At (insloc 0 ))) by FUNCT_4:79;
set SAt = Start-At (insloc 0 );
A3: dom I misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
Start-At (insloc 0 ) c= (I ';' J) +* (Start-At (insloc 0 )) by FUNCT_4:26;
then A4: Start-At (insloc 0 ) c= s by A1, XBOOLE_1:1;
then s +* (Start-At (insloc 0 )) = s by FUNCT_4:79;
then s +* ((Start-At (insloc 0 )) +* I) = s +* I by FUNCT_4:15;
then A5: s +* (I +* (Start-At (insloc 0 ))) = s +* I by A3, FUNCT_4:36;
then A6: I +* (Start-At (insloc 0 )) c= s +* I by FUNCT_4:26;
A7: s +* I = (s +* (Start-At (insloc 0 ))) +* I by A4, FUNCT_4:79
.= (s +* I) +* (Start-At (insloc 0 )) by Th14
.= s +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:15 ;
A8: s +* I is halting by A5, Th18, FUNCT_4:26;
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 ))));
set D = Int-Locations \/ FinSeq-Locations ;
reconsider kk = DataPart (J +* (Start-At (insloc 0 ))) as Function ;
A9: ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) | (Int-Locations \/ FinSeq-Locations ) = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) +* kk by FUNCT_4:75, SCMFSA_2:127;
A10: now
let x be set ; :: thesis: ( x in dom (DataPart (J +* (Start-At (insloc 0 )))) implies kk . b1 = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b1 )
assume x in dom (DataPart (J +* (Start-At (insloc 0 )))) ; :: thesis: kk . b1 = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b1
then A11: x in (dom (J +* (Start-At (insloc 0 )))) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then A12: ( x in dom (J +* (Start-At (insloc 0 ))) & x in Int-Locations \/ FinSeq-Locations ) by 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 A13: ( 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 A13, TARSKI:def 1;
suppose A14: x in dom J ; :: thesis: kk . b1 = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b1
dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCM+FSA by A14, AMI_1:def 4;
kk . l = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . l by A12, SCMFSA6A:37;
hence kk . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x ; :: 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 A15: 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 A15, 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 DataPart (J +* (Start-At (insloc 0 ))) c= DataPart (Computation (s +* I),(LifeSpan (s +* I))) by A10, GRFUNC_1:8;
then DataPart (Computation (s +* I),(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) by A9, LATTICE2:8, SCMFSA_2:127;
then A16: DataPart (Computation s,(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) by A2, A7, A8, Th40, SCMFSA6A:39;
( 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 A17: (Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))) is halting by AMI_1:def 26;
A18: dom (Directed I) = dom I by FUNCT_4:105;
A19: Directed I c= I ';' J by SCMFSA6A:55;
dom (I ';' J) misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then A20: I ';' J c= (I ';' J) +* (Start-At (insloc 0 )) by FUNCT_4:33;
A21: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A18, FUNCT_4:20
.= (s +* ((I ';' J) +* (Start-At (insloc 0 )))) +* (Directed I) by A1, LATTICE2:8
.= s +* (((I ';' J) +* (Start-At (insloc 0 ))) +* (Directed I)) by FUNCT_4:15
.= s +* ((I ';' J) +* (Start-At (insloc 0 ))) by A19, A20, LATTICE2:8, XBOOLE_1:1
.= s by A1, LATTICE2:8 ;
then A22: Directed I c= s by FUNCT_4:26;
A23: IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) by A4, A8, A21, Th37, FUNCT_4:26;
A24: DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 )))) by A4, A6, A16, A22, Th18, Th38;
reconsider m = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))))) as Element of NAT ;
set s4 = Computation s,((LifeSpan (s +* I)) + 1);
A25: J +* (Start-At (insloc 0 )) c= (Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A26: I ';' J c= s by A1, A20, XBOOLE_1:1;
ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
then ProgramPart (Relocated J,(card I)) c= s by A26, XBOOLE_1:1;
then A27: [(ProgramPart (Relocated J,(card I)))] c= Computation s,((LifeSpan (s +* I)) + 1) by AMI_1:81;
take m ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,m) = halt SCM+FSA
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 A23, A24, A25, A27, Th27;
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 s,(((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))))))) by AMI_1:51;
hence CurInstr (Computation s,m) = IncAddr (halt SCM+FSA ),(card I) by A17, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
:: thesis: verum