(STRATEGY
    INNERMOST)

(VAR
    h in_2 in_3 m n pid st_1 st_2
    st_3 t x)
(DATATYPES
    A = µX.< 0, nil, s(X), cons(X, X), true, false, f(X, X), two, three >)
(SIGNATURES
    fstsplit :: [A x A] -> A
    sndsplit :: [A x A] -> A
    empty :: [A] -> A
    leq :: [A x A] -> A
    length :: [A] -> A
    app :: [A x A] -> A
    map_f :: [A x A] -> A
    head :: [A] -> A
    tail :: [A] -> A
    ring :: [A x A x A x A x A x A] -> A
    if_1 :: [A x A x A x A x A x A x A] -> A
    if_2 :: [A x A x A x A x A x A x A] -> A
    if_3 :: [A x A x A x A x A x A x A] -> A
    if_4 :: [A x A x A x A x A x A x A] -> A
    if_5 :: [A x A x A x A x A x A x A] -> A
    if_6 :: [A x A x A x A x A x A x A] -> A
    if_7 :: [A x A x A x A x A x A x A] -> A
    if_8 :: [A x A x A x A x A x A x A] -> A
    if_9 :: [A x A x A x A x A x A x A] -> A)
(RULES
    fstsplit(0(),x) -> nil()
    fstsplit(s(n),nil()) -> nil()
    fstsplit(s(n),cons(h,t)) ->
      cons(h,fstsplit(n,t))
    sndsplit(0(),x) -> x
    sndsplit(s(n),nil()) -> nil()
    sndsplit(s(n),cons(h,t)) ->
      sndsplit(n,t)
    empty(nil()) -> true()
    empty(cons(h,t)) -> false()
    leq(0(),m) -> true()
    leq(s(n),0()) -> false()
    leq(s(n),s(m)) -> leq(n,m)
    length(nil()) -> 0()
    length(cons(h,t)) ->
      s(length(t))
    app(nil(),x) -> x
    app(cons(h,t),x) -> cons(h
                            ,app(t,x))
    map_f(pid,nil()) -> nil()
    map_f(pid,cons(h,t)) ->
      app(f(pid,h),map_f(pid,t))
    head(cons(h,t)) -> h
    tail(cons(h,t)) -> t
    ring(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m) -> if_1(st_1
                   ,in_2
                   ,st_2
                   ,in_3
                   ,st_3
                   ,m
                   ,empty(fstsplit(m,st_1)))
    if_1(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,false()) -> ring(sndsplit(m
                                  ,st_1)
                         ,cons(fstsplit(m,st_1),in_2)
                         ,st_2
                         ,in_3
                         ,st_3
                         ,m)
    ring(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m) -> if_2(st_1
                   ,in_2
                   ,st_2
                   ,in_3
                   ,st_3
                   ,m
                   ,leq(m,length(st_2)))
    if_2(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,true()) -> if_3(st_1
                        ,in_2
                        ,st_2
                        ,in_3
                        ,st_3
                        ,m
                        ,empty(fstsplit(m,st_2)))
    if_3(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,false()) -> ring(st_1
                         ,in_2
                         ,sndsplit(m,st_2)
                         ,cons(fstsplit(m,st_2),in_3)
                         ,st_3
                         ,m)
    if_2(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,false()) -> if_4(st_1
                         ,in_2
                         ,st_2
                         ,in_3
                         ,st_3
                         ,m
                         ,empty(fstsplit(m
                                        ,app(map_f(two(),head(in_2))
                                            ,st_2))))
    if_4(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,false()) -> ring(st_1
                         ,tail(in_2)
                         ,sndsplit(m
                                  ,app(map_f(two(),head(in_2))
                                      ,st_2))
                         ,cons(fstsplit(m
                                       ,app(map_f(two(),head(in_2))
                                           ,st_2))
                              ,in_3)
                         ,st_3
                         ,m)
    ring(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m) -> if_5(st_1
                   ,in_2
                   ,st_2
                   ,in_3
                   ,st_3
                   ,m
                   ,empty(map_f(two(),head(in_2))))
    if_5(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,true()) -> ring(st_1
                        ,tail(in_2)
                        ,st_2
                        ,in_3
                        ,st_3
                        ,m)
    ring(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m) -> if_6(st_1
                   ,in_2
                   ,st_2
                   ,in_3
                   ,st_3
                   ,m
                   ,leq(m,length(st_3)))
    if_6(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,true()) -> if_7(st_1
                        ,in_2
                        ,st_2
                        ,in_3
                        ,st_3
                        ,m
                        ,empty(fstsplit(m,st_3)))
    if_7(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,false()) -> ring(st_1
                         ,in_2
                         ,st_2
                         ,in_3
                         ,sndsplit(m,st_3)
                         ,m)
    if_6(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,false()) -> if_8(st_1
                         ,in_2
                         ,st_2
                         ,in_3
                         ,st_3
                         ,m
                         ,empty(fstsplit(m
                                        ,app(map_f(three(),head(in_3))
                                            ,st_3))))
    if_8(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,false()) -> ring(st_1
                         ,in_2
                         ,st_2
                         ,tail(in_3)
                         ,sndsplit(m
                                  ,app(map_f(three(),head(in_3))
                                      ,st_3))
                         ,m)
    ring(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m) -> if_9(st_1
                   ,in_2
                   ,st_2
                   ,in_3
                   ,st_3
                   ,m
                   ,empty(map_f(three()
                               ,head(in_3))))
    if_9(st_1
        ,in_2
        ,st_2
        ,in_3
        ,st_3
        ,m
        ,true()) -> ring(st_1
                        ,in_2
                        ,st_2
                        ,tail(in_3)
                        ,st_3
                        ,m))