(STRATEGY
    INNERMOST)

(VAR
    x1 x2 x3 x4 x5)
(DATATYPES
    A = µX.< s(X), 0 >)
(SIGNATURES
    f :: [A x A x A x A x A] -> A)
(RULES
    f(s(x1),x2,x3,x4,x5) -> f(x1
                             ,x2
                             ,x3
                             ,x4
                             ,x5)
    f(0(),s(x2),x3,x4,x5) -> f(x2
                              ,x2
                              ,x3
                              ,x4
                              ,x5)
    f(0(),0(),s(x3),x4,x5) -> f(x3
                               ,x3
                               ,x3
                               ,x4
                               ,x5)
    f(0(),0(),0(),s(x4),x5) -> f(x4
                                ,x4
                                ,x4
                                ,x4
                                ,x5)
    f(0(),0(),0(),0(),s(x5)) -> f(x5
                                 ,x5
                                 ,x5
                                 ,x5
                                 ,x5)
    f(0(),0(),0(),0(),0()) -> 0())