:: GFACIRC1 semantic presentation

REAL is set
NAT is non empty V9() V10() V11() V36() V51() V52() Element of K18(REAL)
K18(REAL) is set
COMPLEX is set
RAT is set
INT is set
K19(COMPLEX,COMPLEX) is Relation-like set
K18(K19(COMPLEX,COMPLEX)) is set
K19(K19(COMPLEX,COMPLEX),COMPLEX) is Relation-like set
K18(K19(K19(COMPLEX,COMPLEX),COMPLEX)) is set
K19(REAL,REAL) is Relation-like set
K18(K19(REAL,REAL)) is set
K19(K19(REAL,REAL),REAL) is Relation-like set
K18(K19(K19(REAL,REAL),REAL)) is set
K19(RAT,RAT) is Relation-like set
K18(K19(RAT,RAT)) is set
K19(K19(RAT,RAT),RAT) is Relation-like set
K18(K19(K19(RAT,RAT),RAT)) is set
K19(INT,INT) is Relation-like set
K18(K19(INT,INT)) is set
K19(K19(INT,INT),INT) is Relation-like set
K18(K19(K19(INT,INT),INT)) is set
K19(NAT,NAT) is Relation-like set
K19(K19(NAT,NAT),NAT) is Relation-like set
K18(K19(K19(NAT,NAT),NAT)) is set
NAT is non empty V9() V10() V11() V36() V51() V52() set
K18(NAT) is set
K18(NAT) is set
BOOLEAN is non empty set
1 is non empty V9() V10() V11() V15() non pair V119() Element of NAT
{} is set
the empty Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional non pair V36() FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() V51() non with_pair set is empty Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional non pair V36() FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() V51() non with_pair set
{{},1} is set
K348() is set
K18(K348()) is set
K349() is Element of K18(K348())
K389() is non empty V95() L10()
the carrier of K389() is non empty set
K352( the carrier of K389()) is non empty M24( the carrier of K389())
K388(K389()) is Element of K18(K352( the carrier of K389()))
K18(K352( the carrier of K389())) is set
K19(K388(K389()),NAT) is Relation-like set
K18(K19(K388(K389()),NAT)) is set
K19(NAT,K388(K389())) is Relation-like set
K18(K19(NAT,K388(K389()))) is set
2 is non empty V9() V10() V11() V15() non pair V119() Element of NAT
2 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((2 -tuples_on BOOLEAN),BOOLEAN)) is set
3 is non empty V9() V10() V11() V15() non pair V119() Element of NAT
3 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((3 -tuples_on BOOLEAN),BOOLEAN)) is set
'xor' is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
0 is V9() V10() V11() V15() non pair Element of NAT
Seg 1 is non empty V36() V43(1) V51() Element of K18(NAT)
TRUE is boolean Element of BOOLEAN
and2 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
and2a is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
and2b is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
nand2 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
or2 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
nor2a is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
xor2 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
xor2a is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
xor2b is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
nor3 is Relation-like Function-like V27(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((3 -tuples_on BOOLEAN),BOOLEAN))
or3 is Relation-like Function-like V27(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((3 -tuples_on BOOLEAN),BOOLEAN))
or3a is Relation-like Function-like V27(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((3 -tuples_on BOOLEAN),BOOLEAN))
or3b is Relation-like Function-like V27(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((3 -tuples_on BOOLEAN),BOOLEAN))
or3c is Relation-like Function-like V27(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((3 -tuples_on BOOLEAN),BOOLEAN))
K217() is set
1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((1 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((1 -tuples_on BOOLEAN),BOOLEAN)) is set
f1 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f3 is boolean Element of BOOLEAN
<*f3*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
f2 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f2 . <*f3*> is boolean set
f0 is Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() Element of 1 -tuples_on BOOLEAN
f0 . 1 is set
F₁((f0 . 1)) is boolean Element of BOOLEAN
F₁(f3) is boolean Element of BOOLEAN
1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((1 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((1 -tuples_on BOOLEAN),BOOLEAN)) is set
f1 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f2 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f3 is Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() Element of 1 -tuples_on BOOLEAN
f0 is boolean Element of BOOLEAN
<*f0*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
f1 . f3 is boolean Element of BOOLEAN
F₁(f0) is boolean Element of BOOLEAN
f2 . f3 is boolean Element of BOOLEAN
1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((1 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((1 -tuples_on BOOLEAN),BOOLEAN)) is set
f1 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f3 is boolean Element of BOOLEAN
<*f3*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
f2 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f2 . <*f3*> is boolean set
f0 is Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() Element of 1 -tuples_on BOOLEAN
f0 . 1 is set
F₁((f0 . 1)) is boolean Element of BOOLEAN
F₁(f3) is boolean Element of BOOLEAN
f2 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f3 is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
f0 is Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() Element of 1 -tuples_on BOOLEAN
x is boolean Element of BOOLEAN
<*x*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
f2 . f0 is boolean Element of BOOLEAN
F₁(x) is boolean Element of BOOLEAN
f3 . f0 is boolean Element of BOOLEAN
1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((1 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((1 -tuples_on BOOLEAN),BOOLEAN)) is set
() is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
<*0*> is non empty Relation-like NAT -defined NAT -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() nonpair-yielding FinSequence of NAT
() . <*0*> is boolean set
<*1*> is non empty Relation-like NAT -defined NAT -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() nonpair-yielding FinSequence of NAT
() . <*1*> is boolean set
f1 is boolean Element of BOOLEAN
<*f1*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
() . <*f1*> is boolean set
'not' f1 is boolean Element of BOOLEAN
K114(1,f1) is set
<*f1,f1*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
nand2 . <*f1,f1*> is boolean set
f1 '&' f1 is boolean Element of BOOLEAN
K111(f1,f1) is set
'not' (f1 '&' f1) is boolean Element of BOOLEAN
K114(1,(f1 '&' f1)) is set
FALSE is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
K114(1,FALSE) is set
'not' TRUE is boolean Element of BOOLEAN
K114(1,TRUE) is set
() is Relation-like Function-like V27(1 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((1 -tuples_on BOOLEAN),BOOLEAN))
() . <*0*> is boolean set
() . <*1*> is boolean set
f1 is boolean Element of BOOLEAN
<*f1*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
() . <*f1*> is boolean set
<*f1,f1*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
and2 . <*f1,f1*> is boolean set
f1 '&' f1 is boolean Element of BOOLEAN
K111(f1,f1) is set
FALSE is boolean Element of BOOLEAN
() is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
<*0,0*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() nonpair-yielding set
() . <*0,0*> is boolean set
<*0,1*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() nonpair-yielding set
() . <*0,1*> is boolean set
<*1,0*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() nonpair-yielding set
() . <*1,0*> is boolean set
<*1,1*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() nonpair-yielding set
() . <*1,1*> is boolean set
f1 is boolean Element of BOOLEAN
f2 is boolean Element of BOOLEAN
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
() . <*f1,f2*> is boolean set
'not' f2 is boolean Element of BOOLEAN
K114(1,f2) is set
f1 '&' ('not' f2) is boolean Element of BOOLEAN
K111(f1,('not' f2)) is set
<*f2,f1*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
and2a . <*f2,f1*> is boolean set
nor2a . <*f1,f2*> is boolean set
'not' f1 is boolean Element of BOOLEAN
K114(1,f1) is set
'not' ('not' f2) is boolean Element of BOOLEAN
K114(1,('not' f2)) is set
('not' f1) 'or' ('not' ('not' f2)) is boolean Element of BOOLEAN
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
'not' ('not' ('not' f2)) is boolean set
K114(1,('not' ('not' f2))) is set
('not' ('not' f1)) '&' ('not' ('not' ('not' f2))) is set
K111(('not' ('not' f1)),('not' ('not' ('not' f2)))) is set
'not' (('not' ('not' f1)) '&' ('not' ('not' ('not' f2)))) is boolean set
'not' (('not' f1) 'or' ('not' ('not' f2))) is boolean Element of BOOLEAN
K114(1,(('not' f1) 'or' ('not' ('not' f2)))) is set
FALSE is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
K114(1,FALSE) is set
FALSE '&' ('not' FALSE) is boolean Element of BOOLEAN
K111(FALSE,('not' FALSE)) is set
'not' TRUE is boolean Element of BOOLEAN
K114(1,TRUE) is set
FALSE '&' ('not' TRUE) is boolean Element of BOOLEAN
K111(FALSE,('not' TRUE)) is set
TRUE '&' ('not' FALSE) is boolean Element of BOOLEAN
K111(TRUE,('not' FALSE)) is set
TRUE '&' ('not' TRUE) is boolean Element of BOOLEAN
K111(TRUE,('not' TRUE)) is set
() is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
() . <*0,0*> is boolean set
() . <*0,1*> is boolean set
() . <*1,0*> is boolean set
() . <*1,1*> is boolean set
f1 is boolean Element of BOOLEAN
f2 is boolean Element of BOOLEAN
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
() . <*f1,f2*> is boolean set
'not' f2 is boolean Element of BOOLEAN
K114(1,f2) is set
f1 'xor' ('not' f2) is boolean Element of BOOLEAN
K222(f1,('not' f2)) is set
K221(f1,('not' f2)) is set
'not' f1 is boolean set
K114(1,f1) is set
K220(('not' f1),('not' f2)) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' f1)) '&' ('not' ('not' f2)) is set
K111(('not' ('not' f1)),('not' ('not' f2))) is set
'not' (('not' ('not' f1)) '&' ('not' ('not' f2))) is boolean set
K221(('not' f2),f1) is set
K220(('not' ('not' f2)),f1) is set
'not' ('not' ('not' f2)) is boolean set
K114(1,('not' ('not' f2))) is set
('not' ('not' ('not' f2))) '&' ('not' f1) is set
K111(('not' ('not' ('not' f2))),('not' f1)) is set
'not' (('not' ('not' ('not' f2))) '&' ('not' f1)) is boolean set
K221(f1,('not' f2)) '&' K221(('not' f2),f1) is set
'not' K222(f1,('not' f2)) is boolean set
xor2a . <*f1,f2*> is boolean set
and2b . <*f1,f2*> is boolean set
and2 . <*f1,f2*> is boolean set
<*(and2b . <*f1,f2*>),(and2 . <*f1,f2*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
or2 . <*(and2b . <*f1,f2*>),(and2 . <*f1,f2*>)*> is boolean set
'not' f1 is boolean Element of BOOLEAN
('not' f1) 'xor' f2 is boolean Element of BOOLEAN
K222(('not' f1),f2) is set
K221(('not' f1),f2) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
K220(('not' ('not' f1)),f2) is set
'not' ('not' ('not' f1)) is boolean set
K114(1,('not' ('not' f1))) is set
'not' f2 is boolean set
('not' ('not' ('not' f1))) '&' ('not' f2) is set
K111(('not' ('not' ('not' f1))),('not' f2)) is set
'not' (('not' ('not' ('not' f1))) '&' ('not' f2)) is boolean set
K221(f2,('not' f1)) is set
K220(('not' f2),('not' f1)) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' f2)) '&' ('not' ('not' f1)) is set
K111(('not' ('not' f2)),('not' ('not' f1))) is set
'not' (('not' ('not' f2)) '&' ('not' ('not' f1))) is boolean set
K221(('not' f1),f2) '&' K221(f2,('not' f1)) is set
'not' K222(('not' f1),f2) is boolean set
('not' f1) '&' ('not' f2) is boolean Element of BOOLEAN
K111(('not' f1),('not' f2)) is set
'not' ('not' f2) is boolean Element of BOOLEAN
f1 '&' ('not' ('not' f2)) is boolean Element of BOOLEAN
K111(f1,('not' ('not' f2))) is set
(('not' f1) '&' ('not' f2)) 'or' (f1 '&' ('not' ('not' f2))) is boolean Element of BOOLEAN
'not' (('not' f1) '&' ('not' f2)) is boolean set
K114(1,(('not' f1) '&' ('not' f2))) is set
'not' (f1 '&' ('not' ('not' f2))) is boolean set
K114(1,(f1 '&' ('not' ('not' f2)))) is set
('not' (('not' f1) '&' ('not' f2))) '&' ('not' (f1 '&' ('not' ('not' f2)))) is set
K111(('not' (('not' f1) '&' ('not' f2))),('not' (f1 '&' ('not' ('not' f2))))) is set
'not' (('not' (('not' f1) '&' ('not' f2))) '&' ('not' (f1 '&' ('not' ('not' f2))))) is boolean set
f1 '&' f2 is boolean Element of BOOLEAN
K111(f1,f2) is set
<*(('not' f1) '&' ('not' f2)),(f1 '&' f2)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
or2 . <*(('not' f1) '&' ('not' f2)),(f1 '&' f2)*> is boolean set
<*(and2b . <*f1,f2*>),(f1 '&' f2)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
or2 . <*(and2b . <*f1,f2*>),(f1 '&' f2)*> is boolean set
FALSE is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
K114(1,FALSE) is set
FALSE 'xor' ('not' FALSE) is boolean Element of BOOLEAN
K222(FALSE,('not' FALSE)) is set
K221(FALSE,('not' FALSE)) is set
'not' FALSE is boolean set
K220(('not' FALSE),('not' FALSE)) is set
'not' ('not' FALSE) is boolean set
K114(1,('not' FALSE)) is set
'not' ('not' FALSE) is boolean set
K114(1,('not' FALSE)) is set
('not' ('not' FALSE)) '&' ('not' ('not' FALSE)) is set
K111(('not' ('not' FALSE)),('not' ('not' FALSE))) is set
'not' (('not' ('not' FALSE)) '&' ('not' ('not' FALSE))) is boolean set
K221(('not' FALSE),FALSE) is set
K220(('not' ('not' FALSE)),FALSE) is set
'not' ('not' ('not' FALSE)) is boolean set
K114(1,('not' ('not' FALSE))) is set
('not' ('not' ('not' FALSE))) '&' ('not' FALSE) is set
K111(('not' ('not' ('not' FALSE))),('not' FALSE)) is set
'not' (('not' ('not' ('not' FALSE))) '&' ('not' FALSE)) is boolean set
K221(FALSE,('not' FALSE)) '&' K221(('not' FALSE),FALSE) is set
'not' K222(FALSE,('not' FALSE)) is boolean set
'not' TRUE is boolean Element of BOOLEAN
K114(1,TRUE) is set
FALSE 'xor' ('not' TRUE) is boolean Element of BOOLEAN
K222(FALSE,('not' TRUE)) is set
K221(FALSE,('not' TRUE)) is set
K220(('not' FALSE),('not' TRUE)) is set
'not' ('not' TRUE) is boolean set
K114(1,('not' TRUE)) is set
('not' ('not' FALSE)) '&' ('not' ('not' TRUE)) is set
K111(('not' ('not' FALSE)),('not' ('not' TRUE))) is set
'not' (('not' ('not' FALSE)) '&' ('not' ('not' TRUE))) is boolean set
K221(('not' TRUE),FALSE) is set
K220(('not' ('not' TRUE)),FALSE) is set
'not' ('not' ('not' TRUE)) is boolean set
K114(1,('not' ('not' TRUE))) is set
('not' ('not' ('not' TRUE))) '&' ('not' FALSE) is set
K111(('not' ('not' ('not' TRUE))),('not' FALSE)) is set
'not' (('not' ('not' ('not' TRUE))) '&' ('not' FALSE)) is boolean set
K221(FALSE,('not' TRUE)) '&' K221(('not' TRUE),FALSE) is set
'not' K222(FALSE,('not' TRUE)) is boolean set
TRUE 'xor' ('not' FALSE) is boolean Element of BOOLEAN
K222(TRUE,('not' FALSE)) is set
K221(TRUE,('not' FALSE)) is set
'not' TRUE is boolean set
K220(('not' TRUE),('not' FALSE)) is set
'not' ('not' TRUE) is boolean set
K114(1,('not' TRUE)) is set
('not' ('not' TRUE)) '&' ('not' ('not' FALSE)) is set
K111(('not' ('not' TRUE)),('not' ('not' FALSE))) is set
'not' (('not' ('not' TRUE)) '&' ('not' ('not' FALSE))) is boolean set
K221(('not' FALSE),TRUE) is set
K220(('not' ('not' FALSE)),TRUE) is set
('not' ('not' ('not' FALSE))) '&' ('not' TRUE) is set
K111(('not' ('not' ('not' FALSE))),('not' TRUE)) is set
'not' (('not' ('not' ('not' FALSE))) '&' ('not' TRUE)) is boolean set
K221(TRUE,('not' FALSE)) '&' K221(('not' FALSE),TRUE) is set
'not' K222(TRUE,('not' FALSE)) is boolean set
TRUE 'xor' ('not' TRUE) is boolean Element of BOOLEAN
K222(TRUE,('not' TRUE)) is set
K221(TRUE,('not' TRUE)) is set
K220(('not' TRUE),('not' TRUE)) is set
('not' ('not' TRUE)) '&' ('not' ('not' TRUE)) is set
K111(('not' ('not' TRUE)),('not' ('not' TRUE))) is set
'not' (('not' ('not' TRUE)) '&' ('not' ('not' TRUE))) is boolean set
K221(('not' TRUE),TRUE) is set
K220(('not' ('not' TRUE)),TRUE) is set
('not' ('not' ('not' TRUE))) '&' ('not' TRUE) is set
K111(('not' ('not' ('not' TRUE))),('not' TRUE)) is set
'not' (('not' ('not' ('not' TRUE))) '&' ('not' TRUE)) is boolean set
K221(TRUE,('not' TRUE)) '&' K221(('not' TRUE),TRUE) is set
'not' K222(TRUE,('not' TRUE)) is boolean set
f1 is boolean Element of BOOLEAN
f2 is boolean Element of BOOLEAN
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*f1,f2*> is boolean set
<*(xor2 . <*f1,f2*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
() . <*(xor2 . <*f1,f2*>)*> is boolean set
xor2a . <*f1,f2*> is boolean set
() . <*f1,f2*> is boolean set
<*f1*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
() . <*f1*> is boolean set
<*f2*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
() . <*f2*> is boolean set
<*(() . <*f1*>),(() . <*f2*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*(() . <*f1*>),(() . <*f2*>)*> is boolean set
f1 'xor' f2 is boolean Element of BOOLEAN
K222(f1,f2) is set
K221(f1,f2) is set
'not' f1 is boolean set
K114(1,f1) is set
K220(('not' f1),f2) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
'not' f2 is boolean set
K114(1,f2) is set
('not' ('not' f1)) '&' ('not' f2) is set
K111(('not' ('not' f1)),('not' f2)) is set
'not' (('not' ('not' f1)) '&' ('not' f2)) is boolean set
K221(f2,f1) is set
K220(('not' f2),f1) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' f2)) '&' ('not' f1) is set
K111(('not' ('not' f2)),('not' f1)) is set
'not' (('not' ('not' f2)) '&' ('not' f1)) is boolean set
K221(f1,f2) '&' K221(f2,f1) is set
'not' K222(f1,f2) is boolean set
<*(f1 'xor' f2)*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
() . <*(f1 'xor' f2)*> is boolean set
'not' (f1 'xor' f2) is boolean Element of BOOLEAN
K114(1,(f1 'xor' f2)) is set
'not' f1 is boolean Element of BOOLEAN
('not' f1) 'xor' f2 is boolean Element of BOOLEAN
K222(('not' f1),f2) is set
K221(('not' f1),f2) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
K220(('not' ('not' f1)),f2) is set
'not' ('not' ('not' f1)) is boolean set
K114(1,('not' ('not' f1))) is set
('not' ('not' ('not' f1))) '&' ('not' f2) is set
K111(('not' ('not' ('not' f1))),('not' f2)) is set
'not' (('not' ('not' ('not' f1))) '&' ('not' f2)) is boolean set
K221(f2,('not' f1)) is set
K220(('not' f2),('not' f1)) is set
('not' ('not' f2)) '&' ('not' ('not' f1)) is set
K111(('not' ('not' f2)),('not' ('not' f1))) is set
'not' (('not' ('not' f2)) '&' ('not' ('not' f1))) is boolean set
K221(('not' f1),f2) '&' K221(f2,('not' f1)) is set
'not' K222(('not' f1),f2) is boolean set
<*('not' f1),(() . <*f2*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*('not' f1),(() . <*f2*>)*> is boolean set
'not' f2 is boolean Element of BOOLEAN
<*('not' f1),('not' f2)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*('not' f1),('not' f2)*> is boolean set
('not' f1) 'xor' ('not' f2) is boolean Element of BOOLEAN
K222(('not' f1),('not' f2)) is set
K221(('not' f1),('not' f2)) is set
K220(('not' ('not' f1)),('not' f2)) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' ('not' f1))) '&' ('not' ('not' f2)) is set
K111(('not' ('not' ('not' f1))),('not' ('not' f2))) is set
'not' (('not' ('not' ('not' f1))) '&' ('not' ('not' f2))) is boolean set
K221(('not' f2),('not' f1)) is set
K220(('not' ('not' f2)),('not' f1)) is set
'not' ('not' ('not' f2)) is boolean set
K114(1,('not' ('not' f2))) is set
('not' ('not' ('not' f2))) '&' ('not' ('not' f1)) is set
K111(('not' ('not' ('not' f2))),('not' ('not' f1))) is set
'not' (('not' ('not' ('not' f2))) '&' ('not' ('not' f1))) is boolean set
K221(('not' f1),('not' f2)) '&' K221(('not' f2),('not' f1)) is set
'not' K222(('not' f1),('not' f2)) is boolean set
f1 is boolean Element of BOOLEAN
f2 is boolean Element of BOOLEAN
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
() . <*f1,f2*> is boolean set
f3 is boolean Element of BOOLEAN
<*(() . <*f1,f2*>),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*(() . <*f1,f2*>),f3*> is boolean set
<*(xor2 . <*(() . <*f1,f2*>),f3*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
() . <*(xor2 . <*(() . <*f1,f2*>),f3*>)*> is boolean set
() . <*(() . <*f1,f2*>),f3*> is boolean set
'not' f2 is boolean Element of BOOLEAN
K114(1,f2) is set
f1 'xor' ('not' f2) is boolean Element of BOOLEAN
K222(f1,('not' f2)) is set
K221(f1,('not' f2)) is set
'not' f1 is boolean set
K114(1,f1) is set
K220(('not' f1),('not' f2)) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' f1)) '&' ('not' ('not' f2)) is set
K111(('not' ('not' f1)),('not' ('not' f2))) is set
'not' (('not' ('not' f1)) '&' ('not' ('not' f2))) is boolean set
K221(('not' f2),f1) is set
K220(('not' ('not' f2)),f1) is set
'not' ('not' ('not' f2)) is boolean set
K114(1,('not' ('not' f2))) is set
('not' ('not' ('not' f2))) '&' ('not' f1) is set
K111(('not' ('not' ('not' f2))),('not' f1)) is set
'not' (('not' ('not' ('not' f2))) '&' ('not' f1)) is boolean set
K221(f1,('not' f2)) '&' K221(('not' f2),f1) is set
'not' K222(f1,('not' f2)) is boolean set
<*(f1 'xor' ('not' f2)),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*(f1 'xor' ('not' f2)),f3*> is boolean set
<*(xor2 . <*(f1 'xor' ('not' f2)),f3*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
() . <*(xor2 . <*(f1 'xor' ('not' f2)),f3*>)*> is boolean set
(f1 'xor' ('not' f2)) 'xor' f3 is boolean Element of BOOLEAN
K222((f1 'xor' ('not' f2)),f3) is set
K221((f1 'xor' ('not' f2)),f3) is set
'not' (f1 'xor' ('not' f2)) is boolean set
K114(1,(f1 'xor' ('not' f2))) is set
K220(('not' (f1 'xor' ('not' f2))),f3) is set
'not' ('not' (f1 'xor' ('not' f2))) is boolean set
K114(1,('not' (f1 'xor' ('not' f2)))) is set
'not' f3 is boolean set
K114(1,f3) is set
('not' ('not' (f1 'xor' ('not' f2)))) '&' ('not' f3) is set
K111(('not' ('not' (f1 'xor' ('not' f2)))),('not' f3)) is set
'not' (('not' ('not' (f1 'xor' ('not' f2)))) '&' ('not' f3)) is boolean set
K221(f3,(f1 'xor' ('not' f2))) is set
K220(('not' f3),(f1 'xor' ('not' f2))) is set
'not' ('not' f3) is boolean set
K114(1,('not' f3)) is set
('not' ('not' f3)) '&' ('not' (f1 'xor' ('not' f2))) is set
K111(('not' ('not' f3)),('not' (f1 'xor' ('not' f2)))) is set
'not' (('not' ('not' f3)) '&' ('not' (f1 'xor' ('not' f2)))) is boolean set
K221((f1 'xor' ('not' f2)),f3) '&' K221(f3,(f1 'xor' ('not' f2))) is set
'not' K222((f1 'xor' ('not' f2)),f3) is boolean set
<*((f1 'xor' ('not' f2)) 'xor' f3)*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
() . <*((f1 'xor' ('not' f2)) 'xor' f3)*> is boolean set
'not' ((f1 'xor' ('not' f2)) 'xor' f3) is boolean Element of BOOLEAN
K114(1,((f1 'xor' ('not' f2)) 'xor' f3)) is set
'not' f3 is boolean Element of BOOLEAN
(f1 'xor' ('not' f2)) 'xor' ('not' f3) is boolean Element of BOOLEAN
K222((f1 'xor' ('not' f2)),('not' f3)) is set
K221((f1 'xor' ('not' f2)),('not' f3)) is set
K220(('not' (f1 'xor' ('not' f2))),('not' f3)) is set
'not' ('not' f3) is boolean set
K114(1,('not' f3)) is set
('not' ('not' (f1 'xor' ('not' f2)))) '&' ('not' ('not' f3)) is set
K111(('not' ('not' (f1 'xor' ('not' f2)))),('not' ('not' f3))) is set
'not' (('not' ('not' (f1 'xor' ('not' f2)))) '&' ('not' ('not' f3))) is boolean set
K221(('not' f3),(f1 'xor' ('not' f2))) is set
K220(('not' ('not' f3)),(f1 'xor' ('not' f2))) is set
'not' ('not' ('not' f3)) is boolean set
K114(1,('not' ('not' f3))) is set
('not' ('not' ('not' f3))) '&' ('not' (f1 'xor' ('not' f2))) is set
K111(('not' ('not' ('not' f3))),('not' (f1 'xor' ('not' f2)))) is set
'not' (('not' ('not' ('not' f3))) '&' ('not' (f1 'xor' ('not' f2)))) is boolean set
K221((f1 'xor' ('not' f2)),('not' f3)) '&' K221(('not' f3),(f1 'xor' ('not' f2))) is set
'not' K222((f1 'xor' ('not' f2)),('not' f3)) is boolean set
() . <*(f1 'xor' ('not' f2)),f3*> is boolean set
f1 is boolean Element of BOOLEAN
'not' f1 is boolean Element of BOOLEAN
K114(1,f1) is set
f2 is boolean Element of BOOLEAN
('not' f1) 'xor' f2 is boolean Element of BOOLEAN
K222(('not' f1),f2) is set
K221(('not' f1),f2) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
K220(('not' ('not' f1)),f2) is set
'not' ('not' ('not' f1)) is boolean set
K114(1,('not' ('not' f1))) is set
'not' f2 is boolean set
K114(1,f2) is set
('not' ('not' ('not' f1))) '&' ('not' f2) is set
K111(('not' ('not' ('not' f1))),('not' f2)) is set
'not' (('not' ('not' ('not' f1))) '&' ('not' f2)) is boolean set
K221(f2,('not' f1)) is set
K220(('not' f2),('not' f1)) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' f2)) '&' ('not' ('not' f1)) is set
K111(('not' ('not' f2)),('not' ('not' f1))) is set
'not' (('not' ('not' f2)) '&' ('not' ('not' f1))) is boolean set
K221(('not' f1),f2) '&' K221(f2,('not' f1)) is set
'not' K222(('not' f1),f2) is boolean set
f3 is boolean Element of BOOLEAN
'not' f3 is boolean Element of BOOLEAN
K114(1,f3) is set
(('not' f1) 'xor' f2) 'xor' ('not' f3) is boolean Element of BOOLEAN
K222((('not' f1) 'xor' f2),('not' f3)) is set
K221((('not' f1) 'xor' f2),('not' f3)) is set
'not' (('not' f1) 'xor' f2) is boolean set
K114(1,(('not' f1) 'xor' f2)) is set
K220(('not' (('not' f1) 'xor' f2)),('not' f3)) is set
'not' ('not' (('not' f1) 'xor' f2)) is boolean set
K114(1,('not' (('not' f1) 'xor' f2))) is set
'not' ('not' f3) is boolean set
K114(1,('not' f3)) is set
('not' ('not' (('not' f1) 'xor' f2))) '&' ('not' ('not' f3)) is set
K111(('not' ('not' (('not' f1) 'xor' f2))),('not' ('not' f3))) is set
'not' (('not' ('not' (('not' f1) 'xor' f2))) '&' ('not' ('not' f3))) is boolean set
K221(('not' f3),(('not' f1) 'xor' f2)) is set
K220(('not' ('not' f3)),(('not' f1) 'xor' f2)) is set
'not' ('not' ('not' f3)) is boolean set
K114(1,('not' ('not' f3))) is set
('not' ('not' ('not' f3))) '&' ('not' (('not' f1) 'xor' f2)) is set
K111(('not' ('not' ('not' f3))),('not' (('not' f1) 'xor' f2))) is set
'not' (('not' ('not' ('not' f3))) '&' ('not' (('not' f1) 'xor' f2))) is boolean set
K221((('not' f1) 'xor' f2),('not' f3)) '&' K221(('not' f3),(('not' f1) 'xor' f2)) is set
'not' K222((('not' f1) 'xor' f2),('not' f3)) is boolean set
'not' f2 is boolean Element of BOOLEAN
f1 'xor' ('not' f2) is boolean Element of BOOLEAN
K222(f1,('not' f2)) is set
K221(f1,('not' f2)) is set
'not' f1 is boolean set
K220(('not' f1),('not' f2)) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' f1)) '&' ('not' ('not' f2)) is set
K111(('not' ('not' f1)),('not' ('not' f2))) is set
'not' (('not' ('not' f1)) '&' ('not' ('not' f2))) is boolean set
K221(('not' f2),f1) is set
K220(('not' ('not' f2)),f1) is set
'not' ('not' ('not' f2)) is boolean set
K114(1,('not' ('not' f2))) is set
('not' ('not' ('not' f2))) '&' ('not' f1) is set
K111(('not' ('not' ('not' f2))),('not' f1)) is set
'not' (('not' ('not' ('not' f2))) '&' ('not' f1)) is boolean set
K221(f1,('not' f2)) '&' K221(('not' f2),f1) is set
'not' K222(f1,('not' f2)) is boolean set
(f1 'xor' ('not' f2)) 'xor' ('not' f3) is boolean Element of BOOLEAN
K222((f1 'xor' ('not' f2)),('not' f3)) is set
K221((f1 'xor' ('not' f2)),('not' f3)) is set
'not' (f1 'xor' ('not' f2)) is boolean set
K114(1,(f1 'xor' ('not' f2))) is set
K220(('not' (f1 'xor' ('not' f2))),('not' f3)) is set
'not' ('not' (f1 'xor' ('not' f2))) is boolean set
K114(1,('not' (f1 'xor' ('not' f2)))) is set
('not' ('not' (f1 'xor' ('not' f2)))) '&' ('not' ('not' f3)) is set
K111(('not' ('not' (f1 'xor' ('not' f2)))),('not' ('not' f3))) is set
'not' (('not' ('not' (f1 'xor' ('not' f2)))) '&' ('not' ('not' f3))) is boolean set
K221(('not' f3),(f1 'xor' ('not' f2))) is set
K220(('not' ('not' f3)),(f1 'xor' ('not' f2))) is set
('not' ('not' ('not' f3))) '&' ('not' (f1 'xor' ('not' f2))) is set
K111(('not' ('not' ('not' f3))),('not' (f1 'xor' ('not' f2)))) is set
'not' (('not' ('not' ('not' f3))) '&' ('not' (f1 'xor' ('not' f2)))) is boolean set
K221((f1 'xor' ('not' f2)),('not' f3)) '&' K221(('not' f3),(f1 'xor' ('not' f2))) is set
'not' K222((f1 'xor' ('not' f2)),('not' f3)) is boolean set
f1 is boolean Element of BOOLEAN
f2 is boolean Element of BOOLEAN
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2a . <*f1,f2*> is boolean set
f3 is boolean Element of BOOLEAN
<*(xor2a . <*f1,f2*>),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
() . <*(xor2a . <*f1,f2*>),f3*> is boolean set
() . <*f1,f2*> is boolean set
<*(() . <*f1,f2*>),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
() . <*(() . <*f1,f2*>),f3*> is boolean set
f1 is boolean Element of BOOLEAN
f2 is boolean Element of BOOLEAN
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2b . <*f1,f2*> is boolean set
f3 is boolean Element of BOOLEAN
<*(xor2b . <*f1,f2*>),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
() . <*(xor2b . <*f1,f2*>),f3*> is boolean set
<*(() . <*(xor2b . <*f1,f2*>),f3*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
() . <*(() . <*(xor2b . <*f1,f2*>),f3*>)*> is boolean set
xor2 . <*f1,f2*> is boolean set
<*(xor2 . <*f1,f2*>),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*(xor2 . <*f1,f2*>),f3*> is boolean set
'not' f1 is boolean Element of BOOLEAN
K114(1,f1) is set
'not' f2 is boolean Element of BOOLEAN
K114(1,f2) is set
('not' f1) 'xor' ('not' f2) is boolean Element of BOOLEAN
K222(('not' f1),('not' f2)) is set
K221(('not' f1),('not' f2)) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
K220(('not' ('not' f1)),('not' f2)) is set
'not' ('not' ('not' f1)) is boolean set
K114(1,('not' ('not' f1))) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' ('not' f1))) '&' ('not' ('not' f2)) is set
K111(('not' ('not' ('not' f1))),('not' ('not' f2))) is set
'not' (('not' ('not' ('not' f1))) '&' ('not' ('not' f2))) is boolean set
K221(('not' f2),('not' f1)) is set
K220(('not' ('not' f2)),('not' f1)) is set
'not' ('not' ('not' f2)) is boolean set
K114(1,('not' ('not' f2))) is set
('not' ('not' ('not' f2))) '&' ('not' ('not' f1)) is set
K111(('not' ('not' ('not' f2))),('not' ('not' f1))) is set
'not' (('not' ('not' ('not' f2))) '&' ('not' ('not' f1))) is boolean set
K221(('not' f1),('not' f2)) '&' K221(('not' f2),('not' f1)) is set
'not' K222(('not' f1),('not' f2)) is boolean set
<*(('not' f1) 'xor' ('not' f2)),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
() . <*(('not' f1) 'xor' ('not' f2)),f3*> is boolean set
<*(() . <*(('not' f1) 'xor' ('not' f2)),f3*>)*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
() . <*(() . <*(('not' f1) 'xor' ('not' f2)),f3*>)*> is boolean set
'not' f3 is boolean Element of BOOLEAN
K114(1,f3) is set
(('not' f1) 'xor' ('not' f2)) 'xor' ('not' f3) is boolean Element of BOOLEAN
K222((('not' f1) 'xor' ('not' f2)),('not' f3)) is set
K221((('not' f1) 'xor' ('not' f2)),('not' f3)) is set
'not' (('not' f1) 'xor' ('not' f2)) is boolean set
K114(1,(('not' f1) 'xor' ('not' f2))) is set
K220(('not' (('not' f1) 'xor' ('not' f2))),('not' f3)) is set
'not' ('not' (('not' f1) 'xor' ('not' f2))) is boolean set
K114(1,('not' (('not' f1) 'xor' ('not' f2)))) is set
'not' ('not' f3) is boolean set
K114(1,('not' f3)) is set
('not' ('not' (('not' f1) 'xor' ('not' f2)))) '&' ('not' ('not' f3)) is set
K111(('not' ('not' (('not' f1) 'xor' ('not' f2)))),('not' ('not' f3))) is set
'not' (('not' ('not' (('not' f1) 'xor' ('not' f2)))) '&' ('not' ('not' f3))) is boolean set
K221(('not' f3),(('not' f1) 'xor' ('not' f2))) is set
K220(('not' ('not' f3)),(('not' f1) 'xor' ('not' f2))) is set
'not' ('not' ('not' f3)) is boolean set
K114(1,('not' ('not' f3))) is set
('not' ('not' ('not' f3))) '&' ('not' (('not' f1) 'xor' ('not' f2))) is set
K111(('not' ('not' ('not' f3))),('not' (('not' f1) 'xor' ('not' f2)))) is set
'not' (('not' ('not' ('not' f3))) '&' ('not' (('not' f1) 'xor' ('not' f2)))) is boolean set
K221((('not' f1) 'xor' ('not' f2)),('not' f3)) '&' K221(('not' f3),(('not' f1) 'xor' ('not' f2))) is set
'not' K222((('not' f1) 'xor' ('not' f2)),('not' f3)) is boolean set
<*((('not' f1) 'xor' ('not' f2)) 'xor' ('not' f3))*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() FinSequence of BOOLEAN
() . <*((('not' f1) 'xor' ('not' f2)) 'xor' ('not' f3))*> is boolean set
'not' ((('not' f1) 'xor' ('not' f2)) 'xor' ('not' f3)) is boolean Element of BOOLEAN
K114(1,((('not' f1) 'xor' ('not' f2)) 'xor' ('not' f3))) is set
f1 'xor' f2 is boolean Element of BOOLEAN
K222(f1,f2) is set
K221(f1,f2) is set
'not' f1 is boolean set
K220(('not' f1),f2) is set
'not' ('not' f1) is boolean set
K114(1,('not' f1)) is set
'not' f2 is boolean set
('not' ('not' f1)) '&' ('not' f2) is set
K111(('not' ('not' f1)),('not' f2)) is set
'not' (('not' ('not' f1)) '&' ('not' f2)) is boolean set
K221(f2,f1) is set
K220(('not' f2),f1) is set
'not' ('not' f2) is boolean set
K114(1,('not' f2)) is set
('not' ('not' f2)) '&' ('not' f1) is set
K111(('not' ('not' f2)),('not' f1)) is set
'not' (('not' ('not' f2)) '&' ('not' f1)) is boolean set
K221(f1,f2) '&' K221(f2,f1) is set
'not' K222(f1,f2) is boolean set
(f1 'xor' f2) 'xor' f3 is boolean Element of BOOLEAN
K222((f1 'xor' f2),f3) is set
K221((f1 'xor' f2),f3) is set
'not' (f1 'xor' f2) is boolean set
K114(1,(f1 'xor' f2)) is set
K220(('not' (f1 'xor' f2)),f3) is set
'not' ('not' (f1 'xor' f2)) is boolean set
K114(1,('not' (f1 'xor' f2))) is set
'not' f3 is boolean set
('not' ('not' (f1 'xor' f2))) '&' ('not' f3) is set
K111(('not' ('not' (f1 'xor' f2))),('not' f3)) is set
'not' (('not' ('not' (f1 'xor' f2))) '&' ('not' f3)) is boolean set
K221(f3,(f1 'xor' f2)) is set
K220(('not' f3),(f1 'xor' f2)) is set
'not' ('not' f3) is boolean set
K114(1,('not' f3)) is set
('not' ('not' f3)) '&' ('not' (f1 'xor' f2)) is set
K111(('not' ('not' f3)),('not' (f1 'xor' f2))) is set
'not' (('not' ('not' f3)) '&' ('not' (f1 'xor' f2))) is boolean set
K221((f1 'xor' f2),f3) '&' K221(f3,(f1 'xor' f2)) is set
'not' K222((f1 'xor' f2),f3) is boolean set
<*(f1 'xor' f2),f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
xor2 . <*(f1 'xor' f2),f3*> is boolean set
f2 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
f3 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
f1 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
f0 is set
x is set
y is set
<*x,y*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
[<*x,y*>,f2] is non empty pair set
{<*x,y*>,f2} is functional set
{<*x,y*>} is functional V49() set
{{<*x,y*>,f2},{<*x,y*>}} is set
<*y,f0*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
[<*y,f0*>,f3] is non empty pair set
{<*y,f0*>,f3} is functional set
{<*y,f0*>} is functional V49() set
{{<*y,f0*>,f3},{<*y,f0*>}} is set
<*f0,x*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
[<*f0,x*>,f1] is non empty pair set
{<*f0,x*>,f1} is functional set
{<*f0,x*>} is functional V49() set
{{<*f0,x*>,f1},{<*f0,x*>}} is set
{x,y} is set
{[<*f0,x*>,f1],[<*x,y*>,f2]} is Relation-like set
{f0,x,y} is set
dom <*f0,x*> is non empty V51() Element of K18(NAT)
Seg 2 is non empty V36() V43(2) V51() Element of K18(NAT)
<*f0,x*> . 2 is set
[2,x] is non empty pair set
{2,x} is set
{2} is non with_pair set
{{2,x},{2}} is set
{2,y} is set
[2,y] is non empty pair set
{{2,y},{2}} is set
<*y*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
[1,y] is non empty pair set
{1,y} is set
{1} is non with_pair set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like set
<*f0*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
[1,f0] is non empty pair set
{1,f0} is set
{{1,f0},{1}} is set
{[1,f0]} is Relation-like Function-like set
dom <*y,f0*> is non empty V51() Element of K18(NAT)
<*y,f0*> . 2 is set
[2,f0] is non empty pair set
{2,f0} is set
{{2,f0},{2}} is set
<*y*> ^ <*f0*> is non empty Relation-like NAT -defined Function-like V36() V43(1 + 1) FinSequence-like FinSubsequence-like V51() set
1 + 1 is V9() V10() V11() V15() non pair Element of NAT
dom <*x,y*> is non empty V51() Element of K18(NAT)
<*x,y*> . 2 is set
<*x*> is non empty Relation-like NAT -defined Function-like V36() V43(1) FinSequence-like FinSubsequence-like V51() set
<*f0*> ^ <*x*> is non empty Relation-like NAT -defined Function-like V36() V43(1 + 1) FinSequence-like FinSubsequence-like V51() set
f1 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
f2 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
f3 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
f0 is Relation-like Function-like V27(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((3 -tuples_on BOOLEAN),BOOLEAN))
x is set
y is set
z is set
{x,y,z} is set
<*x,y*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
[<*x,y*>,f1] is non empty pair set
{<*x,y*>,f1} is functional set
{<*x,y*>} is functional V49() set
{{<*x,y*>,f1},{<*x,y*>}} is set
<*y,z*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
[<*y,z*>,f2] is non empty pair set
{<*y,z*>,f2} is functional set
{<*y,z*>} is functional V49() set
{{<*y,z*>,f2},{<*y,z*>}} is set
<*z,x*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
[<*z,x*>,f3] is non empty pair set
{<*z,x*>,f3} is functional set
{<*z,x*>} is functional V49() set
{{<*z,x*>,f3},{<*z,x*>}} is set
<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> is non empty Relation-like NAT -defined Function-like V36() V43(3) FinSequence-like FinSubsequence-like V51() set
[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f0] is non empty pair set
{<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f0} is functional set
{<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>} is functional V49() set
{{<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f0},{<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>}} is set
{[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f0]} is Relation-like Function-like set
{x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f0]} is Element of K18({x,y,z})
K18({x,y,z}) is set
<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> . 3 is set
len <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> is V9() V10() V11() V15() non pair Element of NAT
Seg 3 is non empty V36() V43(3) V51() Element of K18(NAT)
dom <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> is non empty V51() Element of K18(NAT)
[3,[<*z,x*>,f3]] is non empty pair set
{3,[<*z,x*>,f3]} is set
{3} is non with_pair set
{{3,[<*z,x*>,f3]},{3}} is set
proj2 <*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> is non empty set
the_rank_of [<*z,x*>,f3] is V9() V10() V11() set
the_rank_of [<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f0] is V9() V10() V11() set
proj2 <*y,z*> is non empty set
{y,z} is set
<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> . 2 is set
A1 is set
<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*> . 1 is set
[1,[<*x,y*>,f1]] is non empty pair set
{1,[<*x,y*>,f1]} is set
{1} is non with_pair set
{{1,[<*x,y*>,f1]},{1}} is set
the_rank_of [<*x,y*>,f1] is V9() V10() V11() set
proj2 <*z,x*> is non empty set
{z,x} is set
[2,[<*y,z*>,f2]] is non empty pair set
{2,[<*y,z*>,f2]} is set
{2} is non with_pair set
{{2,[<*y,z*>,f2]},{2}} is set
the_rank_of [<*y,z*>,f2] is V9() V10() V11() set
proj2 <*x,y*> is non empty set
{x,y} is set
f1 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
f0 is set
f2 is set
f3 is set
<*f2,f3*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
[<*f2,f3*>,f1] is non empty pair set
{<*f2,f3*>,f1} is functional set
{<*f2,f3*>} is functional V49() set
{{<*f2,f3*>,f1},{<*f2,f3*>}} is set
2GatesCircStr (f2,f3,f0,f1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*f2,f3*>,f1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*[<*f2,f3*>,f1],f0*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*f2,f3*>,f1)) +* (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircuit (f2,f3,f0,f1) is strict non-empty finitely-generated V107( 2GatesCircStr (f2,f3,f0,f1)) gate`2=den Boolean MSAlgebra over 2GatesCircStr (f2,f3,f0,f1)
1GateCircuit (f2,f3,f1) is strict non-empty finitely-generated V107( 1GateCircStr (<*f2,f3*>,f1)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*f2,f3*>,f1)
1GateCircuit (<*f2,f3*>,f1) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*f2,f3*>,f1)
1GateCircuit ([<*f2,f3*>,f1],f0,f1) is strict non-empty finitely-generated V107( 1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)
1GateCircuit (<*[<*f2,f3*>,f1],f0*>,f1) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)
(1GateCircuit (f2,f3,f1)) +* (1GateCircuit ([<*f2,f3*>,f1],f0,f1)) is strict non-empty finitely-generated V107((1GateCircStr (<*f2,f3*>,f1)) +* (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*f2,f3*>,f1)) +* (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))
the Sorts of (2GatesCircuit (f2,f3,f0,f1)) is Relation-like the carrier of (2GatesCircStr (f2,f3,f0,f1)) -defined Function-like V23( the carrier of (2GatesCircStr (f2,f3,f0,f1))) set
the carrier of (2GatesCircStr (f2,f3,f0,f1)) is non empty set
K230( the Sorts of (2GatesCircuit (f2,f3,f0,f1))) is functional V49() V50() set
2GatesCircOutput (f2,f3,f0,f1) is non empty pair Element of InnerVertices (2GatesCircStr (f2,f3,f0,f1))
InnerVertices (2GatesCircStr (f2,f3,f0,f1)) is non empty Element of K18( the carrier of (2GatesCircStr (f2,f3,f0,f1)))
K18( the carrier of (2GatesCircStr (f2,f3,f0,f1))) is set
the ResultSort of (2GatesCircStr (f2,f3,f0,f1)) is Relation-like Function-like V27( the carrier' of (2GatesCircStr (f2,f3,f0,f1)), the carrier of (2GatesCircStr (f2,f3,f0,f1))) Element of K18(K19( the carrier' of (2GatesCircStr (f2,f3,f0,f1)), the carrier of (2GatesCircStr (f2,f3,f0,f1))))
the carrier' of (2GatesCircStr (f2,f3,f0,f1)) is non empty set
K19( the carrier' of (2GatesCircStr (f2,f3,f0,f1)), the carrier of (2GatesCircStr (f2,f3,f0,f1))) is Relation-like set
K18(K19( the carrier' of (2GatesCircStr (f2,f3,f0,f1)), the carrier of (2GatesCircStr (f2,f3,f0,f1)))) is set
K538( the carrier of (2GatesCircStr (f2,f3,f0,f1)), the ResultSort of (2GatesCircStr (f2,f3,f0,f1))) is Element of K18( the carrier of (2GatesCircStr (f2,f3,f0,f1)))
[<*[<*f2,f3*>,f1],f0*>,f1] is non empty pair set
{<*[<*f2,f3*>,f1],f0*>,f1} is functional set
{<*[<*f2,f3*>,f1],f0*>} is functional V49() set
{{<*[<*f2,f3*>,f1],f0*>,f1},{<*[<*f2,f3*>,f1],f0*>}} is set
InputVertices (2GatesCircStr (f2,f3,f0,f1)) is Element of K18( the carrier of (2GatesCircStr (f2,f3,f0,f1)))
the carrier of (2GatesCircStr (f2,f3,f0,f1)) \ K538( the carrier of (2GatesCircStr (f2,f3,f0,f1)), the ResultSort of (2GatesCircStr (f2,f3,f0,f1))) is Element of K18( the carrier of (2GatesCircStr (f2,f3,f0,f1)))
{f2,f3,f0} is set
{[<*f2,f3*>,f1],(2GatesCircOutput (f2,f3,f0,f1))} is Relation-like set
A1 is Relation-like Function-like Element of K230( the Sorts of (2GatesCircuit (f2,f3,f0,f1)))
Following A1 is Relation-like Function-like Element of K230( the Sorts of (2GatesCircuit (f2,f3,f0,f1)))
(Following A1) . (2GatesCircOutput (f2,f3,f0,f1)) is boolean Element of BOOLEAN
A1 . [<*f2,f3*>,f1] is set
A1 . f0 is set
<*(A1 . [<*f2,f3*>,f1]),(A1 . f0)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
f1 . <*(A1 . [<*f2,f3*>,f1]),(A1 . f0)*> is boolean set
(Following A1) . [<*f2,f3*>,f1] is set
A1 . f2 is set
A1 . f3 is set
<*(A1 . f2),(A1 . f3)*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like V51() set
f1 . <*(A1 . f2),(A1 . f3)*> is boolean set
(Following A1) . f2 is set
(Following A1) . f3 is set
(Following A1) . f0 is set
the Sorts of (1GateCircuit (f2,f3,f1)) is Relation-like the carrier of (1GateCircStr (<*f2,f3*>,f1)) -defined Function-like V23( the carrier of (1GateCircStr (<*f2,f3*>,f1))) set
the carrier of (1GateCircStr (<*f2,f3*>,f1)) is non empty set
K230( the Sorts of (1GateCircuit (f2,f3,f1))) is functional V49() V50() set
A1 | the carrier of (1GateCircStr (<*f2,f3*>,f1)) is Relation-like Function-like set
the Sorts of (1GateCircuit ([<*f2,f3*>,f1],f0,f1)) is Relation-like the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) -defined Function-like V23( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))) set
the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) is non empty set
K230( the Sorts of (1GateCircuit ([<*f2,f3*>,f1],f0,f1))) is functional V49() V50() set
A1 | the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) is Relation-like Function-like set
t is Relation-like Function-like Element of K230( the Sorts of (1GateCircuit ([<*f2,f3*>,f1],f0,f1)))
proj1 t is set
proj2 <*[<*f2,f3*>,f1],f0*> is non empty set
S2 is Element of InnerVertices (2GatesCircStr (f2,f3,f0,f1))
{S2,f0} is set
InputVertices (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) is Element of K18( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)))
K18( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))) is set
the ResultSort of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) is Relation-like Function-like V27( the carrier' of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)), the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))) Element of K18(K19( the carrier' of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)), the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))))
the carrier' of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) is non empty set
K19( the carrier' of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)), the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))) is Relation-like set
K18(K19( the carrier' of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)), the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)))) is set
K538( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)), the ResultSort of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))) is Element of K18( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)))
the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) \ K538( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)), the ResultSort of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1))) is Element of K18( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)))
InnerVertices (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)) is non empty Element of K18( the carrier of (1GateCircStr (<*[<*f2,f3*>,f1],f0*>,f1)))
InnerVertices (1GateCircStr (<*f2,f3*>,f1)) is non empty Element of K18( the carrier of (1GateCircStr (<*f2,f3*>,f1)))
K18( the carrier of (1GateCircStr (<*f2,f3*>,f1))) is set
the ResultSort of (1GateCircStr (<*f2,f3*>,f1)) is Relation-like Function-like V27( the carrier' of (1GateCircStr (<*f2,f3*>,f1)), the carrier of (1GateCircStr (<*f2,f3