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, Th21;
hence InputVertices (BitAdderWithOverflowStr x,y,c) = {x,y,c} by A5, Th22, CIRCCOMB:55; :: thesis: verum