def bitw.popcount_not

bend-osdev-algo@0.1.0.0 · PROOF.bend:171

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

171def bitw.popcount_not(n: Nat, w: Word(n)) -> {Nat.add(A.bitw.popcount(n, w), A.bitw.popcount(n, Word.not(n, w))) == n : Nat}:
172  match n:
173    case 0n:
174      {==}
175    case 1n+ +p:
176      match w:
177        case WCon{True{}, +t}:
178          %bitw.popcount_not(p, t) : {1n+Nat.add(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t))) == 1n+_ : Nat}
179          {==}
180        case WCon{False{}, +t}:
181          %Equal.sym(Nat, Nat.add(A.bitw.popcount(p, t), 1n+A.bitw.popcount(p, Word.not(p, t))), 1n+Nat.add(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t))), nat.add_succ(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t)))) : {_ == 1n+p : Nat}
182          %bitw.popcount_not(p, t) : {1n+Nat.add(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t))) == 1n+_ : Nat}
183          {==}