:: deftheorem Def5 defines -BitMajorityOutput FACIRC_2:def 5 :
for n being Nat
for x, y being FinSequence
for b₄ being Element of InnerVertices (n -BitAdderStr (x,y)) holds
( b₄ = n -BitMajorityOutput (x,y) iff ex h being ManySortedSet of NAT st
( b₄ = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );