For a proof of correctness, you can consider the operation of a circuit, treating it one full adder at a time. The output carry bit is monotone in the inputs, s

For a proof of correctness, you can consider the operation of a circuit, treating it one full adder at a time. The output carry bit is monotone in the inputs, so if an unknown bit could affect whether the input carry bit is set, it will be 1 when all unknown bits are assumed to be 1 and 0 when all unknown bits are assumed to be 0. The output non-carry bit is unknown if and only if at least one of the inputs (a,b or carry) is unknown. The first 2 cases are covered explicitly (a.unknowns|b.unknowns), and if both a and b are known and input carry is unknown, the input carry bit will differ between min and max (by the above argument), hence min will differ from max at that bit.