:: BVFUNC_4 semantic presentation

K92() is Element of K19(K88())
K88() is set
K19(K88()) is set
K89() is set
K90() is set
K91() is set
K20(K89(),K89()) is set
K19(K20(K89(),K89())) is set
K20(K20(K89(),K89()),K89()) is set
K19(K20(K20(K89(),K89()),K89())) is set
K20(K88(),K88()) is set
K19(K20(K88(),K88())) is set
K20(K20(K88(),K88()),K88()) is set
K19(K20(K20(K88(),K88()),K88())) is set
K20(K90(),K90()) is set
K19(K20(K90(),K90())) is set
K20(K20(K90(),K90()),K90()) is set
K19(K20(K20(K90(),K90()),K90())) is set
K20(K91(),K91()) is set
K19(K20(K91(),K91())) is set
K20(K20(K91(),K91()),K91()) is set
K19(K20(K20(K91(),K91()),K91())) is set
K20(K92(),K92()) is set
K20(K20(K92(),K92()),K92()) is set
K19(K20(K20(K92(),K92()),K92())) is set
K87() is set
K19(K87()) is set
K19(K92()) is set
BOOLEAN is non empty set
1 is non empty set
FALSE is V27() boolean Element of BOOLEAN
K93() is empty V47() Element of K92()
TRUE is V27() boolean Element of BOOLEAN
FALSE is V27() boolean set
TRUE is V27() boolean set
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(a '&' b) 'imp' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Element of Y
((a '&' b) 'imp' G) . PA is V27() boolean Element of BOOLEAN
a 'imp' (b 'imp' G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(a 'imp' (b 'imp' G)) . PA is V27() boolean Element of BOOLEAN
a . PA is V27() boolean Element of BOOLEAN
'not' (a . PA) is V27() boolean Element of BOOLEAN
K100(1,(a . PA)) is set
(b 'imp' G) . PA is V27() boolean Element of BOOLEAN
('not' (a . PA)) 'or' ((b 'imp' G) . PA) is V27() boolean set
'not' ('not' (a . PA)) is V27() boolean set
K100(1,('not' (a . PA))) is set
'not' ((b 'imp' G) . PA) is V27() boolean set
K100(1,((b 'imp' G) . PA)) is set
('not' ('not' (a . PA))) '&' ('not' ((b 'imp' G) . PA)) is V27() boolean set
K97(('not' ('not' (a . PA))),('not' ((b 'imp' G) . PA))) is set
'not' (('not' ('not' (a . PA))) '&' ('not' ((b 'imp' G) . PA))) is V27() boolean set
K100(1,(('not' ('not' (a . PA))) '&' ('not' ((b 'imp' G) . PA)))) is set
b . PA is V27() boolean Element of BOOLEAN
'not' (b . PA) is V27() boolean Element of BOOLEAN
K100(1,(b . PA)) is set
G . PA is V27() boolean Element of BOOLEAN
('not' (b . PA)) 'or' (G . PA) is V27() boolean set
'not' ('not' (b . PA)) is V27() boolean set
K100(1,('not' (b . PA))) is set
'not' (G . PA) is V27() boolean set
K100(1,(G . PA)) is set
('not' ('not' (b . PA))) '&' ('not' (G . PA)) is V27() boolean set
K97(('not' ('not' (b . PA))),('not' (G . PA))) is set
'not' (('not' ('not' (b . PA))) '&' ('not' (G . PA))) is V27() boolean set
K100(1,(('not' ('not' (b . PA))) '&' ('not' (G . PA)))) is set
('not' (a . PA)) 'or' (('not' (b . PA)) 'or' (G . PA)) is V27() boolean set
'not' (('not' (b . PA)) 'or' (G . PA)) is V27() boolean set
K100(1,(('not' (b . PA)) 'or' (G . PA))) is set
('not' ('not' (a . PA))) '&' ('not' (('not' (b . PA)) 'or' (G . PA))) is V27() boolean set
K97(('not' ('not' (a . PA))),('not' (('not' (b . PA)) 'or' (G . PA)))) is set
'not' (('not' ('not' (a . PA))) '&' ('not' (('not' (b . PA)) 'or' (G . PA)))) is V27() boolean set
K100(1,(('not' ('not' (a . PA))) '&' ('not' (('not' (b . PA)) 'or' (G . PA))))) is set
('not' (a . PA)) 'or' ('not' (b . PA)) is V27() boolean set
('not' ('not' (a . PA))) '&' ('not' ('not' (b . PA))) is V27() boolean set
K97(('not' ('not' (a . PA))),('not' ('not' (b . PA)))) is set
'not' (('not' ('not' (a . PA))) '&' ('not' ('not' (b . PA)))) is V27() boolean set
K100(1,(('not' ('not' (a . PA))) '&' ('not' ('not' (b . PA))))) is set
(('not' (a . PA)) 'or' ('not' (b . PA))) 'or' (G . PA) is V27() boolean set
'not' (('not' (a . PA)) 'or' ('not' (b . PA))) is V27() boolean set
K100(1,(('not' (a . PA)) 'or' ('not' (b . PA)))) is set
('not' (('not' (a . PA)) 'or' ('not' (b . PA)))) '&' ('not' (G . PA)) is V27() boolean set
K97(('not' (('not' (a . PA)) 'or' ('not' (b . PA)))),('not' (G . PA))) is set
'not' (('not' (('not' (a . PA)) 'or' ('not' (b . PA)))) '&' ('not' (G . PA))) is V27() boolean set
K100(1,(('not' (('not' (a . PA)) 'or' ('not' (b . PA)))) '&' ('not' (G . PA)))) is set
(a '&' b) . PA is V27() boolean Element of BOOLEAN
'not' ((a '&' b) . PA) is V27() boolean Element of BOOLEAN
K100(1,((a '&' b) . PA)) is set
('not' ((a '&' b) . PA)) 'or' (G . PA) is V27() boolean set
'not' ('not' ((a '&' b) . PA)) is V27() boolean set
K100(1,('not' ((a '&' b) . PA))) is set
('not' ('not' ((a '&' b) . PA))) '&' ('not' (G . PA)) is V27() boolean set
K97(('not' ('not' ((a '&' b) . PA))),('not' (G . PA))) is set
'not' (('not' ('not' ((a '&' b) . PA))) '&' ('not' (G . PA))) is V27() boolean set
K100(1,(('not' ('not' ((a '&' b) . PA))) '&' ('not' (G . PA)))) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' (b 'imp' G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Element of Y
(a 'imp' (b 'imp' G)) . PA is V27() boolean Element of BOOLEAN
a . PA is V27() boolean Element of BOOLEAN
'not' (a . PA) is V27() boolean Element of BOOLEAN
K100(1,(a . PA)) is set
(b 'imp' G) . PA is V27() boolean Element of BOOLEAN
('not' (a . PA)) 'or' ((b 'imp' G) . PA) is V27() boolean set
'not' ('not' (a . PA)) is V27() boolean set
K100(1,('not' (a . PA))) is set
'not' ((b 'imp' G) . PA) is V27() boolean set
K100(1,((b 'imp' G) . PA)) is set
('not' ('not' (a . PA))) '&' ('not' ((b 'imp' G) . PA)) is V27() boolean set
K97(('not' ('not' (a . PA))),('not' ((b 'imp' G) . PA))) is set
'not' (('not' ('not' (a . PA))) '&' ('not' ((b 'imp' G) . PA))) is V27() boolean set
K100(1,(('not' ('not' (a . PA))) '&' ('not' ((b 'imp' G) . PA)))) is set
b . PA is V27() boolean Element of BOOLEAN
'not' (b . PA) is V27() boolean Element of BOOLEAN
K100(1,(b . PA)) is set
G . PA is V27() boolean Element of BOOLEAN
('not' (b . PA)) 'or' (G . PA) is V27() boolean set
'not' ('not' (b . PA)) is V27() boolean set
K100(1,('not' (b . PA))) is set
'not' (G . PA) is V27() boolean set
K100(1,(G . PA)) is set
('not' ('not' (b . PA))) '&' ('not' (G . PA)) is V27() boolean set
K97(('not' ('not' (b . PA))),('not' (G . PA))) is set
'not' (('not' ('not' (b . PA))) '&' ('not' (G . PA))) is V27() boolean set
K100(1,(('not' ('not' (b . PA))) '&' ('not' (G . PA)))) is set
('not' (a . PA)) 'or' (('not' (b . PA)) 'or' (G . PA)) is V27() boolean set
'not' (('not' (b . PA)) 'or' (G . PA)) is V27() boolean set
K100(1,(('not' (b . PA)) 'or' (G . PA))) is set
('not' ('not' (a . PA))) '&' ('not' (('not' (b . PA)) 'or' (G . PA))) is V27() boolean set
K97(('not' ('not' (a . PA))),('not' (('not' (b . PA)) 'or' (G . PA)))) is set
'not' (('not' ('not' (a . PA))) '&' ('not' (('not' (b . PA)) 'or' (G . PA)))) is V27() boolean set
K100(1,(('not' ('not' (a . PA))) '&' ('not' (('not' (b . PA)) 'or' (G . PA))))) is set
('not' (a . PA)) 'or' ('not' (b . PA)) is V27() boolean set
('not' ('not' (a . PA))) '&' ('not' ('not' (b . PA))) is V27() boolean set
K97(('not' ('not' (a . PA))),('not' ('not' (b . PA)))) is set
'not' (('not' ('not' (a . PA))) '&' ('not' ('not' (b . PA)))) is V27() boolean set
K100(1,(('not' ('not' (a . PA))) '&' ('not' ('not' (b . PA))))) is set
(('not' (a . PA)) 'or' ('not' (b . PA))) 'or' (G . PA) is V27() boolean set
'not' (('not' (a . PA)) 'or' ('not' (b . PA))) is V27() boolean set
K100(1,(('not' (a . PA)) 'or' ('not' (b . PA)))) is set
('not' (('not' (a . PA)) 'or' ('not' (b . PA)))) '&' ('not' (G . PA)) is V27() boolean set
K97(('not' (('not' (a . PA)) 'or' ('not' (b . PA)))),('not' (G . PA))) is set
'not' (('not' (('not' (a . PA)) 'or' ('not' (b . PA)))) '&' ('not' (G . PA))) is V27() boolean set
K100(1,(('not' (('not' (a . PA)) 'or' ('not' (b . PA)))) '&' ('not' (G . PA)))) is set
(a '&' b) 'imp' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((a '&' b) 'imp' G) . PA is V27() boolean Element of BOOLEAN
(a '&' b) . PA is V27() boolean Element of BOOLEAN
'not' ((a '&' b) . PA) is V27() boolean Element of BOOLEAN
K100(1,((a '&' b) . PA)) is set
('not' ((a '&' b) . PA)) 'or' (G . PA) is V27() boolean set
'not' ('not' ((a '&' b) . PA)) is V27() boolean set
K100(1,('not' ((a '&' b) . PA))) is set
('not' ('not' ((a '&' b) . PA))) '&' ('not' (G . PA)) is V27() boolean set
K97(('not' ('not' ((a '&' b) . PA))),('not' (G . PA))) is set
'not' (('not' ('not' ((a '&' b) . PA))) '&' ('not' (G . PA))) is V27() boolean set
K100(1,(('not' ('not' ((a '&' b) . PA))) '&' ('not' (G . PA)))) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'or' (a '&' b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of Y
(a 'or' (a '&' b)) . G is set
a . G is set
(a 'or' (a '&' b)) . G is V27() boolean Element of BOOLEAN
a . G is V27() boolean Element of BOOLEAN
(a '&' b) . G is V27() boolean Element of BOOLEAN
(a . G) 'or' ((a '&' b) . G) is V27() boolean set
'not' (a . G) is V27() boolean set
K100(1,(a . G)) is set
'not' ((a '&' b) . G) is V27() boolean set
K100(1,((a '&' b) . G)) is set
('not' (a . G)) '&' ('not' ((a '&' b) . G)) is V27() boolean set
K97(('not' (a . G)),('not' ((a '&' b) . G))) is set
'not' (('not' (a . G)) '&' ('not' ((a '&' b) . G))) is V27() boolean set
K100(1,(('not' (a . G)) '&' ('not' ((a '&' b) . G)))) is set
b . G is V27() boolean Element of BOOLEAN
(a . G) '&' (b . G) is V27() boolean Element of BOOLEAN
K97((a . G),(b . G)) is set
(a . G) 'or' ((a . G) '&' (b . G)) is V27() boolean set
'not' ((a . G) '&' (b . G)) is V27() boolean set
K100(1,((a . G) '&' (b . G))) is set
('not' (a . G)) '&' ('not' ((a . G) '&' (b . G))) is V27() boolean set
K97(('not' (a . G)),('not' ((a . G) '&' (b . G)))) is set
'not' (('not' (a . G)) '&' ('not' ((a . G) '&' (b . G)))) is V27() boolean set
K100(1,(('not' (a . G)) '&' ('not' ((a . G) '&' (b . G))))) is set
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'or' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' (a 'or' b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of Y
(a '&' (a 'or' b)) . G is set
a . G is set
(a '&' (a 'or' b)) . G is V27() boolean Element of BOOLEAN
a . G is V27() boolean Element of BOOLEAN
(a 'or' b) . G is V27() boolean Element of BOOLEAN
(a . G) '&' ((a 'or' b) . G) is V27() boolean Element of BOOLEAN
K97((a . G),((a 'or' b) . G)) is set
b . G is V27() boolean Element of BOOLEAN
(a . G) 'or' (b . G) is V27() boolean set
'not' (a . G) is V27() boolean set
K100(1,(a . G)) is set
'not' (b . G) is V27() boolean set
K100(1,(b . G)) is set
('not' (a . G)) '&' ('not' (b . G)) is V27() boolean set
K97(('not' (a . G)),('not' (b . G))) is set
'not' (('not' (a . G)) '&' ('not' (b . G))) is V27() boolean set
K100(1,(('not' (a . G)) '&' ('not' (b . G)))) is set
(a . G) '&' ((a . G) 'or' (b . G)) is V27() boolean set
K97((a . G),((a . G) 'or' (b . G))) is set
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
O_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' ('not' a) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Element of Y
(a '&' ('not' a)) . b is set
(O_el Y) . b is set
(a '&' ('not' a)) . b is V27() boolean Element of BOOLEAN
a . b is V27() boolean Element of BOOLEAN
('not' a) . b is V27() boolean Element of BOOLEAN
(a . b) '&' (('not' a) . b) is V27() boolean Element of BOOLEAN
K97((a . b),(('not' a) . b)) is set
'not' (a . b) is V27() boolean Element of BOOLEAN
K100(1,(a . b)) is set
(a . b) '&' ('not' (a . b)) is V27() boolean Element of BOOLEAN
K97((a . b),('not' (a . b))) is set
(O_el Y) . b is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'or' ('not' a) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Element of Y
(a 'or' ('not' a)) . b is set
(I_el Y) . b is set
(a 'or' ('not' a)) . b is V27() boolean Element of BOOLEAN
a . b is V27() boolean Element of BOOLEAN
('not' a) . b is V27() boolean Element of BOOLEAN
(a . b) 'or' (('not' a) . b) is V27() boolean set
'not' (a . b) is V27() boolean set
K100(1,(a . b)) is set
'not' (('not' a) . b) is V27() boolean set
K100(1,(('not' a) . b)) is set
('not' (a . b)) '&' ('not' (('not' a) . b)) is V27() boolean set
K97(('not' (a . b)),('not' (('not' a) . b))) is set
'not' (('not' (a . b)) '&' ('not' (('not' a) . b))) is V27() boolean set
K100(1,(('not' (a . b)) '&' ('not' (('not' a) . b)))) is set
'not' (a . b) is V27() boolean Element of BOOLEAN
(a . b) 'or' ('not' (a . b)) is V27() boolean set
'not' ('not' (a . b)) is V27() boolean set
K100(1,('not' (a . b))) is set
('not' (a . b)) '&' ('not' ('not' (a . b))) is V27() boolean set
K97(('not' (a . b)),('not' ('not' (a . b)))) is set
'not' (('not' (a . b)) '&' ('not' ('not' (a . b)))) is V27() boolean set
K100(1,(('not' (a . b)) '&' ('not' ('not' (a . b))))) is set
(I_el Y) . b is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(a 'imp' b) '&' (b 'imp' a) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of Y
(a 'eqv' b) . G is set
((a 'imp' b) '&' (b 'imp' a)) . G is set
(a 'eqv' b) . G is V27() boolean Element of BOOLEAN
a . G is V27() boolean Element of BOOLEAN
b . G is V27() boolean Element of BOOLEAN
(a . G) <=> (b . G) is V27() boolean Element of BOOLEAN
(a . G) 'xor' (b . G) is V27() boolean set
(a . G) <=> (b . G) is V27() boolean set
'not' ((a . G) <=> (b . G)) is V27() boolean set
K100(1,((a . G) <=> (b . G))) is set
'not' ((a . G) 'xor' (b . G)) is V27() boolean set
K100(1,((a . G) 'xor' (b . G))) is set
(a . G) => (b . G) is V27() boolean set
'not' (a . G) is V27() boolean set
K100(1,(a . G)) is set
('not' (a . G)) 'or' (b . G) is V27() boolean set
'not' ('not' (a . G)) is V27() boolean set
K100(1,('not' (a . G))) is set
'not' (b . G) is V27() boolean set
K100(1,(b . G)) is set
('not' ('not' (a . G))) '&' ('not' (b . G)) is V27() boolean set
K97(('not' ('not' (a . G))),('not' (b . G))) is set
'not' (('not' ('not' (a . G))) '&' ('not' (b . G))) is V27() boolean set
K100(1,(('not' ('not' (a . G))) '&' ('not' (b . G)))) is set
(b . G) => (a . G) is V27() boolean set
('not' (b . G)) 'or' (a . G) is V27() boolean set
'not' ('not' (b . G)) is V27() boolean set
K100(1,('not' (b . G))) is set
('not' ('not' (b . G))) '&' ('not' (a . G)) is V27() boolean set
K97(('not' ('not' (b . G))),('not' (a . G))) is set
'not' (('not' ('not' (b . G))) '&' ('not' (a . G))) is V27() boolean set
K100(1,(('not' ('not' (b . G))) '&' ('not' (a . G)))) is set
((a . G) => (b . G)) '&' ((b . G) => (a . G)) is V27() boolean set
K97(((a . G) => (b . G)),((b . G) => (a . G))) is set
(a 'imp' b) . G is V27() boolean Element of BOOLEAN
((a 'imp' b) . G) '&' ((b . G) => (a . G)) is V27() boolean set
K97(((a 'imp' b) . G),((b . G) => (a . G))) is set
(b 'imp' a) . G is V27() boolean Element of BOOLEAN
((a 'imp' b) . G) '&' ((b 'imp' a) . G) is V27() boolean Element of BOOLEAN
K97(((a 'imp' b) . G),((b 'imp' a) . G)) is set
((a 'imp' b) '&' (b 'imp' a)) . G is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' a) 'or' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of Y
(a 'imp' b) . G is set
(('not' a) 'or' b) . G is set
(a 'imp' b) . G is V27() boolean Element of BOOLEAN
a . G is V27() boolean Element of BOOLEAN
b . G is V27() boolean Element of BOOLEAN
(a . G) => (b . G) is V27() boolean set
'not' (a . G) is V27() boolean set
K100(1,(a . G)) is set
('not' (a . G)) 'or' (b . G) is V27() boolean set
'not' ('not' (a . G)) is V27() boolean set
K100(1,('not' (a . G))) is set
'not' (b . G) is V27() boolean set
K100(1,(b . G)) is set
('not' ('not' (a . G))) '&' ('not' (b . G)) is V27() boolean set
K97(('not' ('not' (a . G))),('not' (b . G))) is set
'not' (('not' ('not' (a . G))) '&' ('not' (b . G))) is V27() boolean set
K100(1,(('not' ('not' (a . G))) '&' ('not' (b . G)))) is set
'not' (a . G) is V27() boolean Element of BOOLEAN
('not' (a . G)) 'or' (b . G) is V27() boolean set
'not' ('not' (a . G)) is V27() boolean set
K100(1,('not' (a . G))) is set
('not' ('not' (a . G))) '&' ('not' (b . G)) is V27() boolean set
K97(('not' ('not' (a . G))),('not' (b . G))) is set
'not' (('not' ('not' (a . G))) '&' ('not' (b . G))) is V27() boolean set
K100(1,(('not' ('not' (a . G))) '&' ('not' (b . G)))) is set
('not' a) . G is V27() boolean Element of BOOLEAN
(('not' a) . G) 'or' (b . G) is V27() boolean set
'not' (('not' a) . G) is V27() boolean set
K100(1,(('not' a) . G)) is set
('not' (('not' a) . G)) '&' ('not' (b . G)) is V27() boolean set
K97(('not' (('not' a) . G)),('not' (b . G))) is set
'not' (('not' (('not' a) . G)) '&' ('not' (b . G))) is V27() boolean set
K100(1,(('not' (('not' a) . G)) '&' ('not' (b . G)))) is set
(('not' a) 'or' b) . G is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'xor' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' a) '&' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' ('not' b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' a) '&' b) 'or' (a '&' ('not' b)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of Y
(a 'xor' b) . G is set
((('not' a) '&' b) 'or' (a '&' ('not' b))) . G is set
(a 'xor' b) . G is V27() boolean Element of BOOLEAN
a . G is V27() boolean Element of BOOLEAN
b . G is V27() boolean Element of BOOLEAN
(a . G) 'xor' (b . G) is V27() boolean set
(a . G) <=> (b . G) is V27() boolean set
'not' ((a . G) 'xor' (b . G)) is V27() boolean set
K100(1,((a . G) 'xor' (b . G))) is set
(a . G) => (b . G) is V27() boolean set
'not' (a . G) is V27() boolean set
K100(1,(a . G)) is set
('not' (a . G)) 'or' (b . G) is V27() boolean set
'not' ('not' (a . G)) is V27() boolean set
K100(1,('not' (a . G))) is set
'not' (b . G) is V27() boolean set
K100(1,(b . G)) is set
('not' ('not' (a . G))) '&' ('not' (b . G)) is V27() boolean set
K97(('not' ('not' (a . G))),('not' (b . G))) is set
'not' (('not' ('not' (a . G))) '&' ('not' (b . G))) is V27() boolean set
K100(1,(('not' ('not' (a . G))) '&' ('not' (b . G)))) is set
(b . G) => (a . G) is V27() boolean set
('not' (b . G)) 'or' (a . G) is V27() boolean set
'not' ('not' (b . G)) is V27() boolean set
K100(1,('not' (b . G))) is set
('not' ('not' (b . G))) '&' ('not' (a . G)) is V27() boolean set
K97(('not' ('not' (b . G))),('not' (a . G))) is set
'not' (('not' ('not' (b . G))) '&' ('not' (a . G))) is V27() boolean set
K100(1,(('not' ('not' (b . G))) '&' ('not' (a . G)))) is set
((a . G) => (b . G)) '&' ((b . G) => (a . G)) is V27() boolean set
K97(((a . G) => (b . G)),((b . G) => (a . G))) is set
'not' ((a . G) <=> (b . G)) is V27() boolean set
K100(1,((a . G) <=> (b . G))) is set
'not' (a . G) is V27() boolean Element of BOOLEAN
('not' (a . G)) '&' (b . G) is V27() boolean Element of BOOLEAN
K97(('not' (a . G)),(b . G)) is set
'not' (b . G) is V27() boolean Element of BOOLEAN
(a . G) '&' ('not' (b . G)) is V27() boolean Element of BOOLEAN
K97((a . G),('not' (b . G))) is set
(('not' (a . G)) '&' (b . G)) 'or' ((a . G) '&' ('not' (b . G))) is V27() boolean set
'not' (('not' (a . G)) '&' (b . G)) is V27() boolean set
K100(1,(('not' (a . G)) '&' (b . G))) is set
'not' ((a . G) '&' ('not' (b . G))) is V27() boolean set
K100(1,((a . G) '&' ('not' (b . G)))) is set
('not' (('not' (a . G)) '&' (b . G))) '&' ('not' ((a . G) '&' ('not' (b . G)))) is V27() boolean set
K97(('not' (('not' (a . G)) '&' (b . G))),('not' ((a . G) '&' ('not' (b . G))))) is set
'not' (('not' (('not' (a . G)) '&' (b . G))) '&' ('not' ((a . G) '&' ('not' (b . G))))) is V27() boolean set
K100(1,(('not' (('not' (a . G)) '&' (b . G))) '&' ('not' ((a . G) '&' ('not' (b . G)))))) is set
('not' b) . G is V27() boolean Element of BOOLEAN
(a . G) '&' (('not' b) . G) is V27() boolean Element of BOOLEAN
K97((a . G),(('not' b) . G)) is set
(('not' (a . G)) '&' (b . G)) 'or' ((a . G) '&' (('not' b) . G)) is V27() boolean set
'not' ((a . G) '&' (('not' b) . G)) is V27() boolean set
K100(1,((a . G) '&' (('not' b) . G))) is set
('not' (('not' (a . G)) '&' (b . G))) '&' ('not' ((a . G) '&' (('not' b) . G))) is V27() boolean set
K97(('not' (('not' (a . G)) '&' (b . G))),('not' ((a . G) '&' (('not' b) . G)))) is set
'not' (('not' (('not' (a . G)) '&' (b . G))) '&' ('not' ((a . G) '&' (('not' b) . G)))) is V27() boolean set
K100(1,(('not' (('not' (a . G)) '&' (b . G))) '&' ('not' ((a . G) '&' (('not' b) . G))))) is set
('not' a) . G is V27() boolean Element of BOOLEAN
(('not' a) . G) '&' (b . G) is V27() boolean Element of BOOLEAN
K97((('not' a) . G),(b . G)) is set
((('not' a) . G) '&' (b . G)) 'or' ((a . G) '&' (('not' b) . G)) is V27() boolean set
'not' ((('not' a) . G) '&' (b . G)) is V27() boolean set
K100(1,((('not' a) . G) '&' (b . G))) is set
('not' ((('not' a) . G) '&' (b . G))) '&' ('not' ((a . G) '&' (('not' b) . G))) is V27() boolean set
K97(('not' ((('not' a) . G) '&' (b . G))),('not' ((a . G) '&' (('not' b) . G)))) is set
'not' (('not' ((('not' a) . G) '&' (b . G))) '&' ('not' ((a . G) '&' (('not' b) . G)))) is V27() boolean set
K100(1,(('not' ((('not' a) . G) '&' (b . G))) '&' ('not' ((a . G) '&' (('not' b) . G))))) is set
(('not' a) '&' b) . G is V27() boolean Element of BOOLEAN
((('not' a) '&' b) . G) 'or' ((a . G) '&' (('not' b) . G)) is V27() boolean set
'not' ((('not' a) '&' b) . G) is V27() boolean set
K100(1,((('not' a) '&' b) . G)) is set
('not' ((('not' a) '&' b) . G)) '&' ('not' ((a . G) '&' (('not' b) . G))) is V27() boolean set
K97(('not' ((('not' a) '&' b) . G)),('not' ((a . G) '&' (('not' b) . G)))) is set
'not' (('not' ((('not' a) '&' b) . G)) '&' ('not' ((a . G) '&' (('not' b) . G)))) is V27() boolean set
K100(1,(('not' ((('not' a) '&' b) . G)) '&' ('not' ((a . G) '&' (('not' b) . G))))) is set
(a '&' ('not' b)) . G is V27() boolean Element of BOOLEAN
((('not' a) '&' b) . G) 'or' ((a '&' ('not' b)) . G) is V27() boolean set
'not' ((a '&' ('not' b)) . G) is V27() boolean set
K100(1,((a '&' ('not' b)) . G)) is set
('not' ((('not' a) '&' b) . G)) '&' ('not' ((a '&' ('not' b)) . G)) is V27() boolean set
K97(('not' ((('not' a) '&' b) . G)),('not' ((a '&' ('not' b)) . G))) is set
'not' (('not' ((('not' a) '&' b) . G)) '&' ('not' ((a '&' ('not' b)) . G))) is V27() boolean set
K100(1,(('not' ((('not' a) '&' b) . G)) '&' ('not' ((a '&' ('not' b)) . G)))) is set
((('not' a) '&' b) 'or' (a '&' ('not' b))) . G is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(I_el Y) '&' (I_el Y) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' a) 'eqv' ('not' b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G 'eqv' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b '&' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(a '&' G) 'eqv' (b '&' PA) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G 'eqv' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(a 'imp' G) 'eqv' (b 'imp' PA) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G 'eqv' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'or' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'or' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(a 'or' G) 'eqv' (b 'or' PA) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G 'eqv' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' G is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'eqv' PA is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(a 'eqv' G) 'eqv' (b 'eqv' PA) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of K19((PARTITIONS Y))
PA is a_partition of Y
All ((a 'eqv' b),PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,G) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
G \ {PA} is Element of K19((PARTITIONS Y))
'/\' (G \ {PA}) is a_partition of Y
B_INF ((a 'eqv' b),(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All ((a 'imp' b),PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_INF ((a 'imp' b),(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All ((b 'imp' a),PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_INF ((b 'imp' a),(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
(All ((a 'eqv' b),PA,G)) . z is set
((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z is set
(All ((a 'eqv' b),PA,G)) . z is V27() boolean Element of BOOLEAN
(a 'imp' b) '&' (b 'imp' a) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All (((a 'imp' b) '&' (b 'imp' a)),PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_INF (((a 'imp' b) '&' (b 'imp' a)),(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (((a 'imp' b) '&' (b 'imp' a)),PA,G)) . z is V27() boolean Element of BOOLEAN
((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Element of K19((PARTITIONS Y))
G is a_partition of Y
All (a,G,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (G,b) is a_partition of Y
{G} is non empty Element of K19((PARTITIONS Y))
b \ {G} is Element of K19((PARTITIONS Y))
'/\' (b \ {G}) is a_partition of Y
B_INF (a,(CompF (G,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is a_partition of Y
Ex (a,PA,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,b) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
b \ {PA} is Element of K19((PARTITIONS Y))
'/\' (b \ {PA}) is a_partition of Y
B_SUP (a,(CompF (PA,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of K19((PARTITIONS Y))
PA is a_partition of Y
All (a,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,G) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
G \ {PA} is Element of K19((PARTITIONS Y))
'/\' (G \ {PA}) is a_partition of Y
B_INF (a,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (a,PA,G)) 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
((All (a,PA,G)) 'imp' b) . z is V27() boolean Element of BOOLEAN
(a 'imp' b) . z is V27() boolean Element of BOOLEAN
a . z is V27() boolean Element of BOOLEAN
'not' (a . z) is V27() boolean Element of BOOLEAN
K100(1,(a . z)) is set
b . z is V27() boolean Element of BOOLEAN
('not' (a . z)) 'or' (b . z) is V27() boolean set
'not' ('not' (a . z)) is V27() boolean set
K100(1,('not' (a . z))) is set
'not' (b . z) is V27() boolean set
K100(1,(b . z)) is set
('not' ('not' (a . z))) '&' ('not' (b . z)) is V27() boolean set
K97(('not' ('not' (a . z))),('not' (b . z))) is set
'not' (('not' ('not' (a . z))) '&' ('not' (b . z))) is V27() boolean set
K100(1,(('not' ('not' (a . z))) '&' ('not' (b . z)))) is set
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
(B_INF (a,(CompF (PA,G)))) . z is V27() boolean Element of BOOLEAN
TRUE 'or' (b . z) is V27() boolean set
'not' TRUE is V27() boolean set
K100(1,TRUE) is set
('not' TRUE) '&' ('not' (b . z)) is V27() boolean set
K97(('not' TRUE),('not' (b . z))) is set
'not' (('not' TRUE) '&' ('not' (b . z))) is V27() boolean set
K100(1,(('not' TRUE) '&' ('not' (b . z)))) is set
(All (a,PA,G)) . z is V27() boolean Element of BOOLEAN
'not' ((All (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K100(1,((All (a,PA,G)) . z)) is set
('not' ((All (a,PA,G)) . z)) 'or' TRUE is V27() boolean set
'not' ('not' ((All (a,PA,G)) . z)) is V27() boolean set
K100(1,('not' ((All (a,PA,G)) . z))) is set
'not' TRUE is V27() boolean set
K100(1,TRUE) is set
('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' TRUE) is V27() boolean set
K97(('not' ('not' ((All (a,PA,G)) . z))),('not' TRUE)) is set
'not' (('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' TRUE)) is V27() boolean set
K100(1,(('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' TRUE))) is set
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Element of K19((PARTITIONS Y))
G is a_partition of Y
Ex (a,G,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (G,b) is a_partition of Y
{G} is non empty Element of K19((PARTITIONS Y))
b \ {G} is Element of K19((PARTITIONS Y))
'/\' (b \ {G}) is a_partition of Y
B_SUP (a,(CompF (G,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(Ex (a,G,b)) 'imp' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Element of Y
((Ex (a,G,b)) 'imp' a) . PA is V27() boolean Element of BOOLEAN
(Ex (a,G,b)) . PA is V27() boolean Element of BOOLEAN
'not' ((Ex (a,G,b)) . PA) is V27() boolean Element of BOOLEAN
K100(1,((Ex (a,G,b)) . PA)) is set
a . PA is V27() boolean Element of BOOLEAN
('not' ((Ex (a,G,b)) . PA)) 'or' (a . PA) is V27() boolean set
'not' ('not' ((Ex (a,G,b)) . PA)) is V27() boolean set
K100(1,('not' ((Ex (a,G,b)) . PA))) is set
'not' (a . PA) is V27() boolean set
K100(1,(a . PA)) is set
('not' ('not' ((Ex (a,G,b)) . PA))) '&' ('not' (a . PA)) is V27() boolean set
K97(('not' ('not' ((Ex (a,G,b)) . PA))),('not' (a . PA))) is set
'not' (('not' ('not' ((Ex (a,G,b)) . PA))) '&' ('not' (a . PA))) is V27() boolean set
K100(1,(('not' ('not' ((Ex (a,G,b)) . PA))) '&' ('not' (a . PA)))) is set
EqClass (PA,(CompF (G,b))) is Element of CompF (G,b)
z is Element of Y
a . z is V27() boolean Element of BOOLEAN
(B_SUP (a,(CompF (G,b)))) . PA is V27() boolean Element of BOOLEAN
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Element of K19((PARTITIONS Y))
G is a_partition of Y
All (a,G,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (G,b) is a_partition of Y
{G} is non empty Element of K19((PARTITIONS Y))
b \ {G} is Element of K19((PARTITIONS Y))
'/\' (b \ {G}) is a_partition of Y
B_INF (a,(CompF (G,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' (All (a,G,b)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is Element of Y
(a 'imp' (All (a,G,b))) . PA is V27() boolean Element of BOOLEAN
a . PA is V27() boolean Element of BOOLEAN
'not' (a . PA) is V27() boolean Element of BOOLEAN
K100(1,(a . PA)) is set
(All (a,G,b)) . PA is V27() boolean Element of BOOLEAN
('not' (a . PA)) 'or' ((All (a,G,b)) . PA) is V27() boolean set
'not' ('not' (a . PA)) is V27() boolean set
K100(1,('not' (a . PA))) is set
'not' ((All (a,G,b)) . PA) is V27() boolean set
K100(1,((All (a,G,b)) . PA)) is set
('not' ('not' (a . PA))) '&' ('not' ((All (a,G,b)) . PA)) is V27() boolean set
K97(('not' ('not' (a . PA))),('not' ((All (a,G,b)) . PA))) is set
'not' (('not' ('not' (a . PA))) '&' ('not' ((All (a,G,b)) . PA))) is V27() boolean set
K100(1,(('not' ('not' (a . PA))) '&' ('not' ((All (a,G,b)) . PA)))) is set
EqClass (PA,(CompF (G,b))) is Element of CompF (G,b)
z is Element of Y
a . z is V27() boolean Element of BOOLEAN
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Element of K19((PARTITIONS Y))
PA is a_partition of Y
G is a_partition of Y
All (a,G,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (G,b) is a_partition of Y
{G} is non empty Element of K19((PARTITIONS Y))
b \ {G} is Element of K19((PARTITIONS Y))
'/\' (b \ {G}) is a_partition of Y
B_INF (a,(CompF (G,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All (a,PA,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,b) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
b \ {PA} is Element of K19((PARTITIONS Y))
'/\' (b \ {PA}) is a_partition of Y
B_INF (a,(CompF (PA,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (a,G,b)) 'imp' (All (a,PA,b)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
((All (a,G,b)) 'imp' (All (a,PA,b))) . z is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,b))) is Element of CompF (PA,b)
(All (a,G,b)) . z is V27() boolean Element of BOOLEAN
'not' ((All (a,G,b)) . z) is V27() boolean Element of BOOLEAN
K100(1,((All (a,G,b)) . z)) is set
(All (a,PA,b)) . z is V27() boolean Element of BOOLEAN
('not' ((All (a,G,b)) . z)) 'or' ((All (a,PA,b)) . z) is V27() boolean set
'not' ('not' ((All (a,G,b)) . z)) is V27() boolean set
K100(1,('not' ((All (a,G,b)) . z))) is set
'not' ((All (a,PA,b)) . z) is V27() boolean set
K100(1,((All (a,PA,b)) . z)) is set
('not' ('not' ((All (a,G,b)) . z))) '&' ('not' ((All (a,PA,b)) . z)) is V27() boolean set
K97(('not' ('not' ((All (a,G,b)) . z))),('not' ((All (a,PA,b)) . z))) is set
'not' (('not' ('not' ((All (a,G,b)) . z))) '&' ('not' ((All (a,PA,b)) . z))) is V27() boolean set
K100(1,(('not' ('not' ((All (a,G,b)) . z))) '&' ('not' ((All (a,PA,b)) . z)))) is set
EqClass (z,(CompF (G,b))) is Element of CompF (G,b)
a . z is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Element of K19((PARTITIONS Y))
G is a_partition of Y
Ex (a,G,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (G,b) is a_partition of Y
{G} is non empty Element of K19((PARTITIONS Y))
b \ {G} is Element of K19((PARTITIONS Y))
'/\' (b \ {G}) is a_partition of Y
B_SUP (a,(CompF (G,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
PA is a_partition of Y
Ex (a,PA,b) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,b) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
b \ {PA} is Element of K19((PARTITIONS Y))
'/\' (b \ {PA}) is a_partition of Y
B_SUP (a,(CompF (PA,b))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(Ex (a,G,b)) 'imp' (Ex (a,PA,b)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
((Ex (a,G,b)) 'imp' (Ex (a,PA,b))) . z is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,b))) is Element of CompF (PA,b)
(Ex (a,G,b)) . z is V27() boolean Element of BOOLEAN
'not' ((Ex (a,G,b)) . z) is V27() boolean Element of BOOLEAN
K100(1,((Ex (a,G,b)) . z)) is set
(Ex (a,PA,b)) . z is V27() boolean Element of BOOLEAN
('not' ((Ex (a,G,b)) . z)) 'or' ((Ex (a,PA,b)) . z) is V27() boolean set
'not' ('not' ((Ex (a,G,b)) . z)) is V27() boolean set
K100(1,('not' ((Ex (a,G,b)) . z))) is set
'not' ((Ex (a,PA,b)) . z) is V27() boolean set
K100(1,((Ex (a,PA,b)) . z)) is set
('not' ('not' ((Ex (a,G,b)) . z))) '&' ('not' ((Ex (a,PA,b)) . z)) is V27() boolean set
K97(('not' ('not' ((Ex (a,G,b)) . z))),('not' ((Ex (a,PA,b)) . z))) is set
'not' (('not' ('not' ((Ex (a,G,b)) . z))) '&' ('not' ((Ex (a,PA,b)) . z))) is V27() boolean set
K100(1,(('not' ('not' ((Ex (a,G,b)) . z))) '&' ('not' ((Ex (a,PA,b)) . z)))) is set
EqClass (z,(CompF (G,b))) is Element of CompF (G,b)
a . z is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
(B_SUP (a,(CompF (G,b)))) . z is V27() boolean Element of BOOLEAN
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of K19((PARTITIONS Y))
PA is a_partition of Y
All ((a 'eqv' b),PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,G) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
G \ {PA} is Element of K19((PARTITIONS Y))
'/\' (G \ {PA}) is a_partition of Y
B_INF ((a 'eqv' b),(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All (a,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_INF (a,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All (b,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_INF (b,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (a,PA,G)) 'eqv' (All (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
(All ((a 'eqv' b),PA,G)) . z is V27() boolean Element of BOOLEAN
((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z is V27() boolean Element of BOOLEAN
(All (a,PA,G)) . z is V27() boolean Element of BOOLEAN
(All (b,PA,G)) . z is V27() boolean Element of BOOLEAN
((All (a,PA,G)) . z) 'xor' ((All (b,PA,G)) . z) is V27() boolean set
((All (a,PA,G)) . z) <=> ((All (b,PA,G)) . z) is V27() boolean set
'not' (((All (a,PA,G)) . z) 'xor' ((All (b,PA,G)) . z)) is V27() boolean set
K100(1,(((All (a,PA,G)) . z) 'xor' ((All (b,PA,G)) . z))) is set
((All (a,PA,G)) . z) => ((All (b,PA,G)) . z) is V27() boolean set
'not' ((All (a,PA,G)) . z) is V27() boolean set
K100(1,((All (a,PA,G)) . z)) is set
('not' ((All (a,PA,G)) . z)) 'or' ((All (b,PA,G)) . z) is V27() boolean set
'not' ('not' ((All (a,PA,G)) . z)) is V27() boolean set
K100(1,('not' ((All (a,PA,G)) . z))) is set
'not' ((All (b,PA,G)) . z) is V27() boolean set
K100(1,((All (b,PA,G)) . z)) is set
('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' ((All (b,PA,G)) . z)) is V27() boolean set
K97(('not' ('not' ((All (a,PA,G)) . z))),('not' ((All (b,PA,G)) . z))) is set
'not' (('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
K100(1,(('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' ((All (b,PA,G)) . z)))) is set
((All (b,PA,G)) . z) => ((All (a,PA,G)) . z) is V27() boolean set
('not' ((All (b,PA,G)) . z)) 'or' ((All (a,PA,G)) . z) is V27() boolean set
'not' ('not' ((All (b,PA,G)) . z)) is V27() boolean set
K100(1,('not' ((All (b,PA,G)) . z))) is set
('not' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)) is V27() boolean set
K97(('not' ('not' ((All (b,PA,G)) . z))),('not' ((All (a,PA,G)) . z))) is set
'not' (('not' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z))) is V27() boolean set
K100(1,(('not' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)))) is set
(((All (a,PA,G)) . z) => ((All (b,PA,G)) . z)) '&' (((All (b,PA,G)) . z) => ((All (a,PA,G)) . z)) is V27() boolean set
K97((((All (a,PA,G)) . z) => ((All (b,PA,G)) . z)),(((All (b,PA,G)) . z) => ((All (a,PA,G)) . z))) is set
'not' (((All (a,PA,G)) . z) <=> ((All (b,PA,G)) . z)) is V27() boolean set
K100(1,(((All (a,PA,G)) . z) <=> ((All (b,PA,G)) . z))) is set
'not' ((All (b,PA,G)) . z) is V27() boolean Element of BOOLEAN
((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z)) is V27() boolean set
'not' ('not' ((All (b,PA,G)) . z)) is V27() boolean set
K100(1,('not' ((All (b,PA,G)) . z))) is set
('not' ((All (a,PA,G)) . z)) '&' ('not' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
K97(('not' ((All (a,PA,G)) . z)),('not' ('not' ((All (b,PA,G)) . z)))) is set
'not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' ((All (a,PA,G)) . z)) '&' ('not' ('not' ((All (b,PA,G)) . z))))) is set
'not' ((All (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
(((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)) is V27() boolean set
K97((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))),('not' ((All (a,PA,G)) . z))) is set
(((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z) is V27() boolean set
K97((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))),((All (b,PA,G)) . z)) is set
((((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)) is V27() boolean set
'not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z))) is V27() boolean set
K100(1,((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)))) is set
'not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z)) is V27() boolean set
K100(1,((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z))) is set
('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)))) '&' ('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z))) is V27() boolean set
K97(('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)))),('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z)))) is set
'not' (('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)))) '&' ('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z)))) '&' ('not' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z))))) is set
('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K97(('not' ((All (a,PA,G)) . z)),((All (a,PA,G)) . z)) is set
('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)) is V27() boolean Element of BOOLEAN
K97(('not' ((All (a,PA,G)) . z)),('not' ((All (b,PA,G)) . z))) is set
(('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
'not' (('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) is V27() boolean set
K100(1,(('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z))) is set
'not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
K100(1,(('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) is set
('not' (('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z))) '&' ('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K97(('not' (('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z))),('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) is set
'not' (('not' (('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z))) '&' ('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) is V27() boolean set
K100(1,(('not' (('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z))) '&' ('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))))) is set
((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
K97(((All (b,PA,G)) . z),(((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z)))) is set
((('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)))) is V27() boolean set
'not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K100(1,((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) is set
'not' (((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K100(1,(((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))))) is set
('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' (((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))))) is V27() boolean set
K97(('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))),('not' (((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z)))))) is set
'not' (('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' (((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z)))))) is V27() boolean set
K100(1,(('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' (((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))))))) is set
((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K97(((All (b,PA,G)) . z),((All (a,PA,G)) . z)) is set
((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)) is V27() boolean Element of BOOLEAN
K97(((All (b,PA,G)) . z),('not' ((All (b,PA,G)) . z))) is set
(((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
'not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) is V27() boolean set
K100(1,(((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) is set
'not' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
K100(1,(((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))) is set
('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K97(('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))),('not' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))))) is set
'not' (('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))))) is V27() boolean set
K100(1,(('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))))) is set
((('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)))) is V27() boolean set
'not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K100(1,((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))))) is set
('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))))) is V27() boolean set
K97(('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))),('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))))) is set
'not' (('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))))) is V27() boolean set
K100(1,(('not' ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))))))) is set
FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
'not' FALSE is V27() boolean set
K100(1,FALSE) is set
('not' FALSE) '&' ('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K97(('not' FALSE),('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) is set
'not' (('not' FALSE) '&' ('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) is V27() boolean set
K100(1,(('not' FALSE) '&' ('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))))) is set
(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)))) is V27() boolean set
'not' (FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) is V27() boolean set
K100(1,(FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) is set
('not' (FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))))) is V27() boolean set
K97(('not' (FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))),('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))))) is set
'not' (('not' (FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))))) is V27() boolean set
K100(1,(('not' (FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z))))))) is set
(((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE is V27() boolean set
('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) '&' ('not' FALSE) is V27() boolean set
K97(('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))),('not' FALSE)) is set
'not' (('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) '&' ('not' FALSE)) is V27() boolean set
K100(1,(('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) '&' ('not' FALSE))) is set
(('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) is V27() boolean set
'not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE) is V27() boolean set
K100(1,((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE)) is set
('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE)) is V27() boolean set
K97(('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))),('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE))) is set
'not' (('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE))) is V27() boolean set
K100(1,(('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE)))) is set
(('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) is V27() boolean set
('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) is V27() boolean set
K97(('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))),('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is set
'not' (('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))))) is set
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
(B_INF (b,(CompF (PA,G)))) . z is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
(a 'eqv' b) . x1 is V27() boolean Element of BOOLEAN
(a . x1) 'xor' (b . x1) is V27() boolean set
(a . x1) <=> (b . x1) is V27() boolean set
'not' ((a . x1) 'xor' (b . x1)) is V27() boolean set
K100(1,((a . x1) 'xor' (b . x1))) is set
(a . x1) => (b . x1) is V27() boolean set
'not' (a . x1) is V27() boolean set
K100(1,(a . x1)) is set
('not' (a . x1)) 'or' (b . x1) is V27() boolean set
'not' ('not' (a . x1)) is V27() boolean set
K100(1,('not' (a . x1))) is set
'not' (b . x1) is V27() boolean set
K100(1,(b . x1)) is set
('not' ('not' (a . x1))) '&' ('not' (b . x1)) is V27() boolean set
K97(('not' ('not' (a . x1))),('not' (b . x1))) is set
'not' (('not' ('not' (a . x1))) '&' ('not' (b . x1))) is V27() boolean set
K100(1,(('not' ('not' (a . x1))) '&' ('not' (b . x1)))) is set
(b . x1) => (a . x1) is V27() boolean set
('not' (b . x1)) 'or' (a . x1) is V27() boolean set
'not' ('not' (b . x1)) is V27() boolean set
K100(1,('not' (b . x1))) is set
('not' ('not' (b . x1))) '&' ('not' (a . x1)) is V27() boolean set
K97(('not' ('not' (b . x1))),('not' (a . x1))) is set
'not' (('not' ('not' (b . x1))) '&' ('not' (a . x1))) is V27() boolean set
K100(1,(('not' ('not' (b . x1))) '&' ('not' (a . x1)))) is set
((a . x1) => (b . x1)) '&' ((b . x1) => (a . x1)) is V27() boolean set
K97(((a . x1) => (b . x1)),((b . x1) => (a . x1))) is set
'not' ((a . x1) <=> (b . x1)) is V27() boolean set
K100(1,((a . x1) <=> (b . x1))) is set
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
b . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
a . c₈ is V27() boolean Element of BOOLEAN
(a 'eqv' b) . x1 is V27() boolean Element of BOOLEAN
(a . x1) 'xor' (b . x1) is V27() boolean set
(a . x1) <=> (b . x1) is V27() boolean set
'not' ((a . x1) 'xor' (b . x1)) is V27() boolean set
K100(1,((a . x1) 'xor' (b . x1))) is set
(a . x1) => (b . x1) is V27() boolean set
'not' (a . x1) is V27() boolean set
K100(1,(a . x1)) is set
('not' (a . x1)) 'or' (b . x1) is V27() boolean set
'not' ('not' (a . x1)) is V27() boolean set
K100(1,('not' (a . x1))) is set
'not' (b . x1) is V27() boolean set
K100(1,(b . x1)) is set
('not' ('not' (a . x1))) '&' ('not' (b . x1)) is V27() boolean set
K97(('not' ('not' (a . x1))),('not' (b . x1))) is set
'not' (('not' ('not' (a . x1))) '&' ('not' (b . x1))) is V27() boolean set
K100(1,(('not' ('not' (a . x1))) '&' ('not' (b . x1)))) is set
(b . x1) => (a . x1) is V27() boolean set
('not' (b . x1)) 'or' (a . x1) is V27() boolean set
'not' ('not' (b . x1)) is V27() boolean set
K100(1,('not' (b . x1))) is set
('not' ('not' (b . x1))) '&' ('not' (a . x1)) is V27() boolean set
K97(('not' ('not' (b . x1))),('not' (a . x1))) is set
'not' (('not' ('not' (b . x1))) '&' ('not' (a . x1))) is V27() boolean set
K100(1,(('not' ('not' (b . x1))) '&' ('not' (a . x1)))) is set
((a . x1) => (b . x1)) '&' ((b . x1) => (a . x1)) is V27() boolean set
K97(((a . x1) => (b . x1)),((b . x1) => (a . x1))) is set
'not' ((a . x1) <=> (b . x1)) is V27() boolean set
K100(1,((a . x1) <=> (b . x1))) is set
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
(B_INF (b,(CompF (PA,G)))) . z is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
c₉ is Element of Y
a . c₉ is V27() boolean Element of BOOLEAN
c₁₀ is Element of Y
b . c₁₀ is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of K19((PARTITIONS Y))
PA is a_partition of Y
All ((a '&' b),PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,G) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
G \ {PA} is Element of K19((PARTITIONS Y))
'/\' (G \ {PA}) is a_partition of Y
B_INF ((a '&' b),(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All (b,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_INF (b,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a '&' (All (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
(All ((a '&' b),PA,G)) . z is V27() boolean Element of BOOLEAN
(a '&' (All (b,PA,G))) . z is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
(a '&' b) . x1 is V27() boolean Element of BOOLEAN
b . x1 is V27() boolean Element of BOOLEAN
(a . x1) '&' (b . x1) is V27() boolean Element of BOOLEAN
K97((a . x1),(b . x1)) is set
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
(a '&' b) . x1 is V27() boolean Element of BOOLEAN
a . x1 is V27() boolean Element of BOOLEAN
(a . x1) '&' (b . x1) is V27() boolean Element of BOOLEAN
K97((a . x1),(b . x1)) is set
(B_INF (b,(CompF (PA,G)))) . z is V27() boolean Element of BOOLEAN
a . z is V27() boolean Element of BOOLEAN
TRUE '&' TRUE is V27() boolean Element of BOOLEAN
K97(TRUE,TRUE) is set
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of K19((PARTITIONS Y))
PA is a_partition of Y
All (a,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,G) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
G \ {PA} is Element of K19((PARTITIONS Y))
'/\' (G \ {PA}) is a_partition of Y
B_INF (a,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (a,PA,G)) 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Ex ((a 'imp' b),PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_SUP ((a 'imp' b),(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
((All (a,PA,G)) 'imp' b) . z is V27() boolean Element of BOOLEAN
(Ex ((a 'imp' b),PA,G)) . z is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
(All (a,PA,G)) . z is V27() boolean Element of BOOLEAN
'not' ((All (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K100(1,((All (a,PA,G)) . z)) is set
b . z is V27() boolean Element of BOOLEAN
('not' ((All (a,PA,G)) . z)) 'or' (b . z) is V27() boolean set
'not' ('not' ((All (a,PA,G)) . z)) is V27() boolean set
K100(1,('not' ((All (a,PA,G)) . z))) is set
'not' (b . z) is V27() boolean set
K100(1,(b . z)) is set
('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' (b . z)) is V27() boolean set
K97(('not' ('not' ((All (a,PA,G)) . z))),('not' (b . z))) is set
'not' (('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' (b . z))) is V27() boolean set
K100(1,(('not' ('not' ((All (a,PA,G)) . z))) '&' ('not' (b . z)))) is set
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
(a 'imp' b) . x1 is V27() boolean Element of BOOLEAN
'not' (a . x1) is V27() boolean Element of BOOLEAN
K100(1,(a . x1)) is set
b . x1 is V27() boolean Element of BOOLEAN
('not' (a . x1)) 'or' (b . x1) is V27() boolean set
'not' ('not' (a . x1)) is V27() boolean set
K100(1,('not' (a . x1))) is set
'not' (b . x1) is V27() boolean set
K100(1,(b . x1)) is set
('not' ('not' (a . x1))) '&' ('not' (b . x1)) is V27() boolean set
K97(('not' ('not' (a . x1))),('not' (b . x1))) is set
'not' (('not' ('not' (a . x1))) '&' ('not' (b . x1))) is V27() boolean set
K100(1,(('not' ('not' (a . x1))) '&' ('not' (b . x1)))) is set
c₈ is Element of Y
(a 'imp' b) . c₈ is V27() boolean Element of BOOLEAN
(a 'imp' b) . z is V27() boolean Element of BOOLEAN
a . z is V27() boolean Element of BOOLEAN
'not' (a . z) is V27() boolean Element of BOOLEAN
K100(1,(a . z)) is set
('not' (a . z)) 'or' (b . z) is V27() boolean set
'not' ('not' (a . z)) is V27() boolean set
K100(1,('not' (a . z))) is set
('not' ('not' (a . z))) '&' ('not' (b . z)) is V27() boolean set
K97(('not' ('not' (a . z))),('not' (b . z))) is set
'not' (('not' ('not' (a . z))) '&' ('not' (b . z))) is V27() boolean set
K100(1,(('not' ('not' (a . z))) '&' ('not' (b . z)))) is set
x1 is Element of Y
(a 'imp' b) . x1 is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of K19((PARTITIONS Y))
PA is a_partition of Y
All (a,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,G) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
G \ {PA} is Element of K19((PARTITIONS Y))
'/\' (G \ {PA}) is a_partition of Y
B_INF (a,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
All (b,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_INF (b,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (a,PA,G)) 'eqv' (All (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' b) 'or' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' a) 'or' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
a . x1 is V27() boolean Element of BOOLEAN
(('not' a) 'or' b) . x1 is V27() boolean Element of BOOLEAN
('not' a) . x1 is V27() boolean Element of BOOLEAN
(('not' a) . x1) 'or' (b . x1) is V27() boolean set
'not' (('not' a) . x1) is V27() boolean set
K100(1,(('not' a) . x1)) is set
'not' (b . x1) is V27() boolean set
K100(1,(b . x1)) is set
('not' (('not' a) . x1)) '&' ('not' (b . x1)) is V27() boolean set
K97(('not' (('not' a) . x1)),('not' (b . x1))) is set
'not' (('not' (('not' a) . x1)) '&' ('not' (b . x1))) is V27() boolean set
K100(1,(('not' (('not' a) . x1)) '&' ('not' (b . x1)))) is set
FALSE 'or' FALSE is V27() boolean set
'not' FALSE is V27() boolean set
K100(1,FALSE) is set
('not' FALSE) '&' ('not' FALSE) is V27() boolean set
K97(('not' FALSE),('not' FALSE)) is set
'not' (('not' FALSE) '&' ('not' FALSE)) is V27() boolean set
K100(1,(('not' FALSE) '&' ('not' FALSE))) is set
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
b . x1 is V27() boolean Element of BOOLEAN
(('not' b) 'or' a) . x1 is V27() boolean Element of BOOLEAN
('not' b) . x1 is V27() boolean Element of BOOLEAN
(('not' b) . x1) 'or' (a . x1) is V27() boolean set
'not' (('not' b) . x1) is V27() boolean set
K100(1,(('not' b) . x1)) is set
'not' (a . x1) is V27() boolean set
K100(1,(a . x1)) is set
('not' (('not' b) . x1)) '&' ('not' (a . x1)) is V27() boolean set
K97(('not' (('not' b) . x1)),('not' (a . x1))) is set
'not' (('not' (('not' b) . x1)) '&' ('not' (a . x1))) is V27() boolean set
K100(1,(('not' (('not' b) . x1)) '&' ('not' (a . x1)))) is set
(All (a,PA,G)) 'imp' (All (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (b,PA,G)) 'imp' (All (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((All (a,PA,G)) 'imp' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' (All (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (All (a,PA,G))) 'or' (All (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' (All (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (All (b,PA,G))) 'or' (All (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (('not' (All (b,PA,G))) 'or' (All (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ('not' (All (b,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (All (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (b,PA,G)) '&' ('not' (All (b,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' ('not' (All (b,PA,G)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (All (a,PA,G))) '&' (All (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(All (b,PA,G)) '&' (All (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) '&' (All (a,PA,G))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
O_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' (O_el Y) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z is V27() boolean Element of BOOLEAN
((All (b,PA,G)) '&' (All (a,PA,G))) . z is V27() boolean Element of BOOLEAN
((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) is V27() boolean set
'not' ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z) is V27() boolean set
K100(1,((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z)) is set
'not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) is V27() boolean set
K100(1,(((All (b,PA,G)) '&' (All (a,PA,G))) . z)) is set
('not' ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z)) '&' ('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z)) is V27() boolean set
K97(('not' ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z)),('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z))) is set
'not' (('not' ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z)) '&' ('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z))) is V27() boolean set
K100(1,(('not' ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z)) '&' ('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z)))) is set
('not' (All (a,PA,G))) . z is V27() boolean Element of BOOLEAN
('not' (All (b,PA,G))) . z is V27() boolean Element of BOOLEAN
(('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z) is V27() boolean Element of BOOLEAN
K97((('not' (All (a,PA,G))) . z),(('not' (All (b,PA,G))) . z)) is set
((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) is V27() boolean set
'not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) is V27() boolean set
K100(1,((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))) is set
('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z)) is V27() boolean set
K97(('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))),('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z))) is set
'not' (('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z))) is V27() boolean set
K100(1,(('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) '&' (All (a,PA,G))) . z)))) is set
(All (b,PA,G)) . z is V27() boolean Element of BOOLEAN
(All (a,PA,G)) . z is V27() boolean Element of BOOLEAN
((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K97(((All (b,PA,G)) . z),((All (a,PA,G)) . z)) is set
((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) is V27() boolean set
'not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) is V27() boolean set
K100(1,(((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) is set
('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) is V27() boolean set
K97(('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))),('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is set
'not' (('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))))) is set
'not' ((All (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K100(1,((All (a,PA,G)) . z)) is set
('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z) is V27() boolean Element of BOOLEAN
K97(('not' ((All (a,PA,G)) . z)),(('not' (All (b,PA,G))) . z)) is set
(('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) is V27() boolean set
'not' (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z)) is V27() boolean set
K100(1,(('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z))) is set
('not' (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) is V27() boolean set
K97(('not' (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z))),('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is set
'not' (('not' (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))))) is set
'not' ((All (b,PA,G)) . z) is V27() boolean Element of BOOLEAN
K100(1,((All (b,PA,G)) . z)) is set
('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)) is V27() boolean Element of BOOLEAN
K97(('not' ((All (a,PA,G)) . z)),('not' ((All (b,PA,G)) . z))) is set
(('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) is V27() boolean set
'not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) is V27() boolean set
K100(1,(('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) is set
('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))) is V27() boolean set
K97(('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))),('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is set
'not' (('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) '&' ('not' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z))))) is set
(B_INF (b,(CompF (PA,G)))) . z is V27() boolean Element of BOOLEAN
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
c₉ is Element of Y
a . c₉ is V27() boolean Element of BOOLEAN
c₁₀ is Element of Y
b . c₁₀ is V27() boolean Element of BOOLEAN
Y is non empty set
K20(Y,BOOLEAN) is set
K19(K20(Y,BOOLEAN)) is set
PARTITIONS Y is partition-membered Element of K19(K19(K270(Y)))
K270(Y) is Element of K19(K19(Y))
K19(Y) is set
K19(K19(Y)) is set
K19(K270(Y)) is set
K19(K19(K270(Y))) is set
K19((PARTITIONS Y)) is set
I_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'eqv' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
G is Element of K19((PARTITIONS Y))
PA is a_partition of Y
Ex (a,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
CompF (PA,G) is a_partition of Y
{PA} is non empty Element of K19((PARTITIONS Y))
G \ {PA} is Element of K19((PARTITIONS Y))
'/\' (G \ {PA}) is a_partition of Y
B_SUP (a,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
Ex (b,PA,G) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
B_SUP (b,(CompF (PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
b 'imp' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' b) 'or' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
a 'imp' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' a is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' a) 'or' b is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
z is Element of Y
((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z is V27() boolean Element of BOOLEAN
(Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(Ex (b,PA,G)) 'imp' (Ex (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) '&' ((Ex (b,PA,G)) 'imp' (Ex (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' (Ex (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' ((Ex (b,PA,G)) 'imp' (Ex (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
'not' (Ex (b,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (Ex (b,PA,G))) 'or' (Ex (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (('not' (Ex (b,PA,G))) 'or' (Ex (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' ('not' (Ex (b,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (Ex (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(Ex (b,PA,G)) '&' ('not' (Ex (b,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' ('not' (Ex (b,PA,G)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
('not' (Ex (a,PA,G))) '&' (Ex (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(Ex (b,PA,G)) '&' (Ex (a,PA,G)) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) '&' (Ex (a,PA,G))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
O_el Y is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' (O_el Y) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(O_el Y) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
((('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)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((O_el Y) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G))) is Function-like quasi_total boolean-valued Element of K19(K20(Y,BOOLEAN))
(('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z is V27() boolean Element of BOOLEAN
((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z is V27() boolean Element of BOOLEAN
((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z) 'or' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z) is V27() boolean set
'not' ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z) is V27() boolean set
K100(1,((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z)) is set
'not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z) is V27() boolean set
K100(1,(((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z)) is set
('not' ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z)) '&' ('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z)) is V27() boolean set
K97(('not' ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z)),('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z))) is set
'not' (('not' ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z)) '&' ('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z))) is V27() boolean set
K100(1,(('not' ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z)) '&' ('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z)))) is set
('not' (Ex (a,PA,G))) . z is V27() boolean Element of BOOLEAN
('not' (Ex (b,PA,G))) . z is V27() boolean Element of BOOLEAN
(('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z) is V27() boolean Element of BOOLEAN
K97((('not' (Ex (a,PA,G))) . z),(('not' (Ex (b,PA,G))) . z)) is set
((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z) is V27() boolean set
'not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z)) is V27() boolean set
K100(1,((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))) is set
('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z)) is V27() boolean set
K97(('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))),('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z))) is set
'not' (('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z))) is V27() boolean set
K100(1,(('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z)))) is set
(Ex (b,PA,G)) . z is V27() boolean Element of BOOLEAN
(Ex (a,PA,G)) . z is V27() boolean Element of BOOLEAN
((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K97(((Ex (b,PA,G)) . z),((Ex (a,PA,G)) . z)) is set
((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) is V27() boolean set
'not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) is V27() boolean set
K100(1,(((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z))) is set
('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z))) is V27() boolean set
K97(('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))),('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)))) is set
'not' (('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z))))) is set
'not' ((Ex (a,PA,G)) . z) is V27() boolean Element of BOOLEAN
K100(1,((Ex (a,PA,G)) . z)) is set
('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z) is V27() boolean Element of BOOLEAN
K97(('not' ((Ex (a,PA,G)) . z)),(('not' (Ex (b,PA,G))) . z)) is set
(('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) is V27() boolean set
'not' (('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z)) is V27() boolean set
K100(1,(('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z))) is set
('not' (('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z))) is V27() boolean set
K97(('not' (('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z))),('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)))) is set
'not' (('not' (('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' (('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z))))) is set
'not' ((Ex (b,PA,G)) . z) is V27() boolean Element of BOOLEAN
K100(1,((Ex (b,PA,G)) . z)) is set
('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z)) is V27() boolean Element of BOOLEAN
K97(('not' ((Ex (a,PA,G)) . z)),('not' ((Ex (b,PA,G)) . z))) is set
(('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z))) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) is V27() boolean set
'not' (('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z))) is V27() boolean set
K100(1,(('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z)))) is set
('not' (('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z)))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z))) is V27() boolean set
K97(('not' (('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z)))),('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)))) is set
'not' (('not' (('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z)))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)))) is V27() boolean set
K100(1,(('not' (('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z)))) '&' ('not' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z))))) is set
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
(B_SUP (b,(CompF (PA,G)))) . z is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
a . x1 is V27() boolean Element of BOOLEAN
b . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
a . c₈ is V27() boolean Element of BOOLEAN
(('not' a) 'or' b) . x1 is V27() boolean Element of BOOLEAN
('not' a) . x1 is V27() boolean Element of BOOLEAN
(('not' a) . x1) 'or' (b . x1) is V27() boolean set
'not' (('not' a) . x1) is V27() boolean set
K100(1,(('not' a) . x1)) is set
'not' (b . x1) is V27() boolean set
K100(1,(b . x1)) is set
('not' (('not' a) . x1)) '&' ('not' (b . x1)) is V27() boolean set
K97(('not' (('not' a) . x1)),('not' (b . x1))) is set
'not' (('not' (('not' a) . x1)) '&' ('not' (b . x1))) is V27() boolean set
K100(1,(('not' (('not' a) . x1)) '&' ('not' (b . x1)))) is set
FALSE 'or' FALSE is V27() boolean set
'not' FALSE is V27() boolean set
K100(1,FALSE) is set
('not' FALSE) '&' ('not' FALSE) is V27() boolean set
K97(('not' FALSE),('not' FALSE)) is set
'not' (('not' FALSE) '&' ('not' FALSE)) is V27() boolean set
K100(1,(('not' FALSE) '&' ('not' FALSE))) is set
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
a . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
b . c₈ is V27() boolean Element of BOOLEAN
(('not' b) 'or' a) . x1 is V27() boolean Element of BOOLEAN
('not' b) . x1 is V27() boolean Element of BOOLEAN
(('not' b) . x1) 'or' (a . x1) is V27() boolean set
'not' (('not' b) . x1) is V27() boolean set
K100(1,(('not' b) . x1)) is set
'not' (a . x1) is V27() boolean set
K100(1,(a . x1)) is set
('not' (('not' b) . x1)) '&' ('not' (a . x1)) is V27() boolean set
K97(('not' (('not' b) . x1)),('not' (a . x1))) is set
'not' (('not' (('not' b) . x1)) '&' ('not' (a . x1))) is V27() boolean set
K100(1,(('not' (('not' b) . x1)) '&' ('not' (a . x1)))) is set
FALSE 'or' FALSE is V27() boolean set
'not' FALSE is V27() boolean set
K100(1,FALSE) is set
('not' FALSE) '&' ('not' FALSE) is V27() boolean set
K97(('not' FALSE),('not' FALSE)) is set
'not' (('not' FALSE) '&' ('not' FALSE)) is V27() boolean set
K100(1,(('not' FALSE) '&' ('not' FALSE))) is set
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
(B_SUP (b,(CompF (PA,G)))) . z is V27() boolean Element of BOOLEAN
EqClass (z,(CompF (PA,G))) is Element of CompF (PA,G)
x1 is Element of Y
b . x1 is V27() boolean Element of BOOLEAN
c₈ is Element of Y
a . c₈ is V27() boolean Element of BOOLEAN
c₉ is Element of Y
a . c₉ is V27() boolean Element of BOOLEAN
c₁₀ is Element of Y
b . c₁₀ is V27() boolean Element of BOOLEAN