let I be Program of SCM+FSA; :: thesis: ( I is parahalting implies I is paraclosed )
set IAt = Initialize I;
assume I is parahalting ; :: thesis: I is paraclosed
then A1: Initialize I is halting by Def3;
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 Initialize I 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 Initialize I c= s holds
IC (Comput (P,s,n)) in dom I )
assume A2: I c= P ; :: thesis: for n being Element of NAT st Initialize I c= s holds
IC (Comput (P,s,n)) in dom I
let n be Element of NAT ; :: thesis: ( Initialize I 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: Initialize I 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 +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))));
set s1 = (Comput (P,s,n)) +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))));
A8: ProgramPart s = ProgramPart (Comput (P,s,n)) by AMI_1:123;
set P0 = P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))));
A9: ProgramPart (Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),(s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),n)) = ProgramPart (s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))) by AMI_1:123
.= ProgramPart ((Comput (P,s,n)) +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))) by A8, FUNCT_7:95 ;
A10: s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))),s equal_outside NAT by FUNCT_7:28, FUNCT_7:93;
A11: Comput (P,s,n),(Comput (P,s,n)) +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) equal_outside NAT by FUNCT_7:93;
(Initialize I) | NAT = I by COMPOS_1:144;
then dom I = (dom (Initialize I)) /\ NAT by RELAT_1:90;
then not IC (Comput (P,s,n)) in dom (Initialize I) by A5, XBOOLE_0:def 4;
then A12: Initialize I c= s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A3, FUNCT_7:91;
A13: I c= P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A5, A2, FUNCT_7:91;
then Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),(s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),n), Comput (P,s,n) equal_outside NAT by A10, A7, AMISTD_2:66, A2;
then Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),(s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),n),(Comput (P,s,n)) +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) equal_outside NAT by A11, FUNCT_7:29;
then A14: Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),(s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),n) = (Comput (P,s,n)) +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A9, FUNCT_7:92;
A15: not P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on (Comput (P,s,n)) +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by Th20;
ProgramPart (Initialize I) = (ProgramPart I) +* (ProgramPart (Start-At (0,SCM+FSA))) by FUNCT_4:75
.= (ProgramPart I) +* {} by COMPOS_1:27
.= ProgramPart I by FUNCT_4:22
.= I by RELAT_1:209 ;
then P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on s +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A1, A12, EXTPRO_1:def 10, A13;
then 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 +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),n) by EXTPRO_1:22;
hence contradiction by A14, A15; :: thesis: verum