YES
Problem:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Proof:
DP Processor:
DPs:
1024#() -> 1024_1#(0())
1024_1#(x) -> 10#()
1024_1#(x) -> lt#(x,10())
1024_1#(x) -> if#(lt(x,10()),x)
if#(true(),x) -> 1024_1#(s(x))
if#(true(),x) -> double#(1024_1(s(x)))
lt#(s(x),s(y)) -> lt#(x,y)
double#(s(x)) -> double#(x)
10#() -> double#(s(s(0())))
10#() -> double#(s(double(s(s(0())))))
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
EDG Processor:
DPs:
1024#() -> 1024_1#(0())
1024_1#(x) -> 10#()
1024_1#(x) -> lt#(x,10())
1024_1#(x) -> if#(lt(x,10()),x)
if#(true(),x) -> 1024_1#(s(x))
if#(true(),x) -> double#(1024_1(s(x)))
lt#(s(x),s(y)) -> lt#(x,y)
double#(s(x)) -> double#(x)
10#() -> double#(s(s(0())))
10#() -> double#(s(double(s(s(0())))))
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
graph:
double#(s(x)) -> double#(x) ->
double#(s(x)) -> double#(x)
if#(true(),x) -> double#(1024_1(s(x))) ->
double#(s(x)) -> double#(x)
if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> 10#()
if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> lt#(x,10())
if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> if#(lt(x,10()),x)
lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
10#() -> double#(s(double(s(s(0()))))) ->
double#(s(x)) -> double#(x)
10#() -> double#(s(s(0()))) -> double#(s(x)) -> double#(x)
1024_1#(x) -> if#(lt(x,10()),x) ->
if#(true(),x) -> 1024_1#(s(x))
1024_1#(x) -> if#(lt(x,10()),x) ->
if#(true(),x) -> double#(1024_1(s(x)))
1024_1#(x) -> lt#(x,10()) -> lt#(s(x),s(y)) -> lt#(x,y)
1024_1#(x) -> 10#() -> 10#() -> double#(s(s(0())))
1024_1#(x) -> 10#() -> 10#() -> double#(s(double(s(s(0())))))
1024#() -> 1024_1#(0()) -> 1024_1#(x) -> 10#()
1024#() -> 1024_1#(0()) -> 1024_1#(x) -> lt#(x,10())
1024#() -> 1024_1#(0()) -> 1024_1#(x) -> if#(lt(x,10()),x)
SCC Processor:
#sccs: 3
#rules: 4
#arcs: 16/100
DPs:
if#(true(),x) -> 1024_1#(s(x))
1024_1#(x) -> if#(lt(x,10()),x)
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Usable Rule Processor:
DPs:
if#(true(),x) -> 1024_1#(s(x))
1024_1#(x) -> if#(lt(x,10()),x)
TRS:
f16(x,y) -> x
f16(x,y) -> y
10() -> double(s(double(s(s(0())))))
double(s(x)) -> s(s(double(x)))
double(0()) -> 0()
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
Bounds Processor:
bound: 10
enrichment: top-dp
automaton:
final states: {25}
transitions:
lt7(25,271) -> 251*
lt7(20,271) -> 251*
lt7(20,273) -> 251*
lt7(15,273) -> 251*
lt7(223,258) -> 251*
lt7(21,274) -> 251*
lt7(16,274) -> 251*
lt7(189,257) -> 251*
lt7(22,273) -> 251*
lt7(98,270) -> 251*
lt7(124,263) -> 251*
lt7(23,274) -> 251*
lt7(18,274) -> 251*
lt7(24,273) -> 251*
lt7(19,273) -> 251*
lt7(14,273) -> 251*
lt7(25,272) -> 251*
lt7(20,272) -> 251*
lt7(20,274) -> 251*
lt7(15,274) -> 251*
lt7(51,269) -> 251*
lt7(249,250) -> 251*
lt7(21,273) -> 251*
lt7(16,273) -> 251*
lt7(22,274) -> 251*
lt7(23,273) -> 251*
lt7(18,273) -> 251*
lt7(24,274) -> 251*
lt7(19,274) -> 251*
lt7(14,274) -> 251*
lt7(161,264) -> 251*
107() -> 250*
double7(267) -> 273*
double7(252) -> 267*
double7(259) -> 269*
double7(254) -> 255*
double7(256) -> 250*
double7(268) -> 271*
double7(253) -> 259*
double7(260) -> 263*
double7(255) -> 257*
07() -> 273,267,252
false6() -> 225*
true7() -> 251*
1024_1{#,8}(275) -> 16,14,25
s8(297) -> 298*
s8(292) -> 285*
s8(287) -> 288*
s8(294) -> 289*
s8(289) -> 290*
s8(279) -> 280*
s8(249) -> 275*
s8(296) -> 293*
s8(291) -> 292*
s8(286) -> 281*
s8(281) -> 282*
s8(298) -> 295*
s8(293) -> 294*
s8(288) -> 276*
s8(278) -> 279*
s8(295) -> 296*
s8(290) -> 287*
s8(285) -> 286*
if{#,8}(277,275) -> 25,16,14
lt8(25,295) -> 277*
lt8(20,295) -> 277*
lt8(25,297) -> 277*
lt8(20,297) -> 277*
lt8(51,296) -> 277*
lt8(275,276) -> 277*
lt8(161,289) -> 277*
lt8(25,298) -> 277*
lt8(20,298) -> 277*
lt8(223,287) -> 277*
lt8(249,288) -> 277*
lt8(189,290) -> 277*
lt8(98,293) -> 277*
lt8(124,294) -> 277*
108() -> 276*
double8(292) -> 295*
double8(282) -> 276*
double8(279) -> 285*
double8(291) -> 297*
double8(286) -> 289*
double8(281) -> 287*
double8(278) -> 291*
double8(285) -> 293*
double8(280) -> 281*
08() -> 297,291,278
false7() -> 251*
true8() -> 277*
1024_1{#,9}(301) -> 16,14,25
s9(327) -> 324*
s9(317) -> 314*
s9(307) -> 308*
s9(324) -> 325*
s9(319) -> 310*
s9(314) -> 315*
s9(304) -> 305*
s9(326) -> 327*
s9(321) -> 318*
s9(316) -> 317*
s9(311) -> 302*
s9(318) -> 319*
s9(325) -> 320*
s9(320) -> 321*
s9(315) -> 307*
s9(310) -> 311*
s9(305) -> 306*
s9(275) -> 301*
if{#,9}(303,301) -> 25,16,14
if{#,0}(22,14) -> 14*
if{#,0}(22,16) -> 14*
if{#,0}(22,18) -> 14*
if{#,0}(22,20) -> 14*
if{#,0}(22,22) -> 14*
if{#,0}(22,24) -> 14*
if{#,0}(23,15) -> 14*
if{#,0}(18,15) -> 16,14
if{#,0}(23,19) -> 14*
if{#,0}(18,19) -> 16,14
if{#,0}(23,21) -> 14*
if{#,0}(18,21) -> 16,14
if{#,0}(23,23) -> 14*
if{#,0}(18,23) -> 16,14
if{#,0}(23,25) -> 14*
if{#,0}(18,25) -> 16,14
if{#,0}(24,14) -> 14*
if{#,0}(19,14) -> 14*
if{#,0}(24,16) -> 14*
if{#,0}(14,14) -> 14*
if{#,0}(19,16) -> 14*
if{#,0}(24,18) -> 14*
if{#,0}(14,16) -> 14*
if{#,0}(19,18) -> 14*
if{#,0}(24,20) -> 14*
if{#,0}(14,18) -> 14*
if{#,0}(19,20) -> 14*
if{#,0}(24,22) -> 14*
if{#,0}(14,20) -> 14*
if{#,0}(19,22) -> 14*
if{#,0}(24,24) -> 14*
if{#,0}(14,22) -> 14*
if{#,0}(19,24) -> 14*
if{#,0}(14,24) -> 14*
if{#,0}(25,15) -> 14*
if{#,0}(20,15) -> 14*
if{#,0}(15,15) -> 14*
if{#,0}(25,19) -> 14*
if{#,0}(20,19) -> 14*
if{#,0}(25,21) -> 14*
if{#,0}(15,19) -> 14*
if{#,0}(20,21) -> 14*
if{#,0}(25,23) -> 14*
if{#,0}(15,21) -> 14*
if{#,0}(20,23) -> 14*
if{#,0}(25,25) -> 14*
if{#,0}(15,23) -> 14*
if{#,0}(20,25) -> 14*
if{#,0}(15,25) -> 14*
if{#,0}(21,14) -> 14*
if{#,0}(16,14) -> 14*
if{#,0}(21,16) -> 14*
if{#,0}(16,16) -> 14*
if{#,0}(21,18) -> 14*
if{#,0}(16,18) -> 14*
if{#,0}(21,20) -> 14*
if{#,0}(16,20) -> 14*
if{#,0}(21,22) -> 14*
if{#,0}(16,22) -> 14*
if{#,0}(21,24) -> 14*
if{#,0}(16,24) -> 14*
if{#,0}(22,15) -> 14*
if{#,0}(22,19) -> 14*
if{#,0}(22,21) -> 14*
if{#,0}(22,23) -> 14*
if{#,0}(22,25) -> 14*
if{#,0}(23,14) -> 14*
if{#,0}(18,14) -> 16,14
if{#,0}(23,16) -> 14*
if{#,0}(18,16) -> 16,14
if{#,0}(23,18) -> 14*
if{#,0}(18,18) -> 16,14
if{#,0}(23,20) -> 14*
if{#,0}(18,20) -> 16,14
if{#,0}(23,22) -> 14*
if{#,0}(18,22) -> 16,14
if{#,0}(23,24) -> 14*
if{#,0}(18,24) -> 25,14
if{#,0}(24,15) -> 14*
if{#,0}(19,15) -> 14*
if{#,0}(14,15) -> 14*
if{#,0}(24,19) -> 14*
if{#,0}(19,19) -> 14*
if{#,0}(24,21) -> 14*
if{#,0}(14,19) -> 14*
if{#,0}(19,21) -> 14*
if{#,0}(24,23) -> 14*
if{#,0}(14,21) -> 14*
if{#,0}(19,23) -> 14*
if{#,0}(24,25) -> 14*
if{#,0}(14,23) -> 14*
if{#,0}(19,25) -> 14*
if{#,0}(14,25) -> 14*
if{#,0}(25,14) -> 14*
if{#,0}(20,14) -> 14*
if{#,0}(25,16) -> 14*
if{#,0}(15,14) -> 14*
if{#,0}(20,16) -> 14*
if{#,0}(25,18) -> 14*
if{#,0}(15,16) -> 14*
if{#,0}(20,18) -> 14*
if{#,0}(25,20) -> 14*
if{#,0}(15,18) -> 14*
if{#,0}(20,20) -> 14*
if{#,0}(25,22) -> 14*
if{#,0}(15,20) -> 14*
if{#,0}(20,22) -> 14*
if{#,0}(25,24) -> 14*
if{#,0}(15,22) -> 14*
if{#,0}(20,24) -> 14*
if{#,0}(15,24) -> 14*
if{#,0}(21,15) -> 14*
if{#,0}(16,15) -> 14*
if{#,0}(21,19) -> 14*
if{#,0}(16,19) -> 14*
if{#,0}(21,21) -> 14*
if{#,0}(16,21) -> 14*
if{#,0}(21,23) -> 14*
if{#,0}(16,23) -> 14*
if{#,0}(21,25) -> 14*
if{#,0}(16,25) -> 14*
lt9(98,325) -> 303*
lt9(124,320) -> 303*
lt9(25,327) -> 303*
lt9(20,327) -> 303*
lt9(51,324) -> 303*
lt9(161,321) -> 303*
lt9(25,326) -> 303*
lt9(20,326) -> 303*
lt9(223,319) -> 303*
lt9(249,310) -> 303*
lt9(275,311) -> 303*
lt9(189,318) -> 303*
lt9(301,302) -> 303*
true0() -> 18,15
109() -> 302*
1024_1{#,0}(25) -> 16*
1024_1{#,0}(20) -> 16*
1024_1{#,0}(15) -> 16*
1024_1{#,0}(22) -> 16*
1024_1{#,0}(24) -> 25*
1024_1{#,0}(19) -> 16*
1024_1{#,0}(14) -> 16*
1024_1{#,0}(21) -> 16*
1024_1{#,0}(16) -> 16*
1024_1{#,0}(23) -> 16*
1024_1{#,0}(18) -> 16*
false8() -> 277*
s0(25) -> 24*
s0(20) -> 24*
s0(15) -> 24*
s0(22) -> 24*
s0(24) -> 19,21,24
s0(19) -> 24*
s0(14) -> 24*
s0(21) -> 24*
s0(16) -> 24*
s0(23) -> 24*
s0(18) -> 24*
double9(317) -> 324*
double9(307) -> 310*
double9(314) -> 320*
double9(304) -> 316*
double9(316) -> 326*
double9(306) -> 307*
double9(308) -> 302*
double9(315) -> 318*
double9(305) -> 314*
lt0(22,14) -> 18*
lt0(22,16) -> 18*
lt0(22,18) -> 18*
lt0(22,20) -> 18*
lt0(22,22) -> 18*
lt0(22,24) -> 18*
lt0(23,15) -> 18*
lt0(18,15) -> 18*
lt0(23,19) -> 18*
lt0(18,19) -> 18*
lt0(23,21) -> 18*
lt0(18,21) -> 18*
lt0(23,23) -> 18*
lt0(18,23) -> 18*
lt0(23,25) -> 18*
lt0(18,25) -> 18*
lt0(24,14) -> 18*
lt0(19,14) -> 18*
lt0(24,16) -> 18*
lt0(14,14) -> 18*
lt0(19,16) -> 18*
lt0(24,18) -> 18*
lt0(14,16) -> 18*
lt0(19,18) -> 18*
lt0(24,20) -> 18*
lt0(14,18) -> 18*
lt0(19,20) -> 18*
lt0(24,22) -> 18*
lt0(14,20) -> 18*
lt0(19,22) -> 18*
lt0(24,24) -> 18*
lt0(14,22) -> 18*
lt0(19,24) -> 18*
lt0(14,24) -> 18*
lt0(25,15) -> 18*
lt0(20,15) -> 18*
lt0(15,15) -> 18*
lt0(25,19) -> 18*
lt0(20,19) -> 18*
lt0(25,21) -> 18*
lt0(15,19) -> 18*
lt0(20,21) -> 18*
lt0(25,23) -> 18*
lt0(15,21) -> 18*
lt0(20,23) -> 18*
lt0(25,25) -> 18*
lt0(15,23) -> 18*
lt0(20,25) -> 18*
lt0(15,25) -> 18*
lt0(21,14) -> 18*
lt0(16,14) -> 18*
lt0(21,16) -> 18*
lt0(16,16) -> 18*
lt0(21,18) -> 18*
lt0(16,18) -> 18*
lt0(21,20) -> 18*
lt0(16,20) -> 18*
lt0(21,22) -> 18*
lt0(16,22) -> 18*
lt0(21,24) -> 18*
lt0(16,24) -> 18*
lt0(22,15) -> 18*
lt0(22,19) -> 18*
lt0(22,21) -> 18*
lt0(22,23) -> 18*
lt0(22,25) -> 18*
lt0(23,14) -> 18*
lt0(18,14) -> 18*
lt0(23,16) -> 18*
lt0(18,16) -> 18*
lt0(23,18) -> 18*
lt0(18,18) -> 18*
lt0(23,20) -> 18*
lt0(18,20) -> 18*
lt0(23,22) -> 18*
lt0(18,22) -> 18*
lt0(23,24) -> 18*
lt0(18,24) -> 18*
lt0(24,15) -> 18*
lt0(19,15) -> 18*
lt0(14,15) -> 18*
lt0(24,19) -> 18*
lt0(19,19) -> 18*
lt0(24,21) -> 18*
lt0(14,19) -> 18*
lt0(19,21) -> 18*
lt0(24,23) -> 18*
lt0(14,21) -> 18*
lt0(19,23) -> 18*
lt0(24,25) -> 18*
lt0(14,23) -> 18*
lt0(19,25) -> 18*
lt0(14,25) -> 18*
lt0(25,14) -> 18*
lt0(20,14) -> 18*
lt0(25,16) -> 18*
lt0(15,14) -> 18*
lt0(20,16) -> 18*
lt0(25,18) -> 18*
lt0(15,16) -> 18*
lt0(20,18) -> 18*
lt0(25,20) -> 18*
lt0(15,18) -> 18*
lt0(20,20) -> 18*
lt0(25,22) -> 18*
lt0(15,20) -> 18*
lt0(20,22) -> 18*
lt0(25,24) -> 18*
lt0(15,22) -> 18*
lt0(20,24) -> 18*
lt0(15,24) -> 18*
lt0(21,15) -> 18*
lt0(16,15) -> 18*
lt0(21,19) -> 18*
lt0(16,19) -> 18*
lt0(21,21) -> 18*
lt0(16,21) -> 18*
lt0(21,23) -> 18*
lt0(16,23) -> 18*
lt0(21,25) -> 18*
lt0(16,25) -> 18*
09() -> 326,316,304
100() -> 19*
true9() -> 303*
f160(22,14) -> 20*
f160(22,16) -> 20*
f160(22,18) -> 20*
f160(22,20) -> 20*
f160(22,22) -> 20*
f160(22,24) -> 20*
f160(23,15) -> 20*
f160(18,15) -> 20*
f160(23,19) -> 20*
f160(18,19) -> 20*
f160(23,21) -> 20*
f160(18,21) -> 20*
f160(23,23) -> 20*
f160(18,23) -> 20*
f160(23,25) -> 20*
f160(18,25) -> 20*
f160(24,14) -> 20*
f160(19,14) -> 20*
f160(24,16) -> 20*
f160(14,14) -> 20*
f160(19,16) -> 20*
f160(24,18) -> 20*
f160(14,16) -> 20*
f160(19,18) -> 20*
f160(24,20) -> 20*
f160(14,18) -> 20*
f160(19,20) -> 20*
f160(24,22) -> 20*
f160(14,20) -> 20*
f160(19,22) -> 20*
f160(24,24) -> 20*
f160(14,22) -> 20*
f160(19,24) -> 20*
f160(14,24) -> 20*
f160(25,15) -> 20*
f160(20,15) -> 20*
f160(15,15) -> 20*
f160(25,19) -> 20*
f160(20,19) -> 20*
f160(25,21) -> 20*
f160(15,19) -> 20*
f160(20,21) -> 20*
f160(25,23) -> 20*
f160(15,21) -> 20*
f160(20,23) -> 20*
f160(25,25) -> 20*
f160(15,23) -> 20*
f160(20,25) -> 20*
f160(15,25) -> 20*
f160(21,14) -> 20*
f160(16,14) -> 20*
f160(21,16) -> 20*
f160(16,16) -> 20*
f160(21,18) -> 20*
f160(16,18) -> 20*
f160(21,20) -> 20*
f160(16,20) -> 20*
f160(21,22) -> 20*
f160(16,22) -> 20*
f160(21,24) -> 20*
f160(16,24) -> 20*
f160(22,15) -> 20*
f160(22,19) -> 20*
f160(22,21) -> 20*
f160(22,23) -> 20*
f160(22,25) -> 20*
f160(23,14) -> 20*
f160(18,14) -> 20*
f160(23,16) -> 20*
f160(18,16) -> 20*
f160(23,18) -> 20*
f160(18,18) -> 20*
f160(23,20) -> 20*
f160(18,20) -> 20*
f160(23,22) -> 20*
f160(18,22) -> 20*
f160(23,24) -> 20*
f160(18,24) -> 20*
f160(24,15) -> 20*
f160(19,15) -> 20*
f160(14,15) -> 20*
f160(24,19) -> 20*
f160(19,19) -> 20*
f160(24,21) -> 20*
f160(14,19) -> 20*
f160(19,21) -> 20*
f160(24,23) -> 20*
f160(14,21) -> 20*
f160(19,23) -> 20*
f160(24,25) -> 20*
f160(14,23) -> 20*
f160(19,25) -> 20*
f160(14,25) -> 20*
f160(25,14) -> 20*
f160(20,14) -> 20*
f160(25,16) -> 20*
f160(15,14) -> 20*
f160(20,16) -> 20*
f160(25,18) -> 20*
f160(15,16) -> 20*
f160(20,18) -> 20*
f160(25,20) -> 20*
f160(15,18) -> 20*
f160(20,20) -> 20*
f160(25,22) -> 20*
f160(15,20) -> 20*
f160(20,22) -> 20*
f160(25,24) -> 20*
f160(15,22) -> 20*
f160(20,24) -> 20*
f160(15,24) -> 20*
f160(21,15) -> 20*
f160(16,15) -> 20*
f160(21,19) -> 20*
f160(16,19) -> 20*
f160(21,21) -> 20*
f160(16,21) -> 20*
f160(21,23) -> 20*
f160(16,23) -> 20*
f160(21,25) -> 20*
f160(16,25) -> 20*
1024_1{#,10}(328) -> 16,14,25
double0(25) -> 21*
double0(20) -> 21*
double0(15) -> 21*
double0(22) -> 21*
double0(24) -> 19,21
double0(19) -> 21*
double0(14) -> 21*
double0(21) -> 21*
double0(16) -> 21*
double0(23) -> 21*
double0(18) -> 21*
s10(352) -> 349*
s10(347) -> 348*
s10(342) -> 329*
s10(337) -> 338*
s10(354) -> 351*
s10(349) -> 350*
s10(344) -> 339*
s10(339) -> 340*
s10(351) -> 352*
s10(346) -> 341*
s10(341) -> 342*
s10(336) -> 337*
s10(301) -> 328*
s10(353) -> 354*
s10(348) -> 343*
s10(343) -> 344*
s10(350) -> 345*
s10(345) -> 346*
00() -> 21,22
false9() -> 303*
false0() -> 18,23
if{#,10}(330,328) -> 25,16,14
1024_1{#,1}(51) -> 16,25,14
lt10(223,345) -> 330*
lt10(249,346) -> 330*
lt10(275,341) -> 330*
lt10(98,351) -> 330*
lt10(189,350) -> 330*
lt10(301,342) -> 330*
lt10(124,352) -> 330*
lt10(25,353) -> 330*
lt10(20,353) -> 330*
lt10(51,354) -> 330*
lt10(328,329) -> 330*
lt10(161,349) -> 330*
s1(90) -> 85*
s1(85) -> 86*
s1(80) -> 81*
s1(25) -> 51*
s1(20) -> 51*
s1(15) -> 51*
s1(92) -> 87*
s1(87) -> 88*
s1(22) -> 51*
s1(104) -> 93*
s1(94) -> 89*
s1(89) -> 90*
s1(24) -> 51*
s1(19) -> 51*
s1(14) -> 51*
s1(111) -> 103*
s1(91) -> 92*
s1(86) -> 65*
s1(81) -> 82*
s1(21) -> 51*
s1(16) -> 51*
s1(103) -> 104*
s1(93) -> 94*
s1(88) -> 83*
s1(83) -> 84*
s1(23) -> 51*
s1(18) -> 51*
s1(110) -> 111*
1010() -> 329*
if{#,1}(66,51) -> 25,16,14
double10(347) -> 353*
double10(337) -> 343*
double10(344) -> 345*
double10(339) -> 341*
double10(336) -> 347*
double10(348) -> 351*
double10(343) -> 349*
double10(338) -> 339*
double10(340) -> 329*
lt1(22,111) -> 66*
lt1(23,94) -> 66*
lt1(18,94) -> 66*
lt1(23,104) -> 66*
lt1(18,104) -> 66*
lt1(24,89) -> 66*
lt1(19,89) -> 66*
lt1(23,110) -> 66*
lt1(14,89) -> 66*
lt1(18,110) -> 66*
lt1(24,93) -> 66*
lt1(19,93) -> 66*
lt1(14,93) -> 66*
lt1(51,65) -> 66*
lt1(24,103) -> 66*
lt1(19,103) -> 66*
lt1(14,103) -> 66*
lt1(25,86) -> 66*
lt1(20,86) -> 66*
lt1(25,90) -> 66*
lt1(20,90) -> 66*
lt1(24,111) -> 66*
lt1(19,111) -> 66*
lt1(14,111) -> 66*
lt1(20,94) -> 66*
lt1(15,94) -> 66*
lt1(20,104) -> 66*
lt1(15,104) -> 66*
lt1(21,89) -> 66*
lt1(16,89) -> 66*
lt1(20,110) -> 66*
lt1(15,110) -> 66*
lt1(21,93) -> 66*
lt1(16,93) -> 66*
lt1(21,103) -> 66*
lt1(16,103) -> 66*
lt1(21,111) -> 66*
lt1(16,111) -> 66*
lt1(22,94) -> 66*
lt1(22,104) -> 66*
lt1(23,89) -> 66*
lt1(18,89) -> 66*
lt1(22,110) -> 66*
lt1(23,93) -> 66*
lt1(18,93) -> 66*
lt1(23,103) -> 66*
lt1(18,103) -> 66*
lt1(23,111) -> 66*
lt1(18,111) -> 66*
lt1(24,94) -> 66*
lt1(19,94) -> 66*
lt1(14,94) -> 66*
lt1(24,104) -> 66*
lt1(25,85) -> 66*
lt1(19,104) -> 66*
lt1(20,85) -> 66*
lt1(14,104) -> 66*
lt1(20,89) -> 66*
lt1(24,110) -> 66*
lt1(15,89) -> 66*
lt1(19,110) -> 66*
lt1(14,110) -> 66*
lt1(20,93) -> 66*
lt1(15,93) -> 66*
lt1(20,103) -> 66*
lt1(15,103) -> 66*
lt1(20,111) -> 66*
lt1(15,111) -> 66*
lt1(21,94) -> 66*
lt1(16,94) -> 66*
lt1(21,104) -> 66*
lt1(16,104) -> 66*
lt1(22,89) -> 66*
lt1(21,110) -> 66*
lt1(16,110) -> 66*
lt1(22,93) -> 66*
lt1(22,103) -> 66*
010() -> 353,347,336
101() -> 65*
false10() -> 330*
double1(80) -> 91*
double1(92) -> 103*
double1(87) -> 93*
double1(82) -> 83*
double1(84) -> 65*
double1(91) -> 110*
double1(81) -> 87*
double1(88) -> 89*
double1(83) -> 85*
01() -> 110,91,80
true1() -> 66*
if{#,2}(102,98) -> 25,16,14
lt2(25,117) -> 102*
lt2(20,117) -> 102*
lt2(20,121) -> 102*
lt2(15,121) -> 102*
lt2(20,123) -> 102*
lt2(15,123) -> 102*
lt2(20,127) -> 102*
lt2(15,127) -> 102*
lt2(21,116) -> 102*
lt2(16,116) -> 102*
lt2(21,120) -> 102*
lt2(16,120) -> 102*
lt2(21,122) -> 102*
lt2(16,122) -> 102*
lt2(21,128) -> 102*
lt2(16,128) -> 102*
lt2(22,121) -> 102*
lt2(22,123) -> 102*
lt2(22,127) -> 102*
lt2(23,116) -> 102*
lt2(25,112) -> 102*
lt2(18,116) -> 102*
lt2(20,112) -> 102*
lt2(23,120) -> 102*
lt2(18,120) -> 102*
lt2(23,122) -> 102*
lt2(18,122) -> 102*
lt2(23,128) -> 102*
lt2(18,128) -> 102*
lt2(24,121) -> 102*
lt2(19,121) -> 102*
lt2(24,123) -> 102*
lt2(14,121) -> 102*
lt2(19,123) -> 102*
lt2(14,123) -> 102*
lt2(24,127) -> 102*
lt2(19,127) -> 102*
lt2(14,127) -> 102*
lt2(98,101) -> 102*
lt2(20,116) -> 102*
lt2(15,116) -> 102*
lt2(20,120) -> 102*
lt2(15,120) -> 102*
lt2(20,122) -> 102*
lt2(15,122) -> 102*
lt2(51,113) -> 102*
lt2(20,128) -> 102*
lt2(15,128) -> 102*
lt2(21,121) -> 102*
lt2(16,121) -> 102*
lt2(21,123) -> 102*
lt2(16,123) -> 102*
lt2(21,127) -> 102*
lt2(16,127) -> 102*
lt2(22,116) -> 102*
lt2(22,120) -> 102*
lt2(22,122) -> 102*
lt2(22,128) -> 102*
lt2(23,121) -> 102*
lt2(18,121) -> 102*
lt2(23,123) -> 102*
lt2(18,123) -> 102*
lt2(23,127) -> 102*
lt2(18,127) -> 102*
lt2(24,116) -> 102*
lt2(19,116) -> 102*
lt2(14,116) -> 102*
lt2(24,120) -> 102*
lt2(19,120) -> 102*
lt2(24,122) -> 102*
lt2(14,120) -> 102*
lt2(19,122) -> 102*
lt2(14,122) -> 102*
lt2(24,128) -> 102*
lt2(19,128) -> 102*
lt2(14,128) -> 102*
102() -> 101*
1024_1{#,2}(98) -> 16,14,25
s2(105) -> 106*
s2(127) -> 128*
s2(122) -> 123*
s2(117) -> 112*
s2(112) -> 113*
s2(119) -> 114*
s2(114) -> 115*
s2(121) -> 116*
s2(116) -> 117*
s2(106) -> 107*
s2(51) -> 98*
s2(128) -> 122*
s2(123) -> 120*
s2(118) -> 119*
s2(113) -> 101*
s2(108) -> 109*
s2(120) -> 121*
s2(115) -> 108*
double2(105) -> 118*
double2(107) -> 108*
double2(119) -> 122*
double2(114) -> 120*
double2(109) -> 101*
double2(106) -> 114*
double2(118) -> 127*
double2(108) -> 112*
double2(115) -> 116*
02() -> 127,118,105
true2() -> 102*
1024_1{#,3}(124) -> 16,14,25
s3(157) -> 158*
s3(147) -> 148*
s3(142) -> 125*
s3(132) -> 133*
s3(159) -> 160*
s3(149) -> 150*
s3(144) -> 132*
s3(129) -> 130*
s3(146) -> 143*
s3(141) -> 142*
s3(158) -> 149*
s3(148) -> 141*
s3(143) -> 144*
s3(98) -> 124*
s3(160) -> 157*
s3(150) -> 147*
s3(145) -> 146*
s3(130) -> 131*
if{#,3}(126,124) -> 25,16,14
lt3(23,157) -> 126*
lt3(18,157) -> 126*
lt3(23,159) -> 126*
lt3(18,159) -> 126*
lt3(24,150) -> 126*
lt3(19,150) -> 126*
lt3(14,150) -> 126*
lt3(24,158) -> 126*
lt3(19,158) -> 126*
lt3(24,160) -> 126*
lt3(14,158) -> 126*
lt3(19,160) -> 126*
lt3(14,160) -> 126*
lt3(25,147) -> 126*
lt3(20,147) -> 126*
lt3(20,149) -> 126*
lt3(15,149) -> 126*
lt3(20,157) -> 126*
lt3(15,157) -> 126*
lt3(20,159) -> 126*
lt3(15,159) -> 126*
lt3(21,150) -> 126*
lt3(16,150) -> 126*
lt3(21,158) -> 126*
lt3(16,158) -> 126*
lt3(21,160) -> 126*
lt3(16,160) -> 126*
lt3(124,125) -> 126*
lt3(98,142) -> 126*
lt3(22,149) -> 126*
lt3(22,157) -> 126*
lt3(22,159) -> 126*
lt3(23,150) -> 126*
lt3(18,150) -> 126*
lt3(23,158) -> 126*
lt3(18,158) -> 126*
lt3(23,160) -> 126*
lt3(18,160) -> 126*
lt3(24,149) -> 126*
lt3(19,149) -> 126*
lt3(14,149) -> 126*
lt3(24,157) -> 126*
lt3(19,157) -> 126*
lt3(24,159) -> 126*
lt3(14,157) -> 126*
lt3(19,159) -> 126*
lt3(14,159) -> 126*
lt3(25,148) -> 126*
lt3(20,148) -> 126*
lt3(20,150) -> 126*
lt3(15,150) -> 126*
lt3(51,141) -> 126*
lt3(20,158) -> 126*
lt3(15,158) -> 126*
lt3(20,160) -> 126*
lt3(15,160) -> 126*
lt3(21,149) -> 126*
lt3(16,149) -> 126*
lt3(21,157) -> 126*
lt3(16,157) -> 126*
lt3(21,159) -> 126*
lt3(16,159) -> 126*
lt3(22,150) -> 126*
lt3(22,158) -> 126*
lt3(22,160) -> 126*
lt3(23,149) -> 126*
lt3(18,149) -> 126*
103() -> 125*
double3(132) -> 141*
double3(144) -> 147*
double3(129) -> 145*
double3(146) -> 157*
double3(131) -> 132*
double3(143) -> 149*
double3(133) -> 125*
double3(145) -> 159*
double3(130) -> 143*
03() -> 159,145,129
false1() -> 66*
true3() -> 126*
1024_1{#,4}(161) -> 16,14,25
s4(187) -> 188*
s4(182) -> 173*
s4(184) -> 179*
s4(179) -> 180*
s4(174) -> 171*
s4(169) -> 170*
s4(124) -> 161*
s4(186) -> 183*
s4(181) -> 182*
s4(176) -> 166*
s4(171) -> 172*
s4(188) -> 185*
s4(183) -> 184*
s4(173) -> 174*
s4(168) -> 169*
s4(185) -> 186*
s4(180) -> 175*
s4(175) -> 176*
false2() -> 102*
if{#,4}(167,161) -> 25,16,14
lt4(98,175) -> 167*
lt4(22,186) -> 167*
lt4(22,188) -> 167*
lt4(124,176) -> 167*
lt4(23,185) -> 167*
lt4(18,185) -> 167*
lt4(23,187) -> 167*
lt4(18,187) -> 167*
lt4(161,166) -> 167*
lt4(24,186) -> 167*
lt4(19,186) -> 167*
lt4(24,188) -> 167*
lt4(14,186) -> 167*
lt4(19,188) -> 167*
lt4(14,188) -> 167*
lt4(25,179) -> 167*
lt4(20,179) -> 167*
lt4(25,183) -> 167*
lt4(20,183) -> 167*
lt4(20,185) -> 167*
lt4(15,185) -> 167*
lt4(20,187) -> 167*
lt4(15,187) -> 167*
lt4(51,180) -> 167*
lt4(21,186) -> 167*
lt4(16,186) -> 167*
lt4(21,188) -> 167*
lt4(16,188) -> 167*
lt4(22,185) -> 167*
lt4(22,187) -> 167*
lt4(23,186) -> 167*
lt4(18,186) -> 167*
lt4(23,188) -> 167*
lt4(18,188) -> 167*
lt4(24,185) -> 167*
lt4(19,185) -> 167*
lt4(24,187) -> 167*
lt4(14,185) -> 167*
lt4(19,187) -> 167*
lt4(14,187) -> 167*
lt4(25,184) -> 167*
lt4(20,184) -> 167*
lt4(20,186) -> 167*
lt4(15,186) -> 167*
lt4(20,188) -> 167*
lt4(15,188) -> 167*
lt4(21,185) -> 167*
lt4(16,185) -> 167*
lt4(21,187) -> 167*
lt4(16,187) -> 167*
104() -> 166*
double4(182) -> 185*
double4(172) -> 166*
double4(174) -> 179*
double4(169) -> 173*
double4(181) -> 187*
double4(171) -> 175*
double4(173) -> 183*
double4(168) -> 181*
double4(170) -> 171*
04() -> 187,181,168
false3() -> 126*
true4() -> 167*
1024_1{#,5}(189) -> 16,14,25
s5(212) -> 213*
s5(207) -> 202*
s5(202) -> 203*
s5(197) -> 198*
s5(219) -> 220*
s5(209) -> 204*
s5(204) -> 205*
s5(211) -> 206*
s5(206) -> 207*
s5(161) -> 189*
s5(213) -> 210*
s5(208) -> 209*
s5(203) -> 193*
s5(198) -> 199*
s5(220) -> 212*
s5(210) -> 211*
s5(205) -> 200*
s5(200) -> 201*
if{#,5}(194,189) -> 25,16,14
lt5(25,210) -> 194*
lt5(20,210) -> 194*
lt5(20,212) -> 194*
lt5(15,212) -> 194*
lt5(20,220) -> 194*
lt5(15,220) -> 194*
lt5(21,213) -> 194*
lt5(16,213) -> 194*
lt5(21,219) -> 194*
lt5(16,219) -> 194*
lt5(98,207) -> 194*
lt5(22,212) -> 194*
lt5(22,220) -> 194*
lt5(124,202) -> 194*
lt5(23,213) -> 194*
lt5(18,213) -> 194*
lt5(23,219) -> 194*
lt5(18,219) -> 194*
lt5(24,212) -> 194*
lt5(19,212) -> 194*
lt5(14,212) -> 194*
lt5(24,220) -> 194*
lt5(19,220) -> 194*
lt5(14,220) -> 194*
lt5(25,211) -> 194*
lt5(20,211) -> 194*
lt5(20,213) -> 194*
lt5(15,213) -> 194*
lt5(20,219) -> 194*
lt5(51,206) -> 194*
lt5(15,219) -> 194*
lt5(21,212) -> 194*
lt5(16,212) -> 194*
lt5(189,193) -> 194*
lt5(21,220) -> 194*
lt5(16,220) -> 194*
lt5(22,213) -> 194*
lt5(22,219) -> 194*
lt5(23,212) -> 194*
lt5(18,212) -> 194*
lt5(23,220) -> 194*
lt5(18,220) -> 194*
lt5(24,213) -> 194*
lt5(19,213) -> 194*
lt5(14,213) -> 194*
lt5(161,203) -> 194*
lt5(24,219) -> 194*
lt5(19,219) -> 194*
lt5(14,219) -> 194*
105() -> 193*
double5(197) -> 208*
double5(209) -> 212*
double5(204) -> 210*
double5(199) -> 200*
double5(201) -> 193*
double5(208) -> 219*
double5(198) -> 204*
double5(205) -> 206*
double5(200) -> 202*
05() -> 219,208,197
false4() -> 167*
true5() -> 194*
1024_1{#,6}(223) -> 16,14,25
s6(247) -> 248*
s6(237) -> 238*
s6(232) -> 224*
s6(227) -> 228*
s6(244) -> 235*
s6(234) -> 229*
s6(229) -> 230*
s6(189) -> 223*
s6(246) -> 243*
s6(236) -> 231*
s6(231) -> 232*
s6(226) -> 227*
s6(248) -> 245*
s6(243) -> 244*
s6(238) -> 233*
s6(233) -> 234*
s6(245) -> 246*
s6(235) -> 236*
if{#,6}(225,223) -> 25,16,14
lt6(22,245) -> 225*
lt6(22,247) -> 225*
lt6(161,231) -> 225*
lt6(23,248) -> 225*
lt6(18,248) -> 225*
lt6(24,245) -> 225*
lt6(19,245) -> 225*
lt6(24,247) -> 225*
lt6(14,245) -> 225*
lt6(19,247) -> 225*
lt6(14,247) -> 225*
lt6(189,232) -> 225*
lt6(98,235) -> 225*
lt6(25,246) -> 225*
lt6(20,246) -> 225*
lt6(20,248) -> 225*
lt6(15,248) -> 225*
lt6(124,236) -> 225*
lt6(21,245) -> 225*
lt6(16,245) -> 225*
lt6(21,247) -> 225*
lt6(16,247) -> 225*
lt6(22,248) -> 225*
lt6(23,245) -> 225*
lt6(18,245) -> 225*
lt6(23,247) -> 225*
lt6(18,247) -> 225*
lt6(223,224) -> 225*
lt6(24,248) -> 225*
lt6(19,248) -> 225*
lt6(14,248) -> 225*
lt6(25,243) -> 225*
lt6(20,243) -> 225*
lt6(20,245) -> 225*
lt6(15,245) -> 225*
lt6(20,247) -> 225*
lt6(15,247) -> 225*
lt6(51,244) -> 225*
lt6(21,248) -> 225*
lt6(16,248) -> 225*
106() -> 224*
double6(237) -> 247*
double6(227) -> 233*
double6(234) -> 235*
double6(229) -> 231*
double6(226) -> 237*
double6(238) -> 245*
double6(233) -> 243*
double6(228) -> 229*
double6(230) -> 224*
06() -> 247,237,226
false5() -> 194*
true6() -> 225*
1024_1{#,7}(249) -> 16,14,25
s7(272) -> 269*
s7(267) -> 268*
s7(257) -> 258*
s7(252) -> 253*
s7(274) -> 271*
s7(269) -> 270*
s7(264) -> 257*
s7(259) -> 260*
s7(271) -> 272*
s7(273) -> 274*
s7(268) -> 259*
s7(263) -> 264*
s7(258) -> 250*
s7(253) -> 254*
s7(223) -> 249*
s7(270) -> 263*
s7(260) -> 255*
s7(255) -> 256*
if{#,7}(251,249) -> 25,16,14
14 -> 20*
15 -> 20*
16 -> 20*
18 -> 20*
19 -> 20*
21 -> 20*
22 -> 20*
23 -> 20*
24 -> 20*
25 -> 20*
problem:
DPs:
1024_1#(x) -> if#(lt(x,10()),x)
TRS:
f16(x,y) -> x
f16(x,y) -> y
10() -> double(s(double(s(s(0())))))
double(s(x)) -> s(s(double(x)))
double(0()) -> 0()
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
Restore Modifier:
DPs:
1024_1#(x) -> if#(lt(x,10()),x)
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Matrix Interpretation Processor:
dimension: 1
interpretation:
[if#](x0, x1) = 0,
[1024_1#](x0) = 1,
[false] = 0,
[double](x0) = 0,
[s](x0) = 0,
[true] = 0,
[if](x0, x1) = 0,
[lt](x0, x1) = 0,
[10] = 0,
[1024_1](x0) = 0,
[0] = 0,
[1024] = 0
orientation:
1024_1#(x) = 1 >= 0 = if#(lt(x,10()),x)
1024() = 0 >= 0 = 1024_1(0())
1024_1(x) = 0 >= 0 = if(lt(x,10()),x)
if(true(),x) = 0 >= 0 = double(1024_1(s(x)))
if(false(),x) = 0 >= 0 = s(0())
lt(0(),s(y)) = 0 >= 0 = true()
lt(x,0()) = 0 >= 0 = false()
lt(s(x),s(y)) = 0 >= 0 = lt(x,y)
double(0()) = 0 >= 0 = 0()
double(s(x)) = 0 >= 0 = s(s(double(x)))
10() = 0 >= 0 = double(s(double(s(s(0())))))
problem:
DPs:
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Qed
DPs:
lt#(s(x),s(y)) -> lt#(x,y)
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Subterm Criterion Processor:
simple projection:
pi(lt#) = 1
problem:
DPs:
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Qed
DPs:
double#(s(x)) -> double#(x)
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Subterm Criterion Processor:
simple projection:
pi(double#) = 0
problem:
DPs:
TRS:
1024() -> 1024_1(0())
1024_1(x) -> if(lt(x,10()),x)
if(true(),x) -> double(1024_1(s(x)))
if(false(),x) -> s(0())
lt(0(),s(y)) -> true()
lt(x,0()) -> false()
lt(s(x),s(y)) -> lt(x,y)
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
10() -> double(s(double(s(s(0())))))
Qed