def trep_slots

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
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/lib/lemmas/proofs/nat_algebra.bend as NA

124def trep_slots(-T: Data, +d: Nat, +v: T) -> {slots(T, trep(T, d, v)) == SC.replicate(T, SC.pow2(d), v) : List<&2, T>}:
125  match d:
126    case 0n:
127      {==}
128    case 1n+p:
129      %Equal.sym(List<&2, T>, slots(T, trep(T, p, v)), SC.replicate(T, SC.pow2(p), v), trep_slots(T, p, v)) : {SC.append(T, _, _) == SC.replicate(T, Nat.double(SC.pow2(p)), v) : List<&2, T>}
130      %Equal.sym(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p))) : {SC.append(T, SC.replicate(T, SC.pow2(p), v), SC.replicate(T, SC.pow2(p), v)) == SC.replicate(T, _, v) : List<&2, T>}
131      LL.replicate_add(T, SC.pow2(p), SC.pow2(p), v)