YES
0 QTRS
↳1 DependencyPairsProof (⇔, 46 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 UsableRulesReductionPairsProof (⇔, 0 ms)
↳9 QDP
↳10 QDPSizeChangeProof (⇔, 0 ms)
↳11 YES
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 QDPSizeChangeProof (⇔, 0 ms)
↳16 YES
app(app(append, nil), l) → l
app(app(append, app(app(cons, h), t)), l) → app(app(cons, h), app(app(append, t), l))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, h), t)) → app(app(cons, app(f, h)), app(app(map, f), t))
app(app(append, app(app(append, l1), l2)), l3) → app(app(append, l1), app(app(append, l2), l3))
app(app(map, f), app(app(append, l1), l2)) → app(app(append, app(app(map, f), l1)), app(app(map, f), l2))
APP(app(append, app(app(cons, h), t)), l) → APP(app(cons, h), app(app(append, t), l))
APP(app(append, app(app(cons, h), t)), l) → APP(app(append, t), l)
APP(app(append, app(app(cons, h), t)), l) → APP(append, t)
APP(app(map, f), app(app(cons, h), t)) → APP(app(cons, app(f, h)), app(app(map, f), t))
APP(app(map, f), app(app(cons, h), t)) → APP(cons, app(f, h))
APP(app(map, f), app(app(cons, h), t)) → APP(f, h)
APP(app(map, f), app(app(cons, h), t)) → APP(app(map, f), t)
APP(app(append, app(app(append, l1), l2)), l3) → APP(app(append, l1), app(app(append, l2), l3))
APP(app(append, app(app(append, l1), l2)), l3) → APP(app(append, l2), l3)
APP(app(append, app(app(append, l1), l2)), l3) → APP(append, l2)
APP(app(map, f), app(app(append, l1), l2)) → APP(app(append, app(app(map, f), l1)), app(app(map, f), l2))
APP(app(map, f), app(app(append, l1), l2)) → APP(append, app(app(map, f), l1))
APP(app(map, f), app(app(append, l1), l2)) → APP(app(map, f), l1)
APP(app(map, f), app(app(append, l1), l2)) → APP(app(map, f), l2)
app(app(append, nil), l) → l
app(app(append, app(app(cons, h), t)), l) → app(app(cons, h), app(app(append, t), l))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, h), t)) → app(app(cons, app(f, h)), app(app(map, f), t))
app(app(append, app(app(append, l1), l2)), l3) → app(app(append, l1), app(app(append, l2), l3))
app(app(map, f), app(app(append, l1), l2)) → app(app(append, app(app(map, f), l1)), app(app(map, f), l2))
APP(app(append, app(app(append, l1), l2)), l3) → APP(app(append, l1), app(app(append, l2), l3))
APP(app(append, app(app(cons, h), t)), l) → APP(app(append, t), l)
APP(app(append, app(app(append, l1), l2)), l3) → APP(app(append, l2), l3)
app(app(append, nil), l) → l
app(app(append, app(app(cons, h), t)), l) → app(app(cons, h), app(app(append, t), l))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, h), t)) → app(app(cons, app(f, h)), app(app(map, f), t))
app(app(append, app(app(append, l1), l2)), l3) → app(app(append, l1), app(app(append, l2), l3))
app(app(map, f), app(app(append, l1), l2)) → app(app(append, app(app(map, f), l1)), app(app(map, f), l2))
APP(app(append, app(app(append, l1), l2)), l3) → APP(app(append, l1), app(app(append, l2), l3))
APP(app(append, app(app(cons, h), t)), l) → APP(app(append, t), l)
APP(app(append, app(app(append, l1), l2)), l3) → APP(app(append, l2), l3)
app(app(append, nil), l) → l
app(app(append, app(app(cons, h), t)), l) → app(app(cons, h), app(app(append, t), l))
app(app(append, app(app(append, l1), l2)), l3) → app(app(append, l1), app(app(append, l2), l3))
append1(append(l1, l2), l3) → append1(l1, append(l2, l3))
append1(cons(h, t), l) → append1(t, l)
append1(append(l1, l2), l3) → append1(l2, l3)
append(nil, l) → l
append(cons(h, t), l) → cons(h, append(t, l))
append(append(l1, l2), l3) → append(l1, append(l2, l3))
Used ordering: POLO with Polynomial interpretation [POLO]:
app(app(append, nil), l) → l
app(app(append, app(app(cons, h), t)), l) → app(app(cons, h), app(app(append, t), l))
app(app(append, app(app(append, l1), l2)), l3) → app(app(append, l1), app(app(append, l2), l3))
POL(append(x1, x2)) = x1 + x2
POL(append1(x1, x2)) = 2·x1 + x2
POL(cons(x1, x2)) = 2·x1 + x2
POL(nil) = 0
append1(append(l1, l2), l3) → append1(l1, append(l2, l3))
append1(cons(h, t), l) → append1(t, l)
append1(append(l1, l2), l3) → append1(l2, l3)
append(cons(h, t), l) → cons(h, append(t, l))
append(append(l1, l2), l3) → append(l1, append(l2, l3))
From the DPs we obtained the following set of size-change graphs:
APP(app(map, f), app(app(cons, h), t)) → APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) → APP(f, h)
APP(app(map, f), app(app(append, l1), l2)) → APP(app(map, f), l1)
APP(app(map, f), app(app(append, l1), l2)) → APP(app(map, f), l2)
app(app(append, nil), l) → l
app(app(append, app(app(cons, h), t)), l) → app(app(cons, h), app(app(append, t), l))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, h), t)) → app(app(cons, app(f, h)), app(app(map, f), t))
app(app(append, app(app(append, l1), l2)), l3) → app(app(append, l1), app(app(append, l2), l3))
app(app(map, f), app(app(append, l1), l2)) → app(app(append, app(app(map, f), l1)), app(app(map, f), l2))
APP(app(map, f), app(app(cons, h), t)) → APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) → APP(f, h)
APP(app(map, f), app(app(append, l1), l2)) → APP(app(map, f), l1)
APP(app(map, f), app(app(append, l1), l2)) → APP(app(map, f), l2)
From the DPs we obtained the following set of size-change graphs: