let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s,P holds
DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,s))
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 J is_pseudo-closed_on ss,P holds
DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,ss))
set D = Data-Locations ;
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 J is_pseudo-closed_on ss,P holds
DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,ss))
let a be read-write Int-Location; :: thesis: ( ss . (intloc 0) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss,P implies DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,ss)) )
set J0 = Directed J;
set s = Initialized ss;
set s0 = Initialized (Initialized ss);
set J9 = J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)));
set s00 = Initialize (Initialized ss);
set P00 = P +* (Directed J);
set s3 = Initialize (Initialized ss);
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1);
set s5 = Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2);
set i = a >0_goto ((card J) + 3);
A1: if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:25;
A2: Directed J c= P +* (Directed J) by FUNCT_4:25;
assume A3: ss . (intloc 0) = 1 ; :: thesis: ( not ss . a <= 0 or not Directed J is_pseudo-closed_on ss,P or DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,ss)) )
set s1 = Initialize (Initialized ss);
set P1 = P +* (J ";" (Stop SCM+FSA));
assume ss . a <= 0 ; :: thesis: ( not Directed J is_pseudo-closed_on ss,P or DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,ss)) )
then A4: (Initialized (Initialized ss)) . a <= 0 by SCMFSA_M:37;
A5: 0 in dom (if>0 (a,I,J)) by Th25;
A6: (P +* (if>0 (a,I,J))) . 0 = (if>0 (a,I,J)) . 0 by A5, FUNCT_4:13
.= a >0_goto ((card J) + 3) by Th26 ;
(Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized (Initialized ss)) by MEMSTR_0:44;
then A7: (Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized ss) ;
A8: (Directed J) ";" (Stop SCM+FSA) = J ";" (Stop SCM+FSA) by SCMFSA8A:25;
A9: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A10: IC (Initialize (Initialized ss)) = IC (Initialize (Initialized ss))
.= IC (Start-At (0,SCM+FSA)) by A9, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) by SCMFSA8B:def 2;
then if>0 (a,I,J) = (((Macro (a >0_goto ((card J) + 3))) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25;
then if>0 (a,I,J) = ((Macro (a >0_goto ((card J) + 3))) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25;
then A11: if>0 (a,I,J) = (Macro (a >0_goto ((card J) + 3))) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) by SCMFSA6A:25;
card (Macro (a >0_goto ((card J) + 3))) = 2 by COMPOS_1:56;
then A12: Reloc ((J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))),2) c= if>0 (a,I,J) by A11, FUNCT_4:25;
A13: Reloc ((Directed J),2) c= Reloc ((J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))),2) by COMPOS_1:44, SCMFSA6A:16;
Reloc ((Directed J),2) c= if>0 (a,I,J) by A12, A13, XBOOLE_1:1;
then A14: Reloc ((Directed J),2) c= P +* (if>0 (a,I,J)) by A1, XBOOLE_1:1;
A15: Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(0 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),0))) by EXTPRO_1:3
.= Following ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)))
.= Exec ((a >0_goto ((card J) + 3)),(Initialize (Initialized ss))) by A10, A6, PBOOLE:143 ;
assume Directed J is_pseudo-closed_on ss,P ; :: thesis: DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,ss))
then A16: Directed J is_pseudo-closed_on Initialized ss,P by A3, Th24;
then J ";" (Stop SCM+FSA) is_halting_on Initialized ss,P by Th29;
then A17: P +* (J ";" (Stop SCM+FSA)) halts_on Initialize (Initialized ss) by SCMFSA7B:def 7;
DataPart (Initialized ss) = DataPart (Initialize (Initialized ss)) by MEMSTR_0:79;
then A18: Directed J is_pseudo-closed_on Initialize (Initialized ss),P +* (Directed J) by A16, Th23;
(Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized (Initialized ss)) by MEMSTR_0:44;
then A19: (Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized ss) ;
A20: Directed (Directed J) = Directed J by SCMFSA6A:22;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:12
.= ((card J) + 2) + ((card I) + 2) ;
then ((card J) + 2) + 0 < card (if>0 (a,I,J)) by XREAL_1:8;
then A21: (card J) + 2 in dom (if>0 (a,I,J)) by AFINSQ_1:66;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:12
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if>0 (a,I,J)) by NAT_1:13;
then A22: ((card I) + (card J)) + 3 in dom (if>0 (a,I,J)) by AFINSQ_1:66;
set s9 = Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2));
LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize (Initialized ss))) = pseudo-LifeSpan ((Initialized ss),P,(Directed J)) by A16, Th29;
then A23: DataPart (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialized ss),P,(Directed J))))) = DataPart (Comput ((P +* (J ";" (Stop SCM+FSA))),(Initialize (Initialized ss)),(LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize (Initialized ss)))))) by A16, A20, A8, Th29;
A24: 1 in dom (if>0 (a,I,J)) by Th25;
A25: a <> IC by SCMFSA_2:56;
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then not a in dom (Start-At (0,SCM+FSA)) by A25, TARSKI:def 1;
then not a in dom (Start-At (0,SCM+FSA)) ;
then (Initialize (Initialized ss)) . a = (Initialized (Initialized ss)) . a by FUNCT_4:11;
then A26: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)) = succ (IC (Initialize (Initialized ss))) by A4, A15, SCMFSA_2:71
.= 0 + 1 by A10 ;
A27: (P +* (if>0 (a,I,J))) . 1 = (if>0 (a,I,J)) . 1 by A24, FUNCT_4:13
.= goto 2 by Th26 ;
A28: Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(1 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1))) by A26, A27, PBOOLE:143 ;
then A29: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) = 2 by SCMFSA_2:69;

A30: now :: thesis: for f being FinSeq-Location holds (Initialize (Initialized ss)) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . f

let f be FinSeq-Location ; :: thesis: (Initialize (Initialized ss)) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . f
thus (Initialize (Initialized ss)) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)) . f by A15, SCMFSA_2:71
.= (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . f by A28, SCMFSA_2:69 ; :: thesis: verum

end;

now :: thesis: for a being Int-Location holds (Initialize (Initialized ss)) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . a

let a be Int-Location; :: thesis: (Initialize (Initialized ss)) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . a
thus (Initialize (Initialized ss)) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)) . a by A15, SCMFSA_2:71
.= (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . a by A28, SCMFSA_2:69 ; :: thesis: verum

end;

then A31: DataPart (Initialize (Initialized ss)) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) by A30, SCMFSA_M:2;
A32: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))))) by EXTPRO_1:4
.= (IC (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J)))))) + 2 by A18, A29, A31, Th22, A2, A14
.= (IC (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialized ss),P,(Directed J)))))) + 2 by A16, Th21
.= (card (Directed J)) + 2 by A16, SCMFSA8A:def 4
.= (card J) + 2 by SCMFSA8A:20 ;
then A33: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2)))) = (P +* (if>0 (a,I,J))) . ((card J) + 2) by PBOOLE:143
.= (if>0 (a,I,J)) . ((card J) + 2) by A21, A1, GRFUNC_1:2
.= goto (((card I) + (card J)) + 3) by Th35 ;
IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2) + 1))) = IC (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))))) by EXTPRO_1:3
.= ((card I) + (card J)) + 3 by A33, SCMFSA_2:69 ;
then A34: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2) + 1)))) = (P +* (if>0 (a,I,J))) . (((card I) + (card J)) + 3) by PBOOLE:143
.= (if>0 (a,I,J)) . (((card I) + (card J)) + 3) by A22, A1, GRFUNC_1:2
.= halt SCM+FSA by Th33 ;
then A35: P +* (if>0 (a,I,J)) halts_on Initialize (Initialized ss) by EXTPRO_1:29;
A36: CurInstr ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss))) = a >0_goto ((card J) + 3) by A10, A6, PBOOLE:143;

now :: thesis: for k being Element of NAT st CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) = halt SCM+FSA holds
(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k

A37: 0 + 2 < ((card I) + (card J)) + 3 by XREAL_1:8;
then A38: 2 in dom (if>0 (a,I,J)) by Th28;
A39: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2))) = (P +* (if>0 (a,I,J))) . 2 by A29, PBOOLE:143
.= (if>0 (a,I,J)) . 2 by A38, A1, GRFUNC_1:2 ;
let k be Element of NAT ; :: thesis: ( CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) = halt SCM+FSA implies (pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k )
assume A40: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) = halt SCM+FSA ; :: thesis: (pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k
A41: k <> 0 by A40, A36, EXTPRO_1:2;
A42: k <> 1 by A26, A27, A40, PBOOLE:143;
2 <> k by A40, A37, Th28, A39;
then 2 < k by A41, A42, NAT_1:26;
then consider k2 being Nat such that
A43: 2 + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 12;
reconsider n = IC (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),k2)) as Element of NAT ;
assume not (pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k ; :: thesis: contradiction
then k < ((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 1) + 2 ;
then k2 < (pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 1 by A43, XREAL_1:6;
then A44: k2 <= pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J)) by NAT_1:13;
then A45: k2 <= pseudo-LifeSpan ((Initialized ss),P,(Directed J)) by A16, Th21;

A46: now :: thesis: n + 2 < ((card I) + (card J)) + 3

per cases ( k2 = pseudo-LifeSpan ((Initialized ss),P,(Directed J)) or k2 < pseudo-LifeSpan ((Initialized ss),P,(Directed J)) ) by A45, XXREAL_0:1;

suppose A47: k2 = pseudo-LifeSpan ((Initialized ss),P,(Directed J)) ; :: thesis: n + 2 < ((card I) + (card J)) + 3

((card I) + (card J)) + (2 + 1) = (((card J) + 2) + 1) + (card I) ;
then A48: ((card J) + 2) + 1 <= ((card I) + (card J)) + 3 by NAT_1:11;
IC (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),k2)) = card (Directed J) by A16, A47, SCMFSA8A:def 4;
then n = card J by SCMFSA8A:20;
hence n + 2 < ((card I) + (card J)) + 3 by A48, NAT_1:13; :: thesis: verum

end;

suppose k2 < pseudo-LifeSpan ((Initialized ss),P,(Directed J)) ; :: thesis: n + 2 < ((card I) + (card J)) + 3

then n in dom (Directed J) by A16, SCMFSA8A:17;
then n < card (Directed J) by AFINSQ_1:66;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:6;
then A49: n + 2 < (card J) + 2 by SCMFSA8A:20;
((card I) + (card J)) + (1 + 2) = ((card J) + 2) + ((card I) + 1) ;
then (card J) + 2 <= ((card I) + (card J)) + 3 by NAT_1:11;
hence n + 2 < ((card I) + (card J)) + 3 by A49, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then A50: n + 2 in dom (if>0 (a,I,J)) by Th28;
A51: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k)) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)),k2)) by A43, EXTPRO_1:4
.= n + 2 by A18, A29, A31, A44, Th22, A2, A14 ;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) by PBOOLE:143
.= (if>0 (a,I,J)) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) by A51, A50, A1, GRFUNC_1:2 ;
hence contradiction by A40, A51, A46, Th28; :: thesis: verum

end;

then A52: LifeSpan ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss))) = ((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2) + 1 by A34, A35, EXTPRO_1:def 15;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2)))) = (P +* (if>0 (a,I,J))) . ((card J) + 2) by A32, PBOOLE:143
.= (if>0 (a,I,J)) . ((card J) + 2) by A21, A1, GRFUNC_1:2
.= goto (((card I) + (card J)) + 3) by Th35 ;
then InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))))) = 6 by SCMFSA_2:23;
then InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))))) in {0,6,7,8} by ENUMSET1:def 2;
then A53: DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))) = DataPart (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))))) by Th12;
A54: DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))))) by EXTPRO_1:4
.= DataPart (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))))) by A18, A29, A31, Th22, A2, A14 ;
thus DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((if>0 (a,I,J)),P,(Initialized ss)))
.= DataPart (Result ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)))) by A7
.= DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(LifeSpan ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)))))) by A35, EXTPRO_1:23
.= DataPart (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))))) by A52, EXTPRO_1:3
.= DataPart (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialized ss),P,(Directed J))))) by A16, A54, A53, Th21
.= DataPart (Result ((P +* (J ";" (Stop SCM+FSA))),(Initialize (Initialized ss)))) by A17, A23, EXTPRO_1:23
.= DataPart (IExec ((J ";" (Stop SCM+FSA)),P,(Initialized ss))) by A19
.= DataPart (IExec ((J ";" (Stop SCM+FSA)),P,ss)) ; :: thesis: verum