PROOF.un.or_zero: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 2099-2108 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=2099&end_line=2108

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

def un.or_zero(n: Nat, +a: Word(n), +b: Word(n), hb: {Word.to_nat(n, b) == 0n : Nat}) -> {Word.to_nat(n, Word.or(n, a, b)) == Word.to_nat(n, a) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+ +p:
      match a b:
        case WCon{+x, +at} WCon{True{}, +bt}:
          Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{True{}, bt})) == Word.to_nat(1n+p, WCon{x, at}) : Nat}, un.sz(Nat.double(Word.to_nat(p, bt)), hb))
        case WCon{+x, +at} WCon{False{}, +bt}:
          Equal.trans(Nat, Word.to_nat(1n+p, WCon{Bool.or(x, False{}), Word.or(p, at, bt)}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, at))), Word.to_nat(1n+p, WCon{x, at}), Equal.trans(Nat, Word.to_nat(1n+p, WCon{Bool.or(x, False{}), Word.or(p, at, bt)}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, Word.or(p, at, bt)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, at))), Equal.trans(Nat, Word.to_nat(1n+p, WCon{Bool.or(x, False{}), Word.or(p, at, bt)}), Nat.add(U.U32Nat.bit(Bool.or(x, False{})), Nat.double(Word.to_nat(p, Word.or(p, at, bt)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, Word.or(p, at, bt)))), un.wc(p, Bool.or(x, False{}), Word.or(p, at, bt)), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.double(Word.to_nat(p, Word.or(p, at, bt)))), U.U32Nat.bit(Bool.or(x, False{})), U.U32Nat.bit(x), Equal.cong(Bool, Nat, zz => U.U32Nat.bit(zz), Bool.or(x, False{}), x, un.bor_f(x)))), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.bit(x), Nat.double(zz)), Word.to_nat(p, Word.or(p, at, bt)), Word.to_nat(p, at), un.or_zero(p, at, bt, un.dz0(Word.to_nat(p, bt), hb)))), Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, at}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, at))), un.wc(p, x, at)))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.bor_f
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.dz0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.sz
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.wc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit