let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS st ( for t being State of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t ) holds
I is_closed_on s
let I be Program of SCMPDS; :: thesis: ( ( for t being State of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t ) implies I is_closed_on s )
assume A1: for t being State of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t ; :: thesis: I is_closed_on s
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 COMPOS_1:125;
assume not I is_closed_on s ; :: thesis: contradiction
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 COMPOS_1:134;
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 COMPOS_1:134;
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 COMPOS_1:134;
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 COMPOS_1:134;
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));
((stop I) +* (Start-At (0,SCMPDS))) | NAT = stop I by COMPOS_1:133;
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 COMPOS_1:130;
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, 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 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 COMPOS_1:134;
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, COMPOS_1:138
.= 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 COMPOS_1:125;
(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 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, EXTPRO_1:22;
hence contradiction by A22, A7, AMI_1:123; :: thesis: verum