let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being good Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialized (I ';' J) c= s & I ';' J c= p 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
let I be good Program of SCM+FSA; :: thesis: for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialized (I ';' J) c= s & I ';' J c= p 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
let J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialized (I ';' J) c= s & I ';' J c= p 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
let s be State of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialized (I ';' J) c= s & I ';' J c= p 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) ) )
assume that
A1: s . (intloc 0) = 1 and
A2: I is_halting_on s,p and
A3: J is_halting_on IExec (I,p,s),p and
A4: I is_closed_on s,p and
A5: J is_closed_on IExec (I,p,s),p ; :: thesis: ( not Initialized (I ';' J) c= s or not I ';' J c= p or ( 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) ) )
A6: Start-At (0,SCM+FSA) c= Initialize (I ';' J) by FUNCT_4:26;
set s1 = s +* I;
set p1 = p +* I;
set m1 = LifeSpan ((p +* I),(s +* I));
set s4 = Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1));
set p4 = p;
A7: ProgramPart I = I by RELAT_1:209;
A8: ProgramPart J = J by RELAT_1:209;
A9: Initialize (Directed I) c= Initialize (I ';' J) by PRE_CIRC:3, SCMFSA6A:55;
assume A10: Initialized (I ';' J) c= s ; :: thesis: ( not I ';' J c= p or ( 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) ) )
then Initialize (I ';' J) c= s by SCMFSA6B:8;
then A11: Start-At (0,SCM+FSA) c= s by A6, XBOOLE_1:1;
then A12: s +* I = (Initialize s) +* I by FUNCT_4:79
.= Initialize (s +* I) by COMPOS_1:83
.= s +* (Initialize I) by FUNCT_4:15 ;
then A13: p +* I halts_on s +* I by A2, SCMFSA7B:def 8, A7;
assume A14: I ';' J c= p ; :: 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
Directed I c= I ';' J by SCMFSA6A:55;
then Directed I c= p by A14, XBOOLE_1:1;
then A15: p +* (Directed I) = p by FUNCT_4:79;
Initialize (I ';' J) c= s by A10, SCMFSA6B:8;
then Initialize (Directed I) c= s by A9, XBOOLE_1:1;
then A16: s = s +* (Initialize (Directed I)) by FUNCT_4:79;
hence A17: IC (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) = card I by A2, A4, A12, SCMFSA8A:36, A15; :: 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= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
set JAt = Initialize J;
set InJ = Initialized J;
set s3 = (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J);
set p3 = (p +* I) +* J;
A18: J c= (p +* I) +* J by FUNCT_4:26;
reconsider kk = DataPart (Initialize J) as Function ;
A19: DataPart (Initialize J) = {} by Th2;
(Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) . (intloc 0) = s . (intloc 0) by A4, A12, SCMFSA8C:97;
then A20: (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) = (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialize J) by A1, SCMFSA8C:18;
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)))))) +* kk by FUNCT_4:75;
then 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 A19, LATTICE2:8, XBOOLE_1:2;
hence A21: DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) by A2, A4, A12, A16, SCMFSA8A:36, A15; :: thesis: ( Reloc (J,(card I)) c= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) & (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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
A22: Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
A23: intloc 0 in dom (Initialized J) by SCMFSA6A:45;
A24: s +* I = s +* (Initialized I) by A10, SCMFSA6A:51;
A25: DataPart (IExec (I,p,s)) = DataPart ((Result ((p +* I),(s +* (Initialized I)))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((p +* I),(s +* (Initialized I)))) by COMPOS_1:82
.= DataPart (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) by A13, A24, EXTPRO_1:23 ;
then J is_halting_on Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))),p +* I by A3, A5, SCMFSA8B:8;
then A26: (p +* I) +* J halts_on (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by A20, SCMFSA7B:def 8, A8;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then I ';' J c= s by A10, XBOOLE_1:1;
then Reloc (J,(card I)) c= s by A22, XBOOLE_1:1;
then Reloc (J,(card I)) c= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) by AMI_1:81;
hence Reloc (J,(card I)) c= Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1)) ; :: 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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
A27: Reloc (J,(card I)) c= p by A14, A22, XBOOLE_1:1;
intloc 0 in Int-Locations by SCMFSA_2:def 4;
then A28: 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 A21, FUNCT_1:72
.= ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) . (intloc 0) by A28, FUNCT_1:72
.= (Initialized J) . (intloc 0) by A23, 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 good implies (Result (p,s)) . (intloc 0) = 1 ) )
A29: I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)));
A30: dom (Directed I) = dom I by FUNCT_4:105;
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 ;
A31: Directed I c= I ';' J by SCMFSA6A:55;
(s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A30, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A10, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A31, A29, LATTICE2:8, XBOOLE_1:1
.= s by A10, LATTICE2:8 ;
then Directed I c= s by FUNCT_4:26;
then s +* (Directed I) = s by FUNCT_4:79;
then Initialize (s +* (Directed I)) = s by A11, FUNCT_4:79;
then A32: s +* (Initialize (Directed I)) = s by FUNCT_4:15;
A33: DataPart (IExec (I,p,s)) = DataPart ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) by A20, A25, SCMFSA8A:11;
then A34: J is_closed_on (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J),(p +* I) +* J by A5, SCMFSA8B:6;
A35: 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;
A36: Initialize J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
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 A34, A17, A21, SCMFSA8C:42, A27, A18;
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,s,(((LifeSpan ((p +* I),(s +* I))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)))))))) by A35;
then A37: CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A26, EXTPRO_1:def 14
.= 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 good 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;
A41: Comput (p,s,(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),(s +* I))) + 1))),k) by EXTPRO_1:5;
assume A42: 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 A34, A17, A21, A36, SCMFSA8C:42, A27, A18
.= halt SCM+FSA by A42, A41 ;
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 A26, 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 A43: 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 k <= LifeSpan ((p +* I),(s +* I)) ; :: thesis: CurInstr (p,(Comput (p,s,b₁))) <> halt SCM+FSA

hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A2, A4, A12, A32, SCMFSA8A:35, A15; :: 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;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
((LifeSpan ((p +* I),(s +* I))) + 1) + kk = k by A44;
hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A39, A43; :: thesis: verum

end;

end;

end;

then for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA holds
m <= k ;
then A45: LifeSpan (p,s) = m by A37, A38, EXTPRO_1:def 14;
Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I)))) = Result ((p +* I),(s +* I)) by A13, 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; :: thesis: ( J is good implies (Result (p,s)) . (intloc 0) = 1 )
Initialize J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
then A46: ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) +* (Initialize J) = (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:79;
A47: Initialized J c= (Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J) by FUNCT_4:26;

hereby :: thesis: verum

A48: 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 A34, A17, A21, A36, SCMFSA8C:42, A27, A18;
assume A49: J is good ; :: thesis: (Result (p,s)) . (intloc 0) = 1
thus (Result (p,s)) . (intloc 0) = (Comput (p,s,m)) . (intloc 0) by A38, A45, 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 A48, SCMFSA6A:38
.= ((Comput ((p +* I),(s +* I),(LifeSpan ((p +* I),(s +* I))))) +* (Initialized J)) . (intloc 0) by A5, A33, A46, A49, SCMFSA8B:6, SCMFSA8C:97
.= (Initialized J) . (intloc 0) by A23, A47, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis: verum

end;