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 S_{1}[ 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

then ex k being Nat st S_{1}[k]
by SCMPDS_6:def 2;

then A3: ex k being Nat st S_{1}[k]
;

consider n being Nat such that

A4: S_{1}[n]
and

A5: for m being Nat st S_{1}[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

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 S

A2: for a being Int_position holds s . a = (Initialize s) . a

proof

assume
not I is_closed_on s,P
; :: thesis: contradiction
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;not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

hence s . a = (Initialize s) . a by FUNCT_4:11; :: thesis: verum

then ex k being Nat st S

then A3: ex k being Nat st S

consider n being Nat such that

A4: S

A5: for m being Nat st S

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