~/bend-docscommunity

proofs/math/random/wrappers.bend source

proofs/math/random/wrappers.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/w64.bend as SWimport ../../../spec/math/random/source.bend as SRCimport ../../../spec/math/random.bend as SRMimport ../../../src/math/u64.bend as Wimport ../../../src/math/w64.bend as Ximport ../../../src/math/random/rand.bend as Rimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/u32.bend as Uimport ../../lib/lemmas/spec/numeric.bend as Simport ../typed/width.bend as WWimport ../typed/u32laws.bend as LWimport ../typed/w64add.bend as WAimport ../typed/f64bits.bend as FBimport ../typed/w64clz.bend as WCimport ../typed/w64sh.bend as SHimport ../typed/w64div.bend as W64Dimport ../u64/u64div.bend as PDimport ../typed/w64mul.bend as W64Mimport ../../lib/word.bend as WDimport ../../lib/arith.bend as LAimport ../natural/arith.bend as ARimport ./bounded.bend as MRimport ./lemire.bend as LE# The word slices (Go's Uint32, Int64, Int32) and the bounded wrappers# (Uint32N, IntN, lo + IntN(hi - lo)) of src/math/random/rand.bend, for every# source: the slices are the stated bits of the output, and the bounded ones# inherit Uint64n.lt.def v(+x: U32) -> Nat:  U32.to_nat(x)def val(+l: U32, +h: U32) -> Nat:  Nat.add(v(l), C.shift(32n, v(h)))# ---- Uint32: the top 32 bits ----def u32_p(-S: Data, p: W.U64 & S) -> {U32.to_nat(R.fst(U32, S, R.top32(S, p))) == C.high(32n, SW.value(SRC.fst64(S, p))) : Nat}:  match p:    case Tuple{x, s}:      match x:        case W.U64{+l, +h}:          Equal.sym(Nat, C.high(32n, val(l, h)), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l)))def uint32_value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> SRM.Uint32.value(~S, ~next, s):  u32_p(S, next(s))# ---- Int64: the low 63 bits ----def low63_v(+l: U32, +h: U32) -> {SW.value(W.U64{l, U32.and(h, 2147483647)}) == C.low(63n, val(l, h)) : Nat}:  +n = val(l, h)  Equal.trans(Nat, Nat.add(v(l), C.shift(32n, v(U32.and(h, 2147483647)))), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))), C.low(63n, n),    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), v(U32.and(h, 2147483647)), C.low(31n, v(h)), FB.andm(h, 31n, 2147483647, {==})),    Equal.sym(Nat, C.low(63n, n), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))),      Equal.trans(Nat, C.low(63n, n), Nat.add(C.low(32n, n), C.shift(32n, C.low(31n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))),        FB.low_split(32n, 31n, n),        Equal.trans(Nat, Nat.add(C.low(32n, n), C.shift(32n, C.low(31n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(31n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))),          Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.low(31n, C.high(32n, n)))), C.low(32n, n), v(l), WW.low_u(32n, v(l), v(h), LW.vb(l))),          Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, C.low(31n, z))), C.high(32n, n), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l)))))))def i64_p(-S: Data, p: W.U64 & S) -> {SW.value(R.fst(W.U64, S, R.low63(S, p))) == C.low(63n, SW.value(SRC.fst64(S, p))) : Nat}:  match p:    case Tuple{x, s}:      match x:        case W.U64{+l, +h}:          low63_v(l, h)def int64_value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> SRM.Int64.value(~S, ~next, s):  i64_p(S, next(s))# ---- Int32: the top 31 bits ----def half_bv(+b: Bool) -> {C.half(S.bit_value(b)) == 0n : Nat}:  match b:    case True{}:      {==}    case False{}:      {==}# x >> 1 is half of xdef shr_half(+x: U32) -> {v(U32.shr(x)) == C.half(v(x)) : Nat}:  +b = S.bit_value(U.low_bit(x))  +y = v(U32.shr(x))  Equal.sym(Nat, C.half(v(x)), y,    Equal.trans(Nat, C.half(v(x)), C.half(Nat.add(b, Nat.double(y))), y,      Equal.cong(Nat, Nat, z => C.half(z), v(x), Nat.add(b, Nat.double(y)), U.shr_split(x)),      Equal.trans(Nat, C.half(Nat.add(b, Nat.double(y))), Nat.add(C.half(b), y), y, WW.half_dbl(b, y),        Equal.cong(Nat, Nat, z => Nat.add(z, y), C.half(b), 0n, half_bv(U.low_bit(x))))))def i32_p(-S: Data, p: W.U64 & S) -> {U32.to_nat(R.fst(U32, S, R.top31(S, p))) == C.high(33n, SW.value(SRC.fst64(S, p))) : Nat}:  match p:    case Tuple{x, s}:      match x:        case W.U64{+l, +h}:          Equal.trans(Nat, v(U32.shr(h)), C.half(v(h)), C.high(33n, val(l, h)),            shr_half(h),            Equal.sym(Nat, C.high(33n, val(l, h)), C.half(v(h)),              Equal.trans(Nat, C.high(Nat.add(32n, 1n), val(l, h)), C.high(1n, C.high(32n, val(l, h))), C.half(v(h)),                WW.high_comp(1n, 32n, val(l, h)),                Equal.cong(Nat, Nat, z => C.high(1n, z), C.high(32n, val(l, h)), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l))))))def int32_value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> SRM.Int32.value(~S, ~next, s):  i32_p(S, next(s))# ---- Uint32N ----def lo_le(-S: Data, r: W.U64 & S) -> {Nat.is_le(U32.to_nat(R.fst(U32, S, R.lo32(S, r))), SW.value(R.fst(W.U64, S, r))) == True{} : Bool}:  match r:    case Tuple{x, s}:      match x:        case W.U64{+l, +h}:          N.le_add_right(v(l), C.shift(32n, v(h)))def nz_word(+n: U32, +hn: {U32.is_zero(n) == False{} : Bool}) -> {X.is_zero(W.U64{n, 0}) == False{} : Bool}:  %Equal.sym(Bool, U32.is_zero(n), False{}, hn) : {Bool.and(_, U32.is_zero(0)) == False{} : Bool}  {==}def uint32n_lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: U32, +hn: {U32.is_zero(n) == False{} : Bool}) -> SRM.Uint32n.lt(~S, ~next, s, n, hn):  h1 = MR.uint64n_lt(~S, ~next, s, W.U64{n, 0}, nz_word(n, hn))  +h2 = Equal.trans(Bool, Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), v(n)), Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), Nat.add(v(n), C.shift(32n, 0n))), True{},    Equal.cong(Nat, Bool, z => Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), z), v(n), Nat.add(v(n), C.shift(32n, 0n)), Equal.sym(Nat, Nat.add(v(n), 0n), v(n), N.add_zero(v(n)))),    h1)  N.le_lt_trans(U32.to_nat(R.fst(U32, S, R.lo32(S, R.uint64n(~S, ~next, s, W.U64{n, 0})))), SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), v(n), lo_le(S, R.uint64n(~S, ~next, s, W.U64{n, 0})), h2)# ---- Nat <-> U64 below 2^64: n48 (from proofs/math/typed/u64bgcd.bend)# and rand.bend's nat64, a byte at a time ----def vv(+x: W.U64) -> Nat:  SW.value(x)def s32(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {Nat.mul(Nat.mul(x, 65536n), 65536n) == C.shift(32n, x) : Nat}:  +k = W64D.k65536(one, h1)  +e1 = PD.mul_pow(one, h1, 16n, x, 65536n, k)  +e2 = Equal.trans(Nat, Nat.mul(Nat.mul(x, 65536n), 65536n), Nat.mul(WD.sc(16n, x), 65536n), WD.sc(16n, WD.sc(16n, x)), Equal.cong(Nat, Nat, z => Nat.mul(z, 65536n), Nat.mul(x, 65536n), WD.sc(16n, x), e1), PD.mul_pow(one, h1, 16n, WD.sc(16n, x), 65536n, k))  Equal.trans(Nat, Nat.mul(Nat.mul(x, 65536n), 65536n), WD.sc(16n, WD.sc(16n, x)), C.shift(32n, x), e2, Equal.trans(Nat, WD.sc(16n, WD.sc(16n, x)), WD.sc(32n, x), C.shift(32n, x), W64M.sc_sc(16n, 16n, x), Equal.sym(Nat, C.shift(32n, x), WD.sc(32n, x), W64M.shift_sc(32n, x))))def n48v(+one: Nat, +h1: {one == 1n : Nat}, +a: W.U64) -> {X.n48(a) == vv(a) : Nat}:  match a:    case W.U64{+l, +h}:      Equal.cong(Nat, Nat, z => Nat.add(U32.to_nat(l), z), Nat.mul(Nat.mul(U32.to_nat(h), 65536n), 65536n), C.shift(32n, U32.to_nat(h)), s32(one, h1, U32.to_nat(h)))def fits0(+a: Nat) -> {C.fits(a, 0n) == True{} : Bool}:  %Equal.sym(Nat, C.high(a, 0n), 0n, WC.high0(a)) : {Nat.is_eq(_, 0n) == True{} : Bool}  {==}# x < 2^k gives x 2^a < 2^(a + k)def fits_shift(+a: Nat, +k: Nat, +x: Nat, +h: {C.fits(k, x) == True{} : Bool}) -> {C.fits(Nat.add(a, k), C.shift(a, x)) == True{} : Bool}:  WW.limbs_fit(a, k, 0n, x, fits0(a), h)def sh8(k: Nat) -> Nat:  match k:    case 0n:      0n    case 1n+j:      Nat.add(8n, sh8(j))def div256(+n: Nat) -> {Nat.div(n, 256n) == C.high(8n, n) : Nat}:  Equal.sym(Nat, C.high(8n, n), Nat.div(n, 256n), WW.high_div(8n, n, 255n, {==}))def mod256(+n: Nat) -> {Nat.mod(n, 256n) == C.low(8n, n) : Nat}:  +q = C.high(8n, n)  +r = C.low(8n, n)  +e = Equal.trans(Nat, n, Nat.add(r, C.shift(8n, q)), Nat.add(Nat.mul(q, 256n), r), WW.low_high(8n, n),    Equal.trans(Nat, Nat.add(r, C.shift(8n, q)), Nat.add(C.shift(8n, q), r), Nat.add(Nat.mul(q, 256n), r), N.add_comm(r, C.shift(8n, q)),      Equal.cong(Nat, Nat, z => Nat.add(z, r), C.shift(8n, q), Nat.mul(q, 256n), WW.shift_mul(8n, q))))  Equal.trans(Nat, Nat.mod(n, 256n), Nat.mod(Nat.add(Nat.mul(q, 256n), r), 256n), r,    Equal.cong(Nat, Nat, z => Nat.mod(z, 256n), n, Nat.add(Nat.mul(q, 256n), r), e),    AR.mod_of(q, 255n, r, WW.lt_of_fits(8n, r, WW.low_fits(8n, n))))def byte_v(+n: Nat) -> {v(U32.from_nat(Nat.mod(n, 256n))) == C.low(8n, n) : Nat}:  %Equal.sym(Nat, Nat.mod(n, 256n), C.low(8n, n), mod256(n)) : {v(U32.from_nat(_)) == C.low(8n, n) : Nat}  U.to_nat_from_nat(C.low(8n, n), 8n, {==}, WW.lt_of_fits(8n, C.low(8n, n), WW.low_fits(8n, n)))# the words of w_go are the low 8k bits, for 8k <= 32def wgo(+k: Nat, +n: Nat, +hk: {Nat.is_le(sh8(k), 32n) == True{} : Bool}) -> {v(R.w_go(k, n)) == C.low(sh8(k), n) : Nat}:  match k:    case 0n:      {==}    case 1n+j:      +d = C.high(8n, n)      +hj = N.le_trans(sh8(j), Nat.add(8n, sh8(j)), 32n, LE.le_plus(8n, sh8(j)), hk)      +hj24 = Equal.trans(Bool, Nat.is_le(sh8(j), 24n), Nat.is_le(Nat.add(8n, sh8(j)), 32n), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(8n, sh8(j)), 32n), Nat.is_le(sh8(j), 24n), AR.le_add_cancel(8n, sh8(j), 24n)), hk)      +ih = Equal.trans(Nat, v(R.w_go(j, Nat.div(n, 256n))), C.low(sh8(j), Nat.div(n, 256n)), C.low(sh8(j), d), wgo(j, Nat.div(n, 256n), hj), Equal.cong(Nat, Nat, z => C.low(sh8(j), z), Nat.div(n, 256n), d, div256(n)))      +lw = C.low(sh8(j), d)      +f24 = SH.fits_mono(sh8(j), 24n, lw, hj24, WW.low_fits(sh8(j), d))      +f32s = fits_shift(8n, 24n, lw, f24)      +em = Equal.trans(Nat, v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))), C.low(32n, C.shift(8n, v(R.w_go(j, Nat.div(n, 256n))))), C.shift(8n, lw),        SH.mul_p2(R.w_go(j, Nat.div(n, 256n)), 8n, {==}),        Equal.trans(Nat, C.low(32n, C.shift(8n, v(R.w_go(j, Nat.div(n, 256n))))), C.low(32n, C.shift(8n, lw)), C.shift(8n, lw), Equal.cong(Nat, Nat, z => C.low(32n, C.shift(8n, z)), v(R.w_go(j, Nat.div(n, 256n))), lw, ih), WW.low_fit(32n, C.shift(8n, lw), f32s)))      +sum = Nat.add(C.low(8n, n), C.shift(8n, lw))      +es = Equal.sym(Nat, C.low(Nat.add(8n, sh8(j)), n), sum, FB.low_split(8n, sh8(j), n))      +fsum = SH.fits_mono(Nat.add(8n, sh8(j)), 32n, sum, hk, Equal.trans(Bool, C.fits(Nat.add(8n, sh8(j)), sum), C.fits(Nat.add(8n, sh8(j)), C.low(Nat.add(8n, sh8(j)), n)), True{}, Equal.cong(Nat, Bool, z => C.fits(Nat.add(8n, sh8(j)), z), sum, C.low(Nat.add(8n, sh8(j)), n), es), WW.low_fits(Nat.add(8n, sh8(j)), n)))      +bv = byte_v(n)      +vsum = Equal.trans(Nat, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), Nat.add(C.low(8n, n), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum,        Equal.cong(Nat, Nat, z => Nat.add(z, v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), v(U32.from_nat(Nat.mod(n, 256n))), C.low(8n, n), bv),        Equal.cong(Nat, Nat, z => Nat.add(C.low(8n, n), z), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))), C.shift(8n, lw), em))      +hf = Equal.trans(Bool, C.fits(32n, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))))), C.fits(32n, sum), True{}, Equal.cong(Nat, Bool, z => C.fits(32n, z), Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum, vsum), fsum)      Equal.trans(Nat, v(U32.add(U32.from_nat(Nat.mod(n, 256n)), U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), C.low(Nat.add(8n, sh8(j)), n),        WA.add_exact(1n, {==}, U32.from_nat(Nat.mod(n, 256n)), U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)), hf),        Equal.trans(Nat, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum, C.low(Nat.add(8n, sh8(j)), n), vsum, es))# skip(k, n) = n div 2^(8k)def skip_v(+k: Nat, +n: Nat) -> {R.skip(k, n) == C.high(sh8(k), n) : Nat}:  match k:    case 0n:      {==}    case 1n+j:      Equal.trans(Nat, R.skip(j, Nat.div(n, 256n)), C.high(sh8(j), Nat.div(n, 256n)), C.high(Nat.add(8n, sh8(j)), n),        skip_v(j, Nat.div(n, 256n)),        Equal.trans(Nat, C.high(sh8(j), Nat.div(n, 256n)), C.high(sh8(j), C.high(8n, n)), C.high(Nat.add(8n, sh8(j)), n),          Equal.cong(Nat, Nat, z => C.high(sh8(j), z), Nat.div(n, 256n), C.high(8n, n), div256(n)),          Equal.sym(Nat, C.high(Nat.add(8n, sh8(j)), n), C.high(sh8(j), C.high(8n, n)), WW.high_comp(sh8(j), 8n, n))))# THEOREM: nat64(n) denotes n, for n < 2^64def nat64_v(+n: Nat, +hn: {C.fits(64n, n) == True{} : Bool}) -> {vv(R.nat64(n)) == n : Nat}:  +l = C.low(32n, n)  +h = C.low(32n, C.high(32n, n))  +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), v(R.w_go(4n, n)), l, wgo(4n, n, {==}))  +e2 = Equal.cong(Nat, Nat, z => Nat.add(l, C.shift(32n, z)), v(R.w_go(4n, R.skip(4n, n))), h, Equal.trans(Nat, v(R.w_go(4n, R.skip(4n, n))), C.low(32n, R.skip(4n, n)), h, wgo(4n, R.skip(4n, n), {==}), Equal.cong(Nat, Nat, z => C.low(32n, z), R.skip(4n, n), C.high(32n, n), skip_v(4n, n))))  +e3 = Equal.sym(Nat, C.low(64n, n), Nat.add(l, C.shift(32n, h)), FB.low_split(32n, 32n, n))  Equal.trans(Nat, Nat.add(v(R.w_go(4n, n)), C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), Nat.add(l, C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), n, e1,    Equal.trans(Nat, Nat.add(l, C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), Nat.add(l, C.shift(32n, h)), n, e2,      Equal.trans(Nat, Nat.add(l, C.shift(32n, h)), C.low(64n, n), n, e3, WW.low_fit(64n, n, hn))))# ---- IntN ----def n48_p(-S: Data, r: W.U64 & S) -> {R.fst(Nat, S, R.to_nat(S, r)) == SW.value(R.fst(W.U64, S, r)) : Nat}:  match r:    case Tuple{x, s}:      n48v(1n, {==}, x)def intn_pos(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hw: {C.fits(64n, n) == True{} : Bool}) -> {Nat.is_lt(R.fst(Nat, S, R.intn_z(~S, ~next, s, n, False{})), n) == True{} : Bool}:  +w = {R.nat64(n) : W.U64}  +ev = nat64_v(n, hw)  +hz = Equal.trans(Bool, X.is_zero(w), Nat.is_eq(SW.value(w), 0n), False{}, WA.is_zero_value(w),    Equal.trans(Bool, Nat.is_eq(SW.value(w), 0n), Nat.is_eq(n, 0n), False{}, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(w), n, ev), N.is_eq_sym_false(0n, n, N.is_eq_lt(0n, n, hn))))  %Equal.sym(Nat, R.fst(Nat, S, R.to_nat(S, R.uint64n(~S, ~next, s, w))), SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, w))), n48_p(S, R.uint64n(~S, ~next, s, w))) : {Nat.is_lt(_, n) == True{} : Bool}  %ev : {Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, w))), _) == True{} : Bool}  MR.uint64n_lt(~S, ~next, s, w, hz)def intn_lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hw: {C.fits(64n, n) == True{} : Bool}) -> SRM.Intn.lt(~S, ~next, s, n, hn, hw):  %Equal.sym(Bool, Nat.is_eq(n, 0n), False{}, N.is_eq_sym_false(0n, n, N.is_eq_lt(0n, n, hn))) : {Nat.is_lt(R.fst(Nat, S, R.intn_z(~S, ~next, s, n, _)), n) == True{} : Bool}  intn_pos(~S, ~next, s, n, hn, hw)# ---- int_range ----def plus_fst(-S: Data, +lo: Nat, r: Nat & S) -> {R.fst(Nat, S, R.plus(S, lo, r)) == Nat.add(lo, R.fst(Nat, S, r)) : Nat}:  match r:    case Tuple{k, s}:      {==}def lt_pos(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(b, a)) == True{} : Bool}:  match a b:    case _ 0n:      Empty.absurd({Nat.is_lt(0n, Nat.sub(0n, a)) == True{} : Bool}, N.lt_zero_absurd(a, h))    case 0n 1n+q:      {==}    case 1n+p 1n+q:      lt_pos(p, q, h)def int_range_bounds(~S: Data, ~next: S -> W.U64 & S, +s: S, +lo: Nat, +hi: Nat, +h: {Nat.is_lt(lo, hi) == True{} : Bool}, +hw: {C.fits(64n, Nat.sub(hi, lo)) == True{} : Bool}) -> SRM.IntRange.bounds(~S, ~next, s, lo, hi, h, hw):  +d = Nat.sub(hi, lo)  +k = R.fst(Nat, S, R.intn(~S, ~next, s, d))  hk = intn_lt(~S, ~next, s, d, lt_pos(lo, hi, h), hw)  +up = Equal.trans(Bool, Nat.is_lt(Nat.add(lo, k), hi), Nat.is_lt(Nat.add(lo, k), Nat.add(lo, d)), True{},    Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(lo, k), z), hi, Nat.add(lo, d), Equal.sym(Nat, Nat.add(lo, d), hi, N.sub_add(hi, lo, N.lt_le(lo, hi, h)))),    N.lt_add_left(k, d, lo, hk))  %Equal.sym(Nat, R.fst(Nat, S, R.plus(S, lo, R.intn(~S, ~next, s, d))), Nat.add(lo, k), plus_fst(S, lo, R.intn(~S, ~next, s, d))) : {Bool.and(Nat.is_le(lo, _), Nat.is_lt(_, hi)) == True{} : Bool}  L.and_intro(Nat.is_le(lo, Nat.add(lo, k)), Nat.is_lt(Nat.add(lo, k), hi), N.le_add_right(lo, k), up)