REAL is set
NAT is non empty V12() V21() V22() V23() V28() cardinal limit_cardinal Element of K27(REAL)
K27(REAL) is set
NAT is non empty V12() V21() V22() V23() V28() cardinal limit_cardinal set
K27(NAT) is V12() V28() set
K27(NAT) is V12() V28() set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty non pair V21() V22() V23() V25() V26() V27() V28() V29() V32() cardinal {} -element V37() FinSequence-like FinSubsequence-like FinSequence-membered non with_pair nonpair-yielding ext-real non positive non negative V115() V126() set
1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
{{},1} is non empty V28() V32() non with_pair set
K228() is set
K27(K228()) is set
K229() is Element of K27(K228())
K279() is non empty V83() L10()
the carrier of K279() is non empty set
K232( the carrier of K279()) is non empty M19( the carrier of K279())
K278(K279()) is Element of K27(K232( the carrier of K279()))
K27(K232( the carrier of K279())) is set
K28(K278(K279()),NAT) is Relation-like set
K27(K28(K278(K279()),NAT)) is set
K28(NAT,K278(K279())) is Relation-like set
K27(K28(NAT,K278(K279()))) is set
BOOLEAN is non empty set
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty non pair V21() V22() V23() V25() V26() V27() V28() V29() V32() cardinal {} -element V37() FinSequence-like FinSubsequence-like FinSequence-membered non with_pair nonpair-yielding ext-real non positive non negative V115() V126() Element of NAT
{0,1} is non empty V28() V32() non with_pair set
2 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
2 -tuples_on BOOLEAN is functional non empty FinSequence-membered FinSequenceSet of BOOLEAN
K28((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K27(K28((2 -tuples_on BOOLEAN),BOOLEAN)) is set
3 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
3 -tuples_on BOOLEAN is functional non empty FinSequence-membered FinSequenceSet of BOOLEAN
K28((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K27(K28((3 -tuples_on BOOLEAN),BOOLEAN)) is set
'xor' is Relation-like Function-like V18(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((2 -tuples_on BOOLEAN),BOOLEAN))
1 -tuples_on BOOLEAN is functional non empty FinSequence-membered FinSequenceSet of BOOLEAN
K28((1 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K27(K28((1 -tuples_on BOOLEAN),BOOLEAN)) is set
Seg 1 is non empty V12() V28() 1 -element Element of K27(NAT)
K28(NAT,NAT) is Relation-like V12() V28() set
K27(K28(NAT,NAT)) is V12() V28() set
xor2 is Relation-like Function-like V18(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((2 -tuples_on BOOLEAN),BOOLEAN))
and2 is Relation-like Function-like V18(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((2 -tuples_on BOOLEAN),BOOLEAN))
xor2c is Relation-like Function-like V18(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((2 -tuples_on BOOLEAN),BOOLEAN))
and2c is Relation-like Function-like V18(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((2 -tuples_on BOOLEAN),BOOLEAN))
and2a is Relation-like Function-like V18(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((2 -tuples_on BOOLEAN),BOOLEAN))
0 -tuples_on BOOLEAN is functional non empty FinSequence-membered FinSequenceSet of BOOLEAN
FALSE is boolean Element of BOOLEAN
(0 -tuples_on BOOLEAN) --> FALSE is Relation-like Function-like V18(0 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((0 -tuples_on BOOLEAN),BOOLEAN))
K28((0 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K27(K28((0 -tuples_on BOOLEAN),BOOLEAN)) is set
1GateCircStr ({},((0 -tuples_on BOOLEAN) --> FALSE)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[{},((0 -tuples_on BOOLEAN) --> FALSE)] is non empty pair set
n is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
f is Relation-like NAT -defined Function-like V28() FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined Function-like V28() FinSequence-like FinSubsequence-like set
h0 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
N is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn is Relation-like NAT -defined Function-like V14( NAT ) set
Sn . n is set
Sn . 0 is set
An is Relation-like NAT -defined Function-like V14( NAT ) set
An . 0 is set
h is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
o0 is Relation-like NAT -defined Function-like V14( NAT ) set
o0 . n is set
o0 . 0 is set
f1 is Relation-like NAT -defined Function-like V14( NAT ) set
f1 . 0 is set
h0 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
N is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h is Relation-like NAT -defined Function-like V14( NAT ) set
h . h0 is set
h . 0 is set
Sn is Relation-like NAT -defined Function-like V14( NAT ) set
Sn . 0 is set
n is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
f is Relation-like NAT -defined Function-like V28() FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined Function-like V28() FinSequence-like FinSubsequence-like set
(n,f,g) is non empty non void V56() 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 V95( 1GateCircStr ({},((0 -tuples_on BOOLEAN) --> FALSE))) gate`2=den Boolean MSAlgebra over 1GateCircStr ({},((0 -tuples_on BOOLEAN) --> FALSE))
h is non empty V56() ManySortedSign
o0 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
o0 + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (o0 + 1) is set
g . (o0 + 1) is set
An is set
BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (o0 + 1)),(g . (o0 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2] is non empty pair set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (o0 + 1)),An*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(g . (o0 + 1)),An*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*An,(f . (o0 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*An,(f . (o0 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) +* (1GateCircStr (<*An,(f . (o0 + 1))*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
or3 is Relation-like Function-like V18(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((3 -tuples_on BOOLEAN),BOOLEAN))
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2] is non empty pair set
[<*(g . (o0 + 1)),An*>,and2] is non empty pair set
[<*An,(f . (o0 + 1))*>,and2] is non empty pair set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*> is Relation-like NAT -defined Function-like non empty V28() 3 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn is non-empty MSAlgebra over h
BitGFA0Circ ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An)
GFA0AdderCirc ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)
2GatesCircuit ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2) is strict non-empty finitely-generated V95( 2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2)) gate`2=den Boolean MSAlgebra over 2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2)
1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)
1GateCircuit (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)
1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An,xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)
1GateCircuit (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)
(1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),xor2)) +* (1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An,xor2)) is strict non-empty finitely-generated V95((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2))
GFA0CarryCirc ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An)
GFA0CarryICirc ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)
1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)
1GateCircuit (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)
1GateCircuit ((g . (o0 + 1)),An,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)
1GateCircuit (<*(g . (o0 + 1)),An*>,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)
(1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),and2)) +* (1GateCircuit ((g . (o0 + 1)),An,and2)) is strict non-empty finitely-generated V95((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))
1GateCircuit (An,(f . (o0 + 1)),and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)
1GateCircuit (<*An,(f . (o0 + 1))*>,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)
((1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),and2)) +* (1GateCircuit ((g . (o0 + 1)),An,and2))) +* (1GateCircuit (An,(f . (o0 + 1)),and2)) is strict non-empty finitely-generated V95(((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) +* (1GateCircStr (<*An,(f . (o0 + 1))*>,and2))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) +* (1GateCircStr (<*An,(f . (o0 + 1))*>,and2))
1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2],or3) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)
1GateCircuit (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)
(GFA0CarryICirc ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2],or3)) is strict non-empty finitely-generated V95((GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3))) gate`2=den Boolean MSAlgebra over (GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3))
(GFA0AdderCirc ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryCirc ((f . (o0 + 1)),(g . (o0 + 1)),An)) is strict non-empty finitely-generated V95((GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An))) gate`2=den Boolean MSAlgebra over (GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An))
Sn +* (BitGFA0Circ ((f . (o0 + 1)),(g . (o0 + 1)),An)) is strict non-empty MSAlgebra over h +* (BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An))
h +* (BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V56() strict ManySortedSign
An is Relation-like NAT -defined Function-like V14( NAT ) set
An . n is set
h is strict non-empty finitely-generated V95((n,f,g)) gate`2=den Boolean MSAlgebra over (n,f,g)
o0 is Relation-like NAT -defined Function-like V14( NAT ) set
o0 . n is set
An . 0 is set
o0 . 0 is set
f1 is Relation-like NAT -defined Function-like V14( NAT ) set
f1 . 0 is set
g1 is Relation-like NAT -defined Function-like V14( NAT ) set
g1 . n is set
Sn is strict non-empty finitely-generated V95((n,f,g)) gate`2=den Boolean MSAlgebra over (n,f,g)
h1 is Relation-like NAT -defined Function-like V14( NAT ) set
h1 . n is set
g1 . 0 is set
h1 . 0 is set
f1 is Relation-like NAT -defined Function-like V14( NAT ) set
f1 . 0 is set
h is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
An is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
An + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (An + 1) is set
g . (An + 1) is set
Sn is set
BitGFA0Str ((f . (An + 1)),(g . (An + 1)),Sn) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (An + 1)),(g . (An + 1)),Sn) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (An + 1)),(g . (An + 1)),Sn,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (An + 1)),(g . (An + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (An + 1)),(g . (An + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (An + 1)),(g . (An + 1))*>,xor2] is non empty pair set
<*[<*(f . (An + 1)),(g . (An + 1))*>,xor2],Sn*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (An + 1)),(g . (An + 1))*>,xor2],Sn*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (An + 1)),(g . (An + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (An + 1)),(g . (An + 1))*>,xor2],Sn*>,xor2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((f . (An + 1)),(g . (An + 1)),Sn) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((f . (An + 1)),(g . (An + 1)),Sn) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (An + 1)),(g . (An + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (An + 1)),Sn*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(g . (An + 1)),Sn*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (An + 1)),(g . (An + 1))*>,and2)) +* (1GateCircStr (<*(g . (An + 1)),Sn*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*Sn,(f . (An + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*Sn,(f . (An + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (An + 1)),(g . (An + 1))*>,and2)) +* (1GateCircStr (<*(g . (An + 1)),Sn*>,and2))) +* (1GateCircStr (<*Sn,(f . (An + 1))*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
or3 is Relation-like Function-like V18(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((3 -tuples_on BOOLEAN),BOOLEAN))
[<*(f . (An + 1)),(g . (An + 1))*>,and2] is non empty pair set
[<*(g . (An + 1)),Sn*>,and2] is non empty pair set
[<*Sn,(f . (An + 1))*>,and2] is non empty pair set
<*[<*(f . (An + 1)),(g . (An + 1))*>,and2],[<*(g . (An + 1)),Sn*>,and2],[<*Sn,(f . (An + 1))*>,and2]*> is Relation-like NAT -defined Function-like non empty V28() 3 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (An + 1)),(g . (An + 1))*>,and2],[<*(g . (An + 1)),Sn*>,and2],[<*Sn,(f . (An + 1))*>,and2]*>,or3) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((f . (An + 1)),(g . (An + 1)),Sn)) +* (1GateCircStr (<*[<*(f . (An + 1)),(g . (An + 1))*>,and2],[<*(g . (An + 1)),Sn*>,and2],[<*Sn,(f . (An + 1))*>,and2]*>,or3)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((f . (An + 1)),(g . (An + 1)),Sn)) +* (GFA0CarryStr ((f . (An + 1)),(g . (An + 1)),Sn)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h +* (BitGFA0Str ((f . (An + 1)),(g . (An + 1)),Sn)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
o0 is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
g1 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
g1 + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (g1 + 1) is set
g . (g1 + 1) is set
f1 is set
BitGFA0Str ((f . (g1 + 1)),(g . (g1 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (g1 + 1)),(g . (g1 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (g1 + 1)),(g . (g1 + 1)),f1,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (g1 + 1)),(g . (g1 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (g1 + 1)),(g . (g1 + 1))*>,xor2] is non empty pair set
<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,xor2],f1*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,xor2],f1*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,xor2],f1*>,xor2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((f . (g1 + 1)),(g . (g1 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((f . (g1 + 1)),(g . (g1 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (g1 + 1)),f1*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(g . (g1 + 1)),f1*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2)) +* (1GateCircStr (<*(g . (g1 + 1)),f1*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*f1,(f . (g1 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*f1,(f . (g1 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2)) +* (1GateCircStr (<*(g . (g1 + 1)),f1*>,and2))) +* (1GateCircStr (<*f1,(f . (g1 + 1))*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2] is non empty pair set
[<*(g . (g1 + 1)),f1*>,and2] is non empty pair set
[<*f1,(f . (g1 + 1))*>,and2] is non empty pair set
<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2],[<*(g . (g1 + 1)),f1*>,and2],[<*f1,(f . (g1 + 1))*>,and2]*> is Relation-like NAT -defined Function-like non empty V28() 3 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2],[<*(g . (g1 + 1)),f1*>,and2],[<*f1,(f . (g1 + 1))*>,and2]*>,or3) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((f . (g1 + 1)),(g . (g1 + 1)),f1)) +* (1GateCircStr (<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2],[<*(g . (g1 + 1)),f1*>,and2],[<*f1,(f . (g1 + 1))*>,and2]*>,or3)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((f . (g1 + 1)),(g . (g1 + 1)),f1)) +* (GFA0CarryStr ((f . (g1 + 1)),(g . (g1 + 1)),f1)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
o0 +* (BitGFA0Str ((f . (g1 + 1)),(g . (g1 + 1)),f1)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h1 is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f2 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
f2 + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (f2 + 1) is set
g . (f2 + 1) is set
f1 is set
BitGFA0Str ((f . (f2 + 1)),(g . (f2 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (f2 + 1)),(g . (f2 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (f2 + 1)),(g . (f2 + 1)),f1,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (f2 + 1)),(g . (f2 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (f2 + 1)),(g . (f2 + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (f2 + 1)),(g . (f2 + 1))*>,xor2] is non empty pair set
<*[<*(f . (f2 + 1)),(g . (f2 + 1))*>,xor2],f1*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (f2 + 1)),(g . (f2 + 1))*>,xor2],f1*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (f2 + 1)),(g . (f2 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (f2 + 1)),(g . (f2 + 1))*>,xor2],f1*>,xor2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((f . (f2 + 1)),(g . (f2 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((f . (f2 + 1)),(g . (f2 + 1)),f1) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (f2 + 1)),(g . (f2 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (f2 + 1)),f1*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(g . (f2 + 1)),f1*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (f2 + 1)),(g . (f2 + 1))*>,and2)) +* (1GateCircStr (<*(g . (f2 + 1)),f1*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*f1,(f . (f2 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*f1,(f . (f2 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (f2 + 1)),(g . (f2 + 1))*>,and2)) +* (1GateCircStr (<*(g . (f2 + 1)),f1*>,and2))) +* (1GateCircStr (<*f1,(f . (f2 + 1))*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (f2 + 1)),(g . (f2 + 1))*>,and2] is non empty pair set
[<*(g . (f2 + 1)),f1*>,and2] is non empty pair set
[<*f1,(f . (f2 + 1))*>,and2] is non empty pair set
<*[<*(f . (f2 + 1)),(g . (f2 + 1))*>,and2],[<*(g . (f2 + 1)),f1*>,and2],[<*f1,(f . (f2 + 1))*>,and2]*> is Relation-like NAT -defined Function-like non empty V28() 3 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (f2 + 1)),(g . (f2 + 1))*>,and2],[<*(g . (f2 + 1)),f1*>,and2],[<*f1,(f . (f2 + 1))*>,and2]*>,or3) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((f . (f2 + 1)),(g . (f2 + 1)),f1)) +* (1GateCircStr (<*[<*(f . (f2 + 1)),(g . (f2 + 1))*>,and2],[<*(g . (f2 + 1)),f1*>,and2],[<*f1,(f . (f2 + 1))*>,and2]*>,or3)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((f . (f2 + 1)),(g . (f2 + 1)),f1)) +* (GFA0CarryStr ((f . (f2 + 1)),(g . (f2 + 1)),f1)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h1 +* (BitGFA0Str ((f . (f2 + 1)),(g . (f2 + 1)),f1)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f3 is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
n + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (n + 1) is set
g . (n + 1) is set
f0 is set
BitGFA0Str ((f . (n + 1)),(g . (n + 1)),f0) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (n + 1)),(g . (n + 1)),f0) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (n + 1)),(g . (n + 1)),f0,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (n + 1)),(g . (n + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (n + 1)),(g . (n + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (n + 1)),(g . (n + 1))*>,xor2] is non empty pair set
<*[<*(f . (n + 1)),(g . (n + 1))*>,xor2],f0*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (n + 1)),(g . (n + 1))*>,xor2],f0*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (n + 1)),(g . (n + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (n + 1)),(g . (n + 1))*>,xor2],f0*>,xor2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((f . (n + 1)),(g . (n + 1)),f0) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((f . (n + 1)),(g . (n + 1)),f0) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (n + 1)),(g . (n + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (n + 1)),f0*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(g . (n + 1)),f0*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (n + 1)),(g . (n + 1))*>,and2)) +* (1GateCircStr (<*(g . (n + 1)),f0*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*f0,(f . (n + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*f0,(f . (n + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (n + 1)),(g . (n + 1))*>,and2)) +* (1GateCircStr (<*(g . (n + 1)),f0*>,and2))) +* (1GateCircStr (<*f0,(f . (n + 1))*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (n + 1)),(g . (n + 1))*>,and2] is non empty pair set
[<*(g . (n + 1)),f0*>,and2] is non empty pair set
[<*f0,(f . (n + 1))*>,and2] is non empty pair set
<*[<*(f . (n + 1)),(g . (n + 1))*>,and2],[<*(g . (n + 1)),f0*>,and2],[<*f0,(f . (n + 1))*>,and2]*> is Relation-like NAT -defined Function-like non empty V28() 3 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (n + 1)),(g . (n + 1))*>,and2],[<*(g . (n + 1)),f0*>,and2],[<*f0,(f . (n + 1))*>,and2]*>,or3) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((f . (n + 1)),(g . (n + 1)),f0)) +* (1GateCircStr (<*[<*(f . (n + 1)),(g . (n + 1))*>,and2],[<*(g . (n + 1)),f0*>,and2],[<*f0,(f . (n + 1))*>,and2]*>,or3)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((f . (n + 1)),(g . (n + 1)),f0)) +* (GFA0CarryStr ((f . (n + 1)),(g . (n + 1)),f0)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f3 +* (BitGFA0Str ((f . (n + 1)),(g . (n + 1)),f0)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h2 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
h2 + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (h2 + 1) is set
g . (h2 + 1) is set
g2 is set
BitGFA0Str ((f . (h2 + 1)),(g . (h2 + 1)),g2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (h2 + 1)),(g . (h2 + 1)),g2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (h2 + 1)),(g . (h2 + 1)),g2,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (h2 + 1)),(g . (h2 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (h2 + 1)),(g . (h2 + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (h2 + 1)),(g . (h2 + 1))*>,xor2] is non empty pair set
<*[<*(f . (h2 + 1)),(g . (h2 + 1))*>,xor2],g2*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (h2 + 1)),(g . (h2 + 1))*>,xor2],g2*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (h2 + 1)),(g . (h2 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (h2 + 1)),(g . (h2 + 1))*>,xor2],g2*>,xor2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((f . (h2 + 1)),(g . (h2 + 1)),g2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((f . (h2 + 1)),(g . (h2 + 1)),g2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (h2 + 1)),(g . (h2 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (h2 + 1)),g2*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(g . (h2 + 1)),g2*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (h2 + 1)),(g . (h2 + 1))*>,and2)) +* (1GateCircStr (<*(g . (h2 + 1)),g2*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*g2,(f . (h2 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*g2,(f . (h2 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (h2 + 1)),(g . (h2 + 1))*>,and2)) +* (1GateCircStr (<*(g . (h2 + 1)),g2*>,and2))) +* (1GateCircStr (<*g2,(f . (h2 + 1))*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (h2 + 1)),(g . (h2 + 1))*>,and2] is non empty pair set
[<*(g . (h2 + 1)),g2*>,and2] is non empty pair set
[<*g2,(f . (h2 + 1))*>,and2] is non empty pair set
<*[<*(f . (h2 + 1)),(g . (h2 + 1))*>,and2],[<*(g . (h2 + 1)),g2*>,and2],[<*g2,(f . (h2 + 1))*>,and2]*> is Relation-like NAT -defined Function-like non empty V28() 3 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (h2 + 1)),(g . (h2 + 1))*>,and2],[<*(g . (h2 + 1)),g2*>,and2],[<*g2,(f . (h2 + 1))*>,and2]*>,or3) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((f . (h2 + 1)),(g . (h2 + 1)),g2)) +* (1GateCircStr (<*[<*(f . (h2 + 1)),(g . (h2 + 1))*>,and2],[<*(g . (h2 + 1)),g2*>,and2],[<*g2,(f . (h2 + 1))*>,and2]*>,or3)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((f . (h2 + 1)),(g . (h2 + 1)),g2)) +* (GFA0CarryStr ((f . (h2 + 1)),(g . (h2 + 1)),g2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x +* (BitGFA0Str ((f . (h2 + 1)),(g . (h2 + 1)),g2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h is non empty V56() ManySortedSign
o0 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
o0 + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (o0 + 1) is set
g . (o0 + 1) is set
An is set
BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (o0 + 1)),(g . (o0 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2] is non empty pair set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (o0 + 1)),An*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(g . (o0 + 1)),An*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*An,(f . (o0 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*An,(f . (o0 + 1))*>,and2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) +* (1GateCircStr (<*An,(f . (o0 + 1))*>,and2)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
or3 is Relation-like Function-like V18(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K27(K28((3 -tuples_on BOOLEAN),BOOLEAN))
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2] is non empty pair set
[<*(g . (o0 + 1)),An*>,and2] is non empty pair set
[<*An,(f . (o0 + 1))*>,and2] is non empty pair set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*> is Relation-like NAT -defined Function-like non empty V28() 3 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn is non-empty MSAlgebra over h
BitGFA0Circ ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An)
GFA0AdderCirc ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)
2GatesCircuit ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2) is strict non-empty finitely-generated V95( 2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2)) gate`2=den Boolean MSAlgebra over 2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,xor2)
1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)
1GateCircuit (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)
1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An,xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)
1GateCircuit (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2)
(1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),xor2)) +* (1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An,xor2)) is strict non-empty finitely-generated V95((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,xor2],An*>,xor2))
GFA0CarryCirc ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An)
GFA0CarryICirc ((f . (o0 + 1)),(g . (o0 + 1)),An) is strict non-empty finitely-generated V95( GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) gate`2=den Boolean MSAlgebra over GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)
1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)
1GateCircuit (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)
1GateCircuit ((g . (o0 + 1)),An,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)
1GateCircuit (<*(g . (o0 + 1)),An*>,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (o0 + 1)),An*>,and2)
(1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),and2)) +* (1GateCircuit ((g . (o0 + 1)),An,and2)) is strict non-empty finitely-generated V95((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))
1GateCircuit (An,(f . (o0 + 1)),and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)
1GateCircuit (<*An,(f . (o0 + 1))*>,and2) is strict non-empty finitely-generated V95( 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*An,(f . (o0 + 1))*>,and2)
((1GateCircuit ((f . (o0 + 1)),(g . (o0 + 1)),and2)) +* (1GateCircuit ((g . (o0 + 1)),An,and2))) +* (1GateCircuit (An,(f . (o0 + 1)),and2)) is strict non-empty finitely-generated V95(((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) +* (1GateCircStr (<*An,(f . (o0 + 1))*>,and2))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) +* (1GateCircStr (<*An,(f . (o0 + 1))*>,and2))
1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2],or3) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)
1GateCircuit (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3) is strict non-empty finitely-generated V95( 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3)
(GFA0CarryICirc ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircuit ([<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2],or3)) is strict non-empty finitely-generated V95((GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3))) gate`2=den Boolean MSAlgebra over (GFA0CarryIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2],[<*(g . (o0 + 1)),An*>,and2],[<*An,(f . (o0 + 1))*>,and2]*>,or3))
(GFA0AdderCirc ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryCirc ((f . (o0 + 1)),(g . (o0 + 1)),An)) is strict non-empty finitely-generated V95((GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An))) gate`2=den Boolean MSAlgebra over (GFA0AdderStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (GFA0CarryStr ((f . (o0 + 1)),(g . (o0 + 1)),An))
Sn +* (BitGFA0Circ ((f . (o0 + 1)),(g . (o0 + 1)),An)) is strict non-empty MSAlgebra over h +* (BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An))
h +* (BitGFA0Str ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V56() strict ManySortedSign
h is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f1 is non pair V21() V22() V23() V27() V28() cardinal ext-real non negative V115() V126() set
f1 + 1 is non empty non pair V21() V22() V23() V27() V28() cardinal ext-real positive non negative V115() V126() Element of NAT
f . (f1 + 1) is set
g . (f1 + 1) is set
o0 is set
BitGFA0Str ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (f1 + 1)),(g . (f1 + 1))*> is Relation-like NAT -defined Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,xor2) is non empty non void V56() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[