def AP.new_leaves.go

bend-osdev-array@0.1.0.1 · PROOF.bend:1261

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

1261def AP.new_leaves.go(-T: Data, +d: Nat, +v: T) -> {A.Arrays.leaves(T, Array.new(T, d, v)) == List.replicate(T, A.Arrays.slots(d), v) : List<&2, T>}:
1262  match d:
1263    case 0n:
1264      {==}
1265    case 1n+ +p:
1266      +s = A.Arrays.slots(p)
1267      %Equal.sym(List<&2, T>, A.Arrays.leaves(T, Array.new(T, p, v)), List.replicate(T, s, v), AP.new_leaves.go(T, p, v)) : {List.append(&2, T, _, _) == List.replicate(T, Nat.double(s), v) : List<&2, T>}
1268      %Equal.sym(Nat, Nat.double(s), Nat.add(s, s), UL.nat_double(s)) : {List.append(&2, T, List.replicate(T, s, v), List.replicate(T, s, v)) == List.replicate(T, _, v) : List<&2, T>}
1269      Equal.sym(List<&2, T>, List.replicate(T, Nat.add(s, s), v), List.append(&2, T, List.replicate(T, s, v), List.replicate(T, s, v)), AP.rep_add(T, s, s, v))