MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , append3(@l1, @l2) -> append3#1(@l1, @l2) , append3#1(::(@x, @xs), @l2) -> ::(@x, append3(@xs, @l2)) , append3#1(nil(), @l2) -> @l2 , append4(@l1, @l2) -> append4#1(@l1, @l2) , append4#1(::(@x, @xs), @l2) -> ::(@x, append4(@xs, @l2)) , append4#1(nil(), @l2) -> @l2 , attach(@n, @l) -> attach#1(@l, @n) , attach#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach(@n, @xs)) , attach#1(nil(), @n) -> nil() , attach3(@n, @l) -> attach3#1(@l, @n) , attach3#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach3(@n, @xs)) , attach3#1(nil(), @n) -> nil() , attach4(@n, @l) -> attach4#1(@l, @n) , attach4#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach4(@n, @xs)) , attach4#1(nil(), @n) -> nil() , pairs(@l) -> pairs#1(@l) , pairs#1(::(@x, @xs)) -> append(attach(@x, @xs), pairs(@xs)) , pairs#1(nil()) -> nil() , pairs'(@l) -> pairs'#1(@l) , pairs'#1(::(@x, @xs)) -> append(pairs'(@xs), attach(@x, @xs)) , pairs'#1(nil()) -> nil() , pairs_aux(@l, @acc) -> pairs_aux#1(@l, @acc) , pairs_aux#1(::(@x, @xs), @acc) -> pairs_aux(@xs, append(attach(@x, @xs), @acc)) , pairs_aux#1(nil(), @acc) -> @acc , quadruples(@l) -> quadruples#1(@l) , quadruples#1(::(@x, @xs)) -> append4(attach4(@x, triples(@xs)), quadruples(@xs)) , quadruples#1(nil()) -> nil() , triples(@l) -> triples#1(@l) , triples#1(::(@x, @xs)) -> append3(attach3(@x, pairs(@xs)), triples(@xs)) , triples#1(nil()) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { pairs_aux#1(nil(), @acc) -> @acc } 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(append) = {1, 2}, Uargs(::) = {2}, Uargs(append3) = {1, 2}, Uargs(append4) = {1, 2}, Uargs(attach3) = {2}, Uargs(attach4) = {2}, Uargs(pairs_aux) = {2} 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 + [0] [nil] = [0] [append3](x1, x2) = [2] x1 + [2] x2 + [0] [append3#1](x1, x2) = [2] x1 + [2] x2 + [0] [append4](x1, x2) = [2] x1 + [2] x2 + [0] [append4#1](x1, x2) = [2] x1 + [2] x2 + [0] [attach](x1, x2) = [0] [attach#1](x1, x2) = [0] [tuple#2](x1, x2) = [1] x1 + [0] [attach3](x1, x2) = [2] x2 + [0] [attach3#1](x1, x2) = [2] x1 + [0] [attach4](x1, x2) = [2] x2 + [0] [attach4#1](x1, x2) = [2] x1 + [0] [pairs](x1) = [0] [pairs#1](x1) = [0] [pairs'](x1) = [2] x1 + [0] [pairs'#1](x1) = [2] x1 + [0] [pairs_aux](x1, x2) = [2] x2 + [2] [pairs_aux#1](x1, x2) = [2] x2 + [2] [quadruples](x1) = [0] [quadruples#1](x1) = [0] [triples](x1) = [0] [triples#1](x1) = [0] 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 + [0] >= [1] @l2 + [1] @xs + [0] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [append3(@l1, @l2)] = [2] @l1 + [2] @l2 + [0] >= [2] @l1 + [2] @l2 + [0] = [append3#1(@l1, @l2)] [append3#1(::(@x, @xs), @l2)] = [2] @l2 + [2] @xs + [0] >= [2] @l2 + [2] @xs + [0] = [::(@x, append3(@xs, @l2))] [append3#1(nil(), @l2)] = [2] @l2 + [0] >= [1] @l2 + [0] = [@l2] [append4(@l1, @l2)] = [2] @l1 + [2] @l2 + [0] >= [2] @l1 + [2] @l2 + [0] = [append4#1(@l1, @l2)] [append4#1(::(@x, @xs), @l2)] = [2] @l2 + [2] @xs + [0] >= [2] @l2 + [2] @xs + [0] = [::(@x, append4(@xs, @l2))] [append4#1(nil(), @l2)] = [2] @l2 + [0] >= [1] @l2 + [0] = [@l2] [attach(@n, @l)] = [0] >= [0] = [attach#1(@l, @n)] [attach#1(::(@x, @xs), @n)] = [0] >= [0] = [::(tuple#2(@n, @x), attach(@n, @xs))] [attach#1(nil(), @n)] = [0] >= [0] = [nil()] [attach3(@n, @l)] = [2] @l + [0] >= [2] @l + [0] = [attach3#1(@l, @n)] [attach3#1(::(@x, @xs), @n)] = [2] @xs + [0] >= [2] @xs + [0] = [::(tuple#2(@n, @x), attach3(@n, @xs))] [attach3#1(nil(), @n)] = [0] >= [0] = [nil()] [attach4(@n, @l)] = [2] @l + [0] >= [2] @l + [0] = [attach4#1(@l, @n)] [attach4#1(::(@x, @xs), @n)] = [2] @xs + [0] >= [2] @xs + [0] = [::(tuple#2(@n, @x), attach4(@n, @xs))] [attach4#1(nil(), @n)] = [0] >= [0] = [nil()] [pairs(@l)] = [0] >= [0] = [pairs#1(@l)] [pairs#1(::(@x, @xs))] = [0] >= [0] = [append(attach(@x, @xs), pairs(@xs))] [pairs#1(nil())] = [0] >= [0] = [nil()] [pairs'(@l)] = [2] @l + [0] >= [2] @l + [0] = [pairs'#1(@l)] [pairs'#1(::(@x, @xs))] = [2] @xs + [0] >= [2] @xs + [0] = [append(pairs'(@xs), attach(@x, @xs))] [pairs'#1(nil())] = [0] >= [0] = [nil()] [pairs_aux(@l, @acc)] = [2] @acc + [2] >= [2] @acc + [2] = [pairs_aux#1(@l, @acc)] [pairs_aux#1(::(@x, @xs), @acc)] = [2] @acc + [2] >= [2] @acc + [2] = [pairs_aux(@xs, append(attach(@x, @xs), @acc))] [pairs_aux#1(nil(), @acc)] = [2] @acc + [2] > [1] @acc + [0] = [@acc] [quadruples(@l)] = [0] >= [0] = [quadruples#1(@l)] [quadruples#1(::(@x, @xs))] = [0] >= [0] = [append4(attach4(@x, triples(@xs)), quadruples(@xs))] [quadruples#1(nil())] = [0] >= [0] = [nil()] [triples(@l)] = [0] >= [0] = [triples#1(@l)] [triples#1(::(@x, @xs))] = [0] >= [0] = [append3(attach3(@x, pairs(@xs)), triples(@xs))] [triples#1(nil())] = [0] >= [0] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , append3(@l1, @l2) -> append3#1(@l1, @l2) , append3#1(::(@x, @xs), @l2) -> ::(@x, append3(@xs, @l2)) , append3#1(nil(), @l2) -> @l2 , append4(@l1, @l2) -> append4#1(@l1, @l2) , append4#1(::(@x, @xs), @l2) -> ::(@x, append4(@xs, @l2)) , append4#1(nil(), @l2) -> @l2 , attach(@n, @l) -> attach#1(@l, @n) , attach#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach(@n, @xs)) , attach#1(nil(), @n) -> nil() , attach3(@n, @l) -> attach3#1(@l, @n) , attach3#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach3(@n, @xs)) , attach3#1(nil(), @n) -> nil() , attach4(@n, @l) -> attach4#1(@l, @n) , attach4#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach4(@n, @xs)) , attach4#1(nil(), @n) -> nil() , pairs(@l) -> pairs#1(@l) , pairs#1(::(@x, @xs)) -> append(attach(@x, @xs), pairs(@xs)) , pairs#1(nil()) -> nil() , pairs'(@l) -> pairs'#1(@l) , pairs'#1(::(@x, @xs)) -> append(pairs'(@xs), attach(@x, @xs)) , pairs'#1(nil()) -> nil() , pairs_aux(@l, @acc) -> pairs_aux#1(@l, @acc) , pairs_aux#1(::(@x, @xs), @acc) -> pairs_aux(@xs, append(attach(@x, @xs), @acc)) , quadruples(@l) -> quadruples#1(@l) , quadruples#1(::(@x, @xs)) -> append4(attach4(@x, triples(@xs)), quadruples(@xs)) , quadruples#1(nil()) -> nil() , triples(@l) -> triples#1(@l) , triples#1(::(@x, @xs)) -> append3(attach3(@x, pairs(@xs)), triples(@xs)) , triples#1(nil()) -> nil() } Weak Trs: { pairs_aux#1(nil(), @acc) -> @acc } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { pairs'#1(nil()) -> nil() , quadruples#1(nil()) -> 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(append) = {1, 2}, Uargs(::) = {2}, Uargs(append3) = {1, 2}, Uargs(append4) = {1, 2}, Uargs(attach3) = {2}, Uargs(attach4) = {2}, Uargs(pairs_aux) = {2} 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 + [0] [nil] = [0] [append3](x1, x2) = [1] x1 + [1] x2 + [0] [append3#1](x1, x2) = [1] x1 + [1] x2 + [0] [append4](x1, x2) = [1] x1 + [1] x2 + [0] [append4#1](x1, x2) = [1] x1 + [1] x2 + [0] [attach](x1, x2) = [0] [attach#1](x1, x2) = [0] [tuple#2](x1, x2) = [1] x1 + [0] [attach3](x1, x2) = [2] x2 + [0] [attach3#1](x1, x2) = [2] x1 + [0] [attach4](x1, x2) = [1] x2 + [0] [attach4#1](x1, x2) = [1] x1 + [0] [pairs](x1) = [0] [pairs#1](x1) = [0] [pairs'](x1) = [2] [pairs'#1](x1) = [2] [pairs_aux](x1, x2) = [2] x1 + [2] x2 + [0] [pairs_aux#1](x1, x2) = [2] x1 + [2] x2 + [0] [quadruples](x1) = [1] x1 + [2] [quadruples#1](x1) = [1] x1 + [2] [triples](x1) = [0] [triples#1](x1) = [0] 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 + [0] >= [1] @l2 + [1] @xs + [0] = [::(@x, append(@xs, @l2))] [append#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [append3(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] >= [1] @l1 + [1] @l2 + [0] = [append3#1(@l1, @l2)] [append3#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [0] >= [1] @l2 + [1] @xs + [0] = [::(@x, append3(@xs, @l2))] [append3#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [append4(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] >= [1] @l1 + [1] @l2 + [0] = [append4#1(@l1, @l2)] [append4#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [0] >= [1] @l2 + [1] @xs + [0] = [::(@x, append4(@xs, @l2))] [append4#1(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [@l2] [attach(@n, @l)] = [0] >= [0] = [attach#1(@l, @n)] [attach#1(::(@x, @xs), @n)] = [0] >= [0] = [::(tuple#2(@n, @x), attach(@n, @xs))] [attach#1(nil(), @n)] = [0] >= [0] = [nil()] [attach3(@n, @l)] = [2] @l + [0] >= [2] @l + [0] = [attach3#1(@l, @n)] [attach3#1(::(@x, @xs), @n)] = [2] @xs + [0] >= [2] @xs + [0] = [::(tuple#2(@n, @x), attach3(@n, @xs))] [attach3#1(nil(), @n)] = [0] >= [0] = [nil()] [attach4(@n, @l)] = [1] @l + [0] >= [1] @l + [0] = [attach4#1(@l, @n)] [attach4#1(::(@x, @xs), @n)] = [1] @xs + [0] >= [1] @xs + [0] = [::(tuple#2(@n, @x), attach4(@n, @xs))] [attach4#1(nil(), @n)] = [0] >= [0] = [nil()] [pairs(@l)] = [0] >= [0] = [pairs#1(@l)] [pairs#1(::(@x, @xs))] = [0] >= [0] = [append(attach(@x, @xs), pairs(@xs))] [pairs#1(nil())] = [0] >= [0] = [nil()] [pairs'(@l)] = [2] >= [2] = [pairs'#1(@l)] [pairs'#1(::(@x, @xs))] = [2] >= [2] = [append(pairs'(@xs), attach(@x, @xs))] [pairs'#1(nil())] = [2] > [0] = [nil()] [pairs_aux(@l, @acc)] = [2] @acc + [2] @l + [0] >= [2] @acc + [2] @l + [0] = [pairs_aux#1(@l, @acc)] [pairs_aux#1(::(@x, @xs), @acc)] = [2] @acc + [2] @xs + [0] >= [2] @acc + [2] @xs + [0] = [pairs_aux(@xs, append(attach(@x, @xs), @acc))] [pairs_aux#1(nil(), @acc)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [quadruples(@l)] = [1] @l + [2] >= [1] @l + [2] = [quadruples#1(@l)] [quadruples#1(::(@x, @xs))] = [1] @xs + [2] >= [1] @xs + [2] = [append4(attach4(@x, triples(@xs)), quadruples(@xs))] [quadruples#1(nil())] = [2] > [0] = [nil()] [triples(@l)] = [0] >= [0] = [triples#1(@l)] [triples#1(::(@x, @xs))] = [0] >= [0] = [append3(attach3(@x, pairs(@xs)), triples(@xs))] [triples#1(nil())] = [0] >= [0] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { append(@l1, @l2) -> append#1(@l1, @l2) , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) , append#1(nil(), @l2) -> @l2 , append3(@l1, @l2) -> append3#1(@l1, @l2) , append3#1(::(@x, @xs), @l2) -> ::(@x, append3(@xs, @l2)) , append3#1(nil(), @l2) -> @l2 , append4(@l1, @l2) -> append4#1(@l1, @l2) , append4#1(::(@x, @xs), @l2) -> ::(@x, append4(@xs, @l2)) , append4#1(nil(), @l2) -> @l2 , attach(@n, @l) -> attach#1(@l, @n) , attach#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach(@n, @xs)) , attach#1(nil(), @n) -> nil() , attach3(@n, @l) -> attach3#1(@l, @n) , attach3#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach3(@n, @xs)) , attach3#1(nil(), @n) -> nil() , attach4(@n, @l) -> attach4#1(@l, @n) , attach4#1(::(@x, @xs), @n) -> ::(tuple#2(@n, @x), attach4(@n, @xs)) , attach4#1(nil(), @n) -> nil() , pairs(@l) -> pairs#1(@l) , pairs#1(::(@x, @xs)) -> append(attach(@x, @xs), pairs(@xs)) , pairs#1(nil()) -> nil() , pairs'(@l) -> pairs'#1(@l) , pairs'#1(::(@x, @xs)) -> append(pairs'(@xs), attach(@x, @xs)) , pairs_aux(@l, @acc) -> pairs_aux#1(@l, @acc) , pairs_aux#1(::(@x, @xs), @acc) -> pairs_aux(@xs, append(attach(@x, @xs), @acc)) , quadruples(@l) -> quadruples#1(@l) , quadruples#1(::(@x, @xs)) -> append4(attach4(@x, triples(@xs)), quadruples(@xs)) , triples(@l) -> triples#1(@l) , triples#1(::(@x, @xs)) -> append3(attach3(@x, pairs(@xs)), triples(@xs)) , triples#1(nil()) -> nil() } Weak Trs: { pairs'#1(nil()) -> nil() , pairs_aux#1(nil(), @acc) -> @acc , quadruples#1(nil()) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..