ProofBytes.pack4_bytes.go: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytes
Lines 1309-1328 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=1309&end_line=1328

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 pack4_bytes.go(+w: U32, +j: Nat, +k: Nat, +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, z: Bool, +ez: {Nat.is_lt(j, 4n) == z : Bool}) ->
  {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), Nat.add(Nat.mul(8n, j), k)) == D.bit(w, Nat.add(Nat.mul(8n, j), k)) : Bool}:
  match z:
    case True{}:
      +p = Nat.add(Nat.mul(8n, j), k)
      %Equal.sym(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p),
          D.bit(D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), k),
          pack_byte(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n), j, k,
            lt256(D.byte(w, 0n), byte_lt(w, 0n)), lt256(D.byte(w, 1n), byte_lt(w, 1n)), lt256(D.byte(w, 2n), byte_lt(w, 2n)), lt256(D.byte(w, 3n), byte_lt(w, 3n)), ez, hk)) :
        {_ == D.bit(w, p) : Bool}
      %Equal.sym(U32, D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), D.byte(w, j), nth4_byte(w, j, ez)) : {D.bit(_, k) == D.bit(w, p) : Bool}
      %Equal.sym(Bool, D.bit(D.byte(w, j), k), Bool.and(Nat.is_lt(k, 8n), D.bit(w, p)), bit_byte(w, j, k)) : {_ == D.bit(w, p) : Bool}
      %Equal.sym(Bool, Nat.is_lt(k, 8n), True{}, hk) : {Bool.and(_, D.bit(w, p)) == D.bit(w, p) : Bool}
      {==}
    case False{}:
      +p = Nat.add(Nat.mul(8n, j), k)
      +h32 = N.le_trans(32n, Nat.mul(8n, j), p, N.le_mul_l(8n, 4n, j, N.not_lt_le(j, 4n, ez)), N.le_add_r(Nat.mul(8n, j), k))
      Equal.trans(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p), False{}, D.bit(w, p),
        bit_ge32(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p, h32),
        Equal.sym(Bool, D.bit(w, p), False{}, bit_ge32(w, p, h32)))

Uses (23):
  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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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_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=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=nth4
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=pack4
  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=byte_lt
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=lt256
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=nth4_byte
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=pack_byte
  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
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=not_lt_le