MAYBE Problem: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() Proof: DP Processor: DPs: cond1#(true(),x,y,z) -> gr#(y,z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) cond2#(true(),x,y,z) -> p#(y) cond2#(true(),x,y,z) -> p#(x) cond2#(true(),x,y,z) -> gr#(y,z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) cond2#(false(),x,y,z) -> gr#(x,z) cond2#(false(),x,y,z) -> eq#(x,y) cond2#(false(),x,y,z) -> and#(eq(x,y),gr(x,z)) cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) gr#(s(x),s(y)) -> gr#(x,y) eq#(s(x),s(y)) -> eq#(x,y) TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() TDG Processor: DPs: cond1#(true(),x,y,z) -> gr#(y,z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) cond2#(true(),x,y,z) -> p#(y) cond2#(true(),x,y,z) -> p#(x) cond2#(true(),x,y,z) -> gr#(y,z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) cond2#(false(),x,y,z) -> gr#(x,z) cond2#(false(),x,y,z) -> eq#(x,y) cond2#(false(),x,y,z) -> and#(eq(x,y),gr(x,z)) cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) gr#(s(x),s(y)) -> gr#(x,y) eq#(s(x),s(y)) -> eq#(x,y) TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() graph: eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y) cond2#(false(),x,y,z) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y) cond2#(false(),x,y,z) -> gr#(x,z) -> gr#(s(x),s(y)) -> gr#(x,y) cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) -> cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) -> cond1#(true(),x,y,z) -> gr#(y,z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(false(),x,y,z) -> and#(eq(x,y),gr(x,z)) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(false(),x,y,z) -> eq#(x,y) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(false(),x,y,z) -> gr#(x,z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(true(),x,y,z) -> gr#(y,z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(true(),x,y,z) -> p#(x) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) -> cond2#(true(),x,y,z) -> p#(y) cond2#(true(),x,y,z) -> gr#(y,z) -> gr#(s(x),s(y)) -> gr#(x,y) gr#(s(x),s(y)) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(false(),x,y,z) -> and#(eq(x,y),gr(x,z)) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(false(),x,y,z) -> eq#(x,y) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(false(),x,y,z) -> gr#(x,z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(true(),x,y,z) -> gr#(y,z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(true(),x,y,z) -> p#(x) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) -> cond2#(true(),x,y,z) -> p#(y) cond1#(true(),x,y,z) -> gr#(y,z) -> gr#(s(x),s(y)) -> gr#(x,y) SCC Processor: #sccs: 3 #rules: 5 #arcs: 24/144 DPs: cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) cond2#(true(),x,y,z) -> cond2#(gr(y,z),p(x),p(y),z) TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() Arctic Interpretation Processor: dimension: 1 interpretation: [cond2#](x0, x1, x2, x3) = 1x0 + -7x1 + x2 + -16, [cond1#](x0, x1, x2, x3) = -2x0 + -7x1 + x2 + 4, [s](x0) = 1x0 + 6, [0] = 4, [and](x0, x1) = 1x0 + -4x1 + 6, [eq](x0, x1) = 1x1, [false] = 3, [p](x0) = -1x0 + 4, [cond2](x0, x1, x2, x3) = x3, [gr](x0, x1) = -2x0 + 3, [cond1](x0, x1, x2, x3) = x3, [true] = 4 orientation: cond2#(false(),x,y,z) = -7x + y + 4 >= -7x + y + 4 = cond1#(and(eq(x,y),gr(x,z)),x,y,z) cond1#(true(),x,y,z) = -7x + y + 4 >= -7x + y + 4 = cond2#(gr(y,z),x,y,z) cond2#(true(),x,y,z) = -7x + y + 5 >= -8x + -1y + 4 = cond2#(gr(y,z),p(x),p(y),z) cond1(true(),x,y,z) = z >= z = cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) = z >= z = cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) = z >= z = cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) = 3 >= 3 = false() gr(s(x),0()) = -1x + 4 >= 4 = true() gr(s(x),s(y)) = -1x + 4 >= -2x + 3 = gr(x,y) p(0()) = 4 >= 4 = 0() p(s(x)) = x + 5 >= x = x eq(0(),0()) = 5 >= 4 = true() eq(s(x),0()) = 5 >= 3 = false() eq(0(),s(x)) = 2x + 7 >= 3 = false() eq(s(x),s(y)) = 2y + 7 >= 1y = eq(x,y) and(true(),true()) = 6 >= 4 = true() and(false(),x) = -4x + 6 >= 3 = false() and(x,false()) = 1x + 6 >= 3 = false() problem: DPs: cond2#(false(),x,y,z) -> cond1#(and(eq(x,y),gr(x,z)),x,y,z) cond1#(true(),x,y,z) -> cond2#(gr(y,z),x,y,z) TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() Open DPs: gr#(s(x),s(y)) -> gr#(x,y) TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() Subterm Criterion Processor: simple projection: pi(gr#) = 1 problem: DPs: TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() Qed DPs: eq#(s(x),s(y)) -> eq#(x,y) TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() Subterm Criterion Processor: simple projection: pi(eq#) = 1 problem: DPs: TRS: cond1(true(),x,y,z) -> cond2(gr(y,z),x,y,z) cond2(true(),x,y,z) -> cond2(gr(y,z),p(x),p(y),z) cond2(false(),x,y,z) -> cond1(and(eq(x,y),gr(x,z)),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x eq(0(),0()) -> true() eq(s(x),0()) -> false() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() Qed