:: A Theory of Boolean Valued Functions and Quantifiers with
:: Respect to Partitions
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, PARTIT1, EQREL_1, TARSKI, ZFMISC_1, FUNCT_1,
SETFAM_1, RELAT_1, PARTFUN1, MARGREL1, BVFUNC_1, XBOOLEAN, BVFUNC_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1,
FUNCT_1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, EQREL_1, PARTIT1,
BVFUNC_1;
constructors SETFAM_1, PARTIT1, BVFUNC_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XBOOLEAN, EQREL_1, MARGREL1,
PARTIT1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, BVFUNC_1, FUNCT_2;
equalities XBOOLEAN;
expansions TARSKI;
theorems TARSKI, FUNCT_1, SETFAM_1, EQREL_1, ZFMISC_1, SUBSET_1, MARGREL1,
BINARITH, PARTIT1, BVFUNC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XBOOLEAN,
PARTFUN1;
schemes DOMAIN_1, PARTFUN2, XFAMILY;
begin :: Chap. 1 Preliminaries
reserve Y for non empty set,
G for Subset of PARTITIONS(Y);
definition
let X be set;
redefine func PARTITIONS X -> Part-Family of X; :: redefines PARTITIONS (PARTIT1, definition)
coherence
proof
A1: PARTITIONS X c= bool bool X
proof
let x be object;
assume x in PARTITIONS X;
then x is a_partition of X by PARTIT1:def 3;
hence thesis;
end;
for S being set st S in PARTITIONS X holds S is a_partition of X by
PARTIT1:def 3;
hence thesis by A1,EQREL_1:def 7;
end;
end;
definition
let X be set;
let F be non empty Part-Family of X;
redefine mode Element of F -> a_partition of X; :: redefines Element (SUBSET_1, definition)
coherence by EQREL_1:def 7;
end;
theorem Th1:
for y being Element of Y ex X being Subset of Y st y in X & ex h
being Function, F being Subset-Family of Y st dom h=G & rng h = F & (for d
being set st d in G holds h.d in d) & X=Intersect F & X<>{}
proof
let y be Element of Y;
deffunc F(Element of PARTITIONS(Y)) = EqClass(y,$1);
defpred P[set] means $1 in G;
consider h being PartFunc of PARTITIONS(Y), bool Y such that
A1: for d being Element of PARTITIONS(Y) holds d in dom h iff P[d] and
A2: for d being Element of PARTITIONS(Y) st d in dom h holds h/.d = F(d)
from PARTFUN2:sch 2;
A3: G c= dom h
by A1;
A4: for d being set st d in G holds h.d in d
proof
let d be set;
assume
A5: d in G;
then reconsider d as a_partition of Y by PARTIT1:def 3;
h/.d=h.d by A3,A5,PARTFUN1:def 6;
then h.d = EqClass(y,d) by A2,A3,A5;
hence thesis;
end;
dom h c= G
by A1;
then
A6: dom h = G by A3,XBOOLE_0:def 10;
reconsider rr = rng h as Subset-Family of Y;
A7: for d being Element of PARTITIONS(Y) st d in dom h holds y in h.d
proof
let d be Element of PARTITIONS(Y);
assume
A8: d in dom h;
then h/.d = EqClass(y,d) by A2;
then h.d = EqClass(y,d) by A8,PARTFUN1:def 6;
hence thesis by EQREL_1:def 6;
end;
A9: for c being set holds c in rng h implies y in c
proof
let c be set;
assume c in rng h;
then ex a being object st a in dom h & c = h.a by FUNCT_1:def 3;
hence thesis by A7;
end;
per cases;
suppose
rng h ={};
then Intersect rr = Y by SETFAM_1:def 9;
hence thesis by A6,A4;
end;
suppose
rng h <> {};
then y in meet (rng h) & Intersect rr = meet (rng h) by A9,SETFAM_1:def 1
,def 9;
hence thesis by A6,A4;
end;
end;
definition
let Y;
let G be Subset of PARTITIONS(Y);
func '/\' G -> a_partition of Y means
:Def1:
for x being set holds x in it
iff ex h being Function, F being Subset-Family of Y st dom h=G & rng h = F & (
for d being set st d in G holds h.d in d) & x=Intersect F & x<>{};
existence
proof
defpred P[set] means (ex h being Function, F being Subset-Family of Y st
dom h=G & rng h = F & (for d being set st d in G holds h.d in d) & $1=Intersect
F & $1<>{});
consider X being set such that
A1: for x being set holds x in X iff x in bool Y & P[x] from XFAMILY:
sch 1;
A2: for A being Subset of Y st A in X holds A<>{} & for B being Subset of
Y st B in X holds A=B or A misses B
proof
let A be Subset of Y;
assume A in X;
then consider h1 being Function, F1 being Subset-Family of Y such that
A3: dom h1=G and
A4: rng h1 = F1 and
A5: for d being set st d in G holds h1.d in d and
A6: A=Intersect F1 and
A7: A<>{} by A1;
thus A<>{} by A7;
let B be Subset of Y;
assume B in X;
then consider h2 being Function, F2 being Subset-Family of Y such that
A8: dom h2=G and
A9: rng h2 =F2 and
A10: for d being set st d in G holds h2.d in d and
A11: B=Intersect F2 and
B<>{} by A1;
per cases;
suppose
A12: G={};
then rng h1={} by A3,RELAT_1:42;
hence thesis by A4,A6,A8,A9,A11,A12,RELAT_1:42;
end;
suppose
A13: G<>{};
now
assume A meets B;
then consider p being object such that
A14: p in A and
A15: p in B by XBOOLE_0:3;
A16: p in meet (rng h2) by A9,A11,A13,A15,A8,RELAT_1:42,SETFAM_1:def 9;
A17: p in meet (rng h1) by A4,A6,A3,A13,A14,RELAT_1:42,SETFAM_1:def 9;
for g being object st g in G holds h1.g=h2.g
proof
let g be object;
assume
A18: g in G;
then reconsider g as a_partition of Y by PARTIT1:def 3;
h1.g in rng h1 by A3,A18,FUNCT_1:def 3;
then
A19: p in h1.g by A17,SETFAM_1:def 1;
h2.g in rng h2 by A8,A18,FUNCT_1:def 3;
then
A20: p in h2.g by A16,SETFAM_1:def 1;
h1.g in g & h2.g in g by A5,A10,A18;
hence thesis by A19,A20,EQREL_1:def 4,XBOOLE_0:3;
end;
hence thesis by A3,A4,A6,A8,A9,A11,FUNCT_1:2;
end;
hence thesis;
end;
end;
A21: Y c= union X
proof
let y be object;
assume y in Y;
then reconsider y as Element of Y;
consider a being Subset of Y such that
A22: y in a and
A23: ex h being Function, F being Subset-Family of Y st dom h=G &
rng h = F & (for d being set st d in G holds h.d in d) & a=Intersect F & a<>{}
by Th1;
a in X by A1,A23;
hence thesis by A22,TARSKI:def 4;
end;
A24: union X c= Y
proof
let a be object;
assume a in union X;
then consider p being set such that
A25: a in p and
A26: p in X by TARSKI:def 4;
ex h being Function, F being Subset-Family of Y st dom h=G & rng h =
F &( for d being set st d in G holds h.d in d)& p=Intersect F & p <>{} by A1
,A26;
hence thesis by A25;
end;
take X;
X c= bool Y
by A1;
then reconsider X as Subset-Family of Y;
X is a_partition of Y by A24,A2,A21,EQREL_1:def 4,XBOOLE_0:def 10;
hence thesis by A1;
end;
uniqueness
proof
let A1,A2 be a_partition of Y such that
A27: for x being set holds x in A1 iff ex h being Function, F being
Subset-Family of Y st dom h=G & rng h = F & (for d being set st d in G holds h.
d in d)& x=Intersect F & x<>{} and
A28: for x being set holds x in A2 iff ex h being Function, F being
Subset-Family of Y st dom h=G & rng h = F & (for d being set st d in G holds h.
d in d)& x=Intersect F & x<>{};
now
let y be object;
y in A1 iff ex h being Function, F being Subset-Family of Y st dom
h=G & rng h =F & (for d being set st d in G holds h.d in d)& y=Intersect F & y
<>{} by A27;
hence y in A1 iff y in A2 by A28;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let Y;
let G be Subset of PARTITIONS(Y),b be set;
pred b is_upper_min_depend_of G means
(for d being a_partition of Y
st d in G holds b is_a_dependent_set_of d) & for e being set st e c= b & (for d
being a_partition of Y st d in G holds e is_a_dependent_set_of d) holds e=b;
end;
theorem Th2:
for y being Element of Y st G<>{} holds ex X being Subset of Y st
y in X & X is_upper_min_depend_of G
proof
let y be Element of Y;
defpred P[set] means y in $1 & for d being a_partition of Y st d in G holds
$1 is_a_dependent_set_of d;
reconsider XX={ X where X is Subset of Y: P[X]} as Subset-Family of Y from
DOMAIN_1:sch 7;
reconsider XX as Subset-Family of Y;
assume G<>{};
then consider g being object such that
A1: g in G by XBOOLE_0:def 1;
reconsider g as a_partition of Y by A1,PARTIT1:def 3;
A2: union g = Y by EQREL_1:def 4;
take Intersect(XX);
Y c= Y & for d being a_partition of Y st d in G holds Y
is_a_dependent_set_of d by PARTIT1:7;
then
A3: Y in XX;
A4: for A being set st A in g holds A<>{} & for B being set st B in g holds
A=B or A misses B by EQREL_1:def 4;
A5: for e being set st e c= Intersect(XX) & (for d being a_partition of Y
st d in G holds e is_a_dependent_set_of d) holds e=Intersect(XX)
proof
let e be set;
assume that
A6: e c= Intersect(XX) and
A7: for d being a_partition of Y st d in G holds e is_a_dependent_set_of d;
consider Ad being set such that
A8: Ad c= g and
A9: Ad<>{} and
A10: e = union Ad by A1,A7,PARTIT1:def 1;
A11: e c= Y by A2,A8,A10,ZFMISC_1:77;
per cases;
suppose
y in e;
then
A12: e in XX by A7,A11;
Intersect(XX) c= e
proof
let X1 be object;
assume X1 in Intersect(XX);
then X1 in meet XX by A3,SETFAM_1:def 9;
hence thesis by A12,SETFAM_1:def 1;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
suppose
A13: not y in e;
reconsider e as Subset of Y by A2,A8,A10,ZFMISC_1:77;
e` = Y \ e by SUBSET_1:def 4;
then
A14: y in e` by A13,XBOOLE_0:def 5;
e <> Y by A13;
then for d being a_partition of Y st d in G holds e`
is_a_dependent_set_of d by A7,PARTIT1:10;
then
A15: e` in XX by A14;
A16: Intersect(XX) c= e`
proof
let X1 be object;
assume X1 in Intersect XX;
then X1 in meet XX by A3,SETFAM_1:def 9;
hence thesis by A15,SETFAM_1:def 1;
end;
A17: e /\ e = e;
consider ad being object such that
A18: ad in Ad by A9,XBOOLE_0:def 1;
reconsider ad as set by TARSKI:1;
e /\ e` = {} by SUBSET_1:24,XBOOLE_0:def 7;
then e /\ Intersect(XX) = {} by A16,XBOOLE_1:3,26;
then e c= {} by A6,A17,XBOOLE_1:26;
then union Ad = {} by A10;
then
A19: ad c= {} by A18,ZFMISC_1:74;
ad<>{} by A4,A8,A18;
hence thesis by A19;
end;
end;
for X1 be set st X1 in XX holds y in X1
proof
let X1 be set;
assume X1 in XX;
then
ex X be Subset of Y st X=X1 & y in X & for d being a_partition of Y st
d in G holds X is_a_dependent_set_of d;
hence thesis;
end;
then
A20: y in meet XX by A3,SETFAM_1:def 1;
then
A21: Intersect(XX)<>{} by SETFAM_1:def 9;
for d being a_partition of Y st d in G holds Intersect(XX)
is_a_dependent_set_of d
proof
let d be a_partition of Y;
assume
A22: d in G;
for X1 be set st X1 in XX holds X1 is_a_dependent_set_of d
proof
let X1 be set;
assume X1 in XX;
then ex X be Subset of Y st X=X1 & y in X & for d being a_partition of Y
st d in G holds X is_a_dependent_set_of d;
hence thesis by A22;
end;
hence thesis by A21,PARTIT1:8;
end;
hence thesis by A3,A20,A5,SETFAM_1:def 9;
end;
definition
let Y;
let G be Subset of PARTITIONS(Y);
func '\/' G -> a_partition of Y means
:Def3:
for x being set holds x in it
iff x is_upper_min_depend_of G if G<>{} otherwise it = %I(Y);
existence
proof
thus G<>{} implies ex X being a_partition of Y st for x being set holds x
in X iff x is_upper_min_depend_of G
proof
defpred P[set] means $1 is_upper_min_depend_of G;
consider X being set such that
A1: for x being set holds x in X iff x in bool Y & P[x] from
XFAMILY:sch 1;
A2: union X c= Y
proof
let y be object;
assume y in union X;
then consider a being set such that
A3: y in a and
A4: a in X by TARSKI:def 4;
a in bool Y by A1,A4;
hence thesis by A3;
end;
assume
A5: G<>{};
then consider g being object such that
A6: g in G by XBOOLE_0:def 1;
reconsider g as a_partition of Y by A6,PARTIT1:def 3;
A7: union g = Y by EQREL_1:def 4;
A8: for x being set holds x in X iff x is_upper_min_depend_of G
proof
let x be set;
for x being set holds x is_upper_min_depend_of G implies x in bool Y
proof
let x be set;
assume x is_upper_min_depend_of G;
then ex A being set st A c= g & A<>{} & x = union A
by A6,PARTIT1:def 1;
then x c= union g by ZFMISC_1:77;
hence thesis by A7;
end;
hence thesis by A1;
end;
A9: Y c= union X
proof
let y be object;
assume y in Y;
then reconsider y as Element of Y;
consider a being Subset of Y such that
A10: y in a and
A11: a is_upper_min_depend_of G by A5,Th2;
a in X by A8,A11;
hence thesis by A10,TARSKI:def 4;
end;
A12: for A being set st A in g holds A<>{} & for B being set st B in g
holds A=B or A misses B by EQREL_1:def 4;
A13: for A being Subset of Y st A in X holds A<>{} & for B being Subset
of Y st B in X holds A=B or A misses B
proof
let A be Subset of Y;
assume A in X;
then
A14: A is_upper_min_depend_of G by A8;
then consider Aa being set such that
A15: Aa c= g and
A16: Aa<>{} and
A17: A = union Aa by A6,PARTIT1:def 1;
consider aa being object such that
A18: aa in Aa by A16,XBOOLE_0:def 1;
reconsider aa as set by TARSKI:1;
A19: aa c= union Aa by A18,ZFMISC_1:74;
aa<>{} by A12,A15,A18;
hence A<>{} by A17,A19;
let B be Subset of Y;
assume B in X;
then
A20: B is_upper_min_depend_of G by A8;
now
assume
A21: A meets B;
A22: for d being a_partition of Y st d in G holds A /\ B
is_a_dependent_set_of d
proof
let d be a_partition of Y;
assume d in G;
then
A is_a_dependent_set_of d & B is_a_dependent_set_of d by A14,A20;
hence thesis by A21,PARTIT1:9;
end;
A23: A /\ B = B by A20,A22,XBOOLE_1:17;
A24: B c= A
by A23,XBOOLE_0:def 4;
A25: A /\ B = A by A14,A22,XBOOLE_1:17;
A c= B
by A25,XBOOLE_0:def 4;
hence A=B by A24,XBOOLE_0:def 10;
end;
hence thesis;
end;
take X;
X c= bool Y
by A1;
then reconsider X as Subset-Family of Y;
X is a_partition of Y by A9,A13,A2,EQREL_1:def 4,XBOOLE_0:def 10;
hence thesis by A8;
end;
thus thesis;
end;
uniqueness
proof
let A1,A2 be a_partition of Y;
now
assume that
G<>{} and
A26: for x being set holds x in A1 iff x is_upper_min_depend_of G and
A27: for x being set holds x in A2 iff x is_upper_min_depend_of G;
for y being object holds y in A1 iff y in A2 by A27,A26;
hence A1=A2 by TARSKI:2;
end;
hence thesis;
end;
consistency;
end;
theorem
for G being Subset of PARTITIONS(Y),PA being a_partition of Y st PA in
G holds PA '>' ('/\' G)
proof
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
assume
A1: PA in G;
for x being set st x in ('/\' G) ex a being set st a in PA & x c= a
proof
let x be set;
assume x in ('/\' G);
then consider h being Function, F being Subset-Family of Y such that
A2: dom h=G and
A3: rng h =F and
A4: for d being set st d in G holds h.d in d and
A5: x=Intersect F and
x<>{} by Def1;
set a = h.PA;
A6: a in PA by A1,A4;
A7: a in rng h by A1,A2,FUNCT_1:def 3;
then Intersect F = meet F by A3,SETFAM_1:def 9;
hence thesis by A3,A5,A6,A7,SETFAM_1:3;
end;
hence thesis by SETFAM_1:def 2;
end;
theorem
for G being Subset of PARTITIONS(Y),PA being a_partition of Y st PA in
G holds PA '<' ('\/' G)
proof
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
assume
A1: PA in G;
for a being set st a in PA ex b being set st b in ('\/' G) & a c= b
proof
let a be set;
set x = the Element of a;
A2: union ('\/' G) = Y by EQREL_1:def 4;
assume
A3: a in PA;
then
A4: a<>{} by EQREL_1:def 4;
then x in Y by A3,TARSKI:def 3;
then consider b being set such that
A5: x in b and
A6: b in ('\/' G) by A2,TARSKI:def 4;
b is_upper_min_depend_of G by A1,A6,Def3;
then consider B being set such that
A7: B c= PA and
B<>{} and
A8: b = union B by A1,PARTIT1:def 1;
a in B
proof
consider u being set such that
A9: x in u and
A10: u in B by A5,A8,TARSKI:def 4;
A11: a /\ u <> {} by A4,A9,XBOOLE_0:def 4;
u in PA by A7,A10;
hence thesis by A3,A10,A11,EQREL_1:def 4,XBOOLE_0:def 7;
end;
hence thesis by A6,A8,ZFMISC_1:74;
end;
hence thesis by SETFAM_1:def 2;
end;
begin :: Chap. 2 Coordinate and Quantifiers
definition
let Y;
let G be Subset of PARTITIONS(Y);
attr G is generating means
('/\' G) = %I(Y);
end;
definition
let Y;
let G be Subset of PARTITIONS(Y);
attr G is independent means
for h being Function, F being Subset-Family of Y
st dom h=G & rng h=F & (for d being set st d in G holds h.d in d) holds (
Intersect F)<>{};
end;
definition
let Y;
let G be Subset of PARTITIONS(Y);
pred G is_a_coordinate means
G is independent generating;
end;
definition
let Y;
let PA be a_partition of Y;
redefine func {PA} -> Subset of PARTITIONS(Y); :: redefines { (TARSKI, definition)
coherence
proof
PA in PARTITIONS(Y) by PARTIT1:def 3;
hence thesis by ZFMISC_1:31;
end;
end;
definition
let Y;
let PA be a_partition of Y;
let G be Subset of PARTITIONS(Y);
func CompF(PA,G) -> a_partition of Y equals
'/\' (G \ {PA});
correctness;
end;
definition
let Y;
let a be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y),PA be a_partition of Y;
pred a is_independent_of PA,G means
a is_dependent_of CompF(PA,G);
end;
definition
let Y;
let a be Function of Y,BOOLEAN, G be Subset of PARTITIONS(Y), PA be
a_partition of Y;
func All(a,PA,G) -> Function of Y,BOOLEAN equals
B_INF(a,CompF(PA,G));
correctness;
end;
definition
let Y;
let a be Function of Y,BOOLEAN, G be Subset of PARTITIONS(Y), PA be
a_partition of Y;
func Ex(a,PA,G) -> Function of Y,BOOLEAN equals
B_SUP(a,CompF(PA,G));
correctness;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a,PA,G) is_dependent_of CompF(PA,G)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let F be set;
assume
A1: F in CompF(PA,G);
thus for x1,x2 being set st x1 in F & x2 in F holds All(a,PA,G).x1=All(a,PA,
G).x2
proof
let x1,x2 be set;
assume
A2: x1 in F & x2 in F;
then reconsider x1,x2 as Element of Y by A1;
A3: x2 in EqClass(x2,CompF(PA,G)) by EQREL_1:def 6;
F = EqClass(x2,CompF(PA,G)) or F misses EqClass(x2,CompF(PA,G)) by A1,
EQREL_1:def 4;
then
A4: EqClass(x1,CompF(PA,G)) = EqClass(x2,CompF(PA,G)) by A2,A3,EQREL_1:def 6
,XBOOLE_0:3;
per cases;
suppose
A5: (for x being Element of Y st x in EqClass(x1,CompF(PA,G)) holds
a.x=TRUE) & for x being Element of Y st x in EqClass(x2,CompF(PA,G)) holds a.x=
TRUE;
then All(a,PA,G).x2=TRUE by BVFUNC_1:def 16;
hence thesis by A5,BVFUNC_1:def 16;
end;
suppose
(for x being Element of Y st x in EqClass(x1,CompF(PA,G)) holds
a.x=TRUE) & not (for x being Element of Y st x in EqClass(x2,CompF(PA,G)) holds
a.x=TRUE);
hence thesis by A4;
end;
suppose
not (for x being Element of Y st x in EqClass(x1,CompF(PA,G))
holds a.x=TRUE) & for x being Element of Y st x in EqClass(x2,CompF(PA,G))
holds a.x=TRUE;
hence thesis by A4;
end;
suppose
A6: not (for x being Element of Y st x in EqClass(x1,CompF(PA,G))
holds a.x=TRUE) & not (for x being Element of Y st x in EqClass(x2,CompF(PA,G))
holds a.x=TRUE);
then All(a,PA,G).x2=FALSE by BVFUNC_1:def 16;
hence thesis by A6,BVFUNC_1:def 16;
end;
end;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(a,PA,G) is_dependent_of CompF(PA,G)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let F be set;
assume
A1: F in CompF(PA,G);
thus for x1,x2 being set st x1 in F & x2 in F holds Ex(a,PA,G).x1=Ex(a,PA,G)
.x2
proof
let x1,x2 be set;
assume
A2: x1 in F & x2 in F;
then reconsider x1, x2 as Element of Y by A1;
A3: x2 in EqClass(x2,CompF(PA,G)) by EQREL_1:def 6;
F = EqClass(x2,CompF(PA,G)) or F misses EqClass(x2,CompF(PA,G)) by A1,
EQREL_1:def 4;
then
A4: EqClass(x1,CompF(PA,G)) = EqClass(x2,CompF(PA,G)) by A2,A3,EQREL_1:def 6
,XBOOLE_0:3;
per cases;
suppose
A5: (ex x being Element of Y st x in EqClass(x1,CompF(PA,G)) & a.x=
TRUE) & ex x being Element of Y st x in EqClass(x2,CompF(PA,G)) & a.x=TRUE;
then B_SUP(a,CompF(PA,G)).x1 = TRUE by BVFUNC_1:def 17;
hence thesis by A5,BVFUNC_1:def 17;
end;
suppose
(ex x being Element of Y st x in EqClass(x1,CompF(PA,G)) & a.x=
TRUE) & not (ex x being Element of Y st x in EqClass(x2,CompF(PA,G)) & a.x=TRUE
);
hence thesis by A4;
end;
suppose
not (ex x being Element of Y st x in EqClass(x1,CompF(PA,G)) &
a.x=TRUE) & ex x being Element of Y st x in EqClass(x2,CompF(PA,G)) & a.x=TRUE;
hence thesis by A4;
end;
suppose
A6: not (ex x being Element of Y st x in EqClass(x1,CompF(PA,G)) &
a.x=TRUE) & not (ex x being Element of Y st x in EqClass(x2,CompF(PA,G)) & a.x=
TRUE);
then B_SUP(a,CompF(PA,G)).x1 = FALSE by BVFUNC_1:def 17;
hence thesis by A6,BVFUNC_1:def 17;
end;
end;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(I_el(Y),PA,G) = I_el(Y)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
for z being Element of Y holds All(I_el Y,PA,G).z=TRUE
proof
let z be Element of Y;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (I_el Y)
.x=TRUE by BVFUNC_1:def 11;
hence thesis by BVFUNC_1:def 16;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(I_el(Y),PA,G) = I_el(Y)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
for z being Element of Y holds Ex(I_el Y,PA,G).z=TRUE
proof
let z be Element of Y;
z in EqClass(z,CompF(PA,G)) & (I_el Y).z=TRUE by BVFUNC_1:def 11
,EQREL_1:def 6;
hence thesis by BVFUNC_1:def 17;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(O_el(Y),PA,G) = O_el(Y)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
for z being Element of Y holds All(O_el Y,PA,G).z=FALSE
proof
let z be Element of Y;
z in EqClass(z,CompF(PA,G)) & (O_el Y).z=FALSE by BVFUNC_1:def 10
,EQREL_1:def 6;
hence thesis by BVFUNC_1:def 16;
end;
hence thesis by BVFUNC_1:def 10;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(O_el(Y),PA,G) = O_el(Y)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
for z being Element of Y holds Ex(O_el Y,PA,G).z=FALSE
proof
let z be Element of Y;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (O_el Y)
.x<>TRUE by BVFUNC_1:def 10;
hence thesis by BVFUNC_1:def 17;
end;
hence thesis by BVFUNC_1:def 10;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a,PA,G) '<' a
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let z be Element of Y;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume All(a,PA,G).z= TRUE;
hence a.z=TRUE by A1,BVFUNC_1:def 16;
end;
theorem
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds a '<' Ex(a,PA,G)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let z be Element of Y;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume a.z= TRUE;
hence Ex(a,PA,G).z=TRUE by A1,BVFUNC_1:def 17;
end;
theorem
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a,PA,G) 'or' All(b,PA,G) '<' All(a 'or' b,PA,G)
proof
let a,b be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let z be Element of Y;
assume (All(a,PA,G) 'or' All(b,PA,G)).z=TRUE;
then
A1: All(a,PA,G).z 'or' All(b,PA,G).z=TRUE by BVFUNC_1:def 4;
A2: All(b,PA,G).z=TRUE or All(b,PA,G).z=FALSE by XBOOLEAN:def 3;
now
per cases by A1,A2,BINARITH:3;
case
A3: All(a,PA,G).z=TRUE;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a
'or' b).x=TRUE
proof
let x be Element of Y;
assume
A4: x in EqClass(z,CompF(PA,G));
(a 'or' b).x =a.x 'or' b.x by BVFUNC_1:def 4
.=TRUE 'or' b.x by A3,A4,BVFUNC_1:def 16
.=TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 16;
end;
case
A5: All(b,PA,G).z=TRUE;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a
'or' b).x=TRUE
proof
let x be Element of Y;
assume
A6: x in EqClass(z,CompF(PA,G));
(a 'or' b).x =a.x 'or' b.x by BVFUNC_1:def 4
.=a.x 'or' TRUE by A5,A6,BVFUNC_1:def 16
.=TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 16;
end;
end;
hence thesis;
end;
theorem
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' All(b,PA,G)
proof
let a,b be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let z be Element of Y;
assume
A1: All(a 'imp' b,PA,G).z=TRUE;
A2: (All(a,PA,G) 'imp' All(b,PA,G)).z =('not' All(a,PA,G).z) 'or' All(b,PA,G
).z by BVFUNC_1:def 8;
per cases;
suppose
(for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x
=TRUE) & for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE
;
then B_INF(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
then
(All(a,PA,G) 'imp' All(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
.=TRUE by BINARITH:10;
hence thesis;
end;
suppose
A3: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x
=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x
=TRUE);
then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: b.x1<>TRUE;
A6: a.x1=TRUE by A3,A4;
(a 'imp' b).x1 =('not' a.x1) 'or' b.x1 by BVFUNC_1:def 8
.=('not' TRUE) 'or' FALSE by A5,A6,XBOOLEAN:def 3
.=FALSE 'or' FALSE by MARGREL1:11
.=FALSE;
hence thesis by A1,A4,BVFUNC_1:def 16;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
b.x=TRUE;
then
(All(a,PA,G) 'imp' All(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by A2,
BVFUNC_1:def 16
.=TRUE by BINARITH:10;
hence thesis;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds b.x=TRUE);
then (All(a,PA,G) 'imp' All(b,PA,G)).z
=TRUE 'or' All(b,PA,G).z by A2,BVFUNC_1:def 16,MARGREL1:11
.=TRUE by BINARITH:10;
hence thesis;
end;
end;
theorem
for a,b being Function of Y,BOOLEAN,G being Subset of PARTITIONS
(Y) , PA being a_partition of Y holds Ex(a '&' b,PA,G) '<' Ex(a,PA,G) '&' Ex(b,
PA,G)
proof
let a,b be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
let z be Element of Y;
assume Ex(a '&' b,PA,G).z=TRUE;
then consider x1 being Element of Y such that
A1: x1 in EqClass(z,CompF(PA,G)) and
A2: (a '&' b).x1=TRUE by BVFUNC_1:def 17;
A3: a.x1 '&' b.x1=TRUE by A2,MARGREL1:def 20;
then
A4: b.x1=TRUE by MARGREL1:12;
a.x1=TRUE by A3,MARGREL1:12;
then
A5: Ex(a,PA,G).z=TRUE by A1,BVFUNC_1:def 17;
(Ex(a,PA,G) '&' Ex(b,PA,G)).z = Ex(a,PA,G).z '&' Ex(b,PA,G).z by
MARGREL1:def 20
.= TRUE '&' TRUE by A1,A4,A5,BVFUNC_1:def 17
.= TRUE;
hence thesis;
end;
theorem
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(a,PA,G) 'xor' Ex(b,PA,G) '<' Ex(a 'xor' b,PA,G)
proof
let a,b be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let z be Element of Y;
A1: (Ex(a,PA,G) 'xor' Ex(b,PA,G)).z =Ex(a,PA,G).z 'xor' Ex(b,PA,G).z by
BVFUNC_1:def 5
.=('not' Ex(a,PA,G).z '&' Ex(b,PA,G).z) 'or' (Ex(a,PA,G).z '&' 'not' Ex(
b,PA,G).z);
A2: ('not' Ex(a,PA,G).z '&' Ex(b,PA,G).z)=TRUE or ('not' Ex(a,PA,G).z '&' Ex
(b,PA,G).z)=FALSE by XBOOLEAN:def 3;
A3: 'not' FALSE=TRUE by MARGREL1:11;
assume
A4: (Ex(a,PA,G) 'xor' Ex(b,PA,G)).z=TRUE;
now
per cases by A4,A1,A2,BINARITH:3;
case
A5: ('not' Ex(a,PA,G).z '&' Ex(b,PA,G).z)=TRUE;
then Ex(b,PA,G).z=TRUE by MARGREL1:12;
then consider x1 being Element of Y such that
A6: x1 in EqClass(z,CompF(PA,G)) and
A7: b.x1=TRUE by BVFUNC_1:def 17;
'not' Ex(a,PA,G).z=TRUE by A5,MARGREL1:12;
then a.x1<>TRUE by A6,BVFUNC_1:def 17,MARGREL1:11;
then
A8: a.x1=FALSE by XBOOLEAN:def 3;
(a 'xor' b).x1 =a.x1 'xor' b.x1 by BVFUNC_1:def 5
.=TRUE 'or' FALSE by A3,A7,A8
.=TRUE by BINARITH:10;
hence thesis by A6,BVFUNC_1:def 17;
end;
case
A9: (Ex(a,PA,G).z '&' 'not' Ex(b,PA,G).z)=TRUE;
then Ex(a,PA,G).z=TRUE by MARGREL1:12;
then consider x1 being Element of Y such that
A10: x1 in EqClass(z,CompF(PA,G)) and
A11: a.x1=TRUE by BVFUNC_1:def 17;
'not' Ex(b,PA,G).z=TRUE by A9,MARGREL1:12;
then b.x1<>TRUE by A10,BVFUNC_1:def 17,MARGREL1:11;
then
A12: b.x1=FALSE by XBOOLEAN:def 3;
(a 'xor' b).x1=a.x1 'xor' b.x1 by BVFUNC_1:def 5
.=FALSE 'or' TRUE by A3,A11,A12
.=TRUE by BINARITH:10;
hence thesis by A10,BVFUNC_1:def 17;
end;
end;
hence thesis;
end;
theorem
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(a,PA,G) 'imp' Ex(b,PA,G) '<' Ex(a 'imp' b,PA,G)
proof
let a,b be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let z be Element of Y;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume (Ex(a,PA,G) 'imp' Ex(b,PA,G)).z=TRUE;
then
A2: ('not' Ex(a,PA,G).z) 'or' Ex(b,PA,G).z=TRUE by BVFUNC_1:def 8;
A3: ('not' Ex(a,PA,G).z)=TRUE or ('not' Ex(a,PA,G).z)=FALSE by XBOOLEAN:def 3;
now
per cases by A2,A3,BINARITH:3;
case
('not' Ex(a,PA,G).z)=TRUE;
then
A4: a.z<>TRUE by A1,BVFUNC_1:def 17,MARGREL1:11;
(a 'imp' b).z=('not' a.z) 'or' b.z by BVFUNC_1:def 8
.=TRUE 'or' b.z by A4,MARGREL1:11,XBOOLEAN:def 3
.=TRUE by BINARITH:10;
hence thesis by A1,BVFUNC_1:def 17;
end;
case
Ex(b,PA,G).z=TRUE;
then consider x1 being Element of Y such that
A5: x1 in EqClass(z,CompF(PA,G)) and
A6: b.x1=TRUE by BVFUNC_1:def 17;
(a 'imp' b).x1 =('not' a.x1) 'or' b.x1 by BVFUNC_1:def 8
.=TRUE by A6,BINARITH:10;
hence thesis by A5,BVFUNC_1:def 17;
end;
end;
hence thesis;
end;
reserve a, u for Function of Y,BOOLEAN;
theorem :: De'Morgan's Law
for PA being a_partition of Y holds 'not' All(a,PA,G) = Ex('not' a,PA, G)
proof
let PA be a_partition of Y;
let z be Element of Y;
per cases;
suppose
A1: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a
.x=TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & ('not' a).x
=TRUE;
then consider x1 being Element of Y such that
A2: x1 in EqClass(z,CompF(PA,G)) and
A3: ('not' a).x1=TRUE;
'not' a.x1 = TRUE by A3,MARGREL1:def 19;
hence thesis by A1,A2,MARGREL1:11;
end;
suppose
A4: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a
.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & ('not'
a).x=TRUE);
then B_INF(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
then
A5: ('not' B_INF(a,CompF(PA,G))).z = 'not' TRUE by MARGREL1:def 19;
B_SUP('not' a,CompF(PA,G)).z = FALSE by A4,BVFUNC_1:def 17;
hence thesis by A5,MARGREL1:11;
end;
suppose
A6: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (
'not' a).x=TRUE;
then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
then
A7: ('not' B_INF(a,CompF(PA,G))).z = 'not' FALSE by MARGREL1:def 19;
B_SUP('not' a,CompF(PA,G)).z = TRUE by A6,BVFUNC_1:def 17;
hence thesis by A7,MARGREL1:11;
end;
suppose
A8: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
('not' a).x=TRUE);
then consider x1 being Element of Y such that
A9: x1 in EqClass(z,CompF(PA,G)) and
A10: a.x1<>TRUE;
('not' a).x1<>TRUE by A8,A9;
then 'not' a.x1<>TRUE by MARGREL1:def 19;
hence thesis by A10,MARGREL1:11,XBOOLEAN:def 3;
end;
end;
theorem :: De'Morgan's Law
for PA being a_partition of Y holds 'not' Ex(a,PA,G) = All('not' a,PA, G)
proof
let PA be a_partition of Y;
let z be Element of Y;
per cases;
suppose
A1: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (
'not' a).x=TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x
=TRUE;
then consider x1 being Element of Y such that
A2: x1 in EqClass(z,CompF(PA,G)) and
A3: a.x1=TRUE;
('not' a).x1='not' TRUE by A3,MARGREL1:def 19;
hence thesis by A1,A2,MARGREL1:11;
end;
suppose
A4: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (
'not' a).x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G))
& a.x=TRUE);
then 'not' B_SUP(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17,MARGREL1:11;
then ('not' B_SUP(a,CompF(PA,G))).z = TRUE by MARGREL1:def 19;
hence thesis by A4,BVFUNC_1:def 16;
end;
suppose
A5: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds ('not' a).x=TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)
) & a.x=TRUE;
then B_SUP(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17;
then
A6: ('not' B_SUP(a,CompF(PA,G))).z = 'not' TRUE by MARGREL1:def 19;
B_INF('not' a,CompF(PA,G)).z = FALSE by A5,BVFUNC_1:def 16;
hence thesis by A6,MARGREL1:11;
end;
suppose
A7: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds ('not' a).x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(
PA,G)) & a.x=TRUE);
then consider x1 being Element of Y such that
A8: x1 in EqClass(z,CompF(PA,G)) and
A9: ('not' a).x1<>TRUE;
('not' a).x1=FALSE by A9,XBOOLEAN:def 3;
then 'not' a.x1=FALSE by MARGREL1:def 19;
hence thesis by A7,A8,MARGREL1:11;
end;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds All(u
'imp' a,PA,G) = u 'imp' All(a,PA,G)
proof
let PA be a_partition of Y;
assume
A1: u is_independent_of PA,G;
A2: (u 'imp' All(a,PA,G)) '<' All(u 'imp' a,PA,G)
proof
let z be Element of Y;
assume (u 'imp' All(a,PA,G)).z= TRUE;
then
A3: ('not' u.z) 'or' All(a,PA,G).z = TRUE by BVFUNC_1:def 8;
A4: All(a,PA,G).z=TRUE or All(a,PA,G).z=FALSE by XBOOLEAN:def 3;
now
per cases by A3,A4,BINARITH:3;
suppose
A5: All(a,PA,G).z=TRUE;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (u
'imp' a).x=TRUE
proof
let x be Element of Y;
assume
A6: x in EqClass(z,CompF(PA,G));
(u 'imp' a).x = ('not' u.x) 'or' a.x by BVFUNC_1:def 8
.= ('not' u.x) 'or' TRUE by A5,A6,BVFUNC_1:def 16
.= TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 16;
end;
suppose
A7: All(a,PA,G).z<>TRUE & ('not' u.z)=TRUE;
A8: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (u
'imp' a).x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then (u 'imp' a).x=('not' u.x) 'or' a.x & u.x = u.z
by A1,A8,BVFUNC_1:def 8,def 15;
hence thesis by A7,BINARITH:10;
end;
hence thesis by BVFUNC_1:def 16;
end;
end;
hence thesis;
end;
All(u 'imp' a,PA,G) '<' (u 'imp' All(a,PA,G))
proof
let z be Element of Y;
assume
A9: All(u 'imp' a,PA,G).z= TRUE;
A10: (u 'imp' All(a,PA,G)).z = ('not' u.z) 'or' All(a,PA,G).z by BVFUNC_1:def 8
;
per cases;
suppose
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a. x=TRUE;
then All(a,PA,G).z =TRUE by BVFUNC_1:def 16;
hence thesis by A10,BINARITH:10;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
('not' u.x)=TRUE;
then ('not' u.z)=TRUE by EQREL_1:def 6;
hence thesis by A10,BINARITH:10;
end;
suppose
A11: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds ('not' u.x)=TRUE);
then consider x1 being Element of Y such that
A12: x1 in EqClass(z,CompF(PA,G)) and
A13: ('not' u.x1)<>TRUE;
consider x2 being Element of Y such that
A14: x2 in EqClass(z,CompF(PA,G)) and
A15: a.x2<>TRUE by A11;
u.x1 = u.x2 by A1,A12,A14,BVFUNC_1:def 15;
then
A16: u.x2=TRUE by A13,MARGREL1:11,XBOOLEAN:def 3;
a.x2=FALSE by A15,XBOOLEAN:def 3;
then (u 'imp' a).x2 = 'not' TRUE 'or' FALSE by A16,BVFUNC_1:def 8;
then (u 'imp' a).x2 = FALSE 'or' FALSE by MARGREL1:11
.= FALSE;
hence thesis by A9,A14,BVFUNC_1:def 16;
end;
end;
hence thesis by A2,BVFUNC_1:15;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'imp' u,PA,G) = Ex(a,PA,G) 'imp' u
proof
let PA be a_partition of Y;
assume
A1: u is_independent_of PA,G;
A2: (Ex(a,PA,G) 'imp' u) '<' All(a 'imp' u,PA,G)
proof
let z be Element of Y;
A3: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume (Ex(a,PA,G) 'imp' u).z= TRUE;
then
A4: ('not' Ex(a,PA,G).z) 'or' u.z = TRUE by BVFUNC_1:def 8;
A5: ('not' Ex(a,PA,G).z)= TRUE or ('not' Ex(a,PA,G).z)= FALSE by XBOOLEAN:def 3
;
now
per cases by A4,A5,BINARITH:3,XBOOLEAN:def 3;
case
A6: u.z= TRUE;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a
'imp' u).x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then (a 'imp' u).x=('not' a.x) 'or' u.x & u.x = u.z by A1,A3,
BVFUNC_1:def 8,def 15;
hence thesis by A6,BINARITH:10;
end;
hence thesis by BVFUNC_1:def 16;
end;
case
A7: ('not' Ex(a,PA,G).z)= TRUE & u.z= FALSE;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a
'imp' u).x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then a.x<>TRUE by A7,BVFUNC_1:def 17,MARGREL1:11;
then (a 'imp' u).x=('not' a.x) 'or' u.x & a.x=FALSE by BVFUNC_1:def 8
,XBOOLEAN:def 3;
then (a 'imp' u).x = TRUE 'or' u.x by MARGREL1:11
.= TRUE by BINARITH:10;
hence thesis;
end;
hence thesis by BVFUNC_1:def 16;
end;
end;
hence thesis;
end;
All(a 'imp' u,PA,G) '<' (Ex(a,PA,G) 'imp' u)
proof
let z be Element of Y;
assume
A8: All(a 'imp' u,PA,G).z= TRUE;
A9: (Ex(a,PA,G) 'imp' u).z = ('not' Ex(a,PA,G).z) 'or' u.z by BVFUNC_1:def 8;
per cases;
suppose
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u. x=TRUE;
then (Ex(a,PA,G) 'imp' u).z = ('not' Ex(a,PA,G).z) 'or' TRUE
by A9,EQREL_1:def 6
.= TRUE by BINARITH:10;
hence thesis;
end;
suppose
A10: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=
TRUE;
then consider x1 being Element of Y such that
A11: x1 in EqClass(z,CompF(PA,G)) and
A12: u.x1<>TRUE;
consider x2 being Element of Y such that
A13: x2 in EqClass(z,CompF(PA,G)) and
A14: a.x2=TRUE by A10;
A15: u.x1 = u.x2 by A1,A11,A13,BVFUNC_1:def 15;
(a 'imp' u).x2 = ('not' a.x2) 'or' u.x2 by BVFUNC_1:def 8
.= ('not' TRUE) 'or' FALSE by A12,A14,A15,XBOOLEAN:def 3
.= FALSE 'or' FALSE by MARGREL1:11
.= FALSE;
hence thesis by A8,A13,BVFUNC_1:def 16;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
a.x=TRUE);
then (Ex(a,PA,G) 'imp' u).z = ('not' FALSE) 'or' u.z by A9,
BVFUNC_1:def 17
.= TRUE 'or' u.z by MARGREL1:11
.= TRUE by BINARITH:10;
hence thesis;
end;
end;
hence thesis by A2,BVFUNC_1:15;
end;
theorem Th22:
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'or' a,PA,G) = u 'or' All(a,PA,G)
proof
let PA be a_partition of Y;
assume
A1: u is_independent_of PA,G;
let z be Element of Y;
A2: (u 'or' B_INF(a,CompF(PA,G))).z = u.z 'or' B_INF(a,CompF(PA,G)).z by
BVFUNC_1:def 4;
per cases;
suppose
A3: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a. x=TRUE;
A4: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (u
'or' a).x=TRUE
proof
let x be Element of Y;
assume
A5: x in EqClass(z,CompF(PA,G));
(u 'or' a).x = u.x 'or' a.x by BVFUNC_1:def 4
.= u.x 'or' TRUE by A3,A5
.= TRUE by BINARITH:10;
hence thesis;
end;
B_INF(a,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 16;
then (u 'or' B_INF(a,CompF(PA,G))).z = TRUE by A2,BINARITH:10;
hence thesis by A4,BVFUNC_1:def 16;
end;
suppose
A6: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
u.x=TRUE;
A7: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (u
'or' a).x=TRUE
proof
let x be Element of Y;
assume
A8: x in EqClass(z,CompF(PA,G));
(u 'or' a).x = u.x 'or' a.x by BVFUNC_1:def 4
.= TRUE 'or' a.x by A6,A8
.= TRUE by BINARITH:10;
hence thesis;
end;
(u 'or' B_INF(a,CompF(PA,G))).z = TRUE 'or' B_INF(a,CompF(PA,G)).z
by A2,A6,EQREL_1:def 6;
then (u 'or' B_INF(a,CompF(PA,G))).z = TRUE by BINARITH:10;
hence thesis by A7,BVFUNC_1:def 16;
end;
suppose
A9: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE);
then consider x2 being Element of Y such that
A10: x2 in EqClass(z,CompF(PA,G)) and
A11: u.x2<>TRUE;
consider x1 being Element of Y such that
A12: x1 in EqClass(z,CompF(PA,G)) and
A13: a.x1<>TRUE by A9;
u.x1 = u.x2 by A1,A12,A10,BVFUNC_1:def 15;
then
A14: u.x1 = FALSE by A11,XBOOLEAN:def 3;
A15: B_INF(a,CompF(PA,G)).z = FALSE by A9,BVFUNC_1:def 16;
z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
then
A16: u.x1 = u.z by A1,A12,BVFUNC_1:def 15;
a.x1 = FALSE by A13,XBOOLEAN:def 3;
then (u 'or' a).x1 = FALSE 'or' FALSE by A14,BVFUNC_1:def 4;
hence thesis by A2,A15,A12,A14,A16,BVFUNC_1:def 16;
end;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'or' u,PA,G) = All(a,PA,G) 'or' u by Th22;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'or' u,PA,G) '<' Ex(a,PA,G) 'or' u
proof
let PA be a_partition of Y;
assume
A1: u is_independent_of PA,G;
let z be Element of Y;
assume
A2: All(a 'or' u,PA,G).z= TRUE;
A3: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE
or u.x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then (a 'or' u).x=TRUE by A2,BVFUNC_1:def 16;
then
A4: a.x 'or' u.x=TRUE by BVFUNC_1:def 4;
u.x= TRUE or u.x=FALSE by XBOOLEAN:def 3;
hence thesis by A4,BINARITH:3;
end;
A5: (Ex(a,PA,G) 'or' u).z = Ex(a,PA,G).z 'or' u.z by BVFUNC_1:def 4;
per cases;
suppose
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.x =TRUE;
then (Ex(a,PA,G) 'or' u).z = Ex(a,PA,G).z 'or' TRUE by A5,EQREL_1:def 6
.= TRUE by BINARITH:10;
hence thesis;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=
TRUE;
then (Ex(a,PA,G) 'or' u).z = TRUE 'or' u.z by A5,BVFUNC_1:def 17
.= TRUE by BINARITH:10;
hence thesis;
end;
suppose
A6: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
a.x=TRUE);
A7: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
A8: a.z<>TRUE by A6,EQREL_1:def 6;
consider x1 being Element of Y such that
A9: x1 in EqClass(z,CompF(PA,G)) and
A10: u.x1<>TRUE by A6;
u.x1=u.z by A1,A7,A9,BVFUNC_1:def 15;
hence thesis by A3,A8,A10,EQREL_1:def 6;
end;
end;
theorem Th25:
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u '&' a,PA,G) = u '&' All(a,PA,G)
proof
let PA be a_partition of Y;
A1: All(u '&' a,PA,G) '<' (u '&' All(a,PA,G))
proof
let z be Element of Y;
assume
A2: All(u '&' a,PA,G).z= TRUE;
A3: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then
A4: (u '&' a).x=TRUE by A2,BVFUNC_1:def 16;
(u '&' a).x=u.x '&' a.x by MARGREL1:def 20;
hence thesis by A4,MARGREL1:12;
end;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then
A5: (u '&' a).x=TRUE by A2,BVFUNC_1:def 16;
(u '&' a).x=u.x '&' a.x by MARGREL1:def 20;
hence thesis by A5,MARGREL1:12;
end;
then
A6: (u '&' All(a,PA,G)).z= u.z '&' All(a,PA,G).z & All(a,PA,G).z=TRUE by
BVFUNC_1:def 16,MARGREL1:def 20;
u.z=TRUE by A3,EQREL_1:def 6;
hence thesis by A6;
end;
assume
A7: u is_independent_of PA,G;
(u '&' All(a,PA,G)) '<' All(u '&' a,PA,G)
proof
let z be Element of Y;
A8: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume (u '&' All(a,PA,G)).z= TRUE;
then
A9: u.z '&' All(a,PA,G).z= TRUE by MARGREL1:def 20;
then
A10: All(a,PA,G).z=TRUE by MARGREL1:12;
A11: u.z=TRUE by A9,MARGREL1:12;
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (u '&'
a).x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then a.x=TRUE & u.x=u.z by A7,A10,A8,BVFUNC_1:def 15,def 16;
then (u '&' a).x =TRUE '&' TRUE by A11,MARGREL1:def 20
.=TRUE;
hence thesis;
end;
hence thesis by BVFUNC_1:def 16;
end;
hence thesis by A1,BVFUNC_1:15;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'&' u,PA,G) = All(a,PA,G) '&' u by Th25;
theorem
for PA being a_partition of Y holds All(a '&' u,PA,G) '<' Ex(a,PA,G) '&' u
proof
let PA be a_partition of Y;
let z be Element of Y;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume
A2: All(a '&' u,PA,G).z= TRUE;
A3: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE &
u.x=TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(PA,G));
then (a '&' u).x=TRUE by A2,BVFUNC_1:def 16;
then a.x '&' u.x=TRUE by MARGREL1:def 20;
hence thesis by MARGREL1:12;
end;
A4: (Ex(a,PA,G) '&' u).z = Ex(a,PA,G).z '&' u.z by MARGREL1:def 20;
per cases;
suppose
A5: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.x= TRUE;
now
per cases;
suppose
ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE;
then Ex(a,PA,G).z = TRUE by BVFUNC_1:def 17;
hence (Ex(a,PA,G) '&' u).z = TRUE '&' TRUE by A4,A5,EQREL_1:def 6
.= TRUE;
end;
suppose
not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
a.x=TRUE);
then a.z<>TRUE by EQREL_1:def 6;
hence thesis by A3,A1;
end;
end;
hence thesis;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE);
hence thesis by A3;
end;
end;
theorem Th28:
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'xor' a,PA,G) '<' u 'xor' All(a,PA,G)
proof
let PA be a_partition of Y;
assume
A1: u is_independent_of PA,G;
let z be Element of Y;
assume
A2: All(u 'xor' a,PA,G).z= TRUE;
A3: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
A4: 'not' FALSE=TRUE & (u 'xor' All(a,PA,G)).z = All(a,PA,G).z 'xor' u.z by
BVFUNC_1:def 5,MARGREL1:11;
per cases;
suppose
(for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.x
=TRUE) & for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE
;
then
A5: u.z=TRUE & a.z=TRUE by EQREL_1:def 6;
A6: FALSE '&' TRUE = FALSE by MARGREL1:12;
(u 'xor' a).z =a.z 'xor' u.z by BVFUNC_1:def 5
.=FALSE by A5,A6,MARGREL1:11;
hence thesis by A2,A3,BVFUNC_1:def 16;
end;
suppose
A7: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.
x=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.
x=TRUE);
then consider x1 being Element of Y such that
A8: x1 in EqClass(z,CompF(PA,G)) and
a.x1<>TRUE;
A9: u.x1=TRUE by A7,A8;
A10: All(a,PA,G).z = FALSE by A7,BVFUNC_1:def 16;
u.z=u.x1 by A1,A3,A8,BVFUNC_1:def 15;
then (u 'xor' All(a,PA,G)).z =TRUE 'or' FALSE by A4,A10,A9
.=TRUE by BINARITH:3;
hence thesis;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE);
then consider x1 being Element of Y such that
A11: x1 in EqClass(z,CompF(PA,G)) and
A12: u.x1<>TRUE;
now
per cases;
suppose
A13: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE;
u.z=u.x1 by A1,A3,A11,BVFUNC_1:def 15;
then
A14: u.z=FALSE by A12,XBOOLEAN:def 3;
All(a,PA,G).z = TRUE by A13,BVFUNC_1:def 16;
then (u 'xor' All(a,PA,G)).z =FALSE 'or' TRUE by A4,A14
.=TRUE by BINARITH:3;
hence thesis;
end;
suppose
not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE);
then consider x2 being Element of Y such that
A15: x2 in EqClass(z,CompF(PA,G)) and
A16: a.x2<>TRUE;
A17: a.x2=FALSE by A16,XBOOLEAN:def 3;
u.x1=u.x2 by A1,A11,A15,BVFUNC_1:def 15;
then
A18: u.x2=FALSE by A12,XBOOLEAN:def 3;
(u 'xor' a).x2 =a.x2 'xor' u.x2 by BVFUNC_1:def 5
.=FALSE by A18,A17,MARGREL1:12;
hence thesis by A2,A15,BVFUNC_1:def 16;
end;
end;
hence thesis;
end;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'xor' u,PA,G) '<' All(a,PA,G) 'xor' u by Th28;
theorem Th30:
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'eqv' a,PA,G) '<' u 'eqv' All(a,PA,G)
proof
let PA be a_partition of Y;
A1: 'not' FALSE=TRUE by MARGREL1:11;
assume
A2: u is_independent_of PA,G;
let z be Element of Y;
assume
A3: All(u 'eqv' a,PA,G).z= TRUE;
A4: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
per cases;
suppose
(for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.x
=TRUE) & for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE
;
then
A5: All(a,PA,G).z=TRUE & u.z=TRUE by BVFUNC_1:def 16,EQREL_1:def 6;
(u 'eqv' All(a,PA,G)).z ='not'(u.z 'xor' All(a,PA,G).z) by BVFUNC_1:def 9
.=TRUE by A1,A5,MARGREL1:13;
hence thesis;
end;
suppose
A6: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.
x=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.
x=TRUE);
then consider x1 being Element of Y such that
A7: x1 in EqClass(z,CompF(PA,G)) and
A8: a.x1<>TRUE;
A9: u.x1=TRUE by A6,A7;
A10: a.x1=FALSE by A8,XBOOLEAN:def 3;
(u 'eqv' a).x1 ='not'(u.x1 'xor' a.x1) by BVFUNC_1:def 9
.='not'(FALSE 'or' TRUE) by A1,A9,A10
.=FALSE by BINARITH:3,MARGREL1:11;
hence thesis by A3,A7,BVFUNC_1:def 16;
end;
suppose
A11: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE) & for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
a.x=TRUE;
then consider x1 being Element of Y such that
A12: x1 in EqClass(z,CompF(PA,G)) and
A13: u.x1<>TRUE;
A14: a.x1=TRUE by A11,A12;
A15: u.x1=FALSE by A13,XBOOLEAN:def 3;
(u 'eqv' a).x1 ='not'(u.x1 'xor' a.x1) by BVFUNC_1:def 9
.='not'(TRUE 'or' FALSE) by A1,A15,A14
.=FALSE by BINARITH:3,MARGREL1:11;
hence thesis by A3,A12,BVFUNC_1:def 16;
end;
suppose
A16: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds u.x=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE);
then consider x1 being Element of Y such that
A17: x1 in EqClass(z,CompF(PA,G)) and
A18: u.x1<>TRUE;
u.x1=u.z by A2,A4,A17,BVFUNC_1:def 15;
then
A19: u.z=FALSE by A18,XBOOLEAN:def 3;
A20: All(a,PA,G).z = FALSE by A16,BVFUNC_1:def 16;
(u 'eqv' All(a,PA,G)).z ='not'(u.z 'xor' All(a,PA,G).z) by BVFUNC_1:def 9
.=TRUE by A20,A19,MARGREL1:11,13;
hence thesis;
end;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'eqv' u,PA,G) '<' All(a,PA,G) 'eqv' u by Th30;
theorem Th32:
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(u 'or' a,PA,G) = u 'or' Ex(a,PA,G)
proof
let PA be a_partition of Y;
assume
A1: u is_independent_of PA,G;
A2: Ex(u 'or' a,PA,G) '<' u 'or' Ex(a,PA,G)
proof
let z be Element of Y;
A3: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
A4: (u 'or' Ex(a,PA,G)).z = u.z 'or' Ex(a,PA,G).z by BVFUNC_1:def 4;
assume Ex(u 'or' a,PA,G).z= TRUE;
then consider x1 being Element of Y such that
A5: x1 in EqClass(z,CompF(PA,G)) and
A6: (u 'or' a).x1=TRUE by BVFUNC_1:def 17;
A7: u.x1= TRUE or u.x1=FALSE by XBOOLEAN:def 3;
A8: u.x1 'or' a.x1=TRUE by A6,BVFUNC_1:def 4;
now
per cases by A8,A7,BINARITH:3;
case
A9: u.x1=TRUE;
u.z=u.x1 by A1,A5,A3,BVFUNC_1:def 15;
hence thesis by A4,A9,BINARITH:10;
end;
case
a.x1=TRUE;
then (u 'or' Ex(a,PA,G)).z = u.z 'or' TRUE by A5,A4,BVFUNC_1:def 17
.= TRUE by BINARITH:10;
hence thesis;
end;
end;
hence thesis;
end;
u 'or' Ex(a,PA,G) '<' Ex(u 'or' a,PA,G)
proof
let z be Element of Y;
A10: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume (u 'or' Ex(a,PA,G)).z= TRUE;
then
A11: u.z 'or' Ex(a,PA,G).z=TRUE by BVFUNC_1:def 4;
A12: Ex(a,PA,G).z= TRUE or Ex(a,PA,G).z=FALSE by XBOOLEAN:def 3;
now
per cases by A11,A12,BINARITH:3;
case
u.z=TRUE;
then (u 'or' a).z = TRUE 'or' a.z by BVFUNC_1:def 4
.= TRUE by BINARITH:10;
hence thesis by A10,BVFUNC_1:def 17;
end;
case
Ex(a,PA,G).z=TRUE;
then consider x1 being Element of Y such that
A13: x1 in EqClass(z,CompF(PA,G)) and
A14: a.x1=TRUE by BVFUNC_1:def 17;
(u 'or' a).x1 = u.x1 'or' a.x1 by BVFUNC_1:def 4
.= TRUE by A14,BINARITH:10;
hence thesis by A13,BVFUNC_1:def 17;
end;
end;
hence thesis;
end;
hence thesis by A2,BVFUNC_1:15;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds Ex(a
'or' u,PA,G) = Ex(a,PA,G) 'or' u by Th32;
theorem Th34:
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(u '&' a,PA,G) = u '&' Ex(a,PA,G)
proof
let PA be a_partition of Y;
assume
A1: u is_independent_of PA,G;
A2: Ex(u '&' a,PA,G) '<' (u '&' Ex(a,PA,G))
proof
let z be Element of Y;
assume Ex(u '&' a,PA,G).z= TRUE;
then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: (u '&' a).x1=TRUE by BVFUNC_1:def 17;
A5: u.x1 '&' a.x1=TRUE by A4,MARGREL1:def 20;
then a.x1=TRUE by MARGREL1:12;
then
A6: Ex(a,PA,G).z=TRUE by A3,BVFUNC_1:def 17;
z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
then
A7: u.z=u.x1 by A1,A3,BVFUNC_1:def 15;
u.x1=TRUE by A5,MARGREL1:12;
then (u '&' Ex(a,PA,G)).z =TRUE '&' TRUE by A6,A7,MARGREL1:def 20
.=TRUE;
hence thesis;
end;
(u '&' Ex(a,PA,G)) '<' Ex(u '&' a,PA,G)
proof
let z be Element of Y;
assume (u '&' Ex(a,PA,G)).z= TRUE;
then
A8: u.z '&' Ex(a,PA,G).z=TRUE by MARGREL1:def 20;
then
A9: u.z=TRUE by MARGREL1:12;
Ex(a,PA,G).z=TRUE by A8,MARGREL1:12;
then consider x1 being Element of Y such that
A10: x1 in EqClass(z,CompF(PA,G)) and
A11: a.x1=TRUE by BVFUNC_1:def 17;
z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
then u.x1=u.z by A1,A10,BVFUNC_1:def 15;
then (u '&' a).x1=TRUE '&' TRUE by A9,A11,MARGREL1:def 20
.=TRUE;
hence thesis by A10,BVFUNC_1:def 17;
end;
hence thesis by A2,BVFUNC_1:15;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds Ex(a
'&' u,PA,G) = Ex(a,PA,G) '&' u by Th34;
theorem
for PA being a_partition of Y holds u 'imp' Ex(a,PA,G) '<' Ex(u 'imp' a,PA,G)
proof
let PA be a_partition of Y;
let z be Element of Y;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume (u 'imp' Ex(a,PA,G)).z= TRUE;
then
A2: ('not' u.z) 'or' Ex(a,PA,G).z=TRUE by BVFUNC_1:def 8;
A3: Ex(a,PA,G).z= TRUE or Ex(a,PA,G).z=FALSE by XBOOLEAN:def 3;
now
per cases by A2,A3,BINARITH:3;
case
A4: 'not' u.z=TRUE;
(u 'imp' a).z = ('not' u.z) 'or' a.z by BVFUNC_1:def 8
.= TRUE by A4,BINARITH:10;
hence thesis by A1,BVFUNC_1:def 17;
end;
case
Ex(a,PA,G).z=TRUE;
then consider x1 being Element of Y such that
A5: x1 in EqClass(z,CompF(PA,G)) and
A6: a.x1=TRUE by BVFUNC_1:def 17;
(u 'imp' a).x1 =('not' u.x1) 'or' a.x1 by BVFUNC_1:def 8
.=TRUE by A6,BINARITH:10;
hence thesis by A5,BVFUNC_1:def 17;
end;
end;
hence thesis;
end;
theorem
for PA being a_partition of Y holds Ex(a,PA,G) 'imp' u '<' Ex(a 'imp' u,PA,G)
proof
let PA be a_partition of Y;
let z be Element of Y;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume (Ex(a,PA,G) 'imp' u).z= TRUE;
then
A2: ('not' Ex(a,PA,G).z) 'or' u.z=TRUE by BVFUNC_1:def 8;
A3: u.z= TRUE or u.z=FALSE by XBOOLEAN:def 3;
now
per cases by A2,A3,BINARITH:3;
case
('not' Ex(a,PA,G).z)=TRUE;
then
A4: a.z<>TRUE by A1,BVFUNC_1:def 17,MARGREL1:11;
(a 'imp' u).z =('not' a.z) 'or' u.z by BVFUNC_1:def 8
.= TRUE 'or' u.z by A4,MARGREL1:11,XBOOLEAN:def 3
.= TRUE by BINARITH:10;
hence thesis by A1,BVFUNC_1:def 17;
end;
case
A5: u.z=TRUE;
(a 'imp' u).z =('not' a.z) 'or' u.z by BVFUNC_1:def 8
.=TRUE by A5,BINARITH:10;
hence thesis by A1,BVFUNC_1:def 17;
end;
end;
hence thesis;
end;
theorem Th38:
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' Ex(a,PA,G) '<' Ex(u 'xor' a,PA,G)
proof
let PA be a_partition of Y;
A1: 'not' FALSE=TRUE by MARGREL1:11;
assume
A2: u is_independent_of PA,G;
let z be Element of Y;
A3: (u 'xor' Ex(a,PA,G)).z =u.z 'xor' Ex(a,PA,G).z by BVFUNC_1:def 5
.=('not' u.z '&' Ex(a,PA,G).z) 'or' (u.z '&' 'not' Ex(a,PA,G).z);
A4: (u.z '&' 'not' Ex(a,PA,G).z)=TRUE or (u.z '&' 'not' Ex(a,PA,G).z)=FALSE
by XBOOLEAN:def 3;
A5: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume
A6: (u 'xor' Ex(a,PA,G)).z= TRUE;
now
per cases by A6,A3,A4,BINARITH:3;
case
A7: 'not' u.z '&' Ex(a,PA,G).z=TRUE;
then Ex(a,PA,G).z=TRUE by MARGREL1:12;
then consider x1 being Element of Y such that
A8: x1 in EqClass(z,CompF(PA,G)) and
A9: a.x1=TRUE by BVFUNC_1:def 17;
A10: u.z=u.x1 by A2,A5,A8,BVFUNC_1:def 15;
A11: 'not' u.z=TRUE by A7,MARGREL1:12;
(u 'xor' a).x1 =u.x1 'xor' a.x1 by BVFUNC_1:def 5
.= TRUE 'or' FALSE by A11,A9,A10,MARGREL1:11
.= TRUE by BINARITH:10;
hence thesis by A8,BVFUNC_1:def 17;
end;
case
A12: u.z '&' 'not' Ex(a,PA,G).z=TRUE;
then 'not' Ex(a,PA,G).z=TRUE by MARGREL1:12;
then a.z<>TRUE by A5,BVFUNC_1:def 17,MARGREL1:11;
then
A13: a.z=FALSE by XBOOLEAN:def 3;
A14: u.z=TRUE by A12,MARGREL1:12;
(u 'xor' a).z = u.z 'xor' a.z by BVFUNC_1:def 5
.= FALSE 'or' TRUE by A1,A14,A13
.= TRUE by BINARITH:10;
hence thesis by A5,BVFUNC_1:def 17;
end;
end;
hence thesis;
end;
theorem
for PA being a_partition of Y st u is_independent_of PA,G holds Ex(a,
PA,G) 'xor' u '<' Ex(a 'xor' u,PA,G) by Th38;