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:55;
then InnerVertices (BitSubtracterWithBorrowStr x,y,c) = (InnerVertices (2GatesCircStr x,y,c,'xor' )) \/ (InnerVertices (BorrowStr x,y,c)) by CIRCCOMB:15
.= {[<*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