KILLED proof of input_zs55Dg0807.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) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxRNTS (17) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) IntTrsBoundProof [UPPER BOUND(ID), 161 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 58 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 149 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 32 ms] (30) CpxRNTS (31) CompletionProof [UPPER BOUND(ID), 0 ms] (32) CpxTypedWeightedCompleteTrs (33) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 1 ms] (34) CpxRNTS (35) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (36) CdtProblem (37) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (40) CdtProblem (41) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (42) CdtProblem (43) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (60) CdtProblem (61) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CdtProblem (65) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (66) 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: nats -> adx(zeros) zeros -> cons(0, zeros) incr(cons(X, Y)) -> cons(s(X), incr(Y)) adx(cons(X, Y)) -> incr(cons(X, adx(Y))) hd(cons(X, Y)) -> X tl(cons(X, Y)) -> Y 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: nats -> adx(zeros) zeros -> cons(0', zeros) incr(cons(X, Y)) -> cons(s(X), incr(Y)) adx(cons(X, Y)) -> incr(cons(X, adx(Y))) hd(cons(X, Y)) -> X tl(cons(X, Y)) -> Y 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: nats -> adx(zeros) zeros -> cons(0, zeros) incr(cons(X, Y)) -> cons(s(X), incr(Y)) adx(cons(X, Y)) -> incr(cons(X, adx(Y))) hd(cons(X, Y)) -> X tl(cons(X, Y)) -> Y 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: nats -> adx(zeros) [1] zeros -> cons(0, zeros) [1] incr(cons(X, Y)) -> cons(s(X), incr(Y)) [1] adx(cons(X, Y)) -> incr(cons(X, adx(Y))) [1] hd(cons(X, Y)) -> X [1] tl(cons(X, Y)) -> Y [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: nats -> adx(zeros) [1] zeros -> cons(0, zeros) [1] incr(cons(X, Y)) -> cons(s(X), incr(Y)) [1] adx(cons(X, Y)) -> incr(cons(X, adx(Y))) [1] hd(cons(X, Y)) -> X [1] tl(cons(X, Y)) -> Y [1] The TRS has the following type information: nats :: cons adx :: cons -> cons zeros :: cons cons :: 0:s -> cons -> cons 0 :: 0:s incr :: cons -> cons s :: 0:s -> 0:s hd :: cons -> 0:s tl :: cons -> cons 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: nats hd_1 tl_1 (c) The following functions are completely defined: zeros adx_1 incr_1 Due to the following rules being added: adx(v0) -> const [0] incr(v0) -> const [0] And the following fresh constants: const ---------------------------------------- (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: nats -> adx(zeros) [1] zeros -> cons(0, zeros) [1] incr(cons(X, Y)) -> cons(s(X), incr(Y)) [1] adx(cons(X, Y)) -> incr(cons(X, adx(Y))) [1] hd(cons(X, Y)) -> X [1] tl(cons(X, Y)) -> Y [1] adx(v0) -> const [0] incr(v0) -> const [0] The TRS has the following type information: nats :: cons:const adx :: cons:const -> cons:const zeros :: cons:const cons :: 0:s -> cons:const -> cons:const 0 :: 0:s incr :: cons:const -> cons:const s :: 0:s -> 0:s hd :: cons:const -> 0:s tl :: cons:const -> cons:const const :: cons:const 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: nats -> adx(cons(0, zeros)) [2] zeros -> cons(0, zeros) [1] incr(cons(X, Y)) -> cons(s(X), incr(Y)) [1] adx(cons(X, cons(X', Y'))) -> incr(cons(X, incr(cons(X', adx(Y'))))) [2] adx(cons(X, Y)) -> incr(cons(X, const)) [1] hd(cons(X, Y)) -> X [1] tl(cons(X, Y)) -> Y [1] adx(v0) -> const [0] incr(v0) -> const [0] The TRS has the following type information: nats :: cons:const adx :: cons:const -> cons:const zeros :: cons:const cons :: 0:s -> cons:const -> cons:const 0 :: 0:s incr :: cons:const -> cons:const s :: 0:s -> 0:s hd :: cons:const -> 0:s tl :: cons:const -> cons:const const :: cons:const 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: 0 => 0 const => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 1 }-> incr(1 + X + 0) :|: Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 incr(z) -{ 1 }-> 1 + (1 + X) + incr(Y) :|: Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: ---------------------------------------- (15) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 1 }-> incr(1 + X + 0) :|: Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 }-> 1 + (1 + X) + incr(Y) :|: Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { incr } { zeros } { tl } { hd } { adx } { nats } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 1 }-> incr(1 + X + 0) :|: Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 }-> 1 + (1 + X) + incr(Y) :|: Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: Function symbols to be analyzed: {incr}, {zeros}, {tl}, {hd}, {adx}, {nats} ---------------------------------------- (19) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 1 }-> incr(1 + X + 0) :|: Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 }-> 1 + (1 + X) + incr(Y) :|: Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: Function symbols to be analyzed: {incr}, {zeros}, {tl}, {hd}, {adx}, {nats} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: incr after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 2*z ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 1 }-> incr(1 + X + 0) :|: Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 }-> 1 + (1 + X) + incr(Y) :|: Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: Function symbols to be analyzed: {incr}, {zeros}, {tl}, {hd}, {adx}, {nats} Previous analysis results are: incr: runtime: ?, size: O(n^1) [2*z] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: incr after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 1 }-> incr(1 + X + 0) :|: Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 }-> 1 + (1 + X) + incr(Y) :|: Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: Function symbols to be analyzed: {zeros}, {tl}, {hd}, {adx}, {nats} Previous analysis results are: incr: runtime: O(n^1) [z], size: O(n^1) [2*z] ---------------------------------------- (25) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 + X }-> s' :|: s' >= 0, s' <= 2 * (1 + X + 0), Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 + Y }-> 1 + (1 + X) + s :|: s >= 0, s <= 2 * Y, Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: Function symbols to be analyzed: {zeros}, {tl}, {hd}, {adx}, {nats} Previous analysis results are: incr: runtime: O(n^1) [z], size: O(n^1) [2*z] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: zeros after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 + X }-> s' :|: s' >= 0, s' <= 2 * (1 + X + 0), Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 + Y }-> 1 + (1 + X) + s :|: s >= 0, s <= 2 * Y, Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: Function symbols to be analyzed: {zeros}, {tl}, {hd}, {adx}, {nats} Previous analysis results are: incr: runtime: O(n^1) [z], size: O(n^1) [2*z] zeros: runtime: ?, size: O(1) [0] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: zeros after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 2 + X }-> s' :|: s' >= 0, s' <= 2 * (1 + X + 0), Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 2 }-> incr(1 + X + incr(1 + X' + adx(Y'))) :|: Y' >= 0, X >= 0, z = 1 + X + (1 + X' + Y'), X' >= 0 adx(z) -{ 0 }-> 0 :|: z >= 0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 incr(z) -{ 0 }-> 0 :|: z >= 0 incr(z) -{ 1 + Y }-> 1 + (1 + X) + s :|: s >= 0, s <= 2 * Y, Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 2 }-> adx(1 + 0 + zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 zeros -{ 1 }-> 1 + 0 + zeros :|: Function symbols to be analyzed: {zeros}, {tl}, {hd}, {adx}, {nats} Previous analysis results are: incr: runtime: O(n^1) [z], size: O(n^1) [2*z] zeros: runtime: INF, size: O(1) [0] ---------------------------------------- (31) 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: incr(v0) -> null_incr [0] adx(v0) -> null_adx [0] hd(v0) -> null_hd [0] tl(v0) -> null_tl [0] And the following fresh constants: null_incr, null_adx, null_hd, null_tl ---------------------------------------- (32) 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: nats -> adx(zeros) [1] zeros -> cons(0, zeros) [1] incr(cons(X, Y)) -> cons(s(X), incr(Y)) [1] adx(cons(X, Y)) -> incr(cons(X, adx(Y))) [1] hd(cons(X, Y)) -> X [1] tl(cons(X, Y)) -> Y [1] incr(v0) -> null_incr [0] adx(v0) -> null_adx [0] hd(v0) -> null_hd [0] tl(v0) -> null_tl [0] The TRS has the following type information: nats :: cons:null_incr:null_adx:null_tl adx :: cons:null_incr:null_adx:null_tl -> cons:null_incr:null_adx:null_tl zeros :: cons:null_incr:null_adx:null_tl cons :: 0:s:null_hd -> cons:null_incr:null_adx:null_tl -> cons:null_incr:null_adx:null_tl 0 :: 0:s:null_hd incr :: cons:null_incr:null_adx:null_tl -> cons:null_incr:null_adx:null_tl s :: 0:s:null_hd -> 0:s:null_hd hd :: cons:null_incr:null_adx:null_tl -> 0:s:null_hd tl :: cons:null_incr:null_adx:null_tl -> cons:null_incr:null_adx:null_tl null_incr :: cons:null_incr:null_adx:null_tl null_adx :: cons:null_incr:null_adx:null_tl null_hd :: 0:s:null_hd null_tl :: cons:null_incr:null_adx:null_tl Rewrite Strategy: INNERMOST ---------------------------------------- (33) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 null_incr => 0 null_adx => 0 null_hd => 0 null_tl => 0 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: adx(z) -{ 1 }-> incr(1 + X + adx(Y)) :|: Y >= 0, z = 1 + X + Y, X >= 0 adx(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 hd(z) -{ 1 }-> X :|: Y >= 0, z = 1 + X + Y, X >= 0 hd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 incr(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 incr(z) -{ 1 }-> 1 + (1 + X) + incr(Y) :|: Y >= 0, z = 1 + X + Y, X >= 0 nats -{ 1 }-> adx(zeros) :|: tl(z) -{ 1 }-> Y :|: Y >= 0, z = 1 + X + Y, X >= 0 tl(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 zeros -{ 1 }-> 1 + 0 + zeros :|: Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (35) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: nats -> adx(zeros) zeros -> cons(0, zeros) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) hd(cons(z0, z1)) -> z0 tl(cons(z0, z1)) -> z1 Tuples: NATS -> c(ADX(zeros), ZEROS) ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) HD(cons(z0, z1)) -> c4 TL(cons(z0, z1)) -> c5 S tuples: NATS -> c(ADX(zeros), ZEROS) ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) HD(cons(z0, z1)) -> c4 TL(cons(z0, z1)) -> c5 K tuples:none Defined Rule Symbols: nats, zeros, incr_1, adx_1, hd_1, tl_1 Defined Pair Symbols: NATS, ZEROS, INCR_1, ADX_1, HD_1, TL_1 Compound Symbols: c_2, c1_1, c2_1, c3_2, c4, c5 ---------------------------------------- (37) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: TL(cons(z0, z1)) -> c5 HD(cons(z0, z1)) -> c4 ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: nats -> adx(zeros) zeros -> cons(0, zeros) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) hd(cons(z0, z1)) -> z0 tl(cons(z0, z1)) -> z1 Tuples: NATS -> c(ADX(zeros), ZEROS) ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) S tuples: NATS -> c(ADX(zeros), ZEROS) ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) K tuples:none Defined Rule Symbols: nats, zeros, incr_1, adx_1, hd_1, tl_1 Defined Pair Symbols: NATS, ZEROS, INCR_1, ADX_1 Compound Symbols: c_2, c1_1, c2_1, c3_2 ---------------------------------------- (39) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: nats -> adx(zeros) zeros -> cons(0, zeros) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) hd(cons(z0, z1)) -> z0 tl(cons(z0, z1)) -> z1 Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(zeros)) NATS -> c4(ZEROS) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(zeros)) NATS -> c4(ZEROS) K tuples:none Defined Rule Symbols: nats, zeros, incr_1, adx_1, hd_1, tl_1 Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (41) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: NATS -> c4(ZEROS) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: nats -> adx(zeros) zeros -> cons(0, zeros) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) hd(cons(z0, z1)) -> z0 tl(cons(z0, z1)) -> z1 Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(zeros)) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(zeros)) K tuples:none Defined Rule Symbols: nats, zeros, incr_1, adx_1, hd_1, tl_1 Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (43) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: NATS -> c4(ADX(zeros)) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: nats -> adx(zeros) zeros -> cons(0, zeros) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) hd(cons(z0, z1)) -> z0 tl(cons(z0, z1)) -> z1 Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(zeros)) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: nats, zeros, incr_1, adx_1, hd_1, tl_1 Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (45) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: nats -> adx(zeros) hd(cons(z0, z1)) -> z0 tl(cons(z0, z1)) -> z1 ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(zeros)) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (47) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace NATS -> c4(ADX(zeros)) by NATS -> c4(ADX(cons(0, zeros))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(cons(0, zeros))) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (49) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace NATS -> c4(ADX(cons(0, zeros))) by NATS -> c4(ADX(cons(0, cons(0, zeros)))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(cons(0, cons(0, zeros)))) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (51) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace NATS -> c4(ADX(cons(0, cons(0, zeros)))) by NATS -> c4(ADX(cons(0, cons(0, cons(0, zeros))))) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(cons(0, cons(0, cons(0, zeros))))) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, z1)) -> c2(INCR(z1)) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace INCR(cons(z0, z1)) -> c2(INCR(z1)) by INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) NATS -> c4(ADX(cons(0, cons(0, cons(0, zeros))))) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) S tuples: ZEROS -> c1(ZEROS) ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, ADX_1, NATS, INCR_1 Compound Symbols: c1_1, c3_2, c4_1, c2_1 ---------------------------------------- (55) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1)) by ADX(cons(x0, cons(z0, z1))) -> c3(INCR(cons(x0, incr(cons(z0, adx(z1))))), ADX(cons(z0, z1))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) NATS -> c4(ADX(cons(0, cons(0, cons(0, zeros))))) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, z1))) -> c3(INCR(cons(x0, incr(cons(z0, adx(z1))))), ADX(cons(z0, z1))) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, z1))) -> c3(INCR(cons(x0, incr(cons(z0, adx(z1))))), ADX(cons(z0, z1))) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, NATS, INCR_1, ADX_1 Compound Symbols: c1_1, c4_1, c2_1, c3_2 ---------------------------------------- (57) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ADX(cons(x0, cons(z0, z1))) -> c3(INCR(cons(x0, incr(cons(z0, adx(z1))))), ADX(cons(z0, z1))) by ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) ADX(cons(x0, cons(x1, cons(z0, z1)))) -> c3(INCR(cons(x0, incr(cons(x1, incr(cons(z0, adx(z1))))))), ADX(cons(x1, cons(z0, z1)))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) NATS -> c4(ADX(cons(0, cons(0, cons(0, zeros))))) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) ADX(cons(x0, cons(x1, cons(z0, z1)))) -> c3(INCR(cons(x0, incr(cons(x1, incr(cons(z0, adx(z1))))))), ADX(cons(x1, cons(z0, z1)))) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) ADX(cons(x0, cons(x1, cons(z0, z1)))) -> c3(INCR(cons(x0, incr(cons(x1, incr(cons(z0, adx(z1))))))), ADX(cons(x1, cons(z0, z1)))) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, NATS, INCR_1, ADX_1 Compound Symbols: c1_1, c4_1, c2_1, c3_2 ---------------------------------------- (59) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace NATS -> c4(ADX(cons(0, cons(0, cons(0, zeros))))) by NATS -> c4(ADX(cons(0, cons(0, cons(0, cons(0, zeros)))))) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) ADX(cons(x0, cons(x1, cons(z0, z1)))) -> c3(INCR(cons(x0, incr(cons(x1, incr(cons(z0, adx(z1))))))), ADX(cons(x1, cons(z0, z1)))) NATS -> c4(ADX(cons(0, cons(0, cons(0, cons(0, zeros)))))) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) ADX(cons(x0, cons(x1, cons(z0, z1)))) -> c3(INCR(cons(x0, incr(cons(x1, incr(cons(z0, adx(z1))))))), ADX(cons(x1, cons(z0, z1)))) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (61) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace ADX(cons(x0, cons(x1, cons(z0, z1)))) -> c3(INCR(cons(x0, incr(cons(x1, incr(cons(z0, adx(z1))))))), ADX(cons(x1, cons(z0, z1)))) by ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(incr(cons(z2, adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) NATS -> c4(ADX(cons(0, cons(0, cons(0, cons(0, zeros)))))) ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(incr(cons(z2, adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) S tuples: ZEROS -> c1(ZEROS) INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(incr(cons(z2, adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, INCR_1, ADX_1, NATS Compound Symbols: c1_1, c2_1, c3_2, c4_1 ---------------------------------------- (63) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace INCR(cons(z0, cons(y0, y1))) -> c2(INCR(cons(y0, y1))) by INCR(cons(z0, cons(z1, cons(y1, y2)))) -> c2(INCR(cons(z1, cons(y1, y2)))) ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) NATS -> c4(ADX(cons(0, cons(0, cons(0, cons(0, zeros)))))) ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(incr(cons(z2, adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) INCR(cons(z0, cons(z1, cons(y1, y2)))) -> c2(INCR(cons(z1, cons(y1, y2)))) S tuples: ZEROS -> c1(ZEROS) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(incr(cons(z2, adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) INCR(cons(z0, cons(z1, cons(y1, y2)))) -> c2(INCR(cons(z1, cons(y1, y2)))) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, ADX_1, NATS, INCR_1 Compound Symbols: c1_1, c3_2, c4_1, c2_1 ---------------------------------------- (65) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(incr(cons(z2, adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) by ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(cons(s(z2), incr(adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: adx(cons(z0, z1)) -> incr(cons(z0, adx(z1))) incr(cons(z0, z1)) -> cons(s(z0), incr(z1)) zeros -> cons(0, zeros) Tuples: ZEROS -> c1(ZEROS) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) NATS -> c4(ADX(cons(0, cons(0, cons(0, cons(0, zeros)))))) INCR(cons(z0, cons(z1, cons(y1, y2)))) -> c2(INCR(cons(z1, cons(y1, y2)))) ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(cons(s(z2), incr(adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) S tuples: ZEROS -> c1(ZEROS) ADX(cons(x0, cons(z0, x2))) -> c3(INCR(cons(x0, cons(s(z0), incr(adx(x2))))), ADX(cons(z0, x2))) INCR(cons(z0, cons(z1, cons(y1, y2)))) -> c2(INCR(cons(z1, cons(y1, y2)))) ADX(cons(z0, cons(z1, cons(z2, z3)))) -> c3(INCR(cons(z0, cons(s(z1), incr(cons(s(z2), incr(adx(z3))))))), ADX(cons(z1, cons(z2, z3)))) K tuples: NATS -> c4(ADX(zeros)) Defined Rule Symbols: adx_1, incr_1, zeros Defined Pair Symbols: ZEROS, ADX_1, NATS, INCR_1 Compound Symbols: c1_1, c3_2, c4_1, c2_1