def perm_append_comm

bend-mathlib@0.8.1.0 · perm.bend:169

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

169# Appending commutes up to permutation (derived without symmetry).
170def perm_append_comm(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, ys), List.append(&2, A, ys, xs)):
171  match xs:
172    case Nil{}:
173      (Nil{}, Equal.sym(List<&2, A>, List.append(&2, A, ys, Nil{}), ys, internal_append_nil(A, ys)))
174    case +x <> r:
175      perm_trans(A, x <> List.append(&2, A, r, ys), x <> List.append(&2, A, ys, r), List.append(&2, A, ys, x <> r), perm_cons(A, x, List.append(&2, A, r, ys), List.append(&2, A, ys, r), perm_append_comm(A, r, ys)), perm_move_rev(A, ys, x, r))