let x, y, c be set ; :: thesis: ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] implies InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c} )
assume that
A1: x <> [<*y,c*>,'&'] and
A2: y <> [<*c,x*>,'&'] and
A3: c <> [<*x,y*>,'&'] and
A4: c <> [<*x,y*>,'xor'] ; :: thesis: InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}
A5: InputVertices (2GatesCircStr (x,y,c,'xor')) = {x,y,c} by A4, FACIRC_1:57;
InputVertices (MajorityStr (x,y,c)) = {x,y,c} by A1, A2, A3, Th20;
hence InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c} by A5, Th21, CIRCCOMB:47; :: thesis: verum