let I be Program of SCMPDS ; :: thesis: ( I is parahalting implies I is paraclosed )
assume A1: I is parahalting ; :: thesis: I is paraclosed
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) )
assume A2: Initialized (stop I) c= s ; :: thesis: IC (Computation s,n) in dom (stop I)
defpred S₁[ Nat] means not IC (Computation s,c₁) in dom (stop I);
assume not IC (Computation 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: not Next (IC (Computation s,n)) in dom (stop I) by A4, Th71;
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 ;
set IAt = (stop I) +* (Start-At (inspos 0 ));
dom (stop I) misses dom (Start-At (inspos 0 )) by Th54;
then A7: stop I c= (stop I) +* (Start-At (inspos 0 )) by FUNCT_4:33;
A8: IC (Computation s,n) in NAT by AMI_1:def 4;
Initialized (stop I) = (stop I) +* (Start-At (inspos 0 )) ;
then A10: (stop I) +* (Start-At (inspos 0 )) is halting by A1;
((stop I) +* (Start-At (inspos 0 ))) | NAT = stop I by Th58;
then A11: dom (stop I) = (dom ((stop I) +* (Start-At (inspos 0 )))) /\ NAT by RELAT_1:90;
then A12: not IC (Computation s,n) in dom ((stop I) +* (Start-At (inspos 0 ))) by A4, A8, XBOOLE_0:def 4;
A13: not Next (IC (Computation s,n)) in dom ((stop I) +* (Start-At (inspos 0 ))) by A6, A11, XBOOLE_0:def 4;
(stop I) +* (Start-At (inspos 0 )) c= s +* (IC (Computation s,n)),(goto 1) by A2, A12, 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 A13, FUNCT_7:91;
then A14: (stop I) +* (Start-At (inspos 0 )) c= s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) by Th69;
then A15: s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) is halting by A10, AMI_1:def 26;
A16: s,s +* (IC (Computation s,n)),(goto 1) equal_outside NAT by A8, FUNCT_7:93;
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;
then s,(s +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1)) equal_outside NAT by A16, 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 A17: s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))),s equal_outside NAT by FUNCT_7:28;
A18: stop I c= s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) by A7, A14, XBOOLE_1:1;
A19: stop I c= s by A2, A7, XBOOLE_1:1;
for m being Element of NAT st m < n holds
IC (Computation s,m) in dom (stop I) by A5;
then A20: Computation (s +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1)))),n, Computation s,n equal_outside NAT by A17, A18, A19, Th67;
A21: Computation s,n,(Computation s,n) +* (IC (Computation s,n)),(goto 1) equal_outside NAT by A8, FUNCT_7:93;
(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;
then Computation s,n,((Computation s,n) +* (IC (Computation s,n)),(goto 1)) +* (Next (IC (Computation s,n))),(goto (- 1)) equal_outside NAT by A21, FUNCT_7:29;
then B22: 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 | 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 (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;
then A23: 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 B22, A20, FUNCT_7:29, FUNCT_7:92;
not (Computation s,n) +* ((IC (Computation s,n)),(Next (IC (Computation s,n))) --> (goto 1),(goto (- 1))) is halting by Th66;
hence contradiction by A15, A23, AMI_1:93; :: thesis: verum