Alphabet

app:[list × list] ⟶ list
cons:[nat × list] ⟶ list
hshuffle:[nat → nat × list] ⟶ list
nil:list
reverse:[list] ⟶ list

Variables

X:list
Y:nat
U:list
V:list
W:nat
P:list
F1:nat → nat
Z1:nat → nat
U1:nat
V1:list

Rules

app(nil, X)⇒X
app(cons(Y, U), V)⇒cons(Y, app(U, V))
reverse(nil)⇒nil
reverse(cons(W, P))⇒app(reverse(P), cons(W, nil))
hshuffle(F1, nil)⇒nil
hshuffle(Z1, cons(U1, V1))⇒cons(Z1 · U1, hshuffle(Z1, reverse(V1)))