let I be Program of SCMPDS; :: thesis: ( I is parahalting implies I is paraclosed )
assume A1: I is parahalting ; :: thesis: I is paraclosed
set IAt = Initialize (stop I);
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 9 :: thesis: for n being Element of NAT
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 the Instructions of SCMPDS -valued ManySortedSet of NAT st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I)
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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 13;
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 the Instructions of SCMPDS -valued ManySortedSet of NAT ;
reconsider P3 = P +* ((IC (Comput (P,s,n))),(goto 1)) as the Instructions of SCMPDS -valued ManySortedSet of NAT ;
reconsider P2 = P3 +* ((succ (IC (Comput (P,s,n)))),(goto (- 1))) as the Instructions of SCMPDS -valued ManySortedSet of NAT ;
reconsider P4 = P3 +* ((succ (IC (Comput (P,s,n)))),(goto (- 1))) as the Instructions of SCMPDS -valued ManySortedSet of NAT ;
U: P0 = P4 by FUNCT_7:141;
A9: not succ (IC (Comput (P,s,n))) in dom (stop I) by A4, AFINSQ_1:77;
A12: NPP s = NPP s ;
stop I c= P3 by A2, A4, FUNCT_7:91;
then stop I c= P4 by A9, FUNCT_7:91;
then A13: stop I c= P0 by U;
then NPP (Comput (P0,s,n)) = NPP (Comput (P,s,n)) by A12, A2, A6, Th67;
then XX: NPP (Comput (P0,s,n)) = NPP (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, AMISTD_2:69;
hence contradiction by A15; :: thesis: verum