:: BVFUNC26 semantic presentation

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

1 is non empty set
{K115(),1} is non empty set

dom Y is set

dom a is set
(dom Y) /\ (dom a) is 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

dom b is 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

dom b is set

dom c is 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

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

dom b is 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

dom b is set

dom c is 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,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

(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

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set

dom a is set
dom b is set
dom (a,b) is set
Y /\ Y is set
rng (a,b) is set

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

dom a is set
dom b is set
dom (a,b) is set
Y /\ Y is set
rng (a,b) is set

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

(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) 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

(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 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

(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 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

(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' ((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

(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' ((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

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))

(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))

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set

(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' (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))

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is 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))
'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))

'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

(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' (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))

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set

(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

(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

(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))

('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

(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 '&' 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' (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

(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))

() '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 '&' (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))

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))
() '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

(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))
(() '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 '&' (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))

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))
() '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))
() '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

(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))

'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))

() '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' ('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))
() '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))
() '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

(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))

(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

(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))

() '&' ('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' (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

(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' (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))

() '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' ('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))
() '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))
() '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

(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 '&' ('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))
() '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))

(() '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

(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 '&' ('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' ('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))
() '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))

(() '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))

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set

(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' (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 '&' ('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))
() '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) '&' (() 'or' ()) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
() 'or' ((a 'or' b) '&' (() 'or' ())) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
() '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))
() 'or' (() 'or' ()) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(() 'or' (a 'or' b)) '&' (() 'or' (() 'or' ())) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(() '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))
((() 'or' a) 'or' b) '&' (() 'or' (() 'or' ())) 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) '&' (() 'or' (() 'or' ())) 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' (() 'or' ())) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

(() 'or' ()) 'or' () 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

(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' ('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

(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,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))

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))

('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))

('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

(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))

(() '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))

'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))

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))

(a '&' ()) '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 '&' ()) '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 '&' ()) 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 '&' c)) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))

() 'or' ('not' ()) is non empty Relation-like Y -defined BOOLEAN -valued Function-like V17(Y) quasi_total boolean-valued Element of K10(K11(Y,BOOLEAN))
(() '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

(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))

(() '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) '&' ('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

(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' ((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))

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set

(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' ((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

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))

(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))

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is set

(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' (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))

Y is non empty set
K11(Y,BOOLEAN) is set
K10(K11(Y,BOOLEAN)) is 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))
'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))

'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

(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' (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 'or' ()) 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 '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))

(() '&' b) '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))
() '&' ((() '&' b) '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))
() '&' (() '&' 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 '&' ()) 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' (() '&' (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))
((() '&' ()) '&' b) '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))

(() '&' 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) '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))

(() '&' 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))
(() '&' 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

(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))

('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

(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))

'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))

'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