let p be autonomic FinPartState of SCMPDS; :: thesis: ( DataPart p <> {} implies IC SCMPDS in dom p )
assume DataPart p <> {} ; :: thesis: IC SCMPDS in dom p
then A1: dom (DataPart p) <> {} ;
assume A2: not IC SCMPDS in dom p ; :: thesis: contradiction
not p is autonomic

proof

consider il being Element of NAT \ (dom p);
consider d1 being Element of dom (DataPart p);
A3: d1 in dom (DataPart p) by A1;
dom (DataPart p) c= the carrier of SCMPDS by RELAT_1:def 18;
then reconsider d1 = d1 as Element of SCMPDS by A3;
not NAT c= dom p ;
then A4: NAT \ (dom p) <> {} by XBOOLE_1:37;
then il is Element of NAT by XBOOLE_0:def 5;
then reconsider il = il as Element of NAT ;
not il in dom p by A4, XBOOLE_0:def 5;
then A5: dom p misses {il} by ZFMISC_1:56;
dom (DataPart p) c= SCM-Data-Loc by RELAT_1:87, SCMPDS_2:100;
then reconsider d1 = d1 as Int_position by A3, SCMPDS_2:9;
A6: dom (Start-At (il,SCMPDS)) = {(IC SCMPDS)} by FUNCOP_1:19;
then A7: IC SCMPDS in dom (Start-At (il,SCMPDS)) by TARSKI:def 1;
il <> IC SCMPDS by COMPOS_1:3;
then A8: not il in dom (Start-At (il,SCMPDS)) by A6, TARSKI:def 1;
A9: dom p misses {(IC SCMPDS)} by A2, ZFMISC_1:56;
set p2 = p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)));
set p1 = p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)));
consider s1 being State of SCMPDS such that
A10: p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) c= s1 by PBOOLE:156;
consider s2 being State of SCMPDS such that
A11: p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) c= s2 by PBOOLE:156;
take s1 ; :: according to EXTPRO_1:def 9 :: thesis: ex b₁ being set st
( p c= s1 & p c= b₁ & not for b₂ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₂)) | (proj1 p) = (Comput ((ProgramPart b₁),b₁,b₂)) | (proj1 p) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 p) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 p) )
dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) = (dom (il .--> (d1 := 0))) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1
.= (dom (il .--> (d1 := 0))) \/ {(IC SCMPDS)} by FUNCOP_1:19
.= {il} \/ {(IC SCMPDS)} by FUNCOP_1:19 ;
then (dom p) /\ (dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) = ((dom p) /\ {il}) \/ ((dom p) /\ {(IC SCMPDS)}) by XBOOLE_1:23
.= ((dom p) /\ {il}) \/ {} by A9, XBOOLE_0:def 7
.= {} by A5, XBOOLE_0:def 7 ;
then dom p misses dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) by XBOOLE_0:def 7;
then p c= p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) by FUNCT_4:33;
hence p c= s1 by A10, XBOOLE_1:1; :: thesis: ( p c= s2 & not for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 p) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 p) )
dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) = (dom (il .--> (d1 := 1))) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1
.= (dom (il .--> (d1 := 1))) \/ {(IC SCMPDS)} by FUNCOP_1:19
.= {il} \/ {(IC SCMPDS)} by FUNCOP_1:19 ;
then (dom p) /\ (dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) = ((dom p) /\ {il}) \/ ((dom p) /\ {(IC SCMPDS)}) by XBOOLE_1:23
.= ((dom p) /\ {il}) \/ {} by A9, XBOOLE_0:def 7
.= {} by A5, XBOOLE_0:def 7 ;
then dom p misses dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) by XBOOLE_0:def 7;
then p c= p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) by FUNCT_4:33;
hence p c= s2 by A11, XBOOLE_1:1; :: thesis: not for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 p) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 p)
take 1 ; :: thesis: not (Comput ((ProgramPart s1),s1,1)) | (proj1 p) = (Comput ((ProgramPart s2),s2,1)) | (proj1 p)
A12: dom (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) = (dom p) \/ (dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) by FUNCT_4:def 1;
A13: dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) = (dom (il .--> (d1 := 1))) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1;
then A14: IC SCMPDS in dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) by A7, XBOOLE_0:def 3;
then IC SCMPDS in dom (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) by A12, XBOOLE_0:def 3;
then A15: IC s2 = (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) . (IC SCMPDS) by A11, GRFUNC_1:8
.= ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) . (IC SCMPDS) by A14, FUNCT_4:14
.= (Start-At (il,SCMPDS)) . (IC SCMPDS) by A7, FUNCT_4:14
.= il by FUNCOP_1:87 ;
dom (il .--> (d1 := 1)) = {il} by FUNCOP_1:19;
then il in dom (il .--> (d1 := 1)) by TARSKI:def 1;
then A16: il in dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) by A13, XBOOLE_0:def 3;
then il in dom (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) by A12, XBOOLE_0:def 3;
then A17: s2 . il = (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) . il by A11, GRFUNC_1:8
.= ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) . il by A16, FUNCT_4:14
.= (il .--> (d1 := 1)) . il by A8, FUNCT_4:12
.= d1 := 1 by FUNCOP_1:87 ;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
A18: (Comput ((ProgramPart s2),s2,(0 + 1))) . d1 = (Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,0)))) . d1 by EXTPRO_1:4
.= (Following ((ProgramPart s2),s2)) . d1 by EXTPRO_1:3
.= 1 by A15, A17, Y, SCMPDS_2:57 ;
X: dom p c= the carrier of SCMPDS by RELAT_1:def 18;
dom (Comput ((ProgramPart s1),s1,1)) = the carrier of SCMPDS by PARTFUN1:def 4;
then A19: dom ((Comput ((ProgramPart s1),s1,1)) | (dom p)) = dom p by X, RELAT_1:91;
il <> IC SCMPDS by COMPOS_1:3;
then A20: not il in dom (Start-At (il,SCMPDS)) by A6, TARSKI:def 1;
dom (Comput ((ProgramPart s2),s2,1)) = the carrier of SCMPDS by PARTFUN1:def 4;
then A21: dom ((Comput ((ProgramPart s2),s2,1)) | (dom p)) = dom p by X, RELAT_1:91;
A22: dom (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) = (dom p) \/ (dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) by FUNCT_4:def 1;
A23: dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) = (dom (il .--> (d1 := 0))) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1;
then A24: IC SCMPDS in dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) by A7, XBOOLE_0:def 3;
then IC SCMPDS in dom (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) by A22, XBOOLE_0:def 3;
then A25: IC s1 = (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) . (IC SCMPDS) by A10, GRFUNC_1:8
.= ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) . (IC SCMPDS) by A24, FUNCT_4:14
.= (Start-At (il,SCMPDS)) . (IC SCMPDS) by A7, FUNCT_4:14
.= il by FUNCOP_1:87 ;
dom (il .--> (d1 := 0)) = {il} by FUNCOP_1:19;
then il in dom (il .--> (d1 := 0)) by TARSKI:def 1;
then A26: il in dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) by A23, XBOOLE_0:def 3;
then il in dom (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) by A22, XBOOLE_0:def 3;
then A27: s1 . il = (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) . il by A10, GRFUNC_1:8
.= ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) . il by A26, FUNCT_4:14
.= (il .--> (d1 := 0)) . il by A20, FUNCT_4:12
.= d1 := 0 by FUNCOP_1:87 ;
DataPart p c= p by RELAT_1:88;
then A28: dom (DataPart p) c= dom p by RELAT_1:25;
Y: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
(Comput ((ProgramPart s1),s1,(0 + 1))) . d1 = (Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,0)))) . d1 by EXTPRO_1:4
.= (Following ((ProgramPart s1),s1)) . d1 by EXTPRO_1:3
.= 0 by A25, A27, Y, SCMPDS_2:57 ;
then ((Comput ((ProgramPart s1),s1,1)) | (dom p)) . d1 = 0 by A3, A28, A19, FUNCT_1:70;
hence not (Comput ((ProgramPart s1),s1,1)) | (proj1 p) = (Comput ((ProgramPart s2),s2,1)) | (proj1 p) by A3, A28, A21, A18, FUNCT_1:70; :: thesis: verum

end;

hence contradiction ; :: thesis: verum