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 sI = (Initialize s) +* (stop I);
defpred S₁[ Nat] means not IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),$1) in dom (stop I);
A2: for a being Int_position holds s . a = ((Initialize s) +* (stop I)) . a by SCMPDS_5:19;
I1: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
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 ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n;
set Ig = (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1));
set s0 = ((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)));
set s1 = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)));
set t1 = ((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1);
set t2 = (((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1));
set t3 = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1);
set t4 = ((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1));
A6: ((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1),(((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) by AMI_1:123;
then (((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) | NAT = ((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) | NAT by FUNCT_7:95;
then ((((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1))) | NAT = (((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1))) | NAT by FUNCT_7:95;
then ProgramPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) = (((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1))) | NAT by SCMPDS_4:69;
then ProgramPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) = ProgramPart ((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) by SCMPDS_4:69;
then A7: ProgramPart (Comput (ProgramPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))),(((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))),n) = ProgramPart ((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) by AMI_1:123;
A8: (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1),((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1)) equal_outside NAT by FUNCT_7:93;
(Initialize s) +* (stop I),((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1) equal_outside NAT by FUNCT_7:93;
then (Initialize s) +* (stop I),(((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1)) equal_outside NAT by A6, FUNCT_7:29;
then A10: (Initialize s) +* (stop I),((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by SCMPDS_4:69;
then A11: ((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))),(Initialize s) +* (stop I) equal_outside NAT by FUNCT_7:28;
Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n,(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1) equal_outside NAT by FUNCT_7:93;
then Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n,((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1)) equal_outside NAT by A8, FUNCT_7:29;
then A12: Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n,(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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 ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m) in dom (stop I) by A5;
set IAt = (stop I) +* (Start-At 0 ,SCMPDS );
A14: Initialize (stop I) = (stop I) +* (Start-At 0 ,SCMPDS ) by COMPOS_1:def 31;
((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 ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)) in dom (stop I) by A4, AFINSQ_1:77;
then A16: not succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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;
Initialize (stop I) c= (Initialize s) +* (stop I) by I1, FUNCT_4:26;
then A18: stop I c= (Initialize s) +* (stop I) by A17, A14, XBOOLE_1:1;
not IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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= ((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1) by A14, I1, FUNCT_4:26, FUNCT_7:91;
then (stop I) +* (Start-At 0 ,SCMPDS ) c= (((Initialize s) +* (stop I)) +* (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(goto 1)) +* (succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))),(goto (- 1)) by A16, FUNCT_7:91;
then A19: (stop I) +* (Start-At 0 ,SCMPDS ) c= ((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) by SCMPDS_4:69;
then stop I c= ((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) by A17, XBOOLE_1:1;
then Comput (ProgramPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))),(((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))),n, Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n equal_outside NAT by A11, A18, A13, SCMPDS_4:67;
then Comput (ProgramPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))),(((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))),n,(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) equal_outside NAT by A12, FUNCT_7:29;
then A20: Comput (ProgramPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))),(((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))),n = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) by A7, FUNCT_7:92;
DataPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) = DataPart ((Initialize s) +* (stop I)) by A10, SCMPDS_4:24
.= DataPart s by A2, SCMPDS_4:23 ;
then I is_halting_on ((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) by A1;
then A21: ProgramPart ((Initialize (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))) +* (stop I)) halts_on (Initialize (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))) +* (stop I) by SCMPDS_6:def 3;
A22: not ProgramPart ((Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) halts_on (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) by SCMPDS_4:66;
I2: (Initialize (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))) +* (stop I) = (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) +* (Initialize (stop I)) by SCMPDS_4:5;
(Initialize (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))))) +* (stop I) = ((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) by A14, A19, I2, FUNCT_4:79;
then ProgramPart (((Initialize s) +* (stop I)) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1)))) halts_on (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) +* ((IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)),(succ (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n))) --> (goto 1),(goto (- 1))) by A21, A20, AMI_1:93;
hence contradiction by A22, A7, AMI_1:123; :: thesis: