KILLED proof of input_RM3HbLY4MK.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). (0) CpxTRS (1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxTRS (3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (4) CpxTRS (5) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (6) CpxWeightedTrs (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedTrs (9) CompletionProof [UPPER BOUND(ID), 0 ms] (10) CpxTypedWeightedCompleteTrs (11) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedCompleteTrs (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (14) CpxRNTS (15) InliningProof [UPPER BOUND(ID), 265 ms] (16) CpxRNTS (17) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) CompletionProof [UPPER BOUND(ID), 0 ms] (20) CpxTypedWeightedCompleteTrs (21) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (22) CpxRNTS (23) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (24) CdtProblem (25) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CdtProblem (29) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CdtProblem (31) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CdtProblem (37) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (40) CdtProblem (41) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: a__f(a, b, X) -> a__f(X, X, mark(X)) a__c -> a a__c -> b mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) mark(c) -> a__c mark(a) -> a mark(b) -> b a__f(X1, X2, X3) -> f(X1, X2, X3) a__c -> c S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: a__f(a, b, X) -> a__f(X, X, mark(X)) a__c -> a a__c -> b mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) mark(c) -> a__c mark(a) -> a mark(b) -> b a__f(X1, X2, X3) -> f(X1, X2, X3) a__c -> c S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: a__f(a, b, X) -> a__f(X, X, mark(X)) a__c -> a a__c -> b mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) mark(c) -> a__c mark(a) -> a mark(b) -> b a__f(X1, X2, X3) -> f(X1, X2, X3) a__c -> c S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (6) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: a__f(a, b, X) -> a__f(X, X, mark(X)) [1] a__c -> a [1] a__c -> b [1] mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) [1] mark(c) -> a__c [1] mark(a) -> a [1] mark(b) -> b [1] a__f(X1, X2, X3) -> f(X1, X2, X3) [1] a__c -> c [1] Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: a__f(a, b, X) -> a__f(X, X, mark(X)) [1] a__c -> a [1] a__c -> b [1] mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) [1] mark(c) -> a__c [1] mark(a) -> a [1] mark(b) -> b [1] a__f(X1, X2, X3) -> f(X1, X2, X3) [1] a__c -> c [1] The TRS has the following type information: a__f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c a :: a:b:f:c b :: a:b:f:c mark :: a:b:f:c -> a:b:f:c a__c :: a:b:f:c f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c c :: a:b:f:c Rewrite Strategy: INNERMOST ---------------------------------------- (9) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: none (c) The following functions are completely defined: mark_1 a__c a__f_3 Due to the following rules being added: none And the following fresh constants: none ---------------------------------------- (10) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: a__f(a, b, X) -> a__f(X, X, mark(X)) [1] a__c -> a [1] a__c -> b [1] mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) [1] mark(c) -> a__c [1] mark(a) -> a [1] mark(b) -> b [1] a__f(X1, X2, X3) -> f(X1, X2, X3) [1] a__c -> c [1] The TRS has the following type information: a__f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c a :: a:b:f:c b :: a:b:f:c mark :: a:b:f:c -> a:b:f:c a__c :: a:b:f:c f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c c :: a:b:f:c Rewrite Strategy: INNERMOST ---------------------------------------- (11) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: a__f(a, b, f(X1', X2', X3')) -> a__f(f(X1', X2', X3'), f(X1', X2', X3'), a__f(X1', X2', mark(X3'))) [2] a__f(a, b, c) -> a__f(c, c, a__c) [2] a__f(a, b, a) -> a__f(a, a, a) [2] a__f(a, b, b) -> a__f(b, b, b) [2] a__c -> a [1] a__c -> b [1] mark(f(X1, X2, f(X1'', X2'', X3''))) -> a__f(X1, X2, a__f(X1'', X2'', mark(X3''))) [2] mark(f(X1, X2, c)) -> a__f(X1, X2, a__c) [2] mark(f(X1, X2, a)) -> a__f(X1, X2, a) [2] mark(f(X1, X2, b)) -> a__f(X1, X2, b) [2] mark(c) -> a__c [1] mark(a) -> a [1] mark(b) -> b [1] a__f(X1, X2, X3) -> f(X1, X2, X3) [1] a__c -> c [1] The TRS has the following type information: a__f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c a :: a:b:f:c b :: a:b:f:c mark :: a:b:f:c -> a:b:f:c a__c :: a:b:f:c f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c c :: a:b:f:c Rewrite Strategy: INNERMOST ---------------------------------------- (13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: a => 0 b => 1 c => 2 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: a__c -{ 1 }-> 2 :|: a__c -{ 1 }-> 1 :|: a__c -{ 1 }-> 0 :|: a__f(z, z', z'') -{ 2 }-> a__f(2, 2, a__c) :|: z' = 1, z'' = 2, z = 0 a__f(z, z', z'') -{ 2 }-> a__f(1, 1, 1) :|: z' = 1, z = 0, z'' = 1 a__f(z, z', z'') -{ 2 }-> a__f(0, 0, 0) :|: z'' = 0, z' = 1, z = 0 a__f(z, z', z'') -{ 2 }-> a__f(1 + X1' + X2' + X3', 1 + X1' + X2' + X3', a__f(X1', X2', mark(X3'))) :|: X3' >= 0, X2' >= 0, X1' >= 0, z'' = 1 + X1' + X2' + X3', z' = 1, z = 0 a__f(z, z', z'') -{ 1 }-> 1 + X1 + X2 + X3 :|: X1 >= 0, X3 >= 0, X2 >= 0, z = X1, z' = X2, z'' = X3 mark(z) -{ 2 }-> a__f(X1, X2, a__f(X1'', X2'', mark(X3''))) :|: X1 >= 0, X1'' >= 0, z = 1 + X1 + X2 + (1 + X1'' + X2'' + X3''), X3'' >= 0, X2 >= 0, X2'' >= 0 mark(z) -{ 2 }-> a__f(X1, X2, a__c) :|: X1 >= 0, z = 1 + X1 + X2 + 2, X2 >= 0 mark(z) -{ 2 }-> a__f(X1, X2, 1) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 + 1 mark(z) -{ 2 }-> a__f(X1, X2, 0) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 + 0 mark(z) -{ 1 }-> a__c :|: z = 2 mark(z) -{ 1 }-> 1 :|: z = 1 mark(z) -{ 1 }-> 0 :|: z = 0 ---------------------------------------- (15) InliningProof (UPPER BOUND(ID)) Inlined the following terminating rules on right-hand sides where appropriate: a__c -{ 1 }-> 0 :|: a__c -{ 1 }-> 1 :|: a__c -{ 1 }-> 2 :|: ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: a__c -{ 1 }-> 2 :|: a__c -{ 1 }-> 1 :|: a__c -{ 1 }-> 0 :|: a__f(z, z', z'') -{ 3 }-> a__f(2, 2, 2) :|: z' = 1, z'' = 2, z = 0 a__f(z, z', z'') -{ 3 }-> a__f(2, 2, 1) :|: z' = 1, z'' = 2, z = 0 a__f(z, z', z'') -{ 3 }-> a__f(2, 2, 0) :|: z' = 1, z'' = 2, z = 0 a__f(z, z', z'') -{ 2 }-> a__f(1, 1, 1) :|: z' = 1, z = 0, z'' = 1 a__f(z, z', z'') -{ 2 }-> a__f(0, 0, 0) :|: z'' = 0, z' = 1, z = 0 a__f(z, z', z'') -{ 2 }-> a__f(1 + X1' + X2' + X3', 1 + X1' + X2' + X3', a__f(X1', X2', mark(X3'))) :|: X3' >= 0, X2' >= 0, X1' >= 0, z'' = 1 + X1' + X2' + X3', z' = 1, z = 0 a__f(z, z', z'') -{ 1 }-> 1 + X1 + X2 + X3 :|: X1 >= 0, X3 >= 0, X2 >= 0, z = X1, z' = X2, z'' = X3 mark(z) -{ 2 }-> a__f(X1, X2, a__f(X1'', X2'', mark(X3''))) :|: X1 >= 0, X1'' >= 0, z = 1 + X1 + X2 + (1 + X1'' + X2'' + X3''), X3'' >= 0, X2 >= 0, X2'' >= 0 mark(z) -{ 3 }-> a__f(X1, X2, 2) :|: X1 >= 0, z = 1 + X1 + X2 + 2, X2 >= 0 mark(z) -{ 2 }-> a__f(X1, X2, 1) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 + 1 mark(z) -{ 3 }-> a__f(X1, X2, 1) :|: X1 >= 0, z = 1 + X1 + X2 + 2, X2 >= 0 mark(z) -{ 2 }-> a__f(X1, X2, 0) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 + 0 mark(z) -{ 3 }-> a__f(X1, X2, 0) :|: X1 >= 0, z = 1 + X1 + X2 + 2, X2 >= 0 mark(z) -{ 2 }-> 2 :|: z = 2 mark(z) -{ 1 }-> 1 :|: z = 1 mark(z) -{ 2 }-> 1 :|: z = 2 mark(z) -{ 1 }-> 0 :|: z = 0 mark(z) -{ 2 }-> 0 :|: z = 2 ---------------------------------------- (17) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: a__c -{ 1 }-> 2 :|: a__c -{ 1 }-> 1 :|: a__c -{ 1 }-> 0 :|: a__f(z, z', z'') -{ 3 }-> a__f(2, 2, 2) :|: z' = 1, z'' = 2, z = 0 a__f(z, z', z'') -{ 3 }-> a__f(2, 2, 1) :|: z' = 1, z'' = 2, z = 0 a__f(z, z', z'') -{ 3 }-> a__f(2, 2, 0) :|: z' = 1, z'' = 2, z = 0 a__f(z, z', z'') -{ 2 }-> a__f(1, 1, 1) :|: z' = 1, z = 0, z'' = 1 a__f(z, z', z'') -{ 2 }-> a__f(0, 0, 0) :|: z'' = 0, z' = 1, z = 0 a__f(z, z', z'') -{ 2 }-> a__f(1 + X1' + X2' + X3', 1 + X1' + X2' + X3', a__f(X1', X2', mark(X3'))) :|: X3' >= 0, X2' >= 0, X1' >= 0, z'' = 1 + X1' + X2' + X3', z' = 1, z = 0 a__f(z, z', z'') -{ 1 }-> 1 + z + z' + z'' :|: z >= 0, z'' >= 0, z' >= 0 mark(z) -{ 2 }-> a__f(X1, X2, a__f(X1'', X2'', mark(X3''))) :|: X1 >= 0, X1'' >= 0, z = 1 + X1 + X2 + (1 + X1'' + X2'' + X3''), X3'' >= 0, X2 >= 0, X2'' >= 0 mark(z) -{ 3 }-> a__f(X1, X2, 2) :|: X1 >= 0, z = 1 + X1 + X2 + 2, X2 >= 0 mark(z) -{ 2 }-> a__f(X1, X2, 1) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 + 1 mark(z) -{ 3 }-> a__f(X1, X2, 1) :|: X1 >= 0, z = 1 + X1 + X2 + 2, X2 >= 0 mark(z) -{ 2 }-> a__f(X1, X2, 0) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 + 0 mark(z) -{ 3 }-> a__f(X1, X2, 0) :|: X1 >= 0, z = 1 + X1 + X2 + 2, X2 >= 0 mark(z) -{ 2 }-> 2 :|: z = 2 mark(z) -{ 1 }-> 1 :|: z = 1 mark(z) -{ 2 }-> 1 :|: z = 2 mark(z) -{ 1 }-> 0 :|: z = 0 mark(z) -{ 2 }-> 0 :|: z = 2 ---------------------------------------- (19) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: none And the following fresh constants: none ---------------------------------------- (20) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: a__f(a, b, X) -> a__f(X, X, mark(X)) [1] a__c -> a [1] a__c -> b [1] mark(f(X1, X2, X3)) -> a__f(X1, X2, mark(X3)) [1] mark(c) -> a__c [1] mark(a) -> a [1] mark(b) -> b [1] a__f(X1, X2, X3) -> f(X1, X2, X3) [1] a__c -> c [1] The TRS has the following type information: a__f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c a :: a:b:f:c b :: a:b:f:c mark :: a:b:f:c -> a:b:f:c a__c :: a:b:f:c f :: a:b:f:c -> a:b:f:c -> a:b:f:c -> a:b:f:c c :: a:b:f:c Rewrite Strategy: INNERMOST ---------------------------------------- (21) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: a => 0 b => 1 c => 2 ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: a__c -{ 1 }-> 2 :|: a__c -{ 1 }-> 1 :|: a__c -{ 1 }-> 0 :|: a__f(z, z', z'') -{ 1 }-> a__f(X, X, mark(X)) :|: z'' = X, X >= 0, z' = 1, z = 0 a__f(z, z', z'') -{ 1 }-> 1 + X1 + X2 + X3 :|: X1 >= 0, X3 >= 0, X2 >= 0, z = X1, z' = X2, z'' = X3 mark(z) -{ 1 }-> a__f(X1, X2, mark(X3)) :|: X1 >= 0, X3 >= 0, z = 1 + X1 + X2 + X3, X2 >= 0 mark(z) -{ 1 }-> a__c :|: z = 2 mark(z) -{ 1 }-> 1 :|: z = 1 mark(z) -{ 1 }-> 0 :|: z = 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (23) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, z0) -> c1(A__F(z0, z0, mark(z0)), MARK(z0)) A__F(z0, z1, z2) -> c2 A__C -> c3 A__C -> c4 A__C -> c5 MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) MARK(c) -> c7(A__C) MARK(a) -> c8 MARK(b) -> c9 S tuples: A__F(a, b, z0) -> c1(A__F(z0, z0, mark(z0)), MARK(z0)) A__F(z0, z1, z2) -> c2 A__C -> c3 A__C -> c4 A__C -> c5 MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) MARK(c) -> c7(A__C) MARK(a) -> c8 MARK(b) -> c9 K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, A__C, MARK_1 Compound Symbols: c1_2, c2, c3, c4, c5, c6_2, c7_1, c8, c9 ---------------------------------------- (25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 7 trailing nodes: MARK(b) -> c9 MARK(c) -> c7(A__C) MARK(a) -> c8 A__C -> c3 A__F(z0, z1, z2) -> c2 A__C -> c4 A__C -> c5 ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, z0) -> c1(A__F(z0, z0, mark(z0)), MARK(z0)) MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) S tuples: A__F(a, b, z0) -> c1(A__F(z0, z0, mark(z0)), MARK(z0)) MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_2, c6_2 ---------------------------------------- (27) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) A__F(a, b, z0) -> c1(MARK(z0)) S tuples: MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) A__F(a, b, z0) -> c1(MARK(z0)) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: MARK_1, A__F_3 Compound Symbols: c6_2, c1_1 ---------------------------------------- (29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A__F(a, b, z0) -> c1(MARK(z0)) by A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) S tuples: MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: MARK_1, A__F_3 Compound Symbols: c6_2, c1_1 ---------------------------------------- (31) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MARK(f(z0, z1, z2)) -> c6(A__F(z0, z1, mark(z2)), MARK(z2)) by MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c), MARK(c)) MARK(f(x0, x1, a)) -> c6(A__F(x0, x1, a), MARK(a)) MARK(f(x0, x1, b)) -> c6(A__F(x0, x1, b), MARK(b)) ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c), MARK(c)) MARK(f(x0, x1, a)) -> c6(A__F(x0, x1, a), MARK(a)) MARK(f(x0, x1, b)) -> c6(A__F(x0, x1, b), MARK(b)) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c), MARK(c)) MARK(f(x0, x1, a)) -> c6(A__F(x0, x1, a), MARK(a)) MARK(f(x0, x1, b)) -> c6(A__F(x0, x1, b), MARK(b)) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_2 ---------------------------------------- (33) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: MARK(f(x0, x1, a)) -> c6(A__F(x0, x1, a), MARK(a)) MARK(f(x0, x1, b)) -> c6(A__F(x0, x1, b), MARK(b)) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c), MARK(c)) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c), MARK(c)) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_2 ---------------------------------------- (35) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c)) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c)) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_2, c6_1 ---------------------------------------- (37) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MARK(f(x0, x1, f(z0, z1, z2))) -> c6(A__F(x0, x1, a__f(z0, z1, mark(z2))), MARK(f(z0, z1, z2))) by MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a)), MARK(f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b)), MARK(f(x2, x3, b))) ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c)) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a)), MARK(f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b)), MARK(f(x2, x3, b))) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c)) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a)), MARK(f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b)), MARK(f(x2, x3, b))) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_1, c6_2 ---------------------------------------- (39) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing tuple parts ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c)) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c)) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_1, c6_2 ---------------------------------------- (41) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a__c)) by MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, b)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, c)) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, b)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, c)) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, b)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, c)) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_2, c6_1 ---------------------------------------- (43) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing nodes: MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, c)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, a)) MARK(f(x0, x1, c)) -> c6(A__F(x0, x1, b)) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c)), MARK(f(x2, x3, c))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_2, c6_1 ---------------------------------------- (45) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c))) S tuples: A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c))) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: A__F_3, MARK_1 Compound Symbols: c1_1, c6_2, c6_1 ---------------------------------------- (47) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A__F(a, b, f(y0, y1, y2)) -> c1(MARK(f(y0, y1, y2))) by A__F(a, b, f(z0, z1, f(a, b, y2))) -> c1(MARK(f(z0, z1, f(a, b, y2)))) A__F(a, b, f(z0, z1, f(y2, y3, y4))) -> c1(MARK(f(z0, z1, f(y2, y3, y4)))) A__F(a, b, f(z0, z1, f(y2, y3, f(y4, y5, y6)))) -> c1(MARK(f(z0, z1, f(y2, y3, f(y4, y5, y6))))) A__F(a, b, f(z0, z1, f(y2, y3, a))) -> c1(MARK(f(z0, z1, f(y2, y3, a)))) A__F(a, b, f(z0, z1, f(y2, y3, b))) -> c1(MARK(f(z0, z1, f(y2, y3, b)))) A__F(a, b, f(z0, z1, f(y2, y3, c))) -> c1(MARK(f(z0, z1, f(y2, y3, c)))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: a__f(a, b, z0) -> a__f(z0, z0, mark(z0)) a__f(z0, z1, z2) -> f(z0, z1, z2) a__c -> a a__c -> b a__c -> c mark(f(z0, z1, z2)) -> a__f(z0, z1, mark(z2)) mark(c) -> a__c mark(a) -> a mark(b) -> b Tuples: MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c))) A__F(a, b, f(z0, z1, f(a, b, y2))) -> c1(MARK(f(z0, z1, f(a, b, y2)))) A__F(a, b, f(z0, z1, f(y2, y3, y4))) -> c1(MARK(f(z0, z1, f(y2, y3, y4)))) A__F(a, b, f(z0, z1, f(y2, y3, f(y4, y5, y6)))) -> c1(MARK(f(z0, z1, f(y2, y3, f(y4, y5, y6))))) A__F(a, b, f(z0, z1, f(y2, y3, a))) -> c1(MARK(f(z0, z1, f(y2, y3, a)))) A__F(a, b, f(z0, z1, f(y2, y3, b))) -> c1(MARK(f(z0, z1, f(y2, y3, b)))) A__F(a, b, f(z0, z1, f(y2, y3, c))) -> c1(MARK(f(z0, z1, f(y2, y3, c)))) S tuples: MARK(f(x0, x1, f(a, b, x4))) -> c6(A__F(x0, x1, a__f(mark(x4), mark(x4), mark(mark(x4)))), MARK(f(a, b, x4))) MARK(f(x0, x1, f(z0, z1, x4))) -> c6(A__F(x0, x1, f(z0, z1, mark(x4))), MARK(f(z0, z1, x4))) MARK(f(x0, x1, f(x2, x3, f(z0, z1, z2)))) -> c6(A__F(x0, x1, a__f(x2, x3, a__f(z0, z1, mark(z2)))), MARK(f(x2, x3, f(z0, z1, z2)))) MARK(f(x0, x1, f(x2, x3, a))) -> c6(A__F(x0, x1, a__f(x2, x3, a))) MARK(f(x0, x1, f(x2, x3, b))) -> c6(A__F(x0, x1, a__f(x2, x3, b))) MARK(f(x0, x1, f(x2, x3, c))) -> c6(A__F(x0, x1, a__f(x2, x3, a__c))) A__F(a, b, f(z0, z1, f(a, b, y2))) -> c1(MARK(f(z0, z1, f(a, b, y2)))) A__F(a, b, f(z0, z1, f(y2, y3, y4))) -> c1(MARK(f(z0, z1, f(y2, y3, y4)))) A__F(a, b, f(z0, z1, f(y2, y3, f(y4, y5, y6)))) -> c1(MARK(f(z0, z1, f(y2, y3, f(y4, y5, y6))))) A__F(a, b, f(z0, z1, f(y2, y3, a))) -> c1(MARK(f(z0, z1, f(y2, y3, a)))) A__F(a, b, f(z0, z1, f(y2, y3, b))) -> c1(MARK(f(z0, z1, f(y2, y3, b)))) A__F(a, b, f(z0, z1, f(y2, y3, c))) -> c1(MARK(f(z0, z1, f(y2, y3, c)))) K tuples:none Defined Rule Symbols: a__f_3, a__c, mark_1 Defined Pair Symbols: MARK_1, A__F_3 Compound Symbols: c6_2, c6_1, c1_1