def AP.get_top_eq
bend-osdev-array@0.1.0.1 · PROOF.bend:639
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
639def AP.get_top_eq(-T: Data, +t: AP.Tree<T>, +i: U32) -> {Array.get(T, AP.build(T, t), i) == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}:
640 +n = AP.size(T, t)
641 +j = AP.mask(n, i)
642 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), n), AP.size_eq(T, t)) : {Array.get.at(T, i, _) == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}
643 %Equal.sym(Array<T> & T, Array.get.go(T, AP.build(T, t), n, j, AP.z(n, j)), (AP.build(T, t), AP.get_v(T, t, n, j, AP.z(n, j))), AP.get_eq(T, t, n, j, AP.z(n, j))) : {_ == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}
644 {==}