ProofBytes.byte_merge_hi.k: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytes
Lines 799-824 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=799&end_line=824

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_hi.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +hr: {Nat.is_le(r, 4n) == True{} : Bool}, +hj: {Nat.is_lt(j, 4n) == True{} : Bool},
  +h: {Nat.is_le(4n, Nat.add(j, r)) == True{} : Bool}, +k: Nat) ->
  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}:
  +l = Nat.is_lt(k, 8n)
  +i = Nat.add(Nat.mul(8n, j), k)
  +r8 = Nat.mul(8n, r)
  +u = Nat.sub(4n, r)
  +u8 = Nat.mul(8n, u)
  +hu = le_sub_l(4n, r, j, h)
  +x = D.bit(hi, Nat.add(Nat.mul(8n, Nat.sub(Nat.add(j, r), 4n)), k))
  %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), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))), bit_merge(lo, hi, r, j, k)) :
    {_ == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}
  %Equal.sym(Bool, D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k), Bool.and(l, x), bit_byte(hi, Nat.sub(Nat.add(j, r), 4n), k)) :
    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == _ : Bool}
  %Equal.sym(Bool, D.bit(lo, Nat.add(i, r8)), False{}, bit_ge32(lo, Nat.add(i, r8),
      %Equal.sym(Nat, Nat.add(i, r8), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), idx_add(j, r, k)) : {Nat.is_le(32n, _) == True{} : Bool}
      N.le_trans(32n, Nat.mul(8n, Nat.add(j, r)), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), N.le_mul_l(8n, 4n, Nat.add(j, r), h), N.le_add_r(Nat.mul(8n, Nat.add(j, r)), k)))) :
    {Bool.and(l, Bool.or(_, Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
  %Equal.sym(Bool, Nat.is_le(u8, i), True{}, N.le_trans(u8, Nat.mul(8n, j), i, N.le_mul_l(8n, u, j, hu), N.le_add_r(Nat.mul(8n, j), k))) :
    {Bool.and(l, Bool.or(False{}, Bool.and(_, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
  %Equal.sym(Nat, Nat.sub(i, u8), Nat.add(Nat.mul(8n, Nat.sub(j, u)), k), idx_sub(u, j, k, hu)) :
    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, _))))) == Bool.and(l, x) : Bool}
  %Equal.sym(Nat, Nat.sub(j, u), Nat.sub(Nat.add(j, r), 4n), sub_sub_eq(j, r, 4n, hr)) :
    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.add(Nat.mul(8n, _), k)))))) == Bool.and(l, x) : Bool}
  bimp(l, Nat.is_lt(i, 32n), x, hk => idx32(j, k, hj, hk))

Uses (26):
  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=bimp
  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_ge32
  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=idx32
  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=idx_sub
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=le_sub_l
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=sub_sub_eq
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_add_r
  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_trans