MAYBE 124.11/47.58 MAYBE 124.11/47.58 124.11/47.58 We are left with following problem, upon which TcT provides the 124.11/47.58 certificate MAYBE. 124.11/47.58 124.11/47.58 Strict Trs: 124.11/47.58 { half(0()) -> 0() 124.11/47.58 , half(s(0())) -> 0() 124.11/47.58 , half(s(s(x))) -> s(half(x)) 124.11/47.58 , lastbit(0()) -> 0() 124.11/47.58 , lastbit(s(0())) -> s(0()) 124.11/47.58 , lastbit(s(s(x))) -> lastbit(x) 124.11/47.58 , conv(0()) -> cons(nil(), 0()) 124.11/47.58 , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.58 Obligation: 124.11/47.58 runtime complexity 124.11/47.58 Answer: 124.11/47.58 MAYBE 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'Best' failed due to the following reason: 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 124.11/47.58 seconds)' failed due to the following reason: 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'empty' failed due to the following reason: 124.11/47.58 124.11/47.58 Empty strict component of the problem is NOT empty. 124.11/47.58 124.11/47.58 2) 'With Problem ...' failed due to the following reason: 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'empty' failed due to the following reason: 124.11/47.58 124.11/47.58 Empty strict component of the problem is NOT empty. 124.11/47.58 124.11/47.58 2) 'Fastest' failed due to the following reason: 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'With Problem ...' failed due to the following reason: 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'empty' failed due to the following reason: 124.11/47.58 124.11/47.58 Empty strict component of the problem is NOT empty. 124.11/47.58 124.11/47.58 2) 'With Problem ...' failed due to the following reason: 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'empty' failed due to the following reason: 124.11/47.58 124.11/47.58 Empty strict component of the problem is NOT empty. 124.11/47.58 124.11/47.58 2) 'With Problem ...' failed due to the following reason: 124.11/47.58 124.11/47.58 None of the processors succeeded. 124.11/47.58 124.11/47.58 Details of failed attempt(s): 124.11/47.58 ----------------------------- 124.11/47.58 1) 'empty' failed due to the following reason: 124.11/47.58 124.11/47.58 Empty strict component of the problem is NOT empty. 124.11/47.58 124.11/47.58 2) 'With Problem ...' failed due to the following reason: 124.11/47.58 124.11/47.58 We use the processor 'matrix interpretation of dimension 4' to 124.11/47.58 orient following rules strictly. 124.11/47.58 124.11/47.58 Trs: { conv(0()) -> cons(nil(), 0()) } 124.11/47.58 124.11/47.58 The induced complexity on above rules (modulo remaining rules) is 124.11/47.58 YES(?,O(n^4)) . These rules are moved into the corresponding weak 124.11/47.58 component(s). 124.11/47.58 124.11/47.58 Sub-proof: 124.11/47.58 ---------- 124.11/47.58 TcT has computed the following constructor-based matrix 124.11/47.58 interpretation satisfying not(EDA). 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [half](x1) = [0 1 0 0] x1 + [0] 124.11/47.58 [0 1 0 0] [0] 124.11/47.58 [0 1 0 0] [0] 124.11/47.58 124.11/47.58 [0] 124.11/47.58 [0] = [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [s](x1) = [0 0 1 0] x1 + [0] 124.11/47.58 [1 1 0 0] [0] 124.11/47.58 [1 0 1 0] [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [lastbit](x1) = [0 1 0 0] x1 + [0] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 124.11/47.58 [1 0 0 1] [0] 124.11/47.58 [conv](x1) = [0 0 0 0] x1 + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [1 0 0 0] [0] 124.11/47.58 [cons](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0] 124.11/47.58 [0 0 0 0] [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0 0 0 0] [0] 124.11/47.58 124.11/47.58 [0] 124.11/47.58 [nil] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 124.11/47.58 The order satisfies the following ordering constraints: 124.11/47.58 124.11/47.58 [half(0())] = [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 >= [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [half(s(0()))] = [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 >= [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [half(s(s(x)))] = [1 0 0 0] [0] 124.11/47.58 [1 1 0 0] x + [0] 124.11/47.58 [1 1 0 0] [0] 124.11/47.58 [1 1 0 0] [0] 124.11/47.58 >= [1 0 0 0] [0] 124.11/47.58 [0 1 0 0] x + [0] 124.11/47.58 [1 1 0 0] [0] 124.11/47.58 [1 1 0 0] [0] 124.11/47.58 = [s(half(x))] 124.11/47.58 124.11/47.58 [lastbit(0())] = [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 >= [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [lastbit(s(0()))] = [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 >= [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 = [s(0())] 124.11/47.58 124.11/47.58 [lastbit(s(s(x)))] = [1 0 0 0] [0] 124.11/47.58 [1 1 0 0] x + [0] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 >= [1 0 0 0] [0] 124.11/47.58 [0 1 0 0] x + [0] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 = [lastbit(x)] 124.11/47.58 124.11/47.58 [conv(0())] = [1] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 > [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [cons(nil(), 0())] 124.11/47.58 124.11/47.58 [conv(s(x))] = [2 0 1 0] [0] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 >= [2 0 1 0] [0] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 = [cons(conv(half(s(x))), lastbit(s(x)))] 124.11/47.58 124.11/47.58 124.11/47.58 We return to the main proof. 124.11/47.58 124.11/47.58 We are left with following problem, upon which TcT provides the 124.11/47.58 certificate MAYBE. 124.11/47.58 124.11/47.58 Strict Trs: 124.11/47.58 { half(0()) -> 0() 124.11/47.58 , half(s(0())) -> 0() 124.11/47.58 , half(s(s(x))) -> s(half(x)) 124.11/47.58 , lastbit(0()) -> 0() 124.11/47.58 , lastbit(s(0())) -> s(0()) 124.11/47.58 , lastbit(s(s(x))) -> lastbit(x) 124.11/47.58 , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.58 Weak Trs: { conv(0()) -> cons(nil(), 0()) } 124.11/47.58 Obligation: 124.11/47.58 runtime complexity 124.11/47.58 Answer: 124.11/47.58 MAYBE 124.11/47.58 124.11/47.58 We use the processor 'matrix interpretation of dimension 4' to 124.11/47.58 orient following rules strictly. 124.11/47.58 124.11/47.58 Trs: { conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.58 124.11/47.58 The induced complexity on above rules (modulo remaining rules) is 124.11/47.58 YES(?,O(n^4)) . These rules are moved into the corresponding weak 124.11/47.58 component(s). 124.11/47.58 124.11/47.58 Sub-proof: 124.11/47.58 ---------- 124.11/47.58 TcT has computed the following constructor-based matrix 124.11/47.58 interpretation satisfying not(EDA). 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [half](x1) = [0 0 0 1] x1 + [0] 124.11/47.58 [0 0 1 0] [0] 124.11/47.58 [0 0 0 1] [0] 124.11/47.58 124.11/47.58 [0] 124.11/47.58 [0] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [s](x1) = [1 0 1 1] x1 + [1] 124.11/47.58 [1 0 0 0] [1] 124.11/47.58 [0 0 1 1] [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [lastbit](x1) = [0 0 0 0] x1 + [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 124.11/47.58 [1 1 0 0] [0] 124.11/47.58 [conv](x1) = [0 0 0 0] x1 + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [1 0 0 0] [0] 124.11/47.58 [cons](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0] 124.11/47.58 [0 0 0 0] [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0 0 0 0] [0] 124.11/47.58 124.11/47.58 [0] 124.11/47.58 [nil] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 124.11/47.58 The order satisfies the following ordering constraints: 124.11/47.58 124.11/47.58 [half(0())] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [half(s(0()))] = [0] 124.11/47.58 [0] 124.11/47.58 [1] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [half(s(s(x)))] = [1 0 0 0] [0] 124.11/47.58 [1 0 1 1] x + [1] 124.11/47.58 [1 0 0 0] [1] 124.11/47.58 [1 0 1 1] [1] 124.11/47.58 >= [1 0 0 0] [0] 124.11/47.58 [1 0 1 1] x + [1] 124.11/47.58 [1 0 0 0] [1] 124.11/47.58 [0 0 1 1] [0] 124.11/47.58 = [s(half(x))] 124.11/47.58 124.11/47.58 [lastbit(0())] = [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [lastbit(s(0()))] = [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 [0] 124.11/47.58 = [s(0())] 124.11/47.58 124.11/47.58 [lastbit(s(s(x)))] = [1 0 0 0] [0] 124.11/47.58 [0 0 0 0] x + [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 >= [1 0 0 0] [0] 124.11/47.58 [0 0 0 0] x + [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 = [lastbit(x)] 124.11/47.58 124.11/47.58 [conv(0())] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [cons(nil(), 0())] 124.11/47.58 124.11/47.58 [conv(s(x))] = [2 0 1 1] [1] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 > [2 0 1 1] [0] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 = [cons(conv(half(s(x))), lastbit(s(x)))] 124.11/47.58 124.11/47.58 124.11/47.58 We return to the main proof. 124.11/47.58 124.11/47.58 We are left with following problem, upon which TcT provides the 124.11/47.58 certificate MAYBE. 124.11/47.58 124.11/47.58 Strict Trs: 124.11/47.58 { half(0()) -> 0() 124.11/47.58 , half(s(0())) -> 0() 124.11/47.58 , half(s(s(x))) -> s(half(x)) 124.11/47.58 , lastbit(0()) -> 0() 124.11/47.58 , lastbit(s(0())) -> s(0()) 124.11/47.58 , lastbit(s(s(x))) -> lastbit(x) } 124.11/47.58 Weak Trs: 124.11/47.58 { conv(0()) -> cons(nil(), 0()) 124.11/47.58 , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.58 Obligation: 124.11/47.58 runtime complexity 124.11/47.58 Answer: 124.11/47.58 MAYBE 124.11/47.58 124.11/47.58 We use the processor 'matrix interpretation of dimension 4' to 124.11/47.58 orient following rules strictly. 124.11/47.58 124.11/47.58 Trs: 124.11/47.58 { lastbit(0()) -> 0() 124.11/47.58 , lastbit(s(0())) -> s(0()) } 124.11/47.58 124.11/47.58 The induced complexity on above rules (modulo remaining rules) is 124.11/47.58 YES(?,O(n^4)) . These rules are moved into the corresponding weak 124.11/47.58 component(s). 124.11/47.58 124.11/47.58 Sub-proof: 124.11/47.58 ---------- 124.11/47.58 TcT has computed the following constructor-based matrix 124.11/47.58 interpretation satisfying not(EDA). 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [half](x1) = [0 1 0 0] x1 + [0] 124.11/47.58 [0 1 0 0] [0] 124.11/47.58 [0 1 0 0] [0] 124.11/47.58 124.11/47.58 [0] 124.11/47.58 [0] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [s](x1) = [0 0 1 0] x1 + [0] 124.11/47.58 [1 1 0 0] [1] 124.11/47.58 [1 0 1 0] [1] 124.11/47.58 124.11/47.58 [1 0 0 0] [1] 124.11/47.58 [lastbit](x1) = [0 0 0 0] x1 + [0] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 124.11/47.58 [1 0 0 1] [0] 124.11/47.58 [conv](x1) = [0 0 0 0] x1 + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [1 0 0 0] [0] 124.11/47.58 [cons](x1, x2) = [0 0 1 0] x1 + [0 0 0 0] x2 + [0] 124.11/47.58 [0 0 0 0] [0 0 0 0] [0] 124.11/47.58 [0 0 1 0] [0 0 0 0] [0] 124.11/47.58 124.11/47.58 [0] 124.11/47.58 [nil] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 124.11/47.58 The order satisfies the following ordering constraints: 124.11/47.58 124.11/47.58 [half(0())] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [half(s(0()))] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [half(s(s(x)))] = [1 0 0 0] [0] 124.11/47.58 [1 1 0 0] x + [1] 124.11/47.58 [1 1 0 0] [1] 124.11/47.58 [1 1 0 0] [1] 124.11/47.58 >= [1 0 0 0] [0] 124.11/47.58 [0 1 0 0] x + [0] 124.11/47.58 [1 1 0 0] [1] 124.11/47.58 [1 1 0 0] [1] 124.11/47.58 = [s(half(x))] 124.11/47.58 124.11/47.58 [lastbit(0())] = [1] 124.11/47.58 [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 > [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [0()] 124.11/47.58 124.11/47.58 [lastbit(s(0()))] = [1] 124.11/47.58 [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 > [0] 124.11/47.58 [0] 124.11/47.58 [1] 124.11/47.58 [1] 124.11/47.58 = [s(0())] 124.11/47.58 124.11/47.58 [lastbit(s(s(x)))] = [1 0 0 0] [1] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 >= [1 0 0 0] [1] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 [0 0 0 0] [1] 124.11/47.58 = [lastbit(x)] 124.11/47.58 124.11/47.58 [conv(0())] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 >= [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 = [cons(nil(), 0())] 124.11/47.58 124.11/47.58 [conv(s(x))] = [2 0 1 0] [1] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 >= [2 0 1 0] [1] 124.11/47.58 [0 0 0 0] x + [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 [0 0 0 0] [0] 124.11/47.58 = [cons(conv(half(s(x))), lastbit(s(x)))] 124.11/47.58 124.11/47.58 124.11/47.58 We return to the main proof. 124.11/47.58 124.11/47.58 We are left with following problem, upon which TcT provides the 124.11/47.58 certificate MAYBE. 124.11/47.58 124.11/47.58 Strict Trs: 124.11/47.58 { half(0()) -> 0() 124.11/47.58 , half(s(0())) -> 0() 124.11/47.58 , half(s(s(x))) -> s(half(x)) 124.11/47.58 , lastbit(s(s(x))) -> lastbit(x) } 124.11/47.58 Weak Trs: 124.11/47.58 { lastbit(0()) -> 0() 124.11/47.58 , lastbit(s(0())) -> s(0()) 124.11/47.58 , conv(0()) -> cons(nil(), 0()) 124.11/47.58 , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.58 Obligation: 124.11/47.58 runtime complexity 124.11/47.58 Answer: 124.11/47.58 MAYBE 124.11/47.58 124.11/47.58 We use the processor 'matrix interpretation of dimension 4' to 124.11/47.58 orient following rules strictly. 124.11/47.58 124.11/47.58 Trs: 124.11/47.58 { half(s(0())) -> 0() 124.11/47.58 , half(s(s(x))) -> s(half(x)) 124.11/47.58 , lastbit(s(s(x))) -> lastbit(x) } 124.11/47.58 124.11/47.58 The induced complexity on above rules (modulo remaining rules) is 124.11/47.58 YES(?,O(n^4)) . These rules are moved into the corresponding weak 124.11/47.58 component(s). 124.11/47.58 124.11/47.58 Sub-proof: 124.11/47.58 ---------- 124.11/47.58 TcT has computed the following constructor-based matrix 124.11/47.58 interpretation satisfying not(EDA). 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [half](x1) = [0 0 0 1] x1 + [0] 124.11/47.58 [0 0 1 0] [0] 124.11/47.58 [0 1 0 0] [0] 124.11/47.58 124.11/47.58 [0] 124.11/47.58 [0] = [0] 124.11/47.58 [0] 124.11/47.58 [0] 124.11/47.58 124.11/47.58 [1 0 0 0] [1] 124.11/47.58 [s](x1) = [0 0 1 0] x1 + [0] 124.11/47.58 [1 0 1 0] [1] 124.11/47.58 [1 0 1 0] [1] 124.11/47.58 124.11/47.58 [1 0 0 0] [0] 124.11/47.58 [lastbit](x1) = [0 0 0 0] x1 + [0] 124.11/47.58 [0 0 1 0] [0] 124.11/47.59 [1 0 0 0] [0] 124.11/47.59 124.11/47.59 [1 0 0 1] [0] 124.11/47.59 [conv](x1) = [0 0 0 0] x1 + [0] 124.11/47.59 [0 0 0 0] [0] 124.11/47.59 [0 0 0 0] [0] 124.11/47.59 124.11/47.59 [1 0 0 0] [1 0 0 0] [0] 124.11/47.59 [cons](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0] 124.11/47.59 [0 0 0 0] [0 0 0 0] [0] 124.11/47.59 [0 0 0 0] [0 0 0 0] [0] 124.11/47.59 124.11/47.59 [0] 124.11/47.59 [nil] = [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 124.11/47.59 The order satisfies the following ordering constraints: 124.11/47.59 124.11/47.59 [half(0())] = [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 >= [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 = [0()] 124.11/47.59 124.11/47.59 [half(s(0()))] = [1] 124.11/47.59 [1] 124.11/47.59 [1] 124.11/47.59 [0] 124.11/47.59 > [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 = [0()] 124.11/47.59 124.11/47.59 [half(s(s(x)))] = [1 0 0 0] [2] 124.11/47.59 [2 0 1 0] x + [3] 124.11/47.59 [2 0 1 0] [3] 124.11/47.59 [1 0 1 0] [1] 124.11/47.59 > [1 0 0 0] [1] 124.11/47.59 [0 0 1 0] x + [0] 124.11/47.59 [1 0 1 0] [1] 124.11/47.59 [1 0 1 0] [1] 124.11/47.59 = [s(half(x))] 124.11/47.59 124.11/47.59 [lastbit(0())] = [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 >= [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 = [0()] 124.11/47.59 124.11/47.59 [lastbit(s(0()))] = [1] 124.11/47.59 [0] 124.11/47.59 [1] 124.11/47.59 [1] 124.11/47.59 >= [1] 124.11/47.59 [0] 124.11/47.59 [1] 124.11/47.59 [1] 124.11/47.59 = [s(0())] 124.11/47.59 124.11/47.59 [lastbit(s(s(x)))] = [1 0 0 0] [2] 124.11/47.59 [0 0 0 0] x + [0] 124.11/47.59 [2 0 1 0] [3] 124.11/47.59 [1 0 0 0] [2] 124.11/47.59 > [1 0 0 0] [0] 124.11/47.59 [0 0 0 0] x + [0] 124.11/47.59 [0 0 1 0] [0] 124.11/47.59 [1 0 0 0] [0] 124.11/47.59 = [lastbit(x)] 124.11/47.59 124.11/47.59 [conv(0())] = [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 >= [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 [0] 124.11/47.59 = [cons(nil(), 0())] 124.11/47.59 124.11/47.59 [conv(s(x))] = [2 0 1 0] [2] 124.11/47.59 [0 0 0 0] x + [0] 124.11/47.59 [0 0 0 0] [0] 124.11/47.59 [0 0 0 0] [0] 124.11/47.59 >= [2 0 1 0] [2] 124.11/47.59 [0 0 0 0] x + [0] 124.11/47.59 [0 0 0 0] [0] 124.11/47.59 [0 0 0 0] [0] 124.11/47.59 = [cons(conv(half(s(x))), lastbit(s(x)))] 124.11/47.59 124.11/47.59 124.11/47.59 We return to the main proof. 124.11/47.59 124.11/47.59 We are left with following problem, upon which TcT provides the 124.11/47.59 certificate MAYBE. 124.11/47.59 124.11/47.59 Strict Trs: { half(0()) -> 0() } 124.11/47.59 Weak Trs: 124.11/47.59 { half(s(0())) -> 0() 124.11/47.59 , half(s(s(x))) -> s(half(x)) 124.11/47.59 , lastbit(0()) -> 0() 124.11/47.59 , lastbit(s(0())) -> s(0()) 124.11/47.59 , lastbit(s(s(x))) -> lastbit(x) 124.11/47.59 , conv(0()) -> cons(nil(), 0()) 124.11/47.59 , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.59 Obligation: 124.11/47.59 runtime complexity 124.11/47.59 Answer: 124.11/47.59 MAYBE 124.11/47.59 124.11/47.59 Empty strict component of the problem is NOT empty. 124.11/47.59 124.11/47.59 124.11/47.59 124.11/47.59 124.11/47.59 2) 'With Problem ...' failed due to the following reason: 124.11/47.59 124.11/47.59 None of the processors succeeded. 124.11/47.59 124.11/47.59 Details of failed attempt(s): 124.11/47.59 ----------------------------- 124.11/47.59 1) 'empty' failed due to the following reason: 124.11/47.59 124.11/47.59 Empty strict component of the problem is NOT empty. 124.11/47.59 124.11/47.59 2) 'With Problem ...' failed due to the following reason: 124.11/47.59 124.11/47.59 Empty strict component of the problem is NOT empty. 124.11/47.59 124.11/47.59 124.11/47.59 124.11/47.59 124.11/47.59 124.11/47.59 2) 'Best' failed due to the following reason: 124.11/47.59 124.11/47.59 None of the processors succeeded. 124.11/47.59 124.11/47.59 Details of failed attempt(s): 124.11/47.59 ----------------------------- 124.11/47.59 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 124.11/47.59 following reason: 124.11/47.59 124.11/47.59 The processor is inapplicable, reason: 124.11/47.59 Processor only applicable for innermost runtime complexity analysis 124.11/47.59 124.11/47.59 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 124.11/47.59 to the following reason: 124.11/47.59 124.11/47.59 The processor is inapplicable, reason: 124.11/47.59 Processor only applicable for innermost runtime complexity analysis 124.11/47.59 124.11/47.59 124.11/47.59 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 124.11/47.59 failed due to the following reason: 124.11/47.59 124.11/47.59 None of the processors succeeded. 124.11/47.59 124.11/47.59 Details of failed attempt(s): 124.11/47.59 ----------------------------- 124.11/47.59 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 124.11/47.59 failed due to the following reason: 124.11/47.59 124.11/47.59 match-boundness of the problem could not be verified. 124.11/47.59 124.11/47.59 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 124.11/47.59 failed due to the following reason: 124.11/47.59 124.11/47.59 match-boundness of the problem could not be verified. 124.11/47.59 124.11/47.59 124.11/47.59 124.11/47.59 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 124.11/47.59 the following reason: 124.11/47.59 124.11/47.59 We add the following weak dependency pairs: 124.11/47.59 124.11/47.59 Strict DPs: 124.11/47.59 { half^#(0()) -> c_1() 124.11/47.59 , half^#(s(0())) -> c_2() 124.11/47.59 , half^#(s(s(x))) -> c_3(half^#(x)) 124.11/47.59 , lastbit^#(0()) -> c_4() 124.11/47.59 , lastbit^#(s(0())) -> c_5() 124.11/47.59 , lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) 124.11/47.59 , conv^#(0()) -> c_7() 124.11/47.59 , conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x))) } 124.11/47.59 124.11/47.59 and mark the set of starting terms. 124.11/47.59 124.11/47.59 We are left with following problem, upon which TcT provides the 124.11/47.59 certificate MAYBE. 124.11/47.59 124.11/47.59 Strict DPs: 124.11/47.59 { half^#(0()) -> c_1() 124.11/47.59 , half^#(s(0())) -> c_2() 124.11/47.59 , half^#(s(s(x))) -> c_3(half^#(x)) 124.11/47.59 , lastbit^#(0()) -> c_4() 124.11/47.59 , lastbit^#(s(0())) -> c_5() 124.11/47.59 , lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) 124.11/47.59 , conv^#(0()) -> c_7() 124.11/47.59 , conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x))) } 124.11/47.59 Strict Trs: 124.11/47.59 { half(0()) -> 0() 124.11/47.59 , half(s(0())) -> 0() 124.11/47.59 , half(s(s(x))) -> s(half(x)) 124.11/47.59 , lastbit(0()) -> 0() 124.11/47.59 , lastbit(s(0())) -> s(0()) 124.11/47.59 , lastbit(s(s(x))) -> lastbit(x) 124.11/47.59 , conv(0()) -> cons(nil(), 0()) 124.11/47.59 , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.59 Obligation: 124.11/47.59 runtime complexity 124.11/47.59 Answer: 124.11/47.59 MAYBE 124.11/47.59 124.11/47.59 We estimate the number of application of {1,2,4,5,7} by 124.11/47.59 applications of Pre({1,2,4,5,7}) = {3,6,8}. Here rules are labeled 124.11/47.59 as follows: 124.11/47.59 124.11/47.59 DPs: 124.11/47.59 { 1: half^#(0()) -> c_1() 124.11/47.59 , 2: half^#(s(0())) -> c_2() 124.11/47.59 , 3: half^#(s(s(x))) -> c_3(half^#(x)) 124.11/47.59 , 4: lastbit^#(0()) -> c_4() 124.11/47.59 , 5: lastbit^#(s(0())) -> c_5() 124.11/47.59 , 6: lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) 124.11/47.59 , 7: conv^#(0()) -> c_7() 124.11/47.59 , 8: conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x))) } 124.11/47.59 124.11/47.59 We are left with following problem, upon which TcT provides the 124.11/47.59 certificate MAYBE. 124.11/47.59 124.11/47.59 Strict DPs: 124.11/47.59 { half^#(s(s(x))) -> c_3(half^#(x)) 124.11/47.59 , lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) 124.11/47.59 , conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x))) } 124.11/47.59 Strict Trs: 124.11/47.59 { half(0()) -> 0() 124.11/47.59 , half(s(0())) -> 0() 124.11/47.59 , half(s(s(x))) -> s(half(x)) 124.11/47.59 , lastbit(0()) -> 0() 124.11/47.59 , lastbit(s(0())) -> s(0()) 124.11/47.59 , lastbit(s(s(x))) -> lastbit(x) 124.11/47.59 , conv(0()) -> cons(nil(), 0()) 124.11/47.59 , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x))) } 124.11/47.59 Weak DPs: 124.11/47.59 { half^#(0()) -> c_1() 124.11/47.59 , half^#(s(0())) -> c_2() 124.11/47.59 , lastbit^#(0()) -> c_4() 124.11/47.59 , lastbit^#(s(0())) -> c_5() 124.11/47.59 , conv^#(0()) -> c_7() } 124.11/47.59 Obligation: 124.11/47.59 runtime complexity 124.11/47.59 Answer: 124.11/47.59 MAYBE 124.11/47.59 124.11/47.59 Empty strict component of the problem is NOT empty. 124.11/47.59 124.11/47.59 124.11/47.59 Arrrr.. 124.40/47.73 EOF