def wsd.kn

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:135

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
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

135# x < 2^h 10: x < 2^n (for 10 <= 2^h)
136def wsd.kn(+n: Nat, +h: Nat, +x: Nat, +en: {Nat.add(h, h) == n : Nat}, +h10: {Nat.is_le(10n, U.U32Nat.dbl(h, 1n)) == True{} : Bool}, +hx: {Nat.is_lt(x, U.U32Nat.dbl(h, 10n)) == True{} : Bool}) -> {Nat.is_lt(x, U.U32Nat.dbl(n, 1n)) == True{} : Bool}:
137  +hh = UO.nat_lt_le_trans(x, U.U32Nat.dbl(h, 10n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), hx, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(h, 10n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n))), Nat.is_le(10n, U.U32Nat.dbl(h, 1n)), True{}, UL.dbl_le(h, 10n, U.U32Nat.dbl(h, 1n)), h10))
138  Equal.trans(Bool, Nat.is_lt(x, U.U32Nat.dbl(n, 1n)), Nat.is_lt(x, U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n))), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(x, zz), U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), Equal.sym(Nat, U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), U.U32Nat.dbl(n, 1n), Equal.sym(Nat, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), wm.fn(h, n, 1n, en)))), hh)