MAYBE 0.09/0.18 MAYBE 0.09/0.18 0.09/0.18 Problem: 0.09/0.18 U11(tt(),V2) -> U12(isNat(activate(V2))) 0.09/0.18 U12(tt()) -> tt() 0.09/0.18 U21(tt()) -> tt() 0.09/0.18 U31(tt(),N) -> activate(N) 0.09/0.18 U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N)) 0.09/0.18 U42(tt(),M,N) -> s(plus(activate(N),activate(M))) 0.09/0.18 isNat(n__0()) -> tt() 0.09/0.18 isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2)) 0.09/0.18 isNat(n__s(V1)) -> U21(isNat(activate(V1))) 0.09/0.18 plus(N,0()) -> U31(isNat(N),N) 0.09/0.18 plus(N,s(M)) -> U41(isNat(M),M,N) 0.09/0.18 0() -> n__0() 0.09/0.18 plus(X1,X2) -> n__plus(X1,X2) 0.09/0.18 s(X) -> n__s(X) 0.09/0.18 activate(n__0()) -> 0() 0.09/0.18 activate(n__plus(X1,X2)) -> plus(X1,X2) 0.09/0.18 activate(n__s(X)) -> s(X) 0.09/0.18 activate(X) -> X 0.09/0.18 0.09/0.18 Proof: 0.09/0.18 Open 0.09/0.18 EOF