YES Problem: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Proof: DP Processor: DPs: digits#() -> d#(0()) d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0())))))))))) d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if#(true(),x) -> d#(s(x)) le#(s(x),s(y)) -> le#(x,y) TRS: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) EDG Processor: DPs: digits#() -> d#(0()) d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0())))))))))) d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if#(true(),x) -> d#(s(x)) le#(s(x),s(y)) -> le#(x,y) TRS: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) graph: if#(true(),x) -> d#(s(x)) -> d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0())))))))))) if#(true(),x) -> d#(s(x)) -> d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) -> if#(true(),x) -> d#(s(x)) d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0())))))))))) -> le#(s(x),s(y)) -> le#(x,y) digits#() -> d#(0()) -> d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0())))))))))) digits#() -> d#(0()) -> d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) SCC Processor: #sccs: 2 #rules: 3 #arcs: 7/25 DPs: if#(true(),x) -> d#(s(x)) d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) TRS: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Usable Rule Processor: DPs: if#(true(),x) -> d#(s(x)) d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) TRS: f14(x,y) -> x f14(x,y) -> y le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) le(s(x),0()) -> false() Bounds Processor: bound: 10 enrichment: top-dp automaton: final states: {21} transitions: le7(21,189) -> 197* le7(16,189) -> 197* le7(138,193) -> 197* le7(18,187) -> 197* le7(18,189) -> 197* le7(114,192) -> 197* le7(186,196) -> 197* le7(20,187) -> 197* le7(20,189) -> 197* le7(61,190) -> 197* le7(162,195) -> 197* le7(102,191) -> 197* le7(17,187) -> 197* le7(12,187) -> 197* le7(17,189) -> 197* le7(12,189) -> 197* le7(18,188) -> 197* le7(13,188) -> 197* le7(19,187) -> 197* le7(150,194) -> 197* le7(14,187) -> 197* le7(19,189) -> 197* le7(14,189) -> 197* le7(21,187) -> 197* le7(16,187) -> 197* 07() -> 187* false6() -> 173* true7() -> 197* d{#,8}(198) -> 21,12,14 s8(207) -> 208* s8(202) -> 203* s8(204) -> 205* s8(199) -> 200* s8(206) -> 207* s8(201) -> 202* s8(186) -> 198* s8(203) -> 204* s8(205) -> 206* s8(200) -> 201* if{#,8}(209,198) -> 14,21,12 le8(61,201) -> 209* le8(162,206) -> 209* le8(102,202) -> 209* le8(17,200) -> 209* le8(12,200) -> 209* le8(18,199) -> 209* le8(13,199) -> 209* le8(150,205) -> 209* le8(19,200) -> 209* le8(14,200) -> 209* le8(21,200) -> 209* le8(16,200) -> 209* le8(198,208) -> 209* le8(138,204) -> 209* le8(18,200) -> 209* le8(114,203) -> 209* le8(186,207) -> 209* le8(20,200) -> 209* 08() -> 199* false7() -> 197* true8() -> 209* d{#,9}(210) -> 21,12,14 s9(217) -> 218* s9(212) -> 213* s9(219) -> 220* s9(214) -> 215* s9(216) -> 217* s9(211) -> 212* s9(218) -> 219* s9(213) -> 214* s9(198) -> 210* s9(215) -> 216* false8() -> 209* if{#,9}(221,210) -> 14,21,12 le9(21,211) -> 221* le9(16,211) -> 221* le9(198,219) -> 221* le9(138,215) -> 221* le9(18,211) -> 221* le9(114,214) -> 221* le9(186,218) -> 221* le9(20,211) -> 221* le9(61,212) -> 221* le9(162,217) -> 221* le9(102,213) -> 221* le9(17,211) -> 221* le9(12,211) -> 221* le9(210,220) -> 221* le9(150,216) -> 221* le9(19,211) -> 221* le9(14,211) -> 221* if{#,0}(12,12) -> 12* if{#,0}(17,14) -> 12* if{#,0}(12,14) -> 12* if{#,0}(17,16) -> 12* if{#,0}(12,16) -> 12* if{#,0}(17,18) -> 12* if{#,0}(12,18) -> 12* if{#,0}(17,20) -> 12* if{#,0}(12,20) -> 12* if{#,0}(18,13) -> 12* if{#,0}(13,13) -> 12* if{#,0}(18,17) -> 12* if{#,0}(13,17) -> 12* if{#,0}(18,19) -> 12* if{#,0}(13,19) -> 12* if{#,0}(18,21) -> 12* if{#,0}(13,21) -> 12* if{#,0}(19,12) -> 12* if{#,0}(14,12) -> 12* if{#,0}(19,14) -> 12* if{#,0}(14,14) -> 12* if{#,0}(19,16) -> 12* if{#,0}(14,16) -> 12* if{#,0}(19,18) -> 12* if{#,0}(14,18) -> 12* if{#,0}(19,20) -> 12* if{#,0}(14,20) -> 12* if{#,0}(20,13) -> 12* if{#,0}(20,17) -> 12* if{#,0}(20,19) -> 12* if{#,0}(20,21) -> 12* if{#,0}(21,12) -> 12* if{#,0}(16,12) -> 14,12 if{#,0}(21,14) -> 12* if{#,0}(16,14) -> 14,12 if{#,0}(21,16) -> 12* if{#,0}(16,16) -> 14,12 if{#,0}(21,18) -> 12* if{#,0}(16,18) -> 14,12 if{#,0}(21,20) -> 12* if{#,0}(16,20) -> 21,12 if{#,0}(17,13) -> 12* if{#,0}(12,13) -> 12* if{#,0}(17,17) -> 12* if{#,0}(12,17) -> 12* if{#,0}(17,19) -> 12* if{#,0}(12,19) -> 12* if{#,0}(17,21) -> 12* if{#,0}(12,21) -> 12* if{#,0}(18,12) -> 12* if{#,0}(13,12) -> 12* if{#,0}(18,14) -> 12* if{#,0}(13,14) -> 12* if{#,0}(18,16) -> 12* if{#,0}(13,16) -> 12* if{#,0}(18,18) -> 12* if{#,0}(13,18) -> 12* if{#,0}(18,20) -> 12* if{#,0}(13,20) -> 12* if{#,0}(19,13) -> 12* if{#,0}(14,13) -> 12* if{#,0}(19,17) -> 12* if{#,0}(14,17) -> 12* if{#,0}(19,19) -> 12* if{#,0}(14,19) -> 12* if{#,0}(19,21) -> 12* if{#,0}(14,21) -> 12* if{#,0}(20,12) -> 12* if{#,0}(20,14) -> 12* if{#,0}(20,16) -> 12* if{#,0}(20,18) -> 12* if{#,0}(20,20) -> 12* if{#,0}(21,13) -> 12* if{#,0}(16,13) -> 14,12 if{#,0}(21,17) -> 12* if{#,0}(16,17) -> 14,12 if{#,0}(21,19) -> 12* if{#,0}(16,19) -> 14,12 if{#,0}(21,21) -> 12* if{#,0}(16,21) -> 14,12 if{#,0}(17,12) -> 12* 09() -> 211* true0() -> 16,13 false9() -> 221* d{#,0}(20) -> 21* d{#,0}(17) -> 14* d{#,0}(12) -> 14* d{#,0}(19) -> 14* d{#,0}(14) -> 14* d{#,0}(21) -> 14* d{#,0}(16) -> 14* d{#,0}(18) -> 14* d{#,0}(13) -> 14* true9() -> 221* s0(20) -> 20* s0(17) -> 20* s0(12) -> 20* s0(19) -> 20* s0(14) -> 20* s0(21) -> 20* s0(16) -> 20* s0(18) -> 20* s0(13) -> 20* d{#,10}(222) -> 21,12,14 le0(12,12) -> 16* le0(17,14) -> 16* le0(12,14) -> 16* le0(17,16) -> 16* le0(12,16) -> 16* le0(17,18) -> 16* le0(12,18) -> 16* le0(17,20) -> 16* le0(12,20) -> 16* le0(18,13) -> 16* le0(13,13) -> 16* le0(18,17) -> 16* le0(13,17) -> 16* le0(18,19) -> 16* le0(13,19) -> 16* le0(18,21) -> 16* le0(13,21) -> 16* le0(19,12) -> 16* le0(14,12) -> 16* le0(19,14) -> 16* le0(14,14) -> 16* le0(19,16) -> 16* le0(14,16) -> 16* le0(19,18) -> 16* le0(14,18) -> 16* le0(19,20) -> 16* le0(14,20) -> 16* le0(20,13) -> 16* le0(20,17) -> 16* le0(20,19) -> 16* le0(20,21) -> 16* le0(21,12) -> 16* le0(16,12) -> 16* le0(21,14) -> 16* le0(16,14) -> 16* le0(21,16) -> 16* le0(16,16) -> 16* le0(21,18) -> 16* le0(16,18) -> 16* le0(21,20) -> 16* le0(16,20) -> 16* le0(17,13) -> 16* le0(12,13) -> 16* le0(17,17) -> 16* le0(12,17) -> 16* le0(17,19) -> 16* le0(12,19) -> 16* le0(17,21) -> 16* le0(12,21) -> 16* le0(18,12) -> 16* le0(13,12) -> 16* le0(18,14) -> 16* le0(13,14) -> 16* le0(18,16) -> 16* le0(13,16) -> 16* le0(18,18) -> 16* le0(13,18) -> 16* le0(18,20) -> 16* le0(13,20) -> 16* le0(19,13) -> 16* le0(14,13) -> 16* le0(19,17) -> 16* le0(14,17) -> 16* le0(19,19) -> 16* le0(14,19) -> 16* le0(19,21) -> 16* le0(14,21) -> 16* le0(20,12) -> 16* le0(20,14) -> 16* le0(20,16) -> 16* le0(20,18) -> 16* le0(20,20) -> 16* le0(21,13) -> 16* le0(16,13) -> 16* le0(21,17) -> 16* le0(16,17) -> 16* le0(21,19) -> 16* le0(16,19) -> 16* le0(21,21) -> 16* le0(16,21) -> 16* le0(17,12) -> 16* s10(227) -> 228* s10(229) -> 230* s10(224) -> 225* s10(231) -> 232* s10(226) -> 227* s10(228) -> 229* s10(223) -> 224* s10(230) -> 231* s10(225) -> 226* s10(210) -> 222* 00() -> 17* if{#,10}(233,222) -> 14,21,12 f140(17,12) -> 18* f140(12,12) -> 18* f140(17,14) -> 18* f140(12,14) -> 18* f140(17,16) -> 18* f140(12,16) -> 18* f140(17,18) -> 18* f140(12,18) -> 18* f140(17,20) -> 18* f140(12,20) -> 18* f140(18,13) -> 18* f140(13,13) -> 18* f140(18,17) -> 18* f140(13,17) -> 18* f140(18,19) -> 18* f140(13,19) -> 18* f140(18,21) -> 18* f140(13,21) -> 18* f140(19,12) -> 18* f140(14,12) -> 18* f140(19,14) -> 18* f140(14,14) -> 18* f140(19,16) -> 18* f140(14,16) -> 18* f140(19,18) -> 18* f140(14,18) -> 18* f140(19,20) -> 18* f140(14,20) -> 18* f140(20,13) -> 18* f140(20,17) -> 18* f140(20,19) -> 18* f140(20,21) -> 18* f140(21,12) -> 18* f140(16,12) -> 18* f140(21,14) -> 18* f140(16,14) -> 18* f140(21,16) -> 18* f140(16,16) -> 18* f140(21,18) -> 18* f140(16,18) -> 18* f140(21,20) -> 18* f140(16,20) -> 18* f140(17,13) -> 18* f140(12,13) -> 18* f140(17,17) -> 18* f140(12,17) -> 18* f140(17,19) -> 18* f140(12,19) -> 18* f140(17,21) -> 18* f140(12,21) -> 18* f140(18,12) -> 18* f140(13,12) -> 18* f140(18,14) -> 18* f140(13,14) -> 18* f140(18,16) -> 18* f140(13,16) -> 18* f140(18,18) -> 18* f140(13,18) -> 18* f140(18,20) -> 18* f140(13,20) -> 18* f140(19,13) -> 18* f140(14,13) -> 18* f140(19,17) -> 18* f140(14,17) -> 18* f140(19,19) -> 18* f140(14,19) -> 18* f140(19,21) -> 18* f140(14,21) -> 18* f140(20,12) -> 18* f140(20,14) -> 18* f140(20,16) -> 18* f140(20,18) -> 18* f140(20,20) -> 18* f140(21,13) -> 18* f140(16,13) -> 18* f140(21,17) -> 18* f140(16,17) -> 18* f140(21,19) -> 18* f140(16,19) -> 18* f140(21,21) -> 18* f140(16,21) -> 18* le10(186,229) -> 233* le10(222,232) -> 233* le10(61,223) -> 233* le10(162,228) -> 233* le10(102,224) -> 233* le10(210,231) -> 233* le10(150,227) -> 233* le10(198,230) -> 233* le10(138,226) -> 233* le10(114,225) -> 233* false0() -> 16,19 010() -> 223* d{#,1}(61) -> 21,14,12 false10() -> 233* s1(90) -> 91* s1(20) -> 61* s1(97) -> 98* s1(92) -> 93* s1(17) -> 61* s1(12) -> 61* s1(94) -> 95* s1(19) -> 61* s1(14) -> 61* s1(96) -> 97* s1(91) -> 92* s1(21) -> 61* s1(16) -> 61* s1(98) -> 99* s1(93) -> 94* s1(18) -> 61* s1(13) -> 61* s1(95) -> 96* if{#,1}(100,61) -> 14,21,12 le1(13,90) -> 100* le1(18,92) -> 100* le1(13,92) -> 100* le1(18,94) -> 100* le1(13,94) -> 100* le1(18,96) -> 100* le1(18,98) -> 100* le1(20,96) -> 100* le1(20,98) -> 100* le1(61,99) -> 100* le1(17,96) -> 100* le1(12,96) -> 100* le1(17,98) -> 100* le1(12,98) -> 100* le1(18,91) -> 100* le1(13,91) -> 100* le1(18,93) -> 100* le1(13,93) -> 100* le1(18,95) -> 100* le1(13,95) -> 100* le1(18,97) -> 100* le1(13,97) -> 100* le1(19,96) -> 100* le1(14,96) -> 100* le1(19,98) -> 100* le1(14,98) -> 100* le1(21,96) -> 100* le1(16,96) -> 100* le1(21,98) -> 100* le1(16,98) -> 100* le1(18,90) -> 100* 01() -> 90* true1() -> 100* d{#,2}(102) -> 21,12,14 s2(107) -> 108* s2(109) -> 110* s2(104) -> 105* s2(111) -> 112* s2(106) -> 107* s2(61) -> 102* s2(108) -> 109* s2(103) -> 104* s2(110) -> 111* s2(105) -> 106* if{#,2}(113,102) -> 14,21,12 le2(18,104) -> 113* le2(13,104) -> 113* le2(18,106) -> 113* le2(13,106) -> 113* le2(18,108) -> 113* le2(18,110) -> 113* le2(20,108) -> 113* le2(20,110) -> 113* le2(61,111) -> 113* le2(102,112) -> 113* le2(17,108) -> 113* le2(12,108) -> 113* le2(17,110) -> 113* le2(12,110) -> 113* le2(18,103) -> 113* le2(13,103) -> 113* le2(18,105) -> 113* le2(13,105) -> 113* le2(18,107) -> 113* le2(13,107) -> 113* le2(18,109) -> 113* le2(13,109) -> 113* le2(19,108) -> 113* le2(14,108) -> 113* le2(19,110) -> 113* le2(14,110) -> 113* le2(21,108) -> 113* le2(16,108) -> 113* le2(21,110) -> 113* le2(16,110) -> 113* 02() -> 103* true2() -> 113* d{#,3}(114) -> 21,12,14 s3(122) -> 123* s3(117) -> 118* s3(102) -> 114* s3(119) -> 120* s3(121) -> 122* s3(116) -> 117* s3(123) -> 124* s3(118) -> 119* s3(120) -> 121* s3(115) -> 116* if{#,3}(125,114) -> 14,21,12 le3(20,121) -> 125* le3(61,122) -> 125* le3(102,123) -> 125* le3(17,121) -> 125* le3(12,121) -> 125* le3(18,116) -> 125* le3(13,116) -> 125* le3(18,118) -> 125* le3(13,118) -> 125* le3(18,120) -> 125* le3(13,120) -> 125* le3(19,121) -> 125* le3(14,121) -> 125* le3(21,121) -> 125* le3(16,121) -> 125* le3(18,115) -> 125* le3(13,115) -> 125* le3(18,117) -> 125* le3(13,117) -> 125* le3(18,119) -> 125* le3(13,119) -> 125* le3(18,121) -> 125* le3(114,124) -> 125* 03() -> 115* false1() -> 100* true3() -> 125* d{#,4}(138) -> 21,12,14 s4(147) -> 148* s4(142) -> 143* s4(144) -> 145* s4(139) -> 140* s4(114) -> 138* s4(146) -> 147* s4(141) -> 142* s4(143) -> 144* s4(145) -> 146* s4(140) -> 141* if{#,4}(149,138) -> 14,21,12 le4(19,142) -> 149* le4(14,142) -> 149* le4(19,144) -> 149* le4(14,144) -> 149* le4(21,142) -> 149* le4(16,142) -> 149* le4(21,144) -> 149* le4(16,144) -> 149* le4(138,148) -> 149* le4(18,140) -> 149* le4(13,140) -> 149* le4(18,142) -> 149* le4(18,144) -> 149* le4(114,147) -> 149* le4(20,142) -> 149* le4(20,144) -> 149* le4(61,145) -> 149* le4(102,146) -> 149* le4(17,142) -> 149* le4(12,142) -> 149* le4(17,144) -> 149* le4(12,144) -> 149* le4(18,139) -> 149* le4(13,139) -> 149* le4(18,141) -> 149* le4(13,141) -> 149* le4(18,143) -> 149* le4(13,143) -> 149* 04() -> 139* false2() -> 113* false3() -> 125* true4() -> 149* d{#,5}(150) -> 21,12,14 s5(157) -> 158* s5(152) -> 153* s5(159) -> 160* s5(154) -> 155* s5(156) -> 157* s5(151) -> 152* s5(158) -> 159* s5(153) -> 154* s5(138) -> 150* s5(155) -> 156* if{#,5}(161,150) -> 14,21,12 le5(18,151) -> 161* le5(13,151) -> 161* le5(18,153) -> 161* le5(18,155) -> 161* le5(114,158) -> 161* le5(20,153) -> 161* le5(20,155) -> 161* le5(61,156) -> 161* le5(102,157) -> 161* le5(17,153) -> 161* le5(12,153) -> 161* le5(17,155) -> 161* le5(12,155) -> 161* le5(18,152) -> 161* le5(13,152) -> 161* le5(18,154) -> 161* le5(13,154) -> 161* le5(19,153) -> 161* le5(150,160) -> 161* le5(14,153) -> 161* le5(19,155) -> 161* le5(14,155) -> 161* le5(21,153) -> 161* le5(16,153) -> 161* le5(21,155) -> 161* le5(16,155) -> 161* le5(138,159) -> 161* 05() -> 151* false4() -> 149* true5() -> 161* d{#,6}(162) -> 21,12,14 s6(167) -> 168* s6(169) -> 170* s6(164) -> 165* s6(171) -> 172* s6(166) -> 167* s6(168) -> 169* s6(163) -> 164* s6(170) -> 171* s6(165) -> 166* s6(150) -> 162* if{#,6}(173,162) -> 14,21,12 le6(18,163) -> 173* le6(13,163) -> 173* le6(18,165) -> 173* le6(13,165) -> 173* le6(150,171) -> 173* le6(19,166) -> 173* le6(14,166) -> 173* le6(21,166) -> 173* le6(16,166) -> 173* le6(138,170) -> 173* le6(18,164) -> 173* le6(13,164) -> 173* le6(18,166) -> 173* le6(114,169) -> 173* le6(20,166) -> 173* le6(61,167) -> 173* le6(162,172) -> 173* le6(102,168) -> 173* le6(17,166) -> 173* le6(12,166) -> 173* 06() -> 163* false5() -> 161* true6() -> 173* d{#,7}(186) -> 21,12,14 s7(192) -> 193* s7(187) -> 188* s7(162) -> 186* s7(194) -> 195* s7(189) -> 190* s7(191) -> 192* s7(193) -> 194* s7(188) -> 189* s7(195) -> 196* s7(190) -> 191* if{#,7}(197,186) -> 14,21,12 12 -> 18* 13 -> 18* 14 -> 18* 16 -> 18* 17 -> 18* 19 -> 18* 20 -> 18* 21 -> 18* problem: DPs: d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) TRS: f14(x,y) -> x f14(x,y) -> y le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) le(s(x),0()) -> false() Restore Modifier: DPs: d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) TRS: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Matrix Interpretation Processor: dimension: 1 interpretation: [if#](x0, x1) = 0, [d#](x0) = 1, [nil] = 0, [false] = 0, [cons](x0, x1) = 0, [true] = 0, [if](x0, x1) = 0, [le](x0, x1) = 0, [s](x0) = 0, [d](x0) = 0, [0] = 0, [digits] = 0 orientation: d#(x) = 1 >= 0 = if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) digits() = 0 >= 0 = d(0()) d(x) = 0 >= 0 = if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) = 0 >= 0 = cons(x,d(s(x))) if(false(),x) = 0 >= 0 = nil() le(0(),y) = 0 >= 0 = true() le(s(x),0()) = 0 >= 0 = false() le(s(x),s(y)) = 0 >= 0 = le(x,y) problem: DPs: TRS: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Qed DPs: le#(s(x),s(y)) -> le#(x,y) TRS: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Subterm Criterion Processor: simple projection: pi(le#) = 1 problem: DPs: TRS: digits() -> d(0()) d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) if(true(),x) -> cons(x,d(s(x))) if(false(),x) -> nil() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Qed