MAYBE 872.64/297.03 MAYBE 872.64/297.03 872.64/297.03 We are left with following problem, upon which TcT provides the 872.64/297.03 certificate MAYBE. 872.64/297.03 872.64/297.03 Strict Trs: 872.64/297.03 { and(false(), false()) -> false() 872.64/297.03 , and(false(), true()) -> false() 872.64/297.03 , and(true(), false()) -> false() 872.64/297.03 , and(true(), true()) -> true() 872.64/297.03 , eq(nil(), nil()) -> true() 872.64/297.03 , eq(nil(), cons(T, L)) -> false() 872.64/297.03 , eq(cons(T, L), nil()) -> false() 872.64/297.03 , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) 872.64/297.03 , eq(var(L), var(Lp)) -> eq(L, Lp) 872.64/297.03 , eq(var(L), apply(T, S)) -> false() 872.64/297.03 , eq(var(L), lambda(X, T)) -> false() 872.64/297.03 , eq(apply(T, S), var(L)) -> false() 872.64/297.03 , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) 872.64/297.03 , eq(apply(T, S), lambda(X, Tp)) -> false() 872.64/297.03 , eq(lambda(X, T), var(L)) -> false() 872.64/297.03 , eq(lambda(X, T), apply(Tp, Sp)) -> false() 872.64/297.03 , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) 872.64/297.03 , if(false(), var(K), var(L)) -> var(L) 872.64/297.03 , if(true(), var(K), var(L)) -> var(K) 872.64/297.03 , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) 872.64/297.03 , ren(X, Y, lambda(Z, T)) -> 872.64/297.03 lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), 872.64/297.03 ren(X, 872.64/297.03 Y, 872.64/297.03 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.03 , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } 872.64/297.03 Obligation: 872.64/297.03 runtime complexity 872.64/297.03 Answer: 872.64/297.03 MAYBE 872.64/297.03 872.64/297.03 None of the processors succeeded. 872.64/297.03 872.64/297.03 Details of failed attempt(s): 872.64/297.03 ----------------------------- 872.64/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 872.64/297.03 following reason: 872.64/297.03 872.64/297.03 Computation stopped due to timeout after 297.0 seconds. 872.64/297.03 872.64/297.03 2) 'Best' failed due to the following reason: 872.64/297.03 872.64/297.03 None of the processors succeeded. 872.64/297.03 872.64/297.03 Details of failed attempt(s): 872.64/297.03 ----------------------------- 872.64/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 872.64/297.03 seconds)' failed due to the following reason: 872.64/297.03 872.64/297.03 Computation stopped due to timeout after 148.0 seconds. 872.64/297.03 872.64/297.03 2) 'Best' failed due to the following reason: 872.64/297.03 872.64/297.03 None of the processors succeeded. 872.64/297.03 872.64/297.03 Details of failed attempt(s): 872.64/297.03 ----------------------------- 872.64/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 872.64/297.03 following reason: 872.64/297.03 872.64/297.03 The processor is inapplicable, reason: 872.64/297.03 Processor only applicable for innermost runtime complexity analysis 872.64/297.03 872.64/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 872.64/297.03 to the following reason: 872.64/297.03 872.64/297.03 The processor is inapplicable, reason: 872.64/297.03 Processor only applicable for innermost runtime complexity analysis 872.64/297.03 872.64/297.03 872.64/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 872.64/297.03 failed due to the following reason: 872.64/297.03 872.64/297.03 None of the processors succeeded. 872.64/297.03 872.64/297.03 Details of failed attempt(s): 872.64/297.03 ----------------------------- 872.64/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 872.64/297.03 failed due to the following reason: 872.64/297.03 872.64/297.03 match-boundness of the problem could not be verified. 872.64/297.03 872.64/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 872.64/297.03 failed due to the following reason: 872.64/297.03 872.64/297.03 match-boundness of the problem could not be verified. 872.64/297.03 872.64/297.03 872.64/297.03 872.64/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 872.64/297.03 the following reason: 872.64/297.03 872.64/297.03 We add the following weak dependency pairs: 872.64/297.03 872.64/297.03 Strict DPs: 872.64/297.03 { and^#(false(), false()) -> c_1() 872.64/297.03 , and^#(false(), true()) -> c_2() 872.64/297.03 , and^#(true(), false()) -> c_3() 872.64/297.03 , and^#(true(), true()) -> c_4() 872.64/297.03 , eq^#(nil(), nil()) -> c_5() 872.64/297.03 , eq^#(nil(), cons(T, L)) -> c_6() 872.64/297.03 , eq^#(cons(T, L), nil()) -> c_7() 872.64/297.03 , eq^#(cons(T, L), cons(Tp, Lp)) -> 872.64/297.03 c_8(and^#(eq(T, Tp), eq(L, Lp))) 872.64/297.03 , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) 872.64/297.03 , eq^#(var(L), apply(T, S)) -> c_10() 872.64/297.03 , eq^#(var(L), lambda(X, T)) -> c_11() 872.64/297.03 , eq^#(apply(T, S), var(L)) -> c_12() 872.64/297.03 , eq^#(apply(T, S), apply(Tp, Sp)) -> 872.64/297.03 c_13(and^#(eq(T, Tp), eq(S, Sp))) 872.64/297.03 , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() 872.64/297.03 , eq^#(lambda(X, T), var(L)) -> c_15() 872.64/297.03 , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() 872.64/297.03 , eq^#(lambda(X, T), lambda(Xp, Tp)) -> 872.64/297.03 c_17(and^#(eq(T, Tp), eq(X, Xp))) 872.64/297.03 , if^#(false(), var(K), var(L)) -> c_18(L) 872.64/297.03 , if^#(true(), var(K), var(L)) -> c_19(K) 872.64/297.03 , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) 872.64/297.03 , ren^#(X, Y, lambda(Z, T)) -> 872.64/297.03 c_21(X, 872.64/297.03 Y, 872.64/297.03 Z, 872.64/297.03 T, 872.64/297.03 ren^#(X, 872.64/297.03 Y, 872.64/297.03 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.03 , ren^#(var(L), var(K), var(Lp)) -> 872.64/297.03 c_22(if^#(eq(L, Lp), var(K), var(Lp))) } 872.64/297.03 872.64/297.03 and mark the set of starting terms. 872.64/297.03 872.64/297.03 We are left with following problem, upon which TcT provides the 872.64/297.03 certificate MAYBE. 872.64/297.03 872.64/297.03 Strict DPs: 872.64/297.03 { and^#(false(), false()) -> c_1() 872.64/297.03 , and^#(false(), true()) -> c_2() 872.64/297.03 , and^#(true(), false()) -> c_3() 872.64/297.03 , and^#(true(), true()) -> c_4() 872.64/297.03 , eq^#(nil(), nil()) -> c_5() 872.64/297.03 , eq^#(nil(), cons(T, L)) -> c_6() 872.64/297.03 , eq^#(cons(T, L), nil()) -> c_7() 872.64/297.03 , eq^#(cons(T, L), cons(Tp, Lp)) -> 872.64/297.03 c_8(and^#(eq(T, Tp), eq(L, Lp))) 872.64/297.03 , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) 872.64/297.03 , eq^#(var(L), apply(T, S)) -> c_10() 872.64/297.03 , eq^#(var(L), lambda(X, T)) -> c_11() 872.64/297.03 , eq^#(apply(T, S), var(L)) -> c_12() 872.64/297.03 , eq^#(apply(T, S), apply(Tp, Sp)) -> 872.64/297.03 c_13(and^#(eq(T, Tp), eq(S, Sp))) 872.64/297.03 , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() 872.64/297.03 , eq^#(lambda(X, T), var(L)) -> c_15() 872.64/297.03 , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() 872.64/297.03 , eq^#(lambda(X, T), lambda(Xp, Tp)) -> 872.64/297.03 c_17(and^#(eq(T, Tp), eq(X, Xp))) 872.64/297.03 , if^#(false(), var(K), var(L)) -> c_18(L) 872.64/297.03 , if^#(true(), var(K), var(L)) -> c_19(K) 872.64/297.03 , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) 872.64/297.03 , ren^#(X, Y, lambda(Z, T)) -> 872.64/297.03 c_21(X, 872.64/297.03 Y, 872.64/297.03 Z, 872.64/297.03 T, 872.64/297.03 ren^#(X, 872.64/297.03 Y, 872.64/297.03 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.03 , ren^#(var(L), var(K), var(Lp)) -> 872.64/297.03 c_22(if^#(eq(L, Lp), var(K), var(Lp))) } 872.64/297.03 Strict Trs: 872.64/297.03 { and(false(), false()) -> false() 872.64/297.03 , and(false(), true()) -> false() 872.64/297.03 , and(true(), false()) -> false() 872.64/297.03 , and(true(), true()) -> true() 872.64/297.03 , eq(nil(), nil()) -> true() 872.64/297.03 , eq(nil(), cons(T, L)) -> false() 872.64/297.03 , eq(cons(T, L), nil()) -> false() 872.64/297.03 , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) 872.64/297.03 , eq(var(L), var(Lp)) -> eq(L, Lp) 872.64/297.03 , eq(var(L), apply(T, S)) -> false() 872.64/297.03 , eq(var(L), lambda(X, T)) -> false() 872.64/297.03 , eq(apply(T, S), var(L)) -> false() 872.64/297.03 , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) 872.64/297.03 , eq(apply(T, S), lambda(X, Tp)) -> false() 872.64/297.03 , eq(lambda(X, T), var(L)) -> false() 872.64/297.03 , eq(lambda(X, T), apply(Tp, Sp)) -> false() 872.64/297.03 , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) 872.64/297.03 , if(false(), var(K), var(L)) -> var(L) 872.64/297.03 , if(true(), var(K), var(L)) -> var(K) 872.64/297.03 , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) 872.64/297.03 , ren(X, Y, lambda(Z, T)) -> 872.64/297.03 lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), 872.64/297.03 ren(X, 872.64/297.03 Y, 872.64/297.03 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.03 , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } 872.64/297.03 Obligation: 872.64/297.03 runtime complexity 872.64/297.03 Answer: 872.64/297.03 MAYBE 872.64/297.03 872.64/297.03 We estimate the number of application of 872.64/297.03 {1,2,3,4,5,6,7,10,11,12,14,15,16} by applications of 872.64/297.03 Pre({1,2,3,4,5,6,7,10,11,12,14,15,16}) = {8,9,13,17,18,19,21}. Here 872.64/297.03 rules are labeled as follows: 872.64/297.03 872.64/297.03 DPs: 872.64/297.03 { 1: and^#(false(), false()) -> c_1() 872.64/297.03 , 2: and^#(false(), true()) -> c_2() 872.64/297.03 , 3: and^#(true(), false()) -> c_3() 872.64/297.03 , 4: and^#(true(), true()) -> c_4() 872.64/297.03 , 5: eq^#(nil(), nil()) -> c_5() 872.64/297.03 , 6: eq^#(nil(), cons(T, L)) -> c_6() 872.64/297.03 , 7: eq^#(cons(T, L), nil()) -> c_7() 872.64/297.03 , 8: eq^#(cons(T, L), cons(Tp, Lp)) -> 872.64/297.03 c_8(and^#(eq(T, Tp), eq(L, Lp))) 872.64/297.03 , 9: eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) 872.64/297.03 , 10: eq^#(var(L), apply(T, S)) -> c_10() 872.64/297.03 , 11: eq^#(var(L), lambda(X, T)) -> c_11() 872.64/297.03 , 12: eq^#(apply(T, S), var(L)) -> c_12() 872.64/297.03 , 13: eq^#(apply(T, S), apply(Tp, Sp)) -> 872.64/297.03 c_13(and^#(eq(T, Tp), eq(S, Sp))) 872.64/297.03 , 14: eq^#(apply(T, S), lambda(X, Tp)) -> c_14() 872.64/297.03 , 15: eq^#(lambda(X, T), var(L)) -> c_15() 872.64/297.03 , 16: eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() 872.64/297.03 , 17: eq^#(lambda(X, T), lambda(Xp, Tp)) -> 872.64/297.03 c_17(and^#(eq(T, Tp), eq(X, Xp))) 872.64/297.03 , 18: if^#(false(), var(K), var(L)) -> c_18(L) 872.64/297.03 , 19: if^#(true(), var(K), var(L)) -> c_19(K) 872.64/297.03 , 20: ren^#(X, Y, apply(T, S)) -> 872.64/297.03 c_20(ren^#(X, Y, T), ren^#(X, Y, S)) 872.64/297.03 , 21: ren^#(X, Y, lambda(Z, T)) -> 872.64/297.03 c_21(X, 872.64/297.03 Y, 872.64/297.03 Z, 872.64/297.03 T, 872.64/297.03 ren^#(X, 872.64/297.03 Y, 872.64/297.03 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.03 , 22: ren^#(var(L), var(K), var(Lp)) -> 872.64/297.03 c_22(if^#(eq(L, Lp), var(K), var(Lp))) } 872.64/297.03 872.64/297.03 We are left with following problem, upon which TcT provides the 872.64/297.03 certificate MAYBE. 872.64/297.03 872.64/297.03 Strict DPs: 872.64/297.03 { eq^#(cons(T, L), cons(Tp, Lp)) -> 872.64/297.03 c_8(and^#(eq(T, Tp), eq(L, Lp))) 872.64/297.03 , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) 872.64/297.03 , eq^#(apply(T, S), apply(Tp, Sp)) -> 872.64/297.03 c_13(and^#(eq(T, Tp), eq(S, Sp))) 872.64/297.03 , eq^#(lambda(X, T), lambda(Xp, Tp)) -> 872.64/297.03 c_17(and^#(eq(T, Tp), eq(X, Xp))) 872.64/297.03 , if^#(false(), var(K), var(L)) -> c_18(L) 872.64/297.03 , if^#(true(), var(K), var(L)) -> c_19(K) 872.64/297.03 , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) 872.64/297.03 , ren^#(X, Y, lambda(Z, T)) -> 872.64/297.03 c_21(X, 872.64/297.03 Y, 872.64/297.03 Z, 872.64/297.03 T, 872.64/297.03 ren^#(X, 872.64/297.03 Y, 872.64/297.03 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.03 , ren^#(var(L), var(K), var(Lp)) -> 872.64/297.03 c_22(if^#(eq(L, Lp), var(K), var(Lp))) } 872.64/297.03 Strict Trs: 872.64/297.03 { and(false(), false()) -> false() 872.64/297.03 , and(false(), true()) -> false() 872.64/297.04 , and(true(), false()) -> false() 872.64/297.04 , and(true(), true()) -> true() 872.64/297.04 , eq(nil(), nil()) -> true() 872.64/297.04 , eq(nil(), cons(T, L)) -> false() 872.64/297.04 , eq(cons(T, L), nil()) -> false() 872.64/297.04 , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) 872.64/297.04 , eq(var(L), var(Lp)) -> eq(L, Lp) 872.64/297.04 , eq(var(L), apply(T, S)) -> false() 872.64/297.04 , eq(var(L), lambda(X, T)) -> false() 872.64/297.04 , eq(apply(T, S), var(L)) -> false() 872.64/297.04 , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) 872.64/297.04 , eq(apply(T, S), lambda(X, Tp)) -> false() 872.64/297.04 , eq(lambda(X, T), var(L)) -> false() 872.64/297.04 , eq(lambda(X, T), apply(Tp, Sp)) -> false() 872.64/297.04 , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) 872.64/297.04 , if(false(), var(K), var(L)) -> var(L) 872.64/297.04 , if(true(), var(K), var(L)) -> var(K) 872.64/297.04 , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) 872.64/297.04 , ren(X, Y, lambda(Z, T)) -> 872.64/297.04 lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), 872.64/297.04 ren(X, 872.64/297.04 Y, 872.64/297.04 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.04 , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } 872.64/297.04 Weak DPs: 872.64/297.04 { and^#(false(), false()) -> c_1() 872.64/297.04 , and^#(false(), true()) -> c_2() 872.64/297.04 , and^#(true(), false()) -> c_3() 872.64/297.04 , and^#(true(), true()) -> c_4() 872.64/297.04 , eq^#(nil(), nil()) -> c_5() 872.64/297.04 , eq^#(nil(), cons(T, L)) -> c_6() 872.64/297.04 , eq^#(cons(T, L), nil()) -> c_7() 872.64/297.04 , eq^#(var(L), apply(T, S)) -> c_10() 872.64/297.04 , eq^#(var(L), lambda(X, T)) -> c_11() 872.64/297.04 , eq^#(apply(T, S), var(L)) -> c_12() 872.64/297.04 , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() 872.64/297.04 , eq^#(lambda(X, T), var(L)) -> c_15() 872.64/297.04 , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() } 872.64/297.04 Obligation: 872.64/297.04 runtime complexity 872.64/297.04 Answer: 872.64/297.04 MAYBE 872.64/297.04 872.64/297.04 We estimate the number of application of {1,3,4} by applications of 872.64/297.04 Pre({1,3,4}) = {2,5,6,8}. Here rules are labeled as follows: 872.64/297.04 872.64/297.04 DPs: 872.64/297.04 { 1: eq^#(cons(T, L), cons(Tp, Lp)) -> 872.64/297.04 c_8(and^#(eq(T, Tp), eq(L, Lp))) 872.64/297.04 , 2: eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) 872.64/297.04 , 3: eq^#(apply(T, S), apply(Tp, Sp)) -> 872.64/297.04 c_13(and^#(eq(T, Tp), eq(S, Sp))) 872.64/297.04 , 4: eq^#(lambda(X, T), lambda(Xp, Tp)) -> 872.64/297.04 c_17(and^#(eq(T, Tp), eq(X, Xp))) 872.64/297.04 , 5: if^#(false(), var(K), var(L)) -> c_18(L) 872.64/297.04 , 6: if^#(true(), var(K), var(L)) -> c_19(K) 872.64/297.04 , 7: ren^#(X, Y, apply(T, S)) -> 872.64/297.04 c_20(ren^#(X, Y, T), ren^#(X, Y, S)) 872.64/297.04 , 8: ren^#(X, Y, lambda(Z, T)) -> 872.64/297.04 c_21(X, 872.64/297.04 Y, 872.64/297.04 Z, 872.64/297.04 T, 872.64/297.04 ren^#(X, 872.64/297.04 Y, 872.64/297.04 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.04 , 9: ren^#(var(L), var(K), var(Lp)) -> 872.64/297.04 c_22(if^#(eq(L, Lp), var(K), var(Lp))) 872.64/297.04 , 10: and^#(false(), false()) -> c_1() 872.64/297.04 , 11: and^#(false(), true()) -> c_2() 872.64/297.04 , 12: and^#(true(), false()) -> c_3() 872.64/297.04 , 13: and^#(true(), true()) -> c_4() 872.64/297.04 , 14: eq^#(nil(), nil()) -> c_5() 872.64/297.04 , 15: eq^#(nil(), cons(T, L)) -> c_6() 872.64/297.04 , 16: eq^#(cons(T, L), nil()) -> c_7() 872.64/297.04 , 17: eq^#(var(L), apply(T, S)) -> c_10() 872.64/297.04 , 18: eq^#(var(L), lambda(X, T)) -> c_11() 872.64/297.04 , 19: eq^#(apply(T, S), var(L)) -> c_12() 872.64/297.04 , 20: eq^#(apply(T, S), lambda(X, Tp)) -> c_14() 872.64/297.04 , 21: eq^#(lambda(X, T), var(L)) -> c_15() 872.64/297.04 , 22: eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() } 872.64/297.04 872.64/297.04 We are left with following problem, upon which TcT provides the 872.64/297.04 certificate MAYBE. 872.64/297.04 872.64/297.04 Strict DPs: 872.64/297.04 { eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) 872.64/297.04 , if^#(false(), var(K), var(L)) -> c_18(L) 872.64/297.04 , if^#(true(), var(K), var(L)) -> c_19(K) 872.64/297.04 , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) 872.64/297.04 , ren^#(X, Y, lambda(Z, T)) -> 872.64/297.04 c_21(X, 872.64/297.04 Y, 872.64/297.04 Z, 872.64/297.04 T, 872.64/297.04 ren^#(X, 872.64/297.04 Y, 872.64/297.04 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.04 , ren^#(var(L), var(K), var(Lp)) -> 872.64/297.04 c_22(if^#(eq(L, Lp), var(K), var(Lp))) } 872.64/297.04 Strict Trs: 872.64/297.04 { and(false(), false()) -> false() 872.64/297.04 , and(false(), true()) -> false() 872.64/297.04 , and(true(), false()) -> false() 872.64/297.04 , and(true(), true()) -> true() 872.64/297.04 , eq(nil(), nil()) -> true() 872.64/297.04 , eq(nil(), cons(T, L)) -> false() 872.64/297.04 , eq(cons(T, L), nil()) -> false() 872.64/297.04 , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) 872.64/297.04 , eq(var(L), var(Lp)) -> eq(L, Lp) 872.64/297.04 , eq(var(L), apply(T, S)) -> false() 872.64/297.04 , eq(var(L), lambda(X, T)) -> false() 872.64/297.04 , eq(apply(T, S), var(L)) -> false() 872.64/297.04 , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) 872.64/297.04 , eq(apply(T, S), lambda(X, Tp)) -> false() 872.64/297.04 , eq(lambda(X, T), var(L)) -> false() 872.64/297.04 , eq(lambda(X, T), apply(Tp, Sp)) -> false() 872.64/297.04 , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) 872.64/297.04 , if(false(), var(K), var(L)) -> var(L) 872.64/297.04 , if(true(), var(K), var(L)) -> var(K) 872.64/297.04 , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) 872.64/297.04 , ren(X, Y, lambda(Z, T)) -> 872.64/297.04 lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), 872.64/297.04 ren(X, 872.64/297.04 Y, 872.64/297.04 ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) 872.64/297.04 , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } 872.64/297.04 Weak DPs: 872.64/297.04 { and^#(false(), false()) -> c_1() 872.64/297.04 , and^#(false(), true()) -> c_2() 872.64/297.04 , and^#(true(), false()) -> c_3() 872.64/297.04 , and^#(true(), true()) -> c_4() 872.64/297.04 , eq^#(nil(), nil()) -> c_5() 872.64/297.04 , eq^#(nil(), cons(T, L)) -> c_6() 872.64/297.04 , eq^#(cons(T, L), nil()) -> c_7() 872.64/297.04 , eq^#(cons(T, L), cons(Tp, Lp)) -> 872.64/297.04 c_8(and^#(eq(T, Tp), eq(L, Lp))) 872.64/297.04 , eq^#(var(L), apply(T, S)) -> c_10() 872.64/297.04 , eq^#(var(L), lambda(X, T)) -> c_11() 872.64/297.04 , eq^#(apply(T, S), var(L)) -> c_12() 872.64/297.04 , eq^#(apply(T, S), apply(Tp, Sp)) -> 872.64/297.04 c_13(and^#(eq(T, Tp), eq(S, Sp))) 872.64/297.04 , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() 872.64/297.04 , eq^#(lambda(X, T), var(L)) -> c_15() 872.64/297.04 , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() 872.64/297.04 , eq^#(lambda(X, T), lambda(Xp, Tp)) -> 872.64/297.04 c_17(and^#(eq(T, Tp), eq(X, Xp))) } 872.64/297.04 Obligation: 872.64/297.04 runtime complexity 872.64/297.04 Answer: 872.64/297.04 MAYBE 872.64/297.04 872.64/297.04 Empty strict component of the problem is NOT empty. 872.64/297.04 872.64/297.04 872.64/297.04 Arrrr.. 872.86/297.20 EOF