in nat.maude

fmod NAT-LIST is
   protecting NAT .

   sorts NeList List .
   subsort NeList < List .

   op [] : -> List .
   op _:_ : Nat List -> NeList .
   op tail : NeList -> List .
   op head : NeList -> Nat .
   op _++_ : List List -> List .
   op length : List -> Nat .
   op reverse : List -> List .
   op take_from_ : Nat List -> List .
   op throw_from_ : Nat List -> List .
   op from_to_ : Nat Nat -> List .

   vars N M : Nat .
   vars L L' : List .

   eq tail(N : L) = L .
   eq head(N : L) = N .
   eq [] ++ L = L .
   eq (N : L) ++ L' = N : (L ++ L') .
   eq length([]) = 0 .
   eq length(N : L) = s(0) + length(L) .
   eq reverse([]) = [] .
   eq reverse(N : L) = reverse(L) ++ (N : []) .

   eq take 0 from L = [] .
   eq take N from [] = [] .
   eq take s(N) from (M : L) = M : take N from L .
   eq throw 0 from L = L .
   eq throw N from [] = [] .
   eq throw s(N) from (M : L) = throw N from L  .
   ceq from N to M = [] if N > M .
   ceq from N to M = N : from s(N) to M if N <= M .
endfm

red reverse(
       (take length(from 0 to ((s(s(s(0))) * s(s(s(s(0))))) div s(s(0))))
        from (from 0 to (s(s(s(0))) * s(s(s(s(0)))))))
       ++
       (throw length(from 0 to ((s(s(s(0))) * s(s(s(s(0))))) div s(s(0))))
        from (from 0 to (s(s(s(0))) * s(s(s(s(0)))))))) .

***(
readable trace:

reverse(
  (take length(from 0 to ((3 * 4) div 2)) from (from 0 to (3 * 4))) 
  ++
  (throw length(from 0 to ((3 * 4) div 2)) from (from 0 to (3 * 4))))
-->
reverse(
  (take length(from 0 to 6) from (from 0 to 12)) 
  ++
  (throw length(from 0 to 6) from (from 0 to 12)))
-->
reverse(
  (take length(0 1 ... 6) from (0 1 ... 12)) 
  ++
  (throw length(0 1 ... 6) from (0 1 ... 12)))
-->
reverse((take 7 from (0 1 ... 12)) ++ (throw 7 from (0 1 ... 12)))
-->
reverse((0 1 ... 6) ++ (7 ... 12))
-->
reverse(0 1 ... 12)
-->
(12 11 ... 1 0)

reduce in NAT-LIST : reverse((take length(from 0 to ((s(s(
    s(0))) * s(s(s(s(0))))) div s(s(0)))) from from 0 to (s(s(s(
    0))) * s(s(s(s(0)))))) ++ throw length(from 0 to ((s(s(s(0)))
    * s(s(s(s(0))))) div s(s(0)))) from from 0 to (s(s(s(0))) * s(
    s(s(s(0)))))) .
rewrites: 599 in -10ms cpu (0ms real) (~ rewrites/second)
result NeList: s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) : s(s(s(s(s(
    s(s(s(s(s(s(0))))))))))) : s(s(s(s(s(s(s(s(s(s(0)))))))))) :
    s(s(s(s(s(s(s(s(s(0))))))))) : s(s(s(s(s(s(s(s(0)))))))) : s(
    s(s(s(s(s(s(0))))))) : s(s(s(s(s(s(0)))))) : s(s(s(s(s(0)))))
    : s(s(s(s(0)))) : s(s(s(0))) : s(s(0)) : s(0) : 0 : []
)