for p being autonomic FinPartState of SCM st DataPart p <> {} holds
IC in dom p
proof
let p be
autonomic FinPartState of
SCM;
( DataPart p <> {} implies IC in dom p )
assume
DataPart p <> {}
;
IC in dom p
then A1:
dom (DataPart p) <> {}
;
assume A2:
not
IC in dom p
;
contradiction
then
dom p misses {(IC )}
by ZFMISC_1:56;
then A3:
(dom p) /\ {(IC )} = {}
by XBOOLE_0:def 7;
not
p is
autonomic
proof
set il = the
Element of
NAT \ (dom p);
set d2 = the
Element of
(Data-Locations SCM) \ (dom p);
set d1 = the
Element of
dom (DataPart p);
A4:
the
Element of
dom (DataPart p) in dom (DataPart p)
by A1;
DataPart p c= NPP p
by COMPOS_1:169;
then
dom (DataPart p) c= dom (NPP p)
by RELAT_1:25;
then A5:
the
Element of
dom (DataPart p) in dom (NPP p)
by A4;
dom (DataPart p) c= the
carrier of
SCM
by RELAT_1:def 18;
then reconsider d1 = the
Element of
dom (DataPart p) as
Element of
SCM by A4;
not
Data-Locations SCM c= dom p
;
then A6:
(Data-Locations SCM) \ (dom p) <> {}
by XBOOLE_1:37;
then
the
Element of
(Data-Locations SCM) \ (dom p) in Data-Locations SCM
by XBOOLE_0:def 5;
then reconsider d2 = the
Element of
(Data-Locations SCM) \ (dom p) as
Data-Location by AMI_3:72, AMI_3:def 2;
A7:
not
d2 in dom p
by A6, XBOOLE_0:def 5;
then
dom p misses {d2}
by ZFMISC_1:56;
then A8:
(dom p) /\ {d2} = {}
by XBOOLE_0:def 7;
not
NAT c= dom p
;
then A9:
NAT \ (dom p) <> {}
by XBOOLE_1:37;
then
the
Element of
NAT \ (dom p) is
Element of
NAT
by XBOOLE_0:def 5;
then reconsider il = the
Element of
NAT \ (dom p) as
Element of
NAT ;
A10:
not
il in dom p
by A9, XBOOLE_0:def 5;
then A11:
dom p misses {il}
by ZFMISC_1:56;
dom (DataPart p) c= Data-Locations SCM
by RELAT_1:87;
then reconsider d1 =
d1 as
Data-Location by A4, AMI_3:72, AMI_3:def 2;
A12:
dom ((il .--> (d1 := d2)) +* (d2 .--> 0)) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 0))
by FUNCT_4:def 1;
set p2 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)));
set p1 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)));
consider s1 being
State of
SCM such that A13:
p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))) c= s1
by PBOOLE:156;
dom p misses {d2}
by A7, ZFMISC_1:56;
then A14:
(dom p) /\ {d2} = {}
by XBOOLE_0:def 7;
A15:
dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))) = (dom ((il .--> (d1 := d2)) +* (d2 .--> 1))) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1;
consider s2 being
State of
SCM such that A16:
p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))) c= s2
by PBOOLE:156;
A18:
dom (NPP p) c= the
carrier of
SCM
by RELAT_1:def 18;
dom (Comput ((ProgramPart s2),s2,1)) = the
carrier of
SCM
by PARTFUN1:def 4;
then A19:
dom ((Comput ((ProgramPart s2),s2,1)) | (dom (NPP p))) = dom (NPP p)
by A18, RELAT_1:91;
A20:
dom (Comput ((ProgramPart s1),s1,1)) = the
carrier of
SCM
by PARTFUN1:def 4;
A21:
dom ((Comput ((ProgramPart s1),s1,1)) | (dom (NPP p))) = dom (NPP p)
by A18, A20, RELAT_1:91;
A22:
dom ((il .--> (d1 := d2)) +* (d2 .--> 1)) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 1))
by FUNCT_4:def 1;
A23:
dom p misses {il}
by A10, ZFMISC_1:56;
A24:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))))
by FUNCT_4:def 1;
A25:
dom (Start-At (il,SCM)) = {(IC )}
by FUNCOP_1:19;
then A26:
IC in dom (Start-At (il,SCM))
by TARSKI:def 1;
then A27:
IC in dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))
by A15, XBOOLE_0:def 3;
then
IC in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))))
by A24, XBOOLE_0:def 3;
then A28:
IC s2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))) . (IC )
by A16, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))) . (IC )
by A27, FUNCT_4:14
.=
(Start-At (il,SCM)) . (IC )
by A26, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
d2 <> IC
by Th20;
then A29:
not
d2 in dom (Start-At (il,SCM))
by A25, TARSKI:def 1;
A30:
dom (d2 .--> 1) = {d2}
by FUNCOP_1:19;
then A31:
d2 in dom (d2 .--> 1)
by TARSKI:def 1;
then
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> 1))
by A22, XBOOLE_0:def 3;
then A32:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))
by A15, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))))
by A24, XBOOLE_0:def 3;
then A33:
s2 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))) . d2
by A16, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))) . d2
by A32, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 1)) . d2
by A29, FUNCT_4:12
.=
(d2 .--> 1) . d2
by A31, FUNCT_4:14
.=
1
by FUNCOP_1:87
;
il <> IC
by COMPOS_1:3;
then A34:
not
il in dom (Start-At (il,SCM))
by A25, TARSKI:def 1;
il <> d2
by Th22;
then A35:
not
il in dom (d2 .--> 1)
by A30, TARSKI:def 1;
dom (il .--> (d1 := d2)) = {il}
by FUNCOP_1:19;
then
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
then
il in dom ((il .--> (d1 := d2)) +* (d2 .--> 1))
by A22, XBOOLE_0:def 3;
then A36:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))
by A15, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))))
by A24, XBOOLE_0:def 3;
then A37:
s2 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))) . il
by A16, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))) . il
by A36, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 1)) . il
by A34, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A35, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
A38:
(ProgramPart s2) /. (IC s2) = s2 . (IC s2)
by COMPOS_1:38;
A39:
(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 A28, A37, A33, A38, AMI_3:8
;
dom p misses {(IC )}
by A2, ZFMISC_1:56;
then A40:
(dom p) /\ {(IC )} = {}
by XBOOLE_0:def 7;
take P =
ProgramPart s1;
EXTPRO_1:def 9 ex b1 being set st
( ProgramPart p c= P & 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 (P,b2,b4)) | (proj1 (NPP p)) = (Comput (b1,b3,b4)) | (proj1 (NPP p)) ) )
take Q =
ProgramPart s2;
( ProgramPart p c= P & ProgramPart p c= Q & ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP p)) = (Comput (Q,b2,b3)) | (proj1 (NPP p)) ) )
dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))) =
(dom ((il .--> (d1 := d2)) +* (d2 .--> 0))) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 := d2)) +* (d2 .--> 0))) \/ {(IC )}
by FUNCOP_1:19
.=
((dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 0))) \/ {(IC )}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> 0))) \/ {(IC )}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC )}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))) =
((dom p) /\ ({il} \/ {d2})) \/ {}
by A40, XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A8, XBOOLE_1:23
.=
{}
by A11, XBOOLE_0:def 7
;
then
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))
by FUNCT_4:33;
then A41:
p c= s1
by A13, XBOOLE_1:1;
hence
ProgramPart p c= P
by RELAT_1:105;
( ProgramPart p c= Q & ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP p)) = (Comput (Q,b2,b3)) | (proj1 (NPP p)) ) )
A42:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))))
by FUNCT_4:def 1;
dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM))) =
(dom ((il .--> (d1 := d2)) +* (d2 .--> 1))) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 := d2)) +* (d2 .--> 1))) \/ {(IC )}
by FUNCOP_1:19
.=
((dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 1))) \/ {(IC )}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> 1))) \/ {(IC )}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC )}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))) =
((dom p) /\ ({il} \/ {d2})) \/ {}
by A3, XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A14, XBOOLE_1:23
.=
{}
by A23, XBOOLE_0:def 7
;
then
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At (il,SCM)))
by FUNCT_4:33;
then A43:
p c= s2
by A16, XBOOLE_1:1;
hence
ProgramPart p c= Q
by RELAT_1:105;
ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP p)) = (Comput (Q,b2,b3)) | (proj1 (NPP p)) )
take
s1
;
ex b1 being set st
( NPP p c= s1 & NPP p c= b1 & not for b2 being Element of NAT holds (Comput (P,s1,b2)) | (proj1 (NPP p)) = (Comput (Q,b1,b2)) | (proj1 (NPP p)) )
take
s2
;
( NPP p c= s1 & NPP p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP p)) = (Comput (Q,s2,b1)) | (proj1 (NPP p)) )
p c= s1
by A41;
hence
NPP p c= s1
by XBOOLE_1:1;
( NPP p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP p)) = (Comput (Q,s2,b1)) | (proj1 (NPP p)) )
p c= s2
by A43;
hence
NPP p c= s2
by XBOOLE_1:1;
not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP p)) = (Comput (Q,s2,b1)) | (proj1 (NPP p))
take
1
;
not (Comput (P,s1,1)) | (proj1 (NPP p)) = (Comput (Q,s2,1)) | (proj1 (NPP p))
A44:
dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))) = (dom ((il .--> (d1 := d2)) +* (d2 .--> 0))) \/ (dom (Start-At (il,SCM)))
by FUNCT_4:def 1;
A45:
dom (Start-At (il,SCM)) = {(IC )}
by FUNCOP_1:19;
then A46:
IC in dom (Start-At (il,SCM))
by TARSKI:def 1;
then A47:
IC in dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))
by A44, XBOOLE_0:def 3;
then
IC in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))))
by A42, XBOOLE_0:def 3;
then A48:
IC s1 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))) . (IC )
by A13, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))) . (IC )
by A47, FUNCT_4:14
.=
(Start-At (il,SCM)) . (IC )
by A46, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
d2 <> IC
by Th20;
then A49:
not
d2 in dom (Start-At (il,SCM))
by A45, TARSKI:def 1;
A50:
dom (d2 .--> 0) = {d2}
by FUNCOP_1:19;
then A51:
d2 in dom (d2 .--> 0)
by TARSKI:def 1;
then
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> 0))
by A12, XBOOLE_0:def 3;
then A52:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))
by A44, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))))
by A42, XBOOLE_0:def 3;
then A53:
s1 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))) . d2
by A13, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))) . d2
by A52, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 0)) . d2
by A49, FUNCT_4:12
.=
(d2 .--> 0) . d2
by A51, FUNCT_4:14
.=
0
by FUNCOP_1:87
;
il <> IC
by COMPOS_1:3;
then A54:
not
il in dom (Start-At (il,SCM))
by A45, TARSKI:def 1;
il <> d2
by Th22;
then A55:
not
il in dom (d2 .--> 0)
by A50, TARSKI:def 1;
dom (il .--> (d1 := d2)) = {il}
by FUNCOP_1:19;
then
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
then
il in dom ((il .--> (d1 := d2)) +* (d2 .--> 0))
by A12, XBOOLE_0:def 3;
then A56:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))
by A44, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))))
by A42, XBOOLE_0:def 3;
then A57:
s1 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM)))) . il
by A13, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 0)) +* (Start-At (il,SCM))) . il
by A56, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 0)) . il
by A54, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A55, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
A58:
(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 A48, A57, A53, A58, AMI_3:8
;
then
((Comput (P,s1,1)) | (dom (NPP p))) . d1 = 0
by A5, A21, FUNCT_1:70;
hence
(Comput (P,s1,1)) | (dom (NPP p)) <> (Comput (Q,s2,1)) | (dom (NPP p))
by A19, A39, A5, FUNCT_1:70;
verum
end;
hence
contradiction
;
verum
end;
hence
SCM is IC-recognized
by AMISTD_5:3; verum