def split_perm

bend-mathlib@0.8.1.0 · perm.bend:213

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

213# Splitting into evens and odds is a permutation.
214def split_perm(-A: Data, +xs: List<&2, A>) -> K.perm(A, xs, List.append(&2, A, evens(A, xs), odds(A, xs))):
215  match xs:
216    case Nil{}:
217      perm_refl(A, Nil{})
218    case +x <> r:
219      match r:
220        case Nil{}:
221          perm_refl(A, x <> Nil{})
222        case +y <> t:
223          perm_cons(A, x, y <> t, List.append(&2, A, evens(A, t), y <> odds(A, t)), perm_trans(A, y <> t, y <> List.append(&2, A, evens(A, t), odds(A, t)), List.append(&2, A, evens(A, t), y <> odds(A, t)), perm_cons(A, y, t, List.append(&2, A, evens(A, t), odds(A, t)), split_perm(A, t)), perm_move_rev(A, evens(A, t), y, odds(A, t))))