let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS st ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st DataPart t = DataPart s holds
I is_halting_on t,Q ) implies I is_closed_on s,P )
assume A1: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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:59;
hence s . a = (Initialize s) . a by FUNCT_4:12; :: 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 13;
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)));
set s0 = Initialize s;
set s1 = Comput ((P +* (stop I)),(Initialize s),n);
set t1 = Initialize s;
set t2 = Initialize s;
set t3 = Comput ((P +* (stop I)),(Initialize s),n);
set t4 = Comput ((P +* (stop I)),(Initialize s),n);
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 the Instructions of SCMPDS -valued ManySortedSet of NAT ;
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 the Instructions of SCMPDS -valued ManySortedSet of NAT ;
reconsider P3 = (P +* (stop I)) +* ((IC (Comput ((P +* (stop I)),(Initialize s),n))),(goto 1)) as the Instructions of SCMPDS -valued ManySortedSet of NAT ;
reconsider P4 = P3 +* ((succ (IC (Comput ((P +* (stop I)),(Initialize s),n)))),(goto (- 1))) as the Instructions of SCMPDS -valued ManySortedSet of NAT ;
U: P0 = P4 by FUNCT_7:141;
B9: not succ (IC (Comput ((P +* (stop I)),(Initialize s),n))) in dom (stop I) by A5, AFINSQ_1:77;
A11: NPP (Initialize s) = NPP (Initialize s) ;
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:26;
not IC (Comput ((P +* (stop I)),(Initialize s),n)) in dom (stop I) by A5;
then stop I c= P3 by FUNCT_4:26, FUNCT_7:91;
then stop I c= P4 by B9, FUNCT_7:91;
then A18: stop I c= P0 by U;
then NPP (Comput (P0,(Initialize s),n)) = NPP (Comput ((P +* (stop I)),(Initialize s),n)) by A11, A17, A13, SCMPDS_4:67;
then XX: NPP (Comput (P0,(Initialize s),n)) = NPP (Comput ((P +* (stop I)),(Initialize s),n)) ;
DataPart (Initialize s) = DataPart (Initialize s)
.= DataPart s by A2, SCMPDS_4:23 ;
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:66;
P0 +* (stop I) = P0 by A18, FUNCT_4:104;
then P0 halts_on Comput (P0,(Initialize s),n) by A20, EXTPRO_1:22;
then P0 halts_on Comput ((P +* (stop I)),(Initialize s),n) by XX, AMISTD_2:69;
hence contradiction by A21; :: thesis: verum