let x, y, c be set ; :: thesis: InnerVertices (BitAdderWithOverflowStr x,y,c) = ({[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]}) \/ {(MajorityOutput x,y,c)}
2GatesCircStr x,y,c,'xor' tolerates MajorityStr x,y,c by CIRCCOMB:55;
then InnerVertices (BitAdderWithOverflowStr x,y,c) = (InnerVertices (2GatesCircStr x,y,c,'xor' )) \/ (InnerVertices (MajorityStr x,y,c)) by CIRCCOMB:15
.= {[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ (InnerVertices (MajorityStr x,y,c)) by FACIRC_1:56
.= {[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ ({[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} \/ {(MajorityOutput x,y,c)}) by Th20
.= ({[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]}) \/ {(MajorityOutput x,y,c)} by XBOOLE_1:4 ;
hence InnerVertices (BitAdderWithOverflowStr x,y,c) = ({[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]}) \/ {(MajorityOutput x,y,c)} ; :: thesis: verum