def swap_w.lo

lawful-arrays@0.1.0.0 · proof_shape.bend:92

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

92def swap_w.lo(-T: Type, -xs: Array<T>, ys: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
93  w: SwapW(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n))), B.pred(d))) ->
94  SwapW(T, ANode{xs, ys}, n, i, v, True{}, d):
95  match d:
96    case 0n:
97      (na, old, e, q) = w
98      (ANode{na, ys}, old,
99        lo_eq(T, ys, Array.swap.go(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))), na, old, e), {==})
100    case 1n+p:
101      (na, old, e, q) = w
102      (ANode{na, ys}, old,
103        lo_eq(T, ys, Array.swap.go(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))), na, old, e),
104        and_eq_l(D.full(T, na, p), D.full(T, xs, p), D.full(T, ys, p), q))