law aw_eq
lawful-bytes@0.1.1.0 · proof_fast_append.bend:405
import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend
import Base
import lawful-bytes@0.1.1.0/fast.bend as FA
import lawful-arrays@0.1.0.0/proof_tree.bend as P
405law aw_eq:
406 for +n: Nat
407 for +ts: P.Tree<U32>
408 for +p: U32
409 for +lo: U32
410 for +td: P.Tree<U32>
411 for +si: U32
412 for +di: U32
413 for +sh: Nat
414 {FA.append.words(n, Array.get(U32, P.fromT(U32, ts), p), lo, P.fromT(U32, td), si, di, sh) == (P.fromT(U32, AWT(n, ts, p, lo, td, si, di, sh)), P.fromT(U32, ts)) : Array<U32> & Array<U32>}