law wl_set

lawful-bytes@0.1.1.0 · proof_core.bend:464

import Base
import lawful-arrays@0.1.0.0/defs.bend as A
import lawful-arrays@0.1.0.0/proof_tree.bend as P
import lawful-arrays@0.1.0.0/proof_index.bend as I

464# Writing word k (in range) sets the k-th of the word list.
465law wl_set:
466  for +t: P.Tree<U32>
467  for +d: Nat
468  for +k: U32
469  for +w: U32
470  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
471  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
472  for +hk: {Nat.is_lt(U32.to_nat(k), Nat.pow(2n, d)) == True{} : Bool}
473  {WL(I.set_tree(U32, t, k, w)) == List.set(&2, U32, WL(t), U32.to_nat(k), w) : List<&2, U32>}