let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t,Q ) holds
I is_closed_on s,P
let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t,Q ) holds
I is_closed_on s,P
let I be Program of SCMPDS; :: thesis: ( ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t,Q ) implies I is_closed_on s,P )
assume A1: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t,Q ; :: thesis: I is_closed_on s,P
set pI = stop I;
set sI = Initialize s;
set PI = P +* (stop I);
defpred S₁[ Nat] means not IC (Comput ((P +* (stop I)),(Initialize s),$1)) in dom (stop I);
A2: for a being Int_position holds s . a = (Initialize s) . a

proof

let a be Int_position ; :: thesis: s . a = (Initialize s) . a
not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
hence s . a = (Initialize s) . a by FUNCT_4:11; :: thesis: verum

end;

assume not I is_closed_on s,P ; :: thesis: contradiction
then ex k being Element of NAT st S₁[k] by SCMPDS_6:def 2;
then A4: ex k being Nat st S₁[k] ;
consider n being Nat such that
A5: S₁[n] and
A6: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A4);
reconsider n = n as Element of NAT by ORDINAL1:def 12;
set s2 = Comput ((P +* (stop I)),(Initialize s),n);
set P2 = P +* (stop I);
set Ig = ((IC (Comput ((P +* (stop I)),(Initialize s),n))),(succ (IC (Comput ((P +* (stop I)),(Initialize s),n))))) --> ((goto 1),(goto (- 1)));
reconsider P0 = (P +* (stop I)) +* (((IC (Comput ((P +* (stop I)),(Initialize s),n))),(succ (IC (Comput ((P +* (stop I)),(Initialize s),n))))) --> ((goto 1),(goto (- 1)))) as Instruction-Sequence of SCMPDS ;
reconsider P1 = (P +* (stop I)) +* (((IC (Comput ((P +* (stop I)),(Initialize s),n))),(succ (IC (Comput ((P +* (stop I)),(Initialize s),n))))) --> ((goto 1),(goto (- 1)))) as Instruction-Sequence of SCMPDS ;
reconsider P3 = (P +* (stop I)) +* ((IC (Comput ((P +* (stop I)),(Initialize s),n))),(goto 1)) as Instruction-Sequence of SCMPDS ;
reconsider P4 = P3 +* ((succ (IC (Comput ((P +* (stop I)),(Initialize s),n)))),(goto (- 1))) as Instruction-Sequence of SCMPDS ;
U: P0 = P4 by FUNCT_7:139;
A13: for m being Element of NAT st m < n holds
IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I) by A6;
A17: stop I c= P +* (stop I) by FUNCT_4:25;
stop I c= P3 by A5, FUNCT_4:25, FUNCT_7:89;
then A18: stop I c= P0 by U, A5, AFINSQ_1:73, FUNCT_7:89;
then XX: Comput (P0,(Initialize s),n) = Comput ((P +* (stop I)),(Initialize s),n) by A17, A13, SCMPDS_4:21;
DataPart (Initialize s) = DataPart (Initialize s)
.= DataPart s by A2, SCMPDS_4:8 ;
then I is_halting_on Initialize s,P0 by A1;
then A20: P0 +* (stop I) halts_on Initialize (Initialize s) by SCMPDS_6:def 3;
A21: not P0 halts_on Comput ((P +* (stop I)),(Initialize s),n) by SCMPDS_4:20;
P0 +* (stop I) = P0 by A18, FUNCT_4:98;
hence contradiction by A21, XX, A20, EXTPRO_1:22; :: thesis: verum