K114() is Element of K10(K110())
K110() is set
K10(K110()) is set
K109() is set
K10(K109()) is set
K10(K114()) is set
BOOLEAN is non empty set
K115() is empty Function-like functional V55() Element of K114()
1 is non empty set
{K115(),1} is non empty set
{} is empty Function-like functional V55() set
FALSE is V39() boolean set
TRUE is V39() boolean set
Y is Relation-like Function-like boolean-valued set
dom Y is set
a is Relation-like Function-like boolean-valued set
dom a is set
(dom Y) /\ (dom a) is set
b is Relation-like Function-like set
dom b is set
c is set
b . c is set
Y . c is V39() boolean set
a . c is V39() boolean set
(Y . c) 'nand' (a . c) is V39() boolean set
b is Relation-like Function-like set
dom b is set
c is Relation-like Function-like set
dom c is set
x is set
b . x is set
c . x is set
Y . x is V39() boolean set
a . x is V39() boolean set
(Y . x) 'nand' (a . x) is V39() boolean set
b is Relation-like Function-like set
dom b is set
c is Relation-like Function-like boolean-valued set
dom c is set
x is Relation-like Function-like boolean-valued set
dom x is set
(dom c) /\ (dom x) is set
(dom x) /\ (dom c) is set
c6 is set
b . c6 is set
x . c6 is V39() boolean set
c . c6 is V39() boolean set
(x . c6) 'nand' (c . c6) is V39() boolean set
b is Relation-like Function-like set
dom b is set
c is set
b . c is set
Y . c is V39() boolean set
a . c is V39() boolean set
(Y . c) 'nor' (a . c) is V39() boolean set
b is Relation-like Function-like set
dom b is set
c is Relation-like Function-like set
dom c is set
x is set
b . x is set
c . x is set
Y . x is V39() boolean set
a . x is V39() boolean set
(Y . x) 'nor' (a . x) is V39() boolean set
b is Relation-like Function-like set
dom b is set
c is Relation-like Function-like boolean-valued set
dom c is set
x is Relation-like Function-like boolean-valued set
dom x is set
(dom c) /\ (dom x) is set
(dom x) /\ (dom c) is set
c6 is set
b . c6 is set
x . c6 is V39() boolean set
c . c6 is V39() boolean set
(x . c6) 'nor' (c . c6) is V39() boolean set
Y is Relation-like Function-like boolean-valued set
a is Relation-like Function-like boolean-valued set
(Y,a) is Relation-like Function-like set
b is set
rng (Y,a) is set
dom (Y,a) is set
c is set
(Y,a) . c is set
Y . c is V39() boolean set
a . c is V39() boolean set
(Y . c) 'nand' (a . c) is V39() boolean set
FALSE is V39() boolean Element of BOOLEAN
TRUE is V39() boolean Element of BOOLEAN
(Y,a) is Relation-like Function-like set
b is set
rng (Y,a) is set
dom (Y,a) is set
c is set
(Y,a) . c is set
Y . c is V39() boolean set
a . c is V39() boolean set
(Y . c) 'nor' (a . c) is V39() boolean set
FALSE is V39() boolean Element of BOOLEAN
TRUE is V39() boolean Element of BOOLEAN
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a,b) is Relation-like Function-like boolean-valued set
dom a is set
dom b is set
dom (a,b) is set
Y /\ Y is set
rng (a,b) is set
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
dom c is set
dom a is set
dom b is set
dom (a,b) is set
Y /\ Y is set
x is Element of Y
c . x is V39() boolean Element of BOOLEAN
a . x is V39() boolean Element of BOOLEAN
b . x is V39() boolean Element of BOOLEAN
(a . x) 'nand' (b . x) is V39() boolean Element of BOOLEAN
(dom a) /\ (dom b) is set
x is set
c . x is V39() boolean set
a . x is V39() boolean set
b . x is V39() boolean set
(a . x) 'nand' (b . x) is V39() boolean set
(a,b) is Relation-like Function-like boolean-valued set
dom a is set
dom b is set
dom (a,b) is set
Y /\ Y is set
rng (a,b) is set
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
dom c is set
dom a is set
dom b is set
dom (a,b) is set
Y /\ Y is set
x is Element of Y
c . x is V39() boolean Element of BOOLEAN
a . x is V39() boolean Element of BOOLEAN
b . x is V39() boolean Element of BOOLEAN
(a . x) 'nor' (b . x) is V39() boolean Element of BOOLEAN
(dom a) /\ (dom b) is set
x is set
c . x is V39() boolean set
a . x is V39() boolean set
b . x is V39() boolean set
(a . x) 'nor' (b . x) is V39() boolean set
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a,b) is Relation-like Function-like boolean-valued set
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a,b) is Relation-like Function-like boolean-valued set
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is Element of Y
(Y,a,b) . c is V39() boolean set
('not' (a '&' b)) . c is V39() boolean set
('not' (a '&' b)) . c is V39() boolean Element of BOOLEAN
(a '&' b) . c is V39() boolean Element of BOOLEAN
'not' ((a '&' b) . c) is V39() boolean Element of BOOLEAN
a . c is V39() boolean Element of BOOLEAN
b . c is V39() boolean Element of BOOLEAN
(a . c) '&' (b . c) is V39() boolean Element of BOOLEAN
'not' ((a . c) '&' (b . c)) is V39() boolean Element of BOOLEAN
(a . c) 'nand' (b . c) is V39() boolean Element of BOOLEAN
'not' ((a . c) 'nand' (b . c)) is V39() boolean Element of BOOLEAN
'not' ('not' ((a . c) 'nand' (b . c))) is V39() boolean Element of BOOLEAN
(Y,a,b) . c is V39() boolean Element of BOOLEAN
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is Element of Y
(Y,a,b) . c is V39() boolean set
('not' (a 'or' b)) . c is V39() boolean set
('not' (a 'or' b)) . c is V39() boolean Element of BOOLEAN
(a 'or' b) . c is V39() boolean Element of BOOLEAN
'not' ((a 'or' b) . c) is V39() boolean Element of BOOLEAN
a . c is V39() boolean Element of BOOLEAN
b . c is V39() boolean Element of BOOLEAN
(a . c) 'or' (b . c) is V39() boolean set
'not' ((a . c) 'or' (b . c)) is V39() boolean set
(a . c) 'nor' (b . c) is V39() boolean Element of BOOLEAN
'not' ((a . c) 'nor' (b . c)) is V39() boolean Element of BOOLEAN
'not' ('not' ((a . c) 'nor' (b . c))) is V39() boolean Element of BOOLEAN
(Y,a,b) . c is V39() boolean Element of BOOLEAN
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(I_el Y),a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(I_el Y) '&' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((I_el Y) '&' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(O_el Y),a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(O_el Y) '&' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((O_el Y) '&' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
(Y,(O_el Y),(O_el Y)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(O_el Y),(I_el Y)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(I_el Y),(I_el Y)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (I_el Y) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Y,a,a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,('not' a)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Y,a,('not' a)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' ('not' a)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (O_el Y) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a '&' b) '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a '&' b) '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (b '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (b '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(a '&' b),c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a '&' b) '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a '&' b) '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' (a '&' b)) '&' ('not' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (b 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (b 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a '&' b) 'or' (a '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a '&' b) 'or' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'xor' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b 'xor' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a '&' b) 'eqv' (a '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (b 'xor' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (b 'xor' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a '&' b) 'xor' (a '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a '&' b) 'xor' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a '&' b) 'eqv' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' ((a '&' b) 'eqv' (a '&' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,b,c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(Y,b,c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' (b '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' (b '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (Y,b,c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (Y,b,c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (b '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' (b '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' ('not' (b '&' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (b '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' (b '&' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,b,c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(Y,b,c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' b) 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' (b 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (Y,b,c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (Y,b,c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (b 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' (b 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' ('not' (b 'or' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (b 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' (b 'or' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' (b 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'eqv' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b 'eqv' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'xor' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' (b 'xor' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (b 'eqv' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (b 'eqv' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (b 'eqv' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' (b 'eqv' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (b 'xor' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (b 'xor' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' (b 'xor' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' (b 'xor' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(a '&' a),b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(a 'or' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' (a '&' a)) '&' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'eqv' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(a 'eqv' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'xor' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' (a 'xor' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (a 'eqv' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (a 'eqv' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'eqv' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' (a 'eqv' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'xor' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a 'xor' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' (a 'xor' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' (a 'xor' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(Y,a,b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (Y,a,b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' ('not' (a '&' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' (a '&' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' a) '&' (('not' a) 'or' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(I_el Y) '&' (('not' a) 'or' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(Y,a,b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (Y,a,b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' (a 'or' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' ('not' (a 'or' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a 'or' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' (a 'or' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' a) 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(I_el Y) 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'eqv' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(a 'eqv' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (a 'eqv' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (a 'eqv' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'xor' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'xor' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' (a 'xor' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' ('not' (a 'xor' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a 'xor' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' (a 'xor' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a 'or' b) '&' (('not' a) 'or' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ((a 'or' b) '&' (('not' a) 'or' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' (a 'or' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' (('not' a) 'or' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' (a 'or' b)) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' a) 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
((('not' a) 'or' a) 'or' b) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(I_el Y) 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
((I_el Y) 'or' b) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(I_el Y) '&' (('not' a) 'or' (('not' a) 'or' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' ('not' a)) 'or' ('not' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(Y,a,b),(Y,a,b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) '&' (Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((Y,a,b) '&' (Y,a,b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a '&' b) 'or' ('not' ('not' (a '&' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(Y,a,b),(Y,a,c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (b 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) '&' (Y,a,c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((Y,a,b) '&' (Y,a,c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' (a '&' b)) '&' (Y,a,c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (('not' (a '&' b)) '&' (Y,a,c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' (a '&' b)) '&' ('not' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (('not' (a '&' b)) '&' ('not' (a '&' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' ('not' (a '&' b))) 'or' ('not' ('not' (a '&' c))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'imp' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b 'imp' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' b) '&' ('not' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (b 'imp' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (b 'imp' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' b) 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' (('not' b) 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' (('not' b) 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a '&' ('not' b)) 'or' (a '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a '&' ('not' b)) 'or' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' (a '&' ('not' b))) '&' ('not' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' ('not' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' ('not' ('not' b))) '&' ('not' (a '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'imp' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(a 'imp' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) 'or' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) 'or' a) '&' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(I_el Y) '&' ('not' (a '&' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(I_el Y),a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(I_el Y) 'or' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((I_el Y) 'or' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (I_el Y) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(O_el Y),a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(O_el Y) 'or' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((O_el Y) 'or' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
(Y,(O_el Y),(O_el Y)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(O_el Y),(I_el Y)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,(I_el Y),(I_el Y)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (O_el Y) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Y,a,a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Y,a,b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ('not' (a 'or' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
I_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,('not' a)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (Y,a,('not' a)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' ('not' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' ('not' a)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (I_el Y) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'xor' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' (a 'xor' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a '&' ('not' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) '&' b) 'or' (a '&' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' ((('not' a) '&' b) 'or' (a '&' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' (('not' a) '&' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' (a '&' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) '&' (('not' a) '&' b)) 'or' (('not' a) '&' (a '&' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' ('not' a) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) '&' ('not' a)) '&' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
((('not' a) '&' ('not' a)) '&' b) 'or' (('not' a) '&' (a '&' ('not' b))) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' a) '&' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) '&' a) '&' ('not' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) '&' b) 'or' ((('not' a) '&' a) '&' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
O_el Y is non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(O_el Y) '&' ('not' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) '&' b) 'or' ((O_el Y) '&' ('not' b)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(('not' a) '&' b) 'or' (O_el Y) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' b) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b '&' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
('not' (a 'or' b)) 'or' ('not' (a 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' (b '&' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' (b '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a 'or' b) '&' (a 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a 'or' b) '&' (a 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(Y,a,(b 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(a 'or' b) 'or' c is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' ((a 'or' b) 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
a 'or' (b 'or' c) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' (a 'or' (b 'or' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set
a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
'not' a is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
b is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y)