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