def perm_move

bend-mathlib@0.8.1.0 · perm.bend:122

import Base
import bendlib-kernel-list@1.0.0.0/list.bend as K

122# Moving an element from the middle to the front is a permutation.
123def perm_move(-A: Data, +xs: List<&2, A>, +y: A, +t: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, y <> t), y <> List.append(&2, A, xs, t)):
124  match xs:
125    case Nil{}:
126      perm_refl(A, y <> t)
127    case +x <> r:
128      perm_trans(A, x <> List.append(&2, A, r, y <> t), x <> y <> List.append(&2, A, r, t), y <> x <> List.append(&2, A, r, t), perm_cons(A, x, List.append(&2, A, r, y <> t), y <> List.append(&2, A, r, t), perm_move(A, r, y, t)), perm_swap(A, x, y, List.append(&2, A, r, t)))