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 0 -started State of SCMPDS; :: according to SCMPDS_4:def 9 :: thesis: for n being Element of NAT st stop I c= s holds
IC (Comput ((ProgramPart s),s,n)) in dom (stop I)
let n be Element of NAT ; :: thesis: ( stop I c= s implies IC (Comput ((ProgramPart s),s,n)) in dom (stop I) )
defpred S₁[ Nat] means not IC (Comput ((ProgramPart s),s,c₁)) in dom (stop I);
assume A3: stop I c= s ; :: thesis: IC (Comput ((ProgramPart s),s,n)) in dom (stop I)
assume not IC (Comput ((ProgramPart s),s,n)) in dom (stop I) ; :: thesis: contradiction
then A5: ex n being Nat st S₁[n] ;
consider n being Nat such that
A6: S₁[n] and
A7: for m being Nat st S₁[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)));
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 COMPOS_1:134;
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 COMPOS_1:134;
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;
A12: not succ (IC (Comput ((ProgramPart s),s,n))) in dom (stop I) by A6, AFINSQ_1:77;
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 COMPOS_1:134;
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 COMPOS_1:134;
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;
stop I c= s +* ((IC (Comput ((ProgramPart s),s,n))),(goto 1)) by A3, A6, FUNCT_7:91;
then stop I 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 c= s +* (((IC (Comput ((ProgramPart s),s,n))),(succ (IC (Comput ((ProgramPart s),s,n))))) --> ((goto 1),(goto (- 1)))) by COMPOS_1:134;
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, A3, 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;
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, Def10;
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 EXTPRO_1:22;
hence contradiction by A18, A19, AMI_1:123; :: thesis: verum