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:47;
then InnerVertices (BitAdderWithOverflowStr (x,y,c)) = (InnerVertices (2GatesCircStr (x,y,c,'xor'))) \/ (InnerVertices (MajorityStr (x,y,c))) by CIRCCOMB:11
.= {[<*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 Th19
.= ({[<*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