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 SAt = Start-At (0,SCM+FSA);
set D = Int-Locations \/ FinSeq-Locations;
set I = Ig;
assume that
A1: Ig is_halting_on Initialized s and
A2: J is_halting_on IExec (Ig,s) and
A3: Ig is_closed_on Initialized s and
A4: J is_closed_on IExec (Ig,s) ; :: thesis:
set Is = Initialized s;
A5: (Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
set s1 = s +* (Initialized Ig);
set m1 = LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)));
set s3 = (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J);
s +* (Initialized Ig) = (Initialized s) +* (Initialized Ig) by SCMFSA8A:8;
then A6: s +* (Initialized Ig) = (Initialized s) +* (Initialize Ig) by A5, SCMFSA8C:18;
then A7: ProgramPart (s +* (Initialized Ig)) halts_on s +* (Initialized Ig) by A1, SCMFSA7B:def 8;
then A8: (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) = (Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J) by EXTPRO_1:23;
set s2 = s +* (Initialized (Ig ';' J));
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 A9: DataPart (Initialized s) = DataPart (s +* (Initialized (Ig ';' J))) by SCMFSA8A:11;
then A10: (s +* (Initialized (Ig ';' J))) . (intloc 0) = 1 by A5, SCMFSA6A:38;
set JAt = Initialize J;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A11: dom (ProgramPart s) misses Int-Locations \/ FinSeq-Locations by COMPOS_1:34;
(Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) . (intloc 0) = 1 by A3, A5, A6, SCMFSA8C:97;
then A12: (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) = (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialize J) by SCMFSA8C:18;
then Initialize J c= (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) by FUNCT_4:26;
then A13: (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) = ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)) +* (Initialize J) by FUNCT_4:79;
DataPart (IExec (Ig,s)) = DataPart ((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) by A11, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) by A7, EXTPRO_1:23 ;
then A14: DataPart (IExec (Ig,s)) = DataPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)) by A12, SCMFSA8A:11;
then A15: J is_halting_on (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) by A2, A4, SCMFSA8B:8;
A16: Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
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 A16, XBOOLE_1:1;
then A17: (s +* (Initialized (Ig ';' J))) +* Ig = ((s +* (Initialized (Ig ';' J))) +* Ig) +* (Start-At (0,SCM+FSA)) by FUNCT_4:79
.= (s +* (Initialized (Ig ';' J))) +* (Ig +* (Start-At (0,SCM+FSA))) by FUNCT_4:15 ;
then Result ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig)), Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))) equal_outside NAT by A1, A3, A6, A9, FUNCT_7:28, SCMFSA8C:101;
then A18: DataPart ((Result ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J)) = DataPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)) by A8, FUNCT_7:106, SCMFSA6A:39;
A19: DataPart (IExec (Ig,s)) = DataPart (IExec (Ig,(Initialized s))) by SCMFSA8C:17
.= DataPart (IExec (Ig,(s +* (Initialized (Ig ';' J))))) by A1, A3, A5, A9, SCMFSA8C:46 ;
then A20: J is_closed_on IExec (Ig,(s +* (Initialized (Ig ';' J)))) by A2, A4, SCMFSA8B:8;
A21: Initialized (Ig ';' J) c= s +* (Initialized (Ig ';' J)) by FUNCT_4:26;
A22: Ig is_closed_on s +* (Initialized (Ig ';' J)) by A3, A9, SCMFSA8B:6;
A23: J is_halting_on IExec (Ig,(s +* (Initialized (Ig ';' J)))) by A2, A4, A19, SCMFSA8B:8;
Ig is_halting_on s +* (Initialized (Ig ';' J)) by A1, A3, A9, SCMFSA8B:8;
then A24: LifeSpan ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J)))) = ((LifeSpan ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J))),((Result ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J)))) by A22, A10, A20, A23, A21, Lm1;
set SAt = Start-At (0,SCM+FSA);
J +* (Start-At (0,SCM+FSA)) c= (Result ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
then A25: (Result ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J) = ((Result ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig))) +* (Initialized J)) +* (J +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
A26: J is_closed_on (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) by A4, A14, SCMFSA8B:6;
LifeSpan ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig)) = LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))) by A1, A3, A6, A9, A17, SCMFSA8C:101;
hence LifeSpan ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J)))) = ((LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J)))) by A26, A15, A13, A8, A24, A25, A18, SCMFSA8C:101; :: thesis: