KILLED proof of input_DsbiDRrz3m.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), 765 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 177 ms] (24) CpxRNTS (25) CompletionProof [UPPER BOUND(ID), 0 ms] (26) CpxTypedWeightedCompleteTrs (27) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (28) CpxRNTS (29) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (30) CdtProblem (31) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtNarrowingProof [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) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (58) 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: app(nil, YS) -> YS app(cons(X, XS), YS) -> cons(X, app(XS, YS)) from(X) -> cons(X, from(s(X))) zWadr(nil, YS) -> nil zWadr(XS, nil) -> nil zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) prefix(L) -> cons(nil, zWadr(L, prefix(L))) 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: app(nil, YS) -> YS app(cons(X, XS), YS) -> cons(X, app(XS, YS)) from(X) -> cons(X, from(s(X))) zWadr(nil, YS) -> nil zWadr(XS, nil) -> nil zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) prefix(L) -> cons(nil, zWadr(L, prefix(L))) 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: app(nil, YS) -> YS app(cons(X, XS), YS) -> cons(X, app(XS, YS)) from(X) -> cons(X, from(s(X))) zWadr(nil, YS) -> nil zWadr(XS, nil) -> nil zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) prefix(L) -> cons(nil, zWadr(L, prefix(L))) 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: app(nil, YS) -> YS [1] app(cons(X, XS), YS) -> cons(X, app(XS, YS)) [1] from(X) -> cons(X, from(s(X))) [1] zWadr(nil, YS) -> nil [1] zWadr(XS, nil) -> nil [1] zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) [1] prefix(L) -> cons(nil, zWadr(L, prefix(L))) [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: app(nil, YS) -> YS [1] app(cons(X, XS), YS) -> cons(X, app(XS, YS)) [1] from(X) -> cons(X, from(s(X))) [1] zWadr(nil, YS) -> nil [1] zWadr(XS, nil) -> nil [1] zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) [1] prefix(L) -> cons(nil, zWadr(L, prefix(L))) [1] The TRS has the following type information: app :: nil:cons:s -> nil:cons:s -> nil:cons:s nil :: nil:cons:s cons :: nil:cons:s -> nil:cons:s -> nil:cons:s from :: nil:cons:s -> nil:cons:s s :: nil:cons:s -> nil:cons:s zWadr :: nil:cons:s -> nil:cons:s -> nil:cons:s prefix :: nil:cons:s -> nil:cons:s 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: from_1 (c) The following functions are completely defined: prefix_1 zWadr_2 app_2 Due to the following rules being added: zWadr(v0, v1) -> nil [0] app(v0, v1) -> nil [0] 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: app(nil, YS) -> YS [1] app(cons(X, XS), YS) -> cons(X, app(XS, YS)) [1] from(X) -> cons(X, from(s(X))) [1] zWadr(nil, YS) -> nil [1] zWadr(XS, nil) -> nil [1] zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) [1] prefix(L) -> cons(nil, zWadr(L, prefix(L))) [1] zWadr(v0, v1) -> nil [0] app(v0, v1) -> nil [0] The TRS has the following type information: app :: nil:cons:s -> nil:cons:s -> nil:cons:s nil :: nil:cons:s cons :: nil:cons:s -> nil:cons:s -> nil:cons:s from :: nil:cons:s -> nil:cons:s s :: nil:cons:s -> nil:cons:s zWadr :: nil:cons:s -> nil:cons:s -> nil:cons:s prefix :: nil:cons:s -> nil:cons:s 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: app(nil, YS) -> YS [1] app(cons(X, XS), YS) -> cons(X, app(XS, YS)) [1] from(X) -> cons(X, from(s(X))) [1] zWadr(nil, YS) -> nil [1] zWadr(XS, nil) -> nil [1] zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) [1] prefix(L) -> cons(nil, zWadr(L, cons(nil, zWadr(L, prefix(L))))) [2] zWadr(v0, v1) -> nil [0] app(v0, v1) -> nil [0] The TRS has the following type information: app :: nil:cons:s -> nil:cons:s -> nil:cons:s nil :: nil:cons:s cons :: nil:cons:s -> nil:cons:s -> nil:cons:s from :: nil:cons:s -> nil:cons:s s :: nil:cons:s -> nil:cons:s zWadr :: nil:cons:s -> nil:cons:s -> nil:cons:s prefix :: nil:cons:s -> nil:cons:s 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: nil => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: app(z, z') -{ 1 }-> YS :|: z' = YS, YS >= 0, z = 0 app(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 app(z, z') -{ 1 }-> 1 + X + app(XS, YS) :|: z' = YS, z = 1 + X + XS, X >= 0, YS >= 0, XS >= 0 from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X prefix(z) -{ 2 }-> 1 + 0 + zWadr(L, 1 + 0 + zWadr(L, prefix(L))) :|: z = L, L >= 0 zWadr(z, z') -{ 1 }-> 0 :|: z' = YS, YS >= 0, z = 0 zWadr(z, z') -{ 1 }-> 0 :|: z = XS, XS >= 0, z' = 0 zWadr(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 zWadr(z, z') -{ 1 }-> 1 + app(Y, 1 + X + 0) + zWadr(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 ---------------------------------------- (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: app(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 app(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 app(z, z') -{ 1 }-> 1 + X + app(XS, z') :|: z = 1 + X + XS, X >= 0, z' >= 0, XS >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 prefix(z) -{ 2 }-> 1 + 0 + zWadr(z, 1 + 0 + zWadr(z, prefix(z))) :|: z >= 0 zWadr(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 zWadr(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWadr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 zWadr(z, z') -{ 1 }-> 1 + app(Y, 1 + X + 0) + zWadr(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { from } { app } { zWadr } { prefix } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: app(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 app(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 app(z, z') -{ 1 }-> 1 + X + app(XS, z') :|: z = 1 + X + XS, X >= 0, z' >= 0, XS >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 prefix(z) -{ 2 }-> 1 + 0 + zWadr(z, 1 + 0 + zWadr(z, prefix(z))) :|: z >= 0 zWadr(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 zWadr(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWadr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 zWadr(z, z') -{ 1 }-> 1 + app(Y, 1 + X + 0) + zWadr(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {app}, {zWadr}, {prefix} ---------------------------------------- (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: app(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 app(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 app(z, z') -{ 1 }-> 1 + X + app(XS, z') :|: z = 1 + X + XS, X >= 0, z' >= 0, XS >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 prefix(z) -{ 2 }-> 1 + 0 + zWadr(z, 1 + 0 + zWadr(z, prefix(z))) :|: z >= 0 zWadr(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 zWadr(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWadr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 zWadr(z, z') -{ 1 }-> 1 + app(Y, 1 + X + 0) + zWadr(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {app}, {zWadr}, {prefix} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: from after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: app(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 app(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 app(z, z') -{ 1 }-> 1 + X + app(XS, z') :|: z = 1 + X + XS, X >= 0, z' >= 0, XS >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 prefix(z) -{ 2 }-> 1 + 0 + zWadr(z, 1 + 0 + zWadr(z, prefix(z))) :|: z >= 0 zWadr(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 zWadr(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWadr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 zWadr(z, z') -{ 1 }-> 1 + app(Y, 1 + X + 0) + zWadr(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {app}, {zWadr}, {prefix} Previous analysis results are: from: runtime: ?, size: O(1) [0] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: from after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: app(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 app(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 app(z, z') -{ 1 }-> 1 + X + app(XS, z') :|: z = 1 + X + XS, X >= 0, z' >= 0, XS >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 prefix(z) -{ 2 }-> 1 + 0 + zWadr(z, 1 + 0 + zWadr(z, prefix(z))) :|: z >= 0 zWadr(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 zWadr(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWadr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 zWadr(z, z') -{ 1 }-> 1 + app(Y, 1 + X + 0) + zWadr(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {app}, {zWadr}, {prefix} Previous analysis results are: from: runtime: INF, size: O(1) [0] ---------------------------------------- (25) 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: app(v0, v1) -> null_app [0] zWadr(v0, v1) -> null_zWadr [0] And the following fresh constants: null_app, null_zWadr ---------------------------------------- (26) 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: app(nil, YS) -> YS [1] app(cons(X, XS), YS) -> cons(X, app(XS, YS)) [1] from(X) -> cons(X, from(s(X))) [1] zWadr(nil, YS) -> nil [1] zWadr(XS, nil) -> nil [1] zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nil)), zWadr(XS, YS)) [1] prefix(L) -> cons(nil, zWadr(L, prefix(L))) [1] app(v0, v1) -> null_app [0] zWadr(v0, v1) -> null_zWadr [0] The TRS has the following type information: app :: nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr nil :: nil:cons:s:null_app:null_zWadr cons :: nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr from :: nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr s :: nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr zWadr :: nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr prefix :: nil:cons:s:null_app:null_zWadr -> nil:cons:s:null_app:null_zWadr null_app :: nil:cons:s:null_app:null_zWadr null_zWadr :: nil:cons:s:null_app:null_zWadr Rewrite Strategy: INNERMOST ---------------------------------------- (27) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: nil => 0 null_app => 0 null_zWadr => 0 ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: app(z, z') -{ 1 }-> YS :|: z' = YS, YS >= 0, z = 0 app(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 app(z, z') -{ 1 }-> 1 + X + app(XS, YS) :|: z' = YS, z = 1 + X + XS, X >= 0, YS >= 0, XS >= 0 from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X prefix(z) -{ 1 }-> 1 + 0 + zWadr(L, prefix(L)) :|: z = L, L >= 0 zWadr(z, z') -{ 1 }-> 0 :|: z' = YS, YS >= 0, z = 0 zWadr(z, z') -{ 1 }-> 0 :|: z = XS, XS >= 0, z' = 0 zWadr(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 zWadr(z, z') -{ 1 }-> 1 + app(Y, 1 + X + 0) + zWadr(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (29) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) from(z0) -> cons(z0, from(s(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) Tuples: APP(nil, z0) -> c APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(nil, z0) -> c3 ZWADR(z0, nil) -> c4 ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, prefix(z0)), PREFIX(z0)) S tuples: APP(nil, z0) -> c APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(nil, z0) -> c3 ZWADR(z0, nil) -> c4 ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, prefix(z0)), PREFIX(z0)) K tuples:none Defined Rule Symbols: app_2, from_1, zWadr_2, prefix_1 Defined Pair Symbols: APP_2, FROM_1, ZWADR_2, PREFIX_1 Compound Symbols: c, c1_1, c2_1, c3, c4, c5_1, c6_1, c7_2 ---------------------------------------- (31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing nodes: ZWADR(z0, nil) -> c4 APP(nil, z0) -> c ZWADR(nil, z0) -> c3 ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) from(z0) -> cons(z0, from(s(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) Tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, prefix(z0)), PREFIX(z0)) S tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, prefix(z0)), PREFIX(z0)) K tuples:none Defined Rule Symbols: app_2, from_1, zWadr_2, prefix_1 Defined Pair Symbols: APP_2, FROM_1, ZWADR_2, PREFIX_1 Compound Symbols: c1_1, c2_1, c5_1, c6_1, c7_2 ---------------------------------------- (33) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: from(z0) -> cons(z0, from(s(z0))) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, prefix(z0)), PREFIX(z0)) S tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, prefix(z0)), PREFIX(z0)) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: APP_2, FROM_1, ZWADR_2, PREFIX_1 Compound Symbols: c1_1, c2_1, c5_1, c6_1, c7_2 ---------------------------------------- (35) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace PREFIX(z0) -> c7(ZWADR(z0, prefix(z0)), PREFIX(z0)) by PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, prefix(z0)))), PREFIX(z0)) ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, prefix(z0)))), PREFIX(z0)) S tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, prefix(z0)))), PREFIX(z0)) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: APP_2, FROM_1, ZWADR_2, PREFIX_1 Compound Symbols: c1_1, c2_1, c5_1, c6_1, c7_2 ---------------------------------------- (37) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, prefix(z0)))), PREFIX(z0)) by PREFIX(nil) -> c7(ZWADR(nil, cons(nil, nil)), PREFIX(nil)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(nil) -> c7(ZWADR(nil, cons(nil, nil)), PREFIX(nil)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) S tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(nil) -> c7(ZWADR(nil, cons(nil, nil)), PREFIX(nil)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: APP_2, FROM_1, ZWADR_2, PREFIX_1 Compound Symbols: c1_1, c2_1, c5_1, c6_1, c7_2 ---------------------------------------- (39) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) S tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) FROM(z0) -> c2(FROM(s(z0))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: APP_2, FROM_1, ZWADR_2, PREFIX_1 Compound Symbols: c1_1, c2_1, c5_1, c6_1, c7_2, c7_1 ---------------------------------------- (41) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace FROM(z0) -> c2(FROM(s(z0))) by FROM(s(x0)) -> c2(FROM(s(s(x0)))) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(x0)) -> c2(FROM(s(s(x0)))) S tuples: APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(x0)) -> c2(FROM(s(s(x0)))) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: APP_2, ZWADR_2, PREFIX_1, FROM_1 Compound Symbols: c1_1, c5_1, c6_1, c7_2, c7_1, c2_1 ---------------------------------------- (43) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace APP(cons(z0, z1), z2) -> c1(APP(z1, z2)) by APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(x0)) -> c2(FROM(s(s(x0)))) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) S tuples: ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(x0)) -> c2(FROM(s(s(x0)))) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: ZWADR_2, PREFIX_1, FROM_1, APP_2 Compound Symbols: c5_1, c6_1, c7_2, c7_1, c2_1, c1_1 ---------------------------------------- (45) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace FROM(s(x0)) -> c2(FROM(s(s(x0)))) by FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) S tuples: ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: ZWADR_2, PREFIX_1, APP_2, FROM_1 Compound Symbols: c5_1, c6_1, c7_2, c7_1, c1_1, c2_1 ---------------------------------------- (47) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWADR(cons(z0, z1), cons(z2, z3)) -> c5(APP(z2, cons(z0, nil))) by ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) S tuples: ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: ZWADR_2, PREFIX_1, APP_2, FROM_1 Compound Symbols: c6_1, c7_2, c7_1, c1_1, c2_1, c5_1 ---------------------------------------- (49) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWADR(cons(z0, z1), cons(z2, z3)) -> c6(ZWADR(z1, z3)) by ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) S tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: PREFIX_1, APP_2, FROM_1, ZWADR_2 Compound Symbols: c7_2, c7_1, c1_1, c2_1, c5_1, c6_1 ---------------------------------------- (51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace APP(cons(z0, cons(y0, y1)), z2) -> c1(APP(cons(y0, y1), z2)) by APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) S tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: PREFIX_1, FROM_1, ZWADR_2, APP_2 Compound Symbols: c7_2, c7_1, c2_1, c5_1, c6_1, c1_1 ---------------------------------------- (53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWADR(cons(z0, z1), cons(cons(y0, cons(y1, y2)), z3)) -> c5(APP(cons(y0, cons(y1, y2)), cons(z0, nil))) by ZWADR(cons(z0, z1), cons(cons(z2, cons(z3, cons(y2, y3))), z5)) -> c5(APP(cons(z2, cons(z3, cons(y2, y3))), cons(z0, nil))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) ZWADR(cons(z0, z1), cons(cons(z2, cons(z3, cons(y2, y3))), z5)) -> c5(APP(cons(z2, cons(z3, cons(y2, y3))), cons(z0, nil))) S tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) ZWADR(cons(z0, z1), cons(cons(z2, cons(z3, cons(y2, y3))), z5)) -> c5(APP(cons(z2, cons(z3, cons(y2, y3))), cons(z0, nil))) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: PREFIX_1, FROM_1, ZWADR_2, APP_2 Compound Symbols: c7_2, c7_1, c2_1, c6_1, c1_1, c5_1 ---------------------------------------- (55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c6(ZWADR(cons(y0, y1), cons(y2, y3))) by ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, z2)), cons(z3, cons(cons(y2, cons(y3, cons(y4, y5))), z5))) -> c6(ZWADR(cons(z1, z2), cons(cons(y2, cons(y3, cons(y4, y5))), z5))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) ZWADR(cons(z0, z1), cons(cons(z2, cons(z3, cons(y2, y3))), z5)) -> c5(APP(cons(z2, cons(z3, cons(y2, y3))), cons(z0, nil))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, z2)), cons(z3, cons(cons(y2, cons(y3, cons(y4, y5))), z5))) -> c6(ZWADR(cons(z1, z2), cons(cons(y2, cons(y3, cons(y4, y5))), z5))) S tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) ZWADR(cons(z0, z1), cons(cons(z2, cons(z3, cons(y2, y3))), z5)) -> c5(APP(cons(z2, cons(z3, cons(y2, y3))), cons(z0, nil))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, z2)), cons(z3, cons(cons(y2, cons(y3, cons(y4, y5))), z5))) -> c6(ZWADR(cons(z1, z2), cons(cons(y2, cons(y3, cons(y4, y5))), z5))) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: PREFIX_1, FROM_1, ZWADR_2, APP_2 Compound Symbols: c7_2, c7_1, c2_1, c6_1, c1_1, c5_1 ---------------------------------------- (57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWADR(cons(z0, cons(y0, y1)), cons(z2, cons(cons(y2, cons(y3, y4)), y5))) -> c6(ZWADR(cons(y0, y1), cons(cons(y2, cons(y3, y4)), y5))) by ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, z2)), cons(z3, cons(cons(z4, cons(z5, cons(y4, y5))), z7))) -> c6(ZWADR(cons(z1, z2), cons(cons(z4, cons(z5, cons(y4, y5))), z7))) ZWADR(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(y5, cons(y6, y7))))) -> c6(ZWADR(cons(z1, cons(y1, cons(y2, y3))), cons(cons(z4, cons(z5, z6)), cons(y5, cons(y6, y7))))) ZWADR(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(y5, cons(cons(y6, cons(y7, y8)), y9))))) -> c6(ZWADR(cons(z1, cons(y1, cons(y2, y3))), cons(cons(z4, cons(z5, z6)), cons(y5, cons(cons(y6, cons(y7, y8)), y9))))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, cons(y6, y7))), y8)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, cons(y6, y7))), y8)))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: prefix(z0) -> cons(nil, zWadr(z0, prefix(z0))) zWadr(nil, z0) -> nil zWadr(z0, nil) -> nil zWadr(cons(z0, z1), cons(z2, z3)) -> cons(app(z2, cons(z0, nil)), zWadr(z1, z3)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) Tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) ZWADR(cons(z0, z1), cons(cons(z2, cons(z3, cons(y2, y3))), z5)) -> c5(APP(cons(z2, cons(z3, cons(y2, y3))), cons(z0, nil))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, z2)), cons(z3, cons(cons(y2, cons(y3, cons(y4, y5))), z5))) -> c6(ZWADR(cons(z1, z2), cons(cons(y2, cons(y3, cons(y4, y5))), z5))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(y5, cons(y6, y7))))) -> c6(ZWADR(cons(z1, cons(y1, cons(y2, y3))), cons(cons(z4, cons(z5, z6)), cons(y5, cons(y6, y7))))) ZWADR(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(y5, cons(cons(y6, cons(y7, y8)), y9))))) -> c6(ZWADR(cons(z1, cons(y1, cons(y2, y3))), cons(cons(z4, cons(z5, z6)), cons(y5, cons(cons(y6, cons(y7, y8)), y9))))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, cons(y6, y7))), y8)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, cons(y6, y7))), y8)))) S tuples: PREFIX(z0) -> c7(ZWADR(z0, cons(nil, zWadr(z0, cons(nil, zWadr(z0, prefix(z0)))))), PREFIX(z0)) PREFIX(nil) -> c7(PREFIX(nil)) FROM(s(s(x0))) -> c2(FROM(s(s(s(x0))))) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c1(APP(cons(z1, cons(y1, y2)), z3)) ZWADR(cons(z0, z1), cons(cons(z2, cons(z3, cons(y2, y3))), z5)) -> c5(APP(cons(z2, cons(z3, cons(y2, y3))), cons(z0, nil))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(z4, cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, z2)), cons(z3, cons(cons(y2, cons(y3, cons(y4, y5))), z5))) -> c6(ZWADR(cons(z1, z2), cons(cons(y2, cons(y3, cons(y4, y5))), z5))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, y6)), y7)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, y6)), y7)))) ZWADR(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(y5, cons(y6, y7))))) -> c6(ZWADR(cons(z1, cons(y1, cons(y2, y3))), cons(cons(z4, cons(z5, z6)), cons(y5, cons(y6, y7))))) ZWADR(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(y5, cons(cons(y6, cons(y7, y8)), y9))))) -> c6(ZWADR(cons(z1, cons(y1, cons(y2, y3))), cons(cons(z4, cons(z5, z6)), cons(y5, cons(cons(y6, cons(y7, y8)), y9))))) ZWADR(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, cons(y6, y7))), y8)))) -> c6(ZWADR(cons(z1, cons(y1, y2)), cons(cons(z4, cons(z5, z6)), cons(cons(y4, cons(y5, cons(y6, y7))), y8)))) K tuples:none Defined Rule Symbols: prefix_1, zWadr_2, app_2 Defined Pair Symbols: PREFIX_1, FROM_1, APP_2, ZWADR_2 Compound Symbols: c7_2, c7_1, c2_1, c1_1, c5_1, c6_1