(STRATEGY
    INNERMOST)

(VAR
    I P V V1 V2 X X1 X2 Y Z)
(DATATYPES
    A = µX.< __(X, X), nil, tt, isList(X), isNeList(X), isPal(X), a, e, i, o, u, and(X, X), isQid(X), isNePal(X) >)
(SIGNATURES
    a____ :: [A x A] -> A
    a__and :: [A x A] -> A
    a__isList :: [A] -> A
    a__isNeList :: [A] -> A
    a__isNePal :: [A] -> A
    a__isPal :: [A] -> A
    a__isQid :: [A] -> A
    mark :: [A] -> A)
(RULES
    a____(__(X,Y),Z) ->
      a____(mark(X)
           ,a____(mark(Y),mark(Z)))
    a____(X,nil()) -> mark(X)
    a____(nil(),X) -> mark(X)
    a__and(tt(),X) -> mark(X)
    a__isList(V) -> a__isNeList(V)
    a__isList(nil()) -> tt()
    a__isList(__(V1,V2)) ->
      a__and(a__isList(V1),isList(V2))
    a__isNeList(V) -> a__isQid(V)
    a__isNeList(__(V1,V2)) ->
      a__and(a__isList(V1)
            ,isNeList(V2))
    a__isNeList(__(V1,V2)) ->
      a__and(a__isNeList(V1)
            ,isList(V2))
    a__isNePal(V) -> a__isQid(V)
    a__isNePal(__(I,__(P,I))) ->
      a__and(a__isQid(I),isPal(P))
    a__isPal(V) -> a__isNePal(V)
    a__isPal(nil()) -> tt()
    a__isQid(a()) -> tt()
    a__isQid(e()) -> tt()
    a__isQid(i()) -> tt()
    a__isQid(o()) -> tt()
    a__isQid(u()) -> tt()
    mark(__(X1,X2)) ->
      a____(mark(X1),mark(X2))
    mark(and(X1,X2)) ->
      a__and(mark(X1),X2)
    mark(isList(X)) -> a__isList(X)
    mark(isNeList(X)) ->
      a__isNeList(X)
    mark(isQid(X)) -> a__isQid(X)
    mark(isNePal(X)) ->
      a__isNePal(X)
    mark(isPal(X)) -> a__isPal(X)
    mark(nil()) -> nil()
    mark(tt()) -> tt()
    mark(a()) -> a()
    mark(e()) -> e()
    mark(i()) -> i()
    mark(o()) -> o()
    mark(u()) -> u()
    a____(X1,X2) -> __(X1,X2)
    a__and(X1,X2) -> and(X1,X2)
    a__isList(X) -> isList(X)
    a__isNeList(X) -> isNeList(X)
    a__isQid(X) -> isQid(X)
    a__isNePal(X) -> isNePal(X)
    a__isPal(X) -> isPal(X))