let p be autonomic FinPartState of SCMPDS ; ( DataPart p <> {} implies IC SCMPDS in dom p )
assume
DataPart p <> {}
; IC SCMPDS in dom p
then A1:
dom (DataPart p) <> {}
;
assume A2:
not IC SCMPDS in dom p
; 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 AMI_1:48;
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
;
AMI_1:def 25 ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (ProgramPart s1),s1,b2) | (proj1 p) = (Comput (ProgramPart b1),b1,b2) | (proj1 p) )
take
s2
;
( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 p) = (Comput (ProgramPart s2),s2,b1) | (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;
( p c= s2 & not for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 p) = (Comput (ProgramPart s2),s2,b1) | (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;
not for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 p) = (Comput (ProgramPart s2),s2,b1) | (proj1 p)
take
1
;
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 AMI_1:150;
A18:
(Comput (ProgramPart s2),s2,(0 + 1)) . d1 =
(Following (ProgramPart s2),(Comput (ProgramPart s2),s2,0 )) . d1
by AMI_1:14
.=
(Following (ProgramPart s2),s2) . d1
by AMI_1:13
.=
1
by A15, A17, SCMPDS_2:57, Y
;
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 RELAT_1:91, X;
il <> IC SCMPDS
by AMI_1:48;
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 RELAT_1:91, X;
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 AMI_1:150;
(Comput (ProgramPart s1),s1,(0 + 1)) . d1 =
(Following (ProgramPart s1),(Comput (ProgramPart s1),s1,0 )) . d1
by AMI_1:14
.=
(Following (ProgramPart s1),s1) . d1
by AMI_1:13
.=
0
by A25, A27, SCMPDS_2:57, Y
;
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;
verum
end;
hence
contradiction
; verum