LAWS.vec_array_lower_bound_end: law of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/LAWS.bend as LAWS
Lines 358-359 of bend-osdev-algo@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&start_line=358&end_line=359

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S

law vec_array_lower_bound_end:
  {Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 10)) == 5 : U32}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.array_lower_bound