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 ;
I1:
s +* (Initialize (stop J)) = (Initialize s) +* (stop J)
by SCMPDS_4:5;
I2:
s +* (Initialize (stop (if<0 a,k1,I,J))) = (Initialize s) +* (stop (if<0 a,k1,I,J))
by SCMPDS_4:5;
A1: 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
;
A2: 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 AMI_1:14
.=
Following (ProgramPart ((Initialize s) +* (stop (if<0 a,k1,I,J)))),((Initialize s) +* (stop (if<0 a,k1,I,J)))
by AMI_1:13
.=
Exec (a,k1 >=0_goto ((card I) + 2)),((Initialize s) +* (stop (if<0 a,k1,I,J)))
by A1, Th22, I2
;
A3:
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 A4: ((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 I2, FUNCT_4:12
.=
s . (DataLoc (s . a),k1)
by A3, I2, FUNCT_4:12
;
A5:
IC ((Initialize s) +* (stop (if<0 a,k1,I,J))) = 0
by I2, FUNCT_4:26, SCMPDS_5:18;
A6:
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 A7: 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 A2, A4, SCMPDS_2:69
.=
0 + ((card I) + 2)
by A5, Th23
;
A8:
DataPart ((Initialize s) +* (stop J)) = DataPart ((Initialize s) +* (stop (if<0 a,k1,I,J)))
by FUNCT_7:134, SCMPDS_4:24;
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 A8, 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 A2, SCMPDS_2:69
;
verum end;
then A9:
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 SCMPDS_4:45
.=
(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 A10:
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 A10, XBOOLE_1:1;
then A11:
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 A12:
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 A13:
( Initialize (stop J) c= (Initialize s) +* (stop J) & J is_closed_on (Initialize s) +* (stop J) )
by Th38, I1, FUNCT_4:26;
assume A14:
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 A15:
ProgramPart ((Initialize s) +* (stop J)) halts_on (Initialize s) +* (stop J)
by Def3;
T:
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;
x:
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 AMI_1:51;
TX4:
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),(LifeSpan (ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))
by AMI_1:123;
TX1:
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;
A16: 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 ((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),(LifeSpan (ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))))
by x, T
.=
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 A13, A11, A7, A9, Th45, TX1, TX4
.=
halt SCMPDS
by A15, AMI_1:def 46
;
then A17:
ProgramPart ((Initialize s) +* (stop (if<0 a,k1,I,J))) halts_on (Initialize s) +* (stop (if<0 a,k1,I,J))
by AMI_1:146;
A18:
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 A1, Th22, I2;
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 A19:
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 SCMPDS u:
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 AMI_1:13;
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 SCMPDS then
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 u;
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 A18, Th31;
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 SCMPDS then consider n being
Nat such that A20:
l = n + 1
by NAT_1:6;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A21:
n < LifeSpan (ProgramPart ((Initialize s) +* (stop J))),
((Initialize s) +* (stop J))
by A19, A20, XREAL_1:8;
assume 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))),l) = halt SCMPDS
;
contradictionT:
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;
x:
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 AMI_1:51;
TX1:
ProgramPart ((Initialize s) +* (stop J)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)),n)
by AMI_1:123;
TX4:
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 A13, A11, A7, A9, Th45, TX1, TX4
.=
halt SCMPDS
by A20, A22, x, T
;
hence
contradiction
by A15, A21, AMI_1:def 46;
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 A23:
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 A16, A17, AMI_1:def 46;
T:
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;
A24: 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 A15, AMI_1:122
.=
DataPart (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 A13, A11, A7, A9, Th45, T
.=
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 AMI_1:51
.=
DataPart (Result (ProgramPart ((Initialize s) +* (stop (if<0 a,k1,I,J)))),((Initialize s) +* (stop (if<0 a,k1,I,J))))
by A17, A23, AMI_1:122
;
A25:
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 )A28:
dom (Start-At (((card I) + (card J)) + 2),SCMPDS ) = {(IC SCMPDS )}
by FUNCOP_1:19;
assume A29:
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 SCMPDS or x is Element of NAT )
by A29, SCMPDS_4:20;
suppose A30:
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 SCMPDS
by SCMPDS_2:52;
then A31:
not
x in dom (Start-At (((card I) + (card J)) + 2),SCMPDS )
by A28, TARSKI:def 1;
A32:
not
x in dom (s | NAT )
by A6, A30, 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 A24, A30, SCMPDS_4:23
.=
(IExec J,s) . x
by A32, FUNCT_4:12
.=
((IExec J,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . x
by A31, FUNCT_4:12
;
verum end; suppose A33:
x = IC SCMPDS
;
(IExec (if<0 a,k1,I,J),s) . b1 = ((IExec J,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . b1A34:
not
x in dom (s | NAT )
by A6, A33, COMPOS_1:3;
then A35:
IC (Result (ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J))) =
IC (IExec J,s)
by A33, FUNCT_4:12
.=
card J
by A12, A14, Th48
;
A36:
x in dom (Start-At (((card I) + (card J)) + 2),SCMPDS )
by A28, A33, TARSKI:def 1;
T:
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 A34, 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 A17, A23, AMI_1:122
.=
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 A33, AMI_1:51
.=
(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 A13, A11, A7, A9, Th45, T
.=
(IC (Result (ProgramPart ((Initialize s) +* (stop J))),((Initialize s) +* (stop J)))) + ((card I) + 2)
by A15, AMI_1:122
.=
(Start-At ((card J) + ((card I) + 2)),SCMPDS ) . (IC SCMPDS )
by A35, FUNCOP_1:87
.=
((IExec J,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . x
by A33, A36, 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 A25, FUNCT_1:9; verum