theorem :: FACIRC_2:11

for n being Nat
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitAdderStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr (a,b,(n -BitMajorityOutput (x,y)))) & (n + 1) -BitAdderCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitAdderCirc (x,y)) +* (BitAdderWithOverflowCirc (a,b,(n -BitMajorityOutput (x,y)))) & (n + 1) -BitMajorityOutput ((x ^ <*a*>),(y ^ <*b*>)) = MajorityOutput (a,b,(n -BitMajorityOutput (x,y))) )