NO 0.08/0.19 NO 0.08/0.19 0.08/0.19 Problem: 0.08/0.19 and(tt()) -> X 0.08/0.19 __(__(X,Y),Z) -> __(X,__(Y,Z)) 0.08/0.19 __(X,nil()) -> X 0.08/0.19 __(nil(),X) -> X 0.08/0.19 U11(tt()) -> U12(isNeList()) 0.08/0.19 U12(tt()) -> tt() 0.08/0.19 U21(tt()) -> U22(isList()) 0.08/0.19 U22(tt()) -> U23(isList()) 0.08/0.19 U23(tt()) -> tt() 0.08/0.19 U31(tt()) -> U32(isQid()) 0.08/0.19 U32(tt()) -> tt() 0.08/0.19 U41(tt()) -> U42(isList()) 0.08/0.19 U42(tt()) -> U43(isNeList()) 0.08/0.19 U43(tt()) -> tt() 0.08/0.19 U51(tt()) -> U52(isNeList()) 0.08/0.19 U52(tt()) -> U53(isList()) 0.08/0.19 U53(tt()) -> tt() 0.08/0.19 U61(tt()) -> U62(isQid()) 0.08/0.19 U62(tt()) -> tt() 0.08/0.19 U71(tt()) -> U72(isNePal()) 0.08/0.19 U72(tt()) -> tt() 0.08/0.19 isList() -> U11(isPalListKind()) 0.08/0.19 isList() -> tt() 0.08/0.19 isList() -> U21(and(isPalListKind())) 0.08/0.19 isNeList() -> U31(isPalListKind()) 0.08/0.19 isNeList() -> U41(and(isPalListKind())) 0.08/0.19 isNeList() -> U51(and(isPalListKind())) 0.08/0.19 isNePal() -> U61(isPalListKind()) 0.08/0.19 isNePal() -> and(and(isQid())) 0.08/0.19 isPal() -> U71(isPalListKind()) 0.08/0.19 isPal() -> tt() 0.08/0.19 isPalListKind() -> tt() 0.08/0.19 isPalListKind() -> and(isPalListKind()) 0.08/0.19 isQid() -> tt() 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Fresh Variable Processor: loop length: 1 0.08/0.19 terms: 0.08/0.19 and(tt()) 0.08/0.19 context: [] 0.08/0.19 substitution: 0.08/0.19 X -> and(tt()) 0.08/0.19 Qed 0.08/0.19 EOF