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 SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b₁ being set holds
( not I c= b₁ or for b₂ being Element of NAT holds IC (Comput (b₁,s,b₂)) in K306(NAT,I) )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in K306(NAT,I) )
assume A2: I c= P ; :: thesis: for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in K306(NAT,I)
let n be Element of NAT ; :: thesis: IC (Comput (P,s,n)) in K306(NAT,I)
defpred S₁[ Nat] means not IC (Comput (P,s,c₁)) in dom I;
assume not IC (Comput (P,s,n)) in dom 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 I by A5;
set s2 = Comput (P,s,n);
set s0 = s;
set s1 = Comput (P,s,n);
set P0 = P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))));
A7: I c= P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A4, A2, FUNCT_7:89;
then A8: Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),s,n) = Comput (P,s,n) by A6, A2, AMISTD_2:10;
A9: not P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),s,n) by A8, Lm1;
P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on s by A7, A1, AMISTD_1:def 11;
hence contradiction by A9, EXTPRO_1:22; :: thesis: verum