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:47, FACIRC_2:21; :: thesis: verum