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 (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),$1) in dom (stop I);
A2: for a being Int_position holds s . a = (s +* (Initialized (stop I))) . a by SCMPDS_5:19;
assume not I is_closed_on s ; :: thesis:
then ex k being Element of NAT st S₁[k] by SCMPDS_6:def 2;
then A3: ex k being Nat st S₁[k] ;
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;
set s2 = Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n;
set Ig = (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1));
set s0 = (s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)));
set s1 = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)));
set t1 = (s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1);
set t2 = ((s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1));
set t3 = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1);
set t4 = ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1));
A6: (s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1),((s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
(s +* (Initialized (stop I))) | NAT = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) | NAT by AMI_1:123;
then ((s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) | NAT = ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) | NAT by FUNCT_7:95;
then (((s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1))) | NAT = (((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1))) | NAT by FUNCT_7:95;
then ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT = (((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1))) | NAT by SCMPDS_4:69;
then ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT = ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT by SCMPDS_4:69;
then A7: (Comput (ProgramPart ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))))),((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n) | NAT = ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) | NAT by AMI_1:123;
A8: (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
s +* (Initialized (stop I)),(s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1) equal_outside NAT by FUNCT_7:93;
then s +* (Initialized (stop I)),((s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by A6, FUNCT_7:29;
then A10: s +* (Initialized (stop I)),(s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by SCMPDS_4:69;
then A11: (s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))),s +* (Initialized (stop I)) equal_outside NAT by FUNCT_7:28;
Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n,(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1) equal_outside NAT by FUNCT_7:93;
then Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n,((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1)) equal_outside NAT by A8, FUNCT_7:29;
then A12: Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n,(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by SCMPDS_4:69;
A13: for m being Element of NAT st m < n holds
IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),m) in dom (stop I) by A5;
set IAt = (stop I) +* (Start-At 0 ,SCMPDS );
A14: Initialized (stop I) = (stop I) +* (Start-At 0 ,SCMPDS ) by SCMPDS_4:def 2;
((stop I) +* (Start-At 0 ,SCMPDS )) | NAT = stop I by SCMPDS_4:58;
then A15: dom (stop I) = (dom ((stop I) +* (Start-At 0 ,SCMPDS ))) /\ NAT by RELAT_1:90;
not succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)) in dom (stop I) by A4, SCMPDS_4:71;
then A16: not succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)) in dom ((stop I) +* (Start-At 0 ,SCMPDS )) by A15, XBOOLE_0:def 4;
dom (stop I) misses dom (Start-At 0 ,SCMPDS ) by SCMPDS_4:54;
then A17: stop I c= (stop I) +* (Start-At 0 ,SCMPDS ) by FUNCT_4:33;
Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
then A18: stop I c= s +* (Initialized (stop I)) by A17, A14, XBOOLE_1:1;
not IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) in dom ((stop I) +* (Start-At 0 ,SCMPDS )) by A4, A15, XBOOLE_0:def 4;
then (stop I) +* (Start-At 0 ,SCMPDS ) c= (s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1) by A14, FUNCT_4:26, FUNCT_7:91;
then (stop I) +* (Start-At 0 ,SCMPDS ) c= ((s +* (Initialized (stop I))) +* (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))),(goto (- 1)) by A16, FUNCT_7:91;
then A19: (stop I) +* (Start-At 0 ,SCMPDS ) c= (s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by SCMPDS_4:69;
then stop I c= (s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A17, XBOOLE_1:1;
then Comput (ProgramPart ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))))),((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n, Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n equal_outside NAT by A11, A18, A13, SCMPDS_4:67;
then Comput (ProgramPart ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))))),((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n,(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by A12, FUNCT_7:29;
then A20: Comput (ProgramPart ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))))),((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))),n = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A7, FUNCT_7:92;
DataPart ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) = DataPart (s +* (Initialized (stop I))) by A10, SCMPDS_4:24
.= DataPart s by A2, SCMPDS_4:23 ;
then I is_halting_on (s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A1;
then A21: ProgramPart (((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) +* (Initialized (stop I))) halts_on ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) +* (Initialized (stop I)) by SCMPDS_6:def 3;
A22: not ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) halts_on (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by SCMPDS_4:66;
((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) +* (Initialized (stop I)) = (s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A14, A19, FUNCT_4:79;
then ProgramPart ((s +* (Initialized (stop I))) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1)))) halts_on (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n) +* ((IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n)),(succ (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),n))) --> (goto 1),(goto (- 1))) by A21, A20, AMI_1:93;
hence contradiction by A20, A22, AMI_1:144; :: thesis: