theorem Th5: :: GFACIRC2:5

for n being Nat
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitGFA0Str ((p ^ p1),(q ^ q1)) = n -BitGFA0Str ((p ^ p2),(q ^ q2)) & n -BitGFA0Circ ((p ^ p1),(q ^ q1)) = n -BitGFA0Circ ((p ^ p2),(q ^ q2)) & n -BitGFA0CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA0CarryOutput ((p ^ p2),(q ^ q2)) )