let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS
for I being Program of 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 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 ; :: 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 S1[ 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 Nat st S1[k] by SCMPDS_6:def 2;
then A3: ex k being Nat st S1[k] ;
consider n being Nat such that
A4: S1[n] and
A5: for m being Nat st S1[m] holds
n <= m from NAT_1:sch 5(A3);
 reconsider n = n as Nat ;
set s2 = Comput ((P +* (stop I)),(Initialize s),n);
set P2 = P +* (stop I);
set Ig = ((IC (Comput ((P +* (stop I)),(Initialize s),n))),((IC (Comput ((P +* (stop I)),(Initialize s),n))) + 1)) --> ((goto 1),(goto (- 1)));
reconsider P0 = (P +* (stop I)) +* (((IC (Comput ((P +* (stop I)),(Initialize s),n))),((IC (Comput ((P +* (stop I)),(Initialize s),n))) + 1)) --> ((goto 1),(goto (- 1)))) as Instruction-Sequence of SCMPDS ;
reconsider P1 = (P +* (stop I)) +* (((IC (Comput ((P +* (stop I)),(Initialize s),n))),((IC (Comput ((P +* (stop I)),(Initialize s),n))) + 1)) --> ((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 +* (((IC (Comput ((P +* (stop I)),(Initialize s),n))) + 1),(goto (- 1))) as Instruction-Sequence of SCMPDS ;
A6: P0 = P4 by FUNCT_7:139;
A7: for m being Nat st m < n holds
IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I) by A5;
A8: stop I c= P +* (stop I) by FUNCT_4:25;
stop I c= P3 by A4, FUNCT_4:25, FUNCT_7:89;
then A9: stop I c= P0 by A6, A4, AFINSQ_1:73, FUNCT_7:89;
then A10: Comput (P0,(Initialize s),n) = Comput ((P +* (stop I)),(Initialize s),n) by A8, A7, SCMPDS_4:21;
DataPart (Initialize s) = DataPart s by A2, SCMPDS_4:8;
then I is_halting_on Initialize s,P0 by A1;
then A11: P0 +* (stop I) halts_on Initialize (Initialize s) by SCMPDS_6:def 3;
A12: not P0 halts_on Comput ((P +* (stop I)),(Initialize s),n) by SCMPDS_4:20;
P0 +* (stop I) = P0 by A9, FUNCT_4:98;
hence contradiction by A12, A10, A11, EXTPRO_1:22; :: thesis: verum