YES Problem: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Proof: DP Processor: DPs: eq#(s(x),s(y)) -> eq#(x,y) main#(phi) -> ver#(phi,nil()) in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Usable Rule Processor: DPs: eq#(s(x),s(y)) -> eq#(x,y) main#(phi) -> ver#(phi,nil()) in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) TRS: f23(x,y) -> x f23(x,y) -> y in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) not(tt()) -> ff() not(ff()) -> tt() ADG Processor: DPs: eq#(s(x),s(y)) -> eq#(x,y) main#(phi) -> ver#(phi,nil()) in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) TRS: f23(x,y) -> x f23(x,y) -> y in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) not(tt()) -> ff() not(ff()) -> tt() graph: in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) in#(x,cons(a,l)) -> eq#(x,a) -> eq#(s(x),s(y)) -> eq#(x,y) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y) Restore Modifier: DPs: eq#(s(x),s(y)) -> eq#(x,y) main#(phi) -> ver#(phi,nil()) in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) SCC Processor: #sccs: 3 #rules: 6 #arcs: 41/196 DPs: ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Matrix Interpretation Processor: dimension: 1 interpretation: [ver#](x0, x1) = x0, [Exists](x0, x1) = x1, [Not](x0) = x0, [Or](x0, x1) = x0 + x1 + 1, [t] = 1, [Var](x0) = x0 + 1, [cons](x0, x1) = 0, [in](x0, x1) = 1, [ver](x0, x1) = x0 + x1, [nil] = 0, [main](x0) = x0, [s](x0) = 0, [eq](x0, x1) = 0, [0] = 0, [or](x0, x1) = x1, [ff] = 0, [not](x0) = x0, [tt] = 0 orientation: ver#(Exists(n,phi),t()) = phi >= phi = ver#(phi,t()) ver#(Not(phi),t()) = phi >= phi = ver#(phi,t()) ver#(Or(phi,psi),t()) = phi + psi + 1 >= phi = ver#(phi,t()) ver#(Or(phi,psi),t()) = phi + psi + 1 >= psi = ver#(psi,t()) not(tt()) = 0 >= 0 = ff() not(ff()) = 0 >= 0 = tt() or(tt(),x) = x >= 0 = tt() or(ff(),x) = x >= x = x eq(0(),0()) = 0 >= 0 = tt() eq(s(x),0()) = 0 >= 0 = ff() eq(0(),s(y)) = 0 >= 0 = ff() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) main(phi) = phi >= phi = ver(phi,nil()) in(x,nil()) = 1 >= 0 = ff() in(x,cons(a,l)) = 1 >= 1 = or(eq(x,a),in(x,l)) ver(Var(x),t()) = x + 2 >= 1 = in(x,t()) ver(Or(phi,psi),t()) = phi + psi + 2 >= psi + 1 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = phi + 1 >= phi + 1 = not(ver(phi,t())) ver(Exists(n,phi),t()) = phi + 1 >= phi + 1 = or(ver(phi,cons(n,t())),ver(phi,t())) problem: DPs: ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Matrix Interpretation Processor: dimension: 1 interpretation: [ver#](x0, x1) = x0 + 1, [Exists](x0, x1) = x1, [Not](x0) = x0 + 1, [Or](x0, x1) = 0, [t] = 0, [Var](x0) = 0, [cons](x0, x1) = 0, [in](x0, x1) = 0, [ver](x0, x1) = 0, [nil] = 0, [main](x0) = 0, [s](x0) = 0, [eq](x0, x1) = 0, [0] = 0, [or](x0, x1) = x1, [ff] = 0, [not](x0) = 0, [tt] = 0 orientation: ver#(Exists(n,phi),t()) = phi + 1 >= phi + 1 = ver#(phi,t()) ver#(Not(phi),t()) = phi + 2 >= phi + 1 = ver#(phi,t()) not(tt()) = 0 >= 0 = ff() not(ff()) = 0 >= 0 = tt() or(tt(),x) = x >= 0 = tt() or(ff(),x) = x >= x = x eq(0(),0()) = 0 >= 0 = tt() eq(s(x),0()) = 0 >= 0 = ff() eq(0(),s(y)) = 0 >= 0 = ff() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) main(phi) = 0 >= 0 = ver(phi,nil()) in(x,nil()) = 0 >= 0 = ff() in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l)) ver(Var(x),t()) = 0 >= 0 = in(x,t()) ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t())) ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t())) problem: DPs: ver#(Exists(n,phi),t()) -> ver#(phi,t()) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Matrix Interpretation Processor: dimension: 1 interpretation: [ver#](x0, x1) = x0, [Exists](x0, x1) = x1 + 1, [Not](x0) = 0, [Or](x0, x1) = 0, [t] = 0, [Var](x0) = 0, [cons](x0, x1) = 0, [in](x0, x1) = 0, [ver](x0, x1) = 0, [nil] = 0, [main](x0) = 0, [s](x0) = 0, [eq](x0, x1) = 0, [0] = 0, [or](x0, x1) = x1, [ff] = 0, [not](x0) = 0, [tt] = 0 orientation: ver#(Exists(n,phi),t()) = phi + 1 >= phi = ver#(phi,t()) not(tt()) = 0 >= 0 = ff() not(ff()) = 0 >= 0 = tt() or(tt(),x) = x >= 0 = tt() or(ff(),x) = x >= x = x eq(0(),0()) = 0 >= 0 = tt() eq(s(x),0()) = 0 >= 0 = ff() eq(0(),s(y)) = 0 >= 0 = ff() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) main(phi) = 0 >= 0 = ver(phi,nil()) in(x,nil()) = 0 >= 0 = ff() in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l)) ver(Var(x),t()) = 0 >= 0 = in(x,t()) ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t())) ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t())) problem: DPs: TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Qed DPs: in#(x,cons(a,l)) -> in#(x,l) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Matrix Interpretation Processor: dimension: 1 interpretation: [in#](x0, x1) = x1 + 1, [Exists](x0, x1) = 0, [Not](x0) = 0, [Or](x0, x1) = 0, [t] = 0, [Var](x0) = 0, [cons](x0, x1) = x1 + 1, [in](x0, x1) = 0, [ver](x0, x1) = x1, [nil] = 0, [main](x0) = 0, [s](x0) = 0, [eq](x0, x1) = 0, [0] = 0, [or](x0, x1) = x1, [ff] = 0, [not](x0) = 0, [tt] = 0 orientation: in#(x,cons(a,l)) = l + 2 >= l + 1 = in#(x,l) not(tt()) = 0 >= 0 = ff() not(ff()) = 0 >= 0 = tt() or(tt(),x) = x >= 0 = tt() or(ff(),x) = x >= x = x eq(0(),0()) = 0 >= 0 = tt() eq(s(x),0()) = 0 >= 0 = ff() eq(0(),s(y)) = 0 >= 0 = ff() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) main(phi) = 0 >= 0 = ver(phi,nil()) in(x,nil()) = 0 >= 0 = ff() in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l)) ver(Var(x),t()) = 0 >= 0 = in(x,t()) ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t())) ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t())) problem: DPs: TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Qed DPs: eq#(s(x),s(y)) -> eq#(x,y) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Matrix Interpretation Processor: dimension: 1 interpretation: [eq#](x0, x1) = x1 + 1, [Exists](x0, x1) = 0, [Not](x0) = 0, [Or](x0, x1) = 0, [t] = 0, [Var](x0) = 0, [cons](x0, x1) = 0, [in](x0, x1) = 0, [ver](x0, x1) = 0, [nil] = 0, [main](x0) = 0, [s](x0) = x0 + 1, [eq](x0, x1) = 0, [0] = 0, [or](x0, x1) = x1, [ff] = 0, [not](x0) = 0, [tt] = 0 orientation: eq#(s(x),s(y)) = y + 2 >= y + 1 = eq#(x,y) not(tt()) = 0 >= 0 = ff() not(ff()) = 0 >= 0 = tt() or(tt(),x) = x >= 0 = tt() or(ff(),x) = x >= x = x eq(0(),0()) = 0 >= 0 = tt() eq(s(x),0()) = 0 >= 0 = ff() eq(0(),s(y)) = 0 >= 0 = ff() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) main(phi) = 0 >= 0 = ver(phi,nil()) in(x,nil()) = 0 >= 0 = ff() in(x,cons(a,l)) = 0 >= 0 = or(eq(x,a),in(x,l)) ver(Var(x),t()) = 0 >= 0 = in(x,t()) ver(Or(phi,psi),t()) = 0 >= 0 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = 0 >= 0 = not(ver(phi,t())) ver(Exists(n,phi),t()) = 0 >= 0 = or(ver(phi,cons(n,t())),ver(phi,t())) problem: DPs: TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Qed