law sz_sw

lawful-arrays@0.1.0.0 · proof_tree.bend:312

import Base

312# A swap keeps the left spine, so the size.
313law sz_sw:
314  for -T: Data
315  for +t: Tree<T>
316  for +n: U32
317  for +i: U32
318  for +v: T
319  for +z: Bool
320  {Array.size(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, t), n, i, v, z)))
321    == (Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, t), n, i, v, z)),
322        Pair.snd(Array<T>, U32, Array.size(T, fromT(T, t)))) : Array<T> & U32}