let x, y, c be non pair 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)}
set S1 = 2GatesCircStr x,y,c,'xor' ;
set S2 = MajorityStr x,y,c;
A1: ({[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]}) \/ {(MajorityOutput x,y,c)} = {[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ ({[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} \/ {(MajorityOutput x,y,c)}) by XBOOLE_1:4;
( InnerVertices (2GatesCircStr x,y,c,'xor' ) = {[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} & InnerVertices (MajorityStr x,y,c) = {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} \/ {(MajorityOutput x,y,c)} ) by Th56, Th75;
hence InnerVertices (BitAdderWithOverflowStr x,y,c) = ({[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]}) \/ {(MajorityOutput x,y,c)} by A1, Th27; :: thesis: verum