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 = (stop I) +* (Start-At 0 ,SCMPDS );
let s be State of SCMPDS ; :: according to SCMPDS_4:def 9 :: thesis: for n being Element of NAT st Initialize (stop I) c= s holds
IC (Comput (ProgramPart s),s,n) in dom (stop I)
let n be Element of NAT ; :: thesis: ( Initialize (stop I) c= s implies IC (Comput (ProgramPart s),s,n) in dom (stop I) )
defpred S1[ Nat] means not IC (Comput (ProgramPart s),s,c1) in dom (stop I);
dom (stop I) misses dom (Start-At 0 ,SCMPDS ) by Th54;
then A2: stop I c= (stop I) +* (Start-At 0 ,SCMPDS ) by FUNCT_4:33;
assume A3: Initialize (stop I) c= s ; :: thesis: IC (Comput (ProgramPart s),s,n) in dom (stop I)
then A4: stop I c= s by A2, XBOOLE_1:1;
assume not IC (Comput (ProgramPart s),s,n) in dom (stop I) ; :: thesis: contradiction
then A5: ex n being Nat st S1[n] ;
consider n being Nat such that
A6: S1[n] and
A7: for m being Nat st S1[m] holds
n <= m from NAT_1:sch 5(A5);
 reconsider n = n as Element of NAT by ORDINAL1:def 13;
A8: for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s),s,m) in dom (stop I) by A7;
set s2 = Comput (ProgramPart s),s,n;
set Ig = (IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1));
set s0 = s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)));
set s1 = (Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)));
set t1 = s +* (IC (Comput (ProgramPart s),s,n)),(goto 1);
set t2 = (s +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1));
set t3 = (Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1);
set t4 = ((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1));
((stop I) +* (Start-At 0 ,SCMPDS )) | NAT = stop I by Th58;
then A9: dom (stop I) = (dom ((stop I) +* (Start-At 0 ,SCMPDS ))) /\ NAT by RELAT_1:90;
ProgramPart s = ProgramPart (Comput (ProgramPart s),s,n) by AMI_1:123;
then ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) = ProgramPart ((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) by FUNCT_7:95;
then ProgramPart ((s +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1))) = ProgramPart (((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1))) by FUNCT_7:95;
then ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))) = ProgramPart (((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1))) by Th69;
then ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))) = ProgramPart ((Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))) by Th69;
then A10: ProgramPart (Comput (ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))))),(s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))),n) = ProgramPart ((Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))) by AMI_1:123;
A11: s +* (IC (Comput (ProgramPart s),s,n)),(goto 1),(s +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
not succ (IC (Comput (ProgramPart s),s,n)) in dom (stop I) by A6, AFINSQ_1:77;
then A12: not succ (IC (Comput (ProgramPart s),s,n)) in dom ((stop I) +* (Start-At 0 ,SCMPDS )) by A9, XBOOLE_0:def 4;
A13: (Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1),((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
Comput (ProgramPart s),s,n,(Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1) equal_outside NAT by FUNCT_7:93;
then Comput (ProgramPart s),s,n,((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1)) equal_outside NAT by A13, FUNCT_7:29;
then A15: Comput (ProgramPart s),s,n,(Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) equal_outside NAT by Th69;
s,s +* (IC (Comput (ProgramPart s),s,n)),(goto 1) equal_outside NAT by FUNCT_7:93;
then s,(s +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1)) equal_outside NAT by A11, FUNCT_7:29;
then s,s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) equal_outside NAT by Th69;
then A16: s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))),s equal_outside NAT by FUNCT_7:28;
not IC (Comput (ProgramPart s),s,n) in dom ((stop I) +* (Start-At 0 ,SCMPDS )) by A6, A9, XBOOLE_0:def 4;
then (stop I) +* (Start-At 0 ,SCMPDS ) c= s +* (IC (Comput (ProgramPart s),s,n)),(goto 1) by A3, FUNCT_7:91;
then (stop I) +* (Start-At 0 ,SCMPDS ) c= (s +* (IC (Comput (ProgramPart s),s,n)),(goto 1)) +* (succ (IC (Comput (ProgramPart s),s,n))),(goto (- 1)) by A12, FUNCT_7:91;
then A17: (stop I) +* (Start-At 0 ,SCMPDS ) c= s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) by Th69;
then stop I c= s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) by A2, XBOOLE_1:1;
then Comput (ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))))),(s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))),n, Comput (ProgramPart s),s,n equal_outside NAT by A16, A4, A8, Th67;
then Comput (ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))))),(s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))),n,(Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) equal_outside NAT by A15, FUNCT_7:29;
then A18: Comput (ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))))),(s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))),n = (Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) by A10, FUNCT_7:92;
A19: not ProgramPart ((Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))) halts_on (Comput (ProgramPart s),s,n) +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) by Th66;
Initialize (stop I) = (stop I) +* (Start-At 0 ,SCMPDS ) ;
then ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))) halts_on s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))) by A1, A17, AMI_1:def 26;
then ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))) halts_on Comput (ProgramPart (s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1))))),(s +* ((IC (Comput (ProgramPart s),s,n)),(succ (IC (Comput (ProgramPart s),s,n))) --> (goto 1),(goto (- 1)))),n by AMI_1:93;
hence contradiction by A18, A19, AMI_1:123; :: thesis: verum