def perm_move_rev

bend-mathlib@0.8.1.0 · perm.bend:161

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

161# Moving the front element into the middle is a permutation.
162def perm_move_rev(-A: Data, +xs: List<&2, A>, +y: A, +t: List<&2, A>) -> K.perm(A, y <> List.append(&2, A, xs, t), List.append(&2, A, xs, y <> t)):
163  match xs:
164    case Nil{}:
165      perm_refl(A, y <> t)
166    case +x <> r:
167      perm_trans(A, y <> x <> List.append(&2, A, r, t), x <> y <> List.append(&2, A, r, t), x <> List.append(&2, A, r, y <> t), perm_swap(A, y, x, List.append(&2, A, r, t)), perm_cons(A, x, y <> List.append(&2, A, r, t), List.append(&2, A, r, y <> t), perm_move_rev(A, r, y, t)))