PROOF.keys_sorted.go: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 179-197 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=179&end_line=197

import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O

def keys_sorted.go(
  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: O.OMap<K, V>, +lb: Maybe<&2, K>,
  +acc: List<&2, K>,
  +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, head(K, acc)) == True{} : Bool},
  lt: {lt_m(~K, ~cmp, lb, head(K, acc)) == True{} : Bool},
  sa: {Laws.sorted(~K, ~cmp, acc) == True{} : Bool}
) -> {sfrom(~K, ~cmp, lb, O.OMap.keys.go(K, V, t, acc)) == True{} : Bool}:
  match t:
    case O.OTip{}:
      sfrom.base(~K, ~cmp, lb, acc, lt, sa)
    case O.OBin{s, +k, v, +lo, +hi}:
      +A = Laws.above(~K, ~cmp, lb, k)
      +B = Laws.below(~K, ~cmp, head(K, acc), k)
      +L = Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k})
      +H = Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, head(K, acc))
      ih = keys_sorted.go(~K, ~V, ~cmp, hi, Some{k}, acc, c4.d(A, B, L, H, bt),
        lt_m.some(~K, ~cmp, head(K, acc), k, c4.b(A, B, L, H, bt)), sa)
      keys_sorted.go(~K, ~V, ~cmp, lo, lb, k <> O.OMap.keys.go(K, V, hi, acc),
        c4.c(A, B, L, H, bt), c4.a(A, B, L, H, bt), ih)

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=above
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=below
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=bounded
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=sorted
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.a
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.b
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.c
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.d
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=head
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=lt_m
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=lt_m.some
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=sfrom
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=sfrom.base
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.keys.go