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 (insloc 0 );
set D = Int-Locations \/ FinSeq-Locations ;
set Ins = NAT ;
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 Is = Initialize s;
A5: (Initialize s) . (intloc 0 ) = 1 by SCMFSA6C:3;
set s1 = s +* (Initialized Ig);
set m1 = LifeSpan (s +* (Initialized Ig));
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 DataPart (Initialize s) = DataPart (s +* (Initialized Ig)) by SCMFSA8A:11;
then A7: Ig is_closed_on s +* (Initialized Ig) by A3, SCMFSA8B:6;
set s3 = (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J);
A8: s +* (Initialized Ig) is halting by A1, A6, SCMFSA7B:def 8;
then A9: (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) = (Result (s +* (Initialized Ig))) +* (Initialized J) by AMI_1:122;
set s2 = s +* (Initialized (Ig ';' J));
s +* (Initialized (Ig ';' J)) = (Initialize s) +* (Initialized (Ig ';' J)) by SCMFSA8A:8;
then A10: s +* (Initialized (Ig ';' J)) = (Initialize s) +* ((Ig ';' J) +* (Start-At (insloc 0 ))) by A5, SCMFSA8C:18;
then A11: DataPart (Initialize s) = DataPart (s +* (Initialized (Ig ';' J))) by SCMFSA8A:11;
then A12: (s +* (Initialized (Ig ';' J))) . (intloc 0 ) = 1 by A5, SCMFSA6A:38;
A13: DataPart (IExec Ig,s) = DataPart (IExec Ig,(Initialize s)) by SCMFSA8C:17
.= DataPart (IExec Ig,(s +* (Initialized (Ig ';' J)))) by A1, A3, A5, A11, SCMFSA8C:46 ;
then A14: J is_closed_on IExec Ig,(s +* (Initialized (Ig ';' J))) by A2, A4, SCMFSA8B:8;
A15: Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
Start-At (insloc 0 ) c= Initialized Ig by FUNCT_4:26;
then Start-At (insloc 0 ) c= (s +* (Initialized (Ig ';' J))) +* Ig by A15, 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 A16: LifeSpan ((s +* (Initialized (Ig ';' J))) +* Ig) = LifeSpan (s +* (Initialized Ig)) by A1, A3, A6, A11, SCMFSA8C:101;
set JAt = J +* (Start-At (insloc 0 ));
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A17: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
(Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) . (intloc 0 ) = 1 by A3, A5, A6, SCMFSA8C:97;
then A18: (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;
set m3 = LifeSpan ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J));
set ps = s | NAT ;
A19: 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 ;
Ig ';' J is_halting_on Initialize s by A1, A2, A3, A4, Th4;
then A20: s +* (Initialized (Ig ';' J)) is halting by A10, SCMFSA7B:def 8;
A21: 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 A20, 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, A9, Th6 ;
A22: DataPart (IExec Ig,s) = DataPart ((Result (s +* (Initialized Ig))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (s +* (Initialized Ig))) by A17, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) by A8, AMI_1:122 ;
then J is_halting_on Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig))) by A2, A4, SCMFSA8B:8;
then A23: (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) is halting by A18, SCMFSA7B:def 8;
set IEJIs = IExec J,(IExec Ig,s);
set IAt = Ig +* (Start-At (insloc 0 ));
A24: Ig +* (Start-At (insloc 0 )) c= s +* (Initialized Ig) by FUNCT_4:26, SCMFSA6B:8;
A25: J +* (Start-At (insloc 0 )) c= (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
DataPart (IExec Ig,s) = DataPart ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) by A18, A22, SCMFSA8A:11;
then A26: J is_closed_on (Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) by A4, SCMFSA8B:6;
A27: Initialized (Ig ';' J) c= s +* (Initialized (Ig ';' J)) by FUNCT_4:26;
(IExec Ig,s) . (intloc 0 ) = 1 by A1, A3, SCMFSA8C:96;
then A28: (IExec Ig,s) +* (Initialized J) = (IExec Ig,s) +* (J +* (Start-At (insloc 0 ))) by SCMFSA8C:18;
then A29: IC (Result ((Result (s +* (Initialized Ig))) +* (Initialized J))) = IC (Result ((IExec Ig,s) +* (Initialized J))) by A2, A4, A18, A22, A9, AMI_1:121, SCMFSA8C:101;
Result ((IExec Ig,s) +* (Initialized J)), Result ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) equal_outside NAT by A2, A4, A18, A22, A28, SCMFSA8C:101;
then A30: (Result ((IExec Ig,s) +* (Initialized J))) +* (s | NAT ) = (Result ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))) +* (s | NAT ) by A19, FUNCT_7:108;
(IExec Ig,s) | NAT = ((Result (s +* (Initialized Ig))) +* (s | NAT )) | NAT by SCMFSA6B:def 1
.= s | NAT by CARD_3:99 ;
then A31: 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 A23, A30, AMI_1:122 ;
A32: Ig is_halting_on s +* (Initialized (Ig ';' J)) by A1, A3, A11, SCMFSA8B:8;
reconsider l = (IC (IExec J,(IExec Ig,s))) + (card Ig) as Instruction-Location of SCM+FSA ;
A33: (s +* (Initialized Ig)) +* (Ig ';' J) = s +* ((Initialized Ig) +* (Ig ';' J)) by FUNCT_4:15
.= s +* (Initialized (Ig ';' J)) by SCMFSA6A:58 ;
Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
then A34: Ig +* (Start-At (insloc 0 )) c= (s +* (Initialized (Ig ';' J))) +* Ig by SCMFSA6B:8;
DataPart (s +* (Initialized (Ig ';' J))) = DataPart ((s +* (Initialized (Ig ';' J))) +* Ig) by SCMFSA8C:34;
then A35: Ig is_closed_on (s +* (Initialized (Ig ';' J))) +* Ig by A3, A11, SCMFSA8B:6;
A36: dom (Start-At l) = {(IC SCM+FSA )} by FUNCOP_1:19;
Start-At (insloc 0 ) c= Initialized (Ig ';' J) by SCMFSA6B:4;
then Start-At (insloc 0 ) c= s +* (Initialized (Ig ';' J)) by A27, XBOOLE_1:1;
then (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 ;
then (s +* (Initialized (Ig ';' J))) +* Ig is halting by A32, SCMFSA7B:def 8;
then 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 A35, A34, A16, 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, A7, A24, A33, Th5, SCMFSA6A:39 ;
then A37: 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 ;
A38: Ig is_closed_on s +* (Initialized (Ig ';' J)) by A3, A11, SCMFSA8B:6;
A39: J is_halting_on IExec Ig,(s +* (Initialized (Ig ';' J))) by A2, A4, A13, SCMFSA8B:8;
then A40: DataPart (Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) = DataPart ((Computation ((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) by A27, A38, A32, A16, A12, A14, Lm1;
A41: ProgramPart (Relocated J,(card Ig)) c= Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1) by A27, A38, A32, A16, A12, A14, A39, Lm1;
A42: IC (Computation (s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) = insloc (card Ig) by A27, A38, A32, A16, A12, A14, A39, Lm1;
then A43: 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)))) by A26, A37, A40, A41, A25, SCMFSA8C:42;
A44: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by A19, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A45: 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 A21, 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 A43, AMI_1:51
.= DataPart (IExec J,(IExec Ig,s)) by A31, A44, FUNCT_4:76, SCMFSA_2:127 ;
A46: 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) by A26, A37, A42, A40, A41, A25, SCMFSA8C:42;
A47: 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 A20, 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, A9, 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 A46, AMI_1:51
.= (IC (Result ((Computation (s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) + (card Ig) by A23, 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 A29, SCMFSA8A:7 ;

A48: now

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

per cases by A49, SCMFSA6A:35;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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 ;
hence IExec (Ig ';' J),s = (IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig))) by A48, FUNCT_1:9; :: thesis: