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 Element of 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 Element of 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 Element of NAT by ORDINAL1:def 12;
A6: for m being Element of 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))),(succ (IC (Comput (P,s,n))))) --> ((goto 1),(goto (- 1)));
reconsider P0 = P +* (((IC (Comput (P,s,n))),(succ (IC (Comput (P,s,n))))) --> ((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 +* ((succ (IC (Comput (P,s,n)))),(goto (- 1))) as Instruction-Sequence of SCMPDS ;
reconsider P4 = P3 +* ((succ (IC (Comput (P,s,n)))),(goto (- 1))) as Instruction-Sequence of SCMPDS ;
U: P0 = P4 by FUNCT_7:139;
A9: not succ (IC (Comput (P,s,n))) in dom (stop I) by A4, AFINSQ_1:73;
stop I c= P3 by A2, A4, FUNCT_7:89;
then stop I c= P4 by A9, FUNCT_7:89;
then A13: stop I c= P0 by U;
then Comput (P0,s,n) = Comput (P,s,n) by A2, A6, Th67;
then XX: Comput (P0,s,n) = Comput (P,s,n) ;
A15: not P0 halts_on Comput (P,s,n) by Th66;
P0 halts_on s by A1, A13, Def10;
then P0 halts_on Comput (P0,s,n) by EXTPRO_1:22;
then P0 halts_on Comput (P,s,n) by XX;
hence contradiction by A15; :: thesis: verum