K96() is set
K100() is non empty V21() V22() V23() V34() V49() V50() Element of K27(K96())
K27(K96()) is set
K97() is set
K98() is set
K99() is set
K28(K97(),K97()) is Relation-like set
K27(K28(K97(),K97())) is set
K28(K28(K97(),K97()),K97()) is Relation-like set
K27(K28(K28(K97(),K97()),K97())) is set
K28(K96(),K96()) is Relation-like set
K27(K28(K96(),K96())) is set
K28(K28(K96(),K96()),K96()) is Relation-like set
K27(K28(K28(K96(),K96()),K96())) is set
K28(K98(),K98()) is Relation-like set
K27(K28(K98(),K98())) is set
K28(K28(K98(),K98()),K98()) is Relation-like set
K27(K28(K28(K98(),K98()),K98())) is set
K28(K99(),K99()) is Relation-like set
K27(K28(K99(),K99())) is set
K28(K28(K99(),K99()),K99()) is Relation-like set
K27(K28(K28(K99(),K99()),K99())) is set
K28(K100(),K100()) is Relation-like set
K28(K28(K100(),K100()),K100()) is Relation-like set
K27(K28(K28(K100(),K100()),K100())) is set
K95() is non empty V21() V22() V23() V34() V49() V50() set
K27(K95()) is set
K27(K100()) is set
BOOLEAN is non empty set
1 is non empty non pair V21() V22() V23() V27() Element of K100()
{} is set
{{},1} is set
K342() is set
K27(K342()) is set
K343() is Element of K27(K342())
K383() is non empty V93() L10()
the carrier of K383() is set
K346( the carrier of K383()) is non empty M24( the carrier of K383())
K382(K383()) is Element of K27(K346( the carrier of K383()))
K27(K346( the carrier of K383())) is set
K28(K382(K383()),K100()) is Relation-like set
K27(K28(K382(K383()),K100())) is set
K28(K100(),K382(K383())) is Relation-like set
K27(K28(K100(),K382(K383()))) is set
2 is non empty non pair V21() V22() V23() V27() Element of K100()
K237(2,BOOLEAN) is M8( BOOLEAN )
K28(K237(2,BOOLEAN),BOOLEAN) is Relation-like set
K27(K28(K237(2,BOOLEAN),BOOLEAN)) is set
3 is non empty non pair V21() V22() V23() V27() Element of K100()
K237(3,BOOLEAN) is M8( BOOLEAN )
K28(K237(3,BOOLEAN),BOOLEAN) is Relation-like set
K27(K28(K237(3,BOOLEAN),BOOLEAN)) is set
'xor' is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
K237(1,BOOLEAN) is M8( BOOLEAN )
K28(K237(1,BOOLEAN),BOOLEAN) is Relation-like set
K27(K28(K237(1,BOOLEAN),BOOLEAN)) is set
and2 is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
and2a is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
and2b is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
xor2 is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
K101() is non pair V21() V22() V23() V27() Element of K100()
<*K101(),K101()*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
and2 . <*K101(),K101()*> is boolean set
<*K101(),1*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
and2 . <*K101(),1*> is boolean set
<*1,K101()*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
and2 . <*1,K101()*> is boolean set
<*1,1*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
and2 . <*1,1*> is boolean set
and2a . <*K101(),K101()*> is boolean set
and2a . <*K101(),1*> is boolean set
and2a . <*1,K101()*> is boolean set
and2a . <*1,1*> is boolean set
and2b . <*K101(),K101()*> is boolean set
and2b . <*K101(),1*> is boolean set
and2b . <*1,K101()*> is boolean set
and2b . <*1,1*> is boolean set
xor2 . <*K101(),K101()*> is boolean set
xor2 . <*K101(),1*> is boolean set
xor2 . <*1,K101()*> is boolean set
xor2 . <*1,1*> is boolean set
xor2a is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
xor2a . <*K101(),K101()*> is boolean set
xor2a . <*K101(),1*> is boolean set
xor2a . <*1,K101()*> is boolean set
xor2a . <*1,1*> is boolean set
or3 is Relation-like Function-like V18(K237(3,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(3,BOOLEAN),BOOLEAN))
nor3 is Relation-like Function-like V18(K237(3,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(3,BOOLEAN),BOOLEAN))
and2c is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
nor2a is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
and2c . <*K101(),K101()*> is boolean set
and2c . <*K101(),1*> is boolean set
and2c . <*1,K101()*> is boolean set
and2c . <*1,1*> is boolean set
xor2c is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
or2 is Relation-like Function-like V18(K237(2,BOOLEAN), BOOLEAN ) boolean-valued Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
xor2c . <*K101(),K101()*> is boolean set
xor2c . <*K101(),1*> is boolean set
xor2c . <*1,K101()*> is boolean set
xor2c . <*1,1*> is boolean set
n1 is set
n2 is set
am is set
BitGFA0Str (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (n1,n2,am,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n1,n2*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n1,n2*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,xor2] is non empty pair set
<*[<*n1,n2*>,xor2],am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,xor2)) +* (1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*n1,n2*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n2,am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n2,am*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*am,n1*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*am,n1*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))) +* (1GateCircStr (<*am,n1*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,and2] is non empty pair set
[<*n2,am*>,and2] is non empty pair set
[<*am,n1*>,and2] is non empty pair set
<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr (n1,n2,am)) +* (1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr (n1,n2,am)) +* (GFA0CarryStr (n1,n2,am)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderOutput (n1,n2,am) is Element of InnerVertices (GFA0AdderStr (n1,n2,am))
the carrier of (GFA0AdderStr (n1,n2,am)) is set
InnerVertices (GFA0AdderStr (n1,n2,am)) is Element of K27( the carrier of (GFA0AdderStr (n1,n2,am)))
K27( the carrier of (GFA0AdderStr (n1,n2,am))) is set
2GatesCircOutput (n1,n2,am,xor2) is non empty pair Element of InnerVertices (2GatesCircStr (n1,n2,am,xor2))
the carrier of (2GatesCircStr (n1,n2,am,xor2)) is set
InnerVertices (2GatesCircStr (n1,n2,am,xor2)) is Element of K27( the carrier of (2GatesCircStr (n1,n2,am,xor2)))
K27( the carrier of (2GatesCircStr (n1,n2,am,xor2))) is set
[<*[<*n1,n2*>,xor2],am*>,xor2] is non empty pair set
cm is set
bm is set
BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(GFA0AdderOutput (n1,n2,am)),cm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*cm,bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*cm,bm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*bm,(GFA0AdderOutput (n1,n2,am))*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))) +* (1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2] is non empty pair set
[<*cm,bm*>,and2] is non empty pair set
[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BitGFA0Str (n1,n2,am)) +* (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n1 is set
n2 is set
am is set
BitGFA0Str (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (n1,n2,am,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n1,n2*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n1,n2*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,xor2] is non empty pair set
<*[<*n1,n2*>,xor2],am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,xor2)) +* (1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*n1,n2*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n2,am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n2,am*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*am,n1*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*am,n1*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))) +* (1GateCircStr (<*am,n1*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,and2] is non empty pair set
[<*n2,am*>,and2] is non empty pair set
[<*am,n1*>,and2] is non empty pair set
<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr (n1,n2,am)) +* (1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr (n1,n2,am)) +* (GFA0CarryStr (n1,n2,am)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderOutput (n1,n2,am) is Element of InnerVertices (GFA0AdderStr (n1,n2,am))
the carrier of (GFA0AdderStr (n1,n2,am)) is set
InnerVertices (GFA0AdderStr (n1,n2,am)) is Element of K27( the carrier of (GFA0AdderStr (n1,n2,am)))
K27( the carrier of (GFA0AdderStr (n1,n2,am))) is set
2GatesCircOutput (n1,n2,am,xor2) is non empty pair Element of InnerVertices (2GatesCircStr (n1,n2,am,xor2))
the carrier of (2GatesCircStr (n1,n2,am,xor2)) is set
InnerVertices (2GatesCircStr (n1,n2,am,xor2)) is Element of K27( the carrier of (2GatesCircStr (n1,n2,am,xor2)))
K27( the carrier of (2GatesCircStr (n1,n2,am,xor2))) is set
[<*[<*n1,n2*>,xor2],am*>,xor2] is non empty pair set
cm is set
bm is set
BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(GFA0AdderOutput (n1,n2,am)),cm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*cm,bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*cm,bm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*bm,(GFA0AdderOutput (n1,n2,am))*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))) +* (1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2] is non empty pair set
[<*cm,bm*>,and2] is non empty pair set
[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BitGFA0Circ (n1,n2,am) is strict non-empty V105( BitGFA0Str (n1,n2,am)) gate`2=den Boolean MSAlgebra over BitGFA0Str (n1,n2,am)
GFA0AdderCirc (n1,n2,am) is strict non-empty V105( GFA0AdderStr (n1,n2,am)) gate`2=den Boolean MSAlgebra over GFA0AdderStr (n1,n2,am)
2GatesCircuit (n1,n2,am,xor2) is strict non-empty V105( 2GatesCircStr (n1,n2,am,xor2)) gate`2=den Boolean MSAlgebra over 2GatesCircStr (n1,n2,am,xor2)
1GateCircuit (n1,n2,xor2) is strict non-empty V105( 1GateCircStr (<*n1,n2*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*n1,n2*>,xor2)
1GateCircuit (<*n1,n2*>,xor2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*n1,n2*>,xor2)
1GateCircuit ([<*n1,n2*>,xor2],am,xor2) is strict non-empty V105( 1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2)
1GateCircuit (<*[<*n1,n2*>,xor2],am*>,xor2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2)
(1GateCircuit (n1,n2,xor2)) +* (1GateCircuit ([<*n1,n2*>,xor2],am,xor2)) is strict non-empty V105((1GateCircStr (<*n1,n2*>,xor2)) +* (1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*n1,n2*>,xor2)) +* (1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2))
GFA0CarryCirc (n1,n2,am) is strict non-empty V105( GFA0CarryStr (n1,n2,am)) gate`2=den Boolean MSAlgebra over GFA0CarryStr (n1,n2,am)
GFA0CarryICirc (n1,n2,am) is strict non-empty V105( GFA0CarryIStr (n1,n2,am)) gate`2=den Boolean MSAlgebra over GFA0CarryIStr (n1,n2,am)
1GateCircuit (n1,n2,and2) is strict non-empty V105( 1GateCircStr (<*n1,n2*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*n1,n2*>,and2)
1GateCircuit (<*n1,n2*>,and2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*n1,n2*>,and2)
1GateCircuit (n2,am,and2) is strict non-empty V105( 1GateCircStr (<*n2,am*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*n2,am*>,and2)
1GateCircuit (<*n2,am*>,and2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*n2,am*>,and2)
(1GateCircuit (n1,n2,and2)) +* (1GateCircuit (n2,am,and2)) is strict non-empty V105((1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))
1GateCircuit (am,n1,and2) is strict non-empty V105( 1GateCircStr (<*am,n1*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*am,n1*>,and2)
1GateCircuit (<*am,n1*>,and2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*am,n1*>,and2)
((1GateCircuit (n1,n2,and2)) +* (1GateCircuit (n2,am,and2))) +* (1GateCircuit (am,n1,and2)) is strict non-empty V105(((1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))) +* (1GateCircStr (<*am,n1*>,and2))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))) +* (1GateCircStr (<*am,n1*>,and2))
1GateCircuit ([<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],or3) is strict non-empty V105( 1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3)
1GateCircuit (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3)
(GFA0CarryICirc (n1,n2,am)) +* (1GateCircuit ([<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],or3)) is strict non-empty V105((GFA0CarryIStr (n1,n2,am)) +* (1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3))) gate`2=den Boolean MSAlgebra over (GFA0CarryIStr (n1,n2,am)) +* (1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3))
(GFA0AdderCirc (n1,n2,am)) +* (GFA0CarryCirc (n1,n2,am)) is strict non-empty V105((GFA0AdderStr (n1,n2,am)) +* (GFA0CarryStr (n1,n2,am))) gate`2=den Boolean MSAlgebra over (GFA0AdderStr (n1,n2,am)) +* (GFA0CarryStr (n1,n2,am))
BitGFA0Circ ((GFA0AdderOutput (n1,n2,am)),cm,bm) is strict non-empty V105( BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) gate`2=den Boolean MSAlgebra over BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)
GFA0AdderCirc ((GFA0AdderOutput (n1,n2,am)),cm,bm) is strict non-empty V105( GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) gate`2=den Boolean MSAlgebra over GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)
2GatesCircuit ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2) is strict non-empty V105( 2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2)) gate`2=den Boolean MSAlgebra over 2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2)
1GateCircuit ((GFA0AdderOutput (n1,n2,am)),cm,xor2) is strict non-empty V105( 1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)
1GateCircuit (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)
1GateCircuit ([<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm,xor2) is strict non-empty V105( 1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2)
1GateCircuit (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2)
(1GateCircuit ((GFA0AdderOutput (n1,n2,am)),cm,xor2)) +* (1GateCircuit ([<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm,xor2)) is strict non-empty V105((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2))
GFA0CarryCirc ((GFA0AdderOutput (n1,n2,am)),cm,bm) is strict non-empty V105( GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) gate`2=den Boolean MSAlgebra over GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)
GFA0CarryICirc ((GFA0AdderOutput (n1,n2,am)),cm,bm) is strict non-empty V105( GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) gate`2=den Boolean MSAlgebra over GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)
1GateCircuit ((GFA0AdderOutput (n1,n2,am)),cm,and2) is strict non-empty V105( 1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)
1GateCircuit (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)
1GateCircuit (cm,bm,and2) is strict non-empty V105( 1GateCircStr (<*cm,bm*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*cm,bm*>,and2)
1GateCircuit (<*cm,bm*>,and2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*cm,bm*>,and2)
(1GateCircuit ((GFA0AdderOutput (n1,n2,am)),cm,and2)) +* (1GateCircuit (cm,bm,and2)) is strict non-empty V105((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))
1GateCircuit (bm,(GFA0AdderOutput (n1,n2,am)),and2) is strict non-empty V105( 1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2)
1GateCircuit (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2)
((1GateCircuit ((GFA0AdderOutput (n1,n2,am)),cm,and2)) +* (1GateCircuit (cm,bm,and2))) +* (1GateCircuit (bm,(GFA0AdderOutput (n1,n2,am)),and2)) is strict non-empty V105(((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))) +* (1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))) +* (1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2))
1GateCircuit ([<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2],or3) is strict non-empty V105( 1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3)
1GateCircuit (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3) is strict non-empty gate`2=den MSAlgebra over 1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3)
(GFA0CarryICirc ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (1GateCircuit ([<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2],or3)) is strict non-empty V105((GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3))) gate`2=den Boolean MSAlgebra over (GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3))
(GFA0AdderCirc ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (GFA0CarryCirc ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is strict non-empty V105((GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm))) gate`2=den Boolean MSAlgebra over (GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm))
(BitGFA0Circ (n1,n2,am)) +* (BitGFA0Circ ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is strict non-empty V105((BitGFA0Str (n1,n2,am)) +* (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) gate`2=den Boolean MSAlgebra over (BitGFA0Str (n1,n2,am)) +* (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))
(BitGFA0Str (n1,n2,am)) +* (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(n1,n2,am,bm,cm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n1 is set
n2 is set
am is set
bm is set
cm is set
(n1,n2,am,bm,cm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BitGFA0Str (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (n1,n2,am,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n1,n2*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n1,n2*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,xor2] is non empty pair set
<*[<*n1,n2*>,xor2],am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,xor2)) +* (1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*n1,n2*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n2,am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n2,am*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*am,n1*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*am,n1*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))) +* (1GateCircStr (<*am,n1*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,and2] is non empty pair set
[<*n2,am*>,and2] is non empty pair set
[<*am,n1*>,and2] is non empty pair set
<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr (n1,n2,am)) +* (1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr (n1,n2,am)) +* (GFA0CarryStr (n1,n2,am)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderOutput (n1,n2,am) is Element of InnerVertices (GFA0AdderStr (n1,n2,am))
the carrier of (GFA0AdderStr (n1,n2,am)) is set
InnerVertices (GFA0AdderStr (n1,n2,am)) is Element of K27( the carrier of (GFA0AdderStr (n1,n2,am)))
K27( the carrier of (GFA0AdderStr (n1,n2,am))) is set
2GatesCircOutput (n1,n2,am,xor2) is non empty pair Element of InnerVertices (2GatesCircStr (n1,n2,am,xor2))
the carrier of (2GatesCircStr (n1,n2,am,xor2)) is set
InnerVertices (2GatesCircStr (n1,n2,am,xor2)) is Element of K27( the carrier of (2GatesCircStr (n1,n2,am,xor2)))
K27( the carrier of (2GatesCircStr (n1,n2,am,xor2))) is set
[<*[<*n1,n2*>,xor2],am*>,xor2] is non empty pair set
BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(GFA0AdderOutput (n1,n2,am)),cm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*cm,bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*cm,bm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*bm,(GFA0AdderOutput (n1,n2,am))*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))) +* (1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2] is non empty pair set
[<*cm,bm*>,and2] is non empty pair set
[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BitGFA0Str (n1,n2,am)) +* (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (n1,n2,am,bm,cm) is Element of K27( the carrier of (n1,n2,am,bm,cm))
the carrier of (n1,n2,am,bm,cm) is set
K27( the carrier of (n1,n2,am,bm,cm)) is set
{[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} is set
GFA0CarryOutput (n1,n2,am) is Element of InnerVertices (GFA0CarryStr (n1,n2,am))
the carrier of (GFA0CarryStr (n1,n2,am)) is set
InnerVertices (GFA0CarryStr (n1,n2,am)) is Element of K27( the carrier of (GFA0CarryStr (n1,n2,am)))
K27( the carrier of (GFA0CarryStr (n1,n2,am))) is set
[<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3] is non empty pair set
{[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))} is set
{[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))} is set
GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm) is Element of InnerVertices (GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm))
the carrier of (GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is set
InnerVertices (GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is Element of K27( the carrier of (GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)))
K27( the carrier of (GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
2GatesCircOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2) is non empty pair Element of InnerVertices (2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2))
the carrier of (2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2)) is set
InnerVertices (2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2)) is Element of K27( the carrier of (2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2)))
K27( the carrier of (2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2))) is set
[<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2] is non empty pair set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))}) \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm) is Element of InnerVertices (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm))
the carrier of (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is set
InnerVertices (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is Element of K27( the carrier of (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)))
K27( the carrier of (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
[<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3] is non empty pair set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
(({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))}) \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
InnerVertices (BitGFA0Str (n1,n2,am)) is Element of K27( the carrier of (BitGFA0Str (n1,n2,am)))
the carrier of (BitGFA0Str (n1,n2,am)) is set
K27( the carrier of (BitGFA0Str (n1,n2,am))) is set
InnerVertices (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is Element of K27( the carrier of (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)))
the carrier of (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is set
K27( the carrier of (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
(InnerVertices (BitGFA0Str (n1,n2,am))) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
{[<*n1,n2*>,xor2]} is Relation-like Function-like set
{(GFA0AdderOutput (n1,n2,am))} is set
{[<*n1,n2*>,xor2]} \/ {(GFA0AdderOutput (n1,n2,am))} is set
{[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]} is Relation-like set
({[<*n1,n2*>,xor2]} \/ {(GFA0AdderOutput (n1,n2,am))}) \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]} is set
{(GFA0CarryOutput (n1,n2,am))} is set
(({[<*n1,n2*>,xor2]} \/ {(GFA0AdderOutput (n1,n2,am))}) \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]}) \/ {(GFA0CarryOutput (n1,n2,am))} is set
((({[<*n1,n2*>,xor2]} \/ {(GFA0AdderOutput (n1,n2,am))}) \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]}) \/ {(GFA0CarryOutput (n1,n2,am))}) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
{[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]} is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]}) \/ {(GFA0CarryOutput (n1,n2,am))} is set
(({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]}) \/ {(GFA0CarryOutput (n1,n2,am))}) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
{[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]} \/ {(GFA0CarryOutput (n1,n2,am))} is set
{[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ ({[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]} \/ {(GFA0CarryOutput (n1,n2,am))}) is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ ({[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]} \/ {(GFA0CarryOutput (n1,n2,am))})) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))}) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2]} is Relation-like Function-like set
{(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]} is Relation-like set
({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]} is set
{(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
(({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))}) \/ ((({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) is set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]} is set
({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))}) \/ (({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) is set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]} \/ {(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} \/ ({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]} \/ {(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))}) \/ ({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} \/ ({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]} \/ {(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))})) is set
{[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} is set
({[<*n1,n2*>,xor2],(GFA0AdderOutput (n1,n2,am))} \/ {[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2],(GFA0CarryOutput (n1,n2,am))}) \/ ({[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))} \/ {[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (n1,n2,am)),cm,bm))}) is set
n1 is set
n2 is set
am is set
bm is set
cm is set
(n1,n2,am,bm,cm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BitGFA0Str (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (n1,n2,am,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n1,n2*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n1,n2*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,xor2] is non empty pair set
<*[<*n1,n2*>,xor2],am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,xor2)) +* (1GateCircStr (<*[<*n1,n2*>,xor2],am*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*n1,n2*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n2,am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n2,am*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*am,n1*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*am,n1*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*n1,n2*>,and2)) +* (1GateCircStr (<*n2,am*>,and2))) +* (1GateCircStr (<*am,n1*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,and2] is non empty pair set
[<*n2,am*>,and2] is non empty pair set
[<*am,n1*>,and2] is non empty pair set
<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr (n1,n2,am)) +* (1GateCircStr (<*[<*n1,n2*>,and2],[<*n2,am*>,and2],[<*am,n1*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr (n1,n2,am)) +* (GFA0CarryStr (n1,n2,am)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderOutput (n1,n2,am) is Element of InnerVertices (GFA0AdderStr (n1,n2,am))
the carrier of (GFA0AdderStr (n1,n2,am)) is set
InnerVertices (GFA0AdderStr (n1,n2,am)) is Element of K27( the carrier of (GFA0AdderStr (n1,n2,am)))
K27( the carrier of (GFA0AdderStr (n1,n2,am))) is set
2GatesCircOutput (n1,n2,am,xor2) is non empty pair Element of InnerVertices (2GatesCircStr (n1,n2,am,xor2))
the carrier of (2GatesCircStr (n1,n2,am,xor2)) is set
InnerVertices (2GatesCircStr (n1,n2,am,xor2)) is Element of K27( the carrier of (2GatesCircStr (n1,n2,am,xor2)))
K27( the carrier of (2GatesCircStr (n1,n2,am,xor2))) is set
[<*[<*n1,n2*>,xor2],am*>,xor2] is non empty pair set
BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((GFA0AdderOutput (n1,n2,am)),cm,bm,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(GFA0AdderOutput (n1,n2,am)),cm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,xor2],bm*>,xor2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*cm,bm*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*cm,bm*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*bm,(GFA0AdderOutput (n1,n2,am))*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2)) +* (1GateCircStr (<*cm,bm*>,and2))) +* (1GateCircStr (<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2] is non empty pair set
[<*cm,bm*>,and2] is non empty pair set
[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2] is non empty pair set
<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0CarryIStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (1GateCircStr (<*[<*(GFA0AdderOutput (n1,n2,am)),cm*>,and2],[<*cm,bm*>,and2],[<*bm,(GFA0AdderOutput (n1,n2,am))*>,and2]*>,or3)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(GFA0AdderStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) +* (GFA0CarryStr ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BitGFA0Str (n1,n2,am)) +* (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (n1,n2,am,bm,cm) is Element of K27( the carrier of (n1,n2,am,bm,cm))
the carrier of (n1,n2,am,bm,cm) is set
K27( the carrier of (n1,n2,am,bm,cm)) is set
InnerVertices (BitGFA0Str (n1,n2,am)) is Element of K27( the carrier of (BitGFA0Str (n1,n2,am)))
the carrier of (BitGFA0Str (n1,n2,am)) is set
K27( the carrier of (BitGFA0Str (n1,n2,am))) is set
InnerVertices (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is Element of K27( the carrier of (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)))
the carrier of (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm)) is set
K27( the carrier of (BitGFA0Str ((GFA0AdderOutput (n1,n2,am)),cm,bm))) is set
n1 is set
n2 is set
am is set
GFA0AdderOutput (n1,n2,am) is Element of InnerVertices (GFA0AdderStr (n1,n2,am))
GFA0AdderStr (n1,n2,am) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (n1,n2,am,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*n1,n2*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*n1,n2*>,xor2) is non empty non void strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*n1,n2*>,xor2] is non empty pair set
<*[<*n1,n2*>,xor2],am*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (