ProofShape.swap_w.lo: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape
Lines 92-104 of lawful-arrays@0.1.0.0/proof_shape.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&start_line=92&end_line=104

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

def swap_w.lo(-T: Type, -xs: Array<T>, ys: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
  w: SwapW(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n))), B.pred(d))) ->
  SwapW(T, ANode{xs, ys}, n, i, v, True{}, d):
  match d:
    case 0n:
      (na, old, e, q) = w
      (ANode{na, ys}, old,
        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), {==})
    case 1n+p:
      (na, old, e, q) = w
      (ANode{na, ys}, old,
        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),
        and_eq_l(D.full(T, na, p), D.full(T, xs, p), D.full(T, ys, p), q))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/defs.bend&name=full
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=pred
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=SwapW
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=and_eq_l
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=lo_eq