let x, y, c be non pair 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)}
set S1 = 2GatesCircStr x,y,c,'xor' ;
set S2 = BorrowStr x,y,c;
A1: ( ({[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]}) \/ {(BorrowOutput x,y,c)} = {[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ ({[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)}) & InnerVertices (2GatesCircStr x,y,c,'xor' ) = {[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} ) by FACIRC_1:56, XBOOLE_1:4;
InnerVertices (BorrowStr x,y,c) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)} by Th9;
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)} by A1, FACIRC_1:27; :: thesis: verum