let x, y, c be set ; :: thesis: InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))}
2GatesCircStr (x,y,c,'xor') tolerates BorrowStr (x,y,c) by CIRCCOMB:47;
then InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = (InnerVertices (2GatesCircStr (x,y,c,'xor'))) \/ (InnerVertices (BorrowStr (x,y,c))) by CIRCCOMB:11
.= {[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ (InnerVertices (BorrowStr (x,y,c))) by FACIRC_1:56
.= {[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))}) by Th14
.= ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} by XBOOLE_1:4 ;
hence InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} ; :: thesis: verum