:: deftheorem Def6 defines -BitAdderOutput FACIRC_2:def 6 :
for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b₅ being Element of InnerVertices (n -BitAdderStr (x,y)) holds
( b₅ = (k,n) -BitAdderOutput (x,y) iff ex i being Element of NAT st
( k = i + 1 & b₅ = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) );