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) +* (Ig +* (Start-At 0 ,SCM+FSA )) 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 AMI_1:122;
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) +* ((Ig ';' J) +* (Start-At 0 ,SCM+FSA )) 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 = J +* (Start-At 0 ,SCM+FSA );
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A11: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
(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)))) +* (J +* (Start-At 0 ,SCM+FSA )) by SCMFSA8C:18;
then J +* (Start-At 0 ,SCM+FSA ) 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)) +* (J +* (Start-At 0 ,SCM+FSA )) 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, AMI_1:122 ;
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: