let x, y, c be set ; :: thesis: ( x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] & c <> [<*x,y*>,'xor' ] implies InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c} )
assume that
A1: ( x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] ) and
A2: c <> [<*x,y*>,'xor' ] ; :: thesis: InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c}
A3: InputVertices (2GatesCircStr x,y,c,'xor' ) = {x,y,c} by A2, FACIRC_1:57;
InputVertices (BorrowStr x,y,c) = {x,y,c} by A1, Th15;
hence InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c} by A3, CIRCCOMB:55, FACIRC_2:22; :: thesis: verum