def wm.hl

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:81

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

81def wm.hl(+k: Nat, +x: Nat, +K: Nat, +hx: {Nat.is_lt(x, U.U32Nat.dbl(k, K)) == True{} : Bool}) -> {Nat.is_lt(U.U32Nat.high(k, x), K) == True{} : Bool}:
82  Equal.trans(Bool, Nat.is_lt(U.U32Nat.high(k, x), K), Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), Nat.is_lt(U.U32Nat.high(k, x), K), UL.dbl_lt(k, U.U32Nat.high(k, x), K)), Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x)))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x)))), Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), Equal.cong(Nat, Bool, zz => Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), zz), Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x))), U.U32Nat.dbl(k, K), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x))), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+x), U.U32Nat.dbl(k, K), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x))), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+Nat.add(U.U32Nat.low(k, x), U.U32Nat.dbl(k, U.U32Nat.high(k, x)))), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+x), wr.m0(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x), k, U.U32Nat.high(k, x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+zz), Nat.add(U.U32Nat.low(k, x), U.U32Nat.dbl(k, U.U32Nat.high(k, x))), x, UL.low_high(k, x))), UL.nat_lt_witness(x, U.U32Nat.dbl(k, K), hx)))), UL.nat_lt_add(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)))))