def upd_slots

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:205

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

205def upd_slots(-T: Data, +d: Nat, +t: Tree<T>, +j: Nat, +v: T, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {slots(T, upd(T, d, t, j, v)) == SC.update(T, slots(T, t), j, v) : List<&2, T>}:
206  tupd_slots(T, d, t, j, v, hj, ndec(d, j), {==}, pf)