def un.or_zero

bend-osdev-u32@0.1.0.0 · PROOF.bend:2099

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

2099def 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}:
2100  match n:
2101    case 0n:
2102      {==}
2103    case 1n+ +p:
2104      match a b:
2105        case WCon{+x, +at} WCon{True{}, +bt}:
2106          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))
2107        case WCon{+x, +at} WCon{False{}, +bt}:
2108          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)))