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₁[ Nat] means not IC (Comput (P,s,c₁)) 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₁[n] ;
consider n being Nat such that
A4: S₁[n] and
A5: for m being Nat st S₁[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