:: 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

RAT is set
INT is set

K18(K19(COMPLEX,COMPLEX)) is set

K18(K19(K19(COMPLEX,COMPLEX),COMPLEX)) is set

K18(K19(REAL,REAL)) is set
K19(K19(REAL,REAL),REAL) is Relation-like set
K18(K19(K19(REAL,REAL),REAL)) is set

K18(K19(RAT,RAT)) is set
K19(K19(RAT,RAT),RAT) is Relation-like set
K18(K19(K19(RAT,RAT),RAT)) is 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

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

K19((),BOOLEAN) is Relation-like set
K18(K19((),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

K19((),BOOLEAN) is Relation-like set
K18(K19((),BOOLEAN)) is set

Seg 1 is non empty V2() V36() 1 -element V51() Element of K18(NAT)

K18(K19(NAT,NAT)) is V2() V36() set

K18(K19(,BOOLEAN)) is set

n is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
[{},()] is non empty pair set
{{},()} is non empty functional V36() V51() set
is non empty V2() functional V36() V40() 1 -element V49() V51() non with_pair set
{{{},()},} is non empty V36() V40() V51() set

N . n is set
N . 0 is set

h . 0 is set

Sn . n is set
Sn . 0 is set

An . 0 is set

A0 . n is set
A0 . 0 is set

N . 0 is set
n is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set

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

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

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

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

c19 is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
c19 + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (c19 + 1) is set
g . (c19 + 1) is set
c18 is set
BitSubtracterWithBorrowStr ((f . (c19 + 1)),(g . (c19 + 1)),c18) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (c19 + 1)),(g . (c19 + 1)),c18,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c19 + 1)),(g . (c19 + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor'] is non empty pair set
{<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (c19 + 1)),(g . (c19 + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor'},{<*(f . (c19 + 1)),(g . (c19 + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor'],c18*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor'],c18*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (c19 + 1)),(g . (c19 + 1))*>,'xor'],c18*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (c19 + 1)),(g . (c19 + 1)),c18) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (c19 + 1)),(g . (c19 + 1)),c18) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (c19 + 1)),c18*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (c19 + 1)),c18*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c19 + 1)),c18*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c19 + 1)),c18*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c19 + 1)),c18*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c19 + 1)),c18*>,and2))) +* (1GateCircStr (<*(f . (c19 + 1)),c18*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a] is non empty pair set
{<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a},{<*(f . (c19 + 1)),(g . (c19 + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (c19 + 1)),c18*>,and2] is non empty pair set
{<*(g . (c19 + 1)),c18*>,and2} is non empty functional V36() V51() set
{<*(g . (c19 + 1)),c18*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (c19 + 1)),c18*>,and2},{<*(g . (c19 + 1)),c18*>}} is non empty V36() V40() V51() set
[<*(f . (c19 + 1)),c18*>,and2a] is non empty pair set
{<*(f . (c19 + 1)),c18*>,and2a} is non empty functional V36() V51() set
{<*(f . (c19 + 1)),c18*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c19 + 1)),c18*>,and2a},{<*(f . (c19 + 1)),c18*>}} is non empty V36() V40() V51() set
<*[<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a],[<*(g . (c19 + 1)),c18*>,and2],[<*(f . (c19 + 1)),c18*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a],[<*(g . (c19 + 1)),c18*>,and2],[<*(f . (c19 + 1)),c18*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (c19 + 1)),(g . (c19 + 1)),c18)) +* (1GateCircStr (<*[<*(f . (c19 + 1)),(g . (c19 + 1))*>,and2a],[<*(g . (c19 + 1)),c18*>,and2],[<*(f . (c19 + 1)),c18*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (c19 + 1)),(g . (c19 + 1)),c18,'xor')) +* (BorrowStr ((f . (c19 + 1)),(g . (c19 + 1)),c18)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
xy +* (BitSubtracterWithBorrowStr ((f . (c19 + 1)),(g . (c19 + 1)),c18)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

c22 is V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real non negative set
c22 + 1 is non empty V9() V10() V11() V15() non pair V30() V31() V36() cardinal V51() ext-real positive non negative Element of NAT
f . (c22 + 1) is set
g . (c22 + 1) is set
c21 is set
BitSubtracterWithBorrowStr ((f . (c22 + 1)),(g . (c22 + 1)),c21) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr ((f . (c22 + 1)),(g . (c22 + 1)),c21,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c22 + 1)),(g . (c22 + 1))*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor'] is non empty pair set
{<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor'} is non empty functional V36() V51() set
{<*(f . (c22 + 1)),(g . (c22 + 1))*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor'},{<*(f . (c22 + 1)),(g . (c22 + 1))*>}} is non empty V36() V40() V51() set
<*[<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor'],c21*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor'],c21*>,'xor') is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor')) +* (1GateCircStr (<*[<*(f . (c22 + 1)),(g . (c22 + 1))*>,'xor'],c21*>,'xor')) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowStr ((f . (c22 + 1)),(g . (c22 + 1)),c21) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
BorrowIStr ((f . (c22 + 1)),(g . (c22 + 1)),c21) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(g . (c22 + 1)),c21*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(g . (c22 + 1)),c21*>,and2) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c22 + 1)),c21*>,and2)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*(f . (c22 + 1)),c21*> is non empty Relation-like NAT -defined Function-like V36() 2 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*(f . (c22 + 1)),c21*>,and2a) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a)) +* (1GateCircStr (<*(g . (c22 + 1)),c21*>,and2))) +* (1GateCircStr (<*(f . (c22 + 1)),c21*>,and2a)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a] is non empty pair set
{<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a} is non empty functional V36() V51() set
{{<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a},{<*(f . (c22 + 1)),(g . (c22 + 1))*>}} is non empty V36() V40() V51() set
[<*(g . (c22 + 1)),c21*>,and2] is non empty pair set
{<*(g . (c22 + 1)),c21*>,and2} is non empty functional V36() V51() set
{<*(g . (c22 + 1)),c21*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(g . (c22 + 1)),c21*>,and2},{<*(g . (c22 + 1)),c21*>}} is non empty V36() V40() V51() set
[<*(f . (c22 + 1)),c21*>,and2a] is non empty pair set
{<*(f . (c22 + 1)),c21*>,and2a} is non empty functional V36() V51() set
{<*(f . (c22 + 1)),c21*>} is non empty V2() functional V36() V40() 1 -element V49() V51() set
{{<*(f . (c22 + 1)),c21*>,and2a},{<*(f . (c22 + 1)),c21*>}} is non empty V36() V40() V51() set
<*[<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a],[<*(g . (c22 + 1)),c21*>,and2],[<*(f . (c22 + 1)),c21*>,and2a]*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like V51() set
1GateCircStr (<*[<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a],[<*(g . (c22 + 1)),c21*>,and2],[<*(f . (c22 + 1)),c21*>,and2a]*>,or3) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(BorrowIStr ((f . (c22 + 1)),(g . (c22 + 1)),c21)) +* (1GateCircStr (<*[<*(f . (c22 + 1)),(g . (c22 + 1))*>,and2a],[<*(g . (c22 + 1)),c21*>,and2],[<*(f . (c22 + 1)),c21*>,and2a]*>,or3)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr ((f . (c22 + 1)),(g . (c22 + 1)),c21,'xor')) +* (BorrowStr ((f . (c22 + 1)),(g . (c22 + 1)),c21)) is non empty non void V71() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c20 +* (BitSubtracterWithBorrowStr ((f . (c22 + 1)),(g . (c22 + 1)),c21)) 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)),(