MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x f(x,i(x)) -> f(x,x) f(i(x),i(g(x))) -> a() g(x) -> i(x) - Signature: {f/2,g/1} / {a/0,i/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {a,i} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. f(i(x),i(g(x))) -> a() All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x f(x,i(x)) -> f(x,x) g(x) -> i(x) - Signature: {f/2,g/1} / {a/0,i/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {a,i} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) f#(x,y) -> c_2() f#(x,i(x)) -> c_3(f#(x,x)) g#(x) -> c_4() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) f#(x,y) -> c_2() f#(x,i(x)) -> c_3(f#(x,x)) g#(x) -> c_4() - Weak TRS: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x f(x,i(x)) -> f(x,x) g(x) -> i(x) - Signature: {f/2,g/1,f#/2,g#/1} / {a/0,i/1,c_1/3,c_2/0,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {a,i} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: g(x) -> i(x) f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) f#(x,y) -> c_2() f#(x,i(x)) -> c_3(f#(x,x)) g#(x) -> c_4() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) f#(x,y) -> c_2() f#(x,i(x)) -> c_3(f#(x,x)) g#(x) -> c_4() - Weak TRS: g(x) -> i(x) - Signature: {f/2,g/1,f#/2,g#/1} / {a/0,i/1,c_1/3,c_2/0,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {a,i} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4} by application of Pre({2,4}) = {1,3}. Here rules are labelled as follows: 1: f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) 2: f#(x,y) -> c_2() 3: f#(x,i(x)) -> c_3(f#(x,x)) 4: g#(x) -> c_4() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) f#(x,i(x)) -> c_3(f#(x,x)) - Weak DPs: f#(x,y) -> c_2() g#(x) -> c_4() - Weak TRS: g(x) -> i(x) - Signature: {f/2,g/1,f#/2,g#/1} / {a/0,i/1,c_1/3,c_2/0,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {a,i} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) -->_1 f#(x,i(x)) -> c_3(f#(x,x)):2 -->_3 g#(x) -> c_4():4 -->_2 g#(x) -> c_4():4 -->_1 f#(x,y) -> c_2():3 -->_1 f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)):1 2:S:f#(x,i(x)) -> c_3(f#(x,x)) -->_1 f#(x,y) -> c_2():3 -->_1 f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)):1 3:W:f#(x,y) -> c_2() 4:W:g#(x) -> c_4() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: g#(x) -> c_4() 3: f#(x,y) -> c_2() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) f#(x,i(x)) -> c_3(f#(x,x)) - Weak TRS: g(x) -> i(x) - Signature: {f/2,g/1,f#/2,g#/1} / {a/0,i/1,c_1/3,c_2/0,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {a,i} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)) -->_1 f#(x,i(x)) -> c_3(f#(x,x)):2 -->_1 f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)):1 2:S:f#(x,i(x)) -> c_3(f#(x,x)) -->_1 f#(x,x) -> c_1(f#(i(x),g(g(x))),g#(g(x)),g#(x)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(x,x) -> c_1(f#(i(x),g(g(x)))) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: f#(x,x) -> c_1(f#(i(x),g(g(x)))) f#(x,i(x)) -> c_3(f#(x,x)) - Weak TRS: g(x) -> i(x) - Signature: {f/2,g/1,f#/2,g#/1} / {a/0,i/1,c_1/1,c_2/0,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {a,i} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE