def carry_complement

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/negation_magnitude.bend:10

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend as Counter

10# The increment after complement overflows precisely for a zero input.
11def carry_complement(+n: Nat, word: Word(n)) -> {Counter.carry(n, Word.not(n, word)) == W.is_zero(n, word) : Bool}:
12  match n:
13    case 0n: {==}
14    case 1n+ +p:
15      match word:
16        case WCon{+bit, +tail}:
17          Equal.cong(Bool, Bool, c => Bool.not(bit) && c, Counter.carry(p, Word.not(p, tail)), W.is_zero(p, tail), carry_complement(p, tail))