theorem :: FACIRC_1:89

for x, y, c being non pair object holds InputVertices (BitAdderWithOverflowStr (x,y,c)) is without_pairs