let s be State of SCMPDS; for I being Program of SCMPDS
for J being halt-free shiftable Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
let I be Program of SCMPDS; for J being halt-free shiftable Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
let J be halt-free shiftable Program of SCMPDS; for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
let a be Int_position ; for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
let k1 be Integer; ( s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s & J is_halting_on s implies IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS)) )
set b = DataLoc ((s . a),k1);
set pJ = stop J;
set s1 = (Initialize s) +* (stop J);
set IF = if>0 (a,k1,I,J);
set pIF = stop (if>0 (a,k1,I,J));
set s3 = (Initialize s) +* (stop (if>0 (a,k1,I,J)));
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1);
set i = (a,k1) <=0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
set iG = (((a,k1) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1));
set SAl = Start-At ((((card I) + (card J)) + 2),SCMPDS);
A1:
s +* (Initialize (stop J)) = (Initialize s) +* (stop J)
by COMPOS_1:125;
A2:
s +* (Initialize (stop (if>0 (a,k1,I,J)))) = (Initialize s) +* (stop (if>0 (a,k1,I,J)))
by COMPOS_1:125;
A3: if>0 (a,k1,I,J) =
(((a,k1) <=0_goto ((card I) + 2)) ';' (I ';' (Goto ((card J) + 1)))) ';' J
by SCMPDS_4:50
.=
((a,k1) <=0_goto ((card I) + 2)) ';' ((I ';' (Goto ((card J) + 1))) ';' J)
by SCMPDS_4:50
;
A4: Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),(0 + 1)) =
Following ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),0)))
by EXTPRO_1:4
.=
Following ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))))
by EXTPRO_1:3
.=
Exec (((a,k1) <=0_goto ((card I) + 2)),((Initialize s) +* (stop (if>0 (a,k1,I,J)))))
by A3, Th22, A2
;
A5:
not DataLoc ((s . a),k1) in dom (Initialize (stop (if>0 (a,k1,I,J))))
by SCMPDS_4:31;
not a in dom (Initialize (stop (if>0 (a,k1,I,J))))
by SCMPDS_4:31;
then A6: ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . (DataLoc ((((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . a),k1)) =
((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . (DataLoc ((s . a),k1))
by A2, FUNCT_4:12
.=
s . (DataLoc ((s . a),k1))
by A5, A2, FUNCT_4:12
;
A7:
IC ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = 0
by A2, FUNCT_4:26, SCMPDS_5:18;
A8:
dom (ProgramPart s) = NAT
by COMPOS_1:34;
assume
s . (DataLoc ((s . a),k1)) <= 0
; ( not J is_closed_on s or not J is_halting_on s or IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS)) )
then A9: IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) =
ICplusConst (((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((card I) + 2))
by A4, A6, SCMPDS_2:68
.=
0 + ((card I) + 2)
by A7, Th23
;
A10:
DataPart ((Initialize s) +* (stop J)) = DataPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))
by COMPOS_1:138, FUNCT_7:134;
now let a be
Int_position ;
((Initialize s) +* (stop J)) . a = (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) . athus ((Initialize s) +* (stop J)) . a =
((Initialize s) +* (stop (if>0 (a,k1,I,J)))) . a
by A10, SCMPDS_4:23
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) . a
by A4, SCMPDS_2:68
;
verum end;
then A11:
DataPart ((Initialize s) +* (stop J)) = DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))
by SCMPDS_4:23;
card ((((a,k1) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) =
(card (((a,k1) <=0_goto ((card I) + 2)) ';' I)) + (card (Goto ((card J) + 1)))
by AFINSQ_1:20
.=
(card (((a,k1) <=0_goto ((card I) + 2)) ';' I)) + 1
by SCMPDS_5:6
.=
((card I) + 1) + 1
by Th15
.=
(card I) + (1 + 1)
;
then A12:
Shift ((stop J),((card I) + 2)) c= stop (if>0 (a,k1,I,J))
by Th24;
stop (if>0 (a,k1,I,J)) c= (Initialize s) +* (stop (if>0 (a,k1,I,J)))
by FUNCT_4:26;
then
Shift ((stop J),((card I) + 2)) c= (Initialize s) +* (stop (if>0 (a,k1,I,J)))
by A12, XBOOLE_1:1;
then A13:
Shift ((stop J),((card I) + 2)) c= Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)
by AMI_1:81;
assume A14:
J is_closed_on s
; ( not J is_halting_on s or IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS)) )
then A15:
( Initialize (stop J) c= (Initialize s) +* (stop J) & J is_closed_on (Initialize s) +* (stop J) )
by Th38, A1, FUNCT_4:26;
assume A16:
J is_halting_on s
; IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
then A17:
ProgramPart ((Initialize s) +* (stop J)) halts_on (Initialize s) +* (stop J)
by Def3;
A18:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))
by AMI_1:123;
A19:
Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1)) = Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))))
by EXTPRO_1:5;
A20:
ProgramPart ((Initialize s) +* (stop J)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))))
by AMI_1:123;
A21:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1)))
by AMI_1:123;
A22: CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1)))) =
CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))))),(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))))))
by A19, A18, A21
.=
CurInstr ((ProgramPart ((Initialize s) +* (stop J))),(Comput ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))))))
by A15, A13, A9, A11, Th45, A20
.=
halt SCMPDS
by A17, EXTPRO_1:def 14
;
then A23:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) halts_on (Initialize s) +* (stop (if>0 (a,k1,I,J)))
by EXTPRO_1:30;
A24:
CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J))))) = (a,k1) <=0_goto ((card I) + 2)
by A3, Th22, A2;
now let l be
Element of
NAT ;
( l < (LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1 implies CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),b1))) <> halt SCMPDS )assume A25:
l < (LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1
;
CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),b1))) <> halt SCMPDSA26:
Comput (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),
((Initialize s) +* (stop (if>0 (a,k1,I,J)))),
0)
= (Initialize s) +* (stop (if>0 (a,k1,I,J)))
by EXTPRO_1:3;
per cases
( l = 0 or l <> 0 )
;
suppose
l = 0
;
CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),b1))) <> halt SCMPDSthen
CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),l)))
= CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),
((Initialize s) +* (stop (if>0 (a,k1,I,J)))))
by A26;
hence
CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),l)))
<> halt SCMPDS
by A24, Th30;
verum end; suppose
l <> 0
;
not CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),b1))) = halt SCMPDSthen consider n being
Nat such that A27:
l = n + 1
by NAT_1:6;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A28:
n < LifeSpan (
(ProgramPart ((Initialize s) +* (stop J))),
((Initialize s) +* (stop J)))
by A25, A27, XREAL_1:8;
assume A29:
CurInstr (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),l)))
= halt SCMPDS
;
contradictionA30:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))
by AMI_1:123;
A31:
Comput (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),
((Initialize s) +* (stop (if>0 (a,k1,I,J)))),
(n + 1))
= Comput (
(ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),
n)
by EXTPRO_1:5;
A32:
ProgramPart ((Initialize s) +* (stop J)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)),n))
by AMI_1:123;
A33:
ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),n))
by AMI_1:123;
CurInstr (
(ProgramPart ((Initialize s) +* (stop J))),
(Comput ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)),n))) =
CurInstr (
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),
(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),n)))
by A15, A13, A9, A32, A33, A11, Th45
.=
halt SCMPDS
by A27, A29, A31, A30
;
hence
contradiction
by A17, A28, EXTPRO_1:def 14;
verum end; end;
then
for l being Element of NAT st CurInstr ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),l))) = halt SCMPDS holds
(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1 <= l
;
then A34:
LifeSpan ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J))))) = (LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1
by A22, A23, EXTPRO_1:def 14;
A35: DataPart (Result ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) =
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))))
by A17, EXTPRO_1:23
.=
DataPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))))
by A15, A13, A9, A11, Th45
.=
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1)))
by A18, EXTPRO_1:5
.=
DataPart (Result ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J))))))
by A23, A34, EXTPRO_1:23
;
A36:
now let x be
set ;
( x in dom (IExec ((if>0 (a,k1,I,J)),s)) implies (IExec ((if>0 (a,k1,I,J)),s)) . b1 = ((IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))) . b1 )A37:
dom (Start-At ((((card I) + (card J)) + 2),SCMPDS)) = {(IC )}
by FUNCOP_1:19;
assume A38:
x in dom (IExec ((if>0 (a,k1,I,J)),s))
;
(IExec ((if>0 (a,k1,I,J)),s)) . b1 = ((IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))) . b1per cases
( x is Int_position or x = IC or x is Element of NAT )
by A38, SCMPDS_4:20;
suppose A39:
x is
Int_position
;
(IExec ((if>0 (a,k1,I,J)),s)) . b1 = ((IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))) . b1then
x <> IC
by SCMPDS_2:52;
then A40:
not
x in dom (Start-At ((((card I) + (card J)) + 2),SCMPDS))
by A37, TARSKI:def 1;
A41:
not
x in dom (s | NAT)
by A8, A39, SCMPDS_2:53;
hence (IExec ((if>0 (a,k1,I,J)),s)) . x =
(Result ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))))) . x
by FUNCT_4:12
.=
(Result ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) . x
by A35, A39, SCMPDS_4:23
.=
(IExec (J,s)) . x
by A41, FUNCT_4:12
.=
((IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))) . x
by A40, FUNCT_4:12
;
verum end; suppose A42:
x = IC
;
(IExec ((if>0 (a,k1,I,J)),s)) . b1 = ((IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))) . b1A43:
not
x in dom (s | NAT)
by A8, A42, COMPOS_1:3;
then A44:
IC (Result ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) =
IC (IExec (J,s))
by A42, FUNCT_4:12
.=
card J
by A14, A16, Th48
;
A45:
x in dom (Start-At ((((card I) + (card J)) + 2),SCMPDS))
by A37, A42, TARSKI:def 1;
A46:
ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1))
by AMI_1:123;
thus (IExec ((if>0 (a,k1,I,J)),s)) . x =
(Result ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))))) . x
by A43, FUNCT_4:12
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + 1))) . x
by A23, A34, EXTPRO_1:23
.=
IC (Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (if>0 (a,k1,I,J))))),((Initialize s) +* (stop (if>0 (a,k1,I,J)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))))
by A42, EXTPRO_1:5
.=
(IC (Comput ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))))) + ((card I) + 2)
by A15, A13, A9, A11, Th45, A46
.=
(IC (Result ((ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))) + ((card I) + 2)
by A17, EXTPRO_1:23
.=
(Start-At (((card J) + ((card I) + 2)),SCMPDS)) . (IC )
by A44, FUNCOP_1:87
.=
((IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))) . x
by A42, A45, FUNCT_4:14
;
verum end; end;
dom (IExec ((if>0 (a,k1,I,J)),s)) =
the carrier of SCMPDS
by PARTFUN1:def 4
.=
dom ((IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS)))
by PARTFUN1:def 4
;
hence
IExec ((if>0 (a,k1,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))
by A36, FUNCT_1:9; verum