ProofBytes.byte_merge_lo.k: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytes
Lines 771-786 of lawful-words@0.1.0.0/proof_bytes.bend: https://jend.leeeet.dev/read.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&start_line=771&end_line=786

import Base
import lawful-words@0.1.0.0/defs.bend as D
import lawful-words@0.1.0.0/proof_nat.bend as N

def byte_merge_lo.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}, +k: Nat) ->
  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}:
  +l = Nat.is_lt(k, 8n)
  +i = Nat.add(Nat.mul(8n, j), k)
  +r8 = Nat.mul(8n, r)
  +u8 = Nat.mul(8n, Nat.sub(4n, r))
  +y = Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))
  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k), Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))), bit_merge(lo, hi, r, j, k)) :
    {_ == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}
  %Equal.sym(Bool, D.bit(D.byte(lo, Nat.add(j, r)), k), Bool.and(l, D.bit(lo, Nat.add(Nat.mul(8n, Nat.add(j, r)), k))), bit_byte(lo, Nat.add(j, r), k)) :
    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == _ : Bool}
  %idx_add(j, r, k) : {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == Bool.and(l, D.bit(lo, _)) : Bool}
  bor_low(l, D.bit(lo, Nat.add(i, r8)), Nat.is_le(u8, i), y,
    hk => lt_not_le(i, u8, N.lt_le_trans(i, Nat.mul(8n, 1n+j), u8, lt_mul8(j, k, hk),
      N.le_mul_l(8n, 1n+j, Nat.sub(4n, r), %Equal.sym(Bool, Nat.is_le(1n+j, Nat.sub(4n, r)), Nat.is_lt(j, Nat.sub(4n, r)), N.le_succ_lt(j, Nat.sub(4n, r))) : {_ == True{} : Bool};
        lt_sub(j, r, 4n, h)))))

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=bit
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=merge
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=bit_byte
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=bit_merge
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=bor_low
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=idx_add
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=lt_mul8
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=lt_not_le
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=lt_sub
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_mul_l
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_succ_lt
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_le_trans