bend-osdev-array

Releases (2):
  0.1.0.1  0xf8d2948fe25df08ae8d37c3c80a363ba  indexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-array@0.1.0.1
  0.1.0.0  0x4fcda21d38b51a2f03fa460c0b81cfc3  unindexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-array@0.1.0.0

Definitions (227, 1 to 100 shown):
  LAWS.get_same_array (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=get_same_array)
   law get_same_array:
     for -T: Data
     for a: Array<T>
     for i: U32
     {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}
  LAWS.get_set_same (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=get_set_same)
   law get_set_same:
     for -T: Data
     for a: Array<T>
     for i: U32
     for v: T
     {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}
  LAWS.set_keeps_size (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=set_keeps_size)
   law set_keeps_size:
     for -T: Data
     for a: Array<T>
     for i: U32
     for v: T
     {Pair.snd(Array<T>, U32, Array.size(T, Array.set(T, a, i, v))) == Pair.snd(Array<T>, U32, Array.size(T, a)) : U32}
  LAWS.get_new (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=get_new)
   law get_new:
     for -T: Data
     for d: Nat
     for v: T
     for i: U32
     {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}
  LAWS.new_perfect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=new_perfect)
   law new_perfect:
     for -T: Data
     for d: Nat
     for v: T
     {A.Arrays.is_perfect(T, d, Array.new(T, d, v)) == True{} : Bool}
  LAWS.set_perfect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=set_perfect)
   law set_perfect:
     for -T: Data
     for d: Nat
     for a: Array<T>
     for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
     for i: U32
     for v: T
     {A.Arrays.is_perfect(T, d, Array.set(T, a, i, v)) == True{} : Bool}
  LAWS.size_perfect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=size_perfect)
   law size_perfect:
     for -T: Data
     for d: Nat
     for a: Array<T>
     for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
     {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}
  LAWS.new_leaves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=new_leaves)
   law new_leaves:
     for -T: Data
     for d: Nat
     for v: T
     {A.Arrays.leaves(T, Array.new(T, d, v)) == List.replicate(T, A.Arrays.slots(d), v) : List<&2, T>}
  LAWS.model_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=model_length)
   law model_length:
     for -T: Data
     for d: Nat
     for a: Array<T>
     for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
     {List.length(&2, T, A.Arrays.leaves(T, a)) == A.Arrays.slots(d) : Nat}
  LAWS.model_get (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=model_get)
   law model_get:
     for -T: Data
     for d: Nat
     for a: Array<T>
     for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for i: U32
     {List.get(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} : Maybe<&2, T>}
  LAWS.model_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=model_set)
   law model_set:
     for -T: Data
     for d: Nat
     for a: Array<T>
     for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for i: U32
     for v: T
     {A.Arrays.leaves(T, Array.set(T, a, i, v)) == List.set(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i), v) : List<&2, T>}
  LAWS.get_set_other (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=get_set_other)
   law get_set_other:
     for -T: Data
     for d: Nat
     for a: Array<T>
     for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for i: U32
     for j: U32
     for v: T
     for hij: {U32.is_eq(U32.and(i, U32.sub(U32.shln(1, d), 1)), U32.and(j, U32.sub(U32.shln(1, d), 1))) == False{} : Bool}
     {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}
  LAWS.index_below (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=index_below)
   law index_below:
     for d: Nat
     for i: U32
     {Nat.is_lt(A.Arrays.index(d, i), A.Arrays.slots(d)) == True{} : Bool}
  LAWS.index_of_nat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=index_of_nat)
   law index_of_nat:
     for d: Nat
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for k: Nat
     for hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}
     {A.Arrays.index(d, U32.from_nat(k)) == k : Nat}
  LAWS.index_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=index_wrap)
   law index_wrap:
     for d: Nat
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for k: Nat
     for hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}
     {A.Arrays.index(d, U32.from_nat(Nat.add(A.Arrays.slots(d), k))) == k : Nat}
  LAWS.index_of_u32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=index_of_u32)
   law index_of_u32:
     for d: Nat
     for i: U32
     for hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}
     {A.Arrays.index(d, i) == U32.to_nat(i) : Nat}
  LAWS.of_list_perfect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_perfect)
   law of_list_perfect:
     for -T: Data
     for +d: Nat
     for +xs: List<&2, T>
     for +f: T
     {A.Arrays.is_perfect(T, d, A.Arrays.of_list(T, d, xs, f)) == True{} : Bool}
  LAWS.of_list_leaves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_leaves)
   law of_list_leaves:
     for -T: Data
     for +d: Nat
     for +xs: List<&2, T>
     for +f: T
     for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
     {A.Arrays.leaves(T, A.Arrays.of_list(T, d, xs, f)) == xs : List<&2, T>}
  LAWS.of_list_size (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_size)
   law of_list_size:
     for -T: Data
     for +d: Nat
     for +xs: List<&2, T>
     for +f: T
     {Array.size(T, A.Arrays.of_list(T, d, xs, f)) == (A.Arrays.of_list(T, d, xs, f), U32.shln(1, d)) : Array<T> & U32}
  LAWS.of_list_get (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_get)
   law of_list_get:
     for -T: Data
     for +d: Nat
     for +xs: List<&2, T>
     for +f: T
     for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
     for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for +i: U32
     {Array.get(T, A.Arrays.of_list(T, d, xs, f), i) == (A.Arrays.of_list(T, d, xs, f), A.Arrays.nth(T, xs, A.Arrays.index(d, i), f)) : Array<T> & T}
  LAWS.of_list_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_set)
   law of_list_set:
     for -T: Data
     for +d: Nat
     for +xs: List<&2, T>
     for +f: T
     for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
     for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for +i: U32
     for +v: T
     {Array.set(T, A.Arrays.of_list(T, d, xs, f), i, v) == A.Arrays.of_list(T, d, List.set(&2, T, xs, A.Arrays.index(d, i), v), f) : Array<T>}
  LAWS.of_list_new (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_new)
   law of_list_new:
     for -T: Data
     for +d: Nat
     for +v: T
     {Array.new(T, d, v) == A.Arrays.of_list(T, d, List.replicate(T, A.Arrays.slots(d), v), v) : Array<T>}
  LAWS.reflect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=reflect)
   law reflect:
     for -T: Data
     for +d: Nat
     for a: Array<T>
     for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
     for +f: T
     exs xs: List<&2, T>
     {A.Arrays.of_list(T, d, xs, f) == a : Array<T>} & {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
  LAWS.set_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=set_length)
   law set_length:
     for -T: Data
     for xs: List<&2, T>
     for k: Nat
     for v: T
     {List.length(&2, T, List.set(&2, T, xs, k, v)) == List.length(&2, T, xs) : Nat}
  LAWS.nth_set_same (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=nth_set_same)
   law nth_set_same:
     for -T: Data
     for xs: List<&2, T>
     for k: Nat
     for v: T
     for f: T
     for h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}
     {A.Arrays.nth(T, List.set(&2, T, xs, k, v), k, f) == v : T}
  LAWS.nth_set_other (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=nth_set_other)
   law nth_set_other:
     for -T: Data
     for xs: List<&2, T>
     for k: Nat
     for m: Nat
     for v: T
     for f: T
     for h: {Nat.is_eq(k, m) == False{} : Bool}
     {A.Arrays.nth(T, List.set(&2, T, xs, k, v), m, f) == A.Arrays.nth(T, xs, m, f) : T}
  LAWS.nth_replicate (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=nth_replicate)
   law nth_replicate:
     for -T: Data
     for n: Nat
     for v: T
     for k: Nat
     for f: T
     for h: {Nat.is_lt(k, n) == True{} : Bool}
     {A.Arrays.nth(T, List.replicate(T, n, v), k, f) == v : T}
  LAWS.witness_perfect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=witness_perfect)
   law witness_perfect:
     {Bool.and(A.Arrays.is_perfect(U32, 2n, Array.new(U32, 2n, 0)), Nat.is_lt(2n, 32n)) == True{} : Bool}
  LAWS.witness_other (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=witness_other)
   law witness_other:
     {U32.is_eq(U32.and(1, U32.sub(U32.shln(1, 2n), 1)), U32.and(2, U32.sub(U32.shln(1, 2n), 1))) == False{} : Bool}
  LAWS.witness_index (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=witness_index)
   law witness_index:
     {Nat.is_lt(3n, A.Arrays.slots(2n)) == True{} : Bool}
  LAWS.witness_index_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=witness_index_wrap)
   law witness_index_wrap:
     {Bool.and(Nat.is_lt(U32.to_nat(5), A.Arrays.slots(3n)), Nat.is_lt(3n, A.Arrays.slots(2n))) == True{} : Bool}
  LAWS.witness_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=witness_list)
   law witness_list:
     {Bool.and(Nat.is_eq(List.length(&2, U32, [5, 6, 7, 8]), A.Arrays.slots(2n)), Bool.and(Nat.is_lt(1n, 4n), Nat.is_ne(1n, 2n))) == True{} : Bool}
  LAWS.vector_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=vector_wrap)
   law vector_wrap:
     {Pair.snd(Array<U32>, U32, Array.get(U32, Array.set(U32, Array.new(U32, 2n, 0), 6, 9), 2)) == 9 : U32}
  LAWS.vector_leaves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=vector_leaves)
   law vector_leaves:
     {A.Arrays.leaves(U32, Array.set(U32, Array.new(U32, 2n, 0), 1, 7)) == [0, 7, 0, 0] : List<&2, U32>}
  LAWS.vector_index (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=vector_index)
   law vector_index:
     {A.Arrays.index(3n, 13) == 5n : Nat}
  LAWS.vector_of_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=vector_of_list)
   law vector_of_list:
     {Pair.snd(Array<U32>, U32, Array.get(U32, Array.set(U32, A.Arrays.of_list(U32, 2n, [5, 6, 7, 8], 0), 1, 9), 5)) == 9 : U32}
  LAWS.vector_index_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=vector_index_wrap)
   law vector_index_wrap:
     {A.Arrays.index(2n, U32.from_nat(Nat.add(A.Arrays.slots(2n), 3n))) == 3n : Nat}
  LAWS.vector_not_perfect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=vector_not_perfect)
   law vector_not_perfect:
     {A.Arrays.is_perfect(U32, 2n, ANode{ALeaf{1}, ANode{ALeaf{2}, ALeaf{3}}}) == False{} : Bool}
  PROOF.AP.bool_t (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.bool_t)
   def AP.bool_t(b: Bool) -> Type:
  PROOF.AP.ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.ft)
   def AP.ft(e: {False{} == True{} : Bool}) -> Empty:
  PROOF.AP.tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.tf)
   def AP.tf(e: {True{} == False{} : Bool}) -> Empty:
  PROOF.AP.nat_t (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.nat_t)
   def AP.nat_t(n: Nat) -> Type:
  PROOF.AP.sz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.sz)
   # 1 + k is never 0
   def AP.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
  PROOF.AP.succ_cong (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.succ_cong)
   def AP.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
  PROOF.AP.double_cong (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.double_cong)
   def AP.double_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.double(a) == Nat.double(b) : Nat}:
  PROOF.AP.double_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.double_add)
   def AP.double_add(x: Nat, -y: Nat) -> {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}:
  PROOF.AP.lt_cancel (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_cancel)
   def AP.lt_cancel(s: Nat, -r: Nat, -u: Nat) -> {Nat.is_lt(Nat.add(s, r), Nat.add(s, u)) == Nat.is_lt(r, u) : Bool}:
  PROOF.AP.le_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.le_succ)
   def AP.le_succ(y: Nat, x: Nat) -> {Nat.is_le(1n+y, x) == Nat.is_lt(y, x) : Bool}:
  PROOF.AP.not_lt_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.not_lt_le)
   def AP.not_lt_le(x: Nat, y: Nat, e: {Nat.is_lt(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
  PROOF.AP.lt_one (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_one)
   def AP.lt_one(x: Nat, e: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
  PROOF.AP.double_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.double_zero)
   def AP.double_zero(x: Nat, e: {Nat.double(x) == 0n : Nat}) -> {x == 0n : Nat}:
  PROOF.AP.bv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.bv)
   def AP.bv(b: Bool, x: Nat) -> Nat:
  PROOF.AP.nc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.nc)
   def AP.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(AP.bv(a, x), AP.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
  PROOF.AP.cb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.cb)
   def AP.cb(c: Bool) -> Nat:
  PROOF.AP.fin_le_ff (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.fin_le_ff)
   def AP.fin_le_ff(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, False{}, c)) == Cmp.is_le(c) : Bool}:
  PROOF.AP.fin_le_tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.fin_le_tf)
   def AP.fin_le_tf(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(True{}, False{}, c)) == Cmp.is_lt(c) : Bool}:
  PROOF.AP.fin_le_ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.fin_le_ft)
   def AP.fin_le_ft(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, True{}, c)) == Cmp.is_le(c) : Bool}:
  PROOF.AP.fin_lt_xf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.fin_lt_xf)
   def AP.fin_lt_xf(b: Bool, c: Cmp) -> {Cmp.is_lt(Word.cmp.fin(b, False{}, c)) == Cmp.is_lt(c) : Bool}:
  PROOF.AP.le_bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.le_bits)
   def AP.le_bits(+y: Nat, +x: Nat, +a: Bool, +b: Bool, h: {Nat.is_le(AP.bv(a, y), AP.bv(b, x)) == True{} : Bool}) -> {Cmp.is_le(Word.cmp.fin(a, b, Nat.cmp(y, x))) == True{} : Bool}:
  PROOF.AP.lt_bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_bits)
   def AP.lt_bits(+y: Nat, +x: Nat, +a: Bool, +b: Bool, h: {Nat.is_lt(AP.bv(a, y), AP.bv(b, x)) == True{} : Bool}) -> {Cmp.is_lt(Word.cmp.fin(a, b, Nat.cmp(y, x))) == True{} : Bool}:
  PROOF.AP.ha (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.ha)
   def AP.ha(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(False{}, y), AP.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
  PROOF.AP.hb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.hb)
   def AP.hb(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(True{}, y), AP.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(1n+y, x) == True{} : Bool}:
  PROOF.AP.hc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.hc)
   def AP.hc(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(False{}, y), AP.bv(True{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
  PROOF.AP.alg2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.alg2)
   def AP.alg2(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(1n+Nat.double(r), 1n+Nat.double(y)) : Nat}:
  PROOF.AP.alg4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.alg4)
   def AP.alg4(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(Nat.double(r), 2n+Nat.double(y)) : Nat}:
  PROOF.AP.alg6 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.alg6)
   def AP.alg6(+r: Nat, +y: Nat) -> {1n+Nat.double(Nat.add(r, y)) == Nat.add(Nat.double(r), 1n+Nat.double(y)) : Nat}:
  PROOF.AP.adc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.adc)
   # for b <= a (b < a when the carry in c is False):
   # a = adc(a, b, True, c) + (1 - c) + b
   def AP.adc(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_le(Nat.add(AP.cb(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) -> {Word.to_nat(n, a) == Nat.add(Word.to_nat(n, Word.adc(n, a, b, True{}, c)), Nat.add(AP.cb(c), Word.to_nat(n, b))) : Nat}:
  PROOF.AP.wcon_cong (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.wcon_cong)
   def AP.wcon_cong(-p: Nat, -b: Bool, -x: Word(p), -y: Word(p), e: {x == y : Word(p)}) -> {WCon{b, x} == WCon{b, y} : Word(1n+p)}:
  PROOF.AP.u32_cong (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.u32_cong)
   def AP.u32_cong(-x: Word(32n), -y: Word(32n), e: {x == y : Word(32n)}) -> {U32{x} == U32{y} : U32}:
  PROOF.AP.pw (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.pw)
   def AP.pw(n: Nat, d: Nat) -> Word(n):
  PROOF.AP.lm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lm)
   def AP.lm(n: Nat, d: Nat) -> Word(n):
  PROOF.AP.spzz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.spzz)
   def AP.spzz(n: Nat) -> {Word.shl.put(n, False{}, Word.zero(n)) == Word.zero(n) : Word(n)}:
  PROOF.AP.spz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.spz)
   def AP.spz(n: Nat) -> {Word.shl.put(n, True{}, Word.zero(n)) == AP.pw(n, 0n) : Word(n)}:
  PROOF.AP.sp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.sp)
   def AP.sp(n: Nat, d: Nat) -> {Word.shl.put(n, False{}, AP.pw(n, d)) == AP.pw(n, 1n+d) : Word(n)}:
  PROOF.AP.shl_put (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.shl_put)
   def AP.shl_put(n: Nat, w: Word(n)) -> {Word.shl(n, w) == Word.shl.put(n, False{}, w) : Word(n)}:
  PROOF.AP.shln_pw (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.shln_pw)
   # shln(1, d) is 2^d
   def AP.shln_pw(d: Nat) -> {U32.shln(1, d) == U32{AP.pw(32n, d)} : U32}:
  PROOF.AP.padz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.padz)
   def AP.padz(n: Nat) -> {Word.shr.pad(n, Word.zero(n)) == Word.zero(1n+n) : Word(1n+n)}:
  PROOF.AP.padp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.padp)
   def AP.padp(n: Nat, d: Nat, h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.shr.pad(n, AP.pw(n, d)) == AP.pw(1n+n, d) : Word(1n+n)}:
  PROOF.AP.shr_pw (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.shr_pw)
   def AP.shr_pw(n: Nat, d: Nat, h: {Nat.is_lt(1n+d, n) == True{} : Bool}) -> {Word.shr(n, AP.pw(n, 1n+d)) == AP.pw(n, d) : Word(n)}:
  PROOF.AP.pw_shln (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.pw_shln)
   def AP.pw_shln(+d: Nat) -> {U32{AP.pw(32n, d)} == U32.shln(1, d) : U32}:
  PROOF.AP.shr_shln (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.shr_shln)
   # halving 2^(d+1) gives 2^d (below 2^32)
   def AP.shr_shln(+d: Nat, h: {Nat.is_lt(1n+d, 32n) == True{} : Bool}) -> {U32.shr(U32.shln(1, 1n+d)) == U32.shln(1, d) : U32}:
  PROOF.AP.val_pw (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.val_pw)
   def AP.val_pw(n: Nat, d: Nat, h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.to_nat(n, AP.pw(n, d)) == A.Arrays.slots(d) : Nat}:
  PROOF.AP.val_shln (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.val_shln)
   def AP.val_shln(+d: Nat, h: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.shln(1, d)) == A.Arrays.slots(d) : Nat}:
  PROOF.AP.z1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.z1)
   def AP.z1(n: Nat) -> {Word.adc(n, Word.zero(n), Word.zero(n), True{}, True{}) == Word.zero(n) : Word(n)}:
  PROOF.AP.z2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.z2)
   def AP.z2(n: Nat, d: Nat) -> {Word.adc(n, AP.pw(n, d), Word.zero(n), True{}, False{}) == AP.lm(n, d) : Word(n)}:
  PROOF.AP.sub_one (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.sub_one)
   def AP.sub_one(n: Nat, d: Nat) -> {Word.sub(n, AP.pw(n, d), AP.pw(n, 0n)) == AP.lm(n, d) : Word(n)}:
  PROOF.AP.mask_lm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.mask_lm)
   def AP.mask_lm(+d: Nat) -> {U32.sub(U32.shln(1, d), 1) == U32{AP.lm(32n, d)} : U32}:
  PROOF.AP.Tree (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.Tree)
   type AP.Tree<-T: Data> is Data:
     APLeaf{value: T}
     APNode{xs: AP.Tree<T>, ys: AP.Tree<T>}
  PROOF.AP.build (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.build)
   def AP.build(-T: Data, t: AP.Tree<T>) -> Array<T>:
  PROOF.AP.reflect.node (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.reflect.node)
   def AP.reflect.node(-T: Data, -tx: AP.Tree<T>, -ty: AP.Tree<T>, -xs: Array<T>, -ys: Array<T>, ex: {AP.build(T, tx) == xs : Array<T>}, ey: {AP.build(T, ty) == ys : Array<T>}) -> {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{xs, ys} : Array<T>}:
  PROOF.AP.reflect.join (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.reflect.join)
   def AP.reflect.join(-T: Data, -xs: Array<T>, -ys: Array<T>, rx: &t: AP.Tree<T> -> {AP.build(T, t) == xs : Array<T>}, ry: &t: AP.Tree<T> -> {AP.build(T, t) == ys : Array<T>}) -> &t: AP.Tree<T> -> {AP.build(T, t) == ANode{xs, ys} : Array<T>}:
  PROOF.AP.reflect (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.reflect)
   def AP.reflect(-T: Data, a: Array<T>) -> &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}:
  PROOF.AP.and_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.and_l)
   def AP.and_l(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
  PROOF.AP.and_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.and_r)
   def AP.and_r(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
  PROOF.AP.size (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.size)
   def AP.size(-T: Data, t: AP.Tree<T>) -> U32:
  PROOF.AP.swap_t (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.swap_t)
   def AP.swap_t(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> AP.Tree<T>:
  PROOF.AP.swap_v (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.swap_v)
   def AP.swap_v(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> T:
  PROOF.AP.get_v (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.get_v)
   def AP.get_v(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, z: Bool) -> T:
  PROOF.AP.mask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.mask)
   def AP.mask(+n: U32, i: U32) -> U32:
  PROOF.AP.z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.z)
   def AP.z(+n: U32, +j: U32) -> Bool:
More: https://jend.leeeet.dev/packages/bend-osdev-array.txt?definitions_offset=100