:: A Theory of Boolean Valued Functions and Partitions
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 22, 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 NUMBERS, XBOOLEAN, XXREAL_0, CARD_1, XBOOLE_0, SUBSET_1,
MARGREL1, FUNCT_1, RELAT_1, TARSKI, FUNCOP_1, PARTIT1, EQREL_1, ZFMISC_1,
SETFAM_1, BVFUNC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1,
FUNCT_1, FUNCT_2, SETFAM_1, EQREL_1, ORDINAL1, NUMBERS, PARTIT1,
XXREAL_0, FUNCOP_1;
constructors SETFAM_1, XXREAL_0, XREAL_0, PARTIT1, BINARITH, FUNCOP_1,
RELSET_1, NUMBERS;
registrations SUBSET_1, XREAL_0, XBOOLEAN, EQREL_1, MARGREL1, FUNCT_2,
RELSET_1, FUNCOP_1;
requirements REAL, SUBSET, BOOLE, ARITHM, NUMERALS;
definitions TARSKI, XBOOLE_0, MARGREL1, FUNCT_2;
equalities XBOOLE_0, MARGREL1, XBOOLEAN;
theorems TARSKI, FUNCT_1, FUNCT_2, MARGREL1, EQREL_1, SETFAM_1, PARTIT1,
XBOOLE_0, FUNCOP_1, XBOOLEAN, PARTFUN1;
schemes DOMAIN_1, FUNCT_2, FUNCT_1;
begin :: Chap. 1 Boolean Operations
definition
let k,l be boolean object;
redefine pred k <= l means :: redefines <= (XXREAL_0, definition)
k => l = TRUE;
compatibility
proof
(l=0 or l=1) & (k=0 or k=1) by XBOOLEAN:def 3;
hence thesis;
end;
end;
begin :: Chap.2 Boolean Valued Functions
reserve Y for non empty set;
reserve B for Subset of Y;
scheme
BVFUniq1 {Y() -> non empty set, F(set) -> set}:
for f1,f2 being Function of Y(),BOOLEAN
st (for x being Element of Y() holds f1.x = F(x)) & (for x
being Element of Y() holds f2.x = F(x)) holds f1 = f2 proof
let f1,f2 be Function of Y(),BOOLEAN;
assume that
A1: for x being Element of Y() holds f1.x = F(x) and
A2: for x being Element of Y() holds f2.x = F(x);
let u be Element of Y();
thus f2.u = F(u) by A2 .= f1.u by A1;
end;
definition
let Y;
let a be Function of Y,BOOLEAN;
redefine func 'not' a -> Function of Y,BOOLEAN; :: redefines 'not' (MARGREL1, definition)
coherence
proof
reconsider a as Function of Y,BOOLEAN;
'not' a is Function of Y,BOOLEAN;
hence thesis;
end;
let b be Function of Y,BOOLEAN;
redefine func a '&' b -> Function of Y,BOOLEAN; :: redefines '&' (MARGREL1, definition)
coherence
proof
reconsider a,b as Function of Y,BOOLEAN;
a '&' b is Function of Y,BOOLEAN;
hence thesis;
end;
end;
definition
let p,q be boolean-valued Function;
func p 'or' q -> boolean-valued Function means
:Def2:
dom it = dom p /\ dom q &
for x being object st x in dom it holds it.x = (p.x) 'or' (q.x);
existence
proof
deffunc F(object) = (p.$1) 'or' (q.$1);
consider s being Function such that
A1: dom s = dom p /\ dom q &
for x being object st x in dom p /\ dom q
holds s.x = F(x) from FUNCT_1:sch 3;
s is boolean-valued
proof
let x be object;
assume x in rng s;
then consider y being object such that
A2: y in dom s & x = s.y by FUNCT_1:def 3;
x = (p.y) 'or' (q.y) by A1,A2;
then x = FALSE or x = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let s1,s2 be boolean-valued Function such that
A3: dom s1 = dom p /\ dom q and
A4: for x being object st x in dom s1 holds s1.x = (p.x) 'or' (q.x) and
A5: dom s2 = dom p /\ dom q and
A6: for x being object st x in dom s2 holds s2.x = (p.x) 'or' (q.x);
for x being object st x in dom s1 holds s1.x = s2.x
proof
let x be object;
assume
A7: x in dom s1;
then s1.x = (p.x) 'or' (q.x) by A4;
hence thesis by A3,A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:2;
end;
commutativity;
idempotence;
func p 'xor' q -> Function means
:Def3:
dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) 'xor' (q.x);
existence
proof
deffunc F(object) = (p.$1) 'xor' (q.$1);
consider s being Function such that
A8: dom s = dom p /\ dom q &
for x being object st x in dom p /\ dom q
holds s.x = F(x) from FUNCT_1:sch 3;
take s;
thus thesis by A8;
end;
uniqueness
proof
let s1,s2 be Function such that
A9: dom s1 = dom p /\ dom q and
A10: for x being set st x in dom s1 holds s1.x = (p.x) 'xor' (q.x) and
A11: dom s2 = dom p /\ dom q and
A12: for x being set st x in dom s2 holds s2.x = (p.x) 'xor' (q.x);
for x being object st x in dom s1 holds s1.x = s2.x
proof
let x be object;
assume
A13: x in dom s1;
then s1.x = (p.x) 'xor' (q.x) by A10;
hence thesis by A9,A11,A12,A13;
end;
hence thesis by A9,A11,FUNCT_1:2;
end;
commutativity;
end;
registration
let p,q be boolean-valued Function;
cluster p 'xor' q -> boolean-valued;
coherence
proof
let x be object;
assume x in rng(p 'xor' q);
then consider y being object such that
A1: y in dom(p 'xor' q) & x = (p 'xor' q).y by FUNCT_1:def 3;
x = (p.y) 'xor' (q.y) by A1,Def3;
then x = FALSE or x = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
end;
definition
let A be non empty set;
let p,q be Function of A,BOOLEAN;
redefine func p 'or' q -> Function of A,BOOLEAN means :: redefines 'or' (BVFUNC_1, definition)
:Def4:
for x being Element of A holds it.x = (p.x) 'or' (q.x);
coherence
proof
dom p = A & dom q = A by PARTFUN1:def 2;
then
A1: dom(p 'or' q) = A /\ A by Def2
.= A;
rng(p 'or' q) c= BOOLEAN by MARGREL1:def 16;
hence thesis by A1,FUNCT_2:2;
end;
compatibility
proof
let IT be Function of A,BOOLEAN;
A2: dom IT = A by FUNCT_2:def 1;
hereby
assume
A3: IT = p 'or' q;
let x be Element of A;
dom p = A & dom q = A by FUNCT_2:def 1;
then dom(p 'or' q) = A /\ A by Def2
.= A;
hence IT.x = (p.x) 'or' (q.x) by A3,Def2;
end;
A4: dom q = A by FUNCT_2:def 1;
A5: dom IT = A /\ A by FUNCT_2:def 1
.= dom p /\ dom q by A4,FUNCT_2:def 1;
assume for x being Element of A holds IT.x = (p.x) 'or' (q.x);
then for x being object st x in dom IT holds IT.x = (p.x) 'or' (q.x)
by A2;
hence thesis by A5,Def2;
end;
redefine func p 'xor' q -> Function of A,BOOLEAN means :: redefines 'xor' (BVFUNC_1, definition)
for x being Element of A holds it.x = (p.x) 'xor' (q.x);
coherence
proof
dom p = A & dom q = A by PARTFUN1:def 2;
then
A6: dom(p 'xor' q) = A /\ A by Def3
.= A;
rng(p 'xor' q) c= BOOLEAN by MARGREL1:def 16;
hence thesis by A6,FUNCT_2:2;
end;
compatibility
proof
let IT be Function of A,BOOLEAN;
A7: dom IT = A by FUNCT_2:def 1;
hereby
assume
A8: IT = p 'xor' q;
let x be Element of A;
dom p = A & dom q = A by FUNCT_2:def 1;
then dom(p 'xor' q) = A /\ A by Def3
.= A;
hence IT.x = (p.x) 'xor' (q.x) by A8,Def3;
end;
A9: dom q = A by FUNCT_2:def 1;
A10: dom IT = A /\ A by FUNCT_2:def 1
.= dom p /\ dom q by A9,FUNCT_2:def 1;
assume for x being Element of A holds IT.x = (p.x) 'xor' (q.x);
then
for x being set st x in dom IT holds IT.x = (p.x) 'xor' (q.x) by A7;
hence thesis by A10,Def3;
end;
end;
definition
let p,q be boolean-valued Function;
func p 'imp' q -> Function means
:Def6:
dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) => (q.x);
existence
proof
deffunc F(object) = (p.$1) => (q.$1);
consider s being Function such that
A1: dom s = dom p /\ dom q & for x being object st x in dom p /\ dom q
holds s.x = F(x) from FUNCT_1:sch 3;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s1,s2 be Function such that
A2: dom s1 = dom p /\ dom q and
A3: for x being set st x in dom s1 holds s1.x = (p.x) => (q.x) and
A4: dom s2 = dom p /\ dom q and
A5: for x being set st x in dom s2 holds s2.x = (p.x) => (q.x);
for x being object st x in dom s1 holds s1.x = s2.x
proof
let x be object;
assume
A6: x in dom s1;
then s1.x = (p.x) => (q.x) by A3;
hence thesis by A2,A4,A5,A6;
end;
hence thesis by A2,A4,FUNCT_1:2;
end;
func p 'eqv' q -> Function means
:Def7:
dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) <=> (q.x);
existence
proof
deffunc F(object) = (p.$1) <=> (q.$1);
consider s being Function such that
A7: dom s = dom p /\ dom q &
for x being object st x in dom p /\ dom q
holds s.x = F(x) from FUNCT_1:sch 3;
take s;
thus thesis by A7;
end;
uniqueness
proof
let s1,s2 be Function such that
A8: dom s1 = dom p /\ dom q and
A9: for x being set st x in dom s1 holds s1.x = (p.x) <=> (q.x) and
A10: dom s2 = dom p /\ dom q and
A11: for x being set st x in dom s2 holds s2.x = (p.x) <=> (q.x);
for x being object st x in dom s1 holds s1.x = s2.x
proof
let x be object;
assume
A12: x in dom s1;
then s1.x = (p.x) <=> (q.x) by A9;
hence thesis by A8,A10,A11,A12;
end;
hence thesis by A8,A10,FUNCT_1:2;
end;
commutativity;
end;
registration
let p,q be boolean-valued Function;
cluster p 'imp' q -> boolean-valued;
coherence
proof
let x be object;
assume x in rng(p 'imp' q);
then consider y being object such that
A1: y in dom(p 'imp' q) & x = (p 'imp' q).y by FUNCT_1:def 3;
x = (p.y) => (q.y) by A1,Def6
.= 'not' (p.y) 'or' (q.y);
then x = FALSE or x = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
cluster p 'eqv' q -> boolean-valued;
coherence
proof
let x be object;
assume x in rng(p 'eqv' q);
then consider y being object such that
A2: y in dom(p 'eqv' q) & x = (p 'eqv' q).y by FUNCT_1:def 3;
x = 'not' ((p.y) 'xor' (q.y)) by A2,Def7;
then x = FALSE or x = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
end;
definition
let A be non empty set;
let p,q be Function of A,BOOLEAN;
redefine func p 'imp' q -> Function of A,BOOLEAN means :: redefines 'imp' (BVFUNC_1, definition)
:Def8:
for x being Element of A holds it.x = 'not' p.x 'or' q.x;
coherence
proof
dom p = A & dom q = A by PARTFUN1:def 2;
then
A1: dom(p 'imp' q) = A /\ A by Def6
.= A;
rng(p 'imp' q) c= BOOLEAN by MARGREL1:def 16;
hence thesis by A1,FUNCT_2:2;
end;
compatibility
proof
let IT be Function of A,BOOLEAN;
A2: dom q = A by FUNCT_2:def 1;
hereby
assume
A3: IT = p 'imp' q;
let x be Element of A;
dom p = A & dom q = A by FUNCT_2:def 1;
then dom(p 'imp' q) = A /\ A by Def6
.= A;
hence IT.x = p.x => q.x by A3,Def6
.= 'not' p.x 'or' (q.x);
end;
assume
A4: for x being Element of A holds IT.x = 'not' p.x 'or' q.x;
A5: for x being set st x in dom IT holds IT.x = (p.x) => (q.x)
proof
let x be set;
assume x in dom IT;
then reconsider x as Element of A by FUNCT_2:def 1;
IT.x = 'not' (p.x) 'or' (q.x) by A4;
hence thesis;
end;
dom IT = A /\ A by FUNCT_2:def 1
.= dom p /\ dom q by A2,FUNCT_2:def 1;
hence thesis by A5,Def6;
end;
redefine func p 'eqv' q -> Function of A,BOOLEAN means :: redefines 'eqv' (BVFUNC_1, definition)
:Def9:
for x being Element of A holds it.x = 'not' (p.x 'xor' q.x);
coherence
proof
dom p = A & dom q = A by PARTFUN1:def 2;
then
A6: dom(p 'eqv' q) = A /\ A by Def7
.= A;
rng(p 'eqv' q) c= BOOLEAN by MARGREL1:def 16;
hence thesis by A6,FUNCT_2:2;
end;
compatibility
proof
let IT be Function of A,BOOLEAN;
A7: dom q = A by FUNCT_2:def 1;
hereby
assume
A8: IT = p 'eqv' q;
let x be Element of A;
dom p = A & dom q = A by FUNCT_2:def 1;
then dom(p 'eqv' q) = A /\ A by Def7
.= A;
hence IT.x = 'not' (p.x 'xor' q.x) by A8,Def7;
end;
assume
A9: for x being Element of A holds IT.x = 'not' (p.x 'xor' q.x);
A10: for x being set st x in dom IT holds IT.x = (p.x) <=> (q.x)
proof
let x be set;
assume x in dom IT;
then reconsider x as Element of A by FUNCT_2:def 1;
IT.x = 'not' (p.x 'xor' q.x) by A9;
hence thesis;
end;
dom IT = A /\ A by FUNCT_2:def 1
.= dom p /\ dom q by A7,FUNCT_2:def 1;
hence thesis by A10,Def7;
end;
end;
definition
let Y;
func O_el(Y) ->Function of Y,BOOLEAN means
:Def10:
for x being Element of Y holds it.x= FALSE;
existence
proof
reconsider f = Y --> FALSE as Function of Y, BOOLEAN;
reconsider f as Function of Y,BOOLEAN;
take f;
let x be Element of Y;
thus thesis;
end;
uniqueness
proof
deffunc F(set) = FALSE;
thus for f1,f2 being Function of Y,BOOLEAN st (for x being Element
of Y holds f1.x = F(x)) & (for x being Element of Y holds f2.x = F(x)) holds f1
= f2 from BVFUniq1;
end;
end;
definition
let Y;
func I_el(Y) ->Function of Y,BOOLEAN means
:Def11:
for x being Element of Y holds it.x= TRUE;
existence
proof
reconsider f = Y --> TRUE as Function of Y, BOOLEAN;
reconsider f as Function of Y,BOOLEAN;
take f;
let x be Element of Y;
thus thesis;
end;
uniqueness
proof
deffunc F(set) = TRUE;
thus for f1,f2 being Function of Y,BOOLEAN st (for x being Element
of Y holds f1.x = F(x)) & (for x being Element of Y holds f2.x = F(x)) holds f1
= f2 from BVFUniq1;
end;
end;
::$CT
theorem Th1:
'not' I_el(Y)=O_el(Y) & 'not' O_el(Y)=I_el(Y)
proof
A1: for x being Element of Y holds ('not' O_el Y).x= TRUE
proof
let x be Element of Y;
('not' O_el Y).x= 'not' (O_el Y).x & (O_el Y).x= FALSE by Def10,
MARGREL1:def 19;
hence thesis;
end;
for x being Element of Y holds ('not' I_el Y).x= FALSE
proof
let x be Element of Y;
('not' I_el Y).x= 'not' ((I_el Y).x) & (I_el Y).x= TRUE by Def11,
MARGREL1:def 19;
hence thesis;
end;
hence thesis by A1,Def10,Def11;
end;
theorem
for a,b being Function of Y,BOOLEAN holds a '&' a=a;
theorem
for a,b,c being Function of Y,BOOLEAN
holds a '&' b '&' c = a '&' (b '&' c)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a '&' b '&' c).x = (a '&' b).x '&' c.x by MARGREL1:def 20
.= a.x '&' b.x '&' c.x by MARGREL1:def 20
.= a.x '&' (b.x '&' c.x)
.= a.x '&' (b '&' c).x by MARGREL1:def 20
.= (a '&' (b '&' c)).x by MARGREL1:def 20;
end;
theorem Th4:
for a being Function of Y,BOOLEAN holds a '&' O_el(Y)=O_el( Y)
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a '&' O_el(Y)).x = a.x '&' (O_el Y).x by MARGREL1:def 20
.= a.x '&' FALSE by Def10
.= O_el(Y).x by Def10;
end;
theorem Th5:
for a being Function of Y,BOOLEAN holds a '&' I_el(Y)=a
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a '&' I_el(Y)).x = a.x '&' I_el(Y).x by MARGREL1:def 20
.= a.x '&' TRUE by Def11
.= a.x;
end;
theorem
for a being Function of Y,BOOLEAN holds a 'or' a=a;
theorem
for a,b,c being Function of Y,BOOLEAN
holds a 'or' b 'or' c = a 'or' (b 'or' c)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'or' b 'or' c).x = (a 'or' b).x 'or' c.x by Def4
.= a.x 'or' b.x 'or' c.x by Def4
.= a.x 'or' (b.x 'or' c.x)
.= a.x 'or' (b 'or' c).x by Def4
.= (a 'or' (b 'or' c)).x by Def4;
end;
theorem Th8:
for a being Function of Y,BOOLEAN holds a 'or' O_el(Y)=a
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'or' O_el(Y)).x = a.x 'or' O_el(Y).x by Def4
.= a.x 'or' FALSE by Def10
.= a.x;
end;
theorem Th9:
for a being Function of Y,BOOLEAN holds a 'or' I_el(Y)= I_el(Y)
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'or' I_el(Y)).x = a.x 'or' I_el(Y).x by Def4
.= a.x 'or' TRUE by Def11
.= I_el(Y).x by Def11;
end;
theorem ::Distributive
for a,b,c being Function of Y,BOOLEAN
holds (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
thus ((a '&' b) 'or' c).x = (a '&' b).x 'or' c.x by Def4
.= a.x '&' b.x 'or' c.x by MARGREL1:def 20
.= (a.x 'or' c.x) '&' (b.x 'or' c.x) by XBOOLEAN:9
.= (a.x 'or' c.x) '&' (b 'or' c).x by Def4
.= (a 'or' c).x '&' (b 'or' c).x by Def4
.= ((a 'or' c) '&' (b 'or' c)).x by MARGREL1:def 20;
end;
theorem ::Distributive
for a,b,c being Function of Y,BOOLEAN
holds (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c)
proof
let a,b,c be Function of Y,BOOLEAN;
let x be Element of Y;
thus ((a 'or' b) '&' c).x = (a 'or' b).x '&' c.x by MARGREL1:def 20
.= (a.x 'or' b.x) '&' c.x by Def4
.= a.x '&' c.x 'or' b.x '&' c.x by XBOOLEAN:8
.= a.x '&' c.x 'or' (b '&' c).x by MARGREL1:def 20
.= (a '&' c).x 'or' (b '&' c).x by MARGREL1:def 20
.= ((a '&' c) 'or' (b '&' c)).x by Def4;
end;
theorem ::De'Morgan
for a,b being Function of Y,BOOLEAN
holds 'not' (a 'or' b)=('not' a) '&' ('not' b)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
thus ('not' (a 'or' b)).x = 'not' ((a 'or' b).x) by MARGREL1:def 19
.= 'not' (a.x 'or' b.x) by Def4
.= ('not' a).x '&' 'not' b.x by MARGREL1:def 19
.= ('not' a).x '&' ('not' b).x by MARGREL1:def 19
.= (('not' a) '&' ('not' b)).x by MARGREL1:def 20;
end;
theorem ::De'Morgan
for a,b being Function of Y,BOOLEAN
holds 'not' (a '&' b)=('not' a) 'or' ('not' b)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
thus ('not' (a '&' b)).x = 'not' (a '&' b).x by MARGREL1:def 19
.= 'not' a.x 'or' 'not' b.x by MARGREL1:def 20
.= 'not' a.x 'or' ('not' b).x by MARGREL1:def 19
.= ('not' a).x 'or' ('not' b).x by MARGREL1:def 19
.= (('not' a) 'or' ('not' b)).x by Def4;
end;
definition
let Y;
let a,b be Function of Y,BOOLEAN;
pred a '<' b means
for x being Element of Y st a.x= TRUE holds b.x= TRUE;
reflexivity;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds ( a '<' b & b '<' a
implies a=b)& ( a '<' b & b '<' c implies a '<' c)
proof
let a,b,c be Function of Y,BOOLEAN;
A1: for a,b,c being Function of Y,BOOLEAN holds a '<' b & b '<' a
implies a = b
proof
let a,b,c be Function of Y,BOOLEAN;
assume
A2: a '<' b & b '<' a;
let x be Element of Y;
a.x = FALSE & b.x = FALSE or a.x = FALSE & b.x = TRUE or a.x = TRUE
& b.x = FALSE or a.x = TRUE & b.x = TRUE by XBOOLEAN:def 3;
hence thesis by A2;
end;
for a,b,c being Function of Y,BOOLEAN holds a '<' b & b '<' c
implies a '<' c
proof
let a,b,c be Function of Y,BOOLEAN;
assume that
A3: a '<' b and
A4: b '<' c;
for x being Element of Y st a.x= TRUE holds c.x=TRUE
proof
let x be Element of Y;
b.x = TRUE implies c.x = TRUE by A4;
hence thesis by A3;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th15:
for a,b being Function of Y,BOOLEAN holds (a 'imp' b)=I_el
(Y) iff a '<' b
proof
let a,b be Function of Y,BOOLEAN;
A1: for a,b being Function of Y,BOOLEAN holds a '<' b implies (a 'imp'
b)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume
A2: a '<' b;
A3: for x being Element of Y holds ('not' a.x) 'or' b.x = TRUE
proof
let x be Element of Y;
a.x = FALSE & b.x = FALSE or a.x = FALSE & b.x = TRUE or a.x = TRUE
& b.x = TRUE by A2,XBOOLEAN:def 3;
hence thesis;
end;
let x be Element of Y;
(a 'imp' b).x = ('not' a.x) 'or' b.x & (I_el Y).x= TRUE by Def8,Def11;
hence thesis by A3;
end;
for a,b being Function of Y,BOOLEAN holds (a 'imp' b)=I_el(Y)
implies a '<' b
proof
let a,b be Function of Y,BOOLEAN;
assume
A4: (a 'imp' b)=I_el(Y);
A5: for x being Element of Y holds ('not' a.x) 'or' b.x = TRUE
proof
let x be Element of Y;
(a 'imp' b).x=('not' a.x) 'or' b.x by Def8;
hence thesis by A4,Def11;
end;
for x being Element of Y holds a.x = FALSE & b.x = FALSE or a.x =
FALSE & b.x = TRUE or a.x = TRUE & b.x = TRUE
proof
let x be Element of Y;
A6: ('not' a.x) = TRUE & b.x = FALSE or ('not' a.x) = TRUE & b.x = TRUE
or ('not' a.x) = FALSE & b.x = FALSE or ('not' a.x) = FALSE & b.x = TRUE by
XBOOLEAN:def 3;
('not' a.x) 'or' b.x = TRUE by A5;
hence thesis by A6;
end;
then for x being Element of Y st a.x= TRUE holds b.x=TRUE;
hence thesis;
end;
hence thesis by A1;
end;
theorem
for a,b being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y) iff a = b
proof
let a,b be Function of Y,BOOLEAN;
A1: for a,b being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y)
implies a = b
proof
let a,b be Function of Y,BOOLEAN;
assume
A2: (a 'eqv' b)=I_el(Y);
A3: for x being Element of Y holds ('not' a.x '&' b.x) 'or' (a.x '&' 'not'
b.x) = FALSE
proof
let x be Element of Y;
(a 'eqv' b).x = 'not' (a.x 'xor' b.x) by Def9;
then 'not' (a.x 'xor' b.x) = TRUE by A2,Def11;
hence thesis;
end;
A4: for x being Element of Y holds ('not' a.x '&' b.x) = FALSE & (a.x '&'
'not' b.x) = FALSE
proof
let x be Element of Y;
A5: (a.x '&' 'not' b.x) = TRUE or (a.x '&' 'not' b.x) = FALSE by
XBOOLEAN:def 3;
('not' a.x '&' b.x) 'or' (a.x '&' 'not' b.x) = FALSE by A3;
hence thesis by A5;
end;
let x be Element of Y;
('not' a.x '&' b.x) = FALSE by A4;
then
A6: 'not' a.x = TRUE & b.x = FALSE or 'not' a.x = FALSE & b.x = FALSE
or 'not' a.x = FALSE & b.x = TRUE by MARGREL1:12,XBOOLEAN:def 3;
(a.x '&' 'not' b.x) = FALSE by A4;
hence thesis by A6;
end;
for a,b being Function of Y,BOOLEAN holds a = b implies (a 'eqv'
b)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume
A7: a = b;
A8: for x being Element of Y holds ('not' a.x '&' b.x) = FALSE & (a.x '&'
'not' b.x) = FALSE
proof
let x be Element of Y;
b.x = TRUE iff 'not' b.x = FALSE;
then
a.x = FALSE & 'not' b.x = TRUE or a.x = TRUE & 'not' b.x = FALSE by A7,
XBOOLEAN:def 3;
hence thesis;
end;
let x be Element of Y;
(a.x '&' 'not' b.x) = FALSE by A8;
then 'not' (a.x 'xor' b.x) = TRUE by A8;
then (a 'eqv' b).x= TRUE by Def9;
hence thesis by Def11;
end;
hence thesis by A1;
end;
theorem
for a being Function of Y,BOOLEAN holds O_el(Y) '<' a & a '<' I_el(Y)
proof
let a be Function of Y,BOOLEAN;
A1: (O_el Y) 'imp' a = I_el Y
proof
let x be Element of Y;
((O_el Y) 'imp' a).x=('not' (O_el Y).x) 'or' a.x by Def8;
then ((O_el Y) 'imp' a).x=TRUE 'or' a.x by Def10;
hence thesis by Def11;
end;
a 'imp' I_el(Y)=I_el(Y)
proof
let x be Element of Y;
(a 'imp' I_el Y).x='not' a.x 'or' (I_el Y).x by Def8;
then (a 'imp' I_el Y).x='not' a.x 'or' TRUE by Def11;
hence thesis by Def11;
end;
hence thesis by A1,Th15;
end;
begin :: Chap. 3 Infimum and Supremum
definition
let Y;
let a be Function of Y,BOOLEAN;
func B_INF(a) ->Function of Y,BOOLEAN equals
:Def13:
I_el(Y) if for x being Element of Y holds a.x=TRUE
otherwise O_el(Y);
correctness;
func B_SUP(a) ->Function of Y,BOOLEAN equals
:Def14:
O_el(Y) if for x being Element of Y holds a.x=FALSE
otherwise I_el(Y);
correctness;
end;
theorem Th18:
for a being Function of Y,BOOLEAN holds 'not' B_INF(a) =
B_SUP('not' a) & 'not' B_SUP(a)=B_INF('not' a)
proof
let a be Function of Y,BOOLEAN;
A1: (for x being Element of Y holds ('not' a).x=TRUE) implies for x being
Element of Y holds a.x=FALSE
proof
assume
A2: for x being Element of Y holds ('not' a).x=TRUE;
let x be Element of Y;
('not' a).x=TRUE by A2;
then 'not' a.x=TRUE by MARGREL1:def 19;
hence thesis;
end;
A3: (for x being Element of Y holds ('not' a).x=FALSE) implies for x being
Element of Y holds a.x= TRUE
proof
assume
A4: for x being Element of Y holds ('not' a).x=FALSE;
let x be Element of Y;
('not' a).x=FALSE by A4;
then 'not' a.x=FALSE by MARGREL1:def 19;
hence thesis;
end;
A5: now
assume
A6: (for x being Element of Y holds a.x=TRUE ) or for x being Element
of Y holds a.x=FALSE;
now
per cases by A6;
case
A7: (for x being Element of Y holds a.x=TRUE) & not (for x being
Element of Y holds a.x=FALSE);
A8: for x being Element of Y holds ('not' a).x= FALSE
proof
let x be Element of Y;
'not' (TRUE) = FALSE;
then 'not' a.x= FALSE by A7;
hence thesis by MARGREL1:def 19;
end;
B_INF(a) = I_el(Y) by A7,Def13;
then
A9: 'not' B_INF(a) = O_el(Y) by Th1;
B_INF('not' a) = O_el(Y) & 'not' B_SUP(a) = 'not' I_el(Y) by A1,A7
,Def13,Def14;
hence thesis by A9,A8,Def14,Th1;
end;
case
A10: (for x being Element of Y holds a.x=FALSE) & not (for x being
Element of Y holds a.x=TRUE);
A11: for x being Element of Y holds ('not' a).x= TRUE
proof
let x be Element of Y;
'not' (FALSE) = TRUE;
then 'not' a.x= TRUE by A10;
hence thesis by MARGREL1:def 19;
end;
'not' B_SUP(a) = 'not' O_el(Y) by A10,Def14;
then
A12: 'not' B_SUP(a) = I_el(Y) by Th1;
B_SUP('not' a) = I_el(Y) & 'not' B_INF(a) = 'not' O_el(Y) by A3,A10
,Def13,Def14;
hence thesis by A12,A11,Def13,Th1;
end;
case
A13: (for x being Element of Y holds a.x=TRUE ) & for x being
Element of Y holds a.x=FALSE;
let x be Element of Y;
a.x=TRUE by A13;
hence thesis by A13;
end;
end;
hence thesis;
end;
now
assume that
A14: not( for x being Element of Y holds a.x=TRUE ) and
A15: not(for x being Element of Y holds a.x=FALSE);
'not' B_INF(a) = 'not' O_el(Y) by A14,Def13;
then
A16: 'not' B_INF(a) = I_el(Y) by Th1;
'not' B_SUP(a) = 'not' I_el(Y) & B_INF('not' a) = O_el(Y) by A1,A15,Def13
,Def14;
hence thesis by A3,A14,A16,Def14,Th1;
end;
hence thesis by A5;
end;
theorem
B_INF(O_el(Y)) = O_el(Y) & B_INF(I_el(Y))=I_el(Y) & B_SUP(O_el(Y)) =
O_el(Y) & B_SUP(I_el(Y))=I_el(Y)
proof
A1: not (for x being Element of Y holds (O_el Y).x= TRUE)
proof
now
assume for x being Element of Y holds (O_el Y).x= TRUE;
let x be Element of Y;
(O_el Y).x= FALSE by Def10;
hence thesis;
end;
hence thesis;
end;
A2: not (for x being Element of Y holds (I_el Y).x= FALSE)
proof
now
assume
A3: for x being Element of Y holds (I_el Y).x= FALSE;
let x be Element of Y;
(I_el Y).x= FALSE by A3;
hence thesis by Def11;
end;
hence thesis;
end;
( for x being Element of Y holds (O_el Y).x= FALSE)& for x being Element
of Y holds (I_el Y).x= TRUE by Def10,Def11;
hence thesis by A1,A2,Def13,Def14;
end;
registration
let Y;
cluster O_el(Y) -> constant;
coherence
proof
for n1,n2 being object st n1 in dom O_el(Y) & n2 in dom O_el(Y) holds
O_el(Y).n1=O_el(Y).n2
proof
let n1,n2 be object;
assume n1 in dom O_el(Y) & n2 in dom O_el(Y);
then reconsider n1, n2 as Element of Y by PARTFUN1:def 2;
(O_el Y).n2= FALSE & (O_el Y).n1 = O_el(Y).n1 by Def10;
hence thesis by Def10;
end;
hence thesis by FUNCT_1:def 10;
end;
end;
registration
let Y;
cluster I_el(Y) -> constant;
coherence
proof
thus I_el(Y) is constant
proof
for n1,n2 being object st n1 in dom I_el(Y) & n2 in dom I_el(Y) holds
I_el(Y).n1=I_el(Y).n2
proof
let n1,n2 be object;
assume n1 in dom I_el(Y) & n2 in dom I_el(Y);
then reconsider n1, n2 as Element of Y by PARTFUN1:def 2;
(I_el Y).n2= TRUE & (I_el Y).n1 = I_el(Y).n1 by Def11;
hence thesis by Def11;
end;
hence thesis by FUNCT_1:def 10;
end;
end;
end;
theorem Th20:
for a being constant Function of Y,BOOLEAN holds a=O_el(Y) or a=I_el(Y)
proof
let a be constant Function of Y,BOOLEAN;
A1: (for n1,n2 being set st n1 in Y & n2 in Y holds a.n1=a.n2) implies (for
x being Element of Y holds a.x=TRUE ) or for x being Element of Y holds a.x=
FALSE
proof
assume
A2: for n1,n2 being set st n1 in Y & n2 in Y holds a.n1=a.n2;
now
assume that
A3: not( for x being Element of Y holds a.x=TRUE ) and
A4: not(for x being Element of Y holds a.x=FALSE);
consider x1 being Element of Y such that
A5: a.x1<>TRUE by A3;
a.x1 = FALSE by A5,XBOOLEAN:def 3;
hence contradiction by A2,A4;
end;
hence thesis;
end;
dom a = Y by PARTFUN1:def 2;
hence thesis by A1,Def10,Def11,FUNCT_1:def 10;
end;
theorem Th21:
for d being constant Function of Y,BOOLEAN holds B_INF(d)
= d & B_SUP(d) = d
proof
let d be constant Function of Y,BOOLEAN;
A1: now
assume
A2: (for x being Element of Y holds d.x=TRUE ) or for x being Element
of Y holds d.x=FALSE;
now
per cases by A2;
case
A3: (for x being Element of Y holds d.x=TRUE) & not (for x being
Element of Y holds d.x=FALSE);
then d = I_el(Y) by Def11;
hence thesis by A3,Def13,Def14;
end;
case
A4: (for x being Element of Y holds d.x=FALSE) & not (for x being
Element of Y holds d.x=TRUE);
then d = O_el(Y) by Def10;
hence thesis by A4,Def13,Def14;
end;
case
A5: (for x being Element of Y holds d.x=TRUE) & for x being
Element of Y holds d.x=FALSE;
let x be Element of Y;
d.x=TRUE by A5;
hence thesis by A5;
end;
end;
hence thesis;
end;
now
assume that
A6: not( for x being Element of Y holds d.x=TRUE ) and
A7: not(for x being Element of Y holds d.x=FALSE);
now
per cases by Th20;
case
d=O_el(Y);
hence thesis by A7,Def10;
end;
case
d=I_el(Y);
hence thesis by A6,Def11;
end;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem
for a,b being Function of Y,BOOLEAN holds B_INF(a '&' b) = B_INF
(a) '&' B_INF(b) & B_SUP(a 'or' b) = B_SUP(a) 'or' B_SUP(b)
proof
let a,b be Function of Y,BOOLEAN;
A1: now
assume
A2: for x being Element of Y holds (a '&' b).x=TRUE;
A3: for x being Element of Y holds a.x = TRUE
proof
let x be Element of Y;
(a '&' b).x=a.x '&' b.x by MARGREL1:def 20;
then a.x '&' b.x = TRUE by A2;
hence thesis by XBOOLEAN:101;
end;
not (for x being Element of Y holds a.x=FALSE)
proof
now
assume for x being Element of Y holds a.x=FALSE;
let x be Element of Y;
a.x=TRUE by A3;
hence thesis;
end;
hence thesis;
end;
then
A4: B_SUP(a) = I_el(Y) by Def14;
A5: for x being Element of Y holds b.x = TRUE
proof
let x be Element of Y;
(a '&' b).x=TRUE by A2;
then a.x '&' b.x = TRUE by MARGREL1:def 20;
hence thesis by XBOOLEAN:101;
end;
not (for x being Element of Y holds b.x=FALSE)
proof
now
assume for x being Element of Y holds b.x=FALSE;
let x be Element of Y;
b.x=TRUE by A5;
hence thesis;
end;
hence thesis;
end;
then
A6: B_SUP(a) 'or' B_SUP(b) = I_el(Y) 'or' I_el(Y) by A4,Def14;
A7: not (for x being Element of Y holds (a 'or' b).x=FALSE)
proof
now
assume for x being Element of Y holds (a 'or' b).x=FALSE;
let x be Element of Y;
(a 'or' b).x = a.x 'or' b.x & a.x = TRUE by A3,Def4;
hence thesis;
end;
hence thesis;
end;
B_INF(a) '&' B_INF(b) = B_INF(a) '&' I_el(Y) by A5,Def13
.= I_el Y '&' I_el Y by A3,Def13;
hence thesis by A2,A7,A6,Def13,Def14;
end;
A8: now
assume
A9: for x being Element of Y holds (a 'or' b).x=FALSE;
A10: for x being Element of Y holds a.x = FALSE
proof
let x be Element of Y;
(a 'or' b).x=FALSE by A9;
then
A11: a.x 'or' b.x = FALSE by Def4;
a.x = TRUE or a.x = FALSE by XBOOLEAN:def 3;
hence thesis by A11;
end;
A12: not (for x being Element of Y holds (a '&' b).x=TRUE)
proof
now
assume for x being Element of Y holds (a '&' b).x=TRUE;
let x be Element of Y;
(a '&' b).x = a.x '&' b.x & a.x = FALSE by A10,MARGREL1:def 20;
hence thesis;
end;
hence thesis;
end;
A13: for x being Element of Y holds b.x = FALSE
proof
let x be Element of Y;
(a 'or' b).x=FALSE by A9;
then
A14: a.x 'or' b.x = FALSE by Def4;
b.x = TRUE or b.x = FALSE by XBOOLEAN:def 3;
hence thesis by A14;
end;
then B_SUP(b) = O_el(Y) by Def14;
then
A15: B_SUP(a) 'or' B_SUP(b) = O_el(Y) 'or' O_el(Y) by A10,Def14;
not (for x being Element of Y holds a.x=TRUE)
proof
now
assume for x being Element of Y holds a.x=TRUE;
let x be Element of Y;
a.x=FALSE by A10;
hence thesis;
end;
hence thesis;
end;
then
A16: B_INF(a) = O_el(Y) by Def13;
not (for x being Element of Y holds b.x=TRUE)
proof
now
assume for x being Element of Y holds b.x=TRUE;
let x be Element of Y;
b.x=FALSE by A13;
hence thesis;
end;
hence thesis;
end;
then B_INF(a) '&' B_INF(b) = O_el(Y) '&' O_el(Y) by A16,Def13;
hence thesis by A9,A15,A12,Def13,Def14;
end;
now
assume that
A17: not( for x being Element of Y holds (a '&' b).x=TRUE ) and
A18: not(for x being Element of Y holds (a 'or' b).x=FALSE);
(for x being Element of Y holds a.x = FALSE) & (for x being Element
of Y holds b.x = FALSE) implies for x being Element of Y holds (a 'or' b).x=
FALSE
proof
assume that
A19: for x being Element of Y holds a.x = FALSE and
A20: for x being Element of Y holds b.x = FALSE;
let x be Element of Y;
a.x = FALSE by A19;
then a.x 'or' b.x = FALSE by A20;
hence thesis by Def4;
end;
then B_SUP(a) = I_el(Y) or B_SUP(b) = I_el(Y) by A18,Def14;
then
A21: B_SUP(a) 'or' B_SUP(b) = I_el(Y) by Th9;
(for x being Element of Y holds a.x = TRUE) & (for x being Element of
Y holds b.x = TRUE) implies for x being Element of Y holds (a '&' b).x=TRUE
proof
assume that
A22: for x being Element of Y holds a.x = TRUE and
A23: for x being Element of Y holds b.x = TRUE;
let x be Element of Y;
a.x = TRUE by A22;
then a.x '&' b.x = TRUE by A23;
hence thesis by MARGREL1:def 20;
end;
then B_INF(a) = O_el(Y) or B_INF(b) = O_el(Y) by A17,Def13;
then B_INF(a) '&' B_INF(b) = O_el(Y) by Th4;
hence thesis by A17,A18,A21,Def13,Def14;
end;
hence thesis by A1,A8;
end;
theorem
for a being Function of Y,BOOLEAN, d being constant Function of Y,BOOLEAN
holds B_INF(d 'imp' a) = d 'imp' B_INF(a) & B_INF(a 'imp' d) =
B_SUP(a) 'imp' d
proof
let a be Function of Y,BOOLEAN;
let d be constant Function of Y,BOOLEAN;
A1: (I_el Y) 'imp' I_el Y = I_el Y
proof
let x be Element of Y;
(I_el Y).x = TRUE by Def11;
then ((I_el Y) 'imp' I_el Y).x = ('not' TRUE) 'or' TRUE by Def8;
hence thesis by Def11;
end;
A2: B_SUP(a) 'imp' d = B_SUP(a) 'imp' B_INF(d) by Th21;
A3: B_INF(d) = d by Th21;
A4: O_el(Y) 'imp' I_el(Y)=I_el(Y)
proof
let x be Element of Y;
((O_el Y) 'imp' I_el Y).x = ('not' (O_el Y).x) 'or' (I_el Y).x & (
I_el Y).x = TRUE by Def8,Def11;
hence thesis;
end;
A5: I_el(Y) 'imp' O_el(Y)=O_el(Y)
proof
let x be Element of Y;
(O_el Y).x = FALSE by Def10;
then
A6: ('not' (I_el Y).x) 'or' (O_el Y).x = ('not' TRUE) 'or' FALSE by Def11;
((I_el Y) 'imp' O_el Y).x = ('not' (I_el Y).x) 'or' (O_el Y).x by Def8;
hence thesis by A6,Def10;
end;
A7: O_el(Y) 'imp' O_el(Y)=I_el(Y)
proof
let x be Element of Y;
(O_el Y).x = FALSE by Def10;
then ((O_el Y) 'imp' O_el Y).x = TRUE 'or' FALSE by Def8;
hence thesis by Def11;
end;
A8: d 'imp' B_INF(a) = B_INF(d) 'imp' B_INF(a) by Th21;
A9: B_SUP(a) 'imp' d = B_SUP(a) 'imp' B_SUP(d) by Th21;
A10: now
assume
A11: (for x being Element of Y holds d.x=TRUE ) or for x being Element
of Y holds d.x=FALSE;
now
per cases by A11;
case
A12: (for x being Element of Y holds d.x=TRUE) & not (for x being
Element of Y holds d.x=FALSE);
A13: now
assume
A14: (for x being Element of Y holds a.x=TRUE ) or for x being
Element of Y holds a.x=FALSE;
now
per cases by A14;
case
A15: (for x being Element of Y holds a.x=TRUE) & not (for x
being Element of Y holds a.x=FALSE);
A16: for x being Element of Y holds (a 'imp' d).x = TRUE
proof
let x be Element of Y;
d.x = TRUE & a.x = TRUE by A12,A15;
then (a 'imp' d).x = ('not' TRUE) 'or' TRUE by Def8;
hence thesis;
end;
A17: for x being Element of Y holds (d 'imp' a).x = TRUE
proof
let x be Element of Y;
d.x = TRUE & a.x = TRUE by A12,A15;
then (d 'imp' a).x = ('not' TRUE) 'or' TRUE by Def8;
hence thesis;
end;
B_INF(a) = I_el(Y) by A15,Def13;
then
A18: d 'imp' B_INF(a) = I_el(Y) by A8,A1,A12,Def13;
A19: B_SUP(a) = I_el(Y) by A15,Def14;
B_SUP(d) = I_el(Y) by A12,Def14;
hence thesis by A9,A1,A17,A16,A19,A18,Def13;
end;
case
A20: (for x being Element of Y holds a.x=FALSE) & not (for x
being Element of Y holds a.x=TRUE);
A21: for x being Element of Y holds (d 'imp' a).x = FALSE
proof
let x be Element of Y;
(d 'imp' a).x = ('not' d.x) 'or' a.x & d.x = TRUE by A12,Def8;
hence thesis by A20;
end;
A22: now
assume
A23: for x being Element of Y holds (d 'imp' a).x = TRUE;
let x be Element of Y;
(d 'imp' a).x = TRUE by A23;
hence contradiction by A21;
end;
A24: for x being Element of Y holds (a 'imp' d).x = TRUE
proof
let x be Element of Y;
d.x = TRUE & a.x = FALSE by A12,A20;
then (a 'imp' d).x = ('not' FALSE) 'or' TRUE by Def8;
hence thesis;
end;
A25: B_SUP(a) = O_el(Y) by A20,Def14;
B_SUP(d) = I_el(Y) by A12,Def14;
then
A26: B_SUP(a) 'imp' d = I_el(Y) by A4,A25,Th21;
A27: B_INF(a) = O_el(Y) by A20,Def13;
B_INF(d) = I_el(Y) by A12,Def13;
hence thesis by A8,A5,A22,A24,A27,A26,Def13;
end;
case
A28: (for x being Element of Y holds a.x=FALSE) & for x
being Element of Y holds a.x=TRUE;
A29: for x being Element of Y holds (d 'imp' a).x = TRUE
proof
let x be Element of Y;
(d 'imp' a).x = ('not' d.x) 'or' a.x & a.x = TRUE by A28,Def8;
hence thesis;
end;
A30: B_INF(d) = I_el(Y) by A12,Def13;
A31: for x being Element of Y holds (a 'imp' d).x = TRUE
proof
let x be Element of Y;
(a 'imp' d).x = ('not' a.x) 'or' d.x & d.x = TRUE by A12,Def8;
hence thesis;
end;
B_INF(a) = I_el(Y) & B_SUP(a) = O_el(Y) by A28,Def13,Def14;
hence thesis by A8,A2,A1,A4,A29,A31,A30,Def13;
end;
end;
hence thesis;
end;
now
A32: for x being Element of Y holds (a 'imp' d).x = TRUE
proof
let x be Element of Y;
('not' a.x) 'or' d.x = ('not' a).x 'or' d.x by MARGREL1:def 19;
then ('not' a.x) 'or' d.x = ('not' a 'or' d).x by Def4;
then
A33: ('not' a.x) 'or' d.x = ('not' a 'or' I_el Y).x by A3,A12,Def13;
(a 'imp' d).x = ('not' a.x) 'or' d.x by Def8;
hence thesis by Th9,Def11,A33;
end;
A34: B_INF(d) = I_el(Y) by A12,Def13;
assume that
A35: not( for x being Element of Y holds a.x=TRUE ) and
A36: not(for x being Element of Y holds a.x=FALSE);
A37: B_INF(a) = O_el(Y) by A35,Def13;
B_SUP(a) = I_el(Y) by A36,Def14;
then
A38: B_SUP(a) 'imp' d = I_el(Y) by A1,A34,Th21;
d 'imp' a = a
proof
let x be Element of Y;
('not' d.x) 'or' a.x = ('not' d).x 'or' a.x by MARGREL1:def 19;
then ('not' d.x) 'or' a.x = ('not' d 'or' a).x by Def4;
then ('not' d.x) 'or' a.x = ('not' (I_el Y) 'or' a).x by A3,A12
,Def13;
then
A39: ('not' d.x) 'or' a.x = ((O_el Y) 'or' a).x by Th1;
(d 'imp' a).x = ('not' d.x) 'or' a.x by Def8;
hence thesis by A39,Th8;
end;
hence thesis by A8,A5,A12,Def13,A37,A32,A38;
end;
hence thesis by A13;
end;
case
A40: (for x being Element of Y holds d.x=FALSE) & not (for x
being Element of Y holds d.x=TRUE);
A41: now
assume
A42: (for x being Element of Y holds a.x=TRUE ) or for x being
Element of Y holds a.x=FALSE;
now
per cases by A42;
case
A43: (for x being Element of Y holds a.x=TRUE) & not (for x
being Element of Y holds a.x=FALSE);
A44: for x being Element of Y holds (a 'imp' d).x = FALSE
proof
let x be Element of Y;
d.x = FALSE & a.x = TRUE by A40,A43;
then (a 'imp' d).x = ('not' TRUE) 'or' FALSE by Def8;
hence thesis;
end;
A45: now
assume
A46: for x being Element of Y holds (a 'imp' d).x = TRUE;
let x be Element of Y;
(a 'imp' d).x = TRUE by A46;
hence contradiction by A44;
end;
A47: for x being Element of Y holds (d 'imp' a).x = TRUE
proof
let x be Element of Y;
d.x = FALSE & a.x = TRUE by A40,A43;
then (d 'imp' a).x = ('not' FALSE) 'or' TRUE by Def8;
hence thesis;
end;
A48: B_SUP(a) = I_el(Y) by A43,Def14;
B_SUP(d) = O_el(Y) by A40,Def14;
then
A49: B_SUP(a) 'imp' d = O_el(Y) by A5,A48,Th21;
A50: B_INF(a) = I_el(Y) by A43,Def13;
B_INF(d) = O_el(Y) by A40,Def13;
hence thesis by A8,A4,A47,A45,A50,A49,Def13;
end;
case
A51: (for x being Element of Y holds a.x=FALSE) & not (for
x being Element of Y holds a.x=TRUE);
A52: for x being Element of Y holds (d 'imp' a).x = TRUE
proof
let x be Element of Y;
d.x = FALSE & a.x = FALSE by A40,A51;
then (d 'imp' a).x = ('not' FALSE) 'or' FALSE by Def8;
hence thesis;
end;
A53: B_INF(d) = O_el(Y) by A40,Def13;
A54: for x being Element of Y holds (a 'imp' d).x = TRUE
proof
let x be Element of Y;
(a 'imp' d).x = ('not' a.x) 'or' d.x & a.x = FALSE by A51,Def8;
hence thesis;
end;
B_INF(a) = O_el(Y) & B_SUP(a) = O_el(Y) by A51,Def13,Def14;
hence thesis by A8,A2,A7,A52,A54,A53,Def13;
end;
case
A55: (for x being Element of Y holds a.x=FALSE) & for x
being Element of Y holds a.x=TRUE;
A56: for x being Element of Y holds (a 'imp' d).x = TRUE
proof
let x be Element of Y;
(a 'imp' d).x = ('not' a.x) 'or' d.x & a.x = FALSE by A55,Def8;
hence thesis;
end;
A57: for x being Element of Y holds (d 'imp' a).x = TRUE
proof
let x be Element of Y;
(d 'imp' a).x = ('not' d.x) 'or' a.x & a.x = TRUE by A55,Def8;
hence thesis;
end;
A58: B_INF(d) = O_el(Y) by A40,Def13;
B_SUP(a) = O_el(Y) by A55,Def14;
then
A59: B_SUP(a) 'imp' d = I_el(Y) by A7,A58,Th21;
B_INF(a) = I_el(Y) by A55,Def13;
hence thesis by A8,A4,A57,A56,A58,A59,Def13;
end;
end;
hence thesis;
end;
now
A60: B_INF(d) = O_el(Y) by A40,Def13;
A61: for x being Element of Y holds (d 'imp' a).x = TRUE
proof
let x be Element of Y;
('not' d.x) 'or' a.x = ('not' d).x 'or' a.x by MARGREL1:def 19;
then ('not' d.x) 'or' a.x = ('not' (O_el Y) 'or' a).x by A3,A60
,Def4;
then ('not' d.x) 'or' a.x = ((I_el Y) 'or' a).x by Th1;
then ('not' d.x) 'or' a.x = TRUE by Def11,Th9;
hence thesis by Def8;
end;
(a 'imp' d)='not' a
proof
let x be Element of Y;
('not' a.x) 'or' d.x = ('not' a).x 'or' d.x by MARGREL1:def 19;
then ('not' a.x) 'or' d.x = ('not' a 'or' d).x by Def4;
then ('not' a.x) 'or' d.x = ('not' a).x by A3,A60,Th8;
hence thesis by Def8;
end;
then
A62: B_INF(a 'imp' d) = 'not' B_SUP(a) by Th18;
assume ( not( for x being Element of Y holds a.x=TRUE ))& not(for
x being Element of Y holds a.x=FALSE);
then
A63: B_INF(a) = O_el(Y) & B_SUP(a) = I_el(Y) by Def13,Def14;
B_INF(d) = O_el(Y) by A40,Def13;
hence thesis by A8,A2,A5,A7,A61,A62,A63,Def13,Th1;
end;
hence thesis by A41;
end;
case
A64: (for x being Element of Y holds d.x=TRUE) & for x being
Element of Y holds d.x=FALSE;
let x be Element of Y;
d.x=FALSE by A64;
hence thesis by A64;
end;
end;
hence thesis;
end;
now
assume that
A65: not( for x being Element of Y holds d.x=TRUE ) and
A66: not(for x being Element of Y holds d.x=FALSE);
now
per cases by Th20;
case
d=O_el(Y);
hence thesis by A66,Def10;
end;
case
d=I_el(Y);
hence thesis by A65,Def11;
end;
end;
hence thesis;
end;
hence thesis by A10;
end;
theorem
for a being Function of Y,BOOLEAN, d being constant Function of Y,BOOLEAN
holds B_INF(d 'or' a) = d 'or' B_INF(a) & B_SUP(d '&' a) = d
'&' B_SUP(a) & B_SUP(a '&' d) = B_SUP(a) '&' d
proof
let a be Function of Y,BOOLEAN;
let d be constant Function of Y,BOOLEAN;
A1: d 'or' B_INF(a) = B_INF(d) 'or' B_INF(a) by Th21;
A2: d '&' B_SUP(a) = B_SUP(d) '&' B_SUP(a) by Th21;
A3: B_INF(d) = d by Th21;
A4: now
assume
A5: (for x being Element of Y holds d.x=TRUE ) or for x being Element
of Y holds d.x=FALSE;
now
per cases by A5;
case
A6: (for x being Element of Y holds d.x=TRUE) & not (for x being
Element of Y holds d.x=FALSE);
A7: now
assume
A8: (for x being Element of Y holds a.x=TRUE ) or for x being
Element of Y holds a.x=FALSE;
now
per cases by A8;
case
A9: (for x being Element of Y holds a.x=TRUE) & not (for x
being Element of Y holds a.x=FALSE);
A10: for x being Element of Y holds (d '&' a).x = TRUE
proof
let x be Element of Y;
d.x = TRUE & a.x = TRUE by A6,A9;
then (d '&' a).x = TRUE '&' TRUE by MARGREL1:def 20;
hence thesis;
end;
A11: now
assume
A12: for x being Element of Y holds (d '&' a).x = FALSE;
let x be Element of Y;
(d '&' a).x = TRUE by A10;
hence contradiction by A12;
end;
A13: for x being Element of Y holds (d 'or' a).x = TRUE
proof
let x be Element of Y;
(d 'or' a).x = d.x 'or' a.x & a.x = TRUE by A9,Def4;
hence thesis;
end;
A14: B_INF(a) = I_el(Y) & B_SUP(a) = I_el(Y) by A9,Def13,Def14;
B_INF(d) = I_el(Y) & B_SUP(d) = I_el(Y) by A6,Def13,Def14;
hence thesis by A1,A2,A13,A11,A14,Def13,Def14;
end;
case
A15: (for x being Element of Y holds a.x=FALSE) & not (for x
being Element of Y holds a.x=TRUE);
A16: for x being Element of Y holds (d '&' a).x = FALSE
proof
let x be Element of Y;
(d '&' a).x = d.x '&' a.x & a.x = FALSE by A15,MARGREL1:def 20;
hence thesis;
end;
A17: for x being Element of Y holds (d 'or' a).x = TRUE
proof
let x be Element of Y;
(d 'or' a).x = d.x 'or' a.x & d.x = TRUE by A6,Def4;
hence thesis;
end;
B_SUP(a) = O_el(Y) by A15,Def14;
then
A18: d '&' B_SUP(a) = O_el(Y) by Th4;
A19: B_INF(a) = O_el(Y) by A15,Def13;
B_INF(d) = I_el(Y) by A6,Def13;
then d 'or' B_INF(a) = I_el(Y) by A1,A19,Th8;
hence thesis by A17,A16,A18,Def13,Def14;
end;
case
A20: (for x being Element of Y holds a.x=FALSE) & for x
being Element of Y holds a.x=TRUE;
A21: for x being Element of Y holds (d '&' a).x = FALSE
proof
let x be Element of Y;
d.x = TRUE & a.x = FALSE by A6,A20;
then (d '&' a).x = TRUE '&' FALSE by MARGREL1:def 20;
hence thesis;
end;
A22: for x being Element of Y holds (d 'or' a).x = TRUE
proof
let x be Element of Y;
d.x = TRUE & a.x = FALSE by A6,A20;
then (d 'or' a).x = TRUE 'or' FALSE by Def4;
hence thesis;
end;
B_SUP(a) = O_el(Y) by A20,Def14;
then
A23: d '&' B_SUP(a) = O_el(Y) by Th4;
B_INF(d) = I_el(Y) by A6,Def13;
then d 'or' B_INF(a) = I_el(Y) by A1,Th9;
hence thesis by A22,A21,A23,Def13,Def14;
end;
end;
hence thesis;
end;
now
assume that
A24: not( for x being Element of Y holds a.x=TRUE ) and
not(for x being Element of Y holds a.x=FALSE);
A25: B_INF(a) = O_el(Y) by A24,Def13;
B_INF(d) = I_el(Y) by A6,Def13;
then
A26: d 'or' B_INF(a) = I_el(Y) by A1,A25,Th8;
A27: d = I_el(Y) by A3,A6,Def13;
A28: for x being Element of Y holds (d 'or' a).x = TRUE by A27,Th9,Def11;
A29: d '&' a = a
proof
let x be Element of Y;
(d '&' a).x = (I_el Y).x '&' a.x by A27,MARGREL1:def 20;
then (d '&' a).x = TRUE '&' a.x by Def11;
hence thesis;
end;
B_SUP(d) = I_el(Y) by A6,Def14;
hence thesis by A2,A28,A29,A26,Def13,Th5;
end;
hence thesis by A7;
end;
case
A30: (for x being Element of Y holds d.x=FALSE) & not (for x being
Element of Y holds d.x=TRUE);
A31: now
assume
A32: (for x being Element of Y holds a.x=TRUE ) or for x being
Element of Y holds a.x=FALSE;
now
per cases by A32;
case
A33: (for x being Element of Y holds a.x=TRUE) & not (for x
being Element of Y holds a.x=FALSE);
A34: for x being Element of Y holds (d 'or' a).x = TRUE
proof
let x be Element of Y;
(d 'or' a).x = d.x 'or' a.x & d.x = FALSE by A30,Def4;
hence thesis by A33;
end;
B_SUP(d) = O_el(Y) by A30,Def14;
then
A35: d '&' B_SUP(a) = O_el(Y) by A2,Th4;
A36: for x being Element of Y holds (d '&' a).x = FALSE
proof
let x be Element of Y;
(d '&' a).x = d.x '&' a.x & d.x = FALSE by A30,MARGREL1:def 20;
hence thesis;
end;
A37: B_INF(a) = I_el(Y) by A33,Def13;
B_INF(d) = O_el(Y) by A30,Def13;
then d 'or' B_INF(a) = I_el(Y) by A1,A37,Th8;
hence thesis by A34,A36,A35,Def13,Def14;
end;
case
A38: (for x being Element of Y holds a.x=FALSE) & not (for x
being Element of Y holds a.x=TRUE);
A39: for x being Element of Y holds (d 'or' a).x = FALSE
proof
let x be Element of Y;
d.x = FALSE & a.x = FALSE by A30,A38;
then (d 'or' a).x = FALSE 'or' FALSE by Def4;
hence thesis;
end;
A40: now
assume
A41: for x being Element of Y holds (d 'or' a).x = TRUE;
let x be Element of Y;
(d 'or' a).x = FALSE by A39;
hence contradiction by A41;
end;
B_SUP(d) = O_el(Y) by A30,Def14;
then
A42: d '&' B_SUP(a) = O_el(Y) by A2,Th4;
A43: for x being Element of Y holds (d '&' a).x = FALSE
proof
let x be Element of Y;
d.x = FALSE & a.x = FALSE by A30,A38;
then (d '&' a).x = FALSE '&' FALSE by MARGREL1:def 20;
hence thesis;
end;
A44: B_INF(a) = O_el(Y) by A38,Def13;
B_INF(d) = O_el(Y) by A30,Def13;
hence thesis by A1,A40,A43,A44,A42,Def13,Def14;
end;
case
A45: (for x being Element of Y holds a.x=FALSE) & for x
being Element of Y holds a.x=TRUE;
A46: for x being Element of Y holds (d 'or' a).x = TRUE
proof
let x be Element of Y;
d.x = FALSE & a.x = TRUE by A30,A45;
then (d 'or' a).x = FALSE 'or' TRUE by Def4;
hence thesis;
end;
B_SUP(d) = O_el(Y) by A30,Def14;
then
A47: d '&' B_SUP(a) = O_el(Y) by A2,Th4;
A48: for x being Element of Y holds (d '&' a).x = FALSE
proof
let x be Element of Y;
d.x = FALSE & a.x = TRUE by A30,A45;
then (d '&' a).x = FALSE '&' TRUE by MARGREL1:def 20;
hence thesis;
end;
A49: B_INF(a) = I_el(Y) by A45,Def13;
B_INF(d) = O_el(Y) by A30,Def13;
then d 'or' B_INF(a) = I_el(Y) by A1,A49,Th8;
hence thesis by A46,A48,A47,Def13,Def14;
end;
end;
hence thesis;
end;
now
for x being Element of Y holds (d '&' a).x = FALSE
proof
let x be Element of Y;
(d '&' a).x = ((O_el Y) '&' a).x by A3,A30,Def13;
hence thesis by Def10,Th4;
end;
then
A50: B_SUP(d '&' a) = O_el(Y) by Def14;
assume that
A51: not( for x being Element of Y holds a.x=TRUE ) and
not(for x being Element of Y holds a.x=FALSE);
B_INF(d) = O_el(Y) by A30,Def13;
then
A52: d 'or' B_INF(a) = O_el(Y) 'or' O_el(Y) by A1,A51,Def13;
A53: d 'or' a = a
proof
let x be Element of Y;
(d 'or' a).x = d.x 'or' a.x by Def4;
then (d 'or' a).x = FALSE 'or' a.x by A30;
hence thesis;
end;
B_SUP(d) = O_el(Y) by A30,Def14;
hence thesis by A2,A51,A53,A50,A52,Def13,Th4;
end;
hence thesis by A31;
end;
case
A54: (for x being Element of Y holds d.x=TRUE) & for x being
Element of Y holds d.x=FALSE;
let x be Element of Y;
d.x=FALSE by A54;
hence thesis by A54;
end;
end;
hence thesis;
end;
now
assume that
A55: not( for x being Element of Y holds d.x=TRUE ) and
A56: not(for x being Element of Y holds d.x=FALSE);
now
per cases by Th20;
case
d=O_el(Y);
hence thesis by A56,Def10;
end;
case
d=I_el(Y);
hence thesis by A55,Def11;
end;
end;
hence thesis;
end;
hence thesis by A4;
end;
theorem
for a being Function of Y,BOOLEAN,x being Element of Y holds (
B_INF a).x <= a.x
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
assume not (for x being Element of Y holds a.x=TRUE);
then B_INF(a) = O_el(Y) by Def13;
then (B_INF a).x = FALSE by Def10;
then (B_INF a).x => a.x = TRUE;
hence thesis;
end;
now
assume for x being Element of Y holds a.x=TRUE;
then a.x = TRUE;
then (B_INF a).x => a.x = TRUE;
hence thesis;
end;
hence thesis by A1;
end;
theorem
for a being Function of Y,BOOLEAN,x being Element of Y holds a.x
<= (B_SUP a).x
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
A1: now
assume not (for x being Element of Y holds a.x=FALSE);
then B_SUP(a) = I_el(Y) by Def14;
then (B_SUP a).x = TRUE by Def11;
then a.x => (B_SUP a).x = TRUE;
hence thesis;
end;
now
assume for x being Element of Y holds a.x=FALSE;
then a.x = FALSE;
then a.x => (B_SUP a).x = TRUE;
hence thesis;
end;
hence thesis by A1;
end;
begin :: Chap. 4 Boolean Valued Functions and Partitions
definition
let Y;
let a be Function of Y,BOOLEAN,PA be a_partition of Y;
pred a is_dependent_of PA means
for F being set st F in PA for x1,x2
being set st x1 in F & x2 in F holds a.x1=a.x2;
end;
theorem
for a being Function of Y,BOOLEAN holds a is_dependent_of %I(Y)
proof
let a be Function of Y,BOOLEAN;
for F being set st F in %I(Y) holds for x1,x2 being set st x1 in F & x2
in F holds a.x1=a.x2
proof
let F be set;
assume F in %I(Y);
then F in {B:ex z being set st B={z} & z in Y} by PARTIT1:31;
then ex B st F=B & ex z being set st B={z} & z in Y;
then consider z being set such that
A1: F={z} and
z in Y;
let x1,x2 be set;
assume that
A2: x1 in F and
A3: x2 in F;
x1=z by A1,A2,TARSKI:def 1;
hence thesis by A1,A3,TARSKI:def 1;
end;
hence thesis;
end;
theorem
for a being constant Function of Y,BOOLEAN holds a
is_dependent_of %O(Y)
proof
let a be constant Function of Y,BOOLEAN;
for F being set st F in %O(Y) holds for x1,x2 being set st x1 in F & x2
in F holds a.x1=a.x2
proof
let F be set;
for x1,x2 being Element of Y holds a.x1=a.x2
proof
let x1,x2 be Element of Y;
per cases by Th20;
suppose
A1: a = O_el(Y);
then a.x1 = FALSE by Def10;
hence thesis by A1,Def10;
end;
suppose
A2: a = I_el(Y);
then a.x1 = TRUE by Def11;
hence thesis by A2,Def11;
end;
end;
hence thesis;
end;
hence thesis;
end;
definition
let Y;
let PA be a_partition of Y;
redefine mode Element of PA -> Subset of Y; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of PA;
thus thesis;
end;
end;
definition
let Y;
let x be Element of Y;
let PA be a_partition of Y;
redefine func EqClass(x,PA) -> Element of PA; :: redefines EqClass (EQREL_1, definition)
coherence by EQREL_1:def 6;
end;
definition
let Y;
let a be Function of Y,BOOLEAN,PA be a_partition of Y;
func B_INF(a,PA) -> Function of Y,BOOLEAN means
:Def16:
for y being
Element of Y holds ( (for x being Element of Y st x in EqClass(y,PA) holds a.x=
TRUE) implies it.y = TRUE ) & (not (for x being Element of Y st x in EqClass(y,
PA) holds a.x=TRUE) implies it.y = FALSE);
existence
proof
defpred P[Element of Y,set] means ((for x being Element of Y st x in
EqClass($1,PA) holds a.x=TRUE) implies $2 = TRUE ) & (not (for x being Element
of Y st x in EqClass($1,PA) holds a.x=TRUE) implies $2 = FALSE);
A1: for e being Element of Y ex u being Element of BOOLEAN st P[e,u]
proof
let e be Element of Y;
per cases;
suppose
for x being Element of Y st x in EqClass(e,PA) holds a.x=TRUE;
hence thesis;
end;
suppose
not (for x being Element of Y st x in EqClass(e,PA) holds a.x= TRUE );
hence thesis;
end;
end;
consider f being Function of Y,BOOLEAN such that
A2: for e being Element of Y holds P[e,f.e] from FUNCT_2:sch 3(A1);
reconsider f as Function of Y,BOOLEAN;
reconsider f as Function of Y,BOOLEAN;
take f;
thus thesis by A2;
end;
uniqueness
proof
let A1,A2 be Function of Y,BOOLEAN such that
A3: for y being Element of Y holds ( (for x being Element of Y st x in
EqClass(y,PA) holds a.x=TRUE) implies A1.y = TRUE ) & (not (for x being Element
of Y st x in EqClass(y,PA) holds a.x=TRUE) implies A1.y = FALSE) and
A4: for y being Element of Y holds ( (for x being Element of Y st x in
EqClass(y,PA) holds a.x=TRUE) implies A2.y = TRUE ) & (not (for x being Element
of Y st x in EqClass(y,PA) holds a.x=TRUE) implies A2.y = FALSE);
let y be Element of Y;
A5: now
assume
A6: not (for x being Element of Y st x in EqClass(y,PA) holds a.x =TRUE);
then A2.y = FALSE by A4;
hence thesis by A3,A6;
end;
now
assume
A7: for x being Element of Y st x in EqClass(y,PA) holds a.x=TRUE;
then A2.y = TRUE by A4;
hence thesis by A3,A7;
end;
hence thesis by A5;
end;
end;
definition
let Y;
let a be Function of Y,BOOLEAN,PA be a_partition of Y;
func B_SUP(a,PA) -> Function of Y,BOOLEAN means
:Def17:
for y being
Element of Y holds ( (ex x being Element of Y st x in EqClass(y,PA) & a.x=TRUE)
implies it.y = TRUE ) & (not (ex x being Element of Y st x in EqClass(y,PA) & a
.x=TRUE) implies it.y = FALSE);
existence
proof
defpred P[Element of Y,set] means ( (ex x being Element of Y st x in
EqClass($1,PA) & a.x=TRUE) implies $2 = TRUE ) & (not (ex x being Element of Y
st x in EqClass($1,PA) & a.x=TRUE) implies $2 = FALSE);
A1: for e being Element of Y ex u being Element of BOOLEAN st P[e,u]
proof
let e be Element of Y;
per cases;
suppose
ex x being Element of Y st x in EqClass(e,PA) & a.x=TRUE;
hence thesis;
end;
suppose
not (ex x being Element of Y st x in EqClass(e,PA) & a.x=TRUE);
hence thesis;
end;
end;
consider f being Function of Y,BOOLEAN such that
A2: for e being Element of Y holds P[e,f.e] from FUNCT_2:sch 3(A1);
reconsider f as Function of Y,BOOLEAN;
reconsider f as Function of Y,BOOLEAN;
take f;
thus thesis by A2;
end;
uniqueness
proof
let A1,A2 be Function of Y,BOOLEAN such that
A3: for y being Element of Y holds ( (ex x being Element of Y st x in
EqClass(y,PA) & a.x=TRUE) implies A1.y = TRUE ) & (not (ex x being Element of Y
st x in EqClass(y,PA) & a.x=TRUE) implies A1.y = FALSE) and
A4: for y being Element of Y holds ( (ex x being Element of Y st x in
EqClass(y,PA) & a.x=TRUE) implies A2.y = TRUE ) & (not (ex x being Element of Y
st x in EqClass(y,PA) & a.x=TRUE) implies A2.y = FALSE);
let y be Element of Y;
A5: now
assume
A6: not (ex x being Element of Y st x in EqClass(y,PA) & a.x=TRUE );
then A2.y = FALSE by A4;
hence thesis by A3,A6;
end;
now
assume
A7: ex x being Element of Y st x in EqClass(y,PA) & a.x=TRUE;
then A2.y = TRUE by A4;
hence thesis by A3,A7;
end;
hence thesis by A5;
end;
end;
theorem
for a being Function of Y,BOOLEAN,PA being a_partition of Y
holds B_INF(a,PA) is_dependent_of PA
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
for F being set st F in PA holds for x1,x2 being set st x1 in F & x2 in
F holds B_INF(a,PA).x1=B_INF(a,PA).x2
proof
let F be set;
assume
A1: F in PA;
let x1,x2 be set;
assume that
A2: x1 in F and
A3: x2 in F;
reconsider x1 as Element of Y by A1,A2;
A4: EqClass(x1,PA) = F or EqClass(x1,PA) misses F by A1,EQREL_1:def 4;
reconsider x2 as Element of Y by A1,A3;
A5: x1 in EqClass(x1,PA) & EqClass(x2,PA) = F
by A1,A3,EQREL_1:def 6;
per cases;
suppose
A6: for x being Element of Y st x in EqClass(x1,PA) holds a.x=TRUE;
then (B_INF(a,PA)).x1 = TRUE by Def16;
hence thesis by A2,A4,A5,A6,Def16,XBOOLE_0:3;
end;
suppose
A7: not (for x being Element of Y st x in EqClass(x1,PA) holds a.x= TRUE);
then (B_INF(a,PA)).x1 = FALSE by Def16;
hence thesis by A2,A4,A5,A7,Def16,XBOOLE_0:3;
end;
end;
hence thesis;
end;
theorem
for a being Function of Y,BOOLEAN,PA being a_partition of Y
holds B_SUP(a,PA) is_dependent_of PA
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
for F being set st F in PA holds for x1,x2 being set st x1 in F & x2 in
F holds B_SUP(a,PA).x1=B_SUP(a,PA).x2
proof
let F be set;
assume
A1: F in PA;
let x1,x2 be set;
assume
A2: x1 in F & x2 in F;
then reconsider x1,x2 as Element of Y by A1;
A3: x1 in EqClass(x1,PA) by EQREL_1:def 6;
EqClass(x1,PA) = F or EqClass(x1,PA) misses F by A1,EQREL_1:def 4;
then
A4: EqClass(x2,PA) = EqClass(x1,PA) 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,PA) & a.x=TRUE;
then (B_SUP(a,PA)).x1 = TRUE by Def17;
hence thesis by A4,A5,Def17;
end;
suppose
A6: not (ex x being Element of Y st x in EqClass(x1,PA) & a.x=TRUE);
then (B_SUP(a,PA)).x1 = FALSE by Def17;
hence thesis by A4,A6,Def17;
end;
end;
hence thesis;
end;
theorem
for a being Function of Y,BOOLEAN,PA being a_partition of Y
holds B_INF(a,PA) '<' a
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
B_INF(a,PA) 'imp' a = I_el Y
proof
let y be Element of Y;
per cases;
suppose
A1: for x being Element of Y st x in EqClass(y,PA) holds a.x=TRUE;
A2: a.y = TRUE by A1,EQREL_1:def 6;
'not' B_INF(a,PA).y = ('not' B_INF(a,PA)).y by MARGREL1:def 19;
then
'not' (B_INF(a,PA)).y 'or' a.y = ('not' B_INF(a,PA)).y 'or' (I_el Y)
.y by A2,Def11
.= ('not' B_INF(a,PA) 'or' I_el Y).y by Def4
.= (I_el Y).y by Th9;
hence thesis by Def8;
end;
suppose
not (for x being Element of Y st x in EqClass(y,PA) holds a.x= TRUE );
then (B_INF(a,PA)).y = FALSE by Def16;
then 'not' (B_INF(a,PA)).y 'or' a.y = (I_el Y).y 'or' a.y by Def11
.= ((I_el Y) 'or' a).y by Def4
.= (I_el Y).y by Th9;
hence thesis by Def8;
end;
end;
hence thesis by Th15;
end;
theorem
for a being Function of Y,BOOLEAN,PA being a_partition of Y
holds a '<' B_SUP(a,PA)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
a 'imp' B_SUP(a,PA) = I_el Y
proof
let y be Element of Y;
per cases;
suppose
ex x being Element of Y st x in EqClass(y,PA) & a.x=TRUE;
then (B_SUP(a,PA)).y = TRUE by Def17;
then (B_SUP(a,PA)).y = (I_el Y).y by Def11;
then ('not' a.y) 'or' (B_SUP(a,PA)).y = ('not' a).y 'or' (I_el Y).y by
MARGREL1:def 19
.= ('not' a 'or' I_el Y).y by Def4
.= (I_el Y).y by Th9;
hence thesis by Def8;
end;
suppose
A1: not (ex x being Element of Y st x in EqClass(y,PA) & a.x=TRUE);
a.y<>TRUE by A1,EQREL_1:def 6;
then a.y=FALSE by XBOOLEAN:def 3;
then ('not' a.y) 'or' (B_SUP(a,PA)).y = (I_el Y).y 'or' (B_SUP(a,PA)).y
by Def11
.= ((I_el Y) 'or' B_SUP(a,PA)).y by Def4
.= (I_el Y).y by Th9;
hence thesis by Def8;
end;
end;
hence thesis by Th15;
end;
theorem
for a being Function of Y,BOOLEAN,PA being a_partition of Y
holds 'not' B_INF(a,PA) = B_SUP('not' a,PA)
proof
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let y be Element of Y;
A1: now
assume that
A2: for x being Element of Y st x in EqClass(y,PA) holds a.x=TRUE and
A3: ex x being Element of Y st x in EqClass(y,PA) & ('not' a).x=TRUE;
consider x1 being Element of Y such that
A4: x1 in EqClass(y,PA) and
A5: ('not' a).x1=TRUE by A3;
('not' 'not' a).x1= 'not' TRUE by A5,MARGREL1:def 19;
hence contradiction by A2,A4;
end;
A6: now
assume that
A7: not(for x being Element of Y st x in EqClass(y,PA) holds a.x= TRUE) and
A8: not(ex x being Element of Y st x in EqClass(y,PA) & ('not' a).x = TRUE);
consider x1 being Element of Y such that
A9: x1 in EqClass(y,PA) and
A10: a.x1<>TRUE by A7;
a.x1=FALSE by A10,XBOOLEAN:def 3;
then ('not' a).x1 = 'not' FALSE by MARGREL1:def 19;
hence contradiction by A8,A9;
end;
A11: now
assume that
A12: not(for x being Element of Y st x in EqClass(y,PA) holds a.x= TRUE) and
A13: ex x being Element of Y st x in EqClass(y,PA) & ('not' a).x= TRUE;
(B_INF(a,PA)).y = FALSE by A12,Def16;
then ('not' B_INF(a,PA)).y = 'not' FALSE by MARGREL1:def 19;
hence thesis by A13,Def17;
end;
now
assume that
A14: for x being Element of Y st x in EqClass(y,PA) holds a.x=TRUE and
A15: not(ex x being Element of Y st x in EqClass(y,PA) & ('not' a).x =TRUE );
(B_INF(a,PA)).y = TRUE by A14,Def16;
then ('not' B_INF(a,PA)).y = 'not' TRUE by MARGREL1:def 19;
hence thesis by A15,Def17;
end;
hence thesis by A1,A11,A6;
end;
theorem
for a being Function of Y,BOOLEAN holds B_INF(a,%O(Y))=B_INF(a)
proof
let a be Function of Y,BOOLEAN;
let y be Element of Y;
A1: now
EqClass(y,%O(Y)) in %O(Y);
then EqClass(y,%O(Y)) in {Y} by PARTIT1:def 8;
then
A2: EqClass(y,%O(Y))=Y by TARSKI:def 1;
assume ( not(for x being Element of Y holds a.x=TRUE))& for x being
Element of Y st x in EqClass(y,%O(Y)) holds a.x=TRUE;
hence contradiction by A2;
end;
A3: now
assume that
A4: not(for x being Element of Y holds a.x=TRUE) and
A5: not(for x being Element of Y st x in EqClass(y,%O(Y)) holds a.x = TRUE);
B_INF(a) = O_el(Y) by A4,Def13;
then (B_INF a).y = FALSE by Def10;
hence thesis by A5,Def16;
end;
now
assume that
A6: for x being Element of Y holds a.x=TRUE and
A7: for x being Element of Y st x in EqClass(y,%O(Y)) holds a.x=TRUE;
B_INF(a) = I_el(Y) by A6,Def13;
then (B_INF a).y = TRUE by Def11;
hence thesis by A7,Def16;
end;
hence thesis by A1,A3;
end;
theorem
for a being Function of Y,BOOLEAN holds B_SUP(a,%O(Y))=B_SUP(a)
proof
let a be Function of Y,BOOLEAN;
let y be Element of Y;
EqClass(y,%O(Y)) in %O(Y);
then EqClass(y,%O(Y)) in {Y} by PARTIT1:def 8;
then
A1: EqClass(y,%O(Y))=Y by TARSKI:def 1;
A2: now
assume that
A3: not(ex x being Element of Y st x in EqClass(y,%O(Y)) & a.x=TRUE ) and
A4: for x being Element of Y holds a.x=FALSE;
B_SUP(a) = O_el(Y) by A4,Def14;
then (B_SUP a).y = FALSE by Def10;
hence thesis by A3,Def17;
end;
now
assume that
A5: ex x being Element of Y st x in EqClass(y,%O(Y)) & a.x=TRUE and
not(for x being Element of Y holds a.x=FALSE);
B_SUP(a) = I_el(Y) by A5,Def14;
then (B_SUP a).y = TRUE by Def11;
hence thesis by A5,Def17;
end;
hence thesis by A2,A1,XBOOLEAN:def 3;
end;
theorem
for a being Function of Y,BOOLEAN holds B_INF(a,%I(Y))=a
proof
let a be Function of Y,BOOLEAN;
let y be Element of Y;
A1: now
EqClass(y,%I(Y)) in %I(Y);
then EqClass(y,%I(Y)) in {B:ex z being set st B={z} & z in Y} by
PARTIT1:31;
then ex B st EqClass(y,%I(Y))=B & ex z being set st B={z} & z in Y;
then consider z being set such that
A2: EqClass(y,%I(Y))={z} and
z in Y;
A3: y in {z} by A2,EQREL_1:def 6;
assume that
A4: not(for x being Element of Y st x in EqClass(y,%I(Y)) holds a.x=
TRUE) and
A5: a.y = TRUE;
consider x1 being Element of Y such that
A6: x1 in EqClass(y,%I(Y)) and
A7: a.x1<>TRUE by A4;
x1=z by A6,A2,TARSKI:def 1;
hence contradiction by A5,A7,A3,TARSKI:def 1;
end;
A8: now
assume
A9: for x being Element of Y st x in EqClass(y,%I(Y)) holds a.x=TRUE;
then a.y = TRUE by EQREL_1:def 6;
hence thesis by A9,Def16;
end;
now
assume that
A10: not(for x being Element of Y st x in EqClass(y,%I(Y)) holds a.x
=TRUE) and
A11: a.y<>TRUE;
a.y = FALSE by A11,XBOOLEAN:def 3;
hence thesis by A10,Def16;
end;
hence thesis by A8,A1;
end;
theorem
for a being Function of Y,BOOLEAN holds B_SUP(a,%I(Y))=a
proof
let a be Function of Y,BOOLEAN;
let y be Element of Y;
A1: now
EqClass(y,%I(Y)) in %I(Y);
then EqClass(y,%I(Y)) in {B:ex z being set st B={z} & z in Y} by
PARTIT1:31;
then ex B st EqClass(y,%I(Y))=B & ex z being set st B={z} & z in Y;
then consider z being set such that
A2: EqClass(y,%I(Y))={z} and
z in Y;
A3: y in {z} by A2,EQREL_1:def 6;
assume that
A4: ex x being Element of Y st x in EqClass(y,%I(Y)) & a.x=TRUE and
A5: a.y<>TRUE;
consider x1 being Element of Y such that
A6: x1 in EqClass(y,%I(Y)) and
A7: a.x1=TRUE by A4;
x1=z by A6,A2,TARSKI:def 1;
hence contradiction by A5,A7,A3,TARSKI:def 1;
end;
A8: now
assume that
A9: not(ex x being Element of Y st x in EqClass(y,%I(Y)) & a.x=TRUE ) and
A10: a.y<>TRUE;
a.y = FALSE by A10,XBOOLEAN:def 3;
hence thesis by A9,Def17;
end;
y in EqClass(y,%I(Y)) by EQREL_1:def 6;
hence thesis by A1,A8,Def17;
end;
theorem
for a,b being Function of Y,BOOLEAN,PA being a_partition of Y
holds B_INF(a '&' b,PA)=B_INF(a,PA) '&' B_INF(b,PA)
proof
let a,b be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let y be Element of Y;
A1: now
assume that
for x being Element of Y st x in EqClass(y,PA) holds a.x=TRUE and
A2: not(for x being Element of Y st x in EqClass(y,PA) holds b.x= TRUE);
(B_INF(b,PA)).y = FALSE by A2,Def16;
then (B_INF(a,PA)).y '&' (B_INF(b,PA)).y = FALSE;
then
A3: (B_INF(a,PA) '&' B_INF(b,PA)).y = FALSE by MARGREL1:def 20;
consider x1 being Element of Y such that
A4: x1 in EqClass(y,PA) and
A5: b.x1<>TRUE by A2;
b.x1=FALSE by A5,XBOOLEAN:def 3;
then a.x1 '&' b.x1 = FALSE;
then (a '&' b).x1 <>TRUE by MARGREL1:def 20;
hence thesis by A4,A3,Def16;
end;
A6: now
assume that
A7: not(for x being Element of Y st x in EqClass(y,PA) holds a.x= TRUE) and
A8: not(for x being Element of Y st x in EqClass(y,PA) holds b.x= TRUE);
(B_INF(b,PA)).y = FALSE by A8,Def16;
then (B_INF(a,PA)).y '&' (B_INF(b,PA)).y = FALSE;
then
A9: (B_INF(a,PA) '&' B_INF(b,PA)).y = FALSE by MARGREL1:def 20;
consider xa being Element of Y such that
A10: xa in EqClass(y,PA) and
A11: a.xa<>TRUE by A7;
a.xa=FALSE by A11,XBOOLEAN:def 3;
then a.xa '&' b.xa = FALSE;
then (a '&' b).xa<>TRUE by MARGREL1:def 20;
hence thesis by A10,A9,Def16;
end;
A12: now
assume that
A13: for x being Element of Y st x in EqClass(y,PA) holds a.x=TRUE and
A14: for x being Element of Y st x in EqClass(y,PA) holds b.x=TRUE;
A15: for x being Element of Y st x in EqClass(y,PA) holds (a '&' b).x= TRUE
proof
let x be Element of Y;
assume
A16: x in EqClass(y,PA);
then b.x=TRUE by A14;
then a.x '&' b.x = TRUE '&' TRUE by A13,A16;
hence thesis by MARGREL1:def 20;
end;
(B_INF(b,PA)).y = TRUE by A14,Def16;
then (B_INF(a,PA)).y '&' (B_INF(b,PA)).y = TRUE '&' TRUE by A13,Def16;
then (B_INF(a,PA) '&' B_INF(b,PA)).y = TRUE by MARGREL1:def 20;
hence thesis by A15,Def16;
end;
now
assume that
A17: not(for x being Element of Y st x in EqClass(y,PA) holds a.x= TRUE) and
A18: for x being Element of Y st x in EqClass(y,PA) holds b.x=TRUE;
(B_INF(b,PA)).y = TRUE by A18,Def16;
then (B_INF(a,PA)).y '&' (B_INF(b,PA)).y = FALSE '&' TRUE by A17,Def16;
then
A19: (B_INF(a,PA) '&' B_INF(b,PA)).y = FALSE by MARGREL1:def 20;
consider x1 being Element of Y such that
A20: x1 in EqClass(y,PA) and
A21: a.x1<>TRUE by A17;
a.x1=FALSE by A21,XBOOLEAN:def 3;
then a.x1 '&' b.x1 = FALSE;
then (a '&' b).x1 <>TRUE by MARGREL1:def 20;
hence thesis by A20,A19,Def16;
end;
hence thesis by A12,A1,A6;
end;
theorem
for a,b being Function of Y,BOOLEAN,PA being a_partition of Y
holds B_SUP(a 'or' b,PA)=B_SUP(a,PA) 'or' B_SUP(b,PA)
proof
let a,b be Function of Y,BOOLEAN;
let PA be a_partition of Y;
let y be Element of Y;
A1: now
assume
A2: ex x being Element of Y st x in EqClass(y,PA) & (a 'or' b).x= TRUE;
then consider x1 being Element of Y such that
A3: x1 in EqClass(y,PA) and
A4: (a 'or' b).x1=TRUE;
A5: a.x1 = FALSE & b.x1 = FALSE or a.x1 = FALSE & b.x1 = TRUE or a.x1 =
TRUE & b.x1 = FALSE or a.x1 = TRUE & b.x1 = TRUE by XBOOLEAN:def 3;
A6: a.x1 'or' b.x1=TRUE by A4,Def4;
now
per cases by A6,A5;
case
a.x1 = FALSE & b.x1 = TRUE;
then (B_SUP(b,PA)).y = TRUE by A3,Def17;
then (B_SUP(a,PA)).y 'or' (B_SUP(b,PA)).y = TRUE;
then (B_SUP(a,PA) 'or' B_SUP(b,PA)).y = TRUE by Def4;
hence thesis by A2,Def17;
end;
case
a.x1 = TRUE & b.x1 = FALSE;
then (B_SUP(a,PA)).y = TRUE by A3,Def17;
then (B_SUP(a,PA)).y 'or' (B_SUP(b,PA)).y = TRUE;
then (B_SUP(a,PA) 'or' B_SUP(b,PA)).y = TRUE by Def4;
hence thesis by A2,Def17;
end;
case
a.x1 = TRUE & b.x1 = TRUE;
then (B_SUP(b,PA)).y = TRUE by A3,Def17;
then (B_SUP(a,PA)).y 'or' (B_SUP(b,PA)).y = TRUE;
then (B_SUP(a,PA) 'or' B_SUP(b,PA)).y = TRUE by Def4;
hence thesis by A2,Def17;
end;
end;
hence thesis;
end;
now
assume
A7: not (ex x being Element of Y st x in EqClass(y,PA) & (a 'or' b) .x=TRUE);
now
assume ex x being Element of Y st x in EqClass(y,PA) & b.x=TRUE;
then consider x1 being Element of Y such that
A8: x1 in EqClass(y,PA) and
A9: b.x1=TRUE;
a.x1 'or' b.x1 = TRUE by A9;
then (a 'or' b).x1 = TRUE by Def4;
hence contradiction by A7,A8;
end;
then
A10: (B_SUP(b,PA)).y = FALSE by Def17;
now
assume ex x being Element of Y st x in EqClass(y,PA) & a.x=TRUE;
then consider x1 being Element of Y such that
A11: x1 in EqClass(y,PA) and
A12: a.x1=TRUE;
a.x1 'or' b.x1 = TRUE by A12;
then (a 'or' b).x1 = TRUE by Def4;
hence contradiction by A7,A11;
end;
then (B_SUP(a,PA)).y 'or' (B_SUP(b,PA)).y = FALSE 'or' FALSE by A10,Def17
;
then (B_SUP(a,PA) 'or' B_SUP(b,PA)).y = FALSE by Def4;
hence thesis by A7,Def17;
end;
hence thesis by A1;
end;
definition
let Y;
let f be Function of Y,BOOLEAN;
func GPart(f) -> a_partition of Y equals
{{x where x is Element of Y:f.x =
TRUE }, {x9 where x9 is Element of Y:f.x9 = FALSE}} \ {{}};
correctness
proof
defpred P[set] means f.$1 = TRUE;
reconsider C={x where x is Element of Y: P[x]} as Subset of Y from
DOMAIN_1:sch 7;
defpred P[set] means f.$1 = FALSE;
reconsider D={x9 where x9 is Element of Y: P[x9]} as Subset of Y from
DOMAIN_1:sch 7;
A1: union ({C,D} \ {{}}) = Y
proof
thus union ({C,D} \ {{}}) c= Y
proof
let a be object;
assume a in union ({C,D} \ {{}});
then ex b being set st a in b & b in ({C,D} \ {{}}) by TARSKI:def 4;
then a in C or a in D by TARSKI:def 2;
hence thesis;
end;
let a be object;
A2: C in {C,D} by TARSKI:def 2;
assume a in Y;
then reconsider a as Element of Y;
A3: f.a = TRUE or f.a = FALSE by TARSKI:def 2;
A4: D in {C,D} by TARSKI:def 2;
per cases by A3;
suppose
A5: a in C;
then not C in {{}} by TARSKI:def 1;
then C in ({C,D} \ {{}}) by A2,XBOOLE_0:def 5;
hence thesis by A5,TARSKI:def 4;
end;
suppose
A6: a in D;
then not D in {{}} by TARSKI:def 1;
then D in ({C,D} \ {{}}) by A4,XBOOLE_0:def 5;
hence thesis by A6,TARSKI:def 4;
end;
end;
A7: for A being Subset of Y st A in ({C,D} \ {{}}) holds A<>{} & for B
being Subset of Y st B in ({C,D} \ {{}}) holds A=B or A misses B
proof
let A be Subset of Y;
A8: now
given b being object such that
A9: b in C & b in D;
now
assume b in C;
then
A10: ex x being Element of Y st b=x & f.x=TRUE;
now
assume b in D;
then ex x9 being Element of Y st b=x9 & f.x9=FALSE;
hence contradiction by A10;
end;
hence not b in D;
end;
hence contradiction by A9;
end;
assume
A11: A in ({C,D} \ {{}});
then not A in {{}} by XBOOLE_0:def 5;
hence A<>{} by TARSKI:def 1;
let B be Subset of Y;
assume
A12: B in ({C,D} \ {{}});
per cases by A11,A12,TARSKI:def 2;
suppose
A=C & B=C;
hence thesis;
end;
suppose
A=D & B=D;
hence thesis;
end;
suppose
A=C & B=D;
hence thesis by A8,XBOOLE_0:3;
end;
suppose
A=D & B=C;
hence thesis by A8,XBOOLE_0:3;
end;
end;
{C,D} \ {{}} c= bool Y
proof
let a be object;
assume a in {C,D} \ {{}};
then a=C or a=D by TARSKI:def 2;
hence thesis;
end;
hence thesis by A1,A7,EQREL_1:def 4;
end;
end;
theorem
for a being Function of Y,BOOLEAN holds a is_dependent_of GPart( a)
proof
let a be Function of Y,BOOLEAN;
defpred P[set] means a.$1 = TRUE;
reconsider C={x where x is Element of Y: P[x]} as Subset of Y from DOMAIN_1:
sch 7;
defpred P[set] means a.$1 = FALSE;
reconsider D={x9 where x9 is Element of Y: P[x9]} as Subset of Y from
DOMAIN_1:sch 7;
for F being set st F in GPart(a) holds for x1,x2 being set st x1 in F &
x2 in F holds a.x1=a.x2
proof
let F be set;
assume
A1: F in GPart(a);
thus for x1,x2 being set st x1 in F & x2 in F holds a.x1=a.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;
now
per cases by A1,TARSKI:def 2;
case
F=C;
then (ex x being Element of Y st x=x1 & a.x=TRUE )& ex x5 being
Element of Y st x5=x2 & a.x5=TRUE by A2;
hence thesis;
end;
case
F=D;
then (ex x being Element of Y st x=x1 & a.x=FALSE )& ex x5 being
Element of Y st x5=x2 & a.x5=FALSE by A2;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for a being Function of Y,BOOLEAN,PA being a_partition of Y st a
is_dependent_of PA holds PA is_finer_than GPart(a)
proof
let a be Function of Y,BOOLEAN, PA be a_partition of Y;
defpred P[set] means a.$1 = TRUE;
reconsider C={x where x is Element of Y: P[x]} as Subset of Y from DOMAIN_1:
sch 7;
defpred P[set] means a.$1 = FALSE;
reconsider D={x9 where x9 is Element of Y: P[x9]} as Subset of Y from
DOMAIN_1:sch 7;
assume
A1: a is_dependent_of PA;
for g being set st g in PA ex h being set st h in GPart(a) & g c= h
proof
let g be set;
set u = the Element of g;
assume
A2: g in PA;
then
A3: g <> {} by EQREL_1:def 4;
then u in g;
then reconsider u as Element of Y by A2;
A4: for x1 being set st x1 in g holds a.x1=TRUE or a.x1=FALSE
proof
let x1 be set;
assume x1 in g;
then reconsider x1 as Element of Y by A2;
a.x1 in BOOLEAN;
hence thesis by TARSKI:def 2;
end;
now
per cases by A3,A4;
case
A5: a.u=TRUE;
A6: g c= C
proof
let t be object;
assume
A7: t in g;
then reconsider t as Element of Y by A2;
now
per cases by A4,A7;
case
a.t=TRUE;
hence thesis;
end;
case
a.t=FALSE;
hence contradiction by A1,A2,A5,A7;
end;
end;
hence thesis;
end;
u in C by A5;
then
A8: not C in {{}} by TARSKI:def 1;
C in {C,D} by TARSKI:def 2;
then C in ({C,D} \ {{}}) by A8,XBOOLE_0:def 5;
hence thesis by A6;
end;
case
A9: a.u=FALSE;
A10: g c= D
proof
let t be object;
assume
A11: t in g;
then reconsider t as Element of Y by A2;
now
per cases by A4,A11;
case
a.t=TRUE;
hence contradiction by A1,A2,A9,A11;
end;
case
a.t=FALSE;
hence thesis;
end;
end;
hence thesis;
end;
u in D by A9;
then
A12: not D in {{}} by TARSKI:def 1;
D in {C,D} by TARSKI:def 2;
then D in ({C,D} \ {{}}) by A12,XBOOLE_0:def 5;
hence thesis by A10;
end;
end;
hence thesis;
end;
hence thesis by SETFAM_1:def 2;
end;
begin :: BINARI_5
definition
let x, y be Element of BOOLEAN;
redefine func x 'nand' y -> Element of BOOLEAN; :: redefines 'nand' (XBOOLEAN, definition)
correctness
proof
x 'nand' y =FALSE or x 'nand' y = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
end;
definition
let x, y be Element of BOOLEAN;
redefine func x 'nor' y -> Element of BOOLEAN; :: redefines 'nor' (XBOOLEAN, definition)
correctness
proof
x 'nor' y =FALSE or x 'nor' y = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
end;
definition
let x, y be boolean object;
redefine func x <=> y equals :: redefines <=> (XBOOLEAN, definition)
'not' (x 'xor' y);
correctness;
end;
definition
let x, y be Element of BOOLEAN;
redefine func x <=> y -> Element of BOOLEAN; :: redefines <=> (BVFUNC_1, redefinition) → <=> (XBOOLEAN, definition)
correctness
proof
x <=> y =FALSE or x <=> y = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
end;
reserve x,y,z for boolean object;
theorem
TRUE 'nand' x = 'not' x;
theorem
FALSE 'nand' x = TRUE;
theorem
x 'nand' x = 'not' x & 'not' (x 'nand' x) = x;
theorem
'not' (x 'nand' y) = x '&' y;
theorem
x 'nand' 'not' x = TRUE & 'not' (x 'nand' 'not' x) = FALSE
by XBOOLEAN:135,138;
theorem
x 'nand' (y '&' z) = 'not' (x '&' y '&' z);
theorem
x 'nand' (y '&' z) = (x '&' y) 'nand' z;
theorem
TRUE 'nor' x = FALSE;
theorem
FALSE 'nor' x = 'not' x;
theorem
x 'nor' x = 'not' x & 'not' (x 'nor' x) = x;
theorem
'not' (x 'nor' y) = x 'or' y;
theorem
x 'nor' 'not' x = FALSE & 'not' (x 'nor' 'not' x) = TRUE by XBOOLEAN:134,138;
theorem
x 'nor' (y 'or' z) = 'not' (x 'or' y 'or' z);
theorem
TRUE <=> x = x;
theorem
FALSE <=> x = 'not' x;
theorem
x <=> x = TRUE & 'not' (x <=> x) = FALSE by XBOOLEAN:125,143;
theorem
'not' (x <=> y) = x 'xor' y;
theorem
x <=> 'not' x = FALSE & 'not' (x <=> 'not' x) = TRUE by XBOOLEAN:129,142;
theorem
x <= (y => z) iff x '&' y <= z;
theorem
x <=> y = (x => y) '&' (y => x);
theorem
x => y = 'not' y => 'not' x;
theorem
x <=> y = 'not' x <=> 'not' y;
theorem
x=TRUE & (x => y)=TRUE implies y=TRUE;
theorem
y=TRUE implies (x => y)=TRUE;
theorem
('not' x)=TRUE implies (x => y)=TRUE;
theorem
z => (y => x)=TRUE implies y => (z => x)=TRUE;
theorem
z => (y => x)=TRUE & y=TRUE implies z => x=TRUE;
theorem
z => (y => x)=TRUE & y=TRUE & z = TRUE implies x=TRUE;