theorem Th10: :: FACIRC_2:10

for n being Nat
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitAdderStr ((p ^ p1),(q ^ q1)) = n -BitAdderStr ((p ^ p2),(q ^ q2)) & n -BitAdderCirc ((p ^ p1),(q ^ q1)) = n -BitAdderCirc ((p ^ p2),(q ^ q2)) & n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2)) )