MAYBE 82.08/23.48 MAYBE 82.08/23.49 82.08/23.49 Problem: 82.08/23.49 __(__(X,Y),Z) -> __(X,__(Y,Z)) 82.08/23.49 __(X,nil()) -> X 82.08/23.49 __(nil(),X) -> X 82.08/23.49 U11(tt()) -> tt() 82.08/23.49 U21(tt(),V2) -> U22(isList(activate(V2))) 82.08/23.49 U22(tt()) -> tt() 82.08/23.49 U31(tt()) -> tt() 82.08/23.49 U41(tt(),V2) -> U42(isNeList(activate(V2))) 82.08/23.49 U42(tt()) -> tt() 82.08/23.49 U51(tt(),V2) -> U52(isList(activate(V2))) 82.08/23.49 U52(tt()) -> tt() 82.08/23.49 U61(tt()) -> tt() 82.08/23.49 U71(tt(),P) -> U72(isPal(activate(P))) 82.08/23.49 U72(tt()) -> tt() 82.08/23.49 U81(tt()) -> tt() 82.08/23.49 isList(V) -> U11(isNeList(activate(V))) 82.08/23.49 isList(n__nil()) -> tt() 82.08/23.49 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 82.08/23.49 isNeList(V) -> U31(isQid(activate(V))) 82.08/23.49 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 82.08/23.49 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 82.08/23.49 isNePal(V) -> U61(isQid(activate(V))) 82.08/23.49 isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) 82.08/23.49 isPal(V) -> U81(isNePal(activate(V))) 82.08/23.49 isPal(n__nil()) -> tt() 82.08/23.49 isQid(n__a()) -> tt() 82.08/23.49 isQid(n__e()) -> tt() 82.08/23.49 isQid(n__i()) -> tt() 82.08/23.49 isQid(n__o()) -> tt() 82.08/23.49 isQid(n__u()) -> tt() 82.08/23.49 nil() -> n__nil() 82.08/23.49 __(X1,X2) -> n____(X1,X2) 82.08/23.49 a() -> n__a() 82.08/23.49 e() -> n__e() 82.08/23.49 i() -> n__i() 82.08/23.49 o() -> n__o() 82.08/23.49 u() -> n__u() 82.08/23.49 activate(n__nil()) -> nil() 82.08/23.49 activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) 82.08/23.49 activate(n__a()) -> a() 82.08/23.49 activate(n__e()) -> e() 82.08/23.49 activate(n__i()) -> i() 82.08/23.49 activate(n__o()) -> o() 82.08/23.49 activate(n__u()) -> u() 82.08/23.49 activate(X) -> X 82.08/23.49 82.08/23.49 Proof: 82.08/23.49 Open 82.08/23.49 EOF