let x, y, c be set ; 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))}
; verum