def swap_m_occ

bend-collections-laws-math@1.0.0.0 · proofs/math/random/shuffle.bend:87

import Base
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R

87def swap_m_occ(~A: Data, ~V: Data, ~rel: A -> V -> Bool, +v: V, +xs: List<&2, A>, +i: Nat, +j: Nat, +a: Maybe<&2, A>, +b: Maybe<&2, A>, +ha: {R.nth(A, xs, i) == a : Maybe<&2, A>}, +hb: {R.nth(A, xs, j) == b : Maybe<&2, A>}) -> {occ(~A, ~V, ~rel, v, R.swap_m(A, xs, i, j, a, b)) == occ(~A, ~V, ~rel, v, xs) : Nat}:
88  match a b:
89    case Some{x} Some{y}:
90      swap_some(~A, ~V, ~rel, v, xs, i, j, x, y, ha, hb)
91    case None{} _:
92      {==}
93    case Some{x} None{}:
94      {==}