def AP.swap_size

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

import Base

655def AP.swap_size(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> {AP.size(T, AP.swap_t(T, t, n, i, v, z)) == AP.size(T, t) : U32}:
656  match t z:
657    case APLeaf{x} _:
658      {==}
659    case APNode{xs, ys} True{}:
660      +h = U32.shr(n)
661      +z1 = U32.is_lt(i, U32.shr(h))
662      %Equal.sym(U32, AP.size(T, AP.swap_t(T, xs, h, i, v, z1)), AP.size(T, xs), AP.swap_size(T, xs, h, i, v, z1)) : {U32.shl(_) == U32.shl(AP.size(T, xs)) : U32}
663      {==}
664    case APNode{xs, ys} False{}:
665      {==}