let s be State of SCMPDS ; for I 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
( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s )
let I 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
( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s )
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
( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s )
let k1 be Integer; ( s . (DataLoc (s . a),k1) = 0 & I is_closed_on s & I is_halting_on s implies ( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s ) )
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 ( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s ) )
set i = a,k1 <>0_goto ((card I) + 1);
set IF = if=0 a,k1,I;
set pIF = stop (if=0 a,k1,I);
set IsIF = Initialized (stop (if=0 a,k1,I));
set pI = stop I;
set IsI = Initialized (stop I);
set s2 = s +* (Initialized (stop I));
set s3 = s +* (Initialized (stop (if=0 a,k1,I)));
set s4 = Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1;
A2:
IC (s +* (Initialized (stop (if=0 a,k1,I)))) = 0
by FUNCT_4:26, SCMPDS_5:18;
A3:
not DataLoc (s . a),k1 in dom (Initialized (stop (if=0 a,k1,I)))
by SCMPDS_4:31;
A4: Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),(0 + 1) =
Following (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),0 )
by AMI_1:14
.=
Following (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I))))
by AMI_1:13
.=
Exec (a,k1 <>0_goto ((card I) + 1)),(s +* (Initialized (stop (if=0 a,k1,I))))
by Th22
;
A5:
DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (if=0 a,k1,I))))
by SCMPDS_4:24, SCMPDS_4:36;
now let a be
Int_position ;
(s +* (Initialized (stop I))) . a = (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1) . athus (s +* (Initialized (stop I))) . a =
(s +* (Initialized (stop (if=0 a,k1,I)))) . a
by A5, SCMPDS_4:23
.=
(Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1) . a
by A4, SCMPDS_2:67
;
verum end;
then A6:
DataPart (s +* (Initialized (stop I))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1)
by SCMPDS_4:23;
not a in dom (Initialized (stop (if=0 a,k1,I)))
by SCMPDS_4:31;
then (s +* (Initialized (stop (if=0 a,k1,I)))) . (DataLoc ((s +* (Initialized (stop (if=0 a,k1,I)))) . a),k1) =
(s +* (Initialized (stop (if=0 a,k1,I)))) . (DataLoc (s . a),k1)
by FUNCT_4:12
.=
0
by A1, A3, FUNCT_4:12
;
then A7: IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1) =
succ (IC (s +* (Initialized (stop (if=0 a,k1,I)))))
by A4, SCMPDS_2:67
.=
0 + 1
by A2
;
assume A8:
I is_closed_on s
; ( not I is_halting_on s or ( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s ) )
then A9:
I is_closed_on s +* (Initialized (stop I))
by Th38;
assume
I is_halting_on s
; ( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s )
then A10:
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I))
by Def3;
A11:
0 in dom (stop (if=0 a,k1,I))
by SCMPDS_4:75;
A12:
( Initialized (stop I) c= s +* (Initialized (stop I)) & Shift (stop I),1 c= Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1 )
by Lm5, FUNCT_4:26;
A13: card (stop (if=0 a,k1,I)) =
(card (if=0 a,k1,I)) + 1
by SCMPDS_5:7
.=
((card I) + 1) + 1
by Th15
;
now let k be
Element of
NAT ;
IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),b1) in dom (stop (if=0 a,k1,I))per cases
( 0 < k or k = 0 )
;
suppose
0 < k
;
IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),b1) in dom (stop (if=0 a,k1,I))then consider k1 being
Nat such that A14:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k1) as
Element of
NAT ;
A15:
card (stop (if=0 a,k1,I)) = (card (stop I)) + 1
by A13, SCMPDS_5:7;
m in dom (stop I)
by A8, Def2;
then
m < card (stop I)
by SCMPDS_4:1;
then A16:
m + 1
< card (stop (if=0 a,k1,I))
by A15, XREAL_1:8;
T:
ProgramPart (s +* (Initialized (stop (if=0 a,k1,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1)
by AMI_1:144;
IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),k) =
IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1),k1)
by A14, AMI_1:51
.=
m + 1
by A9, A12, A7, A6, Th45, T
;
hence
IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),k) in dom (stop (if=0 a,k1,I))
by A16, SCMPDS_4:1;
verum end; suppose
k = 0
;
IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),b1) in dom (stop (if=0 a,k1,I))hence
IC (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),k) in dom (stop (if=0 a,k1,I))
by A11, A2, AMI_1:13;
verum end; end;
hence
if=0 a,k1,I is_closed_on s
by Def2; if=0 a,k1,I is_halting_on s
T:
ProgramPart (s +* (Initialized (stop (if=0 a,k1,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1)
by AMI_1:144;
x:
Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I))))
by AMI_1:51;
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) =
CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (if=0 a,k1,I))))),(s +* (Initialized (stop (if=0 a,k1,I)))),1),(LifeSpan (s +* (Initialized (stop I)))))
by x, T
.=
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))
by A9, A12, A7, A6, Th45
.=
halt SCMPDS
by A10, AMI_1:def 46
;
then
ProgramPart (s +* (Initialized (stop (if=0 a,k1,I)))) halts_on s +* (Initialized (stop (if=0 a,k1,I)))
by AMI_1:146;
hence
if=0 a,k1,I is_halting_on s
by Def3; verum