Alphabet

nil:list
cons:[nat × list] ⟶ list
+:[nat × nat] ⟶ nat
map:[nat → nat × list] ⟶ list
ps:[list] ⟶ list

Variables

x:nat
xs:list
F:nat → nat

Rules

map(F, nil)⇒nil
map(F, cons(x, xs))⇒cons(F · x, map(F, xs))
ps(nil)⇒nil
ps(cons(x, xs))⇒cons(x, ps(map(λy:nat.+(x, y), xs)))