*** 1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: a__c() -> b() a__c() -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__f(b(),X,c()) -> a__f(X,a__c(),X) mark(b()) -> b() mark(c()) -> a__c() mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) Weak DP Rules: Weak TRS Rules: Signature: {a__c/0,a__f/3,mark/1} / {b/0,c/0,f/3} Obligation: Innermost basic terms: {a__c,a__f,mark}/{b,c,f} Applied Processor: DependencyPairs {dpKind_ = DT} Proof: We add the following dependency tuples: Strict DPs a__c#() -> c_1() a__c#() -> c_2() a__f#(X1,X2,X3) -> c_3() a__f#(b(),X,c()) -> c_4(a__f#(X,a__c(),X),a__c#()) mark#(b()) -> c_5() mark#(c()) -> c_6(a__c#()) mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)) Weak DPs and mark the set of starting terms. *** 1.1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: a__c#() -> c_1() a__c#() -> c_2() a__f#(X1,X2,X3) -> c_3() a__f#(b(),X,c()) -> c_4(a__f#(X,a__c(),X),a__c#()) mark#(b()) -> c_5() mark#(c()) -> c_6(a__c#()) mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)) Strict TRS Rules: Weak DP Rules: Weak TRS Rules: a__c() -> b() a__c() -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__f(b(),X,c()) -> a__f(X,a__c(),X) mark(b()) -> b() mark(c()) -> a__c() mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/2} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} Proof: We estimate the number of application of {1,2,3,5} by application of Pre({1,2,3,5}) = {4,6,7}. Here rules are labelled as follows: 1: a__c#() -> c_1() 2: a__c#() -> c_2() 3: a__f#(X1,X2,X3) -> c_3() 4: a__f#(b(),X,c()) -> c_4(a__f#(X ,a__c() ,X) ,a__c#()) 5: mark#(b()) -> c_5() 6: mark#(c()) -> c_6(a__c#()) 7: mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3) ,mark#(X2)) *** 1.1.1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: a__f#(b(),X,c()) -> c_4(a__f#(X,a__c(),X),a__c#()) mark#(c()) -> c_6(a__c#()) mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)) Strict TRS Rules: Weak DP Rules: a__c#() -> c_1() a__c#() -> c_2() a__f#(X1,X2,X3) -> c_3() mark#(b()) -> c_5() Weak TRS Rules: a__c() -> b() a__c() -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__f(b(),X,c()) -> a__f(X,a__c(),X) mark(b()) -> b() mark(c()) -> a__c() mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/2} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} Proof: We estimate the number of application of {1,2} by application of Pre({1,2}) = {3}. Here rules are labelled as follows: 1: a__f#(b(),X,c()) -> c_4(a__f#(X ,a__c() ,X) ,a__c#()) 2: mark#(c()) -> c_6(a__c#()) 3: mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3) ,mark#(X2)) 4: a__c#() -> c_1() 5: a__c#() -> c_2() 6: a__f#(X1,X2,X3) -> c_3() 7: mark#(b()) -> c_5() *** 1.1.1.1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)) Strict TRS Rules: Weak DP Rules: a__c#() -> c_1() a__c#() -> c_2() a__f#(X1,X2,X3) -> c_3() a__f#(b(),X,c()) -> c_4(a__f#(X,a__c(),X),a__c#()) mark#(b()) -> c_5() mark#(c()) -> c_6(a__c#()) Weak TRS Rules: a__c() -> b() a__c() -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__f(b(),X,c()) -> a__f(X,a__c(),X) mark(b()) -> b() mark(c()) -> a__c() mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/2} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: RemoveWeakSuffixes Proof: Consider the dependency graph 1:S:mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)) -->_2 mark#(c()) -> c_6(a__c#()):7 -->_1 a__f#(b(),X,c()) -> c_4(a__f#(X,a__c(),X),a__c#()):5 -->_2 mark#(b()) -> c_5():6 -->_1 a__f#(X1,X2,X3) -> c_3():4 -->_2 mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)):1 2:W:a__c#() -> c_1() 3:W:a__c#() -> c_2() 4:W:a__f#(X1,X2,X3) -> c_3() 5:W:a__f#(b(),X,c()) -> c_4(a__f#(X,a__c(),X),a__c#()) -->_1 a__f#(X1,X2,X3) -> c_3():4 -->_2 a__c#() -> c_2():3 -->_2 a__c#() -> c_1():2 6:W:mark#(b()) -> c_5() 7:W:mark#(c()) -> c_6(a__c#()) -->_1 a__c#() -> c_2():3 -->_1 a__c#() -> c_1():2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: mark#(b()) -> c_5() 5: a__f#(b(),X,c()) -> c_4(a__f#(X ,a__c() ,X) ,a__c#()) 4: a__f#(X1,X2,X3) -> c_3() 7: mark#(c()) -> c_6(a__c#()) 2: a__c#() -> c_1() 3: a__c#() -> c_2() *** 1.1.1.1.1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)) Strict TRS Rules: Weak DP Rules: Weak TRS Rules: a__c() -> b() a__c() -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__f(b(),X,c()) -> a__f(X,a__c(),X) mark(b()) -> b() mark(c()) -> a__c() mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/2} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: SimplifyRHS Proof: Consider the dependency graph 1:S:mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)) -->_2 mark#(f(X1,X2,X3)) -> c_7(a__f#(X1,mark(X2),X3),mark#(X2)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) *** 1.1.1.1.1.1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) Strict TRS Rules: Weak DP Rules: Weak TRS Rules: a__c() -> b() a__c() -> c() a__f(X1,X2,X3) -> f(X1,X2,X3) a__f(b(),X,c()) -> a__f(X,a__c(),X) mark(b()) -> b() mark(c()) -> a__c() mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: UsableRules Proof: We replace rewrite rules by usable rules: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) *** 1.1.1.1.1.1.1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) Strict TRS Rules: Weak DP Rules: Weak TRS Rules: Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}} Proof: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly: 1: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) The strictly oriented rules are moved into the weak component. *** 1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] *** Considered Problem: Strict DP Rules: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) Strict TRS Rules: Weak DP Rules: Weak TRS Rules: Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy} Proof: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: {a__c#,a__f#,mark#} TcT has computed the following interpretation: p(a__c) = [1] p(a__f) = [1] x1 + [1] x3 + [8] p(b) = [0] p(c) = [1] p(f) = [1] x2 + [6] p(mark) = [1] p(a__c#) = [8] p(a__f#) = [2] x3 + [1] p(mark#) = [3] x1 + [8] p(c_1) = [1] p(c_2) = [1] p(c_3) = [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [1] x1 + [1] p(c_7) = [1] x1 + [10] Following rules are strictly oriented: mark#(f(X1,X2,X3)) = [3] X2 + [26] > [3] X2 + [18] = c_7(mark#(X2)) Following rules are (at-least) weakly oriented: *** 1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) Weak TRS Rules: Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: Assumption Proof: () *** 1.1.1.1.1.1.1.2 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) Weak TRS Rules: Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: RemoveWeakSuffixes Proof: Consider the dependency graph 1:W:mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) -->_1 mark#(f(X1,X2,X3)) -> c_7(mark#(X2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: mark#(f(X1,X2,X3)) -> c_7(mark#(X2)) *** 1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: Signature: {a__c/0,a__f/3,mark/1,a__c#/0,a__f#/3,mark#/1} / {b/0,c/0,f/3,c_1/0,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1} Obligation: Innermost basic terms: {a__c#,a__f#,mark#}/{b,c,f} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).