let I be Program of ; :: thesis: ( I is parahalting implies I is paraclosed )

assume A1: I is parahalting ; :: thesis: I is paraclosed

let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 6 :: thesis: for n being Nat

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I)

let n be Nat; :: thesis: for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I)

let P be Instruction-Sequence of SCMPDS; :: thesis: ( stop I c= P implies IC (Comput (P,s,n)) in dom (stop I) )

defpred S_{1}[ Nat] means not IC (Comput (P,s,c_{1})) in dom (stop I);

assume A2: stop I c= P ; :: thesis: IC (Comput (P,s,n)) in dom (stop I)

assume not IC (Comput (P,s,n)) in dom (stop I) ; :: thesis: contradiction

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

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 ;

A6: for m being Nat st m < n holds

IC (Comput (P,s,m)) in dom (stop I) by A5;

set s2 = Comput (P,s,n);

set Ig = ((IC (Comput (P,s,n))),((IC (Comput (P,s,n))) + 1)) --> ((goto 1),(goto (- 1)));

reconsider P0 = P +* (((IC (Comput (P,s,n))),((IC (Comput (P,s,n))) + 1)) --> ((goto 1),(goto (- 1)))) as Instruction-Sequence of SCMPDS ;

reconsider P3 = P +* ((IC (Comput (P,s,n))),(goto 1)) as Instruction-Sequence of SCMPDS ;

reconsider P2 = P3 +* (((IC s) + 12),(goto (- 1))) as Instruction-Sequence of SCMPDS ;

reconsider P4 = P3 +* (((IC (Comput (P,s,n))) + 1),(goto (- 1))) as Instruction-Sequence of SCMPDS ;

A7: P0 = P4 by FUNCT_7:139;

stop I c= P3 by A2, A4, FUNCT_7:89;

then A8: stop I c= P0 by A7, A4, AFINSQ_1:73, FUNCT_7:89;

then A9: Comput (P0,s,n) = Comput (P,s,n) by A2, A6, Th19;

not P0 halts_on Comput (P,s,n) by Th18;

hence contradiction by A1, A8, A9, EXTPRO_1:22; :: thesis: verum

assume A1: I is parahalting ; :: thesis: I is paraclosed

let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 6 :: thesis: for n being Nat

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I)

let n be Nat; :: thesis: for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I)

let P be Instruction-Sequence of SCMPDS; :: thesis: ( stop I c= P implies IC (Comput (P,s,n)) in dom (stop I) )

defpred S

assume A2: stop I c= P ; :: thesis: IC (Comput (P,s,n)) in dom (stop I)

assume not IC (Comput (P,s,n)) in dom (stop I) ; :: thesis: contradiction

then A3: ex n 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 ;

A6: for m being Nat st m < n holds

IC (Comput (P,s,m)) in dom (stop I) by A5;

set s2 = Comput (P,s,n);

set Ig = ((IC (Comput (P,s,n))),((IC (Comput (P,s,n))) + 1)) --> ((goto 1),(goto (- 1)));

reconsider P0 = P +* (((IC (Comput (P,s,n))),((IC (Comput (P,s,n))) + 1)) --> ((goto 1),(goto (- 1)))) as Instruction-Sequence of SCMPDS ;

reconsider P3 = P +* ((IC (Comput (P,s,n))),(goto 1)) as Instruction-Sequence of SCMPDS ;

reconsider P2 = P3 +* (((IC s) + 12),(goto (- 1))) as Instruction-Sequence of SCMPDS ;

reconsider P4 = P3 +* (((IC (Comput (P,s,n))) + 1),(goto (- 1))) as Instruction-Sequence of SCMPDS ;

A7: P0 = P4 by FUNCT_7:139;

stop I c= P3 by A2, A4, FUNCT_7:89;

then A8: stop I c= P0 by A7, A4, AFINSQ_1:73, FUNCT_7:89;

then A9: Comput (P0,s,n) = Comput (P,s,n) by A2, A6, Th19;

not P0 halts_on Comput (P,s,n) by Th18;

hence contradiction by A1, A8, A9, EXTPRO_1:22; :: thesis: verum