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 (inspos 0 ));
let s be State of SCMPDS ; :: according to SCMPDS_4:def 9 :: thesis: for n being Element of NAT st Initialized (stop I) c= s holds
IC (Computation s,n) in dom (stop I)
let n be Element of NAT ; :: thesis: ( Initialized (stop I) c= s implies IC (Computation s,n) in dom (stop I) )
defpred S₁[ Nat] means not IC (Computation s,c₁) in dom (stop I);
dom (stop I) misses dom (Start-At (inspos 0 )) by Th54;
then A2: stop I c= (stop I) +* (Start-At (inspos 0 )) by FUNCT_4:33;
assume A3: Initialized (stop I) c= s ; :: thesis: IC (Computation s,n) in dom (stop I)
then A4: stop I c= s by A2, XBOOLE_1:1;
assume not IC (Computation 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 (Computation s,m) in dom (stop I) by A7;
set s2 = Computation s,n;
set Ig = (IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1));
set s0 = s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)));
set s1 = (Computation s,n) +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)));
set t1 = s +* (IC (Computation s,n)),(goto 1);
set t2 = (s +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1));
set t3 = (Computation s,n) +* (IC (Computation s,n)),(goto 1);
set t4 = ((Computation s,n) +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1));
set IL = NAT ;
((stop I) +* (Start-At (inspos 0 ))) | NAT = stop I by Th58;
then A9: dom (stop I) = (dom ((stop I) +* (Start-At (inspos 0 )))) /\ NAT by RELAT_1:90;
s | NAT = (Computation s,n) | NAT by AMI_1:123;
then (s +* (IC (Computation s,n)),(goto 1)) | NAT = ((Computation s,n) +* (IC (Computation s,n)),(goto 1)) | NAT by FUNCT_7:95;
then ((s +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1))) | NAT = (((Computation s,n) +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1))) | NAT by FUNCT_7:95;
then (s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))) | NAT = (((Computation s,n) +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1))) | NAT by Th69;
then (s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))) | NAT = ((Computation s,n) +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))) | NAT by Th69;
then A10: (Computation (s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))),n) | NAT = ((Computation s,n) +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))) | NAT by AMI_1:123;
A11: s +* (IC (Computation s,n)),(goto 1),(s +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
not Next (IC (Computation s,n)) in dom (stop I) by A6, Th71;
then A12: not Next (IC (Computation s,n)) in dom ((stop I) +* (Start-At (inspos 0 ))) by A9, XBOOLE_0:def 4;
A13: (Computation s,n) +* (IC (Computation s,n)),(goto 1),((Computation s,n) +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
A14: IC (Computation s,n) in NAT by AMI_1:def 4;
then Computation s,n,(Computation s,n) +* (IC (Computation s,n)),(goto 1) equal_outside NAT by FUNCT_7:93;
then Computation s,n,((Computation s,n) +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1)) equal_outside NAT by A13, FUNCT_7:29;
then A15: Computation s,n,(Computation s,n) +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) equal_outside NAT by Th69;
s,s +* (IC (Computation s,n)),(goto 1) equal_outside NAT by A14, FUNCT_7:93;
then s,(s +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1)) equal_outside NAT by A11, FUNCT_7:29;
then s,s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) equal_outside NAT by Th69;
then A16: s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))),s equal_outside NAT by FUNCT_7:28;
not IC (Computation s,n) in dom ((stop I) +* (Start-At (inspos 0 ))) by A6, A14, A9, XBOOLE_0:def 4;
then (stop I) +* (Start-At (inspos 0 )) c= s +* (IC (Computation s,n)),(goto 1) by A3, FUNCT_7:91;
then (stop I) +* (Start-At (inspos 0 )) c= (s +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1)) by A12, FUNCT_7:91;
then A17: (stop I) +* (Start-At (inspos 0 )) c= s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) by Th69;
then stop I c= s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) by A2, XBOOLE_1:1;
then Computation (s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))),n, Computation s,n equal_outside NAT by A16, A4, A8, Th67;
then A18: Computation (s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))),n = (Computation s,n) +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) by A15, A10, FUNCT_7:29, FUNCT_7:92;
A19: not (Computation s,n) +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) is halting by Th66;
Initialized (stop I) = (stop I) +* (Start-At (inspos 0 )) ;
then s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) is halting by A1, A17, AMI_1:def 26;
hence contradiction by A18, A19, AMI_1:93; :: thesis: verum