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:
set ps = s | NAT ;
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 m3 = LifeSpan ((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 IAt = Ig +* (Start-At (insloc 0 ));
set IEJIs = IExec J,(IExec Ig,s);
set Is = Initialize s;
A5: (Initialize s) . (intloc 0 ) = 1 by SCMFSA6C:3;
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: DataPart (Initialize s) = DataPart (s +* (Initialized Ig)) by SCMFSA8A:11;
A8: s +* (Initialized Ig) is halting by A1, A6, SCMFSA7B:def 8;
A9: Ig is_closed_on s +* (Initialized Ig) by A3, A7, SCMFSA8B:6;
A10: Ig +* (Start-At (insloc 0 )) c= s +* (Initialized Ig) by FUNCT_4:26, SCMFSA6B:8;
A11: Initialized (Ig ';' J) c= s +* (Initialized (Ig ';' J)) by FUNCT_4:26;
s +* (Initialized (Ig ';' J)) = (Initialize s) +* (Initialized (Ig ';' J)) by SCMFSA8A:8;
then A12: s +* (Initialized (Ig ';' J)) = (Initialize s) +* ((Ig ';' J) +* (Start-At (insloc 0 ))) by A5, SCMFSA8C:18;
then A13: DataPart (Initialize s) = DataPart (s +* (Initialized (Ig ';' J))) by SCMFSA8A:11;
Ig ';' J is_halting_on Initialize s by A1, A2, A3, A4, Th4;
then A14: s +* (Initialized (Ig ';' J)) is halting by A12, SCMFSA7B:def 8;
Start-At (insloc 0 ) c= Initialized (Ig ';' J) by SCMFSA6B:4;
then Start-At (insloc 0 ) c= s +* (Initialized (Ig ';' J)) by A11, XBOOLE_1:1;
then A15: (s +* (Initialized (Ig ';' J))) +* Ig = ((s +* (Initialized (Ig ';' J))) +* (Start-At (insloc 0 ))) +* Ig by FUNCT_4:79
.= ((s +* (Initialized (Ig ';' J))) +* Ig) +* (Start-At (insloc 0 )) by SCMFSA6B:14
.= (s +* (Initialized (Ig ';' J))) +* (Ig +* (Start-At (insloc 0 ))) by FUNCT_4:15 ;
A16: Ig is_closed_on s +* (Initialized (Ig ';' J)) by A3, A13, SCMFSA8B:6;
A17: Ig is_halting_on s +* (Initialized (Ig ';' J)) by A1, A3, A13, SCMFSA8B:8;
then A18: (s +* (Initialized (Ig ';' J))) +* Ig is halting by A15, SCMFSA7B:def 8;
DataPart (s +* (Initialized (Ig ';' J))) = DataPart ((s +* (Initialized (Ig ';' J))) +* Ig) by SCMFSA8C:34;
then A19: Ig is_closed_on (s +* (Initialized (Ig ';' J))) +* Ig by A3, A13, SCMFSA8B:6;
(Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) . (intloc 0 ) = 1 by A3, A5, A6, SCMFSA8C:97;
then A20: (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 A21: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
A22: DataPart (IExec Ig,s) = DataPart ((Result (s +* (Initialized Ig))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (s +* (Initialized Ig))) by A21, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) by A8, AMI_1:122 ;
then DataPart (IExec Ig,s) = DataPart ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) by A20, SCMFSA8A:11;
then A23: J is_closed_on (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) by A4, SCMFSA8B:6;
J is_halting_on Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig))) by A2, A4, A22, SCMFSA8B:8;
then A24: (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) is halting by A20, SCMFSA7B:def 8;
A25: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT by SCMFSA6A:34
.= NAT by XBOOLE_1:21 ;
(IExec Ig,s) . (intloc 0 ) = 1 by A1, A3, SCMFSA8C:96;
then B26: (IExec Ig,s) +* (Initialized J) = (IExec Ig,s) +* (J +* (Start-At (insloc 0 ))) by SCMFSA8C:18;
then Result ((IExec Ig,s) +* (Initialized J)), Result ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) equal_outside NAT by A2, A4, A20, A22, SCMFSA8C:101;
then A27: (Result ((IExec Ig,s) +* (Initialized J))) +* (s | NAT ) = (Result ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))) +* (s | NAT ) by A25, FUNCT_7:108;
A28: (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) = (Result (s +* (Initialized Ig))) +* (Initialized J) by A8, AMI_1:122;
A29: IExec (Ig ';' J),s = (Result (s +* (Initialized (Ig ';' J)))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Computation (s +* (Initialized (Ig ';' J))),(LifeSpan (s +* (Initialized (Ig ';' J))))) +* (s | NAT ) by A14, AMI_1:122
.= (Computation (s +* (Initialized (Ig ';' J))),(((LifeSpan (s +* (Initialized Ig))) + 1) + (LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) +* (s | NAT ) by A1, A2, A3, A4, A28, Th6 ;
(IExec Ig,s) | NAT = ((Result (s +* (Initialized Ig))) +* (s | NAT )) | NAT by SCMFSA6B:def 1
.= s | NAT by CARD_3:99 ;
then A30: IExec J,(IExec Ig,s) = (Result ((IExec Ig,s) +* (Initialized J))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Computation ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) +* (s | NAT ) by A24, A27, AMI_1:122 ;
Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
then A31: Ig +* (Start-At (insloc 0 )) c= (s +* (Initialized (Ig ';' J))) +* Ig by SCMFSA6B:8;
( 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 (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 A32: LifeSpan ((s +* (Initialized (Ig ';' J))) +* Ig) = LifeSpan (s +* (Initialized Ig)) by A1, A3, A6, A13, SCMFSA8C:101;
A33: (s +* (Initialized (Ig ';' J))) . (intloc 0 ) = 1 by A5, A13, SCMFSA6A:38;
A34: (s +* (Initialized Ig)) +* (Ig ';' J) = s +* ((Initialized Ig) +* (Ig ';' J)) by FUNCT_4:15
.= s +* (Initialized (Ig ';' J)) by SCMFSA6A:58 ;
DataPart (Computation ((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan (s +* (Initialized Ig)))) = DataPart (Computation (((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J)),(LifeSpan (s +* (Initialized Ig)))) by A18, A19, A31, A32, Th5, SCMFSA6A:39
.= DataPart (Computation ((s +* (Initialized (Ig ';' J))) +* (Ig +* (Ig ';' J))),(LifeSpan (s +* (Initialized Ig)))) by FUNCT_4:15
.= DataPart (Computation ((s +* (Initialized (Ig ';' J))) +* (Ig ';' J)),(LifeSpan (s +* (Initialized Ig)))) by SCMFSA6A:57
.= DataPart (Computation (s +* ((Initialized (Ig ';' J)) +* (Ig ';' J))),(LifeSpan (s +* (Initialized Ig)))) by FUNCT_4:15
.= DataPart (Computation (s +* (Initialized (Ig ';' J))),(LifeSpan (s +* (Initialized Ig)))) by LATTICE2:8, SCMFSA6A:26
.= DataPart (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) by A8, A9, A10, A34, Th5, SCMFSA6A:39 ;
then A35: DataPart ((Computation ((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) = (DataPart (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig))))) +* (DataPart (Initialized J)) by FUNCT_4:75
.= DataPart ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) by FUNCT_4:75 ;
DataPart (IExec Ig,s) = DataPart (IExec Ig,(Initialize s)) by SCMFSA8C:17
.= DataPart (IExec Ig,(s +* (Initialized (Ig ';' J)))) by A1, A3, A5, A13, SCMFSA8C:46 ;
then ( 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;
then A36: ( IC (Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) = insloc (card Ig) & DataPart (Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) = DataPart ((Computation ((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) & ProgramPart (Relocated J,(card Ig)) c= Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1) & (Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) . (intloc 0 ) = 1 ) by A11, A16, A17, A32, A33, Lm1;
A37: ( DataPart (Computation (Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)),(LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) = DataPart (Computation ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) & IC (Computation (Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)),(LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) = (IC (Computation ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) + (card Ig) )

proof

end;

A38: DataPart (IExec (Ig ';' J),s) = DataPart (IExec J,(IExec Ig,s))

proof

A39: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by A25, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
hence DataPart (IExec (Ig ';' J),s) = DataPart (Computation (s +* (Initialized (Ig ';' J))),(((LifeSpan (s +* (Initialized Ig))) + 1) + (LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) by A29, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Computation ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) by A37, AMI_1:51
.= DataPart (IExec J,(IExec Ig,s)) by A30, A39, FUNCT_4:76, SCMFSA_2:127 ;
:: thesis:

end;

A40: IC (Result ((Result (s +* (Initialized Ig))) +* (Initialized J))) = IC (Result ((IExec Ig,s) +* (Initialized J))) by B26, A28, A2, A4, A20, A22, AMI_1:121, SCMFSA8C:101;
A41: IC (IExec (Ig ';' J),s) = IC (Result (s +* (Initialized (Ig ';' J)))) by SCMFSA8A:7
.= IC (Computation (s +* (Initialized (Ig ';' J))),(LifeSpan (s +* (Initialized (Ig ';' J))))) by A14, AMI_1:122
.= IC (Computation (s +* (Initialized (Ig ';' J))),(((LifeSpan (s +* (Initialized Ig))) + 1) + (LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) by A1, A2, A3, A4, A28, Th6
.= (IC (Computation ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) + (card Ig) by A37, AMI_1:51
.= (IC (Result ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) + (card Ig) by A24, AMI_1:122
.= (IC (Result ((Result (s +* (Initialized Ig))) +* (Initialized J)))) + (card Ig) by A8, AMI_1:122
.= (IC (IExec J,(IExec Ig,s))) + (card Ig) by A40, SCMFSA8A:7 ;
A42: dom (IExec (Ig ';' J),s) = the carrier of SCM+FSA by AMI_1:79
.= dom ((IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)))) by AMI_1:79 ;
reconsider l = (IC (IExec J,(IExec Ig,s))) + (card Ig) as Instruction-Location of SCM+FSA ;
A43: dom (Start-At l) = {(IC SCM+FSA )} by FUNCOP_1:19;

now

let x be set ; :: thesis:
assume A44: x in dom (IExec (Ig ';' J),s) ; :: thesis:

per cases by A44, SCMFSA6A:35;

suppose A45: x is Int-Location ; :: thesis:

then A46: (IExec (Ig ';' J),s) . x = (IExec J,(IExec Ig,s)) . x by A38, SCMFSA6A:38;
x <> IC SCM+FSA by A45, SCMFSA_2:81;
then not x in dom (Start-At l) by A43, TARSKI:def 1;
hence (IExec (Ig ';' J),s) . x = ((IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)))) . x by A46, FUNCT_4:12; :: thesis:

end;

suppose A47: x is FinSeq-Location ; :: thesis:

then A48: (IExec (Ig ';' J),s) . x = (IExec J,(IExec Ig,s)) . x by A38, SCMFSA6A:38;
x <> IC SCM+FSA by A47, SCMFSA_2:82;
then not x in dom (Start-At l) by A43, TARSKI:def 1;
hence (IExec (Ig ';' J),s) . x = ((IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)))) . x by A48, FUNCT_4:12; :: thesis:

end;

suppose A49: x = IC SCM+FSA ; :: thesis:

then x in {(IC SCM+FSA )} by TARSKI:def 1;
then A50: x in dom (Start-At l) by FUNCOP_1:19;
thus (IExec (Ig ';' J),s) . x = (Start-At l) . (IC SCM+FSA ) by A41, A49, FUNCOP_1:87
.= ((IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)))) . x by A49, A50, FUNCT_4:14 ; :: thesis:

end;

suppose A51: x is Instruction-Location of SCM+FSA ; :: thesis:

(IExec (Ig ';' J),s) | NAT = s | NAT by A29, CARD_3:99
.= (IExec J,(IExec Ig,s)) | NAT by A30, CARD_3:99 ;
then A52: (IExec (Ig ';' J),s) . x = (IExec J,(IExec Ig,s)) . x by A51, SCMFSA6A:36;
x <> IC SCM+FSA by A51, AMI_1:48;
then not x in dom (Start-At l) by A43, TARSKI:def 1;
hence (IExec (Ig ';' J),s) . x = ((IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)))) . x by A52, FUNCT_4:12; :: thesis:

end;

hence IExec (Ig ';' J),s = (IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig))) by A42, FUNCT_1:9; :: thesis: