YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , subtrees(@t) -> subtrees#1(@t) , subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { subtrees#1(leaf()) -> nil() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2}, Uargs(subtrees#2) = {1}, Uargs(subtrees#3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [append](x1, x2) = [1] x2 + [0] [append#1](x1, x2) = [1] x2 + [0] [::](x1, x2) = [1] x2 + [0] [nil] = [0] [subtrees](x1) = [2] x1 + [0] [subtrees#1](x1) = [2] x1 + [0] [leaf] = [2] [node](x1, x2, x3) = [1] x2 + [1] x3 + [0] [subtrees#2](x1, x2, x3, x4) = [1] x1 + [2] x3 + [0] [subtrees#3](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [0] This order satisfies following ordering constraints [append(@l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [append#1(@l1, @l2)] [append#1(::(@x, @xs), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [subtrees(@t)] = [2] @t + [0] >= [2] @t + [0] = [subtrees#1(@t)] [subtrees#1(leaf())] = [4] > [0] = [nil()] [subtrees#1(node(@x, @t1, @t2))] = [2] @t1 + [2] @t2 + [0] >= [2] @t1 + [2] @t2 + [0] = [subtrees#2(subtrees(@t1), @t1, @t2, @x)] [subtrees#2(@l1, @t1, @t2, @x)] = [1] @l1 + [2] @t2 + [0] >= [1] @l1 + [2] @t2 + [0] = [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)] [subtrees#3(@l2, @l1, @t1, @t2, @x)] = [1] @l1 + [1] @l2 + [0] >= [1] @l2 + [0] = [::(node(@x, @t1, @t2), append(@l1, @l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , subtrees(@t) -> subtrees#1(@t) , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Weak Trs: { subtrees#1(leaf()) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2}, Uargs(subtrees#2) = {1}, Uargs(subtrees#3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [append](x1, x2) = [1] x2 + [0] [append#1](x1, x2) = [1] x2 + [0] [::](x1, x2) = [1] x2 + [0] [nil] = [0] [subtrees](x1) = [1] x1 + [0] [subtrees#1](x1) = [1] x1 + [0] [leaf] = [0] [node](x1, x2, x3) = [1] x2 + [1] x3 + [1] [subtrees#2](x1, x2, x3, x4) = [1] x1 + [1] x3 + [0] [subtrees#3](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [0] This order satisfies following ordering constraints [append(@l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [append#1(@l1, @l2)] [append#1(::(@x, @xs), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [subtrees(@t)] = [1] @t + [0] >= [1] @t + [0] = [subtrees#1(@t)] [subtrees#1(leaf())] = [0] >= [0] = [nil()] [subtrees#1(node(@x, @t1, @t2))] = [1] @t1 + [1] @t2 + [1] > [1] @t1 + [1] @t2 + [0] = [subtrees#2(subtrees(@t1), @t1, @t2, @x)] [subtrees#2(@l1, @t1, @t2, @x)] = [1] @l1 + [1] @t2 + [0] >= [1] @l1 + [1] @t2 + [0] = [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)] [subtrees#3(@l2, @l1, @t1, @t2, @x)] = [1] @l1 + [1] @l2 + [0] >= [1] @l2 + [0] = [::(node(@x, @t1, @t2), append(@l1, @l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , subtrees(@t) -> subtrees#1(@t) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Weak Trs: { subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2}, Uargs(subtrees#2) = {1}, Uargs(subtrees#3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [append](x1, x2) = [1] x2 + [0] [append#1](x1, x2) = [1] x2 + [0] [::](x1, x2) = [1] x2 + [0] [nil] = [0] [subtrees](x1) = [1] x1 + [0] [subtrees#1](x1) = [1] x1 + [0] [leaf] = [0] [node](x1, x2, x3) = [1] x2 + [1] x3 + [2] [subtrees#2](x1, x2, x3, x4) = [1] x1 + [1] x3 + [1] [subtrees#3](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [0] This order satisfies following ordering constraints [append(@l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [append#1(@l1, @l2)] [append#1(::(@x, @xs), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [subtrees(@t)] = [1] @t + [0] >= [1] @t + [0] = [subtrees#1(@t)] [subtrees#1(leaf())] = [0] >= [0] = [nil()] [subtrees#1(node(@x, @t1, @t2))] = [1] @t1 + [1] @t2 + [2] > [1] @t1 + [1] @t2 + [1] = [subtrees#2(subtrees(@t1), @t1, @t2, @x)] [subtrees#2(@l1, @t1, @t2, @x)] = [1] @l1 + [1] @t2 + [1] > [1] @l1 + [1] @t2 + [0] = [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)] [subtrees#3(@l2, @l1, @t1, @t2, @x)] = [1] @l1 + [1] @l2 + [0] >= [1] @l2 + [0] = [::(node(@x, @t1, @t2), append(@l1, @l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , subtrees(@t) -> subtrees#1(@t) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Weak Trs: { subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { subtrees(@t) -> subtrees#1(@t) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2}, Uargs(subtrees#2) = {1}, Uargs(subtrees#3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [append](x1, x2) = [1] x1 + [1] x2 + [0] [append#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x2 + [1] [nil] = [0] [subtrees](x1) = [2] x1 + [1] [subtrees#1](x1) = [2] x1 + [0] [leaf] = [2] [node](x1, x2, x3) = [1] x2 + [1] x3 + [2] [subtrees#2](x1, x2, x3, x4) = [1] x1 + [2] x3 + [2] [subtrees#3](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [1] This order satisfies following ordering constraints [append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] >= [1] @l1 + [1] @l2 + [0] = [append#1(@l1, @l2)] [append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [1] >= [1] @l2 + [1] @xs + [1] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [subtrees(@t)] = [2] @t + [1] > [2] @t + [0] = [subtrees#1(@t)] [subtrees#1(leaf())] = [4] > [0] = [nil()] [subtrees#1(node(@x, @t1, @t2))] = [2] @t1 + [2] @t2 + [4] > [2] @t1 + [2] @t2 + [3] = [subtrees#2(subtrees(@t1), @t1, @t2, @x)] [subtrees#2(@l1, @t1, @t2, @x)] = [1] @l1 + [2] @t2 + [2] >= [1] @l1 + [2] @t2 + [2] = [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)] [subtrees#3(@l2, @l1, @t1, @t2, @x)] = [1] @l1 + [1] @l2 + [1] >= [1] @l1 + [1] @l2 + [1] = [::(node(@x, @t1, @t2), append(@l1, @l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Weak Trs: { subtrees(@t) -> subtrees#1(@t) , subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2}, Uargs(subtrees#2) = {1}, Uargs(subtrees#3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [append](x1, x2) = [1] x2 + [0] [append#1](x1, x2) = [1] x2 + [0] [::](x1, x2) = [1] x2 + [0] [nil] = [0] [subtrees](x1) = [1] x1 + [0] [subtrees#1](x1) = [1] x1 + [0] [leaf] = [0] [node](x1, x2, x3) = [1] x2 + [1] x3 + [2] [subtrees#2](x1, x2, x3, x4) = [1] x1 + [1] x3 + [1] [subtrees#3](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [1] This order satisfies following ordering constraints [append(@l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [append#1(@l1, @l2)] [append#1(::(@x, @xs), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [subtrees(@t)] = [1] @t + [0] >= [1] @t + [0] = [subtrees#1(@t)] [subtrees#1(leaf())] = [0] >= [0] = [nil()] [subtrees#1(node(@x, @t1, @t2))] = [1] @t1 + [1] @t2 + [2] > [1] @t1 + [1] @t2 + [1] = [subtrees#2(subtrees(@t1), @t1, @t2, @x)] [subtrees#2(@l1, @t1, @t2, @x)] = [1] @l1 + [1] @t2 + [1] >= [1] @l1 + [1] @t2 + [1] = [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)] [subtrees#3(@l2, @l1, @t1, @t2, @x)] = [1] @l1 + [1] @l2 + [1] > [1] @l2 + [0] = [::(node(@x, @t1, @t2), append(@l1, @l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 } Weak Trs: { subtrees(@t) -> subtrees#1(@t) , subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { append#1(nil(), @l2) -> @l2 } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2}, Uargs(subtrees#2) = {1}, Uargs(subtrees#3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [append](x1, x2) = [1] x1 + [1] x2 + [0] [append#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x2 + [2] [nil] = [1] [subtrees](x1) = [2] x1 + [0] [subtrees#1](x1) = [2] x1 + [0] [leaf] = [1] [node](x1, x2, x3) = [1] x2 + [1] x3 + [1] [subtrees#2](x1, x2, x3, x4) = [1] x1 + [2] x3 + [2] [subtrees#3](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [2] This order satisfies following ordering constraints [append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] >= [1] @l1 + [1] @l2 + [0] = [append#1(@l1, @l2)] [append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [2] >= [1] @l2 + [1] @xs + [2] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [1] > [1] @l2 + [0] = [@l2] [subtrees(@t)] = [2] @t + [0] >= [2] @t + [0] = [subtrees#1(@t)] [subtrees#1(leaf())] = [2] > [1] = [nil()] [subtrees#1(node(@x, @t1, @t2))] = [2] @t1 + [2] @t2 + [2] >= [2] @t1 + [2] @t2 + [2] = [subtrees#2(subtrees(@t1), @t1, @t2, @x)] [subtrees#2(@l1, @t1, @t2, @x)] = [1] @l1 + [2] @t2 + [2] >= [1] @l1 + [2] @t2 + [2] = [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)] [subtrees#3(@l2, @l1, @t1, @t2, @x)] = [1] @l1 + [1] @l2 + [2] >= [1] @l1 + [1] @l2 + [2] = [::(node(@x, @t1, @t2), append(@l1, @l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) } Weak Trs: { append#1(nil(), @l2) -> @l2 , subtrees(@t) -> subtrees#1(@t) , subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2}, Uargs(subtrees#2) = {1}, Uargs(subtrees#3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [append](x1, x2) = [0 2] x1 + [1 0] x2 + [1] [0 1] [0 1] [0] [append#1](x1, x2) = [0 2] x1 + [1 0] x2 + [0] [0 1] [0 1] [0] [::](x1, x2) = [1 0] x2 + [0] [0 1] [1] [nil] = [0] [0] [subtrees](x1) = [1 1] x1 + [0] [0 1] [1] [subtrees#1](x1) = [1 1] x1 + [0] [0 1] [1] [leaf] = [0] [0] [node](x1, x2, x3) = [1 1] x1 + [1 2] x2 + [1 1] x3 + [2] [0 0] [0 1] [0 1] [2] [subtrees#2](x1, x2, x3, x4) = [1 2] x1 + [1 2] x3 + [2] [0 1] [0 1] [2] [subtrees#3](x1, x2, x3, x4, x5) = [1 0] x1 + [1 2] x2 + [0 1] x4 + [2] [0 1] [0 1] [0 0] [1] This order satisfies following ordering constraints [append(@l1, @l2)] = [0 2] @l1 + [1 0] @l2 + [1] [0 1] [0 1] [0] > [0 2] @l1 + [1 0] @l2 + [0] [0 1] [0 1] [0] = [append#1(@l1, @l2)] [append#1(::(@x, @xs), @l2)] = [1 0] @l2 + [0 2] @xs + [2] [0 1] [0 1] [1] > [1 0] @l2 + [0 2] @xs + [1] [0 1] [0 1] [1] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1 0] @l2 + [0] [0 1] [0] >= [1 0] @l2 + [0] [0 1] [0] = [@l2] [subtrees(@t)] = [1 1] @t + [0] [0 1] [1] >= [1 1] @t + [0] [0 1] [1] = [subtrees#1(@t)] [subtrees#1(leaf())] = [0] [1] >= [0] [0] = [nil()] [subtrees#1(node(@x, @t1, @t2))] = [1 3] @t1 + [1 2] @t2 + [1 1] @x + [4] [0 1] [0 1] [0 0] [3] >= [1 3] @t1 + [1 2] @t2 + [4] [0 1] [0 1] [3] = [subtrees#2(subtrees(@t1), @t1, @t2, @x)] [subtrees#2(@l1, @t1, @t2, @x)] = [1 2] @l1 + [1 2] @t2 + [2] [0 1] [0 1] [2] >= [1 2] @l1 + [1 2] @t2 + [2] [0 1] [0 1] [2] = [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)] [subtrees#3(@l2, @l1, @t1, @t2, @x)] = [1 2] @l1 + [1 0] @l2 + [0 1] @t2 + [2] [0 1] [0 1] [0 0] [1] > [0 2] @l1 + [1 0] @l2 + [1] [0 1] [0 1] [1] = [::(node(@x, @t1, @t2), append(@l1, @l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , subtrees(@t) -> subtrees#1(@t) , subtrees#1(leaf()) -> nil() , subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x) , subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x) , subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))