BendMlTensorArray.half_go_le: def of bend-ml-tensor-array@0.1.19.0
Import: import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
Lines 1533-1544 of bend-ml-tensor-array@0.1.19.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&start_line=1533&end_line=1544

import Base

# half.go(n, acc) <= n + acc
def half_go_le(+n: Nat, +acc: Nat) -> {True{} == leb(half.go(n, acc), Nat.add(n, acc)) : Bool}:
  match n:
    case 0n:
      leb_refl(acc)
    case 1n+p:
      match p:
        case 0n:
          leb_succ(acc, acc, leb_refl(acc))
        case 1n+q:
          %Equal.sym(Nat, 1n+Nat.add(q, acc), Nat.add(q, 1n+acc), add_succ_r(q, acc)) : {True{} == leb(half.go(q, 1n+acc), 1n+_) : Bool}
          leb_succ(half.go(q, 1n+acc), Nat.add(q, 1n+acc), half_go_le(q, 1n+acc))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=bend-ml-tensor-array@0.1.19.0/main.bend&name=add_succ_r
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=half.go
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_refl
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_succ