let x, y, c be object ; :: thesis: for S being non empty ManySortedSign st S = BitAdderWithOverflowStr (x,y,c) holds

( x in the carrier of S & y in the carrier of S & c in the carrier of S )

set S1 = 2GatesCircStr (x,y,c,'xor');

let S be non empty ManySortedSign ; :: thesis: ( S = BitAdderWithOverflowStr (x,y,c) implies ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) )

assume A1: S = BitAdderWithOverflowStr (x,y,c) ; :: thesis: ( x in the carrier of S & y in the carrier of S & c in the carrier of S )

A2: c in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

( x in the carrier of (2GatesCircStr (x,y,c,'xor')) & y in the carrier of (2GatesCircStr (x,y,c,'xor')) ) by Th60;

hence ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) by A1, A2, Th20; :: thesis: verum

( x in the carrier of S & y in the carrier of S & c in the carrier of S )

set S1 = 2GatesCircStr (x,y,c,'xor');

let S be non empty ManySortedSign ; :: thesis: ( S = BitAdderWithOverflowStr (x,y,c) implies ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) )

assume A1: S = BitAdderWithOverflowStr (x,y,c) ; :: thesis: ( x in the carrier of S & y in the carrier of S & c in the carrier of S )

A2: c in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

( x in the carrier of (2GatesCircStr (x,y,c,'xor')) & y in the carrier of (2GatesCircStr (x,y,c,'xor')) ) by Th60;

hence ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) by A1, A2, Th20; :: thesis: verum