0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 ATransformationProof (⇔)
↳13 QDP
↳14 QReductionProof (⇔)
↳15 QDP
↳16 QDPSizeChangeProof (⇔)
↳17 TRUE
↳18 QDP
↳19 UsableRulesProof (⇔)
↳20 QDP
↳21 QReductionProof (⇔)
↳22 QDP
↳23 ATransformationProof (⇔)
↳24 QDP
↳25 QReductionProof (⇔)
↳26 QDP
↳27 QDPSizeChangeProof (⇔)
↳28 TRUE
↳29 QDP
↳30 UsableRulesProof (⇔)
↳31 QDP
↳32 QReductionProof (⇔)
↳33 QDP
↳34 ForwardInstantiation (⇔)
↳35 QDP
↳36 ForwardInstantiation (⇔)
↳37 QDP
↳38 ForwardInstantiation (⇔)
↳39 QDP
↳40 MNOCProof (⇔)
↳41 QDP
↳42 QDPOrderProof (⇔)
↳43 QDP
↳44 UsableRulesProof (⇔)
↳45 QDP
↳46 QDPSizeChangeProof (⇔)
↳47 TRUE
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
inc → app(map, app(app(curry, plus), app(s, 0)))
double → app(map, app(app(curry, times), app(s, app(s, 0))))
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
inc → app(map, app(app(curry, plus), app(s, 0)))
double → app(map, app(app(curry, times), app(s, app(s, 0))))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
APP(app(plus, app(s, x)), y) → APP(s, app(app(plus, x), y))
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
APP(app(plus, app(s, x)), y) → APP(plus, x)
APP(app(times, app(s, x)), y) → APP(app(plus, app(app(times, x), y)), y)
APP(app(times, app(s, x)), y) → APP(plus, app(app(times, x), y))
APP(app(times, app(s, x)), y) → APP(app(times, x), y)
APP(app(times, app(s, x)), y) → APP(times, x)
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(app(curry, g), x), y) → APP(g, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
INC → APP(map, app(app(curry, plus), app(s, 0)))
INC → APP(app(curry, plus), app(s, 0))
INC → APP(curry, plus)
INC → APP(s, 0)
DOUBLE → APP(map, app(app(curry, times), app(s, app(s, 0))))
DOUBLE → APP(app(curry, times), app(s, app(s, 0)))
DOUBLE → APP(curry, times)
DOUBLE → APP(s, app(s, 0))
DOUBLE → APP(s, 0)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
inc → app(map, app(app(curry, plus), app(s, 0)))
double → app(map, app(app(curry, times), app(s, app(s, 0))))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
inc → app(map, app(app(curry, plus), app(s, 0)))
double → app(map, app(app(curry, times), app(s, app(s, 0))))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
inc
double
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
plus1(s(x), y) → plus1(x, y)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
curry(x0, x1, x2)
map(x0, nil)
map(x0, cons(x1, x2))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
curry(x0, x1, x2)
map(x0, nil)
map(x0, cons(x1, x2))
plus1(s(x), y) → plus1(x, y)
From the DPs we obtained the following set of size-change graphs:
APP(app(times, app(s, x)), y) → APP(app(times, x), y)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
inc → app(map, app(app(curry, plus), app(s, 0)))
double → app(map, app(app(curry, times), app(s, app(s, 0))))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
APP(app(times, app(s, x)), y) → APP(app(times, x), y)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
inc
double
APP(app(times, app(s, x)), y) → APP(app(times, x), y)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
times1(s(x), y) → times1(x, y)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
curry(x0, x1, x2)
map(x0, nil)
map(x0, cons(x1, x2))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
curry(x0, x1, x2)
map(x0, nil)
map(x0, cons(x1, x2))
times1(s(x), y) → times1(x, y)
From the DPs we obtained the following set of size-change graphs:
APP(app(app(curry, g), x), y) → APP(g, x)
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
inc → app(map, app(app(curry, plus), app(s, 0)))
double → app(map, app(app(curry, times), app(s, app(s, 0))))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
APP(app(app(curry, g), x), y) → APP(g, x)
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
inc
double
inc
double
APP(app(app(curry, g), x), y) → APP(g, x)
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(app(curry, app(app(curry, y_0), y_1)), x1), x2) → APP(app(app(curry, y_0), y_1), x1)
APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x2) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(app(curry, app(app(curry, y_0), y_1)), x1), x2) → APP(app(app(curry, y_0), y_1), x1)
APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x2) → APP(app(map, y_0), app(app(cons, y_1), y_2))
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), x2)) → APP(app(app(curry, y_0), y_1), x1)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), x2)) → APP(app(app(curry, app(app(curry, y_0), y_1)), y_2), x1)
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), x2)) → APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x1)
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(app(curry, app(app(curry, y_0), y_1)), x1), x2) → APP(app(app(curry, y_0), y_1), x1)
APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x2) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), x2)) → APP(app(app(curry, y_0), y_1), x1)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), x2)) → APP(app(app(curry, app(app(curry, y_0), y_1)), y_2), x1)
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), x2)) → APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x1)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), app(app(cons, y_2), y_3))) → APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, y_2), y_3))
APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, y_3), y_4))
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, y_3), y_4))
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(app(curry, app(app(curry, y_0), y_1)), x1), x2) → APP(app(app(curry, y_0), y_1), x1)
APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x2) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), x2)) → APP(app(app(curry, y_0), y_1), x1)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), x2)) → APP(app(app(curry, app(app(curry, y_0), y_1)), y_2), x1)
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), x2)) → APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x1)
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), app(app(cons, y_2), y_3))) → APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, y_2), y_3))
APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, y_3), y_4))
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, y_3), y_4))
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(app(curry, app(app(curry, y_0), y_1)), x1), x2) → APP(app(app(curry, y_0), y_1), x1)
APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x2) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), x2)) → APP(app(app(curry, y_0), y_1), x1)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), x2)) → APP(app(app(curry, app(app(curry, y_0), y_1)), y_2), x1)
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), x2)) → APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x1)
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), app(app(cons, y_2), y_3))) → APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, y_2), y_3))
APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, y_3), y_4))
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, y_3), y_4))
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(app(curry, g), x), y) → APP(app(g, x), y)
APP(app(app(curry, app(app(curry, y_0), y_1)), x1), x2) → APP(app(app(curry, y_0), y_1), x1)
APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x2) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), x2)) → APP(app(app(curry, y_0), y_1), x1)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), x2)) → APP(app(app(curry, app(app(curry, y_0), y_1)), y_2), x1)
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), x2)) → APP(app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2)), x1)
POL(0) = 1
POL(APP(x1, x2)) = x1
POL(app(x1, x2)) = 1 + x1 + x1·x2
POL(cons) = 0
POL(curry) = 1
POL(map) = 1
POL(nil) = 1
POL(plus) = 0
POL(s) = 0
POL(times) = 0
app(app(map, f), nil) → nil
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(times, 0), y) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(plus, 0), y) → y
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), app(app(cons, y_2), y_3))) → APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, y_2), y_3))
APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, y_3), y_4))
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, y_3), y_4))
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(app(times, 0), y) → 0
app(app(times, app(s, x)), y) → app(app(plus, app(app(times, x), y)), y)
app(app(app(curry, g), x), y) → app(app(g, x), y)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, x1), app(app(cons, y_2), y_3))) → APP(app(map, app(app(curry, y_0), y_1)), app(app(cons, y_2), y_3))
APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(app(curry, y_0), y_1)), y_2)), app(app(cons, y_3), y_4))
APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, x1), app(app(cons, y_3), y_4))) → APP(app(map, app(app(curry, app(map, y_0)), app(app(cons, y_1), y_2))), app(app(cons, y_3), y_4))
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(app(times, 0), x0)
app(app(times, app(s, x0)), x1)
app(app(app(curry, x0), x1), x2)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
From the DPs we obtained the following set of size-change graphs: