set D = Data-Locations ;
let s be State of SCM+FSA; :: according to SCM_HALT:def 1 :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for P being Instruction-Sequence of SCM+FSA st I ";" J c= P holds
P halts_on s )
assume A1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for P being Instruction-Sequence of SCM+FSA st I ";" J c= P holds
P halts_on s
then A2: s = Initialized s by FUNCT_4:98;
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( I ";" J c= p implies p halts_on s )
assume A3: I ";" J c= p ; :: thesis: p halts_on s
A4: p = p +* (I ";" J) by A3, FUNCT_4:98;
set p1 = p +* I;
set s3 = (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1));
set p3 = (p +* I) +* J;
A5: J c= (p +* I) +* J by FUNCT_4:25;
set m1 = LifeSpan ((p +* I),s);
set s4 = Comput (p,s,((LifeSpan ((p +* I),s)) + 1));
A6: I c= p +* I by FUNCT_4:25;
A7: Reloc (J,(card I)) c= I ";" J by SCMFSA6A:38;
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))));
A8: dom (DataPart (Initialize ((intloc 0) .--> 1))) = (dom (Initialize ((intloc 0) .--> 1))) /\ (Data-Locations ) by RELAT_1:61;
reconsider m = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))) as Element of NAT by ORDINAL1:def 12;
A9: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
I c= p +* I by FUNCT_4:25;
then A10: p +* I halts_on Initialized s by Def1, A9;
A11: now :: thesis: for x being object st x in dom (DataPart (Initialize ((intloc 0) .--> 1))) holds
(DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . x = (DataPart (Initialize ((intloc 0) .--> 1))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Initialize ((intloc 0) .--> 1))) implies (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . b1 = (DataPart (Initialize ((intloc 0) .--> 1))) . b1 )
DataPart (Initialize ((intloc 0) .--> 1)) c= Initialize ((intloc 0) .--> 1) by RELAT_1:59;
then A12: dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (Initialize ((intloc 0) .--> 1)) by RELAT_1:11;
assume A13: x in dom (DataPart (Initialize ((intloc 0) .--> 1))) ; :: thesis: (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . b1 = (DataPart (Initialize ((intloc 0) .--> 1))) . b1
then x in dom (Initialize ((intloc 0) .--> 1)) by A12;
then A14: x in {(intloc 0),(IC )} by Lm2, ENUMSET1:1;
per cases ( x = intloc 0 or x = IC ) by A14, TARSKI:def 2;
end;
end;
take m ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (p,s,m)) in dom p & CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA )
IC (Comput (p,s,m)) in NAT ;
hence IC (Comput (p,s,m)) in dom p by PARTFUN1:def 2; :: thesis: CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA
Directed I c= I ";" J by SCMFSA6A:16;
then A18: Directed I c= p by A3, XBOOLE_1:1;
Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
then dom (Initialize ((intloc 0) .--> 1)) c= dom ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by GRFUNC_1:2;
then dom (Initialize ((intloc 0) .--> 1)) c= the carrier of SCM+FSA by PARTFUN1:def 2;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= the carrier of SCM+FSA /\ (Data-Locations ) by A8, XBOOLE_1:26;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= (dom (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) /\ (Data-Locations ) by PARTFUN1:def 2;
then dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by RELAT_1:61;
then DataPart (Initialize ((intloc 0) .--> 1)) c= DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A11, GRFUNC_1:2;
then A19: DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:98
.= DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71 ;
A20: DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A19, A2, A4, A10, Th12;
I c= p +* I by FUNCT_4:25;
then A21: p +* I halts_on s by A1, Def1;
then A22: DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A1, Th10, A20, A18;
A23: Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))))) by EXTPRO_1:4;
A24: Reloc (J,(card I)) c= p by A7, A3, XBOOLE_1:1;
A25: Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A26: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I by A21, A18, Th9, A1;
A27: IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))))),(card I)) = CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))))) by A23, A25, A5, A24, Th4, A26, A22;
(p +* I) +* J halts_on (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by A5, Def1, A25;
then CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A27, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
hence CurInstr (p,(Comput (p,s,m))) = halt SCM+FSA ; :: thesis: verum