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 ] and
A2: y <> [<*x,c*>,and2a ] and
A3: c <> [<*x,y*>,and2a ] and
A4: c <> [<*x,y*>,'xor' ] ; :: thesis: InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c}
A5: InputVertices (2GatesCircStr x,y,c,'xor' ) = {x,y,c} by A4, FACIRC_1:57;
InputVertices (BorrowStr x,y,c) = {x,y,c} by A1, A2, A3, Th15;
hence InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c} by A5, CIRCCOMB:55, FACIRC_2:22; :: thesis: verum