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) 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) 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) 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) 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) graph: *#(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: 2 #rules: 7 #arcs: 49/144 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) 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) 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) 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: 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* 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* 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) 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) Qed