set D = Int-Locations \/ FinSeq-Locations ;
set SAt = Start-At 0 ,SCM+FSA ;
let s be State of SCM+FSA ; :: according to AMI_1:def 26,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 . b1 = (DataPart (Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (ProgramPart (s +* I)),(s +* I)))) . b1 )
assume x in dom (DataPart (J +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: kk . b1 = (DataPart (Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (ProgramPart (s +* I)),(s +* I)))) . b1
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 . b1 = (DataPart (Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (ProgramPart (s +* I)),(s +* I)))) . b1
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 . b1 = (DataPart (Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (ProgramPart (s +* I)),(s +* I)))) . b1
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 AMI_1:def 20 :: 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 SF_MASTR:64;
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 FUNCT_4:15, SF_MASTR:64;
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 = (s +* (Start-At 0 ,SCM+FSA )) +* I by A17, FUNCT_4:79
.= (s +* I) +* (Start-At 0 ,SCM+FSA ) by Th14
.= 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 AMI_1:51;
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 AMI_1:def 26;
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,m) = IncAddr (halt SCM+FSA ),(card I) by A22, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,m) = halt SCM+FSA ; :: thesis: verum