let I be Program of SCM+FSA; :: thesis: ( I is parahalting implies I is paraclosed )
set IAt = Start-At (0,SCM+FSA);
assume Z: I is parahalting ; :: thesis: I is paraclosed
let s be State of SCM+FSA; :: according to SCMFSA6B:def 2 :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( I c= P implies for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I )
assume A2: I c= P ; :: thesis: for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I
let n be Element of NAT ; :: thesis: ( Start-At (0,SCM+FSA) c= s implies IC (Comput (P,s,n)) in dom I )
defpred S₁[ Nat] means not IC (Comput (P,s,c₁)) in dom I;
assume A3: Start-At (0,SCM+FSA) c= s ; :: thesis: IC (Comput (P,s,n)) in dom I
assume not IC (Comput (P,s,n)) in dom I ; :: thesis: contradiction
then A4: ex n being Nat st S₁[n] ;
consider n being Nat such that
A5: S₁[n] and
A6: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A4);
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A7: for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I by A6;
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)))));
A10: NPP s = NPP s ;
A12: Start-At (0,SCM+FSA) c= s by A3;
A13: I c= P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A5, A2, FUNCT_7:91;
then B14: NPP (Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),s,n)) = NPP (Comput (P,s,n)) by A10, A7, A2, AMISTD_2:66;
not P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on Comput (P,s,n) by Lm45;
then B15: 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 B14, AMISTD_2:69;
P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on s by A12, A13, Z, Def3;
hence contradiction by B15, EXTPRO_1:22; :: thesis: verum