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())) TDG 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())) graph: 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)) -> in#(x,l) -> in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> 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#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,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()) -> 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#(Not(phi),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#(Or(phi,psi),t()) -> ver#(phi,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#(Var(x),t()) -> in#(x,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())) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Not(phi),t()) -> not#(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()) -> ver#(phi,cons(n,t())) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,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#(psi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Not(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#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,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#(Not(phi),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#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Var(x),t()) -> in#(x,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#(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()) -> 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#(Not(phi),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#(Or(phi,psi),t()) -> ver#(phi,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#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,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()) -> 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#(Not(phi),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#(Or(phi,psi),t()) -> ver#(phi,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#(Var(x),t()) -> in#(x,t()) ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> eq#(x,a) ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> in#(x,l) main#(phi) -> ver#(phi,nil()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Not(phi),t()) -> ver#(phi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Var(x),t()) -> in#(x,t()) eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y) EDG 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())) 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) 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())) Arctic Interpretation Processor: dimension: 1 interpretation: [ver#](x0, x1) = x0, [Exists](x0, x1) = 2x0 + 4x1 + 0, [Not](x0) = 4x0 + 0, [Or](x0, x1) = 4x0 + 3x1 + 0, [t] = 1, [Var](x0) = 4x0 + 3, [cons](x0, x1) = 4x0 + 4x1, [in](x0, x1) = x1, [ver](x0, x1) = 3x0 + 0, [nil] = 3, [main](x0) = 5x0 + 8, [s](x0) = 2x0 + 2, [eq](x0, x1) = x1, [0] = 1, [or](x0, x1) = 2x0 + 1x1, [ff] = 0, [not](x0) = 1, [tt] = 0 orientation: ver#(Exists(n,phi),t()) = 2n + 4phi + 0 >= phi = ver#(phi,t()) ver#(Not(phi),t()) = 4phi + 0 >= phi = ver#(phi,t()) ver#(Or(phi,psi),t()) = 4phi + 3psi + 0 >= phi = ver#(phi,t()) ver#(Or(phi,psi),t()) = 4phi + 3psi + 0 >= psi = ver#(psi,t()) not(tt()) = 1 >= 0 = ff() not(ff()) = 1 >= 0 = tt() or(tt(),x) = 1x + 2 >= 0 = tt() or(ff(),x) = 1x + 2 >= x = x eq(0(),0()) = 1 >= 0 = tt() eq(s(x),0()) = 1 >= 0 = ff() eq(0(),s(y)) = 2y + 2 >= 0 = ff() eq(s(x),s(y)) = 2y + 2 >= y = eq(x,y) main(phi) = 5phi + 8 >= 3phi + 0 = ver(phi,nil()) in(x,nil()) = 3 >= 0 = ff() in(x,cons(a,l)) = 4a + 4l >= 2a + 1l = or(eq(x,a),in(x,l)) ver(Var(x),t()) = 7x + 6 >= 1 = in(x,t()) ver(Or(phi,psi),t()) = 7phi + 6psi + 3 >= 5phi + 4psi + 2 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = 7phi + 3 >= 1 = not(ver(phi,t())) ver(Exists(n,phi),t()) = 5n + 7phi + 3 >= 5phi + 2 = 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: dim=1 interpretation: [in#](x0, x1) = 2x1, [Exists](x0, x1) = 3x0 + 4x1 + 4, [Not](x0) = 2, [Or](x0, x1) = 6x0 + 7x1 + 1, [t] = 0, [Var](x0) = 6x0 + 1, [cons](x0, x1) = 3x0 + 2x1 + 2, [in](x0, x1) = 4x1, [ver](x0, x1) = 4x0 + 3x1, [nil] = 2, [main](x0) = 5x0 + 6, [s](x0) = 4x0 + 2, [eq](x0, x1) = 6x1 + 4, [0] = 0, [or](x0, x1) = x0 + x1 + 4, [ff] = 2, [not](x0) = 4, [tt] = 0 orientation: in#(x,cons(a,l)) = 6a + 4l + 4 >= 2l = in#(x,l) not(tt()) = 4 >= 2 = ff() not(ff()) = 4 >= 0 = tt() or(tt(),x) = x + 4 >= 0 = tt() or(ff(),x) = x + 6 >= x = x eq(0(),0()) = 4 >= 0 = tt() eq(s(x),0()) = 4 >= 2 = ff() eq(0(),s(y)) = 24y + 16 >= 2 = ff() eq(s(x),s(y)) = 24y + 16 >= 6y + 4 = eq(x,y) main(phi) = 5phi + 6 >= 4phi + 6 = ver(phi,nil()) in(x,nil()) = 8 >= 2 = ff() in(x,cons(a,l)) = 12a + 8l + 8 >= 6a + 4l + 8 = or(eq(x,a),in(x,l)) ver(Var(x),t()) = 24x + 4 >= 0 = in(x,t()) ver(Or(phi,psi),t()) = 24phi + 28psi + 4 >= 4phi + 4psi + 4 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = 8 >= 4 = not(ver(phi,t())) ver(Exists(n,phi),t()) = 12n + 16phi + 16 >= 9n + 8phi + 10 = 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())) Arctic Interpretation Processor: dimension: 1 interpretation: [eq#](x0, x1) = 3x1, [Exists](x0, x1) = x0 + 4x1 + 2, [Not](x0) = x0 + 3, [Or](x0, x1) = 2x0 + 4x1 + 2, [t] = 2, [Var](x0) = 1x0 + 4, [cons](x0, x1) = 1x0 + 4x1 + 0, [in](x0, x1) = 3x1 + 1, [ver](x0, x1) = 2x0 + x1 + 0, [nil] = 3, [main](x0) = 12x0 + 4, [s](x0) = 1x0 + 4, [eq](x0, x1) = x0 + x1 + 1, [0] = 3, [or](x0, x1) = 1x1 + 1, [ff] = 0, [not](x0) = 1, [tt] = 0 orientation: eq#(s(x),s(y)) = 4y + 7 >= 3y = eq#(x,y) not(tt()) = 1 >= 0 = ff() not(ff()) = 1 >= 0 = tt() or(tt(),x) = 1x + 1 >= 0 = tt() or(ff(),x) = 1x + 1 >= x = x eq(0(),0()) = 3 >= 0 = tt() eq(s(x),0()) = 1x + 4 >= 0 = ff() eq(0(),s(y)) = 1y + 4 >= 0 = ff() eq(s(x),s(y)) = 1x + 1y + 4 >= x + y + 1 = eq(x,y) main(phi) = 12phi + 4 >= 2phi + 3 = ver(phi,nil()) in(x,nil()) = 6 >= 0 = ff() in(x,cons(a,l)) = 4a + 7l + 3 >= 4l + 2 = or(eq(x,a),in(x,l)) ver(Var(x),t()) = 3x + 6 >= 5 = in(x,t()) ver(Or(phi,psi),t()) = 4phi + 6psi + 4 >= 3psi + 3 = or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) = 2phi + 5 >= 1 = not(ver(phi,t())) ver(Exists(n,phi),t()) = 2n + 6phi + 4 >= 3phi + 3 = 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