let p be autonomic FinPartState of SCMPDS; :: according to AMISTD_5:def 3 :: thesis: ( NPP p is empty or IC in proj1 p )
assume A1: not NPP p is empty ; :: thesis: IC in proj1 p
assume A2: not IC in dom p ; :: thesis: contradiction
dom (NPP p) c= dom p by RELAT_1:25;
then not IC in dom (NPP p) by A2;
then A3: dom (NPP p) misses {(IC )} by ZFMISC_1:56;
dom (NPP p) c= {(IC )} \/ (dom (DataPart p)) by COMPOS_1:171;
then A4: dom (NPP p) c= dom (DataPart p) by A3, XBOOLE_1:73;
A5: dom (DataPart p) <> {} by A1, A4, XBOOLE_1:3;
DataPart p c= NPP p by COMPOS_1:169;
then A6: dom (DataPart p) c= dom (NPP p) by RELAT_1:25;
not p is autonomic
proof
set il = the Element of NAT \ (dom p);
set d1 = the Element of dom (DataPart p);
A7: the Element of dom (DataPart p) in dom (DataPart p) by A5;
dom (DataPart p) c= the carrier of SCMPDS by RELAT_1:def 18;
then reconsider d1 = the Element of dom (DataPart p) as Element of SCMPDS by A7;
not NAT c= dom p ;
then A8: NAT \ (dom p) <> {} by XBOOLE_1:37;
then reconsider il = the Element of NAT \ (dom p) as Element of NAT by XBOOLE_0:def 5;
not il in dom p by A8, XBOOLE_0:def 5;
then A9: 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 A7, SCMPDS_2:9;
A10: dom (Start-At (il,SCMPDS)) = {(IC )} by FUNCOP_1:19;
then A11: IC in dom (Start-At (il,SCMPDS)) by TARSKI:def 1;
il <> IC by COMPOS_1:3;
then A12: not il in dom (Start-At (il,SCMPDS)) by A10, TARSKI:def 1;
A13: dom p misses {(IC )} 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
A14: p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) c= s1 by PBOOLE:156;
consider s2 being State of SCMPDS such that
A15: p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) c= s2 by PBOOLE:156;
take P1 = ProgramPart s1; :: according to EXTPRO_1:def 9 :: thesis: ex b1 being set st
( ProgramPart p c= P1 & ProgramPart p c= b1 & ex b2, b3 being set st
( NPP p c= b2 & NPP p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (proj1 (NPP p)) = (Comput (b1,b3,b4)) | (proj1 (NPP p)) ) )
take P2 = ProgramPart s2; :: thesis: ( ProgramPart p c= P1 & ProgramPart p c= P2 & ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP 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 )} by FUNCOP_1:19
.= {il} \/ {(IC )} by FUNCOP_1:19 ;
then (dom p) /\ (dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) = ((dom p) /\ {il}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {il}) \/ {} by A13, XBOOLE_0:def 7
.= {} by A9, 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;
then A16: p c= s1 by A14, XBOOLE_1:1;
hence ProgramPart p c= P1 by RELAT_1:105; :: thesis: ( ProgramPart p c= P2 & ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP 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 )} by FUNCOP_1:19
.= {il} \/ {(IC )} by FUNCOP_1:19 ;
then (dom p) /\ (dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) = ((dom p) /\ {il}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {il}) \/ {} by A13, XBOOLE_0:def 7
.= {} by A9, 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;
then A17: p c= s2 by A15, XBOOLE_1:1;
hence ProgramPart p c= P2 by RELAT_1:105; :: thesis: ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP p)) )
take s1 ; :: thesis: ex b1 being set st
( NPP p c= s1 & NPP p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s1,b2)) | (proj1 (NPP p)) = (Comput (P2,b1,b2)) | (proj1 (NPP p)) )
take s2 ; :: thesis: ( NPP p c= s1 & NPP p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (NPP p)) = (Comput (P2,s2,b1)) | (proj1 (NPP p)) )
p c= s1 by A16;
hence NPP p c= s1 by XBOOLE_1:1; :: thesis: ( NPP p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (NPP p)) = (Comput (P2,s2,b1)) | (proj1 (NPP p)) )
thus NPP p c= s2 by A17, XBOOLE_1:1; :: thesis: not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (NPP p)) = (Comput (P2,s2,b1)) | (proj1 (NPP p))
take 1 ; :: thesis: not (Comput (P1,s1,1)) | (proj1 (NPP p)) = (Comput (P2,s2,1)) | (proj1 (NPP p))
A18: dom (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) = (dom p) \/ (dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) by FUNCT_4:def 1;
A19: dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) = (dom (il .--> (d1 := 1))) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1;
then A20: IC in dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) by A11, XBOOLE_0:def 3;
then IC in dom (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) by A18, XBOOLE_0:def 3;
then A21: IC s2 = (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) . (IC ) by A15, GRFUNC_1:8
.= ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) . (IC ) by A20, FUNCT_4:14
.= (Start-At (il,SCMPDS)) . (IC ) by A11, 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 A22: il in dom ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) by A19, XBOOLE_0:def 3;
then il in dom (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) by A18, XBOOLE_0:def 3;
then A23: s2 . il = (p +* ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS)))) . il by A15, GRFUNC_1:8
.= ((il .--> (d1 := 1)) +* (Start-At (il,SCMPDS))) . il by A22, FUNCT_4:14
.= (il .--> (d1 := 1)) . il by A12, FUNCT_4:12
.= d1 := 1 by FUNCOP_1:87 ;
A24: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
A25: (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 A21, A23, A24, SCMPDS_2:57 ;
A26: dom (NPP 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 A27: dom ((Comput ((ProgramPart s1),s1,1)) | (dom (NPP p))) = dom (NPP p) by A26, RELAT_1:91;
il <> IC by COMPOS_1:3;
then A28: not il in dom (Start-At (il,SCMPDS)) by A10, TARSKI:def 1;
A29: dom (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) = (dom p) \/ (dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) by FUNCT_4:def 1;
A30: dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) = (dom (il .--> (d1 := 0))) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def 1;
then A31: IC in dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) by A11, XBOOLE_0:def 3;
then IC in dom (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) by A29, XBOOLE_0:def 3;
then A32: IC s1 = (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) . (IC ) by A14, GRFUNC_1:8
.= ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) . (IC ) by A31, FUNCT_4:14
.= (Start-At (il,SCMPDS)) . (IC ) by A11, 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 A33: il in dom ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) by A30, XBOOLE_0:def 3;
then il in dom (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) by A29, XBOOLE_0:def 3;
then A34: s1 . il = (p +* ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS)))) . il by A14, GRFUNC_1:8
.= ((il .--> (d1 := 0)) +* (Start-At (il,SCMPDS))) . il by A33, FUNCT_4:14
.= (il .--> (d1 := 0)) . il by A28, FUNCT_4:12
.= d1 := 0 by FUNCOP_1:87 ;
A35: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
A36: dom (Comput ((ProgramPart s2),s2,1)) = the carrier of SCMPDS by PARTFUN1:def 4;
A37: dom ((Comput ((ProgramPart s2),s2,1)) | (dom (NPP p))) = dom (NPP p) by RELAT_1:91, A26, A36;
(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 A32, A34, A35, SCMPDS_2:57 ;
then ((Comput ((ProgramPart s1),s1,1)) | (dom (NPP p))) . d1 = 0 by A7, A27, FUNCT_1:70, A6;
hence not (Comput (P1,s1,1)) | (proj1 (NPP p)) = (Comput (P2,s2,1)) | (proj1 (NPP p)) by A25, FUNCT_1:70, A7, A37, A6; :: thesis: verum
end;
hence contradiction ; :: thesis: verum