let P be Instruction-Sequence of SCMPDS; for s being State of SCMPDS
for I being Program of
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
let s be State of SCMPDS; for I being Program of
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
let I be Program of ; for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
let a be Int_position; for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
let i be Integer; for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
let n be Nat; ( s . (DataLoc ((s . a),i)) >= 0 implies ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )
set d1 = DataLoc ((s . a),i);
assume A1:
s . (DataLoc ((s . a),i)) >= 0
; ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
set i1 = (a,i) >=0_goto ((card I) + 3);
set i2 = AddTo (a,i,n);
set i3 = goto (- ((card I) + 2));
set FOR = for-up (a,i,n,I);
set pFOR = stop (for-up (a,i,n,I));
set s3 = Initialize s;
set P3 = P +* (stop (for-up (a,i,n,I)));
set s4 = Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),1);
set P4 = P +* (stop (for-up (a,i,n,I)));
A2:
IC (Initialize s) = 0
by MEMSTR_0:def 11;
A3:
not DataLoc ((s . a),i) in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
not a in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
then A4: (Initialize s) . (DataLoc (((Initialize s) . a),i)) =
(Initialize s) . (DataLoc ((s . a),i))
by FUNCT_4:11
.=
s . (DataLoc ((s . a),i))
by A3, FUNCT_4:11
;
A5:
for-up (a,i,n,I) = ((a,i) >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2))))
by Th2;
Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),(0 + 1)) =
Following ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),0)))
by EXTPRO_1:3
.=
Exec (((a,i) >=0_goto ((card I) + 3)),(Initialize s))
by A5, SCMPDS_6:11
;
then A6: IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),1)) =
ICplusConst ((Initialize s),((card I) + 3))
by A1, A4, SCMPDS_2:57
.=
0 + ((card I) + 3)
by A2, SCMPDS_6:12
;
A7:
card (for-up (a,i,n,I)) = (card I) + 3
by Th30;
then A8:
(card I) + 3 in dom (stop (for-up (a,i,n,I)))
by COMPOS_1:64;
stop (for-up (a,i,n,I)) c= P +* (stop (for-up (a,i,n,I)))
by FUNCT_4:25;
then (P +* (stop (for-up (a,i,n,I)))) . ((card I) + 3) =
(stop (for-up (a,i,n,I))) . ((card I) + 3)
by A8, GRFUNC_1:2
.=
halt SCMPDS
by A7, COMPOS_1:64
;
then A9:
CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),1))) = halt SCMPDS
by A6, PBOOLE:143;
now for k being Nat holds IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),k)) in dom (stop (for-up (a,i,n,I)))let k be
Nat;
IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),b1)) in dom (stop (for-up (a,i,n,I)))per cases
( 0 < k or k = 0 )
;
suppose
0 < k
;
IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),b1)) in dom (stop (for-up (a,i,n,I)))then
1
+ 0 <= k
by INT_1:7;
hence
IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),k)) in dom (stop (for-up (a,i,n,I)))
by A8, A6, A9, EXTPRO_1:5;
verum end; suppose
k = 0
;
IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),b1)) in dom (stop (for-up (a,i,n,I)))then
Comput (
(P +* (stop (for-up (a,i,n,I)))),
(Initialize s),
k)
= Initialize s
;
hence
IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize s),k)) in dom (stop (for-up (a,i,n,I)))
by A2, COMPOS_1:36;
verum end; end; end;
hence
for-up (a,i,n,I) is_closed_on s,P
by SCMPDS_6:def 2; for-up (a,i,n,I) is_halting_on s,P
P +* (stop (for-up (a,i,n,I))) halts_on Initialize s
by A9, EXTPRO_1:29;
hence
for-up (a,i,n,I) is_halting_on s,P
by SCMPDS_6:def 3; verum