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