:: FSCIRC_1 semantic presentation

K96() is set
K100() is non empty V21() V22() V23() V34() V49() V50() Element of K27(K96())
K27(K96()) is set
K97() is set
K98() is set
K99() is set
K28(K97(),K97()) is set
K27(K28(K97(),K97())) is set
K28(K28(K97(),K97()),K97()) is set
K27(K28(K28(K97(),K97()),K97())) is set
K28(K96(),K96()) is set
K27(K28(K96(),K96())) is set
K28(K28(K96(),K96()),K96()) is set
K27(K28(K28(K96(),K96()),K96())) is set
K28(K98(),K98()) is set
K27(K28(K98(),K98())) is set
K28(K28(K98(),K98()),K98()) is set
K27(K28(K28(K98(),K98()),K98())) is set
K28(K99(),K99()) is set
K27(K28(K99(),K99())) is set
K28(K28(K99(),K99()),K99()) is set
K27(K28(K28(K99(),K99()),K99())) is set
K28(K100(),K100()) is set
K28(K28(K100(),K100()),K100()) is set
K27(K28(K28(K100(),K100()),K100())) is set
K95() is non empty V21() V22() V23() V34() V49() V50() set
K27(K95()) is set
K27(K100()) is set
BOOLEAN is set
1 is non empty non pair V21() V22() V23() V27() Element of K100()
{} is set
{{},1} is set
K342() is set
K27(K342()) is set
K343() is Element of K27(K342())
K383() is non empty V93() L10()
the carrier of K383() is non empty set
K346( the carrier of K383()) is non empty M24( the carrier of K383())
K382(K383()) is Element of K27(K346( the carrier of K383()))
K27(K346( the carrier of K383())) is set
K28(K382(K383()),K100()) is set
K27(K28(K382(K383()),K100())) is set
K28(K100(),K382(K383())) is set
K27(K28(K100(),K382(K383()))) is set
2 is non empty non pair V21() V22() V23() V27() Element of K100()
K237(2,BOOLEAN) is M8( BOOLEAN )
K28(K237(2,BOOLEAN),BOOLEAN) is set
K27(K28(K237(2,BOOLEAN),BOOLEAN)) is set
3 is non empty non pair V21() V22() V23() V27() Element of K100()
K237(3,BOOLEAN) is M8( BOOLEAN )
K28(K237(3,BOOLEAN),BOOLEAN) is set
K27(K28(K237(3,BOOLEAN),BOOLEAN)) is set
'xor' is Relation-like K237(2,BOOLEAN) -defined BOOLEAN -valued Function-like V18(K237(2,BOOLEAN), BOOLEAN ) Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
or3 is Relation-like K237(3,BOOLEAN) -defined BOOLEAN -valued Function-like V18(K237(3,BOOLEAN), BOOLEAN ) Element of K27(K28(K237(3,BOOLEAN),BOOLEAN))
and2 is Relation-like K237(2,BOOLEAN) -defined BOOLEAN -valued Function-like V18(K237(2,BOOLEAN), BOOLEAN ) Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
and2a is Relation-like K237(2,BOOLEAN) -defined BOOLEAN -valued Function-like V18(K237(2,BOOLEAN), BOOLEAN ) Element of K27(K28(K237(2,BOOLEAN),BOOLEAN))
x is set
y is set
c is set
2GatesCircOutput (x,y,c,'xor') is non empty pair Element of InnerVertices (2GatesCircStr (x,y,c,'xor'))
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
the carrier of (2GatesCircStr (x,y,c,'xor')) is non empty set
InnerVertices (2GatesCircStr (x,y,c,'xor')) is non empty Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
K27( the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
the ResultSort of (2GatesCircStr (x,y,c,'xor')) is Relation-like the carrier' of (2GatesCircStr (x,y,c,'xor')) -defined the carrier of (2GatesCircStr (x,y,c,'xor')) -valued Function-like V18( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) Element of K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))))
the carrier' of (2GatesCircStr (x,y,c,'xor')) is non empty set
K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor')))) is set
K532( the carrier of (2GatesCircStr (x,y,c,'xor')), the ResultSort of (2GatesCircStr (x,y,c,'xor'))) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
[<*[<*x,y*>,'xor'],c*>,'xor'] is non empty pair set
x is set
y is set
c is set
2GatesCircuit (x,y,c,'xor') is strict non-empty finitely-generated V105( 2GatesCircStr (x,y,c,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr (x,y,c,'xor')
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircuit (x,y,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,'xor')
1GateCircuit (<*x,y*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,'xor')
1GateCircuit ([<*x,y*>,'xor'],c,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')
1GateCircuit (<*[<*x,y*>,'xor'],c*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')
(1GateCircuit (x,y,'xor')) +* (1GateCircuit ([<*x,y*>,'xor'],c,'xor')) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor'))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor'))
x is set
y is set
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c is set
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is set
y is set
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c is set
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (1GateCircStr (<*x,y*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
the carrier of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,y*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,y*>,and2a)) -defined the carrier of (1GateCircStr (<*x,y*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))))
the carrier' of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,y*>,and2a)), the ResultSort of (1GateCircStr (<*x,y*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
InnerVertices (1GateCircStr (<*y,c*>,and2)) is non empty Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
the carrier of (1GateCircStr (<*y,c*>,and2)) is non empty set
K27( the carrier of (1GateCircStr (<*y,c*>,and2))) is set
the ResultSort of (1GateCircStr (<*y,c*>,and2)) is Relation-like the carrier' of (1GateCircStr (<*y,c*>,and2)) -defined the carrier of (1GateCircStr (<*y,c*>,and2)) -valued Function-like V18( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) Element of K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))))
the carrier' of (1GateCircStr (<*y,c*>,and2)) is non empty set
K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) is set
K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2)))) is set
K532( the carrier of (1GateCircStr (<*y,c*>,and2)), the ResultSort of (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
InnerVertices (1GateCircStr (<*x,c*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
the carrier of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,c*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,c*>,and2a)) -defined the carrier of (1GateCircStr (<*x,c*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))))
the carrier' of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,c*>,and2a)), the ResultSort of (1GateCircStr (<*x,c*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Relation-like the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -defined the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -valued Function-like V18( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) Element of K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))))
the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) is set
K532( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation-like the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -defined the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -valued Function-like V18( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) Element of K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))))
the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) is set
K532( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
A is non empty pair set
InnerVertices (1GateCircStr (<*x,c*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
the carrier of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,c*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,c*>,and2a)) -defined the carrier of (1GateCircStr (<*x,c*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))))
the carrier' of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,c*>,and2a)), the ResultSort of (1GateCircStr (<*x,c*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
{[<*x,c*>,and2a]} is Relation-like Function-like set
InnerVertices (1GateCircStr (<*x,y*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
the carrier of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,y*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,y*>,and2a)) -defined the carrier of (1GateCircStr (<*x,y*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))))
the carrier' of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,y*>,and2a)), the ResultSort of (1GateCircStr (<*x,y*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
{[<*x,y*>,and2a]} is Relation-like Function-like set
InnerVertices (1GateCircStr (<*y,c*>,and2)) is non empty Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
the carrier of (1GateCircStr (<*y,c*>,and2)) is non empty set
K27( the carrier of (1GateCircStr (<*y,c*>,and2))) is set
the ResultSort of (1GateCircStr (<*y,c*>,and2)) is Relation-like the carrier' of (1GateCircStr (<*y,c*>,and2)) -defined the carrier of (1GateCircStr (<*y,c*>,and2)) -valued Function-like V18( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) Element of K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))))
the carrier' of (1GateCircStr (<*y,c*>,and2)) is non empty set
K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) is set
K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2)))) is set
K532( the carrier of (1GateCircStr (<*y,c*>,and2)), the ResultSort of (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
{[<*y,c*>,and2]} is Relation-like Function-like set
InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Relation-like the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -defined the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -valued Function-like V18( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) Element of K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))))
the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) is set
K532( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
{[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} is set
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} is set
{[<*x,y*>,and2a],[<*y,c*>,and2]} is Relation-like set
{[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} is set
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} is Relation-like set
InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation-like the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -defined the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -valued Function-like V18( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) Element of K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))))
the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) is set
K532( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) \ K532( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
(InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (x,y,c)) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
InputVertices (1GateCircStr (<*x,y*>,and2a)) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
the carrier of (1GateCircStr (<*x,y*>,and2a)) \ K532( the carrier of (1GateCircStr (<*x,y*>,and2a)), the ResultSort of (1GateCircStr (<*x,y*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
InputVertices (1GateCircStr (<*y,c*>,and2)) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
the carrier of (1GateCircStr (<*y,c*>,and2)) \ K532( the carrier of (1GateCircStr (<*y,c*>,and2)), the ResultSort of (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
InputVertices (1GateCircStr (<*x,c*>,and2a)) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
the carrier of (1GateCircStr (<*x,c*>,and2a)) \ K532( the carrier of (1GateCircStr (<*x,c*>,and2a)), the ResultSort of (1GateCircStr (<*x,c*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) \ K532( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
(InputVertices (x,y,c)) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (x,y,c))) is set
x is set
y is set
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
[<*x,y*>,and2a] is non empty pair set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
s2 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
s2 . x is set
s2 . y is set
Following s2 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following s2) . [<*x,y*>,and2a] is set
a3 is Element of BOOLEAN
xx is Element of BOOLEAN
'not' a3 is Element of BOOLEAN
('not' a3) '&' xx is Element of BOOLEAN
the carrier of (1GateCircStr (<*x,y*>,and2a)) is non empty set
InnerVertices (1GateCircStr (<*x,y*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
K27( the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,y*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,y*>,and2a)) -defined the carrier of (1GateCircStr (<*x,y*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))))
the carrier' of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,y*>,and2a)), the ResultSort of (1GateCircStr (<*x,y*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
(1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* ((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a))) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
v2 is Element of InnerVertices (1GateCircStr (<*x,y*>,and2a))
(1GateCircuit (y,c,and2)) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a))
(1GateCircuit (x,y,and2a)) +* ((1GateCircuit (y,c,and2)) +* (1GateCircuit (x,c,and2a))) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* ((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a)))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* ((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a)))
the Sorts of (1GateCircuit (x,y,and2a)) is Relation-like the carrier of (1GateCircStr (<*x,y*>,and2a)) -defined Function-like V14( the carrier of (1GateCircStr (<*x,y*>,and2a))) set
K224( the Sorts of (1GateCircuit (x,y,and2a))) is functional V47() V48() set
s2 | the carrier of (1GateCircStr (<*x,y*>,and2a)) is Relation-like Function-like set
cc is Element of the carrier of (1GateCircStr (<*x,y*>,and2a))
cc is Element of the carrier of (1GateCircStr (<*x,y*>,and2a))
s2 is Relation-like Function-like Element of K224( the Sorts of (1GateCircuit (x,y,and2a)))
proj1 s2 is set
Following s2 is Relation-like Function-like Element of K224( the Sorts of (1GateCircuit (x,y,and2a)))
v is Element of InnerVertices (x,y,c)
(Following s2) . v is set
yy is Element of the carrier of (x,y,c)
s2 . yy is set
cc is Element of the carrier of (x,y,c)
s2 . cc is set
<*(s2 . yy),(s2 . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*(s2 . yy),(s2 . cc)*> is set
s2 . yy is Element of BOOLEAN
<*(s2 . yy),(s2 . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*(s2 . yy),(s2 . cc)*> is set
s2 . cc is Element of BOOLEAN
<*(s2 . yy),(s2 . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*(s2 . yy),(s2 . cc)*> is set
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
[<*y,c*>,and2] is non empty pair set
s2 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
s2 . y is set
s2 . c is set
Following s2 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following s2) . [<*y,c*>,and2] is set
a3 is Element of BOOLEAN
xx is Element of BOOLEAN
a3 '&' xx is Element of BOOLEAN
the carrier of (1GateCircStr (<*y,c*>,and2)) is non empty set
InnerVertices (1GateCircStr (<*y,c*>,and2)) is non empty Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
K27( the carrier of (1GateCircStr (<*y,c*>,and2))) is set
the ResultSort of (1GateCircStr (<*y,c*>,and2)) is Relation-like the carrier' of (1GateCircStr (<*y,c*>,and2)) -defined the carrier of (1GateCircStr (<*y,c*>,and2)) -valued Function-like V18( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) Element of K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))))
the carrier' of (1GateCircStr (<*y,c*>,and2)) is non empty set
K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) is set
K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2)))) is set
K532( the carrier of (1GateCircStr (<*y,c*>,and2)), the ResultSort of (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
(1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,y*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*y,c*>,and2)) +* ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a))) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
v2 is Element of InnerVertices (1GateCircStr (<*y,c*>,and2))
(1GateCircuit (y,c,and2)) +* (1GateCircuit (x,y,and2a)) is strict non-empty finitely-generated V105((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,y*>,and2a))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,y*>,and2a))
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a))
(1GateCircuit (y,c,and2)) +* ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (x,c,and2a))) is strict non-empty finitely-generated V105((1GateCircStr (<*y,c*>,and2)) +* ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a)))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*y,c*>,and2)) +* ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a)))
the Sorts of (1GateCircuit (y,c,and2)) is Relation-like the carrier of (1GateCircStr (<*y,c*>,and2)) -defined Function-like V14( the carrier of (1GateCircStr (<*y,c*>,and2))) set
K224( the Sorts of (1GateCircuit (y,c,and2))) is functional V47() V48() set
s2 | the carrier of (1GateCircStr (<*y,c*>,and2)) is Relation-like Function-like set
cc is Element of the carrier of (1GateCircStr (<*y,c*>,and2))
cc is Element of the carrier of (1GateCircStr (<*y,c*>,and2))
s2 is Relation-like Function-like Element of K224( the Sorts of (1GateCircuit (y,c,and2)))
proj1 s2 is set
Following s2 is Relation-like Function-like Element of K224( the Sorts of (1GateCircuit (y,c,and2)))
v is Element of InnerVertices (x,y,c)
(Following s2) . v is set
yy is Element of the carrier of (x,y,c)
s2 . yy is set
cc is Element of the carrier of (x,y,c)
s2 . cc is set
<*(s2 . yy),(s2 . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2 . <*(s2 . yy),(s2 . cc)*> is set
s2 . yy is Element of BOOLEAN
<*(s2 . yy),(s2 . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2 . <*(s2 . yy),(s2 . cc)*> is set
s2 . cc is Element of BOOLEAN
<*(s2 . yy),(s2 . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2 . <*(s2 . yy),(s2 . cc)*> is set
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
[<*x,c*>,and2a] is non empty pair set
s is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
s . x is set
s . c is set
Following s is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following s) . [<*x,c*>,and2a] is set
s1 is Element of BOOLEAN
s2 is Element of BOOLEAN
'not' s1 is Element of BOOLEAN
('not' s1) '&' s2 is Element of BOOLEAN
the carrier of (1GateCircStr (<*x,c*>,and2a)) is non empty set
the Sorts of (1GateCircuit (x,c,and2a)) is Relation-like the carrier of (1GateCircStr (<*x,c*>,and2a)) -defined Function-like V14( the carrier of (1GateCircStr (<*x,c*>,and2a))) set
K224( the Sorts of (1GateCircuit (x,c,and2a))) is functional V47() V48() set
s | the carrier of (1GateCircStr (<*x,c*>,and2a)) is Relation-like Function-like set
InnerVertices (1GateCircStr (<*x,c*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
K27( the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,c*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,c*>,and2a)) -defined the carrier of (1GateCircStr (<*x,c*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))))
the carrier' of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,c*>,and2a)), the ResultSort of (1GateCircStr (<*x,c*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
s2 is Element of InnerVertices (1GateCircStr (<*x,c*>,and2a))
t is Relation-like Function-like Element of K224( the Sorts of (1GateCircuit (x,c,and2a)))
proj1 t is set
t is Element of the carrier of (1GateCircStr (<*x,c*>,and2a))
a is Element of the carrier of (1GateCircStr (<*x,c*>,and2a))
Following t is Relation-like Function-like Element of K224( the Sorts of (1GateCircuit (x,c,and2a)))
a3 is Element of InnerVertices (x,y,c)
(Following t) . a3 is set
xx is Element of the carrier of (x,y,c)
t . xx is set
cc is Element of the carrier of (x,y,c)
t . cc is set
<*(t . xx),(t . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*(t . xx),(t . cc)*> is set
s . xx is Element of BOOLEAN
<*(s . xx),(t . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*(s . xx),(t . cc)*> is set
s . cc is Element of BOOLEAN
<*(s . xx),(s . cc)*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*(s . xx),(s . cc)*> is set
x is set
y is set
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
[<*x,y*>,and2a] is non empty pair set
c is set
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
[<*y,c*>,and2] is non empty pair set
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is non empty pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
the carrier of (x,y,c) is non empty set
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation-like the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -defined the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -valued Function-like V18( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) Element of K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))))
the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) is set
K532( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
the carrier of (x,y,c) is non empty set
the carrier of (1GateCircStr (<*x,c*>,and2a)) is non empty set
the carrier of (x,y,c) is non empty set
the carrier of (1GateCircStr (<*x,y*>,and2a)) is non empty set
the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
x is set
y is set
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
[<*x,y*>,and2a] is non empty pair set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (1GateCircStr (<*x,y*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
the carrier of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,y*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,y*>,and2a)) -defined the carrier of (1GateCircStr (<*x,y*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))))
the carrier' of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,y*>,and2a)), the ResultSort of (1GateCircStr (<*x,y*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Relation-like the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -defined the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -valued Function-like V18( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) Element of K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))))
the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) is set
K532( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (1GateCircStr (<*y,c*>,and2)) is non empty Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
the carrier of (1GateCircStr (<*y,c*>,and2)) is non empty set
K27( the carrier of (1GateCircStr (<*y,c*>,and2))) is set
the ResultSort of (1GateCircStr (<*y,c*>,and2)) is Relation-like the carrier' of (1GateCircStr (<*y,c*>,and2)) -defined the carrier of (1GateCircStr (<*y,c*>,and2)) -valued Function-like V18( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) Element of K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))))
the carrier' of (1GateCircStr (<*y,c*>,and2)) is non empty set
K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) is set
K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2)))) is set
K532( the carrier of (1GateCircStr (<*y,c*>,and2)), the ResultSort of (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
InnerVertices (1GateCircStr (<*x,c*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
the carrier of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,c*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,c*>,and2a)) -defined the carrier of (1GateCircStr (<*x,c*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))))
the carrier' of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,c*>,and2a)), the ResultSort of (1GateCircStr (<*x,c*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
S is set
S1 is set
[S,S1] is non empty pair set
S2 is set
A is set
[S2,A] is non empty pair set
A1 is set
A2 is set
[A1,A2] is non empty pair set
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
{x,y,c} is non with_pair set
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} is Relation-like set
(x,y,c) is Element of InnerVertices (x,y,c)
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is non empty pair set
{(x,y,c)} is set
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(x,y,c)} is set
InputVertices (1GateCircStr (<*x,y*>,and2a)) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
the carrier of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,y*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,y*>,and2a)) -defined the carrier of (1GateCircStr (<*x,y*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))))
the carrier' of (1GateCircStr (<*x,y*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,y*>,and2a)), the carrier of (1GateCircStr (<*x,y*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,y*>,and2a)), the ResultSort of (1GateCircStr (<*x,y*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
the carrier of (1GateCircStr (<*x,y*>,and2a)) \ K532( the carrier of (1GateCircStr (<*x,y*>,and2a)), the ResultSort of (1GateCircStr (<*x,y*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
{x,y} is non with_pair set
InputVertices (1GateCircStr (<*x,c*>,and2a)) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
the carrier of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K27( the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
the ResultSort of (1GateCircStr (<*x,c*>,and2a)) is Relation-like the carrier' of (1GateCircStr (<*x,c*>,and2a)) -defined the carrier of (1GateCircStr (<*x,c*>,and2a)) -valued Function-like V18( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) Element of K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))))
the carrier' of (1GateCircStr (<*x,c*>,and2a)) is non empty set
K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a))) is set
K27(K28( the carrier' of (1GateCircStr (<*x,c*>,and2a)), the carrier of (1GateCircStr (<*x,c*>,and2a)))) is set
K532( the carrier of (1GateCircStr (<*x,c*>,and2a)), the ResultSort of (1GateCircStr (<*x,c*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
the carrier of (1GateCircStr (<*x,c*>,and2a)) \ K532( the carrier of (1GateCircStr (<*x,c*>,and2a)), the ResultSort of (1GateCircStr (<*x,c*>,and2a))) is Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
{x,c} is non with_pair set
InputVertices (1GateCircStr (<*y,c*>,and2)) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
the carrier of (1GateCircStr (<*y,c*>,and2)) is non empty set
K27( the carrier of (1GateCircStr (<*y,c*>,and2))) is set
the ResultSort of (1GateCircStr (<*y,c*>,and2)) is Relation-like the carrier' of (1GateCircStr (<*y,c*>,and2)) -defined the carrier of (1GateCircStr (<*y,c*>,and2)) -valued Function-like V18( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) Element of K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))))
the carrier' of (1GateCircStr (<*y,c*>,and2)) is non empty set
K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2))) is set
K27(K28( the carrier' of (1GateCircStr (<*y,c*>,and2)), the carrier of (1GateCircStr (<*y,c*>,and2)))) is set
K532( the carrier of (1GateCircStr (<*y,c*>,and2)), the ResultSort of (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
the carrier of (1GateCircStr (<*y,c*>,and2)) \ K532( the carrier of (1GateCircStr (<*y,c*>,and2)), the ResultSort of (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
{y,c} is non with_pair set
InnerVertices (1GateCircStr (<*x,y*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,y*>,and2a)))
{[<*x,y*>,and2a]} is Relation-like Function-like set
InnerVertices (1GateCircStr (<*y,c*>,and2)) is non empty Element of K27( the carrier of (1GateCircStr (<*y,c*>,and2)))
{[<*y,c*>,and2]} is Relation-like Function-like set
InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation-like the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -defined the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) -valued Function-like V18( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) Element of K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))))
the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty set
K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
K27(K28( the carrier' of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) is set
K532( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Relation-like the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -defined the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) -valued Function-like V18( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) Element of K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))))
the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty set
K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is set
K27(K28( the carrier' of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) is set
K532( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) \ K532( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))), the ResultSort of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) is Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) \ K532( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)), the ResultSort of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
(InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (x,y,c)) is Element of K27( the carrier of (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))
(InputVertices (x,y,c)) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (x,y,c))) is set
InnerVertices (1GateCircStr (<*x,c*>,and2a)) is non empty Element of K27( the carrier of (1GateCircStr (<*x,c*>,and2a)))
{[<*x,c*>,and2a]} is Relation-like Function-like set
InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is non empty Element of K27( the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))
{[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} is set
({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} is set
{[<*x,y*>,and2a],[<*y,c*>,and2]} is Relation-like set
{[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} is set
(InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) \/ (InputVertices (1GateCircStr (<*x,c*>,and2a))) is set
(InputVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InputVertices (1GateCircStr (<*y,c*>,and2))) is set
((InputVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InputVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InputVertices (1GateCircStr (<*x,c*>,and2a))) is set
{x,y,y,c} is set
{c,x} is non with_pair set
{x,y,y,c} \/ {c,x} is set
{y,y,x,c} is set
{y,y,x,c} \/ {c,x} is set
{y,x,c} is non with_pair set
{y,x,c} \/ {c,x} is non with_pair set
{x,y,c} \/ {c,x} is non with_pair set
{c} is non with_pair set
{x} is non with_pair set
{c} \/ {x} is non with_pair set
{x,y,c} \/ ({c} \/ {x}) is non with_pair set
{x,y,c} \/ {c} is non with_pair set
({x,y,c} \/ {c}) \/ {x} is non with_pair set
{c,x,y} is non with_pair set
{c,x,y} \/ {c} is non with_pair set
({c,x,y} \/ {c}) \/ {x} is non with_pair set
{c,c,x,y} is set
{c,c,x,y} \/ {x} is set
{c,x,y} \/ {x} is non with_pair set
{x,y,c} \/ {x} is non with_pair set
{x,x,y,c} is set
(InnerVertices (x,y,c)) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) is set
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S . x is set
S . y is set
S . c is set
Following S is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following S) . [<*x,y*>,and2a] is set
(Following S) . [<*y,c*>,and2] is set
(Following S) . [<*x,c*>,and2a] is set
S1 is Element of BOOLEAN
S2 is Element of BOOLEAN
A is Element of BOOLEAN
'not' S1 is Element of BOOLEAN
('not' S1) '&' S2 is Element of BOOLEAN
S2 '&' A is Element of BOOLEAN
('not' S1) '&' A is Element of BOOLEAN
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
proj1 S is set
<*x,y*> * S is Relation-like Function-like set
and2a . (<*x,y*> * S) is set
<*S1,S2*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*S1,S2*> is set
<*y,c*> * S is Relation-like Function-like set
and2 . (<*y,c*> * S) is set
<*S2,A*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2 . <*S2,A*> is set
<*x,c*> * S is Relation-like Function-like set
and2a . (<*x,c*> * S) is set
<*S1,A*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
and2a . <*S1,A*> is set
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S1 . x is set
S1 . y is set
Following S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following S1) . [<*x,y*>,and2a] is set
S is Element of the carrier of (x,y,c)
S1 . S is Element of BOOLEAN
S2 is Element of BOOLEAN
A is Element of BOOLEAN
'not' S2 is Element of BOOLEAN
('not' S2) '&' A is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S1 . y is set
S1 . c is set
Following S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following S1) . [<*y,c*>,and2] is set
S is Element of the carrier of (x,y,c)
S1 . S is Element of BOOLEAN
S2 is Element of BOOLEAN
A is Element of BOOLEAN
S2 '&' A is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S1 . x is set
S1 . c is set
Following S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following S1) . [<*x,c*>,and2a] is set
S is Element of the carrier of (x,y,c)
S1 . S is Element of BOOLEAN
S2 is Element of BOOLEAN
A is Element of BOOLEAN
'not' S2 is Element of BOOLEAN
('not' S2) '&' A is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
(x,y,c) is Element of InnerVertices (x,y,c)
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is non empty pair set
a is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
a . [<*x,y*>,and2a] is set
a . [<*y,c*>,and2] is set
a . [<*x,c*>,and2a] is set
Following a is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following a) . (x,y,c) is Element of BOOLEAN
t is Element of BOOLEAN
s2 is Element of BOOLEAN
a3 is Element of BOOLEAN
t 'or' s2 is Element of BOOLEAN
(t 'or' s2) 'or' a3 is Element of BOOLEAN
proj1 a is set
s1 is Element of InnerVertices (x,y,c)
s2 is Element of InnerVertices (x,y,c)
t is Element of InnerVertices (x,y,c)
<*s1,s2,t*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
<*s1,s2,t*> * a is Relation-like Function-like set
or3 . (<*s1,s2,t*> * a) is set
<*t,s2,a3*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
or3 . <*t,s2,a3*> is set
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
(x,y,c) is Element of InnerVertices (x,y,c)
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is non empty pair set
A1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
A1 . x is set
A1 . y is set
A1 . c is set
Following (A1,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following (A1,2)) . (x,y,c) is Element of BOOLEAN
(Following (A1,2)) . [<*x,y*>,and2a] is set
(Following (A1,2)) . [<*y,c*>,and2] is set
(Following (A1,2)) . [<*x,c*>,and2a] is set
Following A1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (Following A1) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
t is Element of BOOLEAN
s2 is Element of BOOLEAN
a3 is Element of BOOLEAN
'not' t is Element of BOOLEAN
('not' t) '&' s2 is Element of BOOLEAN
s2 '&' a3 is Element of BOOLEAN
(('not' t) '&' s2) 'or' (s2 '&' a3) is Element of BOOLEAN
('not' t) '&' a3 is Element of BOOLEAN
((('not' t) '&' s2) 'or' (s2 '&' a3)) 'or' (('not' t) '&' a3) is Element of BOOLEAN
(Following A1) . [<*x,c*>,and2a] is set
(Following A1) . [<*x,y*>,and2a] is set
(Following A1) . [<*y,c*>,and2] is set
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
S2 is Element of the carrier of (x,y,c)
(Following A1) . S2 is Element of BOOLEAN
A is Element of the carrier of (x,y,c)
(Following A1) . A is Element of BOOLEAN
S1 is Element of the carrier of (x,y,c)
(Following A1) . S1 is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S1 . x is set
S1 . y is set
Following (S1,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following (S1,2)) . [<*x,y*>,and2a] is set
S is Element of the carrier of (x,y,c)
S1 . S is Element of BOOLEAN
S2 is Element of BOOLEAN
A is Element of BOOLEAN
'not' S2 is Element of BOOLEAN
('not' S2) '&' A is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S1 . y is set
S1 . c is set
Following (S1,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following (S1,2)) . [<*y,c*>,and2] is set
S is Element of the carrier of (x,y,c)
S1 . S is Element of BOOLEAN
S2 is Element of BOOLEAN
A is Element of BOOLEAN
S2 '&' A is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S1 . x is set
S1 . c is set
Following (S1,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following (S1,2)) . [<*x,c*>,and2a] is set
S is Element of the carrier of (x,y,c)
S1 . S is Element of BOOLEAN
S2 is Element of BOOLEAN
A is Element of BOOLEAN
'not' S2 is Element of BOOLEAN
('not' S2) '&' A is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
S1 is Element of BOOLEAN
S is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S . x is set
S2 is Element of BOOLEAN
S . y is set
A is Element of BOOLEAN
S . c is set
Following (S,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(x,y,c) is Element of InnerVertices (x,y,c)
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is non empty pair set
(Following (S,2)) . (x,y,c) is Element of BOOLEAN
'not' S1 is Element of BOOLEAN
('not' S1) '&' S2 is Element of BOOLEAN
S2 '&' A is Element of BOOLEAN
(('not' S1) '&' S2) 'or' (S2 '&' A) is Element of BOOLEAN
('not' S1) '&' A is Element of BOOLEAN
((('not' S1) '&' S2) 'or' (S2 '&' A)) 'or' (('not' S1) '&' A) is Element of BOOLEAN
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
A1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (A1,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
S1 is Element of the carrier of (x,y,c)
A1 . S1 is Element of BOOLEAN
S2 is Element of the carrier of (x,y,c)
A1 . S2 is Element of BOOLEAN
A is Element of the carrier of (x,y,c)
A1 . A is Element of BOOLEAN
Following (Following (A1,2)) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following A1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (Following A1) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
(Following A1) . y is set
(Following (A1,2)) . y is set
A1 . y is set
(Following (A1,2)) . [<*x,c*>,and2a] is set
'not' (A1 . S1) is Element of BOOLEAN
('not' (A1 . S1)) '&' (A1 . A) is Element of BOOLEAN
(Following A1) . x is set
(Following (A1,2)) . x is set
A1 . x is set
(Following (A1,2)) . [<*y,c*>,and2] is set
(A1 . S2) '&' (A1 . A) is Element of BOOLEAN
(Following A1) . c is set
(Following (A1,2)) . c is set
A1 . c is set
(Following (A1,2)) . [<*x,y*>,and2a] is set
('not' (A1 . S1)) '&' (A1 . S2) is Element of BOOLEAN
(x,y,c) is Element of InnerVertices (x,y,c)
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is non empty pair set
(Following (A1,2)) . (x,y,c) is Element of BOOLEAN
(('not' (A1 . S1)) '&' (A1 . S2)) 'or' ((A1 . S2) '&' (A1 . A)) is Element of BOOLEAN
((('not' (A1 . S1)) '&' (A1 . S2)) 'or' ((A1 . S2) '&' (A1 . A))) 'or' (('not' (A1 . S1)) '&' (A1 . A)) is Element of BOOLEAN
a is set
t is Element of the carrier of (x,y,c)
(InputVertices (x,y,c)) \/ (InnerVertices (x,y,c)) is Element of K27( the carrier of (x,y,c))
(Following (A1,2)) . a is set
(Following (Following (A1,2))) . a is set
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} is Relation-like set
{(x,y,c)} is set
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(x,y,c)} is set
proj1 (Following (Following (A1,2))) is set
proj1 (Following (A1,2)) is set
x is set
y is set
c is set
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
{x,y,c} is non with_pair set
InputVertices (2GatesCircStr (x,y,c,'xor')) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
the carrier of (2GatesCircStr (x,y,c,'xor')) is non empty set
K27( the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
the ResultSort of (2GatesCircStr (x,y,c,'xor')) is Relation-like the carrier' of (2GatesCircStr (x,y,c,'xor')) -defined the carrier of (2GatesCircStr (x,y,c,'xor')) -valued Function-like V18( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) Element of K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))))
the carrier' of (2GatesCircStr (x,y,c,'xor')) is non empty set
K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor')))) is set
K532( the carrier of (2GatesCircStr (x,y,c,'xor')), the ResultSort of (2GatesCircStr (x,y,c,'xor'))) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
the carrier of (2GatesCircStr (x,y,c,'xor')) \ K532( the carrier of (2GatesCircStr (x,y,c,'xor')), the ResultSort of (2GatesCircStr (x,y,c,'xor'))) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (2GatesCircStr (x,y,c,'xor')) is non empty Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
{x,y,c} \/ {x,y,c} is non with_pair set
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
2GatesCircOutput (x,y,c,'xor') is non empty pair Element of InnerVertices (2GatesCircStr (x,y,c,'xor'))
the carrier of (2GatesCircStr (x,y,c,'xor')) is non empty set
InnerVertices (2GatesCircStr (x,y,c,'xor')) is non empty Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
K27( the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
the ResultSort of (2GatesCircStr (x,y,c,'xor')) is Relation-like the carrier' of (2GatesCircStr (x,y,c,'xor')) -defined the carrier of (2GatesCircStr (x,y,c,'xor')) -valued Function-like V18( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) Element of K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))))
the carrier' of (2GatesCircStr (x,y,c,'xor')) is non empty set
K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor')))) is set
K532( the carrier of (2GatesCircStr (x,y,c,'xor')), the ResultSort of (2GatesCircStr (x,y,c,'xor'))) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
[<*[<*x,y*>,'xor'],c*>,'xor'] is non empty pair set
{[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} is Relation-like set
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} is Relation-like set
{[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} is set
(x,y,c) is Element of InnerVertices (x,y,c)
the carrier of (x,y,c) is non empty set
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is non empty pair set
{(x,y,c)} is set
({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(x,y,c)} is set
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(x,y,c)} is set
{[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(x,y,c)}) is set
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S1 is non empty V69() ManySortedSign
the carrier of S1 is non empty set
the carrier of (2GatesCircStr (x,y,c,'xor')) is non empty set
x is set
y is set
c is set
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105( 2GatesCircStr (x,y,c,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr (x,y,c,'xor')
2GatesCircuit (x,y,c,'xor') is strict non-empty finitely-generated V105( 2GatesCircStr (x,y,c,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr (x,y,c,'xor')
1GateCircuit (x,y,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,'xor')
1GateCircuit (<*x,y*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,'xor')
1GateCircuit ([<*x,y*>,'xor'],c,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')
1GateCircuit (<*[<*x,y*>,'xor'],c*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')
(1GateCircuit (x,y,'xor')) +* (1GateCircuit ([<*x,y*>,'xor'],c,'xor')) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor'))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor'))
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
(x,y,c) +* (x,y,c) is strict non-empty finitely-generated V105((2GatesCircStr (x,y,c,'xor')) +* (x,y,c)) gate`2=den Boolean MSAlgebra over (2GatesCircStr (x,y,c,'xor')) +* (x,y,c)
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is set
y is set
c is set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (2GatesCircStr (x,y,c,'xor')) is non empty Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
the carrier of (2GatesCircStr (x,y,c,'xor')) is non empty set
K27( the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
the ResultSort of (2GatesCircStr (x,y,c,'xor')) is Relation-like the carrier' of (2GatesCircStr (x,y,c,'xor')) -defined the carrier of (2GatesCircStr (x,y,c,'xor')) -valued Function-like V18( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) Element of K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))))
the carrier' of (2GatesCircStr (x,y,c,'xor')) is non empty set
K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor')))) is set
K532( the carrier of (2GatesCircStr (x,y,c,'xor')), the ResultSort of (2GatesCircStr (x,y,c,'xor'))) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) is non empty set
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
{x,y,c} is non with_pair set
y is non pair set
c is non pair set
S is non pair set
(y,c,S) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (y,c,S,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*y,c*>,'xor'] is non empty pair set
<*[<*y,c*>,'xor'],S*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*y,c*>,'xor'],S*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*y,c*>,'xor')) +* (1GateCircStr (<*[<*y,c*>,'xor'],S*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(y,c,S) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(y,c,S) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*y,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*c,S*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*c,S*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*y,c*>,and2a)) +* (1GateCircStr (<*c,S*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,S*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,S*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*y,c*>,and2a)) +* (1GateCircStr (<*c,S*>,and2))) +* (1GateCircStr (<*y,S*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*y,c*>,and2a] is non empty pair set
[<*c,S*>,and2] is non empty pair set
[<*y,S*>,and2a] is non empty pair set
<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(y,c,S) +* (1GateCircStr (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (y,c,S,'xor')) +* (y,c,S) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(y,c,S) is strict non-empty finitely-generated V105((y,c,S)) gate`2=den Boolean MSAlgebra over (y,c,S)
(y,c,S) is strict non-empty finitely-generated V105( 2GatesCircStr (y,c,S,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr (y,c,S,'xor')
2GatesCircuit (y,c,S,'xor') is strict non-empty finitely-generated V105( 2GatesCircStr (y,c,S,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr (y,c,S,'xor')
1GateCircuit (y,c,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,'xor')
1GateCircuit (<*y,c*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,'xor')
1GateCircuit ([<*y,c*>,'xor'],S,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*y,c*>,'xor'],S*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*y,c*>,'xor'],S*>,'xor')
1GateCircuit (<*[<*y,c*>,'xor'],S*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*[<*y,c*>,'xor'],S*>,'xor')
(1GateCircuit (y,c,'xor')) +* (1GateCircuit ([<*y,c*>,'xor'],S,'xor')) is strict non-empty finitely-generated V105((1GateCircStr (<*y,c*>,'xor')) +* (1GateCircStr (<*[<*y,c*>,'xor'],S*>,'xor'))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*y,c*>,'xor')) +* (1GateCircStr (<*[<*y,c*>,'xor'],S*>,'xor'))
(y,c,S) is strict non-empty finitely-generated V105((y,c,S)) gate`2=den Boolean MSAlgebra over (y,c,S)
(y,c,S) is strict non-empty finitely-generated V105((y,c,S)) gate`2=den Boolean MSAlgebra over (y,c,S)
1GateCircuit (y,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2a)
1GateCircuit (<*y,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2a)
1GateCircuit (c,S,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*c,S*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*c,S*>,and2)
1GateCircuit (<*c,S*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*c,S*>,and2)
(1GateCircuit (y,c,and2a)) +* (1GateCircuit (c,S,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*y,c*>,and2a)) +* (1GateCircStr (<*c,S*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*y,c*>,and2a)) +* (1GateCircStr (<*c,S*>,and2))
1GateCircuit (y,S,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,S*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,S*>,and2a)
1GateCircuit (<*y,S*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*y,S*>,and2a)
((1GateCircuit (y,c,and2a)) +* (1GateCircuit (c,S,and2))) +* (1GateCircuit (y,S,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*y,c*>,and2a)) +* (1GateCircStr (<*c,S*>,and2))) +* (1GateCircStr (<*y,S*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*y,c*>,and2a)) +* (1GateCircStr (<*c,S*>,and2))) +* (1GateCircStr (<*y,S*>,and2a))
1GateCircuit ([<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3)
1GateCircuit (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3)
(y,c,S) +* (1GateCircuit ([<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a],or3)) is strict non-empty finitely-generated V105((y,c,S) +* (1GateCircStr (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (y,c,S) +* (1GateCircStr (<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3))
(y,c,S) +* (y,c,S) is strict non-empty finitely-generated V105((2GatesCircStr (y,c,S,'xor')) +* (y,c,S)) gate`2=den Boolean MSAlgebra over (2GatesCircStr (y,c,S,'xor')) +* (y,c,S)
the Sorts of (y,c,S) is Relation-like the carrier of (y,c,S) -defined Function-like V14( the carrier of (y,c,S)) set
the carrier of (y,c,S) is non empty set
K224( the Sorts of (y,c,S)) is functional V47() V48() set
(y,c,S) is Element of InnerVertices (2GatesCircStr (y,c,S,'xor'))
the carrier of (2GatesCircStr (y,c,S,'xor')) is non empty set
InnerVertices (2GatesCircStr (y,c,S,'xor')) is non empty Element of K27( the carrier of (2GatesCircStr (y,c,S,'xor')))
K27( the carrier of (2GatesCircStr (y,c,S,'xor'))) is set
the ResultSort of (2GatesCircStr (y,c,S,'xor')) is Relation-like the carrier' of (2GatesCircStr (y,c,S,'xor')) -defined the carrier of (2GatesCircStr (y,c,S,'xor')) -valued Function-like V18( the carrier' of (2GatesCircStr (y,c,S,'xor')), the carrier of (2GatesCircStr (y,c,S,'xor'))) Element of K27(K28( the carrier' of (2GatesCircStr (y,c,S,'xor')), the carrier of (2GatesCircStr (y,c,S,'xor'))))
the carrier' of (2GatesCircStr (y,c,S,'xor')) is non empty set
K28( the carrier' of (2GatesCircStr (y,c,S,'xor')), the carrier of (2GatesCircStr (y,c,S,'xor'))) is set
K27(K28( the carrier' of (2GatesCircStr (y,c,S,'xor')), the carrier of (2GatesCircStr (y,c,S,'xor')))) is set
K532( the carrier of (2GatesCircStr (y,c,S,'xor')), the ResultSort of (2GatesCircStr (y,c,S,'xor'))) is Element of K27( the carrier of (2GatesCircStr (y,c,S,'xor')))
2GatesCircOutput (y,c,S,'xor') is non empty pair Element of InnerVertices (2GatesCircStr (y,c,S,'xor'))
[<*[<*y,c*>,'xor'],S*>,'xor'] is non empty pair set
(y,c,S) is Element of InnerVertices (y,c,S)
the carrier of (y,c,S) is non empty set
InnerVertices (y,c,S) is non empty Element of K27( the carrier of (y,c,S))
K27( the carrier of (y,c,S)) is set
the ResultSort of (y,c,S) is Relation-like the carrier' of (y,c,S) -defined the carrier of (y,c,S) -valued Function-like V18( the carrier' of (y,c,S), the carrier of (y,c,S)) Element of K27(K28( the carrier' of (y,c,S), the carrier of (y,c,S)))
the carrier' of (y,c,S) is non empty set
K28( the carrier' of (y,c,S), the carrier of (y,c,S)) is set
K27(K28( the carrier' of (y,c,S), the carrier of (y,c,S))) is set
K532( the carrier of (y,c,S), the ResultSort of (y,c,S)) is Element of K27( the carrier of (y,c,S))
[<*[<*y,c*>,and2a],[<*c,S*>,and2],[<*y,S*>,and2a]*>,or3] is non empty pair set
s is Relation-like Function-like Element of K224( the Sorts of (y,c,S))
s . y is set
s . c is set
s . S is set
Following (s,2) is Relation-like Function-like Element of K224( the Sorts of (y,c,S))
(Following (s,2)) . (y,c,S) is set
(Following (s,2)) . (y,c,S) is set
s1 is Element of BOOLEAN
s2 is Element of BOOLEAN
t is Element of BOOLEAN
s1 'xor' s2 is Element of BOOLEAN
(s1 'xor' s2) 'xor' t is Element of BOOLEAN
'not' s1 is Element of BOOLEAN
('not' s1) '&' s2 is Element of BOOLEAN
s2 '&' t is Element of BOOLEAN
(('not' s1) '&' s2) 'or' (s2 '&' t) is Element of BOOLEAN
('not' s1) '&' t is Element of BOOLEAN
((('not' s1) '&' s2) 'or' (s2 '&' t)) 'or' (('not' s1) '&' t) is Element of BOOLEAN
the Sorts of (y,c,S) is Relation-like the carrier of (2GatesCircStr (y,c,S,'xor')) -defined Function-like V14( the carrier of (2GatesCircStr (y,c,S,'xor'))) set
K224( the Sorts of (y,c,S)) is functional V47() V48() set
s | the carrier of (2GatesCircStr (y,c,S,'xor')) is Relation-like Function-like set
a is Relation-like Function-like Element of K224( the Sorts of (y,c,S))
proj1 a is set
a . S is set
a . c is set
the Sorts of ((y,c,S) +* (y,c,S)) is Relation-like the carrier of ((2GatesCircStr (y,c,S,'xor')) +* (y,c,S)) -defined Function-like V14( the carrier of ((2GatesCircStr (y,c,S,'xor')) +* (y,c,S))) set
the carrier of ((2GatesCircStr (y,c,S,'xor')) +* (y,c,S)) is non empty set
K224( the Sorts of ((y,c,S) +* (y,c,S))) is functional V47() V48() set
InputVertices (2GatesCircStr (y,c,S,'xor')) is Element of K27( the carrier of (2GatesCircStr (y,c,S,'xor')))
the carrier of (2GatesCircStr (y,c,S,'xor')) \ K532( the carrier of (2GatesCircStr (y,c,S,'xor')), the ResultSort of (2GatesCircStr (y,c,S,'xor'))) is Element of K27( the carrier of (2GatesCircStr (y,c,S,'xor')))
t is Relation-like Function-like Element of K224( the Sorts of ((y,c,S) +* (y,c,S)))
Following (t,2) is Relation-like Function-like Element of K224( the Sorts of ((y,c,S) +* (y,c,S)))
(Following (t,2)) . (2GatesCircOutput (y,c,S,'xor')) is set
Following (a,2) is Relation-like Function-like Element of K224( the Sorts of (y,c,S))
(Following (a,2)) . (2GatesCircOutput (y,c,S,'xor')) is Element of BOOLEAN
the Sorts of (y,c,S) is Relation-like the carrier of (y,c,S) -defined Function-like V14( the carrier of (y,c,S)) set
K224( the Sorts of (y,c,S)) is functional V47() V48() set
s | the carrier of (y,c,S) is Relation-like Function-like set
s2 is Relation-like Function-like Element of K224( the Sorts of (y,c,S))
proj1 s2 is set
a . y is set
InputVertices (y,c,S) is Element of K27( the carrier of (y,c,S))
the carrier of (y,c,S) \ K532( the carrier of (y,c,S), the ResultSort of (y,c,S)) is Element of K27( the carrier of (y,c,S))
(Following (t,2)) . (y,c,S) is set
Following (s2,2) is Relation-like Function-like Element of K224( the Sorts of (y,c,S))
(Following (s2,2)) . (y,c,S) is Element of BOOLEAN
s2 . S is set
s2 . c is set
s2 . y is set
x is non pair set
y is non pair set
c is non pair set
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
2GatesCircStr (x,y,c,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,y*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,y*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,'xor'] is non empty pair set
<*[<*x,y*>,'xor'],c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor') is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
1GateCircStr (<*x,y*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*y,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*y,c*>,and2) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
<*x,c*> is Relation-like K100() -defined Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like V49() nonpair-yielding set
1GateCircStr (<*x,c*>,and2a) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
[<*x,y*>,and2a] is non empty pair set
[<*y,c*>,and2] is non empty pair set
[<*x,c*>,and2a] is non empty pair set
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> is Relation-like K100() -defined Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like V49() set
1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(2GatesCircStr (x,y,c,'xor')) +* (x,y,c) is non empty non void V69() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105( 2GatesCircStr (x,y,c,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr (x,y,c,'xor')
2GatesCircuit (x,y,c,'xor') is strict non-empty finitely-generated V105( 2GatesCircStr (x,y,c,'xor')) gate`2=den Boolean MSAlgebra over 2GatesCircStr (x,y,c,'xor')
1GateCircuit (x,y,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,'xor')
1GateCircuit (<*x,y*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,'xor')
1GateCircuit ([<*x,y*>,'xor'],c,'xor') is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')
1GateCircuit (<*[<*x,y*>,'xor'],c*>,'xor') is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor')
(1GateCircuit (x,y,'xor')) +* (1GateCircuit ([<*x,y*>,'xor'],c,'xor')) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor'))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,'xor')) +* (1GateCircStr (<*[<*x,y*>,'xor'],c*>,'xor'))
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
(x,y,c) is strict non-empty finitely-generated V105((x,y,c)) gate`2=den Boolean MSAlgebra over (x,y,c)
1GateCircuit (x,y,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,y*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (<*x,y*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,y*>,and2a)
1GateCircuit (y,c,and2) is strict non-empty finitely-generated V105( 1GateCircStr (<*y,c*>,and2)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*y,c*>,and2)
1GateCircuit (<*y,c*>,and2) is strict non-empty MSAlgebra over 1GateCircStr (<*y,c*>,and2)
(1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) is strict non-empty finitely-generated V105((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) gate`2=den Boolean MSAlgebra over (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))
1GateCircuit (x,c,and2a) is strict non-empty finitely-generated V105( 1GateCircStr (<*x,c*>,and2a)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
1GateCircuit (<*x,c*>,and2a) is strict non-empty MSAlgebra over 1GateCircStr (<*x,c*>,and2a)
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict non-empty finitely-generated V105(((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))) gate`2=den Boolean MSAlgebra over ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a))
1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3) is strict non-empty finitely-generated V105( 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) gate`2=den Boolean MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
1GateCircuit (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) is strict non-empty MSAlgebra over 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)
(x,y,c) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict non-empty finitely-generated V105((x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) gate`2=den Boolean MSAlgebra over (x,y,c) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))
(x,y,c) +* (x,y,c) is strict non-empty finitely-generated V105((2GatesCircStr (x,y,c,'xor')) +* (x,y,c)) gate`2=den Boolean MSAlgebra over (2GatesCircStr (x,y,c,'xor')) +* (x,y,c)
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
s is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (s,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
the Sorts of (x,y,c) is Relation-like the carrier of (2GatesCircStr (x,y,c,'xor')) -defined Function-like V14( the carrier of (2GatesCircStr (x,y,c,'xor'))) set
the carrier of (2GatesCircStr (x,y,c,'xor')) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
s | the carrier of (2GatesCircStr (x,y,c,'xor')) is Relation-like Function-like set
the Sorts of (x,y,c) is Relation-like the carrier of (x,y,c) -defined Function-like V14( the carrier of (x,y,c)) set
the carrier of (x,y,c) is non empty set
K224( the Sorts of (x,y,c)) is functional V47() V48() set
s | the carrier of (x,y,c) is Relation-like Function-like set
the Sorts of ((x,y,c) +* (x,y,c)) is Relation-like the carrier of ((2GatesCircStr (x,y,c,'xor')) +* (x,y,c)) -defined Function-like V14( the carrier of ((2GatesCircStr (x,y,c,'xor')) +* (x,y,c))) set
the carrier of ((2GatesCircStr (x,y,c,'xor')) +* (x,y,c)) is non empty set
K224( the Sorts of ((x,y,c) +* (x,y,c))) is functional V47() V48() set
Following (s,3) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
proj1 (Following (s,3)) is set
the carrier of (2GatesCircStr (x,y,c,'xor')) \/ the carrier of (x,y,c) is set
InputVertices (2GatesCircStr (x,y,c,'xor')) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
K27( the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
the ResultSort of (2GatesCircStr (x,y,c,'xor')) is Relation-like the carrier' of (2GatesCircStr (x,y,c,'xor')) -defined the carrier of (2GatesCircStr (x,y,c,'xor')) -valued Function-like V18( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) Element of K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))))
the carrier' of (2GatesCircStr (x,y,c,'xor')) is non empty set
K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor'))) is set
K27(K28( the carrier' of (2GatesCircStr (x,y,c,'xor')), the carrier of (2GatesCircStr (x,y,c,'xor')))) is set
K532( the carrier of (2GatesCircStr (x,y,c,'xor')), the ResultSort of (2GatesCircStr (x,y,c,'xor'))) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
the carrier of (2GatesCircStr (x,y,c,'xor')) \ K532( the carrier of (2GatesCircStr (x,y,c,'xor')), the ResultSort of (2GatesCircStr (x,y,c,'xor'))) is Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
InnerVertices (x,y,c) is non empty Element of K27( the carrier of (x,y,c))
K27( the carrier of (x,y,c)) is set
the ResultSort of (x,y,c) is Relation-like the carrier' of (x,y,c) -defined the carrier of (x,y,c) -valued Function-like V18( the carrier' of (x,y,c), the carrier of (x,y,c)) Element of K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c)))
the carrier' of (x,y,c) is non empty set
K28( the carrier' of (x,y,c), the carrier of (x,y,c)) is set
K27(K28( the carrier' of (x,y,c), the carrier of (x,y,c))) is set
K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
s1 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (s1,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
t is Relation-like Function-like Element of K224( the Sorts of ((x,y,c) +* (x,y,c)))
Following (t,2) is Relation-like Function-like Element of K224( the Sorts of ((x,y,c) +* (x,y,c)))
(Following (t,2)) | the carrier of (2GatesCircStr (x,y,c,'xor')) is Relation-like Function-like set
Following (s1,3) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (t,3) is Relation-like Function-like Element of K224( the Sorts of ((x,y,c) +* (x,y,c)))
(Following (t,3)) | the carrier of (2GatesCircStr (x,y,c,'xor')) is Relation-like Function-like set
Following (Following (s1,2)) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
2 + 1 is non pair V21() V22() V23() V27() Element of K100()
Following (s1,(2 + 1)) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
InputVertices (x,y,c) is Element of K27( the carrier of (x,y,c))
the carrier of (x,y,c) \ K532( the carrier of (x,y,c), the ResultSort of (x,y,c)) is Element of K27( the carrier of (x,y,c))
InnerVertices (2GatesCircStr (x,y,c,'xor')) is non empty Element of K27( the carrier of (2GatesCircStr (x,y,c,'xor')))
s2 is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (s2,2) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following (t,2)) | the carrier of (x,y,c) is Relation-like Function-like set
Following (s2,3) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following (t,3)) | the carrier of (x,y,c) is Relation-like Function-like set
Following (Following (s2,2)) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
Following (s2,(2 + 1)) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
proj1 (Following (s1,2)) is set
proj1 (Following (s2,2)) is set
a is set
(Following (s,2)) . a is set
(Following (s1,2)) . a is set
(Following (s,3)) . a is set
(Following (s1,3)) . a is set
(Following (s2,2)) . a is set
(Following (s2,3)) . a is set
Following (Following (s,2)) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
(Following (Following (s,2))) . a is set
Following (s,(2 + 1)) is Relation-like Function-like Element of K224( the Sorts of (x,y,c))
proj1 (Following (s,2)) is set