REAL is set
NAT is non empty V5() V12() V13() V14() V39() cardinal limit_cardinal V54() V55() Element of K23(REAL)
K23(REAL) is non empty set
COMPLEX is set
RAT is set
INT is set
K24(COMPLEX,COMPLEX) is Relation-like set
K23(K24(COMPLEX,COMPLEX)) is non empty set
K24(K24(COMPLEX,COMPLEX),COMPLEX) is Relation-like set
K23(K24(K24(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K24(REAL,REAL) is Relation-like set
K23(K24(REAL,REAL)) is non empty set
K24(K24(REAL,REAL),REAL) is Relation-like set
K23(K24(K24(REAL,REAL),REAL)) is non empty set
K24(RAT,RAT) is Relation-like set
K23(K24(RAT,RAT)) is non empty set
K24(K24(RAT,RAT),RAT) is Relation-like set
K23(K24(K24(RAT,RAT),RAT)) is non empty set
K24(INT,INT) is Relation-like set
K23(K24(INT,INT)) is non empty set
K24(K24(INT,INT),INT) is Relation-like set
K23(K24(K24(INT,INT),INT)) is non empty set
K24(NAT,NAT) is non empty V5() Relation-like V39() set
K24(K24(NAT,NAT),NAT) is non empty V5() Relation-like V39() set
K23(K24(K24(NAT,NAT),NAT)) is non empty V5() V39() set
NAT is non empty V5() V12() V13() V14() V39() cardinal limit_cardinal V54() V55() set
K23(NAT) is non empty V5() V39() set
K23(NAT) is non empty V5() V39() set
BOOLEAN is non empty set
0 is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of NAT
{} is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
1 is ext-real positive non negative non empty V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
{0,1} is non empty V39() V43() V54() non with_pair set
{{},1} is non empty V39() V43() V54() non with_pair set
K353() is set
K23(K353()) is non empty set
K354() is Element of K23(K353())
K394() is non empty V98() L10()
the carrier of K394() is non empty set
K357( the carrier of K394()) is non empty M24( the carrier of K394())
K393(K394()) is Element of K23(K357( the carrier of K394()))
K23(K357( the carrier of K394())) is non empty set
K24(K393(K394()),NAT) is Relation-like set
K23(K24(K393(K394()),NAT)) is non empty set
K24(NAT,K393(K394())) is Relation-like set
K23(K24(NAT,K393(K394()))) is non empty set
2 is ext-real positive non negative non empty V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
2 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K24((2 -tuples_on BOOLEAN),BOOLEAN) is non empty Relation-like set
K23(K24((2 -tuples_on BOOLEAN),BOOLEAN)) is non empty set
3 is ext-real positive non negative non empty V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
3 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K24((3 -tuples_on BOOLEAN),BOOLEAN) is non empty Relation-like set
K23(K24((3 -tuples_on BOOLEAN),BOOLEAN)) is non empty set
'xor' is Relation-like 2 -tuples_on BOOLEAN -defined BOOLEAN -valued Function-like V30(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K23(K24((2 -tuples_on BOOLEAN),BOOLEAN))
Seg 1 is non empty V5() V39() 1 -element V54() Element of K23(NAT)
'&' is Relation-like 2 -tuples_on BOOLEAN -defined BOOLEAN -valued Function-like V30(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K23(K24((2 -tuples_on BOOLEAN),BOOLEAN))
or3 is Relation-like 3 -tuples_on BOOLEAN -defined BOOLEAN -valued Function-like V30(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K23(K24((3 -tuples_on BOOLEAN),BOOLEAN))
n is set
g is set
f is set
{n,f} is non empty V39() V54() set
{g} is non empty V5() V39() 1 -element V54() set
{n,f} \ {g} is V39() V54() Element of K23({n,f})
K23({n,f}) is non empty V39() V43() V54() set
S0 is set
n is set
f is set
<*n,f*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
g is set
[<*n,f*>,g] is non empty pair set
{<*n,f*>,g} is non empty V39() V54() set
{<*n,f*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*n,f*>,g},{<*n,f*>}} is non empty V39() V43() V54() set
proj2 <*n,f*> is non empty V39() V54() set
{n,f} is non empty V39() V54() set
the_rank_of n is V12() V13() V14() set
the_rank_of [<*n,f*>,g] is V12() V13() V14() set
the_rank_of f is V12() V13() V14() set
n is ManySortedSign
the carrier' of n is set
the ResultSort of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like V30( the carrier' of n, the carrier of n) Element of K23(K24( the carrier' of n, the carrier of n))
the carrier of n is set
K24( the carrier' of n, the carrier of n) is Relation-like set
K23(K24( the carrier' of n, the carrier of n)) is non empty set
id the carrier' of n is Relation-like the carrier' of n -defined the carrier' of n -valued Function-like one-to-one total Element of K23(K24( the carrier' of n, the carrier' of n))
K24( the carrier' of n, the carrier' of n) is Relation-like set
K23(K24( the carrier' of n, the carrier' of n)) is non empty set
f is set
the Arity of n is Relation-like the carrier' of n -defined the carrier of n * -valued Function-like V30( the carrier' of n, the carrier of n * ) Element of K23(K24( the carrier' of n,( the carrier of n *)))
the carrier of n * is non empty functional FinSequence-membered FinSequenceSet of the carrier of n
K24( the carrier' of n,( the carrier of n *)) is Relation-like set
K23(K24( the carrier' of n,( the carrier of n *))) is non empty set
the Arity of n . f is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V54() set
f `2 is set
[( the Arity of n . f),(f `2)] is non empty pair set
{( the Arity of n . f),(f `2)} is non empty V39() V54() set
{( the Arity of n . f)} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{( the Arity of n . f),(f `2)},{( the Arity of n . f)}} is non empty V39() V43() V54() set
f is set
the Arity of n is Relation-like the carrier' of n -defined the carrier of n * -valued Function-like V30( the carrier' of n, the carrier of n * ) Element of K23(K24( the carrier' of n,( the carrier of n *)))
the carrier of n * is non empty functional FinSequence-membered FinSequenceSet of the carrier of n
K24( the carrier' of n,( the carrier of n *)) is Relation-like set
K23(K24( the carrier' of n,( the carrier of n *))) is non empty set
the Arity of n . f is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V54() set
f `1 is set
g is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V54() set
len g is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
(len g) -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K24(((len g) -tuples_on BOOLEAN),BOOLEAN) is non empty Relation-like set
K23(K24(((len g) -tuples_on BOOLEAN),BOOLEAN)) is non empty set
the void V74() trivial' strict unsplit gate`1=arity gate`2isBoolean ManySortedSign is void V74() trivial' strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
n is set
{n} is non empty V5() V39() 1 -element V54() set
{n} * is non empty functional FinSequence-membered FinSequenceSet of {n}
K24({},({n} *)) is Relation-like set
K23(K24({},({n} *))) is non empty set
the ext-real non positive non negative empty Relation-like non-empty empty-yielding {} -defined {n} * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( {} ,{n} * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24({},({n} *))) is ext-real non positive non negative empty Relation-like non-empty empty-yielding {} -defined {n} * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( {} ,{n} * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24({},({n} *)))
K24({},{n}) is Relation-like V39() V54() set
K23(K24({},{n})) is non empty V39() V43() V54() set
the ext-real non positive non negative empty Relation-like non-empty empty-yielding {} -defined {n} -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( {} ,{n}) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24({},{n})) is ext-real non positive non negative empty Relation-like non-empty empty-yielding {} -defined {n} -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( {} ,{n}) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24({},{n}))
ManySortedSign(# {n},{}, the ext-real non positive non negative empty Relation-like non-empty empty-yielding {} -defined {n} * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( {} ,{n} * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24({},({n} *))), the ext-real non positive non negative empty Relation-like non-empty empty-yielding {} -defined {n} -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( {} ,{n}) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24({},{n})) #) is strict ManySortedSign
S0 is void V74() trivial' strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
the carrier of S0 is set
f is void V74() trivial' strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
the carrier of f is set
g is void V74() trivial' strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
the carrier of g is set
the Arity of f is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of f -defined the carrier of f * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of f, the carrier of f * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of f,( the carrier of f *)))
the carrier' of f is ext-real non positive non negative empty V5() Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the carrier of f * is non empty functional FinSequence-membered FinSequenceSet of the carrier of f
K24( the carrier' of f,( the carrier of f *)) is Relation-like set
K23(K24( the carrier' of f,( the carrier of f *))) is non empty set
the Arity of g is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of g -defined the carrier of g * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of g, the carrier of g * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of g,( the carrier of g *)))
the carrier' of g is ext-real non positive non negative empty V5() Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the carrier of g * is non empty functional FinSequence-membered FinSequenceSet of the carrier of g
K24( the carrier' of g,( the carrier of g *)) is Relation-like set
K23(K24( the carrier' of g,( the carrier of g *))) is non empty set
n is set
(n) is void V74() trivial' strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
the carrier of (n) is set
{n} is non empty V5() V39() 1 -element V54() set
n is set
(n) is non empty void V74() trivial' strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
g is strict non-empty finitely-generated V110((n)) Boolean MSAlgebra over (n)
S0 is strict non-empty finitely-generated V110((n)) Boolean MSAlgebra over (n)
the Sorts of g is Relation-like non-empty the carrier of (n) -defined Function-like total set
the carrier of (n) is non empty set
the carrier of (n) --> BOOLEAN is Relation-like the carrier of (n) -defined {BOOLEAN} -valued Function-like V30( the carrier of (n),{BOOLEAN}) Element of K23(K24( the carrier of (n),{BOOLEAN}))
{BOOLEAN} is non empty V5() V39() 1 -element V54() set
K24( the carrier of (n),{BOOLEAN}) is non empty Relation-like set
K23(K24( the carrier of (n),{BOOLEAN})) is non empty set
the Charact of g is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional total non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair ManySortedFunction of the Arity of (n) * ( the Sorts of g #), the ResultSort of (n) * the Sorts of g
the carrier' of (n) is ext-real non positive non negative empty V5() Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the Arity of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n) * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n),( the carrier of (n) *)))
the carrier of (n) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (n)
K24( the carrier' of (n),( the carrier of (n) *)) is Relation-like set
K23(K24( the carrier' of (n),( the carrier of (n) *))) is non empty set
the Sorts of g # is Relation-like non-empty the carrier of (n) * -defined Function-like total set
the Arity of (n) * ( the Sorts of g #) is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the ResultSort of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n)) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n), the carrier of (n)))
K24( the carrier' of (n), the carrier of (n)) is Relation-like set
K23(K24( the carrier' of (n), the carrier of (n))) is non empty set
the ResultSort of (n) * the Sorts of g is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the Charact of S0 is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional total non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair ManySortedFunction of the Arity of (n) * ( the Sorts of S0 #), the ResultSort of (n) * the Sorts of S0
the Sorts of S0 is Relation-like non-empty the carrier of (n) -defined Function-like total set
the Sorts of S0 # is Relation-like non-empty the carrier of (n) * -defined Function-like total set
the Arity of (n) * ( the Sorts of S0 #) is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the ResultSort of (n) * the Sorts of S0 is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
n is set
(n) is non empty void V74() trivial' strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f is ManySortedSign
the Arity of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n) * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n),( the carrier of (n) *)))
the carrier' of (n) is ext-real non positive non negative empty V5() Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the carrier of (n) is non empty set
the carrier of (n) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (n)
K24( the carrier' of (n),( the carrier of (n) *)) is Relation-like set
K23(K24( the carrier' of (n),( the carrier of (n) *))) is non empty set
the Arity of f is Relation-like the carrier' of f -defined the carrier of f * -valued Function-like V30( the carrier' of f, the carrier of f * ) Element of K23(K24( the carrier' of f,( the carrier of f *)))
the carrier' of f is set
the carrier of f is set
the carrier of f * is non empty functional FinSequence-membered FinSequenceSet of the carrier of f
K24( the carrier' of f,( the carrier of f *)) is Relation-like set
K23(K24( the carrier' of f,( the carrier of f *))) is non empty set
the ResultSort of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n)) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n), the carrier of (n)))
K24( the carrier' of (n), the carrier of (n)) is Relation-like set
K23(K24( the carrier' of (n), the carrier of (n))) is non empty set
the ResultSort of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V30( the carrier' of f, the carrier of f) Element of K23(K24( the carrier' of f, the carrier of f))
K24( the carrier' of f, the carrier of f) is Relation-like set
K23(K24( the carrier' of f, the carrier of f)) is non empty set
n is set
(n) is non empty void V74() trivial' strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f is non empty V74() ManySortedSign
the carrier of f is non empty set
(n) +* f is non empty V74() strict ManySortedSign
the carrier' of f is set
the Arity of f is Relation-like the carrier' of f -defined the carrier of f * -valued Function-like V30( the carrier' of f, the carrier of f * ) Element of K23(K24( the carrier' of f,( the carrier of f *)))
the carrier of f * is non empty functional FinSequence-membered FinSequenceSet of the carrier of f
K24( the carrier' of f,( the carrier of f *)) is Relation-like set
K23(K24( the carrier' of f,( the carrier of f *))) is non empty set
the ResultSort of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V30( the carrier' of f, the carrier of f) Element of K23(K24( the carrier' of f, the carrier of f))
K24( the carrier' of f, the carrier of f) is Relation-like set
K23(K24( the carrier' of f, the carrier of f)) is non empty set
ManySortedSign(# the carrier of f, the carrier' of f, the Arity of f, the ResultSort of f #) is strict ManySortedSign
{n} is non empty V5() V39() 1 -element V54() set
{n} \/ the carrier of f is non empty set
{} \/ the carrier' of f is set
the carrier of (n) is non empty set
the ResultSort of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n)) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n), the carrier of (n)))
the carrier' of (n) is ext-real non positive non negative empty V5() Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
K24( the carrier' of (n), the carrier of (n)) is Relation-like set
K23(K24( the carrier' of (n), the carrier of (n))) is non empty set
the Arity of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n) * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n),( the carrier of (n) *)))
the carrier of (n) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (n)
K24( the carrier' of (n),( the carrier of (n) *)) is Relation-like set
K23(K24( the carrier' of (n),( the carrier of (n) *))) is non empty set
{} +* the ResultSort of f is Relation-like Function-like set
{} +* the Arity of f is Relation-like Function-like set
the carrier of ((n) +* f) is non empty set
the carrier' of ((n) +* f) is set
the ResultSort of ((n) +* f) is Relation-like the carrier' of ((n) +* f) -defined the carrier of ((n) +* f) -valued Function-like V30( the carrier' of ((n) +* f), the carrier of ((n) +* f)) Element of K23(K24( the carrier' of ((n) +* f), the carrier of ((n) +* f)))
K24( the carrier' of ((n) +* f), the carrier of ((n) +* f)) is Relation-like set
K23(K24( the carrier' of ((n) +* f), the carrier of ((n) +* f))) is non empty set
n is set
(n) is non empty void V74() trivial' strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(n) is strict non-empty finitely-generated V110((n)) Boolean MSAlgebra over (n)
f is non empty V74() strict ManySortedSign
the carrier of f is non empty set
g is non-empty finitely-generated V110(f) Boolean MSAlgebra over f
(n) +* g is strict non-empty MSAlgebra over (n) +* f
(n) +* f is non empty V74() strict ManySortedSign
the Sorts of g is Relation-like non-empty the carrier of f -defined Function-like total set
the Charact of g is Relation-like the carrier' of f -defined Function-like total ManySortedFunction of the Arity of f * ( the Sorts of g #), the ResultSort of f * the Sorts of g
the carrier' of f is set
the Arity of f is Relation-like the carrier' of f -defined the carrier of f * -valued Function-like V30( the carrier' of f, the carrier of f * ) Element of K23(K24( the carrier' of f,( the carrier of f *)))
the carrier of f * is non empty functional FinSequence-membered FinSequenceSet of the carrier of f
K24( the carrier' of f,( the carrier of f *)) is Relation-like set
K23(K24( the carrier' of f,( the carrier of f *))) is non empty set
the Sorts of g # is Relation-like non-empty the carrier of f * -defined Function-like total set
the Arity of f * ( the Sorts of g #) is Relation-like non-empty the carrier' of f -defined Function-like set
the ResultSort of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V30( the carrier' of f, the carrier of f) Element of K23(K24( the carrier' of f, the carrier of f))
K24( the carrier' of f, the carrier of f) is Relation-like set
K23(K24( the carrier' of f, the carrier of f)) is non empty set
the ResultSort of f * the Sorts of g is Relation-like non-empty the carrier' of f -defined Function-like set
MSAlgebra(# the Sorts of g, the Charact of g #) is strict MSAlgebra over f
{n} is non empty V5() V39() 1 -element V54() set
the carrier of (n) is non empty set
the carrier of f --> BOOLEAN is Relation-like the carrier of f -defined {BOOLEAN} -valued Function-like V30( the carrier of f,{BOOLEAN}) Element of K23(K24( the carrier of f,{BOOLEAN}))
{BOOLEAN} is non empty V5() V39() 1 -element V54() set
K24( the carrier of f,{BOOLEAN}) is non empty Relation-like set
K23(K24( the carrier of f,{BOOLEAN})) is non empty set
the Sorts of (n) is Relation-like non-empty the carrier of (n) -defined Function-like total set
the carrier of (n) --> BOOLEAN is Relation-like the carrier of (n) -defined {BOOLEAN} -valued Function-like V30( the carrier of (n),{BOOLEAN}) Element of K23(K24( the carrier of (n),{BOOLEAN}))
K24( the carrier of (n),{BOOLEAN}) is non empty Relation-like set
K23(K24( the carrier of (n),{BOOLEAN})) is non empty set
the Charact of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional total non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair ManySortedFunction of the Arity of (n) * ( the Sorts of (n) #), the ResultSort of (n) * the Sorts of (n)
the carrier' of (n) is ext-real non positive non negative empty V5() Relation-like non-empty empty-yielding NAT -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the Arity of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) * -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n) * ) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n),( the carrier of (n) *)))
the carrier of (n) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (n)
K24( the carrier' of (n),( the carrier of (n) *)) is Relation-like set
K23(K24( the carrier' of (n),( the carrier of (n) *))) is non empty set
the Sorts of (n) # is Relation-like non-empty the carrier of (n) * -defined Function-like total set
the Arity of (n) * ( the Sorts of (n) #) is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the ResultSort of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding the carrier' of (n) -defined the carrier of (n) -valued V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V30( the carrier' of (n), the carrier of (n)) V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair Element of K23(K24( the carrier' of (n), the carrier of (n)))
K24( the carrier' of (n), the carrier of (n)) is Relation-like set
K23(K24( the carrier' of (n), the carrier of (n))) is non empty set
the ResultSort of (n) * the Sorts of (n) is ext-real non positive non negative empty Relation-like non-empty empty-yielding NAT -defined the carrier' of (n) -defined V12() V13() V14() V16() V17() V18() Function-like one-to-one constant functional non pair V33() V34() V39() V40() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V54() non with_pair set
the Charact of (n) +* the Charact of g is Relation-like the carrier' of (n) \/ the carrier' of f -defined Function-like total set
the carrier' of (n) \/ the carrier' of f is set
the Sorts of ((n) +* g) is Relation-like non-empty the carrier of ((n) +* f) -defined Function-like total set
the carrier of ((n) +* f) is non empty set
the Sorts of (n) +* the Sorts of g is Relation-like non-empty the carrier of (n) \/ the carrier of f -defined Function-like total set
the carrier of (n) \/ the carrier of f is non empty set
the Charact of ((n) +* g) is Relation-like the carrier' of ((n) +* f) -defined Function-like total ManySortedFunction of the Arity of ((n) +* f) * ( the Sorts of ((n) +* g) #), the ResultSort of ((n) +* f) * the Sorts of ((n) +* g)
the carrier' of ((n) +* f) is set
the Arity of ((n) +* f) is Relation-like the carrier' of ((n) +* f) -defined the carrier of ((n) +* f) * -valued Function-like V30( the carrier' of ((n) +* f), the carrier of ((n) +* f) * ) Element of K23(K24( the carrier' of ((n) +* f),( the carrier of ((n) +* f) *)))
the carrier of ((n) +* f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of ((n) +* f)
K24( the carrier' of ((n) +* f),( the carrier of ((n) +* f) *)) is Relation-like set
K23(K24( the carrier' of ((n) +* f),( the carrier of ((n) +* f) *))) is non empty set
the Sorts of ((n) +* g) # is Relation-like non-empty the carrier of ((n) +* f) * -defined Function-like total set
the Arity of ((n) +* f) * ( the Sorts of ((n) +* g) #) is Relation-like non-empty the carrier' of ((n) +* f) -defined Function-like set
the ResultSort of ((n) +* f) is Relation-like the carrier' of ((n) +* f) -defined the carrier of ((n) +* f) -valued Function-like V30( the carrier' of ((n) +* f), the carrier of ((n) +* f)) Element of K23(K24( the carrier' of ((n) +* f), the carrier of ((n) +* f)))
K24( the carrier' of ((n) +* f), the carrier of ((n) +* f)) is Relation-like set
K23(K24( the carrier' of ((n) +* f), the carrier of ((n) +* f))) is non empty set
the ResultSort of ((n) +* f) * the Sorts of ((n) +* g) is Relation-like non-empty the carrier' of ((n) +* f) -defined Function-like set
proj1 the Sorts of (n) is set
proj1 the Sorts of g is set
0 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
FALSE is boolean Element of BOOLEAN
(0 -tuples_on BOOLEAN) --> FALSE is Relation-like 0 -tuples_on BOOLEAN -defined BOOLEAN -valued Function-like V30(0 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K23(K24((0 -tuples_on BOOLEAN),BOOLEAN))
K24((0 -tuples_on BOOLEAN),BOOLEAN) is non empty Relation-like set
K23(K24((0 -tuples_on BOOLEAN),BOOLEAN)) is non empty set
1GateCircStr ({},((0 -tuples_on BOOLEAN) --> FALSE)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() set
[{},((0 -tuples_on BOOLEAN) --> FALSE)] is non empty pair set
{{},((0 -tuples_on BOOLEAN) --> FALSE)} is non empty functional V39() V54() set
{{}} is non empty V5() functional V39() V43() 1 -element V52() V54() non with_pair set
{{{},((0 -tuples_on BOOLEAN) --> FALSE)},{{}}} is non empty V39() V43() V54() set
f is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V54() set
g is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V54() set
S0 is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
A0 is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h is Relation-like NAT -defined Function-like total set
h . n is set
h . 0 is set
Sn is Relation-like NAT -defined Function-like total set
Sn . 0 is set
N is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
An is Relation-like NAT -defined Function-like total set
An . n is set
An . 0 is set
o0 is Relation-like NAT -defined Function-like total set
o0 . 0 is set
S0 is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
A0 is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
N is Relation-like NAT -defined Function-like total set
N . S0 is set
N . 0 is set
h is Relation-like NAT -defined Function-like total set
h . 0 is set
n is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() set
f is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V54() set
g is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like V54() set
(n,f,g) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircuit ({},((0 -tuples_on BOOLEAN) --> FALSE)) is strict non-empty finitely-generated V110( 1GateCircStr ({},((0 -tuples_on BOOLEAN) --> FALSE))) gate`2=den Boolean MSAlgebra over 1GateCircStr ({},((0 -tuples_on BOOLEAN) --> FALSE))
Sn is non empty V74() ManySortedSign
f1 is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() set
f1 + 1 is ext-real positive non negative non empty V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
f . (f1 + 1) is set
g . (f1 + 1) is set
o0 is set
BitAdderWithOverflowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (f1 + 1)),(g . (f1 + 1))*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'] is non empty pair set
{<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'} is non empty functional V39() V54() set
{<*(f . (f1 + 1)),(g . (f1 + 1))*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'},{<*(f . (f1 + 1)),(g . (f1 + 1))*>}} is non empty V39() V43() V54() set
<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
MajorityStr ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
MajorityIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (f1 + 1)),o0*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*(g . (f1 + 1)),o0*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,'&')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*o0,(f . (f1 + 1))*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*o0,(f . (f1 + 1))*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,'&'))) +* (1GateCircStr (<*o0,(f . (f1 + 1))*>,'&')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'] is non empty pair set
{<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'} is non empty functional V39() V54() set
{{<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'},{<*(f . (f1 + 1)),(g . (f1 + 1))*>}} is non empty V39() V43() V54() set
[<*(g . (f1 + 1)),o0*>,'&'] is non empty pair set
{<*(g . (f1 + 1)),o0*>,'&'} is non empty functional V39() V54() set
{<*(g . (f1 + 1)),o0*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*(g . (f1 + 1)),o0*>,'&'},{<*(g . (f1 + 1)),o0*>}} is non empty V39() V43() V54() set
[<*o0,(f . (f1 + 1))*>,'&'] is non empty pair set
{<*o0,(f . (f1 + 1))*>,'&'} is non empty functional V39() V54() set
{<*o0,(f . (f1 + 1))*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*o0,(f . (f1 + 1))*>,'&'},{<*o0,(f . (f1 + 1))*>}} is non empty V39() V43() V54() set
<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*> is non empty Relation-like NAT -defined Function-like V39() 3 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(MajorityIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) +* (MajorityStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
An is non-empty MSAlgebra over Sn
BitAdderWithOverflowCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V110( BitAdderWithOverflowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) gate`2=den Boolean MSAlgebra over BitAdderWithOverflowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)
BitAdderCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V110( 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')
2GatesCircuit ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor') is strict non-empty finitely-generated V110( 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')
1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),'xor') is strict non-empty finitely-generated V110( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')
1GateCircuit (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor') is strict non-empty finitely-generated V110( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')
1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0,'xor') is strict non-empty finitely-generated V110( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')
1GateCircuit (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor') is strict non-empty finitely-generated V110( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')
(1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),'xor')) +* (1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0,'xor')) is strict non-empty finitely-generated V110((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor'))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor'))
MajorityCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V110( MajorityStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) gate`2=den Boolean MSAlgebra over MajorityStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)
MajorityICirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V110( MajorityIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) gate`2=den Boolean MSAlgebra over MajorityIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)
1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),'&') is strict non-empty finitely-generated V110( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')
1GateCircuit (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&') is strict non-empty finitely-generated V110( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')
1GateCircuit ((g . (f1 + 1)),o0,'&') is strict non-empty finitely-generated V110( 1GateCircStr (<*(g . (f1 + 1)),o0*>,'&')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (f1 + 1)),o0*>,'&')
1GateCircuit (<*(g . (f1 + 1)),o0*>,'&') is strict non-empty finitely-generated V110( 1GateCircStr (<*(g . (f1 + 1)),o0*>,'&')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (f1 + 1)),o0*>,'&')
(1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),'&')) +* (1GateCircuit ((g . (f1 + 1)),o0,'&')) is strict non-empty finitely-generated V110((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,'&'))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,'&'))
1GateCircuit (o0,(f . (f1 + 1)),'&') is strict non-empty finitely-generated V110( 1GateCircStr (<*o0,(f . (f1 + 1))*>,'&')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*o0,(f . (f1 + 1))*>,'&')
1GateCircuit (<*o0,(f . (f1 + 1))*>,'&') is strict non-empty finitely-generated V110( 1GateCircStr (<*o0,(f . (f1 + 1))*>,'&')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*o0,(f . (f1 + 1))*>,'&')
((1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),'&')) +* (1GateCircuit ((g . (f1 + 1)),o0,'&'))) +* (1GateCircuit (o0,(f . (f1 + 1)),'&')) is strict non-empty finitely-generated V110(((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,'&'))) +* (1GateCircStr (<*o0,(f . (f1 + 1))*>,'&'))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,'&'))) +* (1GateCircStr (<*o0,(f . (f1 + 1))*>,'&'))
1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&'],or3) is strict non-empty finitely-generated V110( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3)
1GateCircuit (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3) is strict non-empty finitely-generated V110( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3)
(MajorityICirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&'],or3)) is strict non-empty finitely-generated V110((MajorityIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3))) gate`2=den Boolean MSAlgebra over (MajorityIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'&'],[<*(g . (f1 + 1)),o0*>,'&'],[<*o0,(f . (f1 + 1))*>,'&']*>,or3))
(BitAdderCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (MajorityCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is strict non-empty finitely-generated V110((2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) +* (MajorityStr ((f . (f1 + 1)),(g . (f1 + 1)),o0))) gate`2=den Boolean MSAlgebra over (2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) +* (MajorityStr ((f . (f1 + 1)),(g . (f1 + 1)),o0))
An +* (BitAdderWithOverflowCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is strict non-empty MSAlgebra over Sn +* (BitAdderWithOverflowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0))
Sn +* (BitAdderWithOverflowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is non empty non void V74() strict ManySortedSign
Sn is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
o0 is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() set
o0 + 1 is ext-real positive non negative non empty V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
f . (o0 + 1) is set
g . (o0 + 1) is set
An is set
BitAdderWithOverflowStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (o0 + 1)),(g . (o0 + 1))*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'] is non empty pair set
{<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'} is non empty functional V39() V54() set
{<*(f . (o0 + 1)),(g . (o0 + 1))*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'},{<*(f . (o0 + 1)),(g . (o0 + 1))*>}} is non empty V39() V43() V54() set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'],An*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'],An*>,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'],An*>,'xor')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
MajorityStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
MajorityIStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (o0 + 1)),An*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*(g . (o0 + 1)),An*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&')) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,'&')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*An,(f . (o0 + 1))*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*An,(f . (o0 + 1))*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&')) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,'&'))) +* (1GateCircStr (<*An,(f . (o0 + 1))*>,'&')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&'] is non empty pair set
{<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&'} is non empty functional V39() V54() set
{{<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&'},{<*(f . (o0 + 1)),(g . (o0 + 1))*>}} is non empty V39() V43() V54() set
[<*(g . (o0 + 1)),An*>,'&'] is non empty pair set
{<*(g . (o0 + 1)),An*>,'&'} is non empty functional V39() V54() set
{<*(g . (o0 + 1)),An*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*(g . (o0 + 1)),An*>,'&'},{<*(g . (o0 + 1)),An*>}} is non empty V39() V43() V54() set
[<*An,(f . (o0 + 1))*>,'&'] is non empty pair set
{<*An,(f . (o0 + 1))*>,'&'} is non empty functional V39() V54() set
{<*An,(f . (o0 + 1))*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*An,(f . (o0 + 1))*>,'&'},{<*An,(f . (o0 + 1))*>}} is non empty V39() V43() V54() set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&'],[<*(g . (o0 + 1)),An*>,'&'],[<*An,(f . (o0 + 1))*>,'&']*> is non empty Relation-like NAT -defined Function-like V39() 3 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&'],[<*(g . (o0 + 1)),An*>,'&'],[<*An,(f . (o0 + 1))*>,'&']*>,or3) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(MajorityIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'&'],[<*(g . (o0 + 1)),An*>,'&'],[<*An,(f . (o0 + 1))*>,'&']*>,or3)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,'xor')) +* (MajorityStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn +* (BitAdderWithOverflowStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f1 is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h1 is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() set
h1 + 1 is ext-real positive non negative non empty V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
f . (h1 + 1) is set
g . (h1 + 1) is set
g1 is set
BitAdderWithOverflowStr ((f . (h1 + 1)),(g . (h1 + 1)),g1) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (h1 + 1)),(g . (h1 + 1)),g1,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (h1 + 1)),(g . (h1 + 1))*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'] is non empty pair set
{<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'} is non empty functional V39() V54() set
{<*(f . (h1 + 1)),(g . (h1 + 1))*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'},{<*(f . (h1 + 1)),(g . (h1 + 1))*>}} is non empty V39() V43() V54() set
<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'],g1*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'],g1*>,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'],g1*>,'xor')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
MajorityStr ((f . (h1 + 1)),(g . (h1 + 1)),g1) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
MajorityIStr ((f . (h1 + 1)),(g . (h1 + 1)),g1) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (h1 + 1)),g1*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*(g . (h1 + 1)),g1*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (h1 + 1)),g1*>,'&')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*g1,(f . (h1 + 1))*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*g1,(f . (h1 + 1))*>,'&') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&')) +* (1GateCircStr (<*(g . (h1 + 1)),g1*>,'&'))) +* (1GateCircStr (<*g1,(f . (h1 + 1))*>,'&')) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&'] is non empty pair set
{<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&'} is non empty functional V39() V54() set
{{<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&'},{<*(f . (h1 + 1)),(g . (h1 + 1))*>}} is non empty V39() V43() V54() set
[<*(g . (h1 + 1)),g1*>,'&'] is non empty pair set
{<*(g . (h1 + 1)),g1*>,'&'} is non empty functional V39() V54() set
{<*(g . (h1 + 1)),g1*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*(g . (h1 + 1)),g1*>,'&'},{<*(g . (h1 + 1)),g1*>}} is non empty V39() V43() V54() set
[<*g1,(f . (h1 + 1))*>,'&'] is non empty pair set
{<*g1,(f . (h1 + 1))*>,'&'} is non empty functional V39() V54() set
{<*g1,(f . (h1 + 1))*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*g1,(f . (h1 + 1))*>,'&'},{<*g1,(f . (h1 + 1))*>}} is non empty V39() V43() V54() set
<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&'],[<*(g . (h1 + 1)),g1*>,'&'],[<*g1,(f . (h1 + 1))*>,'&']*> is non empty Relation-like NAT -defined Function-like V39() 3 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&'],[<*(g . (h1 + 1)),g1*>,'&'],[<*g1,(f . (h1 + 1))*>,'&']*>,or3) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(MajorityIStr ((f . (h1 + 1)),(g . (h1 + 1)),g1)) +* (1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'&'],[<*(g . (h1 + 1)),g1*>,'&'],[<*g1,(f . (h1 + 1))*>,'&']*>,or3)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (h1 + 1)),(g . (h1 + 1)),g1,'xor')) +* (MajorityStr ((f . (h1 + 1)),(g . (h1 + 1)),g1)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f1 +* (BitAdderWithOverflowStr ((f . (h1 + 1)),(g . (h1 + 1)),g1)) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
xx is ext-real non negative V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() set
xx + 1 is ext-real positive non negative non empty V12() V13() V14() V18() non pair V33() V34() V39() cardinal V54() Element of NAT
f . (xx + 1) is set
g . (xx + 1) is set
x is set
BitAdderWithOverflowStr ((f . (xx + 1)),(g . (xx + 1)),x) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (xx + 1)),(g . (xx + 1)),x,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (xx + 1)),(g . (xx + 1))*> is non empty Relation-like NAT -defined Function-like V39() 2 -element FinSequence-like FinSubsequence-like V54() set
1GateCircStr (<*(f . (xx + 1)),(g . (xx + 1))*>,'xor') is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'] is non empty pair set
{<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'} is non empty functional V39() V54() set
{<*(f . (xx + 1)),(g . (xx + 1))*>} is non empty V5() functional V39() V43() 1 -element V52() V54() set
{{<*(f . (xx + 1)),(