set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
let ss be State of SCM+FSA ; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location st ss . (intloc 0 ) = 1 & ss . a = 0 & Directed I is_pseudo-closed_on ss holds
DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss)
let I, J be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st ss . (intloc 0 ) = 1 & ss . a = 0 & Directed I is_pseudo-closed_on ss holds
DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss)
let a be read-write Int-Location ; :: thesis: ( ss . (intloc 0 ) = 1 & ss . a = 0 & Directed I is_pseudo-closed_on ss implies DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss) )
set I0 = Directed I;
set s = Initialize ss;
set I1 = I ';' (Stop SCM+FSA );
set s00 = (Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )));
set s3 = (Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )));
set s4 = Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1;
set i = a =0_goto (insloc ((card J) + 3));
assume A1: ss . (intloc 0 ) = 1 ; :: thesis: ( not ss . a = 0 or not Directed I is_pseudo-closed_on ss or DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss) )
assume ss . a = 0 ; :: thesis: ( not Directed I is_pseudo-closed_on ss or DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss) )
then A2: (Initialize ss) . a = 0 by SCMFSA6C:3;
assume Directed I is_pseudo-closed_on ss ; :: thesis: DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss)
then A3: Directed I is_pseudo-closed_on Initialize ss by A1, Th53;
A4: if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1;
A5: (Directed I) +* (Start-At (insloc 0 )) c= (Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
DataPart (Initialize ss) = DataPart ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) by SCMFSA8A:11;
then A6: Directed I is_pseudo-closed_on (Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 ))) by A3, Th52;
A7: insloc 0 in dom (if=0 a,I,J) by Th54;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A8: dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A9: IC SCM+FSA in dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by SF_MASTR:65;

A10: now

thus IC ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = ((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A9, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ; :: thesis: verum

end;

A11: now

thus ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A7, A8, FUNCT_4:14
.= (if=0 a,I,J) . (insloc 0 ) by A7, SCMFSA6B:7
.= a =0_goto (insloc ((card J) + 3)) by Th55 ; :: thesis: verum

end;

A12: now

thus Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(0 + 1) = Following (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 ) by AMI_1:14
.= Following ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= Exec (a =0_goto (insloc ((card J) + 3))),((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by A10, A11 ; :: thesis: verum

end;

A13: now

thus card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = (card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1)))) by SCMFSA6A:61
.= (card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1 by SCMFSA8A:29
.= ((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1 by SCMFSA6A:61
.= ((card J) + 2) + 1 by SCMFSA7B:6
.= (card J) + (2 + 1) ; :: thesis: verum

end;

( not a in dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) & a in dom (Initialize ss) ) by SCMFSA6B:12, SCMFSA_2:66;
then A14: ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a = 0 by A2, FUNCT_4:12;
A15: (if=0 a,I,J) +* (Start-At (insloc 0 )) c= (Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A16: if=0 a,I,J c= (Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by A15, XBOOLE_1:1;
if=0 a,I,J = (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )) by A4, SCMFSA6A:67;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if=0 a,I,J by A13, FUNCT_4:26;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= (Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by A16, XBOOLE_1:1;
then ProgramPart [(ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)))] c= Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1 by AMI_1:99;
then A17: ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1 by AMI_1:105;
ProgramPart (Relocated (Directed I),((card J) + 3)) c= ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) by Th12, SCMFSA6A:55;
then A18: ProgramPart (Relocated (Directed I),((card J) + 3)) c= Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1 by A17, XBOOLE_1:1;
A19: IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) = insloc ((card J) + 3) by A12, A14, SCMFSA_2:96;
A20: DataPart ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by SCMFSA6A:39, SCMFSA8A:14;

A21: now

let a be Int-Location ; :: thesis: ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . a = (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a
thus ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . a = ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a by A20, SCMFSA6A:38
.= (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a by A12, SCMFSA_2:96 ; :: thesis: verum

end;

now

let f be FinSeq-Location ; :: thesis: ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . f = (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f
thus ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . f = ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . f by A20, SCMFSA6A:38
.= (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f by A12, SCMFSA_2:96 ; :: thesis: verum

end;

then A22: DataPart ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) by A21, SCMFSA6A:38;
A23: if=0 a,I,J c= (Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26, SCMFSA6B:5;

now

thus card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ; :: thesis: verum

end;

then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by NAT_1:13;
then A24: insloc (((card I) + (card J)) + 3) in dom (if=0 a,I,J) by SCMFSA6A:15;

now

thus IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) = IC (Computation (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I))) by AMI_1:51
.= (IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)))) + ((card J) + 3) by A5, A6, A18, A19, A22, Th51
.= (IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize ss),(Directed I)))) + ((card J) + 3) by A3, Th50
.= (insloc (card (ProgramPart (Directed I)))) + ((card J) + 3) by A3, SCMFSA8A:def 5
.= (insloc (card (Directed I))) + ((card J) + 3) by AMI_1:105
.= insloc ((card I) + ((card J) + 3)) by SCMFSA8A:34
.= insloc (((card I) + (card J)) + 3) ; :: thesis: verum

end;

then A25: CurInstr (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) = ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc (((card I) + (card J)) + 3)) by AMI_1:54
.= (if=0 a,I,J) . (insloc (((card I) + (card J)) + 3)) by A23, A24, GRFUNC_1:8
.= halt SCM+FSA by Th61 ;
then A26: (Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;

now

let k be Element of NAT ; :: thesis: ( CurInstr (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA implies (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k )
assume A27: CurInstr (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA ; :: thesis: (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k
assume not (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k ; :: thesis: contradiction
then A28: k <= pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) by NAT_1:13;
A29: insloc 0 in dom (if=0 a,I,J) by Th54;
A30: ( InsCode (halt SCM+FSA ) = 0 & InsCode (a =0_goto (insloc ((card J) + 3))) = 7 ) by SCMFSA_2:48, SCMFSA_2:124;
CurInstr (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 ) = CurInstr ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) by Th31
.= (if=0 a,I,J) . (insloc 0 ) by A29, Th26
.= a =0_goto (insloc ((card J) + 3)) by Th55 ;
then consider k1 being Nat such that
A31: k1 + 1 = k by A27, A30, NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
k1 < k by A31, XREAL_1:31;
then A32: k1 < pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) by A28, XXREAL_0:2;
A33: IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = IC (Computation (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),k1) by A31, AMI_1:51
.= (IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),k1)) + ((card J) + 3) by A5, A6, A18, A19, A22, A32, Th51 ;
reconsider n = IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),k1) as Element of NAT by ORDINAL1:def 13;
k1 < pseudo-LifeSpan (Initialize ss),(Directed I) by A3, A32, Th50;
then insloc n in dom (Directed I) by A3, SCMFSA8A:31;
then n < card (Directed I) by SCMFSA6A:15;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:8;
then A35: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by XREAL_1:31;
then n + ((card J) + 3) < card (if=0 a,I,J) by A35, XXREAL_0:2;
then A36: IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A33, SCMFSA6A:15;
set J1 = (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I;
card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) = (card (((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1) + (card I) by SCMFSA6A:61
.= ((2 + (card J)) + 1) + (card I) by SCMFSA7B:6
.= ((card I) + (card J)) + 3 ;
then IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) by A33, A35, SCMFSA6A:15;
then A37: IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by FUNCT_4:105;
Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) c= if=0 a,I,J by A4, SCMFSA6A:55;
then A38: (if=0 a,I,J) . (IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) = (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by A37, GRFUNC_1:8;
A39: (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) in rng (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by A37, FUNCT_1:def 5;
CurInstr (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by AMI_1:54
.= (if=0 a,I,J) . (IC (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by A36, Th26 ;
hence contradiction by A27, A38, A39, AMI_1:def 52; :: thesis: verum

end;

then A40: LifeSpan ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 by A25, A26, AMI_1:def 46;
set s1 = (Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
( (Initialize ss) +* (Initialized (if=0 a,I,J)) = (Initialize (Initialize ss)) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) & (Initialize ss) +* (Initialized (I ';' (Stop SCM+FSA ))) = (Initialize (Initialize ss)) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) ) by SCMFSA8A:13;
then A41: ( (Initialize ss) +* (Initialized (if=0 a,I,J)) = (Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) & (Initialize ss) +* (Initialized (I ';' (Stop SCM+FSA ))) = (Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) ) by Th15;
A42: ( I ';' (Stop SCM+FSA ) is_halting_on Initialize ss & LifeSpan ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan (Initialize ss),(Directed I) ) by A3, Th58;
then A43: (Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
A44: Directed (Directed I) = Directed I by SCMFSA6A:63;
( (Directed I) ';' (Stop SCM+FSA ) = I ';' (Stop SCM+FSA ) & Directed (Directed I) is_pseudo-closed_on Initialize ss ) by A3, SCMFSA6A:63, SCMFSA8A:41;
then A45: DataPart (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize ss),(Directed I))) = DataPart (Computation ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize ss),(Directed I))) by A44, Th58;
thus DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (if=0 a,I,J),(Initialize ss)) by Th17
.= DataPart ((Result ((Initialize ss) +* (Initialized (if=0 a,I,J)))) +* ((Initialize ss) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))) by A41, Th35
.= DataPart (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))))) by A26, AMI_1:122
.= DataPart (Computation (Computation ((Initialize ss) +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I))) by A40, AMI_1:51
.= DataPart (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I))) by A5, A6, A18, A19, A22, Th51
.= DataPart (Computation ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))) by A3, A42, A45, Th50
.= DataPart (Result ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) by A43, AMI_1:122
.= DataPart ((Result ((Initialize ss) +* (Initialized (I ';' (Stop SCM+FSA ))))) +* ((Initialize ss) | NAT )) by A41, Th35
.= DataPart (IExec (I ';' (Stop SCM+FSA )),(Initialize ss)) by SCMFSA6B:def 1
.= DataPart (IExec (I ';' (Stop SCM+FSA )),ss) by Th17 ; :: thesis: verum