let s be State of SCMPDS ; :: thesis:
let I be Program of SCMPDS ; :: thesis:
assume A1: for t being State of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t ; :: thesis:
set pI = stop I;
set II = Initialized (stop I);
set sI = s +* (Initialized (stop I));
defpred S₁[ Nat] means not IC (Computation (s +* (Initialized (stop I))),$1) in dom (stop I);
assume not I is_closed_on s ; :: thesis:
then ex k being Element of NAT st S₁[k] by SCMPDS_6:def 2;
then A2: ex k being Nat st S₁[k] ;
consider n being Nat such that
A3: S₁[n] and
A4: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A2);
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A5: not Next (IC (Computation (s +* (Initialized (stop I))),n)) in dom (stop I) by A3, SCMPDS_4:71;
set s2 = Computation (s +* (Initialized (stop I))),n;
set Ig = (IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1));
set s0 = (s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)));
set s1 = (Computation (s +* (Initialized (stop I))),n) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)));
set t1 = (s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1);
set t2 = ((s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1));
set t3 = (Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1);
set t4 = ((Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1));
set IL = NAT ;
set IAt = (stop I) +* (Start-At (inspos 0 ));
dom (stop I) misses dom (Start-At (inspos 0 )) by SCMPDS_4:54;
then A6: stop I c= (stop I) +* (Start-At (inspos 0 )) by FUNCT_4:33;
A7: ( IC (Computation (s +* (Initialized (stop I))),n) in NAT & Next (IC (Computation (s +* (Initialized (stop I))),n)) in NAT ) by AMI_1:def 4;
A8: Initialized (stop I) = (stop I) +* (Start-At (inspos 0 )) by SCMPDS_4:def 2;
((stop I) +* (Start-At (inspos 0 ))) | NAT = stop I by SCMPDS_4:58;
then A9: dom (stop I) = (dom ((stop I) +* (Start-At (inspos 0 )))) /\ NAT by RELAT_1:90;
then A10: not IC (Computation (s +* (Initialized (stop I))),n) in dom ((stop I) +* (Start-At (inspos 0 ))) by A3, A7, XBOOLE_0:def 4;
A11: not Next (IC (Computation (s +* (Initialized (stop I))),n)) in dom ((stop I) +* (Start-At (inspos 0 ))) by A5, A9, XBOOLE_0:def 4;
A12: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
(stop I) +* (Start-At (inspos 0 )) c= (s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1) by A8, A10, FUNCT_4:26, FUNCT_7:91;
then (stop I) +* (Start-At (inspos 0 )) c= ((s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1)) by A11, FUNCT_7:91;
then A13: (stop I) +* (Start-At (inspos 0 )) c= (s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by SCMPDS_4:69;
A14: s +* (Initialized (stop I)),(s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1) equal_outside NAT by A7, FUNCT_7:93;
(s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1),((s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
then s +* (Initialized (stop I)),((s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by A14, FUNCT_7:29;
then A15: s +* (Initialized (stop I)),(s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by SCMPDS_4:69;
then A16: (s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))),s +* (Initialized (stop I)) equal_outside NAT by FUNCT_7:28;
A17: for a being Int_position holds s . a = (s +* (Initialized (stop I))) . a by SCMPDS_5:19;
DataPart ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) = DataPart (s +* (Initialized (stop I))) by A15, SCMPDS_4:24
.= DataPart s by A17, SCMPDS_4:23 ;
then I is_halting_on (s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A1;
then A18: ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) +* (Initialized (stop I)) is halting by SCMPDS_6:def 3;
A19: ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) +* (Initialized (stop I)) = (s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A8, A13, FUNCT_4:79;
A20: stop I c= (s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A6, A13, XBOOLE_1:1;
A21: stop I c= s +* (Initialized (stop I)) by A6, A8, A12, XBOOLE_1:1;
for m being Element of NAT st m < n holds
IC (Computation (s +* (Initialized (stop I))),m) in dom (stop I) by A4;
then A22: Computation ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n, Computation (s +* (Initialized (stop I))),n equal_outside NAT by A16, A20, A21, SCMPDS_4:67;
A23: Computation (s +* (Initialized (stop I))),n,(Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1) equal_outside NAT by A7, FUNCT_7:93;
(Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1),((Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
then Computation (s +* (Initialized (stop I))),n,((Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by A23, FUNCT_7:29;
then Computation (s +* (Initialized (stop I))),n,(Computation (s +* (Initialized (stop I))),n) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by SCMPDS_4:69;
then A24: Computation ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n,(Computation (s +* (Initialized (stop I))),n) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by A22, FUNCT_7:29;
(s +* (Initialized (stop I))) | NAT = (Computation (s +* (Initialized (stop I))),n) | NAT by AMI_1:123;
then ((s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) | NAT = ((Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) | NAT by FUNCT_7:95;
then (((s +* (Initialized (stop I))) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1))) | NAT = (((Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1))) | NAT by FUNCT_7:95;
then ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT = (((Computation (s +* (Initialized (stop I))),n) +* (IC (Computation (s +* (Initialized (stop I))),n)),(goto 1)) +* (Next (IC (Computation (s +* (Initialized (stop I))),n))),(goto (- 1))) | NAT by SCMPDS_4:69;
then ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT = ((Computation (s +* (Initialized (stop I))),n) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT by SCMPDS_4:69;
then (Computation ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n) | NAT = ((Computation (s +* (Initialized (stop I))),n) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT by AMI_1:123;
then A25: Computation ((s +* (Initialized (stop I))) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n = (Computation (s +* (Initialized (stop I))),n) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A24, FUNCT_7:92;
not (Computation (s +* (Initialized (stop I))),n) +* ((IC (Computation (s +* (Initialized (stop I))),n)),(Next (IC (Computation (s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) is halting by SCMPDS_4:66;
hence contradiction by A18, A19, A25, AMI_1:93; :: thesis: