R
↳Dependency Pair Analysis
APP(app(mapbt, f), app(leaf, x)) -> APP(leaf, app(f, x))
APP(app(mapbt, f), app(leaf, x)) -> APP(f, x)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(branch, app(f, x)), app(app(mapbt, f), l))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(branch, app(f, x))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(f, x)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(f, x)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(branch, app(f, x)), app(app(mapbt, f), l))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
APP(app(mapbt, f), app(leaf, x)) -> APP(f, x)
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
innermost
six new Dependency Pairs are created:
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(app(branch, app(f'', x)), app(leaf, app(f'', x''))), app(app(mapbt, f''), r))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, f''), r))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(leaf, x''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(leaf, app(f'', x'')))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(app(app(branch, x''), l''), r''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
APP(app(mapbt, f''), app(app(app(branch, x), l), app(app(app(branch, x''), l''), r''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(leaf, x''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(leaf, app(f'', x'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, f''), r))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(app(branch, app(f'', x)), app(leaf, app(f'', x''))), app(app(mapbt, f''), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(f, x)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(branch, app(f, x)), app(app(mapbt, f), l))
APP(app(mapbt, f), app(leaf, x)) -> APP(f, x)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
innermost
four new Dependency Pairs are created:
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(branch, app(f, x)), app(app(mapbt, f), l))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(branch, app(f'', x)), app(leaf, app(f'', x'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Forward Instantiation Transformation
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(branch, app(f'', x)), app(leaf, app(f'', x'')))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(leaf, x''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(leaf, app(f'', x'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, f''), r))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(app(branch, app(f'', x)), app(leaf, app(f'', x''))), app(app(mapbt, f''), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(f, x)
APP(app(mapbt, f), app(leaf, x)) -> APP(f, x)
APP(app(mapbt, f''), app(app(app(branch, x), l), app(app(app(branch, x''), l''), r''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
innermost
eight new Dependency Pairs are created:
APP(app(mapbt, f), app(leaf, x)) -> APP(f, x)
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(leaf, x''))) -> APP(app(mapbt, f''), app(leaf, x''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(app(app(branch, x''), l''), r''))) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(leaf, x'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(leaf, x'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(leaf, x'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Forward Instantiation Transformation
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(leaf, x'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(leaf, x'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(leaf, x'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(app(app(branch, x''), l''), r''))) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(leaf, x''))) -> APP(app(mapbt, f''), app(leaf, x''))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(branch, app(f'', x)), app(leaf, app(f'', x'')))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(app(app(branch, x''), l''), r''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(leaf, x''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(leaf, app(f'', x'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, f''), r))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(app(branch, app(f'', x)), app(leaf, app(f'', x''))), app(app(mapbt, f''), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(f, x)
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
innermost
15 new Dependency Pairs are created:
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(f, x)
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(leaf, x'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(leaf, x'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(leaf, x''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(leaf, x''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(leaf, x'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x''''''))))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r''''''))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Polynomial Ordering
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r''''''))))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x''''''))))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(leaf, x'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(leaf, x''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(leaf, x'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(leaf, x'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(leaf, x'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(leaf, x''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(leaf, x'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(leaf, x'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(app(app(branch, x''), l''), r''))) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(leaf, x''))) -> APP(app(mapbt, f''), app(leaf, x''))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(branch, app(f'', x)), app(leaf, app(f'', x'')))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(app(app(branch, x''), l''), r''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(leaf, x''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(leaf, app(f'', x'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, f''), r))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(app(branch, app(f'', x)), app(leaf, app(f'', x''))), app(app(mapbt, f''), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
innermost
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(branch, app(f'', x)), app(leaf, app(f'', x'')))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(app(app(branch, x''), l''), r''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r'')))
APP(app(mapbt, f''), app(app(app(branch, x), l), app(leaf, x''))) -> APP(app(app(branch, app(f'', x)), app(app(mapbt, f''), l)), app(leaf, app(f'', x'')))
APP(app(mapbt, f''), app(app(app(branch, x), app(app(app(branch, x''), l''), r'')), r)) -> APP(app(app(branch, app(f'', x)), app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, f''), r))
APP(app(mapbt, f''), app(app(app(branch, x), app(leaf, x'')), r)) -> APP(app(app(branch, app(f'', x)), app(leaf, app(f'', x''))), app(app(mapbt, f''), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(app(branch, app(app(app(branch, app(f'', x'')), app(app(mapbt, f''), l'')), app(app(mapbt, f''), r''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(leaf, x'')), l), r)) -> APP(app(app(branch, app(leaf, app(f'', x''))), app(app(mapbt, app(mapbt, f'')), l)), app(app(mapbt, app(mapbt, f'')), r))
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
POL(branch) = 0 POL(mapbt) = 1 POL(leaf) = 0 POL(app(x1, x2)) = x1 POL(APP(x1, x2)) = x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Polynomial Ordering
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r''''''))))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x''''''))))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(leaf, x'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(leaf, x''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(leaf, x'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(leaf, x'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(leaf, x'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(leaf, x''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(leaf, x'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(leaf, x'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(app(app(branch, x''), l''), r''))) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(leaf, x''))) -> APP(app(mapbt, f''), app(leaf, x''))
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
innermost
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(app(app(branch, x''''''), l''''''), r''''''))))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x'''''')))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), l''''), app(leaf, x''''''))))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(app(app(branch, x''''''), l''''''), r'''''')), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(leaf, x'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''''')), app(leaf, app(app(app(branch, x''''), app(leaf, x'''''')), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(app(app(branch, x''''''), l''''''), r'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), l''), app(leaf, x''''))), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(leaf, x'''')))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(app(app(branch, x''''), l''''), r'''')), r''))
APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''), app(leaf, x'''')), r'')), l), r)) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(app(app(branch, x''''), l''''), r'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), app(leaf, x'''')), r''))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), app(leaf, x'''')), r''))
APP(app(mapbt, app(mapbt, app(mapbt, app(mapbt, f'''''')))), app(app(app(branch, app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, app(mapbt, f''''''))), app(leaf, app(app(app(branch, app(leaf, x'''''')), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(leaf, app(app(app(branch, app(leaf, x'''')), l''), r''))) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(app(app(branch, x''''), l''''), r''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''''), l''''), r'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(leaf, app(leaf, x''''))), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(leaf, x'''')))
APP(app(mapbt, app(mapbt, app(mapbt, f''''))), app(app(app(branch, app(app(app(branch, app(leaf, x'''')), l''), r'')), l), r)) -> APP(app(mapbt, app(mapbt, f'''')), app(app(app(branch, app(leaf, x'''')), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(app(app(branch, app(app(app(branch, x''), l''), r'')), l), r)) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(app(app(branch, x''), l''), r''))) -> APP(app(mapbt, f''), app(app(app(branch, x''), l''), r''))
APP(app(mapbt, app(mapbt, f'')), app(leaf, app(leaf, x''))) -> APP(app(mapbt, f''), app(leaf, x''))
APP(app(mapbt, app(mapbt, f'''')), app(leaf, app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))) -> APP(app(mapbt, f''''), app(app(app(branch, x''), l''), app(app(app(branch, x''''), l''''), r'''')))
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
POL(branch) = 0 POL(mapbt) = 0 POL(leaf) = 0 POL(app(x1, x2)) = 1 + x2 POL(APP(x1, x2)) = x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Remaining Obligation(s)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), r)
APP(app(mapbt, f), app(app(app(branch, x), l), r)) -> APP(app(mapbt, f), l)
app(app(mapbt, f), app(leaf, x)) -> app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) -> app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))
innermost