let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let s be State of SCM+FSA; :: thesis:
let J be Program of SCM+FSA; :: thesis:
let Ig be good Program of SCM+FSA; :: thesis:
set I = Ig;
assume that
A1: Ig is_halting_on Initialized s,p and
A2: J is_halting_on IExec (Ig,p,s),p and
A3: Ig is_closed_on Initialized s,p and
A4: J is_closed_on IExec (Ig,p,s),p ; :: thesis:
set Is = Initialized s;
A5: (Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
set s1 = s +* (Initialized Ig);
set p1 = p +* Ig;
set m1 = LifeSpan ((p +* Ig),(s +* (Initialized Ig)));
set s3 = (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J);
set p3 = (p +* Ig) +* J;
A6: ((p +* Ig) +* J) +* J = (p +* Ig) +* J by FUNCT_4:99;
A7: ProgramPart Ig = Ig by RELAT_1:209;
s +* (Initialized Ig) = (Initialized s) +* (Initialized Ig) by SCMFSA8A:8;
then A8: s +* (Initialized Ig) = (Initialized s) +* (Initialize Ig) by A5, SCMFSA8C:18;
then A9: p +* Ig halts_on s +* (Initialized Ig) by A1, SCMFSA7B:def 8, A7;
then A10: (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) = (Result ((p +* Ig),(s +* (Initialized Ig)))) +* (Initialized J) by EXTPRO_1:23;
set s2 = s +* (Initialized (Ig ';' J));
set p2 = p +* (Ig ';' J);
A11: Ig ';' J c= p +* (Ig ';' J) by FUNCT_4:26;
s +* (Initialized (Ig ';' J)) = (Initialized s) +* (Initialized (Ig ';' J)) by SCMFSA8A:8;
then s +* (Initialized (Ig ';' J)) = (Initialized s) +* (Initialize (Ig ';' J)) by A5, SCMFSA8C:18;
then A12: DataPart (Initialized s) = DataPart (s +* (Initialized (Ig ';' J))) by SCMFSA8A:11;
then A13: (s +* (Initialized (Ig ';' J))) . (intloc 0) = 1 by A5, SCMFSA6A:38;
set JAt = Initialize J;
(Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) . (intloc 0) = 1 by A3, A5, A8, SCMFSA8C:97;
then A14: (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) = (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialize J) by SCMFSA8C:18;
then Initialize J c= (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) by FUNCT_4:26;
then A15: (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) = ((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)) +* (Initialize J) by FUNCT_4:79;
DataPart (IExec (Ig,p,s)) = DataPart ((Result ((p +* Ig),(s +* (Initialized Ig)))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((p +* Ig),(s +* (Initialized Ig)))) by COMPOS_1:82
.= DataPart (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A9, EXTPRO_1:23 ;
then A16: DataPart (IExec (Ig,p,s)) = DataPart ((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)) by A14, SCMFSA8A:11;
then A17: J is_halting_on (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J),(p +* Ig) +* J by A2, A4, SCMFSA8B:8;
A18: Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
Initialized Ig = Ig +* (Initialize ((intloc 0) .--> 1))
.= Initialize (Ig +* ((intloc 0) .--> 1)) by FUNCT_4:15 ;
then Start-At (0,SCM+FSA) c= Initialized Ig by FUNCT_4:26;
then Start-At (0,SCM+FSA) c= (s +* (Initialized (Ig ';' J))) +* Ig by A18, XBOOLE_1:1;
then A19: (s +* (Initialized (Ig ';' J))) +* Ig = Initialize ((s +* (Initialized (Ig ';' J))) +* Ig) by FUNCT_4:79
.= (s +* (Initialized (Ig ';' J))) +* (Initialize Ig) by FUNCT_4:15 ;
then Result (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig)), Result ((p +* Ig),(s +* (Initialized Ig))) equal_outside NAT by A1, A3, A8, A12, FUNCT_7:28, SCMFSA8C:101;
then A20: DataPart ((Result (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J)) = DataPart ((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)) by A10, FUNCT_7:106, COMPOS_1:138;
A21: DataPart (IExec (Ig,p,s)) = DataPart (IExec (Ig,p,(Initialized s))) by SCMFSA8C:17
.= DataPart (IExec (Ig,(p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))))) by A1, A3, A5, A12, SCMFSA8C:46 ;
then A22: J is_closed_on IExec (Ig,(p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J)))),p +* (Ig ';' J) by A2, A4, SCMFSA8B:8;
A23: Initialized (Ig ';' J) c= s +* (Initialized (Ig ';' J)) by FUNCT_4:26;
A24: Ig is_closed_on s +* (Initialized (Ig ';' J)),p +* (Ig ';' J) by A3, A12, SCMFSA8B:6;
A25: J is_halting_on IExec (Ig,(p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J)))),p +* (Ig ';' J) by A2, A4, A21, SCMFSA8B:8;
Ig is_halting_on s +* (Initialized (Ig ';' J)),p +* (Ig ';' J) by A1, A3, A12, SCMFSA8B:8;
then A26: LifeSpan ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J)))) = ((LifeSpan (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig))) + 1) + (LifeSpan ((((p +* (Ig ';' J)) +* Ig) +* J),((Result (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J)))) by A24, A13, A22, A25, A23, Lm1, A11;
Initialize J c= (Result (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
then A27: (Result (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J) = ((Result (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J)) +* (Initialize J) by FUNCT_4:79;
A28: J is_closed_on (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J),(p +* Ig) +* J by A4, A16, SCMFSA8B:6;
A29: LifeSpan (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig)) = LifeSpan ((p +* Ig),(s +* (Initialized Ig))) by A1, A3, A8, A12, A19, SCMFSA8C:101;
LifeSpan ((((p +* (Ig ';' J)) +* Ig) +* J),((Result (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J))) = LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))) by A28, A17, A15, A27, A20, SCMFSA8C:101, A6;
hence LifeSpan ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J)))) = ((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialized Ig)))) +* (Initialized J)))) by A10, A26, A29; :: thesis: