let s be State of SCMPDS ; for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) <= 0 holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let I be Program of SCMPDS ; for a being Int_position
for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) <= 0 holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let a be Int_position ; for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) <= 0 holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let i be Integer; for n being Element of NAT st s . (DataLoc (s . a),i) <= 0 holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
let n be Element of NAT ; ( s . (DataLoc (s . a),i) <= 0 implies ( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s ) )
set d1 = DataLoc (s . a),i;
assume A1:
s . (DataLoc (s . a),i) <= 0
; ( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
set i1 = a,i <=0_goto ((card I) + 3);
set i2 = AddTo a,i,(- n);
set i3 = goto (- ((card I) + 2));
set FOR = for-down a,i,n,I;
set pFOR = stop (for-down a,i,n,I);
set iFOR = Initialized (stop (for-down a,i,n,I));
set s3 = s +* (Initialized (stop (for-down a,i,n,I)));
set s4 = Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1;
A2:
IC (s +* (Initialized (stop (for-down a,i,n,I)))) = 0
by SCMPDS_6:21;
A3:
not DataLoc (s . a),i in dom (Initialized (stop (for-down a,i,n,I)))
by SCMPDS_4:31;
not a in dom (Initialized (stop (for-down a,i,n,I)))
by SCMPDS_4:31;
then A4: (s +* (Initialized (stop (for-down a,i,n,I)))) . (DataLoc ((s +* (Initialized (stop (for-down a,i,n,I)))) . a),i) =
(s +* (Initialized (stop (for-down a,i,n,I)))) . (DataLoc (s . a),i)
by FUNCT_4:12
.=
s . (DataLoc (s . a),i)
by A3, FUNCT_4:12
;
A5:
for-down a,i,n,I = (a,i <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo a,i,(- n))) ';' (goto (- ((card I) + 2))))
by Th15;
Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(0 + 1) =
Following (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),0 )
by AMI_1:14
.=
Following (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I))))
by AMI_1:13
.=
Exec (a,i <=0_goto ((card I) + 3)),(s +* (Initialized (stop (for-down a,i,n,I))))
by A5, SCMPDS_6:22
;
then A6: IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) =
ICplusConst (s +* (Initialized (stop (for-down a,i,n,I)))),((card I) + 3)
by A1, A4, SCMPDS_2:68
.=
0 + ((card I) + 3)
by A2, SCMPDS_6:23
;
A7:
card (for-down a,i,n,I) = (card I) + 3
by Th60;
then A8:
(card I) + 3 in dom (stop (for-down a,i,n,I))
by SCMPDS_6:25;
Y:
(ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)) /. (IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)) = (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) . (IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1))
by AMI_1:150;
Initialized (stop (for-down a,i,n,I)) c= s +* (Initialized (stop (for-down a,i,n,I)))
by FUNCT_4:26;
then
stop (for-down a,i,n,I) c= Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1
by AMI_1:81, SCMPDS_4:57;
then (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) . ((card I) + 3) =
(stop (for-down a,i,n,I)) . ((card I) + 3)
by A8, GRFUNC_1:8
.=
halt SCMPDS
by A7, SCMPDS_6:25
;
then A9:
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) = halt SCMPDS
by A6, Y;
TX:
ProgramPart (s +* (Initialized (stop (for-down a,i,n,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)
by AMI_1:144;
now let k be
Element of
NAT ;
IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),b1) in dom (stop (for-down a,i,n,I))per cases
( 0 < k or k = 0 )
;
suppose
0 < k
;
IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),b1) in dom (stop (for-down a,i,n,I))then
1
+ 0 <= k
by INT_1:20;
hence
IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),k) in dom (stop (for-down a,i,n,I))
by A8, A6, A9, AMI_1:52, TX;
verum end; suppose
k = 0
;
IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),b1) in dom (stop (for-down a,i,n,I))then
Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),
(s +* (Initialized (stop (for-down a,i,n,I)))),
k = s +* (Initialized (stop (for-down a,i,n,I)))
by AMI_1:13;
hence
IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),k) in dom (stop (for-down a,i,n,I))
by A2, SCMPDS_4:75;
verum end; end;
hence
for-down a,i,n,I is_closed_on s
by SCMPDS_6:def 2; for-down a,i,n,I is_halting_on s
ProgramPart (s +* (Initialized (stop (for-down a,i,n,I)))) halts_on s +* (Initialized (stop (for-down a,i,n,I)))
by A9, AMI_1:146;
hence
for-down a,i,n,I is_halting_on s
by SCMPDS_6:def 3; verum