FSCIRC_2

:: FSCIRC_2 semantic presentation

REAL is set
NAT is non empty V2() V9() V10() V11() V36() cardinal limit_cardinal V51() V52() Element of K18(REAL)
K18(REAL) is set
COMPLEX is set
RAT is set
INT is set
K19(COMPLEX,COMPLEX) is Relation-like set
K18(K19(COMPLEX,COMPLEX)) is set
K19(K19(COMPLEX,COMPLEX),COMPLEX) is Relation-like set
K18(K19(K19(COMPLEX,COMPLEX),COMPLEX)) is set
K19(REAL,REAL) is Relation-like set
K18(K19(REAL,REAL)) is set
K19(K19(REAL,REAL),REAL) is Relation-like set
K18(K19(K19(REAL,REAL),REAL)) is set
K19(RAT,RAT) is Relation-like set
K18(K19(RAT,RAT)) is set
K19(K19(RAT,RAT),RAT) is Relation-like set
K18(K19(K19(RAT,RAT),RAT)) is set
K19(INT,INT) is Relation-like set
K18(K19(INT,INT)) is set
K19(K19(INT,INT),INT) is Relation-like set
K18(K19(K19(INT,INT),INT)) is set
K19(NAT,NAT) is V2() Relation-like V36() set
K19(K19(NAT,NAT),NAT) is V2() Relation-like V36() set
K18(K19(K19(NAT,NAT),NAT)) is V2() V36() set
NAT is non empty V2() V9() V10() V11() V36() cardinal limit_cardinal V51() V52() set
K18(NAT) is V2() V36() set
K18(NAT) is V2() V36() set
BOOLEAN is non empty set
0 is empty Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional non pair V30() V31() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() V51() non with_pair nonpair-yielding ext-real non positive non negative Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional non pair V30() V31() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() V51() non with_pair nonpair-yielding ext-real non positive non negative set
the empty Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional non pair V30() V31() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() V51() non with_pair nonpair-yielding ext-real non positive non negative set is empty Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional non pair V30() V31() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() V51() non with_pair nonpair-yielding ext-real non positive non negative set
1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
{0,1} is non empty V36() V40() V51() non with_pair set
{{},1} is non empty V36() V40() V51() non with_pair set
K348() is set
K18(K348()) is set
K349() is Element of K18(K348())
K389() is non empty V95() L10()
the carrier of K389() is non empty set
K352( the carrier of K389()) is non empty M24( the carrier of K389())
K388(K389()) is Element of K18(K352( the carrier of K389()))
K18(K352( the carrier of K389())) is set
K19(K388(K389()),NAT) is Relation-like set
K18(K19(K388(K389()),NAT)) is set
K19(NAT,K388(K389())) is Relation-like set
K18(K19(NAT,K388(K389()))) is set
2 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
2 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((2 -tuples_on BOOLEAN),BOOLEAN)) is set
3 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
3 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K19((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((3 -tuples_on BOOLEAN),BOOLEAN)) is set
'xor' is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
Seg 1 is non empty V2() V36() 1 -element V51() Element of K18(NAT)
or3 is Relation-like Function-like V27(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((3 -tuples_on BOOLEAN),BOOLEAN))
and2 is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
and2a is Relation-like Function-like V27(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((2 -tuples_on BOOLEAN),BOOLEAN))
K18(K19(NAT,NAT)) is V2() V36() set
f is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like V51() set
g is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like V51() set
0 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
TRUE is boolean Element of BOOLEAN
(0 -tuples_on BOOLEAN) --> TRUE is Relation-like Function-like V27(0 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K18(K19((0 -tuples_on BOOLEAN),BOOLEAN))
K19((0 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K18(K19((0 -tuples_on BOOLEAN),BOOLEAN)) is set
1GateCircStr ({},((0 -tuples_on BOOLEAN) --> TRUE)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
[{},((0 -tuples_on BOOLEAN) --> TRUE)] is non empty pair set
{{},((0 -tuples_on BOOLEAN) --> TRUE)} is non empty functional V36() V51() set
{{}} is non empty V2() functional V36() V40() 1 -element V49() V51() non with_pair set
{{{},((0 -tuples_on BOOLEAN) --> TRUE)},{{}}} is non empty V36() V40() V51() set
S0 is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
N is Relation-like NAT -defined Function-like V23( NAT ) set
N . n is set
N . 0 is set
h is Relation-like NAT -defined Function-like V23( NAT ) set
h . 0 is set
A0 is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn is Relation-like NAT -defined Function-like V23( NAT ) set
Sn . n is set
Sn . 0 is set
An is Relation-like NAT -defined Function-like V23( NAT ) set
An . 0 is set
S0 is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
A0 is Relation-like NAT -defined Function-like V23( NAT ) set
A0 . n is set
A0 . 0 is set
N is Relation-like NAT -defined Function-like V23( NAT ) set
N . 0 is set
n is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
f is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like V51() set
g is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like V51() set
(n,f,g) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircuit ({},((0 -tuples_on BOOLEAN) --> TRUE)) is strict non-empty finitely-generated V107( 1GateCircStr ({},((0 -tuples_on BOOLEAN) --> TRUE))) gate`2=den Boolean MSAlgebra over 1GateCircStr ({},((0 -tuples_on BOOLEAN) --> TRUE))
Sn is non empty V71() ManySortedSign
f1 is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
f1 + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (f1 + 1) is set
g . (f1 + 1) is set
o0 is set
BitSubtracterWithBorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (f1 + 1)),(g . (f1 + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'] is non empty pair set
{<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (f1 + 1)),(g . (f1 + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'},{<*(f . (f1 + 1)),(g . (f1 + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (f1 + 1)),o0*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (f1 + 1)),o0*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (f1 + 1)),o0*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,and2))) +* (1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a] is non empty pair set
{<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a},{<*(f . (f1 + 1)),(g . (f1 + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (f1 + 1)),o0*>,and2] is non empty pair set
{<*(g . (f1 + 1)),o0*>,and2} is non empty functional V36() V51() set
{<*(g . (f1 + 1)),o0*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (f1 + 1)),o0*>,and2},{<*(g . (f1 + 1)),o0*>}} is non empty V36() V40() V51() set
[<*(f . (f1 + 1)),o0*>,and2a] is non empty pair set
{<*(f . (f1 + 1)),o0*>,and2a} is non empty functional V36() V51() set
{<*(f . (f1 + 1)),o0*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (f1 + 1)),o0*>,and2a},{<*(f . (f1 + 1)),o0*>}} is non empty V36() V40() V51() set
<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) +* (BorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
An is non-empty MSAlgebra over Sn
BitSubtracterWithBorrowCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V107( BitSubtracterWithBorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) gate`2=den Boolean MSAlgebra over BitSubtracterWithBorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)
BitSubtracterCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V107( 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')
2GatesCircuit ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor') is strict non-empty finitely-generated V107( 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')
1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),'xor') is strict non-empty finitely-generated V107( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')
1GateCircuit (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor') is strict non-empty finitely-generated V107( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')
1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0,'xor') is strict non-empty finitely-generated V107( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')
1GateCircuit (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor') is strict non-empty finitely-generated V107( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor')
(1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),'xor')) +* (1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0,'xor')) is strict non-empty finitely-generated V107((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor'))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,'xor'],o0*>,'xor'))
BorrowCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V107( BorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) gate`2=den Boolean MSAlgebra over BorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)
BorrowICirc ((f . (f1 + 1)),(g . (f1 + 1)),o0) is strict non-empty finitely-generated V107( BorrowIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) gate`2=den Boolean MSAlgebra over BorrowIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)
1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),and2a) is strict non-empty finitely-generated V107( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)
1GateCircuit (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a) is strict non-empty finitely-generated V107( 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)
1GateCircuit ((g . (f1 + 1)),o0,and2) is strict non-empty finitely-generated V107( 1GateCircStr (<*(g . (f1 + 1)),o0*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (f1 + 1)),o0*>,and2)
1GateCircuit (<*(g . (f1 + 1)),o0*>,and2) is strict non-empty finitely-generated V107( 1GateCircStr (<*(g . (f1 + 1)),o0*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(g . (f1 + 1)),o0*>,and2)
(1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),and2a)) +* (1GateCircuit ((g . (f1 + 1)),o0,and2)) is strict non-empty finitely-generated V107((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,and2))
1GateCircuit ((f . (f1 + 1)),o0,and2a) is strict non-empty finitely-generated V107( 1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a)
1GateCircuit (<*(f . (f1 + 1)),o0*>,and2a) is strict non-empty finitely-generated V107( 1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a)
((1GateCircuit ((f . (f1 + 1)),(g . (f1 + 1)),and2a)) +* (1GateCircuit ((g . (f1 + 1)),o0,and2))) +* (1GateCircuit ((f . (f1 + 1)),o0,and2a)) is strict non-empty finitely-generated V107(((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,and2))) +* (1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (f1 + 1)),o0*>,and2))) +* (1GateCircStr (<*(f . (f1 + 1)),o0*>,and2a))
1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a],or3) is strict non-empty finitely-generated V107( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3)
1GateCircuit (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3) is strict non-empty finitely-generated V107( 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3)
(BorrowICirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircuit ([<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a],or3)) is strict non-empty finitely-generated V107((BorrowIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (BorrowIStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (1GateCircStr (<*[<*(f . (f1 + 1)),(g . (f1 + 1))*>,and2a],[<*(g . (f1 + 1)),o0*>,and2],[<*(f . (f1 + 1)),o0*>,and2a]*>,or3))
(BitSubtracterCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) +* (BorrowCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is strict non-empty finitely-generated V107((2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) +* (BorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0))) gate`2=den Boolean MSAlgebra over (2GatesCircStr ((f . (f1 + 1)),(g . (f1 + 1)),o0,'xor')) +* (BorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0))
An +* (BitSubtracterWithBorrowCirc ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is strict non-empty MSAlgebra over Sn +* (BitSubtracterWithBorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0))
Sn +* (BitSubtracterWithBorrowStr ((f . (f1 + 1)),(g . (f1 + 1)),o0)) is non empty non void V71() strict ManySortedSign
Sn is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
o0 is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
o0 + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (o0 + 1) is set
g . (o0 + 1) is set
An is set
BitSubtracterWithBorrowStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (o0 + 1)),(g . (o0 + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'] is non empty pair set
{<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (o0 + 1)),(g . (o0 + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'},{<*(f . (o0 + 1)),(g . (o0 + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'],An*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'],An*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,'xor'],An*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (o0 + 1)),(g . (o0 + 1)),An) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (o0 + 1)),An*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (o0 + 1)),An*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (o0 + 1)),An*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (o0 + 1)),An*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (o0 + 1)),An*>,and2))) +* (1GateCircStr (<*(f . (o0 + 1)),An*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a] is non empty pair set
{<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a},{<*(f . (o0 + 1)),(g . (o0 + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (o0 + 1)),An*>,and2] is non empty pair set
{<*(g . (o0 + 1)),An*>,and2} is non empty functional V36() V51() set
{<*(g . (o0 + 1)),An*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (o0 + 1)),An*>,and2},{<*(g . (o0 + 1)),An*>}} is non empty V36() V40() V51() set
[<*(f . (o0 + 1)),An*>,and2a] is non empty pair set
{<*(f . (o0 + 1)),An*>,and2a} is non empty functional V36() V51() set
{<*(f . (o0 + 1)),An*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (o0 + 1)),An*>,and2a},{<*(f . (o0 + 1)),An*>}} is non empty V36() V40() V51() set
<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a],[<*(g . (o0 + 1)),An*>,and2],[<*(f . (o0 + 1)),An*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a],[<*(g . (o0 + 1)),An*>,and2],[<*(f . (o0 + 1)),An*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) +* (1GateCircStr (<*[<*(f . (o0 + 1)),(g . (o0 + 1))*>,and2a],[<*(g . (o0 + 1)),An*>,and2],[<*(f . (o0 + 1)),An*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (o0 + 1)),(g . (o0 + 1)),An,'xor')) +* (BorrowStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn +* (BitSubtracterWithBorrowStr ((f . (o0 + 1)),(g . (o0 + 1)),An)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f1 is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
h1 is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
h1 + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (h1 + 1) is set
g . (h1 + 1) is set
g1 is set
BitSubtracterWithBorrowStr ((f . (h1 + 1)),(g . (h1 + 1)),g1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (h1 + 1)),(g . (h1 + 1)),g1,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (h1 + 1)),(g . (h1 + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'] is non empty pair set
{<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (h1 + 1)),(g . (h1 + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'},{<*(f . (h1 + 1)),(g . (h1 + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'],g1*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'],g1*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,'xor'],g1*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (h1 + 1)),(g . (h1 + 1)),g1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (h1 + 1)),(g . (h1 + 1)),g1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (h1 + 1)),g1*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (h1 + 1)),g1*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (h1 + 1)),g1*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (h1 + 1)),g1*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (h1 + 1)),g1*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (h1 + 1)),g1*>,and2))) +* (1GateCircStr (<*(f . (h1 + 1)),g1*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a] is non empty pair set
{<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a},{<*(f . (h1 + 1)),(g . (h1 + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (h1 + 1)),g1*>,and2] is non empty pair set
{<*(g . (h1 + 1)),g1*>,and2} is non empty functional V36() V51() set
{<*(g . (h1 + 1)),g1*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (h1 + 1)),g1*>,and2},{<*(g . (h1 + 1)),g1*>}} is non empty V36() V40() V51() set
[<*(f . (h1 + 1)),g1*>,and2a] is non empty pair set
{<*(f . (h1 + 1)),g1*>,and2a} is non empty functional V36() V51() set
{<*(f . (h1 + 1)),g1*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (h1 + 1)),g1*>,and2a},{<*(f . (h1 + 1)),g1*>}} is non empty V36() V40() V51() set
<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a],[<*(g . (h1 + 1)),g1*>,and2],[<*(f . (h1 + 1)),g1*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a],[<*(g . (h1 + 1)),g1*>,and2],[<*(f . (h1 + 1)),g1*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (h1 + 1)),(g . (h1 + 1)),g1)) +* (1GateCircStr (<*[<*(f . (h1 + 1)),(g . (h1 + 1))*>,and2a],[<*(g . (h1 + 1)),g1*>,and2],[<*(f . (h1 + 1)),g1*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (h1 + 1)),(g . (h1 + 1)),g1,'xor')) +* (BorrowStr ((f . (h1 + 1)),(g . (h1 + 1)),g1)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f1 +* (BitSubtracterWithBorrowStr ((f . (h1 + 1)),(g . (h1 + 1)),g1)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
xx is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
xx + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (xx + 1) is set
g . (xx + 1) is set
x is set
BitSubtracterWithBorrowStr ((f . (xx + 1)),(g . (xx + 1)),x) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (xx + 1)),(g . (xx + 1)),x,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (xx + 1)),(g . (xx + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (xx + 1)),(g . (xx + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'] is non empty pair set
{<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (xx + 1)),(g . (xx + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'},{<*(f . (xx + 1)),(g . (xx + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'],x*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'],x*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (xx + 1)),(g . (xx + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (xx + 1)),(g . (xx + 1))*>,'xor'],x*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (xx + 1)),(g . (xx + 1)),x) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (xx + 1)),(g . (xx + 1)),x) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (xx + 1)),(g . (xx + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (xx + 1)),x*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (xx + 1)),x*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (xx + 1)),(g . (xx + 1))*>,and2a)) +* (1GateCircStr (<*(g . (xx + 1)),x*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (xx + 1)),x*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (xx + 1)),x*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (xx + 1)),(g . (xx + 1))*>,and2a)) +* (1GateCircStr (<*(g . (xx + 1)),x*>,and2))) +* (1GateCircStr (<*(f . (xx + 1)),x*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (xx + 1)),(g . (xx + 1))*>,and2a] is non empty pair set
{<*(f . (xx + 1)),(g . (xx + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (xx + 1)),(g . (xx + 1))*>,and2a},{<*(f . (xx + 1)),(g . (xx + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (xx + 1)),x*>,and2] is non empty pair set
{<*(g . (xx + 1)),x*>,and2} is non empty functional V36() V51() set
{<*(g . (xx + 1)),x*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (xx + 1)),x*>,and2},{<*(g . (xx + 1)),x*>}} is non empty V36() V40() V51() set
[<*(f . (xx + 1)),x*>,and2a] is non empty pair set
{<*(f . (xx + 1)),x*>,and2a} is non empty functional V36() V51() set
{<*(f . (xx + 1)),x*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (xx + 1)),x*>,and2a},{<*(f . (xx + 1)),x*>}} is non empty V36() V40() V51() set
<*[<*(f . (xx + 1)),(g . (xx + 1))*>,and2a],[<*(g . (xx + 1)),x*>,and2],[<*(f . (xx + 1)),x*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (xx + 1)),(g . (xx + 1))*>,and2a],[<*(g . (xx + 1)),x*>,and2],[<*(f . (xx + 1)),x*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (xx + 1)),(g . (xx + 1)),x)) +* (1GateCircStr (<*[<*(f . (xx + 1)),(g . (xx + 1))*>,and2a],[<*(g . (xx + 1)),x*>,and2],[<*(f . (xx + 1)),x*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (xx + 1)),(g . (xx + 1)),x,'xor')) +* (BorrowStr ((f . (xx + 1)),(g . (xx + 1)),x)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n +* (BitSubtracterWithBorrowStr ((f . (xx + 1)),(g . (xx + 1)),x)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
xy is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c₁₉ is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
c₁₉ + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (c₁₉ + 1) is set
g . (c₁₉ + 1) is set
c₁₈ is set
BitSubtracterWithBorrowStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor'] is non empty pair set
{<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor'},{<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor'],c₁₈*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor'],c₁₈*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,'xor'],c₁₈*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (c₁₉ + 1)),c₁₈*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (c₁₉ + 1)),c₁₈*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c₁₉ + 1)),c₁₈*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c₁₉ + 1)),c₁₈*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c₁₉ + 1)),c₁₈*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c₁₉ + 1)),c₁₈*>,and2))) +* (1GateCircStr (<*(f . (c₁₉ + 1)),c₁₈*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a] is non empty pair set
{<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a},{<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (c₁₉ + 1)),c₁₈*>,and2] is non empty pair set
{<*(g . (c₁₉ + 1)),c₁₈*>,and2} is non empty functional V36() V51() set
{<*(g . (c₁₉ + 1)),c₁₈*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (c₁₉ + 1)),c₁₈*>,and2},{<*(g . (c₁₉ + 1)),c₁₈*>}} is non empty V36() V40() V51() set
[<*(f . (c₁₉ + 1)),c₁₈*>,and2a] is non empty pair set
{<*(f . (c₁₉ + 1)),c₁₈*>,and2a} is non empty functional V36() V51() set
{<*(f . (c₁₉ + 1)),c₁₈*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c₁₉ + 1)),c₁₈*>,and2a},{<*(f . (c₁₉ + 1)),c₁₈*>}} is non empty V36() V40() V51() set
<*[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a],[<*(g . (c₁₉ + 1)),c₁₈*>,and2],[<*(f . (c₁₉ + 1)),c₁₈*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a],[<*(g . (c₁₉ + 1)),c₁₈*>,and2],[<*(f . (c₁₉ + 1)),c₁₈*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈)) +* (1GateCircStr (<*[<*(f . (c₁₉ + 1)),(g . (c₁₉ + 1))*>,and2a],[<*(g . (c₁₉ + 1)),c₁₈*>,and2],[<*(f . (c₁₉ + 1)),c₁₈*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈,'xor')) +* (BorrowStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
xy +* (BitSubtracterWithBorrowStr ((f . (c₁₉ + 1)),(g . (c₁₉ + 1)),c₁₈)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c₂₀ is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c₂₂ is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
c₂₂ + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (c₂₂ + 1) is set
g . (c₂₂ + 1) is set
c₂₁ is set
BitSubtracterWithBorrowStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor'] is non empty pair set
{<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor'},{<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor'],c₂₁*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor'],c₂₁*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,'xor'],c₂₁*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (c₂₂ + 1)),c₂₁*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (c₂₂ + 1)),c₂₁*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c₂₂ + 1)),c₂₁*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c₂₂ + 1)),c₂₁*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c₂₂ + 1)),c₂₁*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c₂₂ + 1)),c₂₁*>,and2))) +* (1GateCircStr (<*(f . (c₂₂ + 1)),c₂₁*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a] is non empty pair set
{<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a},{<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (c₂₂ + 1)),c₂₁*>,and2] is non empty pair set
{<*(g . (c₂₂ + 1)),c₂₁*>,and2} is non empty functional V36() V51() set
{<*(g . (c₂₂ + 1)),c₂₁*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (c₂₂ + 1)),c₂₁*>,and2},{<*(g . (c₂₂ + 1)),c₂₁*>}} is non empty V36() V40() V51() set
[<*(f . (c₂₂ + 1)),c₂₁*>,and2a] is non empty pair set
{<*(f . (c₂₂ + 1)),c₂₁*>,and2a} is non empty functional V36() V51() set
{<*(f . (c₂₂ + 1)),c₂₁*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c₂₂ + 1)),c₂₁*>,and2a},{<*(f . (c₂₂ + 1)),c₂₁*>}} is non empty V36() V40() V51() set
<*[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a],[<*(g . (c₂₂ + 1)),c₂₁*>,and2],[<*(f . (c₂₂ + 1)),c₂₁*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a],[<*(g . (c₂₂ + 1)),c₂₁*>,and2],[<*(f . (c₂₂ + 1)),c₂₁*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁)) +* (1GateCircStr (<*[<*(f . (c₂₂ + 1)),(g . (c₂₂ + 1))*>,and2a],[<*(g . (c₂₂ + 1)),c₂₁*>,and2],[<*(f . (c₂₂ + 1)),c₂₁*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁,'xor')) +* (BorrowStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c₂₀ +* (BitSubtracterWithBorrowStr ((f . (c₂₂ + 1)),(g . (c₂₂ + 1)),c₂₁)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
Sn is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
An is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
g1 is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
g1 + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (g1 + 1) is set
g . (g1 + 1) is set
f1 is set
BitSubtracterWithBorrowStr ((f . (g1 + 1)),(g . (g1 + 1)),f1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (g1 + 1)),(g . (g1 + 1)),f1,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (g1 + 1)),(g . (g1 + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor'] is non empty pair set
{<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (g1 + 1)),(g . (g1 + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor'},{<*(f . (g1 + 1)),(g . (g1 + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor'],f1*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor'],f1*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (g1 + 1)),(g . (g1 + 1))*>,'xor'],f1*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (g1 + 1)),(g . (g1 + 1)),f1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (g1 + 1)),(g . (g1 + 1)),f1) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (g1 + 1)),f1*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (g1 + 1)),f1*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (g1 + 1)),f1*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (g1 + 1)),f1*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (g1 + 1)),f1*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (g1 + 1)),f1*>,and2))) +* (1GateCircStr (<*(f . (g1 + 1)),f1*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2a] is non empty pair set
{<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (g1 + 1)),(g . (g1 + 1))*>,and2a},{<*(f . (g1 + 1)),(g . (g1 + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (g1 + 1)),f1*>,and2] is non empty pair set
{<*(g . (g1 + 1)),f1*>,and2} is non empty functional V36() V51() set
{<*(g . (g1 + 1)),f1*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (g1 + 1)),f1*>,and2},{<*(g . (g1 + 1)),f1*>}} is non empty V36() V40() V51() set
[<*(f . (g1 + 1)),f1*>,and2a] is non empty pair set
{<*(f . (g1 + 1)),f1*>,and2a} is non empty functional V36() V51() set
{<*(f . (g1 + 1)),f1*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (g1 + 1)),f1*>,and2a},{<*(f . (g1 + 1)),f1*>}} is non empty V36() V40() V51() set
<*[<*(f . (g1 + 1)),(