def swap_w.hi

lawful-arrays@0.1.0.0 · proof_shape.bend:106

import Base
import lawful-arrays@0.1.0.0/defs.bend as D
import lawful-arrays@0.1.0.0/proof_base.bend as B

106def swap_w.hi(-T: Type, xs: Array<T>, -ys: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
107  w: SwapW(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v, U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n))), B.pred(d))) ->
108  SwapW(T, ANode{xs, ys}, n, i, v, False{}, d):
109  match d:
110    case 0n:
111      (na, old, e, q) = w
112      (ANode{xs, na}, old,
113        hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v,
114          U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e), {==})
115    case 1n+p:
116      (na, old, e, q) = w
117      (ANode{xs, na}, old,
118        hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v,
119          U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e),
120        and_eq_r(D.full(T, xs, p), D.full(T, na, p), D.full(T, ys, p), q))