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*>,'&' ] & y <> [<*c,x*>,'&' ] & c <> [<*x,y*>,'&' ] ) and
A2: c <> [<*x,y*>,'xor' ] ; :: thesis: InputVertices (BitAdderWithOverflowStr x,y,c) = {x,y,c}
A3: InputVertices (2GatesCircStr x,y,c,'xor' ) = {x,y,c} by A2, FACIRC_1:57;
InputVertices (MajorityStr x,y,c) = {x,y,c} by A1, Th21;
hence InputVertices (BitAdderWithOverflowStr x,y,c) = {x,y,c} by A3, Th22, CIRCCOMB:55; :: thesis: verum