def set

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

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

312def set(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.set(T, thaw(T, t), i, v) == thaw(T, upd(T, d, t, U32.to_nat(i), v)) : Array<T>}:
313  %Equal.sym(Array<T> & T, Array.swap(T, thaw(T, t), i, v), (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x), swap(T, d, t, i, v, x, hd, hi, hx, pf)) : {Array.set.fin(T, _) == thaw(T, upd(T, d, t, U32.to_nat(i), v)) : Array<T>}
314  {==}