let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA
for s being State of SCM+FSA st I ';' J c= P & Initialized (I ';' J) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
set D = Data-Locations SCM+FSA;
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA
for s being State of SCM+FSA st I ';' J c= P & Initialized (I ';' J) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
let J be parahalting Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I ';' J c= P & Initialized (I ';' J) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
let s be State of SCM+FSA; :: thesis: ( I ';' J c= P & Initialized (I ';' J) c= s implies ( IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) ) )
set s1 = s +* I;
set s3 = (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J);
set m1 = LifeSpan ((P +* I),(s +* I));
set m3 = LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)));
A1: dom (Directed I) = dom I by FUNCT_4:105;
A2: ( Directed I c= I ';' J & I ';' J c= Initialized (I ';' J) ) by SCMFSA6A:26, SCMFSA6A:55;
assume that
A3: I ';' J c= P and
A4: Initialized (I ';' J) c= s ; :: thesis: ( IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
( Start-At (0,SCM+FSA) c= Initialize (I ';' J) & Initialize (I ';' J) c= s ) by Th8, FUNCT_4:26, A4;
then A5: Start-At (0,SCM+FSA) c= s by XBOOLE_1:1;
A6: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A1, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A4, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A2, LATTICE2:8, XBOOLE_1:1
.= s by A4, LATTICE2:8 ;
A7: Directed I c= I ';' J by SCMFSA6A:55;
A8: Directed I c= P by A7, A3, XBOOLE_1:1;
then A9: P +* (Directed I) = P by FUNCT_4:79;
Initialize (I ';' J) c= s by A4, Th8;
then A10: s = s +* (Initialize (I ';' J)) by FUNCT_4:79;
A11: P = P +* (I ';' J) by A3, FUNCT_4:79;
A12: Initialized I c= s +* I by A4, SCMFSA6A:52;
then A13: Initialize I c= s +* I by Th8;
A14: P +* I halts_on s +* I by Th18, A13, FUNCT_4:26;
hence A15: IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I by A5, A6, Th37, FUNCT_4:26, A8; :: thesis: ( DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A16: intloc 0 in dom (Initialized I) by SCMFSA6A:45;

A17: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized J)) implies (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁ )
assume x in dom (DataPart (Initialized J)) ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁
then A18: x in (dom (Initialized J)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then A19: x in dom (Initialized J) by XBOOLE_0:def 4;
A20: x in Data-Locations SCM+FSA by A18, XBOOLE_0:def 4;

per cases ( x in dom J or x = intloc 0 or x = IC ) by A19, SCMFSA6A:44;

suppose A21: x in dom J ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁

dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A21;
(DataPart (Initialized J)) . l = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . l by A20, SCMFSA6A:37;
hence (DataPart (Initialized J)) . x = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . x ; :: thesis: verum

end;

suppose A22: x = intloc 0 ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁

thus (DataPart (Initialized J)) . x = (Initialized J) . x by A20, FUNCT_1:72
.= 1 by A22, SCMFSA6A:46
.= (Initialized I) . x by A22, SCMFSA6A:46
.= (s +* I) . x by A12, A16, A22, GRFUNC_1:8
.= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) . x by A13, A22, Def4, FUNCT_4:26
.= (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . x by A20, FUNCT_1:72 ; :: thesis: verum

end;

suppose x = IC ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . b₁

hence (DataPart (Initialized J)) . x = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) . x by A18, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

set s4 = Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1));
reconsider m = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)))) as Element of NAT ;
A23: Initialized J c= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
Initialized J c= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26;
then dom (Initialized J) c= dom ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) by GRFUNC_1:8;
then A24: dom (Initialized J) c= the carrier of SCM+FSA by PARTFUN1:def 4;
J c= (P +* I) +* J by FUNCT_4:26;
then A25: (P +* I) +* J halts_on (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J) by A23, Th19;
dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Data-Locations SCM+FSA) by A24, XBOOLE_1:26;
then dom (DataPart (Initialized J)) c= (dom (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) /\ (Data-Locations SCM+FSA) by PARTFUN1:def 4;
then dom (DataPart (Initialized J)) c= dom (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) by RELAT_1:90;
then ( DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) = (DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))))) +* (DataPart (Initialized J)) & DataPart (Initialized J) c= DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) ) by A17, FUNCT_4:75, GRFUNC_1:8;
then A26: DataPart (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) by LATTICE2:8;
A27: s +* I = (Initialize s) +* I by A5, FUNCT_4:79
.= Initialize (s +* I) by COMPOS_1:83
.= s +* (Initialize I) by FUNCT_4:15 ;
Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* I)))), Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(LifeSpan ((P +* I),(s +* I)))) equal_outside NAT by Th40, A27, A14;
then Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))), Comput (P,s,(LifeSpan ((P +* I),(s +* I)))) equal_outside NAT by A10, A27, A11;
then DataPart (Comput (P,s,(LifeSpan ((P +* I),(s +* I))))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) by A26, COMPOS_1:138;
hence A28: DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) by A5, A6, FUNCT_4:26, A14, Th38, A8; :: thesis: ( Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A29: Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
A30: I ';' J c= P by A3;
A31: Reloc (J,(card I)) c= P by A29, A30, XBOOLE_1:1;
hence Reloc (J,(card I)) c= P ; :: thesis: ( (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A32: intloc 0 in dom (Initialized J) by SCMFSA6A:45;
intloc 0 in Int-Locations by SCMFSA_2:9;
then A33: intloc 0 in Data-Locations SCM+FSA by XBOOLE_0:def 3, SCMFSA_2:127;
hence (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = (DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J))) . (intloc 0) by A28, FUNCT_1:72
.= ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) . (intloc 0) by A33, FUNCT_1:72
.= (Initialized J) . (intloc 0) by A32, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis: ( P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A34: Comput (P,s,(((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)))))) = Comput (P,(Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J))))) by EXTPRO_1:5;
A35: Initialize J c= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J) by Th8, FUNCT_4:26;
A36: J c= (P +* I) +* J by FUNCT_4:26;
then IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J))))))) by A15, A28, Th27, A31, A35;
then A37: CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A25, EXTPRO_1:def 14, A34
.= halt SCM+FSA by COMPOS_1:93 ;
hence A38: P halts_on s by EXTPRO_1:30; :: thesis: ( LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )

A39: now

let k be Element of NAT ; :: thesis: ( ((LifeSpan ((P +* I),(s +* I))) + 1) + k < m implies not CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),(s +* I))) + 1) + k)))) = halt SCM+FSA )
assume ((LifeSpan ((P +* I),(s +* I))) + 1) + k < m ; :: thesis: not CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),(s +* I))) + 1) + k)))) = halt SCM+FSA
then A40: k < LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J))) by XREAL_1:8;
assume A41: CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),(s +* I))) + 1) + k)))) = halt SCM+FSA ; :: thesis: contradiction
IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)),k)))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))),k))) by A15, A28, A35, Th27, A36, A31
.= halt SCM+FSA by A41, EXTPRO_1:5 ;
then InsCode (CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)),k)))) = 0 by COMPOS_1:def 38, SCMFSA_2:124;
then CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)),k))) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A25, A40, EXTPRO_1:def 14; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k < m implies CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA )
assume A42: k < m ; :: thesis: CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA

per cases ( k <= LifeSpan ((P +* I),(s +* I)) or LifeSpan ((P +* I),(s +* I)) < k ) ;

suppose A43: k <= LifeSpan ((P +* I),(s +* I)) ; :: thesis: CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA

(P +* I) +* (Directed I) = P +* (Directed I) by FUNCT_4:78, A1;
hence CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA by A12, A6, Th39, A43, FUNCT_4:26, A9; :: thesis: verum

end;

suppose LifeSpan ((P +* I),(s +* I)) < k ; :: thesis: CurInstr (P,(Comput (P,s,b₁))) <> halt SCM+FSA

then (LifeSpan ((P +* I),(s +* I))) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A44: ((LifeSpan ((P +* I),(s +* I))) + 1) + kk = k by NAT_1:10;
kk in NAT by ORDINAL1:def 13;
hence CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA by A39, A42, A44; :: thesis: verum

end;

end;

end;

then A45: for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt SCM+FSA holds
m <= k ;
then A46: LifeSpan (P,s) = m by A37, A38, EXTPRO_1:def 14;
A47: s +* I = s +* (Initialized I) by A4, SCMFSA6A:51;
A48: Initialized I c= s +* I by A47, FUNCT_4:26;
P +* I halts_on s +* I by Th19, A48, FUNCT_4:26;
then Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I)))) = Result ((P +* I),(s +* I)) by EXTPRO_1:23;
hence LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) by A45, A37, A38, EXTPRO_1:def 14; :: thesis: ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 )
A49: Initialize J c= (Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J) by Th8, FUNCT_4:26;

hereby :: thesis: verum

A50: DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)))))) = DataPart (Comput (P,(Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)))))) by A15, A28, A35, Th27, A36, A31;
assume A51: J is keeping_0 ; :: thesis: (Result (P,s)) . (intloc 0) = 1
thus (Result (P,s)) . (intloc 0) = (Comput (P,s,m)) . (intloc 0) by A38, A46, EXTPRO_1:23
.= (Comput (P,(Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by EXTPRO_1:5
.= (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by A50, SCMFSA6A:38
.= ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) . (intloc 0) by A49, A51, Def4, FUNCT_4:26
.= (Initialized J) . (intloc 0) by A32, A23, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis: verum

end;