YES Problem: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Proof: DP Processor: DPs: +#(O(x),O(y)) -> +#(x,y) +#(O(x),O(y)) -> O#(+(x,y)) +#(O(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) *#(O(x),y) -> *#(x,y) *#(O(x),y) -> O#(*(x,y)) *#(I(x),y) -> *#(x,y) *#(I(x),y) -> O#(*(x,y)) *#(I(x),y) -> +#(O(*(x,y)),y) -#(O(x),O(y)) -> -#(x,y) -#(O(x),O(y)) -> O#(-(x,y)) -#(O(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(I(x),O(y)) -> -#(x,y) -#(I(x),I(y)) -> -#(x,y) -#(I(x),I(y)) -> O#(-(x,y)) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) EDG Processor: DPs: +#(O(x),O(y)) -> +#(x,y) +#(O(x),O(y)) -> O#(+(x,y)) +#(O(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) *#(O(x),y) -> *#(x,y) *#(O(x),y) -> O#(*(x,y)) *#(I(x),y) -> *#(x,y) *#(I(x),y) -> O#(*(x,y)) *#(I(x),y) -> +#(O(*(x,y)),y) -#(O(x),O(y)) -> -#(x,y) -#(O(x),O(y)) -> O#(-(x,y)) -#(O(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(I(x),O(y)) -> -#(x,y) -#(I(x),I(y)) -> -#(x,y) -#(I(x),I(y)) -> O#(-(x,y)) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) graph: -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y) -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y)) -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y) -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(I(x),I(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y) -#(I(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y) -#(I(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y)) -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(O(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(I(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y)) -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(O(x),I(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y)) -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y)) *#(I(x),y) -> *#(x,y) -> *#(O(x),y) -> *#(x,y) *#(I(x),y) -> *#(x,y) -> *#(O(x),y) -> O#(*(x,y)) *#(I(x),y) -> *#(x,y) -> *#(I(x),y) -> *#(x,y) *#(I(x),y) -> *#(x,y) -> *#(I(x),y) -> O#(*(x,y)) *#(I(x),y) -> *#(x,y) -> *#(I(x),y) -> +#(O(*(x,y)),y) *#(I(x),y) -> +#(O(*(x,y)),y) -> +#(O(x),O(y)) -> +#(x,y) *#(I(x),y) -> +#(O(*(x,y)),y) -> +#(O(x),O(y)) -> O#(+(x,y)) *#(I(x),y) -> +#(O(*(x,y)),y) -> +#(O(x),I(y)) -> +#(x,y) *#(I(x),y) -> +#(O(*(x,y)),y) -> +#(I(x),O(y)) -> +#(x,y) *#(I(x),y) -> +#(O(*(x,y)),y) -> +#(I(x),I(y)) -> +#(x,y) *#(I(x),y) -> +#(O(*(x,y)),y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) *#(I(x),y) -> +#(O(*(x,y)),y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) *#(O(x),y) -> *#(x,y) -> *#(O(x),y) -> *#(x,y) *#(O(x),y) -> *#(x,y) -> *#(O(x),y) -> O#(*(x,y)) *#(O(x),y) -> *#(x,y) -> *#(I(x),y) -> *#(x,y) *#(O(x),y) -> *#(x,y) -> *#(I(x),y) -> O#(*(x,y)) *#(O(x),y) -> *#(x,y) -> *#(I(x),y) -> +#(O(*(x,y)),y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(O(x),I(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(I(x),I(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(I(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y)) +#(I(x),I(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(I(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y)) +#(I(x),O(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(O(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y)) +#(O(x),I(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(O(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y)) +#(O(x),O(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) SCC Processor: #sccs: 3 #rules: 12 #arcs: 81/361 DPs: *#(I(x),y) -> *#(x,y) *#(O(x),y) -> *#(x,y) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Subterm Criterion Processor: simple projection: pi(*#) = 0 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Qed DPs: +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(I(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Usable Rule Processor: DPs: +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(I(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) TRS: +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) O(0()) -> 0() Bounds Processor: bound: 2 enrichment: match-dp automaton: final states: {7} transitions: O1(40) -> 40* +{#,2}(43,41) -> 7,4 +{#,2}(38,41) -> 7,4 +{#,2}(43,42) -> 7,4 +{#,0}(3,1) -> 4* +{#,0}(3,3) -> 4* +{#,0}(3,5) -> 4* +{#,0}(4,2) -> 4* +{#,0}(4,4) -> 4* +{#,0}(9,8) -> 7* +{#,0}(5,1) -> 7,4 +{#,0}(5,3) -> 4* +{#,0}(5,5) -> 4* +{#,0}(1,2) -> 4* +{#,0}(1,4) -> 4* +{#,0}(2,1) -> 7,4 +{#,0}(2,3) -> 4* +{#,0}(2,5) -> 4* +{#,0}(3,2) -> 4* +{#,0}(3,4) -> 4* +{#,0}(4,1) -> 4* +{#,0}(4,3) -> 4* +{#,0}(4,5) -> 4* +{#,0}(5,2) -> 4* +{#,0}(5,4) -> 4* +{#,0}(1,1) -> 4* +{#,0}(1,3) -> 4* +{#,0}(1,5) -> 4* +{#,0}(2,2) -> 4* +{#,0}(2,4) -> 4* +2(43,41) -> 43* +2(38,41) -> 43* +2(40,41) -> 43* +2(43,38) -> 43* +2(38,38) -> 43* +2(40,38) -> 43* I0(5) -> 3* I0(2) -> 3* I0(4) -> 3* I0(1) -> 8,3 I0(3) -> 3* I2(41) -> 42* +0(3,1) -> 2* +0(3,3) -> 2* +0(3,5) -> 2* +0(4,2) -> 2* +0(4,4) -> 2* +0(5,1) -> 2* +0(5,3) -> 2* +0(5,5) -> 2* +0(1,2) -> 2* +0(1,4) -> 2* +0(6,6) -> 9* +0(2,1) -> 2* +0(2,3) -> 2* +0(2,5) -> 2* +0(3,2) -> 2* +0(3,4) -> 2* +0(4,1) -> 2* +0(4,3) -> 2* +0(4,5) -> 2* +0(5,2) -> 2* +0(5,4) -> 2* +0(1,1) -> 2* +0(1,3) -> 2* +0(1,5) -> 2* +0(2,2) -> 2* +0(2,4) -> 2* 02() -> 41* 00() -> 5,1 O0(5) -> 5* O0(2) -> 5* O0(4) -> 5* O0(1) -> 5* O0(3) -> 5* +{#,1}(1,41) -> 7,4 +{#,1}(2,38) -> 7,4 +{#,1}(3,41) -> 7,4 +{#,1}(4,38) -> 7,4 +{#,1}(40,39) -> 7,4,6 +{#,1}(1,38) -> 7,4 +{#,1}(2,41) -> 7,4 +{#,1}(43,38) -> 7,4 +{#,1}(3,38) -> 7,4 +{#,1}(4,41) -> 7,4 +{#,1}(40,38) -> 7,4 +1(3,1) -> 40* +1(1,41) -> 40* +1(3,3) -> 40* +1(3,5) -> 40* +1(2,38) -> 40* +1(4,2) -> 40* +1(4,4) -> 40* +1(43,39) -> 40* +1(5,1) -> 40* +1(3,41) -> 40* +1(5,3) -> 40* +1(5,5) -> 40* +1(4,38) -> 40* +1(1,2) -> 40* +1(1,4) -> 40* +1(40,39) -> 40* +1(2,1) -> 40* +1(2,3) -> 40* +1(2,5) -> 40* +1(1,38) -> 40* +1(3,2) -> 40* +1(3,4) -> 40* +1(4,1) -> 40* +1(2,41) -> 40* +1(4,3) -> 40* +1(4,5) -> 40* +1(3,38) -> 40* +1(5,2) -> 40* +1(5,4) -> 40* +1(4,41) -> 40* +1(1,1) -> 40* +1(1,3) -> 40* +1(1,5) -> 40* +1(2,2) -> 40* +1(2,4) -> 40* I1(40) -> 40* I1(43) -> 40* I1(38) -> 39* 01() -> 38* 1 -> 40,2,6 2 -> 40,6 3 -> 40,2,6 4 -> 40,2,6 5 -> 40,2,6 6 -> 9* 38 -> 43,40 39 -> 40* 40 -> 43* 41 -> 40* problem: DPs: +#(I(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) TRS: +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) O(0()) -> 0() Restore Modifier: DPs: +#(I(x),I(y)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Subterm Criterion Processor: simple projection: pi(+#) = 1 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Qed DPs: -#(I(x),I(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(O(x),I(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Usable Rule Processor: DPs: -#(I(x),I(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(O(x),I(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) TRS: -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) O(0()) -> 0() Bounds Processor: bound: 2 enrichment: match-dp automaton: final states: {24} transitions: 02() -> 48* I0(20) -> 19* I0(22) -> 19* I0(17) -> 25,19 I0(19) -> 19* I0(21) -> 19* I0(18) -> 19* -{#,0}(22,18) -> 21* -{#,0}(17,18) -> 21* -{#,0}(22,20) -> 21* -{#,0}(17,20) -> 21* -{#,0}(22,22) -> 21* -{#,0}(17,22) -> 21* -{#,0}(18,17) -> 24,21 -{#,0}(18,19) -> 21* -{#,0}(18,21) -> 21* -{#,0}(19,18) -> 21* -{#,0}(19,20) -> 21* -{#,0}(19,22) -> 21* -{#,0}(20,17) -> 24,21 -{#,0}(20,19) -> 21* -{#,0}(20,21) -> 21* -{#,0}(21,18) -> 21* -{#,0}(21,20) -> 21* -{#,0}(21,22) -> 21* -{#,0}(22,17) -> 24,21 -{#,0}(17,17) -> 24,21 -{#,0}(22,19) -> 21* -{#,0}(17,19) -> 21* -{#,0}(22,21) -> 21* -{#,0}(17,21) -> 21* -{#,0}(18,18) -> 21* -{#,0}(18,20) -> 21* -{#,0}(18,22) -> 21* -{#,0}(19,17) -> 24,21 -{#,0}(19,19) -> 21* -{#,0}(19,21) -> 21* -{#,0}(20,18) -> 21* -{#,0}(20,20) -> 21* -{#,0}(20,22) -> 21* -{#,0}(21,17) -> 24,21 -{#,0}(21,19) -> 21* -{#,0}(21,21) -> 21* -{#,0}(26,25) -> 24* -0(22,18) -> 18* -0(17,18) -> 18* -0(22,20) -> 18* -0(17,20) -> 18* -0(22,22) -> 18* -0(17,22) -> 18* -0(18,17) -> 18* -0(18,19) -> 18* -0(18,21) -> 18* -0(23,23) -> 26* -0(19,18) -> 18* -0(19,20) -> 18* -0(19,22) -> 18* -0(20,17) -> 18* -0(20,19) -> 18* -0(20,21) -> 18* -0(21,18) -> 18* -0(21,20) -> 18* -0(21,22) -> 18* -0(22,17) -> 18* -0(17,17) -> 18* -0(22,19) -> 18* -0(17,19) -> 18* -0(22,21) -> 18* -0(17,21) -> 18* -0(18,18) -> 18* -0(18,20) -> 18* -0(18,22) -> 18* -0(19,17) -> 18* -0(19,19) -> 18* -0(19,21) -> 18* -0(20,18) -> 18* -0(20,20) -> 18* -0(20,22) -> 18* -0(21,17) -> 18* -0(21,19) -> 18* -0(21,21) -> 18* 00() -> 20,22 10() -> 17* O0(20) -> 20* O0(22) -> 20* O0(17) -> 20* O0(19) -> 20* O0(21) -> 20* O0(18) -> 20* -{#,1}(18,43) -> 21,24,18,26 -{#,1}(45,43) -> 21,24,18,26 -{#,1}(49,43) -> 21,24,18,26 -{#,1}(45,44) -> 24,21,23 -1(22,18) -> 45* -1(17,18) -> 45* -1(22,20) -> 45* -1(17,20) -> 45* -1(22,22) -> 45* -1(17,22) -> 45* -1(18,17) -> 45* -1(18,19) -> 45* -1(18,21) -> 45* -1(19,18) -> 45* -1(19,20) -> 45* -1(19,22) -> 45* -1(18,43) -> 45* -1(20,17) -> 45* -1(20,19) -> 45* -1(20,21) -> 45* -1(21,18) -> 45* -1(21,20) -> 45* -1(21,22) -> 45* -1(22,17) -> 45* -1(17,17) -> 45* -1(22,19) -> 45* -1(17,19) -> 45* -1(22,21) -> 45* -1(17,21) -> 45* -1(18,18) -> 45* -1(18,20) -> 45* -1(18,22) -> 45* -1(19,17) -> 45* -1(48,44) -> 52* -1(19,19) -> 45* -1(19,21) -> 45* -1(49,43) -> 48* -1(20,18) -> 45* -1(20,20) -> 45* -1(20,22) -> 45* -1(21,17) -> 45* -1(21,19) -> 45* -1(45,44) -> 49* -1(21,21) -> 45* I1(45) -> 45* I1(52) -> 49* I1(49) -> 45* I1(43) -> 44* 11() -> 43* -{#,2}(48,47) -> 21,24,18,26 01() -> 52,49,45 -2(45,43) -> 48* O1(45) -> 45* O1(48) -> 49* 12() -> 46* I2(46) -> 47* 17 -> 18,23 18 -> 45,23 19 -> 18,23 20 -> 45,18,23 21 -> 18,23 22 -> 18,23 23 -> 26* problem: DPs: -#(I(x),I(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) TRS: -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) O(0()) -> 0() Restore Modifier: DPs: -#(I(x),I(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Subterm Criterion Processor: simple projection: pi(-#) = 1 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> x +(O(x),O(y)) -> O(+(x,y)) +(O(x),I(y)) -> I(+(x,y)) +(I(x),O(y)) -> I(+(x,y)) +(I(x),I(y)) -> O(+(+(x,y),I(0()))) *(0(),x) -> 0() *(x,0()) -> 0() *(O(x),y) -> O(*(x,y)) *(I(x),y) -> +(O(*(x,y)),y) -(x,0()) -> x -(0(),x) -> 0() -(O(x),O(y)) -> O(-(x,y)) -(O(x),I(y)) -> I(-(-(x,y),I(1()))) -(I(x),O(y)) -> I(-(x,y)) -(I(x),I(y)) -> O(-(x,y)) Qed