MAYBE Problem: isLeaf(leaf()) -> true() isLeaf(cons(u,v)) -> false() left(cons(u,v)) -> u right(cons(u,v)) -> v concat(leaf(),y) -> y concat(cons(u,v),y) -> cons(u,concat(v,y)) less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v) if1(b,true(),u,v) -> false() if1(b,false(),u,v) -> if2(b,u,v) if2(true(),u,v) -> true() if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v))) Proof: DP Processor: DPs: concat#(cons(u,v),y) -> concat#(v,y) less_leaves#(u,v) -> isLeaf#(v) less_leaves#(u,v) -> isLeaf#(u) less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v) if1#(b,false(),u,v) -> if2#(b,u,v) if2#(false(),u,v) -> right#(v) if2#(false(),u,v) -> left#(v) if2#(false(),u,v) -> concat#(left(v),right(v)) if2#(false(),u,v) -> right#(u) if2#(false(),u,v) -> left#(u) if2#(false(),u,v) -> concat#(left(u),right(u)) if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) TRS: isLeaf(leaf()) -> true() isLeaf(cons(u,v)) -> false() left(cons(u,v)) -> u right(cons(u,v)) -> v concat(leaf(),y) -> y concat(cons(u,v),y) -> cons(u,concat(v,y)) less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v) if1(b,true(),u,v) -> false() if1(b,false(),u,v) -> if2(b,u,v) if2(true(),u,v) -> true() if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v))) TDG Processor: DPs: concat#(cons(u,v),y) -> concat#(v,y) less_leaves#(u,v) -> isLeaf#(v) less_leaves#(u,v) -> isLeaf#(u) less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v) if1#(b,false(),u,v) -> if2#(b,u,v) if2#(false(),u,v) -> right#(v) if2#(false(),u,v) -> left#(v) if2#(false(),u,v) -> concat#(left(v),right(v)) if2#(false(),u,v) -> right#(u) if2#(false(),u,v) -> left#(u) if2#(false(),u,v) -> concat#(left(u),right(u)) if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) TRS: isLeaf(leaf()) -> true() isLeaf(cons(u,v)) -> false() left(cons(u,v)) -> u right(cons(u,v)) -> v concat(leaf(),y) -> y concat(cons(u,v),y) -> cons(u,concat(v,y)) less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v) if1(b,true(),u,v) -> false() if1(b,false(),u,v) -> if2(b,u,v) if2(true(),u,v) -> true() if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v))) graph: if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) -> less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v) if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) -> less_leaves#(u,v) -> isLeaf#(u) if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) -> less_leaves#(u,v) -> isLeaf#(v) if2#(false(),u,v) -> concat#(left(v),right(v)) -> concat#(cons(u,v),y) -> concat#(v,y) if2#(false(),u,v) -> concat#(left(u),right(u)) -> concat#(cons(u,v),y) -> concat#(v,y) if1#(b,false(),u,v) -> if2#(b,u,v) -> if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) if1#(b,false(),u,v) -> if2#(b,u,v) -> if2#(false(),u,v) -> concat#(left(u),right(u)) if1#(b,false(),u,v) -> if2#(b,u,v) -> if2#(false(),u,v) -> left#(u) if1#(b,false(),u,v) -> if2#(b,u,v) -> if2#(false(),u,v) -> right#(u) if1#(b,false(),u,v) -> if2#(b,u,v) -> if2#(false(),u,v) -> concat#(left(v),right(v)) if1#(b,false(),u,v) -> if2#(b,u,v) -> if2#(false(),u,v) -> left#(v) if1#(b,false(),u,v) -> if2#(b,u,v) -> if2#(false(),u,v) -> right#(v) less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v) -> if1#(b,false(),u,v) -> if2#(b,u,v) concat#(cons(u,v),y) -> concat#(v,y) -> concat#(cons(u,v),y) -> concat#(v,y) SCC Processor: #sccs: 2 #rules: 4 #arcs: 14/144 DPs: if2#(false(),u,v) -> less_leaves#(concat(left(u),right(u)),concat(left(v),right(v))) less_leaves#(u,v) -> if1#(isLeaf(u),isLeaf(v),u,v) if1#(b,false(),u,v) -> if2#(b,u,v) TRS: isLeaf(leaf()) -> true() isLeaf(cons(u,v)) -> false() left(cons(u,v)) -> u right(cons(u,v)) -> v concat(leaf(),y) -> y concat(cons(u,v),y) -> cons(u,concat(v,y)) less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v) if1(b,true(),u,v) -> false() if1(b,false(),u,v) -> if2(b,u,v) if2(true(),u,v) -> true() if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v))) Open DPs: concat#(cons(u,v),y) -> concat#(v,y) TRS: isLeaf(leaf()) -> true() isLeaf(cons(u,v)) -> false() left(cons(u,v)) -> u right(cons(u,v)) -> v concat(leaf(),y) -> y concat(cons(u,v),y) -> cons(u,concat(v,y)) less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v) if1(b,true(),u,v) -> false() if1(b,false(),u,v) -> if2(b,u,v) if2(true(),u,v) -> true() if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v))) Matrix Interpretation Processor: dim=1 interpretation: [concat#](x0, x1) = x0 + 4, [if2](x0, x1, x2) = 1, [if1](x0, x1, x2, x3) = 1, [less_leaves](x0, x1) = 1, [concat](x0, x1) = 2x0 + 4x1 + 4, [right](x0) = 7x0, [left](x0) = x0 + 4, [false] = 0, [cons](x0, x1) = 2x0 + x1 + 2, [true] = 1, [isLeaf](x0) = 1, [leaf] = 4 orientation: concat#(cons(u,v),y) = 2u + v + 6 >= v + 4 = concat#(v,y) isLeaf(leaf()) = 1 >= 1 = true() isLeaf(cons(u,v)) = 1 >= 0 = false() left(cons(u,v)) = 2u + v + 6 >= u = u right(cons(u,v)) = 14u + 7v + 14 >= v = v concat(leaf(),y) = 4y + 12 >= y = y concat(cons(u,v),y) = 4u + 2v + 4y + 8 >= 2u + 2v + 4y + 6 = cons(u,concat(v,y)) less_leaves(u,v) = 1 >= 1 = if1(isLeaf(u),isLeaf(v),u,v) if1(b,true(),u,v) = 1 >= 0 = false() if1(b,false(),u,v) = 1 >= 1 = if2(b,u,v) if2(true(),u,v) = 1 >= 1 = true() if2(false(),u,v) = 1 >= 1 = less_leaves(concat(left(u),right(u)),concat(left(v),right(v))) problem: DPs: TRS: isLeaf(leaf()) -> true() isLeaf(cons(u,v)) -> false() left(cons(u,v)) -> u right(cons(u,v)) -> v concat(leaf(),y) -> y concat(cons(u,v),y) -> cons(u,concat(v,y)) less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v) if1(b,true(),u,v) -> false() if1(b,false(),u,v) -> if2(b,u,v) if2(true(),u,v) -> true() if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v))) Qed