let s be State of SCM+FSA ; :: thesis:
let I be InitHalting keepInt0_1 Program of SCM+FSA ; :: thesis:
let J be InitHalting Program of SCM+FSA ; :: thesis:
set ps = s | NAT ;
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (I ';' J));
set s3 = (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J);
set m1 = LifeSpan (s +* (Initialized I));
set m3 = LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J));
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
A1: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
A2: s +* (Initialized I) is halting by Th5, FUNCT_4:26;
A3: Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
s +* (Initialized (I ';' J)) = s +* ((I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= (s +* (I ';' J)) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15 ;
then A4: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
(s +* (Initialized (I ';' J))) +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) = ((s +* (Initialized (I ';' J))) +* I) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= ((s +* (Initialized (I ';' J))) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* I by Th19
.= (s +* (Initialized (I ';' J))) +* I by A4, FUNCT_4:79 ;
then I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26;
then Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:15;
then A5: (s +* (Initialized (I ';' J))) +* I is halting by Th5;
A6: Initialized J c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) by FUNCT_4:26;
A7: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT by AMI_1:79, SCMFSA_2:8
.= NAT by XBOOLE_1:21 ;
A8: (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J),((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized J) equal_outside dom (s | NAT ) by FUNCT_7:31, FUNCT_7:106;
then A9: ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized J),(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) equal_outside dom (s | NAT ) by FUNCT_7:28;
Result ((IExec I,s) +* (Initialized J)), Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) equal_outside NAT

proof

A10: Initialized J c= (IExec I,s) +* (Initialized J) by FUNCT_4:26;
A11: Initialized J c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) by FUNCT_4:26;
IExec I,s = (Result (s +* (Initialized I))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT ) by A1, Th5, AMI_1:122 ;
hence Result ((IExec I,s) +* (Initialized J)), Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) equal_outside NAT by A7, A9, A10, A11, Th15; :: thesis:

end;

proof

end;

A23: DataPart (IExec (I ';' J),s) = DataPart (IExec J,(IExec I,s))

proof

A24: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by A7, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
hence DataPart (IExec (I ';' J),s) = DataPart (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) by A14, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) by A20, AMI_1:51
.= DataPart (IExec J,(IExec I,s)) by A15, A24, FUNCT_4:76, SCMFSA_2:127 ;
:: thesis:

end;

A25: IExec I,s = (Result (s +* (Initialized I))) +* (s | NAT ) by SCMFSA6B:def 1;
A26: Result (s +* (Initialized I)) = Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))) by A1, Th5, AMI_1:122;
A27: Initialized J c= (Result (s +* (Initialized I))) +* (Initialized J) by FUNCT_4:26;
Initialized J c= (IExec I,s) +* (Initialized J) by FUNCT_4:26;
then A28: IC (Result ((Result (s +* (Initialized I))) +* (Initialized J))) = IC (Result ((IExec I,s) +* (Initialized J))) by A7, A8, A25, A26, A27, Th15, AMI_1:121;
A29: IC (IExec (I ';' J),s) = IC (Result (s +* (Initialized (I ';' J)))) by SCMFSA8A:7
.= IC (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized (I ';' J))))) by A3, Th5, AMI_1:122
.= IC (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) by A13, Th28
.= (IC (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) + (card I) by A20, AMI_1:51
.= (IC (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) + (card I) by A6, Th5, AMI_1:122
.= (IC (Result ((Result (s +* (Initialized I))) +* (Initialized J)))) + (card I) by A1, Th5, AMI_1:122
.= (IC (IExec J,(IExec I,s))) + (card I) by A28, SCMFSA8A:7 ;

hereby :: thesis:

A30: dom (IExec (I ';' J),s) = the carrier of SCM+FSA by AMI_1:79
.= dom ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) by AMI_1:79 ;
reconsider l = (IC (IExec J,(IExec I,s))) + (card I) as Instruction-Location of SCM+FSA ;
A31: dom (Start-At l) = {(IC SCM+FSA )} by FUNCOP_1:19;

now

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

per cases by A32, SCMFSA6A:35;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

end;