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

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

# Bit k of byte J of b << 8X, for b < 256 and k < 8: bit k of b when J = X.
def bsel.go(+b: U32, +x: Nat, +j: Nat, +k: Nat, +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool},
  +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, c: Cmp, +ec: {Nat.cmp(j, x) == c : Cmp}) ->
  {Bool.and(Nat.is_le(Nat.mul(8n, x), Nat.add(Nat.mul(8n, j), k)), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n),
     D.bit(b, Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, x)))))
   == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b, k))) : Bool}:
  match c:
    case LT{}:
      +p = Nat.add(Nat.mul(8n, j), k)
      +ii = Nat.is_lt(p, 32n)
      +hlt = {%Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {Cmp.is_lt(_) == True{} : Bool}; {==} : {Nat.is_lt(j, x) == True{} : Bool}}
      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), False{}, lt_not_le(p, Nat.mul(8n, x), N.lt_le_trans(p, Nat.mul(8n, 1n+j), Nat.mul(8n, x), lt_mul8(j, k, hk),
          N.le_mul_l(8n, 1n+j, x, %Equal.sym(Bool, Nat.is_le(1n+j, x), Nat.is_lt(j, x), N.le_succ_lt(j, x)) : {_ == True{} : Bool}; hlt)))) :
        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
      %Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {False{} == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
      {==}
    case EQ{}:
      +hjx = N.eq_sound(j, x, %Equal.sym(Cmp, Nat.cmp(j, x), EQ{}, ec) : {Cmp.is_eq(_) == True{} : Bool}; {==})
      +p = Nat.add(Nat.mul(8n, j), k)
      +ii = Nat.is_lt(p, 32n)
      %hjx : {Bool.and(Nat.is_le(Nat.mul(8n, _), p), Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, _))))) == Bool.and(Nat.is_eq(j, _), Bool.and(ii, D.bit(b, k))) : Bool}
      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, j), p), True{}, N.le_add_r(Nat.mul(8n, j), k)) :
        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, j))))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, j)), k, N.sub_add_l(Nat.mul(8n, j), k)) :
        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
      %Equal.sym(Bool, Nat.is_eq(j, j), True{}, N.eq_refl(j)) :
        {Bool.and(True{}, Bool.and(ii, D.bit(b, k))) == Bool.and(_, Bool.and(ii, D.bit(b, k))) : Bool}
      {==}
    case GT{}:
      +p = Nat.add(Nat.mul(8n, j), k)
      +ii = Nat.is_lt(p, 32n)
      +hxj = gt_flip(j, x, ec)
      +hle = N.lt_to_le(x, j, hxj)
      +q = Nat.add(Nat.mul(8n, Nat.sub(j, x)), k)
      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), True{}, N.le_trans(Nat.mul(8n, x), Nat.mul(8n, j), p, N.le_mul_l(8n, x, j, hle), N.le_add_r(Nat.mul(8n, j), k))) :
        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, x)), q, idx_sub(x, j, k, hle)) :
        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
      %Equal.sym(Bool, D.bit(b, q), False{}, bit_lt_pow(b, 8n, q, hb,
          N.le_trans(8n, Nat.mul(8n, Nat.sub(j, x)), q,
            N.le_mul_l(8n, 1n, Nat.sub(j, x), %Equal.sym(Bool, Nat.is_le(1n, Nat.sub(j, x)), Nat.is_lt(0n, Nat.sub(j, x)), N.le_succ_lt(0n, Nat.sub(j, x))) : {_ == True{} : Bool};
              lt_sub(0n, x, j, hxj)),
            N.le_add_r(Nat.mul(8n, Nat.sub(j, x)), k)))) :
        {Bool.and(True{}, Bool.and(ii, _)) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
      %Equal.sym(Cmp, Nat.cmp(j, x), GT{}, ec) : {Bool.and(ii, False{}) == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
      N.and_false_r(ii)

Uses (34):
  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=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_lt
  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.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  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.pow
  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=Base/base.bend&name=U32.to_nat
  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/proof_bytes.bend&name=bit_lt_pow
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_bytes.bend&name=gt_flip
  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=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=and_false_r
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=eq_refl
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=eq_sound
  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_succ_lt
  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=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_to_le
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=sub_add_l