KILLED proof of input_fd7MuK1ORp.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), 4 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), 168 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 108 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 774 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 184 ms] (30) CpxRNTS (31) CompletionProof [UPPER BOUND(ID), 0 ms] (32) CpxTypedWeightedCompleteTrs (33) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (34) CpxRNTS (35) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (36) CdtProblem (37) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (40) CdtProblem (41) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 76 ms] (42) CdtProblem (43) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 16 ms] (44) CdtProblem (45) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (60) CdtProblem (61) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CdtProblem (65) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (66) CdtProblem (67) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (68) CdtProblem (69) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CdtProblem (71) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (72) CdtProblem (73) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (74) CdtProblem (75) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (76) CdtProblem (77) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (78) CdtProblem (79) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (80) CdtProblem (81) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (82) CdtProblem (83) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (84) CdtProblem (85) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (86) 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: from(X) -> cons(X, from(s(X))) sel(0, cons(X, XS)) -> X sel(s(N), cons(X, XS)) -> sel(N, XS) minus(X, 0) -> 0 minus(s(X), s(Y)) -> minus(X, Y) quot(0, s(Y)) -> 0 quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) zWquot(XS, nil) -> nil zWquot(nil, XS) -> nil zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) 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: from(X) -> cons(X, from(s(X))) sel(0', cons(X, XS)) -> X sel(s(N), cons(X, XS)) -> sel(N, XS) minus(X, 0') -> 0' minus(s(X), s(Y)) -> minus(X, Y) quot(0', s(Y)) -> 0' quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) zWquot(XS, nil) -> nil zWquot(nil, XS) -> nil zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) 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: from(X) -> cons(X, from(s(X))) sel(0, cons(X, XS)) -> X sel(s(N), cons(X, XS)) -> sel(N, XS) minus(X, 0) -> 0 minus(s(X), s(Y)) -> minus(X, Y) quot(0, s(Y)) -> 0 quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) zWquot(XS, nil) -> nil zWquot(nil, XS) -> nil zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) 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: from(X) -> cons(X, from(s(X))) [1] sel(0, cons(X, XS)) -> X [1] sel(s(N), cons(X, XS)) -> sel(N, XS) [1] minus(X, 0) -> 0 [1] minus(s(X), s(Y)) -> minus(X, Y) [1] quot(0, s(Y)) -> 0 [1] quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1] zWquot(XS, nil) -> nil [1] zWquot(nil, XS) -> nil [1] zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [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: from(X) -> cons(X, from(s(X))) [1] sel(0, cons(X, XS)) -> X [1] sel(s(N), cons(X, XS)) -> sel(N, XS) [1] minus(X, 0) -> 0 [1] minus(s(X), s(Y)) -> minus(X, Y) [1] quot(0, s(Y)) -> 0 [1] quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1] zWquot(XS, nil) -> nil [1] zWquot(nil, XS) -> nil [1] zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1] The TRS has the following type information: from :: s:0 -> cons:nil cons :: s:0 -> cons:nil -> cons:nil s :: s:0 -> s:0 sel :: s:0 -> cons:nil -> s:0 0 :: s:0 minus :: s:0 -> s:0 -> s:0 quot :: s:0 -> s:0 -> s:0 zWquot :: cons:nil -> cons:nil -> cons:nil nil :: cons:nil 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 sel_2 quot_2 zWquot_2 (c) The following functions are completely defined: minus_2 Due to the following rules being added: minus(v0, v1) -> 0 [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: from(X) -> cons(X, from(s(X))) [1] sel(0, cons(X, XS)) -> X [1] sel(s(N), cons(X, XS)) -> sel(N, XS) [1] minus(X, 0) -> 0 [1] minus(s(X), s(Y)) -> minus(X, Y) [1] quot(0, s(Y)) -> 0 [1] quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1] zWquot(XS, nil) -> nil [1] zWquot(nil, XS) -> nil [1] zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1] minus(v0, v1) -> 0 [0] The TRS has the following type information: from :: s:0 -> cons:nil cons :: s:0 -> cons:nil -> cons:nil s :: s:0 -> s:0 sel :: s:0 -> cons:nil -> s:0 0 :: s:0 minus :: s:0 -> s:0 -> s:0 quot :: s:0 -> s:0 -> s:0 zWquot :: cons:nil -> cons:nil -> cons:nil nil :: cons:nil 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: from(X) -> cons(X, from(s(X))) [1] sel(0, cons(X, XS)) -> X [1] sel(s(N), cons(X, XS)) -> sel(N, XS) [1] minus(X, 0) -> 0 [1] minus(s(X), s(Y)) -> minus(X, Y) [1] quot(0, s(Y)) -> 0 [1] quot(s(X), s(0)) -> s(quot(0, s(0))) [2] quot(s(s(X')), s(s(Y'))) -> s(quot(minus(X', Y'), s(s(Y')))) [2] quot(s(X), s(Y)) -> s(quot(0, s(Y))) [1] zWquot(XS, nil) -> nil [1] zWquot(nil, XS) -> nil [1] zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1] minus(v0, v1) -> 0 [0] The TRS has the following type information: from :: s:0 -> cons:nil cons :: s:0 -> cons:nil -> cons:nil s :: s:0 -> s:0 sel :: s:0 -> cons:nil -> s:0 0 :: s:0 minus :: s:0 -> s:0 -> s:0 quot :: s:0 -> s:0 -> s:0 zWquot :: cons:nil -> cons:nil -> cons:nil nil :: cons:nil 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 nil => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X minus(z, z') -{ 1 }-> minus(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0 minus(z, z') -{ 1 }-> 0 :|: X >= 0, z = X, z' = 0 minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 quot(z, z') -{ 1 }-> 0 :|: Y >= 0, z' = 1 + Y, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(X', Y'), 1 + (1 + Y')) :|: z' = 1 + (1 + Y'), Y' >= 0, X' >= 0, z = 1 + (1 + X') quot(z, z') -{ 1 }-> 1 + quot(0, 1 + Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z = 1 + X, X >= 0, z' = 1 + 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 }-> sel(N, XS) :|: z = 1 + N, z' = 1 + X + XS, X >= 0, XS >= 0, N >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z = XS, XS >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z' = XS, z = 0, XS >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(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: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(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: { sel } { from } { minus } { quot } { zWquot } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {sel}, {from}, {minus}, {quot}, {zWquot} ---------------------------------------- (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: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {sel}, {from}, {minus}, {quot}, {zWquot} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: sel after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {sel}, {from}, {minus}, {quot}, {zWquot} Previous analysis results are: sel: runtime: ?, size: O(n^1) [z'] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: sel after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot} Previous analysis results are: sel: runtime: O(n^1) [1 + z], size: O(n^1) [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: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 + z }-> s :|: s >= 0, s <= XS, z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot} Previous analysis results are: sel: runtime: O(n^1) [1 + z], size: O(n^1) [z'] ---------------------------------------- (27) 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 ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 + z }-> s :|: s >= 0, s <= XS, z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot} Previous analysis results are: sel: runtime: O(n^1) [1 + z], size: O(n^1) [z'] from: runtime: ?, size: O(1) [0] ---------------------------------------- (29) 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: ? ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0 quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0 quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0 quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 + z }-> s :|: s >= 0, s <= XS, z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0 zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0 Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot} Previous analysis results are: sel: runtime: O(n^1) [1 + z], size: O(n^1) [z'] from: 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: sel(v0, v1) -> null_sel [0] minus(v0, v1) -> null_minus [0] quot(v0, v1) -> null_quot [0] And the following fresh constants: null_sel, null_minus, null_quot ---------------------------------------- (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: from(X) -> cons(X, from(s(X))) [1] sel(0, cons(X, XS)) -> X [1] sel(s(N), cons(X, XS)) -> sel(N, XS) [1] minus(X, 0) -> 0 [1] minus(s(X), s(Y)) -> minus(X, Y) [1] quot(0, s(Y)) -> 0 [1] quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1] zWquot(XS, nil) -> nil [1] zWquot(nil, XS) -> nil [1] zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1] sel(v0, v1) -> null_sel [0] minus(v0, v1) -> null_minus [0] quot(v0, v1) -> null_quot [0] The TRS has the following type information: from :: s:0:null_sel:null_minus:null_quot -> cons:nil cons :: s:0:null_sel:null_minus:null_quot -> cons:nil -> cons:nil s :: s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot sel :: s:0:null_sel:null_minus:null_quot -> cons:nil -> s:0:null_sel:null_minus:null_quot 0 :: s:0:null_sel:null_minus:null_quot minus :: s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot quot :: s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot zWquot :: cons:nil -> cons:nil -> cons:nil nil :: cons:nil null_sel :: s:0:null_sel:null_minus:null_quot null_minus :: s:0:null_sel:null_minus:null_quot null_quot :: s:0:null_sel:null_minus:null_quot 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 nil => 0 null_sel => 0 null_minus => 0 null_quot => 0 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X minus(z, z') -{ 1 }-> minus(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0 minus(z, z') -{ 1 }-> 0 :|: X >= 0, z = X, z' = 0 minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 quot(z, z') -{ 1 }-> 0 :|: Y >= 0, z' = 1 + Y, z = 0 quot(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 quot(z, z') -{ 1 }-> 1 + quot(minus(X, Y), 1 + Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0 sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0 sel(z, z') -{ 1 }-> sel(N, XS) :|: z = 1 + N, z' = 1 + X + XS, X >= 0, XS >= 0, N >= 0 sel(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 zWquot(z, z') -{ 1 }-> 0 :|: z = XS, XS >= 0, z' = 0 zWquot(z, z') -{ 1 }-> 0 :|: z' = XS, z = 0, XS >= 0 zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(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. ---------------------------------------- (35) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: from(z0) -> cons(z0, from(s(z0))) sel(0, cons(z0, z1)) -> z0 sel(s(z0), cons(z1, z2)) -> sel(z0, z2) minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0, s(z0)) -> 0 quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) zWquot(z0, nil) -> nil zWquot(nil, z0) -> nil zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3)) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(0, cons(z0, z1)) -> c1 SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(z0, 0) -> c3 MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(0, s(z0)) -> c5 QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(z0, nil) -> c7 ZWQUOT(nil, z0) -> c8 ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) S tuples: FROM(z0) -> c(FROM(s(z0))) SEL(0, cons(z0, z1)) -> c1 SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(z0, 0) -> c3 MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(0, s(z0)) -> c5 QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(z0, nil) -> c7 ZWQUOT(nil, z0) -> c8 ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) K tuples:none Defined Rule Symbols: from_1, sel_2, minus_2, quot_2, zWquot_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2 Compound Symbols: c_1, c1, c2_1, c3, c4_1, c5, c6_2, c7, c8, c9_1, c10_1 ---------------------------------------- (37) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 5 trailing nodes: ZWQUOT(nil, z0) -> c8 ZWQUOT(z0, nil) -> c7 SEL(0, cons(z0, z1)) -> c1 MINUS(z0, 0) -> c3 QUOT(0, s(z0)) -> c5 ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: from(z0) -> cons(z0, from(s(z0))) sel(0, cons(z0, z1)) -> z0 sel(s(z0), cons(z1, z2)) -> sel(z0, z2) minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0, s(z0)) -> 0 quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) zWquot(z0, nil) -> nil zWquot(nil, z0) -> nil zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3)) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) S tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) K tuples:none Defined Rule Symbols: from_1, sel_2, minus_2, quot_2, zWquot_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2 Compound Symbols: c_1, c2_1, c4_1, c6_2, c9_1, c10_1 ---------------------------------------- (39) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: from(z0) -> cons(z0, from(s(z0))) sel(0, cons(z0, z1)) -> z0 sel(s(z0), cons(z1, z2)) -> sel(z0, z2) quot(0, s(z0)) -> 0 quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) zWquot(z0, nil) -> nil zWquot(nil, z0) -> nil zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3)) ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) S tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) K tuples:none Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2 Compound Symbols: c_1, c2_1, c4_1, c6_2, c9_1, c10_1 ---------------------------------------- (41) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) We considered the (Usable) Rules: minus(s(z0), s(z1)) -> minus(z0, z1) minus(z0, 0) -> 0 And the Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(FROM(x_1)) = 0 POL(MINUS(x_1, x_2)) = x_1 POL(QUOT(x_1, x_2)) = [1] + x_1 + x_2 POL(SEL(x_1, x_2)) = x_1 + x_2 POL(ZWQUOT(x_1, x_2)) = [1] + x_1 + x_2 POL(c(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1, x_2)) = x_1 + x_2 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(minus(x_1, x_2)) = [1] POL(s(x_1)) = [1] + x_1 ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) S tuples: FROM(z0) -> c(FROM(s(z0))) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2 Compound Symbols: c_1, c2_1, c4_1, c6_2, c9_1, c10_1 ---------------------------------------- (43) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) We considered the (Usable) Rules: minus(s(z0), s(z1)) -> minus(z0, z1) minus(z0, 0) -> 0 And the Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(FROM(x_1)) = 0 POL(MINUS(x_1, x_2)) = 0 POL(QUOT(x_1, x_2)) = x_1 + x_2 POL(SEL(x_1, x_2)) = x_1 + x_2 POL(ZWQUOT(x_1, x_2)) = x_1 + x_2 POL(c(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1, x_2)) = x_1 + x_2 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(minus(x_1, x_2)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2 Compound Symbols: c_1, c2_1, c4_1, c6_2, c9_1, c10_1 ---------------------------------------- (45) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) by QUOT(s(z0), s(0)) -> c6(QUOT(0, s(0)), MINUS(z0, 0)) QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1))) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(z0), s(0)) -> c6(QUOT(0, s(0)), MINUS(z0, 0)) QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1))) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2 Compound Symbols: c_1, c2_1, c4_1, c9_1, c10_1, c6_2 ---------------------------------------- (47) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: QUOT(s(z0), s(0)) -> c6(QUOT(0, s(0)), MINUS(z0, 0)) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1))) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2 Compound Symbols: c_1, c2_1, c4_1, c9_1, c10_1, c6_2 ---------------------------------------- (49) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1))) by QUOT(s(s(z0)), s(s(0))) -> c6(QUOT(0, s(s(0))), MINUS(s(z0), s(0))) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(z0)), s(s(0))) -> c6(QUOT(0, s(s(0))), MINUS(s(z0), s(0))) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2 Compound Symbols: c_1, c2_1, c4_1, c9_1, c10_1, c6_2, c6_1 ---------------------------------------- (51) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(z0) -> c(FROM(s(z0))) SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0))) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2 Compound Symbols: c_1, c2_1, c4_1, c9_1, c10_1, c6_2, c6_1 ---------------------------------------- (53) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace FROM(z0) -> c(FROM(s(z0))) by FROM(s(x0)) -> c(FROM(s(s(x0)))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0))) FROM(s(x0)) -> c(FROM(s(s(x0)))) S tuples: FROM(s(x0)) -> c(FROM(s(s(x0)))) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) Defined Rule Symbols: minus_2 Defined Pair Symbols: SEL_2, MINUS_2, ZWQUOT_2, QUOT_2, FROM_1 Compound Symbols: c2_1, c4_1, c9_1, c10_1, c6_2, c6_1, c_1 ---------------------------------------- (55) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace FROM(s(x0)) -> c(FROM(s(s(x0)))) by FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) Defined Rule Symbols: minus_2 Defined Pair Symbols: SEL_2, MINUS_2, ZWQUOT_2, QUOT_2, FROM_1 Compound Symbols: c2_1, c4_1, c9_1, c10_1, c6_2, c6_1, c_1 ---------------------------------------- (57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) by SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) Defined Rule Symbols: minus_2 Defined Pair Symbols: MINUS_2, ZWQUOT_2, QUOT_2, FROM_1, SEL_2 Compound Symbols: c4_1, c9_1, c10_1, c6_2, c6_1, c_1, c2_1 ---------------------------------------- (59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) by MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) Defined Rule Symbols: minus_2 Defined Pair Symbols: ZWQUOT_2, QUOT_2, FROM_1, SEL_2, MINUS_2 Compound Symbols: c9_1, c10_1, c6_2, c6_1, c_1, c2_1, c4_1 ---------------------------------------- (61) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0))) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) Defined Rule Symbols: minus_2 Defined Pair Symbols: ZWQUOT_2, QUOT_2, FROM_1, SEL_2, MINUS_2 Compound Symbols: c9_1, c10_1, c6_2, c6_1, c_1, c2_1, c4_1 ---------------------------------------- (63) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) by ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: ZWQUOT_2, QUOT_2, FROM_1, SEL_2, MINUS_2 Compound Symbols: c10_1, c6_2, c6_1, c_1, c2_1, c4_1, c9_1 ---------------------------------------- (65) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) by ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) Defined Rule Symbols: minus_2 Defined Pair Symbols: QUOT_2, FROM_1, SEL_2, MINUS_2, ZWQUOT_2 Compound Symbols: c6_2, c6_1, c_1, c2_1, c4_1, c9_1, c10_1 ---------------------------------------- (67) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) by QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) Defined Rule Symbols: minus_2 Defined Pair Symbols: QUOT_2, FROM_1, SEL_2, MINUS_2, ZWQUOT_2 Compound Symbols: c6_2, c_1, c2_1, c4_1, c9_1, c10_1, c6_1 ---------------------------------------- (69) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) by SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: QUOT_2, FROM_1, MINUS_2, ZWQUOT_2, SEL_2 Compound Symbols: c6_2, c_1, c4_1, c9_1, c10_1, c6_1, c2_1 ---------------------------------------- (71) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) by MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: QUOT_2, FROM_1, ZWQUOT_2, SEL_2, MINUS_2 Compound Symbols: c6_2, c_1, c9_1, c10_1, c6_1, c2_1, c4_1 ---------------------------------------- (73) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) by QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(QUOT(minus(s(y0), s(y1)), s(s(s(s(y1))))), MINUS(s(s(s(y0))), s(s(s(y1))))) ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(QUOT(minus(s(y0), s(y1)), s(s(s(s(y1))))), MINUS(s(s(s(y0))), s(s(s(y1))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2 Compound Symbols: c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2 ---------------------------------------- (75) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(QUOT(minus(s(y0), s(y1)), s(s(s(s(y1))))), MINUS(s(s(s(y0))), s(s(s(y1))))) by QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1))))) ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2 Compound Symbols: c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2 ---------------------------------------- (77) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) by ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1))))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2 Compound Symbols: c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2 ---------------------------------------- (79) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) by ZWQUOT(cons(z0, cons(s(s(s(y0))), z2)), cons(z3, cons(s(s(s(y2))), z5))) -> c10(ZWQUOT(cons(s(s(s(y0))), z2), cons(s(s(s(y2))), z5))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ---------------------------------------- (80) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1))))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2 Compound Symbols: c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2 ---------------------------------------- (81) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) by ZWQUOT(cons(z0, cons(s(s(s(y0))), z2)), cons(z3, cons(s(s(s(y2))), z5))) -> c10(ZWQUOT(cons(s(s(s(y0))), z2), cons(s(s(s(y2))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) ---------------------------------------- (82) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1))))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2 Compound Symbols: c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2 ---------------------------------------- (83) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) by QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(MINUS(s(s(s(y0))), s(s(s(y1))))) ---------------------------------------- (84) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1))))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(MINUS(s(s(s(y0))), s(s(s(y1))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, ZWQUOT_2, SEL_2, MINUS_2, QUOT_2 Compound Symbols: c_1, c9_1, c10_1, c2_1, c4_1, c6_2, c6_1 ---------------------------------------- (85) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) by ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ---------------------------------------- (86) Obligation: Complexity Dependency Tuples Problem Rules: minus(z0, 0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) Tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1))))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(MINUS(s(s(s(y0))), s(s(s(y1))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3))) SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1)))) ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1)))))) ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5)))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) Defined Rule Symbols: minus_2 Defined Pair Symbols: FROM_1, ZWQUOT_2, SEL_2, MINUS_2, QUOT_2 Compound Symbols: c_1, c9_1, c10_1, c2_1, c4_1, c6_2, c6_1