mod NoBehaviors is inc NAT . sort List . op nil : -> List [ctor] . subsort Nat < List . op _::_ : List List -> List [ctor assoc id: nil] . vars L L1 L2 L3 : List . var N : Nat . op genperm : List List List List -> List . rl genperm(N :: L, L1, L2, L3) => genperm(L, L1, L2, L3 :: N) . rl genperm(L, N :: L1, L2, L3) => genperm(L, L1, L2, L3 :: N) . rl genperm(L, L1, N :: L2, L3) => genperm(L, L1, L2, L3 :: N) . rl genperm(nil, nil, nil, L) => L . endm rew genperm(1 :: 2, 3 :: 4, 5 :: 6, nil) .