:: Predicate Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-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, MARGREL1, PARTIT1, BVFUNC_1, XBOOLEAN,
FUNCT_1, EQREL_1, BVFUNC_2;
notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1,
FUNCT_2, EQREL_1, BVFUNC_1, BVFUNC_2;
constructors BINARITH, BVFUNC_1, BVFUNC_2, NUMBERS;
registrations XBOOLEAN, MARGREL1;
requirements ARITHM, NUMERALS;
definitions BVFUNC_1, FUNCT_2;
equalities BVFUNC_1, XBOOLEAN, BVFUNC_2;
expansions BVFUNC_1, BVFUNC_2;
theorems BVFUNC_1, BVFUNC_2, MARGREL1, XBOOLEAN, EQREL_1;
begin
::Chap. 1 Preliminaries
reserve Y for non empty set;
theorem
for a,b,c being Function of Y,BOOLEAN holds a '<' (b 'imp' c)
implies a '&' b '<' c
proof
let a,b,c be Function of Y,BOOLEAN;
assume
A1: a '<' (b 'imp' c);
for x being Element of Y holds (a '&' b 'imp' c).x = TRUE
proof
let x be Element of Y;
A2: (a 'imp' (b 'imp' c)).x =('not' a.x) 'or' (b 'imp' c).x by BVFUNC_1:def 8
.=('not' a.x) 'or' (('not' b.x) 'or' c.x) by BVFUNC_1:def 8
.=('not' a.x 'or' 'not' b.x) 'or' c.x;
A3: (a '&' b 'imp' c).x =('not' (a '&' b).x) 'or' c.x by BVFUNC_1:def 8
.=('not' a.x 'or' 'not' b.x) 'or' c.x by MARGREL1:def 20;
a 'imp' (b 'imp' c) = I_el(Y) by A1,BVFUNC_1:16;
hence thesis by A2,A3,BVFUNC_1:def 11;
end;
then (a '&' b) 'imp' c = I_el(Y) by BVFUNC_1:def 11;
hence thesis by BVFUNC_1:16;
end;
theorem
for a,b,c being Function of Y,BOOLEAN holds a '&' b '<' c
implies a '<' (b 'imp' c)
proof
let a,b,c be Function of Y,BOOLEAN;
assume
A1: a '&' b '<' c;
for x being Element of Y holds (a 'imp' (b 'imp' c)).x = TRUE
proof
let x be Element of Y;
A2: (a 'imp' (b 'imp' c)).x =('not' a.x) 'or' (b 'imp' c).x by BVFUNC_1:def 8
.=('not' a.x) 'or' (('not' b.x) 'or' c.x) by BVFUNC_1:def 8
.=('not' a.x 'or' 'not' b.x) 'or' c.x;
A3: (a '&' b 'imp' c).x =('not' (a '&' b).x) 'or' c.x by BVFUNC_1:def 8
.=('not' a.x 'or' 'not' b.x) 'or' c.x by MARGREL1:def 20;
(a '&' b) 'imp' c = I_el(Y) by A1,BVFUNC_1:16;
hence thesis by A2,A3,BVFUNC_1:def 11;
end;
then a 'imp' (b 'imp' c) = I_el(Y) by BVFUNC_1:def 11;
hence thesis by BVFUNC_1:16;
end;
theorem
for a,b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'or' (a '&' b)).x = a.x 'or' (a '&' b).x by BVFUNC_1:def 4
.= a.x 'or' a.x '&' b.x by MARGREL1:def 20
.= a.x by XBOOLEAN:5;
end;
theorem
for a,b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a '&' (a 'or' b)).x = a.x '&' (a 'or' b).x by MARGREL1:def 20
.= a.x '&' (a.x 'or' b.x) by BVFUNC_1:def 4
.= a.x by XBOOLEAN:6;
end;
theorem Th5:
for a being Function of Y,BOOLEAN holds a '&' 'not' a = O_el(Y)
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a '&' 'not' a).x = a.x '&' ('not' a).x by MARGREL1:def 20
.= a.x '&' 'not' a.x by MARGREL1:def 19
.= FALSE by XBOOLEAN:138
.= O_el(Y).x by BVFUNC_1:def 10;
end;
theorem
for a being Function of Y,BOOLEAN holds a 'or' 'not' a = I_el(Y)
proof
let a be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'or' 'not' a).x = a.x 'or' ('not' a).x by BVFUNC_1:def 4
.= a.x 'or' 'not' a.x by MARGREL1:def 19
.= TRUE by XBOOLEAN:102
.= I_el(Y).x by BVFUNC_1:def 11;
end;
theorem Th7:
for a,b being Function of Y,BOOLEAN
holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'eqv' b).x = a.x <=> b.x by BVFUNC_1:def 9
.= (a.x => b.x) '&' (b.x => a.x)
.= (a 'imp' b).x '&' (b.x => a.x) by BVFUNC_1:def 8
.= (a 'imp' b).x '&' (b 'imp' a).x by BVFUNC_1:def 8
.= ((a 'imp' b) '&' (b 'imp' a)).x by MARGREL1:def 20;
end;
theorem Th8:
for a,b being Function of Y,BOOLEAN holds a 'imp' b = 'not' a 'or' b
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'imp' b).x = a.x => b.x by BVFUNC_1:def 8
.= 'not' a.x 'or' b.x
.= ('not' a).x 'or' b.x by MARGREL1:def 19
.= ('not' a 'or' b).x by BVFUNC_1:def 4;
end;
theorem
for a,b being Function of Y,BOOLEAN
holds a 'xor' b = ('not' a '&' b) 'or' (a '&' 'not' b)
proof
let a,b be Function of Y,BOOLEAN;
let x be Element of Y;
thus (a 'xor' b).x = a.x 'xor' b.x by BVFUNC_1:def 5
.= 'not' a.x '&' b.x 'or' a.x '&' 'not' b.x
.= 'not' a.x '&' b.x 'or' a.x '&' ('not' b).x by MARGREL1:def 19
.= ('not' a).x '&' b.x 'or' a.x '&' ('not' b).x by MARGREL1:def 19
.= ('not' a '&' b).x 'or' a.x '&' ('not' b).x by MARGREL1:def 20
.= ('not' a '&' b).x 'or' (a '&' 'not' b).x by MARGREL1:def 20
.= (('not' a '&' b) 'or' (a '&' 'not' b)).x by BVFUNC_1:def 4;
end;
theorem Th10:
for a,b being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el
(Y) iff (a 'imp' b)=I_el(Y) & (b 'imp' a)=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
thus (a 'eqv' b)=I_el(Y) implies (a 'imp' b)=I_el(Y) & (b 'imp' a)=I_el(Y)
proof
assume (a 'eqv' b)=I_el(Y);
then a = b by BVFUNC_1:17;
hence thesis by BVFUNC_1:16;
end;
assume a 'imp' b=I_el(Y) & b 'imp' a=I_el(Y);
then (a 'eqv' b)=I_el(Y) '&' I_el(Y) by Th7;
hence thesis;
end;
theorem
for a,b being Function of Y,BOOLEAN holds a 'eqv' b=I_el(Y)
implies 'not' a 'eqv' 'not' b=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
assume (a 'eqv' b)=I_el(Y);
then a = b by BVFUNC_1:17;
hence thesis by BVFUNC_1:17;
end;
theorem
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a '&' c) 'eqv' (b '&' d))=I_el(Y)
proof
let a,b,c,d be Function of Y,BOOLEAN;
assume a 'eqv' b=I_el(Y) & c 'eqv' d=I_el(Y);
then a = b & c = d by BVFUNC_1:17;
hence thesis by BVFUNC_1:17;
end;
theorem
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a 'imp' c) 'eqv' (b 'imp' d))=I_el(Y)
proof
let a,b,c,d be Function of Y,BOOLEAN;
assume a 'eqv' b=I_el(Y) & c 'eqv' d=I_el(Y);
then a = b & c = d by BVFUNC_1:17;
hence thesis by BVFUNC_1:17;
end;
theorem
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a 'or' c) 'eqv' (b 'or' d))=I_el(Y)
proof
let a,b,c,d be Function of Y,BOOLEAN;
assume a 'eqv' b=I_el(Y) & c 'eqv' d=I_el(Y);
then a = b & c = d by BVFUNC_1:17;
hence thesis by BVFUNC_1:17;
end;
theorem
for a,b,c,d being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y
) & (c 'eqv' d)=I_el(Y) implies ((a 'eqv' c) 'eqv' (b 'eqv' d))=I_el(Y)
proof
let a,b,c,d be Function of Y,BOOLEAN;
assume a 'eqv' b=I_el(Y) & c 'eqv' d=I_el(Y);
then a = b & c = d by BVFUNC_1:17;
hence thesis by BVFUNC_1:17;
end;
begin
::Chap. 2 Predicate Calculus
theorem
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y
holds All(a 'eqv' b,PA,G) = All(a 'imp' b,PA,G) '&' All(b 'imp' a,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;
All(a 'eqv' b,PA,G).z =(All((a 'imp' b) '&' (b 'imp' a),PA,G)).z by Th7
.=(All(a 'imp' b,PA,G) '&' All(b 'imp' a,PA,G)).z by BVFUNC_1:39;
hence thesis;
end;
theorem
for a being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA,PB being a_partition of Y holds All(a,PA,G) '<' Ex(a,PB,G)
proof
let a be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA,PB be a_partition of Y;
All(a,PA,G) '<' a & a '<' Ex(a,PB,G) by BVFUNC_2:11,12;
hence thesis by BVFUNC_1:15;
end;
theorem
for a,u being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y st a 'imp' u = I_el(Y) holds All(a,PA,
G) 'imp' u = I_el(Y)
proof
let a,u be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
assume
A1: a 'imp' u = I_el(Y);
for x being Element of Y holds (All(a,PA,G) 'imp' u).x = TRUE
proof
let x be Element of Y;
(a 'imp' u).x = TRUE by A1,BVFUNC_1:def 11;
then
A2: 'not' a.x 'or' u.x = TRUE by BVFUNC_1:def 8;
A3: 'not' a.x=TRUE or 'not' a.x=FALSE by XBOOLEAN:def 3;
now
per cases by A2,A3;
case
A4: 'not' a.x=TRUE;
x in EqClass(x,CompF(PA,G)) by EQREL_1:def 6;
then B_INF(a,CompF(PA,G)).x = FALSE by A4,BVFUNC_1:def 16;
then (All(a,PA,G) 'imp' u).x =TRUE 'or' u.x by BVFUNC_1:def 8
.=TRUE;
hence thesis;
end;
case
u.x=TRUE;
then (All(a,PA,G) 'imp' u).x ='not' All(a,PA,G).x 'or' TRUE by
BVFUNC_1:def 8
.=TRUE;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA being a_partition of Y st u is_independent_of PA,G holds Ex(u,PA,G) '<'
u
proof
let u be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
assume u is_independent_of PA,G;
then
A1: u is_dependent_of CompF(PA,G);
for z being Element of Y holds (Ex(u,PA,G) 'imp' u).z = TRUE
proof
let z be Element of Y;
A2: (Ex(u,PA,G) 'imp' u).z ='not' Ex(u,PA,G).z 'or' u.z by BVFUNC_1:def 8;
A3: z in EqClass(z,CompF(PA,G)) & EqClass(z,CompF(PA,G)) in CompF(PA,G) by
EQREL_1:def 6;
now
per cases by XBOOLEAN:def 3;
case
u.z=TRUE;
hence thesis by A2;
end;
case
u.z=FALSE;
then
not ex x1 being Element of Y st x1 in EqClass(z,CompF(PA,G)) & u.
x1=TRUE by A1,A3;
then B_SUP(u,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
hence thesis by A2;
end;
end;
hence thesis;
end;
then Ex(u,PA,G) 'imp' u = I_el(Y) by BVFUNC_1:def 11;
hence thesis by BVFUNC_1:16;
end;
theorem
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA being a_partition of Y st u is_independent_of PA,G holds u '<' All(u,PA,
G)
proof
let u be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
assume u is_independent_of PA,G;
then
A1: u is_dependent_of CompF(PA,G);
for z being Element of Y holds (u 'imp' All(u,PA,G)).z = TRUE
proof
let z be Element of Y;
A2: (u 'imp' All(u,PA,G)).z ='not' u.z 'or' All(u,PA,G).z by BVFUNC_1:def 8;
A3: z in EqClass(z,CompF(PA,G)) & EqClass(z,CompF(PA,G)) in CompF(PA,G) by
EQREL_1:def 6;
now
per cases by XBOOLEAN:def 3;
case
u.z=FALSE;
hence thesis by A2;
end;
case
u.z=TRUE;
then
for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds u.x
=TRUE by A1,A3;
then All(u,PA,G).z=TRUE by BVFUNC_1:def 16;
hence thesis by A2;
end;
end;
hence thesis;
end;
then u 'imp' All(u,PA,G) = I_el(Y) by BVFUNC_1:def 11;
hence thesis by BVFUNC_1:16;
end;
theorem
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA,PB being a_partition of Y st u is_independent_of PB,G holds All(u,PA,G)
'<' All(u,PB,G)
proof
let u be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA,PB be a_partition of Y;
assume u is_independent_of PB,G;
then
A1: u is_dependent_of CompF(PB,G);
for z being Element of Y holds (All(u,PA,G) 'imp' All(u,PB,G)).z = TRUE
proof
let z be Element of Y;
A2: z in EqClass(z,CompF(PB,G)) & EqClass(z,CompF(PB,G)) in CompF(PB,G) by
EQREL_1:def 6;
A3: (All(u,PA,G) 'imp' All(u,PB,G)).z ='not' All(u,PA,G).z 'or' All(u,PB,G
).z by BVFUNC_1:def 8;
A4: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
now
per cases by XBOOLEAN:def 3;
case
All(u,PA,G).z=FALSE;
hence thesis by A3;
end;
case
All(u,PA,G).z=TRUE;
then u.z=TRUE by A4,BVFUNC_1:def 16;
then
for x being Element of Y st x in EqClass(z,CompF(PB,G)) holds u.x
=TRUE by A1,A2;
then All(u,PB,G).z=TRUE by BVFUNC_1:def 16;
hence thesis by A3;
end;
end;
hence thesis;
end;
then All(u,PA,G) 'imp' All(u,PB,G) = I_el(Y) by BVFUNC_1:def 11;
hence thesis by BVFUNC_1:16;
end;
theorem
for u being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), PA,PB being a_partition of Y st u is_independent_of PA,G holds Ex(u,PA,G)
'<' Ex(u,PB,G)
proof
let u be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA,PB be a_partition of Y;
assume u is_independent_of PA,G;
then
A1: u is_dependent_of CompF(PA,G);
for z being Element of Y holds (Ex(u,PA,G) 'imp' Ex(u,PB,G)).z = TRUE
proof
let z be Element of Y;
A2: z in EqClass(z,CompF(PB,G)) by EQREL_1:def 6;
A3: (Ex(u,PA,G) 'imp' Ex(u,PB,G)).z ='not' Ex(u,PA,G).z 'or' Ex(u,PB,G).z
by BVFUNC_1:def 8;
A4: z in EqClass(z,CompF(PA,G)) & EqClass(z,CompF(PA,G)) in CompF(PA,G) by
EQREL_1:def 6;
now
per cases by XBOOLEAN:def 3;
case
Ex(u,PB,G).z=TRUE;
hence thesis by A3;
end;
case
Ex(u,PB,G).z=FALSE;
then u.z<>TRUE by A2,BVFUNC_1:def 17;
then
not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & u.x
=TRUE) by A1,A4;
then (B_SUP(u,CompF(PA,G))).z = FALSE by BVFUNC_1:def 17;
hence thesis by A3;
end;
end;
hence thesis;
end;
then Ex(u,PA,G) 'imp' Ex(u,PB,G) = I_el(Y) by BVFUNC_1:def 11;
hence thesis by BVFUNC_1:16;
end;
theorem
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds All(a 'eqv' b,PA,G) '<' All(a,PA
,G) 'eqv' All(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
A1: (All(a 'eqv' b,PA,G)).z=TRUE;
A2: (All(a,PA,G) 'eqv' All(b,PA,G)).z ='not'( All(a,PA,G).z 'xor' All(b,PA,G
).z) by BVFUNC_1:def 9
.=((All(a,PA,G).z 'or' 'not' All(b,PA,G).z) '&' 'not' All(a,PA,G).z)
'or' ((All(a,PA,G).z 'or' 'not' All(b,PA,G).z) '&' All(b,PA,G).z) by XBOOLEAN:8
.=('not' All(a,PA,G).z '&' All(a,PA,G).z 'or' 'not' All(a,PA,G).z '&'
'not' All(b,PA,G).z) 'or' (All(b,PA,G).z '&' (All(a,PA,G).z 'or' 'not' All(b,PA
,G).z)) by XBOOLEAN:8
.=(('not' All(a,PA,G).z '&' All(a,PA,G).z) 'or' ('not' All(a,PA,G).z '&'
'not' All(b,PA,G).z)) 'or' ((All(b,PA,G).z '&' All(a,PA,G).z) 'or' (All(b,PA,G)
.z '&' 'not' All(b,PA,G).z)) by XBOOLEAN:8
.=(FALSE 'or' ('not' All(a,PA,G).z '&' 'not' All(b,PA,G).z)) 'or' ((All(
b,PA,G).z '&' All(a,PA,G).z) 'or' (All(b,PA,G).z '&' 'not' All(b,PA,G).z))
by XBOOLEAN:138
.=(('not' All(a,PA,G).z '&' 'not' All(b,PA,G).z)) 'or' ((All(b,PA,G).z
'&' All(a,PA,G).z) 'or' FALSE) by XBOOLEAN:138
.=('not' All(a,PA,G).z '&' 'not' All(b,PA,G).z) 'or' (All(b,PA,G).z '&'
All(a,PA,G).z);
per cases;
suppose
A3: (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;
hence thesis by A2,A3,BVFUNC_1:def 16;
end;
suppose
A4: (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
A5: x1 in EqClass(z,CompF(PA,G)) and
A6: b.x1<>TRUE;
A7: a.x1=TRUE by A4,A5;
(a 'eqv' b).x1 ='not' (a.x1 'xor' b.x1) by BVFUNC_1:def 9
.=FALSE by A6,A7,XBOOLEAN:def 3;
hence thesis by A1,A5,BVFUNC_1:def 16;
end;
suppose
A8: 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 consider x1 being Element of Y such that
A9: x1 in EqClass(z,CompF(PA,G)) and
A10: a.x1<>TRUE;
A11: b.x1=TRUE by A8,A9;
(a 'eqv' b).x1 ='not' (a.x1 'xor' b.x1) by BVFUNC_1:def 9
.=FALSE by A10,A11,XBOOLEAN:def 3;
hence thesis by A1,A9,BVFUNC_1:def 16;
end;
suppose
A12: 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 B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
hence thesis by A2,A12,BVFUNC_1:def 16;
end;
end;
theorem
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds All(a '&' b,PA,G) '<' a '&' All(
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
A1: All(a '&' b,PA,G).z=TRUE;
A2: now
assume 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
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: a.x1<>TRUE;
(a '&' b).x1=TRUE by A1,A3,BVFUNC_1:def 16;
then
A5: a.x1 '&' b.x1=TRUE by MARGREL1:def 20;
a.x1=FALSE by A4,XBOOLEAN:def 3;
hence contradiction by A5;
end;
now
assume 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
A6: x1 in EqClass(z,CompF(PA,G)) and
A7: b.x1<>TRUE;
(a '&' b).x1=TRUE by A1,A6,BVFUNC_1:def 16;
then
A8: a.x1 '&' b.x1=TRUE by MARGREL1:def 20;
b.x1=FALSE by A7,XBOOLEAN:def 3;
hence contradiction by A8;
end;
then
A9: B_INF(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
then a.z=TRUE by A2;
then (a '&' All(b,PA,G)).z =TRUE '&' TRUE by A9,MARGREL1:def 20
.=TRUE;
hence thesis;
end;
theorem
for a,u being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds All(a,PA,G) 'imp' u '<' Ex(a
'imp' u,PA,G)
proof
let a,u 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;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
assume (All(a,PA,G) 'imp' u).z=TRUE;
then
A2: 'not' All(a,PA,G).z 'or' u.z=TRUE by BVFUNC_1:def 8;
A3: ('not' All(a,PA,G).z)=TRUE or ('not' All(a,PA,G).z)=FALSE by XBOOLEAN:def 3
;
now
per cases by A2,A3;
case
'not' All(a,PA,G).z=TRUE;
then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: a.x1<>TRUE by BVFUNC_1:def 16;
now
assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
(a 'imp' u).x=TRUE);
then (a 'imp' u).x1<>TRUE by A4;
then (a 'imp' u).x1=FALSE by XBOOLEAN:def 3;
then
A6: ('not' a.x1) 'or' u.x1=FALSE by BVFUNC_1:def 8;
'not' a.x1=TRUE or 'not' a.x1=FALSE by XBOOLEAN:def 3;
hence contradiction by A5,A6;
end;
hence thesis by BVFUNC_1:def 17;
end;
case
A7: u.z=TRUE;
now
assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
(a 'imp' u).x=TRUE);
then (a 'imp' u).z<>TRUE by A1;
then (a 'imp' u).z=FALSE by XBOOLEAN:def 3;
then ('not' a.z) 'or' u.z=FALSE by BVFUNC_1:def 8;
hence contradiction by A7;
end;
hence thesis by BVFUNC_1:def 17;
end;
end;
hence thesis;
end;
theorem
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds (a 'eqv' b)=I_el(Y) implies (All
(a,PA,G) 'eqv' All(b,PA,G))=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
assume
A1: (a 'eqv' b)=I_el(Y);
then (b 'imp' a)=I_el(Y) by Th10;
then
A2: 'not' b 'or' a = I_el(Y) by Th8;
(a 'imp' b)=I_el(Y) by A1,Th10;
then
A3: 'not' a 'or' b = I_el(Y) by Th8;
for z being Element of Y holds (All(a,PA,G) 'eqv' All(b,PA,G)).z=TRUE
proof
let z be Element of Y;
A4: now
assume that
A5: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a
.x=TRUE and
A6: not(for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds b .x=TRUE);
consider x1 being Element of Y such that
A7: x1 in EqClass(z,CompF(PA,G)) and
A8: b.x1<>TRUE by A6;
A9: a.x1=TRUE by A5,A7;
A10: b.x1=FALSE by A8,XBOOLEAN:def 3;
('not' a 'or' b).x1 =('not' a).x1 'or' b.x1 by BVFUNC_1:def 4
.=FALSE 'or' FALSE by A10,A9,MARGREL1:def 19
.=FALSE;
hence thesis by A3,BVFUNC_1:def 11;
end;
A11: now
assume that
A12: not(for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x= TRUE) and
A13: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b .x= TRUE;
consider x1 being Element of Y such that
A14: x1 in EqClass(z,CompF(PA,G)) and
A15: a.x1<>TRUE by A12;
A16: b.x1=TRUE by A13,A14;
A17: a.x1=FALSE by A15,XBOOLEAN:def 3;
('not' b 'or' a).x1 =('not' b).x1 'or' a.x1 by BVFUNC_1:def 4
.=FALSE 'or' FALSE by A17,A16,MARGREL1:def 19
.=FALSE;
hence thesis by A2,BVFUNC_1:def 11;
end;
All(a,PA,G) 'eqv' All(b,PA,G) =(All(a,PA,G) 'imp' All(b,PA,G)) '&' (
All(b,PA,G) 'imp' All(a,PA,G)) by Th7
.=('not' All(a,PA,G) 'or' All(b,PA,G)) '&' (All(b,PA,G) 'imp' All(a,PA
,G)) by Th8
.=('not' All(a,PA,G) 'or' All(b,PA,G)) '&' ('not' All(b,PA,G) 'or' All
(a,PA,G)) by Th8
.=(('not' All(a,PA,G) 'or' All(b,PA,G)) '&' 'not' All(b,PA,G)) 'or' ((
'not' All(a,PA,G) 'or' All(b,PA,G)) '&' All(a,PA,G)) by BVFUNC_1:12
.=(('not' All(a,PA,G) '&' 'not' All(b,PA,G)) 'or' (All(b,PA,G) '&'
'not' All(b,PA,G))) 'or' (('not' All(a,PA,G) 'or' All(b,PA,G)) '&' All(a,PA,G))
by BVFUNC_1:12
.=(('not' All(a,PA,G) '&' 'not' All(b,PA,G)) 'or' (All(b,PA,G) '&'
'not' All(b,PA,G))) 'or' (('not' All(a,PA,G) '&' All(a,PA,G)) 'or' (All(b,PA,G)
'&' All(a,PA,G))) by BVFUNC_1:12
.=(('not' All(a,PA,G) '&' 'not' All(b,PA,G)) 'or' O_el(Y)) 'or' ((
'not' All(a,PA,G) '&' All(a,PA,G)) 'or' (All(b,PA,G) '&' All(a,PA,G))) by Th5
.=(('not' All(a,PA,G) '&' 'not' All(b,PA,G)) 'or' O_el(Y)) 'or' (O_el(
Y) 'or' (All(b,PA,G) '&' All(a,PA,G))) by Th5
.=('not' All(a,PA,G) '&' 'not' All(b,PA,G)) 'or' (O_el(Y) 'or' (All(b,
PA,G) '&' All(a,PA,G))) by BVFUNC_1:9
.=('not' All(a,PA,G) '&' 'not' All(b,PA,G)) 'or' (All(b,PA,G) '&' All(
a,PA,G)) by BVFUNC_1:9;
then
A18: (All(a,PA,G) 'eqv' All(b,PA,G)).z =('not' All(a,PA,G) '&' 'not' All(b,
PA,G)).z 'or' ( All(b,PA,G) '&' All(a,PA,G)).z by BVFUNC_1:def 4
.=('not' All(a,PA,G)).z '&' ('not' All(b,PA,G)).z 'or' ( All(b,PA,G)
'&' All(a,PA,G)).z by MARGREL1:def 20
.=(('not' All(a,PA,G)).z '&' ('not' All(b,PA,G)).z) 'or' All(b,PA,G).z
'&' All(a,PA,G).z by MARGREL1:def 20
.=('not' All(a,PA,G).z '&' ('not' All(b,PA,G)).z) 'or' ( All(b,PA,G).z
'&' All(a,PA,G).z) by MARGREL1:def 19
.=('not' All(a,PA,G).z '&' 'not' All(b,PA,G).z) 'or' ( All(b,PA,G).z
'&' All(a,PA,G).z) by MARGREL1:def 19;
A19: now
assume that
A20: not(for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x= TRUE) and
A21: not(for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds b .x=TRUE);
B_INF(b,CompF(PA,G)).z = FALSE by A21,BVFUNC_1:def 16;
hence thesis by A18,A20,BVFUNC_1:def 16;
end;
now
assume that
A22: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a
.x=TRUE and
A23: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b .x= TRUE;
B_INF(b,CompF(PA,G)).z = TRUE by A23,BVFUNC_1:def 16;
hence thesis by A18,A22,BVFUNC_1:def 16;
end;
hence thesis by A4,A11,A19;
end;
hence thesis by BVFUNC_1:def 11;
end;
theorem
for a,b being Function of Y,BOOLEAN, G being Subset of
PARTITIONS(Y), PA being a_partition of Y holds (a 'eqv' b)=I_el(Y) implies (Ex(
a,PA,G) 'eqv' Ex(b,PA,G))=I_el(Y)
proof
let a,b be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y);
let PA be a_partition of Y;
assume
A1: (a 'eqv' b)=I_el(Y);
then (b 'imp' a)=I_el(Y) by Th10;
then
A2: 'not' b 'or' a = I_el(Y) by Th8;
(a 'imp' b)=I_el(Y) by A1,Th10;
then
A3: 'not' a 'or' b = I_el(Y) by Th8;
for z being Element of Y holds (Ex(a,PA,G) 'eqv' Ex(b,PA,G)).z=TRUE
proof
let z be Element of Y;
Ex(a,PA,G) 'eqv' Ex(b,PA,G) =(Ex(a,PA,G) 'imp' Ex(b,PA,G)) '&' (Ex(b,
PA,G) 'imp' Ex(a,PA,G)) by Th7
.=('not' Ex(a,PA,G) 'or' Ex(b,PA,G)) '&' (Ex(b,PA,G) 'imp' Ex(a,PA,G))
by Th8
.=('not' Ex(a,PA,G) 'or' Ex(b,PA,G)) '&' ('not' Ex(b,PA,G) 'or' Ex(a,
PA,G)) by Th8
.=(('not' Ex(a,PA,G) 'or' Ex(b,PA,G)) '&' 'not' Ex(b,PA,G)) 'or' ((
'not' Ex(a,PA,G) 'or' Ex(b,PA,G)) '&' Ex(a,PA,G)) by BVFUNC_1:12
.=(('not' Ex(a,PA,G) '&' 'not' Ex(b,PA,G)) 'or' (Ex(b,PA,G) '&' 'not'
Ex(b,PA,G))) 'or' (('not' Ex(a,PA,G) 'or' Ex(b,PA,G)) '&' Ex(a,PA,G)) by
BVFUNC_1:12
.=(('not' Ex(a,PA,G) '&' 'not' Ex(b,PA,G)) 'or' (Ex(b,PA,G) '&' 'not'
Ex(b,PA,G))) 'or' (('not' Ex(a,PA,G) '&' Ex(a,PA,G)) 'or' (Ex(b,PA,G) '&' Ex(a,
PA,G))) by BVFUNC_1:12
.=(('not' Ex(a,PA,G) '&' 'not' Ex(b,PA,G)) 'or' O_el(Y)) 'or' (('not'
Ex(a,PA,G) '&' Ex(a,PA,G)) 'or' (Ex(b,PA,G) '&' Ex(a,PA,G))) by Th5
.=(('not' Ex(a,PA,G) '&' 'not' Ex(b,PA,G)) 'or' O_el(Y)) 'or' (O_el(Y)
'or' (Ex(b,PA,G) '&' Ex(a,PA,G))) by Th5
.=('not' Ex(a,PA,G) '&' 'not' Ex(b,PA,G)) 'or' (O_el(Y) 'or' (Ex(b,PA,
G) '&' Ex(a,PA,G))) by BVFUNC_1:9
.=('not' Ex(a,PA,G) '&' 'not' Ex(b,PA,G)) 'or' (Ex(b,PA,G) '&' Ex(a,PA
,G)) by BVFUNC_1:9;
then
A4: (Ex(a,PA,G) 'eqv' Ex(b,PA,G)).z =('not' Ex(a,PA,G) '&' 'not' Ex(b,PA,G
)).z 'or' ( Ex(b,PA,G) '&' Ex(a,PA,G)).z by BVFUNC_1:def 4
.= ('not' Ex(a,PA,G)).z '&' ('not' Ex(b,PA,G)).z 'or' ( Ex(b,PA,G) '&'
Ex(a,PA,G)).z by MARGREL1:def 20
.= ('not' Ex(a,PA,G)).z '&' ('not' Ex(b,PA,G)).z 'or' (Ex(b,PA,G).z
'&' Ex(a,PA,G).z) by MARGREL1:def 20
.=('not' Ex(a,PA,G).z '&' ('not' Ex(b,PA,G)).z) 'or' ( Ex(b,PA,G).z
'&' Ex(a,PA,G).z) by MARGREL1:def 19
.=('not' Ex(a,PA,G).z '&' 'not' Ex(b,PA,G).z) 'or' ( Ex(b,PA,G).z '&'
Ex(a,PA,G).z) by MARGREL1:def 19;
per cases;
suppose
A5: (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=
TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE;
then B_SUP(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17;
hence thesis by A4,A5,BVFUNC_1:def 17;
end;
suppose
A6: (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=
TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE)
;
then consider x1 being Element of Y such that
A7: x1 in EqClass(z,CompF(PA,G)) and
A8: a.x1=TRUE;
b.x1<>TRUE by A6,A7;
then
A9: b.x1=FALSE by XBOOLEAN:def 3;
('not' a 'or' b).x1 =('not' a).x1 'or' b.x1 by BVFUNC_1:def 4
.=FALSE 'or' FALSE by A8,A9,MARGREL1:def 19
.=FALSE;
hence thesis by A3,BVFUNC_1:def 11;
end;
suppose
A10: not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a
.x=TRUE) & ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE;
then consider x1 being Element of Y such that
A11: x1 in EqClass(z,CompF(PA,G)) and
A12: b.x1=TRUE;
a.x1<>TRUE by A10,A11;
then
A13: a.x1=FALSE by XBOOLEAN:def 3;
('not' b 'or' a).x1 =('not' b).x1 'or' a.x1 by BVFUNC_1:def 4
.=FALSE 'or' FALSE by A12,A13,MARGREL1:def 19
.=FALSE;
hence thesis by A2,BVFUNC_1:def 11;
end;
suppose
A14: not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a
.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=
TRUE);
then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
hence thesis by A4,A14,BVFUNC_1:def 17;
end;
end;
hence thesis by BVFUNC_1:def 11;
end;