(VAR x y z)
(RULES
  *(x,*(y,z)) -> *(*(x,y),z)
  *(*(x,y),z) -> *(x,*(y,z))

  eq(x,y)           -> eq(y,x)
  eq(a,a)           -> T
  eq(a,*(x,y))      -> F
  eq(*(a,x),*(a,y)) -> eq(x,y)

  rep(0,x)      -> nil
  rep(s(x),y)   -> *(x,rep(x,y))
  hd(*(c(x),y)) -> x
  lt(*(x,c(y))) -> y
  tl(*(c(x),y)) -> y
  lem1(x)       -> eq(*(hd(x),tl(x)), x)
  lem2(*(x,y))  -> eq(lt(*(x,y)), lt(tl(*(x,y))))

  +(x,y)      -> +(y,x)
  +(+(x,y),z) -> +(x,+(y,z))
  +(0,x) -> x
  +(s(x),y) -> s(+(x,y))
)
(COMMENT
  proof score in CafeOBJ
)