def half_len_drop

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:181

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS

181def half_len_drop(+xs: List<&2,T.Out>, +g: Nat, +hl: {SC.length(T.Out,xs) == SC.pow2(1n+g) : Nat}) -> {SC.length(T.Out,SC.drop(T.Out,xs,SC.pow2(g))) == SC.pow2(g) : Nat}:
182  %Equal.sym(Nat,SC.length(T.Out,SC.drop(T.Out,xs,SC.pow2(g))),Nat.sub(SC.length(T.Out,xs),SC.pow2(g)),LS.length_drop(T.Out,xs,SC.pow2(g))) : {_ == SC.pow2(g) : Nat}
183  %Equal.sym(Nat,SC.length(T.Out,xs),SC.pow2(1n+g),hl) : {Nat.sub(_,SC.pow2(g)) == SC.pow2(g) : Nat}
184  LS.sub_double(SC.pow2(g))