let s be State of SCMPDS ; for I being halt-free shiftable Program of SCMPDS
for J being shiftable Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) = 0 & I is_closed_on s & I is_halting_on s holds
IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )
let I be halt-free shiftable Program of SCMPDS ; for J being shiftable Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) = 0 & I is_closed_on s & I is_halting_on s holds
IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )
let J be shiftable Program of SCMPDS ; for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) = 0 & I is_closed_on s & I is_halting_on s holds
IExec (if=0 a,k1,I,J),s = (IExec I,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 & I is_closed_on s & I is_halting_on s holds
IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )
let k1 be Integer; ( s . (DataLoc (s . a),k1) = 0 & I is_closed_on s & I is_halting_on s implies IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ) )
set b = DataLoc (s . a),k1;
assume A1:
s . (DataLoc (s . a),k1) = 0
; ( not I is_closed_on s or not I is_halting_on s or IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ) )
set i = a,k1 <>0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
set I2 = (I ';' (Goto ((card J) + 1))) ';' J;
set IF = if=0 a,k1,I,J;
set pI2 = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set s2 = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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;
I1:
s +* (Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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;
A2:
IC ((Initialize s) +* (stop (if=0 a,k1,I,J))) = 0
by I2, FUNCT_4:26, SCMPDS_5:18;
A3:
not DataLoc (s . a),k1 in dom (Initialize (stop (if=0 a,k1,I,J)))
by SCMPDS_4:31;
A4: 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
;
then A5:
Shift (stop ((I ';' (Goto ((card J) + 1))) ';' J)),1 c= Comput (ProgramPart ((Initialize s) +* (stop (if=0 a,k1,I,J)))),((Initialize s) +* (stop (if=0 a,k1,I,J))),1
by Lm5;
A6: 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 A4, Th22, I2
;
not a in dom (Initialize (stop (if=0 a,k1,I,J)))
by SCMPDS_4:31;
then ((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
.=
0
by A1, A3, I2, FUNCT_4:12
;
then A7: IC (Comput (ProgramPart ((Initialize s) +* (stop (if=0 a,k1,I,J)))),((Initialize s) +* (stop (if=0 a,k1,I,J))),1) =
succ (IC ((Initialize s) +* (stop (if=0 a,k1,I,J))))
by A6, SCMPDS_2:67
.=
0 + 1
by A2
;
A8:
DataPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' 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 A6, SCMPDS_2:67
;
verum end;
then A9:
DataPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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;
A10:
dom (ProgramPart s) = NAT
by COMPOS_1:34;
set SAl = Start-At (((card I) + (card J)) + 2),SCMPDS ;
assume A11:
I is_closed_on s
; ( not I is_halting_on s or IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ) )
assume A12:
I is_halting_on s
; IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )
then
(I ';' (Goto ((card J) + 1))) ';' J is_halting_on s
by A11, Th44;
then A13:
ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) halts_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))
by Def3;
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on s
by A11, A12, Th44;
then A14:
( Initialize (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) )
by Th38, I1, FUNCT_4:26;
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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))
by AMI_1:123;
TX2:
ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))
by AMI_1:123;
A15: 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))
by x, T
.=
CurInstr (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))
by A14, A5, A7, A9, Th45, TX2, TX4
.=
halt SCMPDS
by A13, AMI_1:def 46
;
then A16:
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;
A17:
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 A4, Th22, I2;
now let l be
Element of
NAT ;
( l < (LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 A18:
l < (LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 A17, Th29;
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 A19:
l = n + 1
by NAT_1:6;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A20:
n < LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),
((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))
by A18, A19, XREAL_1:8;
assume A21:
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;
TX2:
ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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;
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;
CurInstr (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),
(Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 A14, A5, A7, A9, TX2, TX4, Th45
.=
halt SCMPDS
by A19, A21, x, T
;
hence
contradiction
by A13, A20, 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) + 1 <= l
;
then A22:
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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) + 1
by A15, A16, 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;
A23: DataPart (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) =
DataPart (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))
by A13, 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))
by A14, A5, 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' 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 A16, A22, AMI_1:122
;
A24:
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 ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . b1 )A27:
dom (Start-At (((card I) + (card J)) + 2),SCMPDS ) = {(IC SCMPDS )}
by FUNCOP_1:19;
assume A28:
x in dom (IExec (if=0 a,k1,I,J),s)
;
(IExec (if=0 a,k1,I,J),s) . b1 = ((IExec ((I ';' (Goto ((card J) + 1))) ';' 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 A28, SCMPDS_4:20;
suppose A29:
x is
Int_position
;
(IExec (if=0 a,k1,I,J),s) . b1 = ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . b1then
x <> IC SCMPDS
by SCMPDS_2:52;
then A30:
not
x in dom (Start-At (((card I) + (card J)) + 2),SCMPDS )
by A27, TARSKI:def 1;
A31:
not
x in dom (s | NAT )
by A10, A29, 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) . x
by A23, A29, SCMPDS_4:23
.=
(IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) . x
by A31, FUNCT_4:12
.=
((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . x
by A30, FUNCT_4:12
;
verum end; suppose A32:
x = IC SCMPDS
;
(IExec (if=0 a,k1,I,J),s) . b1 = ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . b1A33:
not
x in dom (s | NAT )
by A10, A32, COMPOS_1:3;
then A34:
IC (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) =
IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s)
by A32, FUNCT_4:12
.=
((card I) + (card J)) + 1
by A11, A12, Th46
;
A35:
x in dom (Start-At (((card I) + (card J)) + 2),SCMPDS )
by A27, A32, 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 A33, 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) + 1)) . x
by A16, A22, 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 ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))
by A32, AMI_1:51
.=
(IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) + 1
by A14, A5, A7, A9, Th45, T
.=
(IC (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1
by A13, AMI_1:122
.=
(Start-At ((((card I) + (card J)) + 1) + 1),SCMPDS ) . (IC SCMPDS )
by A34, FUNCOP_1:87
.=
((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . x
by A32, A35, 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 ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ))
by PARTFUN1:def 4
;
hence IExec (if=0 a,k1,I,J),s =
(IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )
by A24, FUNCT_1:9
.=
((IExec I,s) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )
by A11, A12, Th47
.=
(IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )
by Th14
;
verum