let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; 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 I is_pseudo-closed_on s,P holds
DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,s))
let ss be State of SCM+FSA; 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,P holds
DataPart (IExec ((if=0 (a,I,J)),P,ss)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,ss))
set A = NAT ;
set D = Data-Locations SCM+FSA;
let I, J be 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,P holds
DataPart (IExec ((if=0 (a,I,J)),P,ss)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,ss))
let a be read-write Int-Location ; ( ss . (intloc 0) = 1 & ss . a = 0 & Directed I is_pseudo-closed_on ss,P implies DataPart (IExec ((if=0 (a,I,J)),P,ss)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,ss)) )
set I0 = Directed I;
set s = Initialized ss;
set I1 = I ';' (Stop SCM+FSA);
set s00 = (Initialized ss) +* (Initialize (Directed I));
set P00 = P +* (Directed I);
set s3 = (Initialized ss) +* (Initialize (if=0 (a,I,J)));
set P3 = P +* (if=0 (a,I,J));
A1:
if=0 (a,I,J) c= P +* (if=0 (a,I,J))
by FUNCT_4:26;
set s4 = Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1);
set i = a =0_goto ((card J) + 3);
A2:
Directed I c= P +* (Directed I)
by FUNCT_4:26;
assume A3:
ss . (intloc 0) = 1
; ( not ss . a = 0 or not Directed I is_pseudo-closed_on ss,P or DataPart (IExec ((if=0 (a,I,J)),P,ss)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,ss)) )
set s1 = (Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA)));
set P1 = P +* (I ';' (Stop SCM+FSA));
A4:
ProgramPart (I ';' (Stop SCM+FSA)) = I ';' (Stop SCM+FSA)
by RELAT_1:209;
assume
ss . a = 0
; ( not Directed I is_pseudo-closed_on ss,P or DataPart (IExec ((if=0 (a,I,J)),P,ss)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,ss)) )
then A5:
(Initialized ss) . a = 0
by SCMFSA6C:3;
IC in dom (Initialize (if=0 (a,I,J)))
by COMPOS_1:141;
then A6: IC ((Initialized ss) +* (Initialize (if=0 (a,I,J)))) =
IC (Initialize (if=0 (a,I,J)))
by FUNCT_4:14
.=
0
by COMPOS_1:142
;
A7:
0 in dom (if=0 (a,I,J))
by Th54;
A8: (P +* (if=0 (a,I,J))) . 0 =
(if=0 (a,I,J)) . 0
by A7, FUNCT_4:14
.=
(if=0 (a,I,J)) . 0
.=
a =0_goto ((card J) + 3)
by Th55
;
A9:
(P +* (if=0 (a,I,J))) /. (IC ((Initialized ss) +* (Initialize (if=0 (a,I,J))))) = (P +* (if=0 (a,I,J))) . (IC ((Initialized ss) +* (Initialize (if=0 (a,I,J)))))
by PBOOLE:158;
A10: Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),(0 + 1)) =
Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),0)))
by EXTPRO_1:4
.=
Following ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))))
by EXTPRO_1:3
.=
Exec ((a =0_goto ((card J) + 3)),((Initialized ss) +* (Initialize (if=0 (a,I,J)))))
by A6, A8, A9
;
not a in dom (Initialize (if=0 (a,I,J)))
by SCMFSA6B:12;
then
((Initialized ss) +* (Initialize (if=0 (a,I,J)))) . a = 0
by A5, FUNCT_4:12;
then A11:
IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)) = (card J) + 3
by A10, SCMFSA_2:96;
assume
Directed I is_pseudo-closed_on ss,P
; DataPart (IExec ((if=0 (a,I,J)),P,ss)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,ss))
then A12:
Directed I is_pseudo-closed_on Initialized ss,P
by A3, Th53;
then A13:
LifeSpan ((P +* (I ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA))))) = pseudo-LifeSpan ((Initialized ss),P,(Directed I))
by Th58;
DataPart (Initialized ss) = DataPart ((Initialized ss) +* (Initialize (Directed I)))
by SCMFSA8A:11;
then A14:
Directed I is_pseudo-closed_on (Initialized ss) +* (Initialize (Directed I)),P +* (Directed I)
by A12, Th52;
A15:
DataPart ((Initialized ss) +* (Initialize (Directed I))) = DataPart ((Initialized ss) +* (Initialize (if=0 (a,I,J))))
by COMPOS_1:138, SCMFSA8A:14;
A16:
now let f be
FinSeq-Location ;
((Initialized ss) +* (Initialize (Directed I))) . f = (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)) . fthus ((Initialized ss) +* (Initialize (Directed I))) . f =
((Initialized ss) +* (Initialize (if=0 (a,I,J)))) . f
by A15, SCMFSA6A:38
.=
(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)) . f
by A10, SCMFSA_2:96
;
verum end;
now let a be
Int-Location ;
((Initialized ss) +* (Initialize (Directed I))) . a = (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)) . athus ((Initialized ss) +* (Initialize (Directed I))) . a =
((Initialized ss) +* (Initialize (if=0 (a,I,J)))) . a
by A15, SCMFSA6A:38
.=
(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)) . a
by A10, SCMFSA_2:96
;
verum end;
then A17:
DataPart ((Initialized ss) +* (Initialize (Directed I))) = DataPart (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1))
by A16, SCMFSA6A:38;
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 NAT_1:13;
then A18:
((card I) + (card J)) + 3 in dom (if=0 (a,I,J))
by AFINSQ_1:70;
A19: card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) =
(card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))
by SCMFSA6A:61
.=
(card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1
by SCMFSA8A:29
.=
((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1
by SCMFSA6A:61
.=
((card J) + 2) + 1
by COMPOS_1:150
.=
(card J) + (2 + 1)
;
(Initialized ss) +* (Initialized (if=0 (a,I,J))) = (Initialized (Initialized ss)) +* (Initialize (if=0 (a,I,J)))
by SCMFSA8A:13;
then A20:
(Initialized ss) +* (Initialized (if=0 (a,I,J))) = (Initialized ss) +* (Initialize (if=0 (a,I,J)))
by Th15;
A21:
if=0 (a,I,J) c= Initialize (if=0 (a,I,J))
by SCMFSA8A:9;
Initialize (if=0 (a,I,J)) c= (Initialized ss) +* (Initialize (if=0 (a,I,J)))
by FUNCT_4:26;
then A22:
if=0 (a,I,J) c= (Initialized ss) +* (Initialize (if=0 (a,I,J)))
by A21, XBOOLE_1:1;
A23:
Initialize (Directed I) c= (Initialized ss) +* (Initialize (Directed I))
by FUNCT_4:26;
A24:
if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)
by SCMFSA8B:def 1;
then
if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA))
by SCMFSA6A:67;
then A25:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= if=0 (a,I,J)
by A19, FUNCT_4:26;
then
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= (Initialized ss) +* (Initialize (if=0 (a,I,J)))
by A22, XBOOLE_1:1;
then
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)
by AMI_1:81;
then A26:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)
;
A27:
Reloc ((Directed I),((card J) + 3)) c= Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3))
by COMPOS_1:156, SCMFSA6A:55;
then A28:
Reloc ((Directed I),((card J) + 3)) c= Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)
by A26, XBOOLE_1:1;
Reloc ((Directed I),((card J) + 3)) c= if=0 (a,I,J)
by A25, A27, XBOOLE_1:1;
then A29:
Reloc ((Directed I),((card J) + 3)) c= P +* (if=0 (a,I,J))
by XBOOLE_1:1, A1;
A30:
(P +* (if=0 (a,I,J))) /. (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1)))) = (P +* (if=0 (a,I,J))) . (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1))))
by PBOOLE:158;
A31:
ProgramPart (Directed I) = Directed I
by RELAT_1:209;
IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1))) =
IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)))))
by EXTPRO_1:5
.=
(IC (Comput ((P +* (Directed I)),((Initialized ss) +* (Initialize (Directed I))),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)))))) + ((card J) + 3)
by A23, A14, A28, A11, A17, Th51, A2, A29
.=
(IC (Comput ((P +* (Directed I)),((Initialized ss) +* (Initialize (Directed I))),(pseudo-LifeSpan ((Initialized ss),P,(Directed I)))))) + ((card J) + 3)
by A12, Th50
.=
(card (Directed I)) + ((card J) + 3)
by A12, SCMFSA8A:def 5, A31
.=
(card I) + ((card J) + 3)
by SCMFSA8A:34
.=
((card I) + (card J)) + 3
;
then A32: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1)))) =
(P +* (if=0 (a,I,J))) . (((card I) + (card J)) + 3)
by A30
.=
(if=0 (a,I,J)) . (((card I) + (card J)) + 3)
by A18, GRFUNC_1:8, A1
.=
halt SCM+FSA
by Th61
;
then A33:
P +* (if=0 (a,I,J)) halts_on (Initialized ss) +* (Initialize (if=0 (a,I,J)))
by EXTPRO_1:30;
now set J1 =
(((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I;
let k be
Element of
NAT ;
( CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k))) = halt SCM+FSA implies (pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1 <= k )assume A34:
CurInstr (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)))
= halt SCM+FSA
;
(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1 <= kassume
not
(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1
<= k
;
contradictionthen A35:
k <= pseudo-LifeSpan (
((Initialized ss) +* (Initialize (Directed I))),
(P +* (Directed I)),
(Directed I))
by NAT_1:13;
A36:
0 in dom (if=0 (a,I,J))
by Th54;
A37:
Comput (
(P +* (if=0 (a,I,J))),
((Initialized ss) +* (Initialize (if=0 (a,I,J)))),
0)
= (Initialized ss) +* (Initialize (if=0 (a,I,J)))
by EXTPRO_1:3;
A38:
(P +* (if=0 (a,I,J))) /. (IC ((Initialized ss) +* (Initialize (if=0 (a,I,J))))) = (P +* (if=0 (a,I,J))) . (IC ((Initialized ss) +* (Initialize (if=0 (a,I,J)))))
by PBOOLE:158;
CurInstr (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),0))) =
(P +* (if=0 (a,I,J))) . 0
by Th31, A38, A37
.=
(if=0 (a,I,J)) . 0
by A36, GRFUNC_1:8, A1
.=
a =0_goto ((card J) + 3)
by Th55
;
then
k <> 0
by A34;
then consider k1 being
Nat such that A39:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
reconsider n =
IC (Comput ((P +* (Directed I)),((Initialized ss) +* (Initialize (Directed I))),k1)) as
Element of
NAT ;
k1 < k
by A39, XREAL_1:31;
then A40:
k1 < pseudo-LifeSpan (
((Initialized ss) +* (Initialize (Directed I))),
(P +* (Directed I)),
(Directed I))
by A35, XXREAL_0:2;
then
k1 < pseudo-LifeSpan (
(Initialized ss),
P,
(Directed I))
by A12, Th50;
then
n in dom (Directed I)
by A12, SCMFSA8A:31, A31;
then
n < card (Directed I)
by AFINSQ_1:70;
then
n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3)
by XREAL_1:8;
then A41:
n + ((card J) + 3) < (card I) + ((card J) + 3)
by SCMFSA8A:34;
A42:
IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)) =
IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)),k1))
by A39, EXTPRO_1:5
.=
(IC (Comput ((P +* (Directed I)),((Initialized ss) +* (Initialize (Directed I))),k1))) + ((card J) + 3)
by A23, A14, A28, A11, A17, A40, Th51, A2, A29
;
card ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) =
(card (((Macro (a =0_goto ((card J) + 3))) ';' J) ';' (Goto ((card I) + 1)))) + (card I)
by SCMFSA6A:61
.=
((card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))) + (card I)
by SCMFSA6A:61
.=
((card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1) + (card I)
by SCMFSA8A:29
.=
(((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1) + (card I)
by SCMFSA6A:61
.=
((2 + (card J)) + 1) + (card I)
by COMPOS_1:150
.=
((card I) + (card J)) + 3
;
then
IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)) in dom ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)
by A42, A41, AFINSQ_1:70;
then A43:
IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)) in dom (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I))
by FUNCT_4:105;
then A44:
(Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k))) in rng (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I))
by FUNCT_1:def 5;
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 A41, XXREAL_0:2;
then A45:
IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)) in dom (if=0 (a,I,J))
by A42, AFINSQ_1:70;
A46:
(P +* (if=0 (a,I,J))) /. (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k))) = (P +* (if=0 (a,I,J))) . (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)))
by PBOOLE:158;
A47:
CurInstr (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k))) =
(P +* (if=0 (a,I,J))) . (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)))
by A46
.=
(if=0 (a,I,J)) . (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)))
by A45, A1, GRFUNC_1:8
;
Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) c= if=0 (
a,
I,
J)
by A24, SCMFSA6A:55;
then
(if=0 (a,I,J)) . (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k))) = (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . (IC (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),k)))
by A43, GRFUNC_1:8;
hence
contradiction
by A34, A44, A47, COMPOS_1:def 7;
verum end;
then A48:
LifeSpan ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J))))) = (pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1
by A32, A33, EXTPRO_1:def 14;
(Initialized ss) +* (Initialized (I ';' (Stop SCM+FSA))) = (Initialized (Initialized ss)) +* (Initialize (I ';' (Stop SCM+FSA)))
by SCMFSA8A:13;
then A49:
(Initialized ss) +* (Initialized (I ';' (Stop SCM+FSA))) = (Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA)))
by Th15;
A50:
(Directed I) ';' (Stop SCM+FSA) = I ';' (Stop SCM+FSA)
by SCMFSA8A:41;
Directed (Directed I) = Directed I
by SCMFSA6A:63;
then A51:
DataPart (Comput ((P +* (Directed I)),((Initialized ss) +* (Initialize (Directed I))),(pseudo-LifeSpan ((Initialized ss),P,(Directed I))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA)))),(pseudo-LifeSpan ((Initialized ss),P,(Directed I)))))
by A12, A50, Th58;
I ';' (Stop SCM+FSA) is_halting_on Initialized ss,P
by A12, Th58;
then A52:
P +* (I ';' (Stop SCM+FSA)) halts_on (Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA)))
by SCMFSA7B:def 8, A4;
thus DataPart (IExec ((if=0 (a,I,J)),P,ss)) =
DataPart (IExec ((if=0 (a,I,J)),P,(Initialized ss)))
by Th17
.=
DataPart ((Result ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialized (if=0 (a,I,J)))))) +* ((Initialized ss) | NAT))
.=
DataPart (Result ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J))))))
by A20, COMPOS_1:82
.=
DataPart (Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),(LifeSpan ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J))))))))
by A33, EXTPRO_1:23
.=
DataPart (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),((Initialized ss) +* (Initialize (if=0 (a,I,J)))),1)),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)))))
by A48, EXTPRO_1:5
.=
DataPart (Comput ((P +* (Directed I)),((Initialized ss) +* (Initialize (Directed I))),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)))))
by A23, A14, A28, A11, A17, Th51, A2, A29
.=
DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA)))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA))))))))
by A12, A13, A51, Th50
.=
DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (I ';' (Stop SCM+FSA))))))
by A52, EXTPRO_1:23
.=
DataPart ((Result ((P +* (I ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialized (I ';' (Stop SCM+FSA)))))) +* ((Initialized ss) | NAT))
by A49, COMPOS_1:82
.=
DataPart (IExec ((I ';' (Stop SCM+FSA)),P,(Initialized ss)))
.=
DataPart (IExec ((I ';' (Stop SCM+FSA)),P,ss))
by Th17
; verum