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