KILLED proof of input_bCv0fx6eoS.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) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxRelTRS (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (12) typed CpxTrs (13) OrderProof [LOWER BOUND(ID), 10 ms] (14) typed CpxTrs (15) RewriteLemmaProof [LOWER BOUND(ID), 1073 ms] (16) typed CpxTrs (17) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (18) TRS for Loop Detection (19) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (20) CdtProblem (21) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CpxRelTRS (25) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (26) CpxTRS (27) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CpxWeightedTrs (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CpxTypedWeightedTrs (31) CompletionProof [UPPER BOUND(ID), 0 ms] (32) CpxTypedWeightedCompleteTrs (33) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CpxTypedWeightedCompleteTrs (35) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (36) CpxRNTS (37) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CpxRNTS (39) CompletionProof [UPPER BOUND(ID), 0 ms] (40) CpxTypedWeightedCompleteTrs (41) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (42) CpxRNTS (43) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtRhsSimplificationProcessorProof [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) CdtNarrowingProof [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 (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), 25 ms] (72) CdtProblem (73) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 4 ms] (74) CdtProblem (75) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 108 ms] (76) CdtProblem (77) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (78) CpxWeightedTrs (79) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (80) CpxTypedWeightedTrs (81) CompletionProof [UPPER BOUND(ID), 0 ms] (82) CpxTypedWeightedCompleteTrs (83) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (84) CpxTypedWeightedCompleteTrs (85) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (86) CpxRNTS (87) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (88) CpxRNTS (89) CompletionProof [UPPER BOUND(ID), 0 ms] (90) CpxTypedWeightedCompleteTrs (91) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (92) CpxRNTS ---------------------------------------- (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: ack(0, y) -> s(y) ack(s(x), 0) -> ack(x, s(0)) ack(s(x), s(y)) -> ack(x, ack(s(x), y)) f(s(x), y) -> f(x, s(x)) f(x, s(y)) -> f(y, x) f(x, y) -> ack(x, y) ack(s(x), y) -> f(x, x) 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: ack(0', y) -> s(y) ack(s(x), 0') -> ack(x, s(0')) ack(s(x), s(y)) -> ack(x, ack(s(x), y)) f(s(x), y) -> f(x, s(x)) f(x, s(y)) -> f(y, x) f(x, y) -> ack(x, y) ack(s(x), y) -> f(x, x) 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: ack(0, y) -> s(y) ack(s(x), 0) -> ack(x, s(0)) ack(s(x), s(y)) -> ack(x, ack(s(x), y)) f(s(x), y) -> f(x, s(x)) f(x, s(y)) -> f(y, x) f(x, y) -> ack(x, y) ack(s(x), y) -> f(x, x) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(0, z0) -> c ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) S tuples: ACK(0, z0) -> c ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c, c1_1, c2_2, c3_1, c4_1, c5_1, c6_1 ---------------------------------------- (7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (8) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: ACK(0, z0) -> c ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) The (relative) TRS S consists of the following rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Rewrite Strategy: INNERMOST ---------------------------------------- (9) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (10) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: ACK(0', z0) -> c ACK(s(z0), 0') -> c1(ACK(z0, s(0'))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) The (relative) TRS S consists of the following rules: ack(0', z0) -> s(z0) ack(s(z0), 0') -> ack(z0, s(0')) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (12) Obligation: Innermost TRS: Rules: ACK(0', z0) -> c ACK(s(z0), 0') -> c1(ACK(z0, s(0'))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ack(0', z0) -> s(z0) ack(s(z0), 0') -> ack(z0, s(0')) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Types: ACK :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 -> c:c1:c2:c3 c2 :: c:c1:c2:c3 -> c:c1:c2:c3 -> c:c1:c2:c3 ack :: 0':s -> 0':s -> 0':s c3 :: c4:c5:c6 -> c:c1:c2:c3 F :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 -> c4:c5:c6 c5 :: c4:c5:c6 -> c4:c5:c6 c6 :: c:c1:c2:c3 -> c4:c5:c6 f :: 0':s -> 0':s -> 0':s hole_c:c1:c2:c31_7 :: c:c1:c2:c3 hole_0':s2_7 :: 0':s hole_c4:c5:c63_7 :: c4:c5:c6 gen_c:c1:c2:c34_7 :: Nat -> c:c1:c2:c3 gen_0':s5_7 :: Nat -> 0':s gen_c4:c5:c66_7 :: Nat -> c4:c5:c6 ---------------------------------------- (13) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: ACK, ack, F, f They will be analysed ascendingly in the following order: ack < ACK ACK = F ack = f ---------------------------------------- (14) Obligation: Innermost TRS: Rules: ACK(0', z0) -> c ACK(s(z0), 0') -> c1(ACK(z0, s(0'))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ack(0', z0) -> s(z0) ack(s(z0), 0') -> ack(z0, s(0')) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Types: ACK :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 -> c:c1:c2:c3 c2 :: c:c1:c2:c3 -> c:c1:c2:c3 -> c:c1:c2:c3 ack :: 0':s -> 0':s -> 0':s c3 :: c4:c5:c6 -> c:c1:c2:c3 F :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 -> c4:c5:c6 c5 :: c4:c5:c6 -> c4:c5:c6 c6 :: c:c1:c2:c3 -> c4:c5:c6 f :: 0':s -> 0':s -> 0':s hole_c:c1:c2:c31_7 :: c:c1:c2:c3 hole_0':s2_7 :: 0':s hole_c4:c5:c63_7 :: c4:c5:c6 gen_c:c1:c2:c34_7 :: Nat -> c:c1:c2:c3 gen_0':s5_7 :: Nat -> 0':s gen_c4:c5:c66_7 :: Nat -> c4:c5:c6 Generator Equations: gen_c:c1:c2:c34_7(0) <=> c gen_c:c1:c2:c34_7(+(x, 1)) <=> c1(gen_c:c1:c2:c34_7(x)) gen_0':s5_7(0) <=> 0' gen_0':s5_7(+(x, 1)) <=> s(gen_0':s5_7(x)) gen_c4:c5:c66_7(0) <=> c6(c) gen_c4:c5:c66_7(+(x, 1)) <=> c4(gen_c4:c5:c66_7(x)) The following defined symbols remain to be analysed: f, ACK, ack, F They will be analysed ascendingly in the following order: ack < ACK ACK = F ack = f ---------------------------------------- (15) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: ack(gen_0':s5_7(1), gen_0':s5_7(+(1, n3196_7))) -> *7_7, rt in Omega(0) Induction Base: ack(gen_0':s5_7(1), gen_0':s5_7(+(1, 0))) Induction Step: ack(gen_0':s5_7(1), gen_0':s5_7(+(1, +(n3196_7, 1)))) ->_R^Omega(0) ack(gen_0':s5_7(0), ack(s(gen_0':s5_7(0)), gen_0':s5_7(+(1, n3196_7)))) ->_IH ack(gen_0':s5_7(0), *7_7) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (16) Obligation: Innermost TRS: Rules: ACK(0', z0) -> c ACK(s(z0), 0') -> c1(ACK(z0, s(0'))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ack(0', z0) -> s(z0) ack(s(z0), 0') -> ack(z0, s(0')) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Types: ACK :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 -> c:c1:c2:c3 c2 :: c:c1:c2:c3 -> c:c1:c2:c3 -> c:c1:c2:c3 ack :: 0':s -> 0':s -> 0':s c3 :: c4:c5:c6 -> c:c1:c2:c3 F :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 -> c4:c5:c6 c5 :: c4:c5:c6 -> c4:c5:c6 c6 :: c:c1:c2:c3 -> c4:c5:c6 f :: 0':s -> 0':s -> 0':s hole_c:c1:c2:c31_7 :: c:c1:c2:c3 hole_0':s2_7 :: 0':s hole_c4:c5:c63_7 :: c4:c5:c6 gen_c:c1:c2:c34_7 :: Nat -> c:c1:c2:c3 gen_0':s5_7 :: Nat -> 0':s gen_c4:c5:c66_7 :: Nat -> c4:c5:c6 Lemmas: ack(gen_0':s5_7(1), gen_0':s5_7(+(1, n3196_7))) -> *7_7, rt in Omega(0) Generator Equations: gen_c:c1:c2:c34_7(0) <=> c gen_c:c1:c2:c34_7(+(x, 1)) <=> c1(gen_c:c1:c2:c34_7(x)) gen_0':s5_7(0) <=> 0' gen_0':s5_7(+(x, 1)) <=> s(gen_0':s5_7(x)) gen_c4:c5:c66_7(0) <=> c6(c) gen_c4:c5:c66_7(+(x, 1)) <=> c4(gen_c4:c5:c66_7(x)) The following defined symbols remain to be analysed: f, ACK, F They will be analysed ascendingly in the following order: ack < ACK ACK = F ack = f ---------------------------------------- (17) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (18) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: ACK(0, z0) -> c ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) The (relative) TRS S consists of the following rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Rewrite Strategy: INNERMOST ---------------------------------------- (19) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(0, z0) -> c ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) S tuples: ACK(0, z0) -> c ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c, c1_1, c2_2, c3_1, c4_1, c5_1, c6_1 ---------------------------------------- (21) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: ACK(0, z0) -> c ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) S tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c1_1, c2_2, c3_1, c4_1, c5_1, c6_1 ---------------------------------------- (23) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (24) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) The (relative) TRS S consists of the following rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Rewrite Strategy: INNERMOST ---------------------------------------- (25) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (26) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (27) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (28) 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: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) [1] ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) [1] ACK(s(z0), z1) -> c3(F(z0, z0)) [1] F(s(z0), z1) -> c4(F(z0, s(z0))) [1] F(z0, s(z1)) -> c5(F(z1, z0)) [1] F(z0, z1) -> c6(ACK(z0, z1)) [1] ack(0, z0) -> s(z0) [0] ack(s(z0), 0) -> ack(z0, s(0)) [0] ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) [0] ack(s(z0), z1) -> f(z0, z0) [0] f(s(z0), z1) -> f(z0, s(z0)) [0] f(z0, s(z1)) -> f(z1, z0) [0] f(z0, z1) -> ack(z0, z1) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (29) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (30) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) [1] ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) [1] ACK(s(z0), z1) -> c3(F(z0, z0)) [1] F(s(z0), z1) -> c4(F(z0, s(z0))) [1] F(z0, s(z1)) -> c5(F(z1, z0)) [1] F(z0, z1) -> c6(ACK(z0, z1)) [1] ack(0, z0) -> s(z0) [0] ack(s(z0), 0) -> ack(z0, s(0)) [0] ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) [0] ack(s(z0), z1) -> f(z0, z0) [0] f(s(z0), z1) -> f(z0, s(z0)) [0] f(z0, s(z1)) -> f(z1, z0) [0] f(z0, z1) -> ack(z0, z1) [0] The TRS has the following type information: ACK :: s:0 -> s:0 -> c1:c2:c3 s :: s:0 -> s:0 0 :: s:0 c1 :: c1:c2:c3 -> c1:c2:c3 c2 :: c1:c2:c3 -> c1:c2:c3 -> c1:c2:c3 ack :: s:0 -> s:0 -> s:0 c3 :: c4:c5:c6 -> c1:c2:c3 F :: s:0 -> s:0 -> c4:c5:c6 c4 :: c4:c5:c6 -> c4:c5:c6 c5 :: c4:c5:c6 -> c4:c5:c6 c6 :: c1:c2:c3 -> c4:c5:c6 f :: s:0 -> s:0 -> s:0 Rewrite Strategy: INNERMOST ---------------------------------------- (31) 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: ACK_2 F_2 (c) The following functions are completely defined: ack_2 f_2 Due to the following rules being added: ack(v0, v1) -> 0 [0] f(v0, v1) -> 0 [0] And the following fresh constants: const, const1 ---------------------------------------- (32) 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: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) [1] ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) [1] ACK(s(z0), z1) -> c3(F(z0, z0)) [1] F(s(z0), z1) -> c4(F(z0, s(z0))) [1] F(z0, s(z1)) -> c5(F(z1, z0)) [1] F(z0, z1) -> c6(ACK(z0, z1)) [1] ack(0, z0) -> s(z0) [0] ack(s(z0), 0) -> ack(z0, s(0)) [0] ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) [0] ack(s(z0), z1) -> f(z0, z0) [0] f(s(z0), z1) -> f(z0, s(z0)) [0] f(z0, s(z1)) -> f(z1, z0) [0] f(z0, z1) -> ack(z0, z1) [0] ack(v0, v1) -> 0 [0] f(v0, v1) -> 0 [0] The TRS has the following type information: ACK :: s:0 -> s:0 -> c1:c2:c3 s :: s:0 -> s:0 0 :: s:0 c1 :: c1:c2:c3 -> c1:c2:c3 c2 :: c1:c2:c3 -> c1:c2:c3 -> c1:c2:c3 ack :: s:0 -> s:0 -> s:0 c3 :: c4:c5:c6 -> c1:c2:c3 F :: s:0 -> s:0 -> c4:c5:c6 c4 :: c4:c5:c6 -> c4:c5:c6 c5 :: c4:c5:c6 -> c4:c5:c6 c6 :: c1:c2:c3 -> c4:c5:c6 f :: s:0 -> s:0 -> s:0 const :: c1:c2:c3 const1 :: c4:c5:c6 Rewrite Strategy: INNERMOST ---------------------------------------- (33) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (34) 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: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) [1] ACK(s(z0), s(0)) -> c2(ACK(z0, ack(z0, s(0))), ACK(s(z0), 0)) [1] ACK(s(z0), s(s(z1'))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1'))), ACK(s(z0), s(z1'))) [1] ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) [1] ACK(s(z0), s(z1)) -> c2(ACK(z0, 0), ACK(s(z0), z1)) [1] ACK(s(z0), z1) -> c3(F(z0, z0)) [1] F(s(z0), z1) -> c4(F(z0, s(z0))) [1] F(z0, s(z1)) -> c5(F(z1, z0)) [1] F(z0, z1) -> c6(ACK(z0, z1)) [1] ack(0, z0) -> s(z0) [0] ack(s(z0), 0) -> ack(z0, s(0)) [0] ack(s(z0), s(0)) -> ack(z0, ack(z0, s(0))) [0] ack(s(z0), s(s(z1''))) -> ack(z0, ack(z0, ack(s(z0), z1''))) [0] ack(s(z0), s(z1)) -> ack(z0, f(z0, z0)) [0] ack(s(z0), s(z1)) -> ack(z0, 0) [0] ack(s(z0), z1) -> f(z0, z0) [0] f(s(z0), z1) -> f(z0, s(z0)) [0] f(z0, s(z1)) -> f(z1, z0) [0] f(z0, z1) -> ack(z0, z1) [0] ack(v0, v1) -> 0 [0] f(v0, v1) -> 0 [0] The TRS has the following type information: ACK :: s:0 -> s:0 -> c1:c2:c3 s :: s:0 -> s:0 0 :: s:0 c1 :: c1:c2:c3 -> c1:c2:c3 c2 :: c1:c2:c3 -> c1:c2:c3 -> c1:c2:c3 ack :: s:0 -> s:0 -> s:0 c3 :: c4:c5:c6 -> c1:c2:c3 F :: s:0 -> s:0 -> c4:c5:c6 c4 :: c4:c5:c6 -> c4:c5:c6 c5 :: c4:c5:c6 -> c4:c5:c6 c6 :: c1:c2:c3 -> c4:c5:c6 f :: s:0 -> s:0 -> s:0 const :: c1:c2:c3 const1 :: c4:c5:c6 Rewrite Strategy: INNERMOST ---------------------------------------- (35) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 const => 0 const1 => 0 ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: ACK(z, z') -{ 1 }-> 1 + F(z0, z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z0, 1 + 0) :|: z = 1 + z0, z0 >= 0, z' = 0 ACK(z, z') -{ 1 }-> 1 + ACK(z0, f(z0, z0)) + ACK(1 + z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 ACK(z, z') -{ 1 }-> 1 + ACK(z0, ack(z0, ack(1 + z0, z1'))) + ACK(1 + z0, 1 + z1') :|: z' = 1 + (1 + z1'), z = 1 + z0, z1' >= 0, z0 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z0, ack(z0, 1 + 0)) + ACK(1 + z0, 0) :|: z = 1 + z0, z' = 1 + 0, z0 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z0, 0) + ACK(1 + z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 F(z, z') -{ 1 }-> 1 + F(z0, 1 + z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 F(z, z') -{ 1 }-> 1 + F(z1, z0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 F(z, z') -{ 1 }-> 1 + ACK(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 ack(z, z') -{ 0 }-> f(z0, z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 ack(z, z') -{ 0 }-> ack(z0, f(z0, z0)) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 ack(z, z') -{ 0 }-> ack(z0, ack(z0, ack(1 + z0, z1''))) :|: z' = 1 + (1 + z1''), z = 1 + z0, z0 >= 0, z1'' >= 0 ack(z, z') -{ 0 }-> ack(z0, ack(z0, 1 + 0)) :|: z = 1 + z0, z' = 1 + 0, z0 >= 0 ack(z, z') -{ 0 }-> ack(z0, 0) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 ack(z, z') -{ 0 }-> ack(z0, 1 + 0) :|: z = 1 + z0, z0 >= 0, z' = 0 ack(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 ack(z, z') -{ 0 }-> 1 + z0 :|: z0 >= 0, z = 0, z' = z0 f(z, z') -{ 0 }-> f(z0, 1 + z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 f(z, z') -{ 0 }-> f(z1, z0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 f(z, z') -{ 0 }-> ack(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 f(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 ---------------------------------------- (37) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (38) Obligation: Complexity RNTS consisting of the following rules: ACK(z, z') -{ 1 }-> 1 + F(z - 1, z - 1) :|: z' >= 0, z - 1 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 0 ACK(z, z') -{ 1 }-> 1 + ACK(z - 1, f(z - 1, z - 1)) + ACK(1 + (z - 1), z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z - 1, ack(z - 1, ack(1 + (z - 1), z' - 2))) + ACK(1 + (z - 1), 1 + (z' - 2)) :|: z' - 2 >= 0, z - 1 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z - 1, ack(z - 1, 1 + 0)) + ACK(1 + (z - 1), 0) :|: z' = 1 + 0, z - 1 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z - 1, 0) + ACK(1 + (z - 1), z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 F(z, z') -{ 1 }-> 1 + F(z - 1, 1 + (z - 1)) :|: z' >= 0, z - 1 >= 0 F(z, z') -{ 1 }-> 1 + F(z' - 1, z) :|: z' - 1 >= 0, z >= 0 F(z, z') -{ 1 }-> 1 + ACK(z, z') :|: z' >= 0, z >= 0 ack(z, z') -{ 0 }-> f(z - 1, z - 1) :|: z' >= 0, z - 1 >= 0 ack(z, z') -{ 0 }-> ack(z - 1, f(z - 1, z - 1)) :|: z' - 1 >= 0, z - 1 >= 0 ack(z, z') -{ 0 }-> ack(z - 1, ack(z - 1, ack(1 + (z - 1), z' - 2))) :|: z - 1 >= 0, z' - 2 >= 0 ack(z, z') -{ 0 }-> ack(z - 1, ack(z - 1, 1 + 0)) :|: z' = 1 + 0, z - 1 >= 0 ack(z, z') -{ 0 }-> ack(z - 1, 0) :|: z' - 1 >= 0, z - 1 >= 0 ack(z, z') -{ 0 }-> ack(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 0 ack(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 ack(z, z') -{ 0 }-> 1 + z' :|: z' >= 0, z = 0 f(z, z') -{ 0 }-> f(z - 1, 1 + (z - 1)) :|: z' >= 0, z - 1 >= 0 f(z, z') -{ 0 }-> f(z' - 1, z) :|: z' - 1 >= 0, z >= 0 f(z, z') -{ 0 }-> ack(z, z') :|: z' >= 0, z >= 0 f(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 ---------------------------------------- (39) 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: ack(v0, v1) -> null_ack [0] f(v0, v1) -> null_f [0] ACK(v0, v1) -> null_ACK [0] And the following fresh constants: null_ack, null_f, null_ACK, const ---------------------------------------- (40) 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: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) [1] ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) [1] ACK(s(z0), z1) -> c3(F(z0, z0)) [1] F(s(z0), z1) -> c4(F(z0, s(z0))) [1] F(z0, s(z1)) -> c5(F(z1, z0)) [1] F(z0, z1) -> c6(ACK(z0, z1)) [1] ack(0, z0) -> s(z0) [0] ack(s(z0), 0) -> ack(z0, s(0)) [0] ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) [0] ack(s(z0), z1) -> f(z0, z0) [0] f(s(z0), z1) -> f(z0, s(z0)) [0] f(z0, s(z1)) -> f(z1, z0) [0] f(z0, z1) -> ack(z0, z1) [0] ack(v0, v1) -> null_ack [0] f(v0, v1) -> null_f [0] ACK(v0, v1) -> null_ACK [0] The TRS has the following type information: ACK :: s:0:null_ack:null_f -> s:0:null_ack:null_f -> c1:c2:c3:null_ACK s :: s:0:null_ack:null_f -> s:0:null_ack:null_f 0 :: s:0:null_ack:null_f c1 :: c1:c2:c3:null_ACK -> c1:c2:c3:null_ACK c2 :: c1:c2:c3:null_ACK -> c1:c2:c3:null_ACK -> c1:c2:c3:null_ACK ack :: s:0:null_ack:null_f -> s:0:null_ack:null_f -> s:0:null_ack:null_f c3 :: c4:c5:c6 -> c1:c2:c3:null_ACK F :: s:0:null_ack:null_f -> s:0:null_ack:null_f -> c4:c5:c6 c4 :: c4:c5:c6 -> c4:c5:c6 c5 :: c4:c5:c6 -> c4:c5:c6 c6 :: c1:c2:c3:null_ACK -> c4:c5:c6 f :: s:0:null_ack:null_f -> s:0:null_ack:null_f -> s:0:null_ack:null_f null_ack :: s:0:null_ack:null_f null_f :: s:0:null_ack:null_f null_ACK :: c1:c2:c3:null_ACK const :: c4:c5:c6 Rewrite Strategy: INNERMOST ---------------------------------------- (41) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 null_ack => 0 null_f => 0 null_ACK => 0 const => 0 ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: ACK(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 ACK(z, z') -{ 1 }-> 1 + F(z0, z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 ACK(z, z') -{ 1 }-> 1 + ACK(z0, 1 + 0) :|: z = 1 + z0, z0 >= 0, z' = 0 ACK(z, z') -{ 1 }-> 1 + ACK(z0, ack(1 + z0, z1)) + ACK(1 + z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 F(z, z') -{ 1 }-> 1 + F(z0, 1 + z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 F(z, z') -{ 1 }-> 1 + F(z1, z0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 F(z, z') -{ 1 }-> 1 + ACK(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 ack(z, z') -{ 0 }-> f(z0, z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 ack(z, z') -{ 0 }-> ack(z0, ack(1 + z0, z1)) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 ack(z, z') -{ 0 }-> ack(z0, 1 + 0) :|: z = 1 + z0, z0 >= 0, z' = 0 ack(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 ack(z, z') -{ 0 }-> 1 + z0 :|: z0 >= 0, z = 0, z' = z0 f(z, z') -{ 0 }-> f(z0, 1 + z0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 f(z, z') -{ 0 }-> f(z1, z0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 f(z, z') -{ 0 }-> ack(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 f(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (43) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ACK(s(z0), s(z1)) -> c2(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1)) by ACK(s(z0), s(0)) -> c2(ACK(z0, ack(z0, s(0))), ACK(s(z0), 0)) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(0)) -> c2(ACK(z0, ack(z0, s(0))), ACK(s(z0), 0)) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) S tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(0)) -> c2(ACK(z0, ack(z0, s(0))), ACK(s(z0), 0)) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c2_2 ---------------------------------------- (45) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ACK(s(z0), s(0)) -> c2(ACK(z0, ack(z0, s(0))), ACK(s(z0), 0)) by ACK(s(0), s(0)) -> c2(ACK(0, s(s(0))), ACK(s(0), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(0), s(0)) -> c2(ACK(0, s(s(0))), ACK(s(0), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) S tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(0), s(0)) -> c2(ACK(0, s(s(0))), ACK(s(0), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c2_2, c2_1 ---------------------------------------- (47) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) S tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c2_2, c2_1 ---------------------------------------- (49) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, ack(s(z0), z1))), ACK(s(z0), s(z1))) by ACK(s(0), s(s(x1))) -> c2(ACK(0, s(ack(s(0), x1))), ACK(s(0), s(x1))) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(0), s(s(x1))) -> c2(ACK(0, s(ack(s(0), x1))), ACK(s(0), s(x1))) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) S tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(0), s(s(x1))) -> c2(ACK(0, s(ack(s(0), x1))), ACK(s(0), s(x1))) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c2_2, c2_1 ---------------------------------------- (51) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) S tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c2_2, c2_1 ---------------------------------------- (53) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ACK(s(z0), s(z1)) -> c2(ACK(z0, f(z0, z0)), ACK(s(z0), z1)) by ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) S tuples: ACK(s(z0), 0) -> c1(ACK(z0, s(0))) ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c2_2, c2_1 ---------------------------------------- (55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ACK(s(z0), 0) -> c1(ACK(z0, s(0))) by ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) S tuples: ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) F(z0, z1) -> c6(ACK(z0, z1)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c3_1, c4_1, c5_1, c6_1, c2_2, c2_1, c1_1 ---------------------------------------- (57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(z0, z1) -> c6(ACK(z0, z1)) by F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) S tuples: ACK(s(z0), z1) -> c3(F(z0, z0)) F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c3_1, c4_1, c5_1, c2_2, c2_1, c1_1, c6_1 ---------------------------------------- (59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ACK(s(z0), z1) -> c3(F(z0, z0)) by ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) S tuples: F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: F_2, ACK_2 Compound Symbols: c4_1, c5_1, c2_2, c2_1, c1_1, c6_1, c3_1 ---------------------------------------- (61) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: ACK(s(0), s(0)) -> c2(ACK(s(0), 0)) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) S tuples: F(s(z0), z1) -> c4(F(z0, s(z0))) F(z0, s(z1)) -> c5(F(z1, z0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: F_2, ACK_2 Compound Symbols: c4_1, c5_1, c2_2, c2_1, c1_1, c6_1, c3_1 ---------------------------------------- (63) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(z0, s(z1)) -> c5(F(z1, z0)) by F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: F(s(z0), z1) -> c4(F(z0, s(z0))) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) S tuples: F(s(z0), z1) -> c4(F(z0, s(z0))) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: F_2, ACK_2 Compound Symbols: c4_1, c2_2, c2_1, c1_1, c6_1, c3_1, c5_1 ---------------------------------------- (65) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(s(z0), z1) -> c4(F(z0, s(z0))) by F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) S tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c2_2, c2_1, c1_1, c6_1, c3_1, c5_1, c4_1 ---------------------------------------- (67) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ACK(s(x0), s(0)) -> c2(ACK(s(x0), 0)) by ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) S tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c2_2, c2_1, c1_1, c6_1, c3_1, c5_1, c4_1 ---------------------------------------- (69) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ACK(s(x0), s(x1)) -> c2(ACK(s(x0), x1)) by ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(z0), s(s(y1))) -> c2(ACK(s(z0), s(y1))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) S tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(y0), z1) -> c6(ACK(s(y0), z1)) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c2_2, c2_1, c1_1, c6_1, c3_1, c5_1, c4_1 ---------------------------------------- (71) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(s(y0), z1) -> c6(ACK(s(y0), z1)) by F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(z0), s(s(0))) -> c6(ACK(s(z0), s(s(0)))) F(s(z0), s(s(s(y1)))) -> c6(ACK(s(z0), s(s(s(y1))))) F(s(z0), s(s(y1))) -> c6(ACK(s(z0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(z0), s(y1)) -> c6(ACK(s(z0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) F(s(s(y0)), z1) -> c6(ACK(s(s(y0)), z1)) F(s(s(0)), z1) -> c6(ACK(s(s(0)), z1)) F(s(s(s(y0))), z1) -> c6(ACK(s(s(s(y0))), z1)) F(s(s(s(0))), z1) -> c6(ACK(s(s(s(0))), z1)) F(s(s(s(s(y0)))), z1) -> c6(ACK(s(s(s(s(y0)))), z1)) F(s(s(s(y0))), s(0)) -> c6(ACK(s(s(s(y0))), s(0))) F(s(s(0)), s(0)) -> c6(ACK(s(s(0)), s(0))) F(s(s(s(0))), s(0)) -> c6(ACK(s(s(s(0))), s(0))) F(s(s(s(s(y0)))), s(0)) -> c6(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), s(s(0))) -> c6(ACK(s(s(y0)), s(s(0)))) F(s(s(y0)), s(s(s(y1)))) -> c6(ACK(s(s(y0)), s(s(s(y1))))) F(s(z0), s(s(s(0)))) -> c6(ACK(s(z0), s(s(s(0))))) F(s(z0), s(s(s(s(y1))))) -> c6(ACK(s(z0), s(s(s(s(y1)))))) F(s(0), s(s(s(y0)))) -> c6(ACK(s(0), s(s(s(y0))))) F(s(s(0)), s(y0)) -> c6(ACK(s(s(0)), s(y0))) F(s(s(s(y0))), s(y1)) -> c6(ACK(s(s(s(y0))), s(y1))) F(s(s(s(0))), s(y0)) -> c6(ACK(s(s(s(0))), s(y0))) F(s(s(s(s(y0)))), s(y1)) -> c6(ACK(s(s(s(s(y0)))), s(y1))) F(s(s(s(y0))), s(s(0))) -> c6(ACK(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(0))) -> c6(ACK(s(s(0)), s(s(0)))) F(s(s(s(0))), s(s(0))) -> c6(ACK(s(s(s(0))), s(s(0)))) F(s(s(s(s(y0)))), s(s(0))) -> c6(ACK(s(s(s(s(y0)))), s(s(0)))) ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), z1) -> c6(ACK(s(s(y0)), z1)) F(s(s(0)), z1) -> c6(ACK(s(s(0)), z1)) F(s(s(s(y0))), z1) -> c6(ACK(s(s(s(y0))), z1)) F(s(s(s(0))), z1) -> c6(ACK(s(s(s(0))), z1)) F(s(s(s(s(y0)))), z1) -> c6(ACK(s(s(s(s(y0)))), z1)) F(s(s(s(y0))), s(0)) -> c6(ACK(s(s(s(y0))), s(0))) F(s(s(0)), s(0)) -> c6(ACK(s(s(0)), s(0))) F(s(s(s(0))), s(0)) -> c6(ACK(s(s(s(0))), s(0))) F(s(s(s(s(y0)))), s(0)) -> c6(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), s(s(0))) -> c6(ACK(s(s(y0)), s(s(0)))) F(s(s(y0)), s(s(s(y1)))) -> c6(ACK(s(s(y0)), s(s(s(y1))))) F(s(z0), s(s(s(0)))) -> c6(ACK(s(z0), s(s(s(0))))) F(s(z0), s(s(s(s(y1))))) -> c6(ACK(s(z0), s(s(s(s(y1)))))) F(s(0), s(s(s(y0)))) -> c6(ACK(s(0), s(s(s(y0))))) F(s(s(0)), s(y0)) -> c6(ACK(s(s(0)), s(y0))) F(s(s(s(y0))), s(y1)) -> c6(ACK(s(s(s(y0))), s(y1))) F(s(s(s(0))), s(y0)) -> c6(ACK(s(s(s(0))), s(y0))) F(s(s(s(s(y0)))), s(y1)) -> c6(ACK(s(s(s(s(y0)))), s(y1))) F(s(s(s(y0))), s(s(0))) -> c6(ACK(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(0))) -> c6(ACK(s(s(0)), s(s(0)))) F(s(s(s(0))), s(s(0))) -> c6(ACK(s(s(s(0))), s(s(0)))) F(s(s(s(s(y0)))), s(s(0))) -> c6(ACK(s(s(s(s(y0)))), s(s(0)))) S tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(z0, s(s(y0))) -> c5(F(s(y0), z0)) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), z1) -> c6(ACK(s(s(y0)), z1)) F(s(s(0)), z1) -> c6(ACK(s(s(0)), z1)) F(s(s(s(y0))), z1) -> c6(ACK(s(s(s(y0))), z1)) F(s(s(s(0))), z1) -> c6(ACK(s(s(s(0))), z1)) F(s(s(s(s(y0)))), z1) -> c6(ACK(s(s(s(s(y0)))), z1)) F(s(s(s(y0))), s(0)) -> c6(ACK(s(s(s(y0))), s(0))) F(s(s(0)), s(0)) -> c6(ACK(s(s(0)), s(0))) F(s(s(s(0))), s(0)) -> c6(ACK(s(s(s(0))), s(0))) F(s(s(s(s(y0)))), s(0)) -> c6(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), s(s(0))) -> c6(ACK(s(s(y0)), s(s(0)))) F(s(s(y0)), s(s(s(y1)))) -> c6(ACK(s(s(y0)), s(s(s(y1))))) F(s(z0), s(s(s(0)))) -> c6(ACK(s(z0), s(s(s(0))))) F(s(z0), s(s(s(s(y1))))) -> c6(ACK(s(z0), s(s(s(s(y1)))))) F(s(0), s(s(s(y0)))) -> c6(ACK(s(0), s(s(s(y0))))) F(s(s(0)), s(y0)) -> c6(ACK(s(s(0)), s(y0))) F(s(s(s(y0))), s(y1)) -> c6(ACK(s(s(s(y0))), s(y1))) F(s(s(s(0))), s(y0)) -> c6(ACK(s(s(s(0))), s(y0))) F(s(s(s(s(y0)))), s(y1)) -> c6(ACK(s(s(s(s(y0)))), s(y1))) F(s(s(s(y0))), s(s(0))) -> c6(ACK(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(0))) -> c6(ACK(s(s(0)), s(s(0)))) F(s(s(s(0))), s(s(0))) -> c6(ACK(s(s(s(0))), s(s(0)))) F(s(s(s(s(y0)))), s(s(0))) -> c6(ACK(s(s(s(s(y0)))), s(s(0)))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c2_2, c2_1, c1_1, c6_1, c3_1, c5_1, c4_1 ---------------------------------------- (73) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(z0, s(s(y0))) -> c5(F(s(y0), z0)) by F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(z1))) -> c5(F(s(z1), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(z1))) -> c5(F(s(z1), s(s(0)))) F(s(s(s(y1))), s(s(z1))) -> c5(F(s(z1), s(s(s(y1))))) F(s(s(y1)), s(s(z1))) -> c5(F(s(z1), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(z1))) -> c5(F(s(z1), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(s(y0))), s(s(0))) -> c5(F(s(0), s(s(s(y0))))) F(s(s(0)), s(s(0))) -> c5(F(s(0), s(s(0)))) F(s(s(s(y1))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(y1))))) F(s(s(y0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(y0)))) F(s(s(y1)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(y1)))) F(s(s(0)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(0)))) F(z0, s(s(s(y0)))) -> c5(F(s(s(y0)), z0)) F(z0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), z0)) F(z0, s(s(s(0)))) -> c5(F(s(s(0)), z0)) F(z0, s(s(s(s(0))))) -> c5(F(s(s(s(0))), z0)) F(z0, s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), z0)) F(s(0), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(0))) F(s(0), s(s(s(0)))) -> c5(F(s(s(0)), s(0))) F(s(0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(0))) F(s(0), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(0))) F(s(s(s(0))), s(s(z1))) -> c5(F(s(z1), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(z1))) -> c5(F(s(z1), s(s(s(s(y1)))))) F(s(y0), s(s(s(0)))) -> c5(F(s(s(0)), s(y0))) F(s(y1), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(y1))) F(s(y0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(y0))) F(s(y1), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(y1))) F(s(s(0)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(0)))) F(s(s(0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(0)))) F(s(s(0)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(0)))) ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), z1) -> c6(ACK(s(s(y0)), z1)) F(s(s(0)), z1) -> c6(ACK(s(s(0)), z1)) F(s(s(s(y0))), z1) -> c6(ACK(s(s(s(y0))), z1)) F(s(s(s(0))), z1) -> c6(ACK(s(s(s(0))), z1)) F(s(s(s(s(y0)))), z1) -> c6(ACK(s(s(s(s(y0)))), z1)) F(s(s(s(y0))), s(0)) -> c6(ACK(s(s(s(y0))), s(0))) F(s(s(0)), s(0)) -> c6(ACK(s(s(0)), s(0))) F(s(s(s(0))), s(0)) -> c6(ACK(s(s(s(0))), s(0))) F(s(s(s(s(y0)))), s(0)) -> c6(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), s(s(0))) -> c6(ACK(s(s(y0)), s(s(0)))) F(s(s(y0)), s(s(s(y1)))) -> c6(ACK(s(s(y0)), s(s(s(y1))))) F(s(z0), s(s(s(0)))) -> c6(ACK(s(z0), s(s(s(0))))) F(s(z0), s(s(s(s(y1))))) -> c6(ACK(s(z0), s(s(s(s(y1)))))) F(s(0), s(s(s(y0)))) -> c6(ACK(s(0), s(s(s(y0))))) F(s(s(0)), s(y0)) -> c6(ACK(s(s(0)), s(y0))) F(s(s(s(y0))), s(y1)) -> c6(ACK(s(s(s(y0))), s(y1))) F(s(s(s(0))), s(y0)) -> c6(ACK(s(s(s(0))), s(y0))) F(s(s(s(s(y0)))), s(y1)) -> c6(ACK(s(s(s(s(y0)))), s(y1))) F(s(s(s(y0))), s(s(0))) -> c6(ACK(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(0))) -> c6(ACK(s(s(0)), s(s(0)))) F(s(s(s(0))), s(s(0))) -> c6(ACK(s(s(s(0))), s(s(0)))) F(s(s(s(s(y0)))), s(s(0))) -> c6(ACK(s(s(s(s(y0)))), s(s(0)))) F(s(s(s(y0))), s(s(0))) -> c5(F(s(0), s(s(s(y0))))) F(s(s(0)), s(s(0))) -> c5(F(s(0), s(s(0)))) F(s(s(s(y1))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(y1))))) F(s(s(y0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(y0)))) F(s(s(y1)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(y1)))) F(s(s(0)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(0)))) F(z0, s(s(s(y0)))) -> c5(F(s(s(y0)), z0)) F(z0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), z0)) F(z0, s(s(s(0)))) -> c5(F(s(s(0)), z0)) F(z0, s(s(s(s(0))))) -> c5(F(s(s(s(0))), z0)) F(z0, s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), z0)) F(s(0), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(0))) F(s(0), s(s(s(0)))) -> c5(F(s(s(0)), s(0))) F(s(0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(0))) F(s(0), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(0))) F(s(s(s(0))), s(s(z1))) -> c5(F(s(z1), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(z1))) -> c5(F(s(z1), s(s(s(s(y1)))))) F(s(y0), s(s(s(0)))) -> c5(F(s(s(0)), s(y0))) F(s(y1), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(y1))) F(s(y0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(y0))) F(s(y1), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(y1))) F(s(s(0)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(0)))) F(s(s(0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(0)))) F(s(s(0)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(0)))) S tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(s(y1), s(z1)) -> c5(F(z1, s(y1))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), z1) -> c6(ACK(s(s(y0)), z1)) F(s(s(0)), z1) -> c6(ACK(s(s(0)), z1)) F(s(s(s(y0))), z1) -> c6(ACK(s(s(s(y0))), z1)) F(s(s(s(0))), z1) -> c6(ACK(s(s(s(0))), z1)) F(s(s(s(s(y0)))), z1) -> c6(ACK(s(s(s(s(y0)))), z1)) F(s(s(s(y0))), s(0)) -> c6(ACK(s(s(s(y0))), s(0))) F(s(s(0)), s(0)) -> c6(ACK(s(s(0)), s(0))) F(s(s(s(0))), s(0)) -> c6(ACK(s(s(s(0))), s(0))) F(s(s(s(s(y0)))), s(0)) -> c6(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), s(s(0))) -> c6(ACK(s(s(y0)), s(s(0)))) F(s(s(y0)), s(s(s(y1)))) -> c6(ACK(s(s(y0)), s(s(s(y1))))) F(s(z0), s(s(s(0)))) -> c6(ACK(s(z0), s(s(s(0))))) F(s(z0), s(s(s(s(y1))))) -> c6(ACK(s(z0), s(s(s(s(y1)))))) F(s(0), s(s(s(y0)))) -> c6(ACK(s(0), s(s(s(y0))))) F(s(s(0)), s(y0)) -> c6(ACK(s(s(0)), s(y0))) F(s(s(s(y0))), s(y1)) -> c6(ACK(s(s(s(y0))), s(y1))) F(s(s(s(0))), s(y0)) -> c6(ACK(s(s(s(0))), s(y0))) F(s(s(s(s(y0)))), s(y1)) -> c6(ACK(s(s(s(s(y0)))), s(y1))) F(s(s(s(y0))), s(s(0))) -> c6(ACK(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(0))) -> c6(ACK(s(s(0)), s(s(0)))) F(s(s(s(0))), s(s(0))) -> c6(ACK(s(s(s(0))), s(s(0)))) F(s(s(s(s(y0)))), s(s(0))) -> c6(ACK(s(s(s(s(y0)))), s(s(0)))) F(s(s(s(y0))), s(s(0))) -> c5(F(s(0), s(s(s(y0))))) F(s(s(0)), s(s(0))) -> c5(F(s(0), s(s(0)))) F(s(s(s(y1))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(y1))))) F(s(s(y0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(y0)))) F(s(s(y1)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(y1)))) F(s(s(0)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(0)))) F(z0, s(s(s(y0)))) -> c5(F(s(s(y0)), z0)) F(z0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), z0)) F(z0, s(s(s(0)))) -> c5(F(s(s(0)), z0)) F(z0, s(s(s(s(0))))) -> c5(F(s(s(s(0))), z0)) F(z0, s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), z0)) F(s(0), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(0))) F(s(0), s(s(s(0)))) -> c5(F(s(s(0)), s(0))) F(s(0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(0))) F(s(0), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(0))) F(s(s(s(0))), s(s(z1))) -> c5(F(s(z1), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(z1))) -> c5(F(s(z1), s(s(s(s(y1)))))) F(s(y0), s(s(s(0)))) -> c5(F(s(s(0)), s(y0))) F(s(y1), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(y1))) F(s(y0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(y0))) F(s(y1), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(y1))) F(s(s(0)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(0)))) F(s(s(0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(0)))) F(s(s(0)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(0)))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c2_2, c2_1, c1_1, c6_1, c3_1, c5_1, c4_1 ---------------------------------------- (75) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(s(y1), s(z1)) -> c5(F(z1, s(y1))) by F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(z0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(z0))) F(s(z0), s(s(y0))) -> c5(F(s(y0), s(z0))) F(s(s(s(y0))), s(s(0))) -> c5(F(s(0), s(s(s(y0))))) F(s(s(0)), s(s(0))) -> c5(F(s(0), s(s(0)))) F(s(s(s(y1))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(y1))))) F(s(s(y0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(y0)))) F(s(s(y1)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(y1)))) F(s(s(0)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(0)))) F(s(s(s(y0))), s(0)) -> c5(F(0, s(s(s(y0))))) F(s(s(s(s(y0)))), s(0)) -> c5(F(0, s(s(s(s(y0)))))) F(s(s(s(0))), s(0)) -> c5(F(0, s(s(s(0))))) F(s(z0), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(z0))) F(s(z0), s(s(s(0)))) -> c5(F(s(s(0)), s(z0))) F(s(z0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(z0))) F(s(z0), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(z0))) F(s(0), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(0))) F(s(0), s(s(s(0)))) -> c5(F(s(s(0)), s(0))) F(s(0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(0))) F(s(0), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(0))) F(s(s(s(0))), s(s(y0))) -> c5(F(s(y0), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(y0))) -> c5(F(s(y0), s(s(s(s(y1)))))) F(s(s(0)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(0)))) F(s(s(0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(0)))) F(s(s(0)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(0)))) F(s(s(s(y1))), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(s(y1))))) F(s(s(s(0))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(s(y1)))))) F(s(s(s(y0))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(y0))))) F(s(s(s(y1))), s(z1)) -> c5(F(z1, s(s(s(y1))))) F(s(s(s(s(y1)))), s(z1)) -> c5(F(z1, s(s(s(s(y1)))))) F(s(s(s(0))), s(z1)) -> c5(F(z1, s(s(s(0))))) F(s(s(s(s(0)))), s(z1)) -> c5(F(z1, s(s(s(s(0)))))) F(s(s(s(s(s(y1))))), s(z1)) -> c5(F(z1, s(s(s(s(s(y1))))))) F(s(s(s(s(y0)))), s(s(0))) -> c5(F(s(0), s(s(s(s(y0)))))) F(s(s(s(0))), s(s(0))) -> c5(F(s(0), s(s(s(0))))) F(s(s(s(s(0)))), s(s(0))) -> c5(F(s(0), s(s(s(s(0)))))) F(s(s(s(s(s(y0))))), s(s(0))) -> c5(F(s(0), s(s(s(s(s(y0))))))) F(s(s(y0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(y0)))) F(s(s(y1)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(y1)))) F(s(s(s(s(0)))), s(s(y0))) -> c5(F(s(y0), s(s(s(s(0)))))) F(s(s(s(s(s(y1))))), s(s(y0))) -> c5(F(s(y0), s(s(s(s(s(y1))))))) F(s(s(s(s(y0)))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(y0)))))) F(s(s(s(0))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(0)))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(0)))))) F(s(s(s(s(s(y0))))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(s(y0))))))) ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: ack(0, z0) -> s(z0) ack(s(z0), 0) -> ack(z0, s(0)) ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1)) ack(s(z0), z1) -> f(z0, z0) f(s(z0), z1) -> f(z0, s(z0)) f(z0, s(z1)) -> f(z1, z0) f(z0, z1) -> ack(z0, z1) Tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), z1) -> c6(ACK(s(s(y0)), z1)) F(s(s(0)), z1) -> c6(ACK(s(s(0)), z1)) F(s(s(s(y0))), z1) -> c6(ACK(s(s(s(y0))), z1)) F(s(s(s(0))), z1) -> c6(ACK(s(s(s(0))), z1)) F(s(s(s(s(y0)))), z1) -> c6(ACK(s(s(s(s(y0)))), z1)) F(s(s(s(y0))), s(0)) -> c6(ACK(s(s(s(y0))), s(0))) F(s(s(0)), s(0)) -> c6(ACK(s(s(0)), s(0))) F(s(s(s(0))), s(0)) -> c6(ACK(s(s(s(0))), s(0))) F(s(s(s(s(y0)))), s(0)) -> c6(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), s(s(0))) -> c6(ACK(s(s(y0)), s(s(0)))) F(s(s(y0)), s(s(s(y1)))) -> c6(ACK(s(s(y0)), s(s(s(y1))))) F(s(z0), s(s(s(0)))) -> c6(ACK(s(z0), s(s(s(0))))) F(s(z0), s(s(s(s(y1))))) -> c6(ACK(s(z0), s(s(s(s(y1)))))) F(s(0), s(s(s(y0)))) -> c6(ACK(s(0), s(s(s(y0))))) F(s(s(0)), s(y0)) -> c6(ACK(s(s(0)), s(y0))) F(s(s(s(y0))), s(y1)) -> c6(ACK(s(s(s(y0))), s(y1))) F(s(s(s(0))), s(y0)) -> c6(ACK(s(s(s(0))), s(y0))) F(s(s(s(s(y0)))), s(y1)) -> c6(ACK(s(s(s(s(y0)))), s(y1))) F(s(s(s(y0))), s(s(0))) -> c6(ACK(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(0))) -> c6(ACK(s(s(0)), s(s(0)))) F(s(s(s(0))), s(s(0))) -> c6(ACK(s(s(s(0))), s(s(0)))) F(s(s(s(s(y0)))), s(s(0))) -> c6(ACK(s(s(s(s(y0)))), s(s(0)))) F(s(s(s(y0))), s(s(0))) -> c5(F(s(0), s(s(s(y0))))) F(s(s(0)), s(s(0))) -> c5(F(s(0), s(s(0)))) F(s(s(s(y1))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(y1))))) F(s(s(y0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(y0)))) F(s(s(y1)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(y1)))) F(s(s(0)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(0)))) F(z0, s(s(s(y0)))) -> c5(F(s(s(y0)), z0)) F(z0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), z0)) F(z0, s(s(s(0)))) -> c5(F(s(s(0)), z0)) F(z0, s(s(s(s(0))))) -> c5(F(s(s(s(0))), z0)) F(z0, s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), z0)) F(s(0), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(0))) F(s(0), s(s(s(0)))) -> c5(F(s(s(0)), s(0))) F(s(0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(0))) F(s(0), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(0))) F(s(s(s(0))), s(s(z1))) -> c5(F(s(z1), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(z1))) -> c5(F(s(z1), s(s(s(s(y1)))))) F(s(y0), s(s(s(0)))) -> c5(F(s(s(0)), s(y0))) F(s(y1), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(y1))) F(s(y0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(y0))) F(s(y1), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(y1))) F(s(s(0)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(0)))) F(s(s(0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(0)))) F(s(s(0)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(0)))) F(s(s(s(y0))), s(0)) -> c5(F(0, s(s(s(y0))))) F(s(s(s(s(y0)))), s(0)) -> c5(F(0, s(s(s(s(y0)))))) F(s(s(s(0))), s(0)) -> c5(F(0, s(s(s(0))))) F(s(s(s(y1))), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(s(y1))))) F(s(s(s(0))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(s(y1)))))) F(s(s(s(y0))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(y0))))) F(s(s(s(y1))), s(z1)) -> c5(F(z1, s(s(s(y1))))) F(s(s(s(s(y1)))), s(z1)) -> c5(F(z1, s(s(s(s(y1)))))) F(s(s(s(0))), s(z1)) -> c5(F(z1, s(s(s(0))))) F(s(s(s(s(0)))), s(z1)) -> c5(F(z1, s(s(s(s(0)))))) F(s(s(s(s(s(y1))))), s(z1)) -> c5(F(z1, s(s(s(s(s(y1))))))) F(s(s(s(s(y0)))), s(s(0))) -> c5(F(s(0), s(s(s(s(y0)))))) F(s(s(s(0))), s(s(0))) -> c5(F(s(0), s(s(s(0))))) F(s(s(s(s(0)))), s(s(0))) -> c5(F(s(0), s(s(s(s(0)))))) F(s(s(s(s(s(y0))))), s(s(0))) -> c5(F(s(0), s(s(s(s(s(y0))))))) F(s(s(y0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(y0)))) F(s(s(y1)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(y1)))) F(s(s(s(s(0)))), s(s(y0))) -> c5(F(s(y0), s(s(s(s(0)))))) F(s(s(s(s(s(y1))))), s(s(y0))) -> c5(F(s(y0), s(s(s(s(s(y1))))))) F(s(s(s(s(y0)))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(y0)))))) F(s(s(s(0))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(0)))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(0)))))) F(s(s(s(s(s(y0))))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(s(y0))))))) S tuples: ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), ack(z0, ack(s(z0), 0))), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(0)) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), 0)) ACK(s(s(z0)), s(s(x1))) -> c2(ACK(s(z0), f(z0, z0)), ACK(s(s(z0)), s(x1))) ACK(s(z0), s(s(0))) -> c2(ACK(z0, ack(z0, ack(z0, s(0)))), ACK(s(z0), s(0))) ACK(s(z0), s(s(s(z1)))) -> c2(ACK(z0, ack(z0, ack(z0, ack(s(z0), z1)))), ACK(s(z0), s(s(z1)))) ACK(s(z0), s(s(z1))) -> c2(ACK(z0, ack(z0, f(z0, z0))), ACK(s(z0), s(z1))) ACK(s(x0), s(s(x1))) -> c2(ACK(s(x0), s(x1))) ACK(s(0), s(s(x1))) -> c2(ACK(s(0), s(x1))) ACK(s(s(z0)), s(x1)) -> c2(ACK(s(z0), f(z0, s(z0))), ACK(s(s(z0)), x1)) ACK(s(z0), s(x1)) -> c2(ACK(z0, ack(z0, z0)), ACK(s(z0), x1)) ACK(s(s(y0)), 0) -> c1(ACK(s(y0), s(0))) ACK(s(s(s(y0))), 0) -> c1(ACK(s(s(y0)), s(0))) ACK(s(s(0)), 0) -> c1(ACK(s(0), s(0))) F(s(s(y0)), s(0)) -> c6(ACK(s(s(y0)), s(0))) F(s(y0), s(0)) -> c6(ACK(s(y0), s(0))) F(s(0), s(0)) -> c6(ACK(s(0), s(0))) F(s(s(y0)), s(s(y1))) -> c6(ACK(s(s(y0)), s(s(y1)))) F(s(y0), s(s(0))) -> c6(ACK(s(y0), s(s(0)))) F(s(y0), s(s(s(y1)))) -> c6(ACK(s(y0), s(s(s(y1))))) F(s(y0), s(s(y1))) -> c6(ACK(s(y0), s(s(y1)))) F(s(0), s(s(y0))) -> c6(ACK(s(0), s(s(y0)))) F(s(s(y0)), s(y1)) -> c6(ACK(s(s(y0)), s(y1))) F(s(y0), s(y1)) -> c6(ACK(s(y0), s(y1))) F(s(s(y0)), 0) -> c6(ACK(s(s(y0)), 0)) F(s(s(s(y0))), 0) -> c6(ACK(s(s(s(y0))), 0)) F(s(s(0)), 0) -> c6(ACK(s(s(0)), 0)) ACK(s(s(y0)), z1) -> c3(F(s(y0), s(y0))) ACK(s(s(0)), z1) -> c3(F(s(0), s(0))) ACK(s(s(s(y0))), z1) -> c3(F(s(s(y0)), s(s(y0)))) ACK(s(s(s(0))), z1) -> c3(F(s(s(0)), s(s(0)))) ACK(s(s(s(s(y1)))), z1) -> c3(F(s(s(s(y1))), s(s(s(y1))))) F(s(0), s(s(s(y0)))) -> c5(F(s(s(y0)), s(0))) F(s(0), s(s(y0))) -> c5(F(s(y0), s(0))) F(s(0), s(s(0))) -> c5(F(s(0), s(0))) F(s(s(y1)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(y1)))) F(s(s(0)), s(s(y0))) -> c5(F(s(y0), s(s(0)))) F(s(s(s(y1))), s(s(y0))) -> c5(F(s(y0), s(s(s(y1))))) F(s(s(y1)), s(s(y0))) -> c5(F(s(y0), s(s(y1)))) F(s(s(y0)), s(s(0))) -> c5(F(s(0), s(s(y0)))) F(s(y1), s(s(s(y0)))) -> c5(F(s(s(y0)), s(y1))) F(s(y1), s(s(y0))) -> c5(F(s(y0), s(y1))) F(0, s(s(s(y0)))) -> c5(F(s(s(y0)), 0)) F(0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), 0)) F(0, s(s(s(0)))) -> c5(F(s(s(0)), 0)) F(s(s(y0)), z1) -> c4(F(s(y0), s(s(y0)))) F(s(s(s(y0))), z1) -> c4(F(s(s(y0)), s(s(s(y0))))) F(s(s(0)), z1) -> c4(F(s(0), s(s(0)))) F(s(s(s(0))), z1) -> c4(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(y0)))), z1) -> c4(F(s(s(s(y0))), s(s(s(s(y0)))))) ACK(s(s(y0)), s(0)) -> c2(ACK(s(s(y0)), 0)) ACK(s(s(s(y0))), s(0)) -> c2(ACK(s(s(s(y0))), 0)) ACK(s(s(0)), s(0)) -> c2(ACK(s(s(0)), 0)) ACK(s(s(s(0))), s(0)) -> c2(ACK(s(s(s(0))), 0)) ACK(s(s(s(s(y0)))), s(0)) -> c2(ACK(s(s(s(s(y0)))), 0)) ACK(s(s(y0)), s(s(0))) -> c2(ACK(s(s(y0)), s(0))) ACK(s(s(y0)), s(s(s(y1)))) -> c2(ACK(s(s(y0)), s(s(y1)))) ACK(s(z0), s(s(s(0)))) -> c2(ACK(s(z0), s(s(0)))) ACK(s(z0), s(s(s(s(y1))))) -> c2(ACK(s(z0), s(s(s(y1))))) ACK(s(z0), s(s(s(y1)))) -> c2(ACK(s(z0), s(s(y1)))) ACK(s(0), s(s(s(y0)))) -> c2(ACK(s(0), s(s(y0)))) ACK(s(s(y0)), s(s(y1))) -> c2(ACK(s(s(y0)), s(y1))) ACK(s(s(y0)), s(z1)) -> c2(ACK(s(s(y0)), z1)) ACK(s(s(0)), s(z1)) -> c2(ACK(s(s(0)), z1)) ACK(s(s(s(y0))), s(z1)) -> c2(ACK(s(s(s(y0))), z1)) ACK(s(s(s(0))), s(z1)) -> c2(ACK(s(s(s(0))), z1)) ACK(s(s(s(s(y0)))), s(z1)) -> c2(ACK(s(s(s(s(y0)))), z1)) ACK(s(s(s(y0))), s(s(0))) -> c2(ACK(s(s(s(y0))), s(0))) ACK(s(s(0)), s(s(0))) -> c2(ACK(s(s(0)), s(0))) ACK(s(s(s(0))), s(s(0))) -> c2(ACK(s(s(s(0))), s(0))) ACK(s(s(s(s(y0)))), s(s(0))) -> c2(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), z1) -> c6(ACK(s(s(y0)), z1)) F(s(s(0)), z1) -> c6(ACK(s(s(0)), z1)) F(s(s(s(y0))), z1) -> c6(ACK(s(s(s(y0))), z1)) F(s(s(s(0))), z1) -> c6(ACK(s(s(s(0))), z1)) F(s(s(s(s(y0)))), z1) -> c6(ACK(s(s(s(s(y0)))), z1)) F(s(s(s(y0))), s(0)) -> c6(ACK(s(s(s(y0))), s(0))) F(s(s(0)), s(0)) -> c6(ACK(s(s(0)), s(0))) F(s(s(s(0))), s(0)) -> c6(ACK(s(s(s(0))), s(0))) F(s(s(s(s(y0)))), s(0)) -> c6(ACK(s(s(s(s(y0)))), s(0))) F(s(s(y0)), s(s(0))) -> c6(ACK(s(s(y0)), s(s(0)))) F(s(s(y0)), s(s(s(y1)))) -> c6(ACK(s(s(y0)), s(s(s(y1))))) F(s(z0), s(s(s(0)))) -> c6(ACK(s(z0), s(s(s(0))))) F(s(z0), s(s(s(s(y1))))) -> c6(ACK(s(z0), s(s(s(s(y1)))))) F(s(0), s(s(s(y0)))) -> c6(ACK(s(0), s(s(s(y0))))) F(s(s(0)), s(y0)) -> c6(ACK(s(s(0)), s(y0))) F(s(s(s(y0))), s(y1)) -> c6(ACK(s(s(s(y0))), s(y1))) F(s(s(s(0))), s(y0)) -> c6(ACK(s(s(s(0))), s(y0))) F(s(s(s(s(y0)))), s(y1)) -> c6(ACK(s(s(s(s(y0)))), s(y1))) F(s(s(s(y0))), s(s(0))) -> c6(ACK(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(0))) -> c6(ACK(s(s(0)), s(s(0)))) F(s(s(s(0))), s(s(0))) -> c6(ACK(s(s(s(0))), s(s(0)))) F(s(s(s(s(y0)))), s(s(0))) -> c6(ACK(s(s(s(s(y0)))), s(s(0)))) F(s(s(s(y0))), s(s(0))) -> c5(F(s(0), s(s(s(y0))))) F(s(s(0)), s(s(0))) -> c5(F(s(0), s(s(0)))) F(s(s(s(y1))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(y1))))) F(s(s(y0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(y0)))) F(s(s(y1)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(y1)))) F(s(s(0)), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(0)))) F(z0, s(s(s(y0)))) -> c5(F(s(s(y0)), z0)) F(z0, s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), z0)) F(z0, s(s(s(0)))) -> c5(F(s(s(0)), z0)) F(z0, s(s(s(s(0))))) -> c5(F(s(s(s(0))), z0)) F(z0, s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), z0)) F(s(0), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(0))) F(s(0), s(s(s(0)))) -> c5(F(s(s(0)), s(0))) F(s(0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(0))) F(s(0), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(0))) F(s(s(s(0))), s(s(z1))) -> c5(F(s(z1), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(z1))) -> c5(F(s(z1), s(s(s(s(y1)))))) F(s(y0), s(s(s(0)))) -> c5(F(s(s(0)), s(y0))) F(s(y1), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(y1))) F(s(y0), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(y0))) F(s(y1), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(y1))) F(s(s(0)), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(0)))) F(s(s(0)), s(s(s(0)))) -> c5(F(s(s(0)), s(s(0)))) F(s(s(0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(0)))) F(s(s(0)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(0)))) F(s(s(s(y0))), s(0)) -> c5(F(0, s(s(s(y0))))) F(s(s(s(s(y0)))), s(0)) -> c5(F(0, s(s(s(s(y0)))))) F(s(s(s(0))), s(0)) -> c5(F(0, s(s(s(0))))) F(s(s(s(y1))), s(s(s(s(y0))))) -> c5(F(s(s(s(y0))), s(s(s(y1))))) F(s(s(s(0))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(0))))) F(s(s(s(s(y1)))), s(s(s(y0)))) -> c5(F(s(s(y0)), s(s(s(s(y1)))))) F(s(s(s(y0))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(y0))))) F(s(s(s(y1))), s(z1)) -> c5(F(z1, s(s(s(y1))))) F(s(s(s(s(y1)))), s(z1)) -> c5(F(z1, s(s(s(s(y1)))))) F(s(s(s(0))), s(z1)) -> c5(F(z1, s(s(s(0))))) F(s(s(s(s(0)))), s(z1)) -> c5(F(z1, s(s(s(s(0)))))) F(s(s(s(s(s(y1))))), s(z1)) -> c5(F(z1, s(s(s(s(s(y1))))))) F(s(s(s(s(y0)))), s(s(0))) -> c5(F(s(0), s(s(s(s(y0)))))) F(s(s(s(0))), s(s(0))) -> c5(F(s(0), s(s(s(0))))) F(s(s(s(s(0)))), s(s(0))) -> c5(F(s(0), s(s(s(s(0)))))) F(s(s(s(s(s(y0))))), s(s(0))) -> c5(F(s(0), s(s(s(s(s(y0))))))) F(s(s(y0)), s(s(s(s(0))))) -> c5(F(s(s(s(0))), s(s(y0)))) F(s(s(y1)), s(s(s(s(s(y0)))))) -> c5(F(s(s(s(s(y0)))), s(s(y1)))) F(s(s(s(s(0)))), s(s(y0))) -> c5(F(s(y0), s(s(s(s(0)))))) F(s(s(s(s(s(y1))))), s(s(y0))) -> c5(F(s(y0), s(s(s(s(s(y1))))))) F(s(s(s(s(y0)))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(y0)))))) F(s(s(s(0))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(0))))) F(s(s(s(s(0)))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(0)))))) F(s(s(s(s(s(y0))))), s(s(s(0)))) -> c5(F(s(s(0)), s(s(s(s(s(y0))))))) K tuples:none Defined Rule Symbols: ack_2, f_2 Defined Pair Symbols: ACK_2, F_2 Compound Symbols: c2_2, c2_1, c1_1, c6_1, c3_1, c5_1, c4_1 ---------------------------------------- (77) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (78) 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: ack(0, y) -> s(y) [1] ack(s(x), 0) -> ack(x, s(0)) [1] ack(s(x), s(y)) -> ack(x, ack(s(x), y)) [1] f(s(x), y) -> f(x, s(x)) [1] f(x, s(y)) -> f(y, x) [1] f(x, y) -> ack(x, y) [1] ack(s(x), y) -> f(x, x) [1] Rewrite Strategy: INNERMOST ---------------------------------------- (79) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (80) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: ack(0, y) -> s(y) [1] ack(s(x), 0) -> ack(x, s(0)) [1] ack(s(x), s(y)) -> ack(x, ack(s(x), y)) [1] f(s(x), y) -> f(x, s(x)) [1] f(x, s(y)) -> f(y, x) [1] f(x, y) -> ack(x, y) [1] ack(s(x), y) -> f(x, x) [1] The TRS has the following type information: ack :: 0:s -> 0:s -> 0:s 0 :: 0:s s :: 0:s -> 0:s f :: 0:s -> 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (81) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: none (c) The following functions are completely defined: ack_2 f_2 Due to the following rules being added: none And the following fresh constants: none ---------------------------------------- (82) 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: ack(0, y) -> s(y) [1] ack(s(x), 0) -> ack(x, s(0)) [1] ack(s(x), s(y)) -> ack(x, ack(s(x), y)) [1] f(s(x), y) -> f(x, s(x)) [1] f(x, s(y)) -> f(y, x) [1] f(x, y) -> ack(x, y) [1] ack(s(x), y) -> f(x, x) [1] The TRS has the following type information: ack :: 0:s -> 0:s -> 0:s 0 :: 0:s s :: 0:s -> 0:s f :: 0:s -> 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (83) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (84) 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: ack(0, y) -> s(y) [1] ack(s(x), 0) -> ack(x, s(0)) [1] ack(s(x), s(0)) -> ack(x, ack(x, s(0))) [2] ack(s(x), s(s(y'))) -> ack(x, ack(x, ack(s(x), y'))) [2] ack(s(x), s(y)) -> ack(x, f(x, x)) [2] f(s(x), y) -> f(x, s(x)) [1] f(x, s(y)) -> f(y, x) [1] f(x, y) -> ack(x, y) [1] ack(s(x), y) -> f(x, x) [1] The TRS has the following type information: ack :: 0:s -> 0:s -> 0:s 0 :: 0:s s :: 0:s -> 0:s f :: 0:s -> 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (85) 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 ---------------------------------------- (86) Obligation: Complexity RNTS consisting of the following rules: ack(z, z') -{ 1 }-> f(x, x) :|: x >= 0, y >= 0, z = 1 + x, z' = y ack(z, z') -{ 2 }-> ack(x, f(x, x)) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x ack(z, z') -{ 2 }-> ack(x, ack(x, ack(1 + x, y'))) :|: z' = 1 + (1 + y'), x >= 0, y' >= 0, z = 1 + x ack(z, z') -{ 2 }-> ack(x, ack(x, 1 + 0)) :|: x >= 0, z' = 1 + 0, z = 1 + x ack(z, z') -{ 1 }-> ack(x, 1 + 0) :|: x >= 0, z = 1 + x, z' = 0 ack(z, z') -{ 1 }-> 1 + y :|: y >= 0, z = 0, z' = y f(z, z') -{ 1 }-> f(x, 1 + x) :|: x >= 0, y >= 0, z = 1 + x, z' = y f(z, z') -{ 1 }-> f(y, x) :|: z' = 1 + y, x >= 0, y >= 0, z = x f(z, z') -{ 1 }-> ack(x, y) :|: x >= 0, y >= 0, z = x, z' = y ---------------------------------------- (87) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (88) Obligation: Complexity RNTS consisting of the following rules: ack(z, z') -{ 1 }-> f(z - 1, z - 1) :|: z - 1 >= 0, z' >= 0 ack(z, z') -{ 2 }-> ack(z - 1, f(z - 1, z - 1)) :|: z - 1 >= 0, z' - 1 >= 0 ack(z, z') -{ 2 }-> ack(z - 1, ack(z - 1, ack(1 + (z - 1), z' - 2))) :|: z - 1 >= 0, z' - 2 >= 0 ack(z, z') -{ 2 }-> ack(z - 1, ack(z - 1, 1 + 0)) :|: z - 1 >= 0, z' = 1 + 0 ack(z, z') -{ 1 }-> ack(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 0 ack(z, z') -{ 1 }-> 1 + z' :|: z' >= 0, z = 0 f(z, z') -{ 1 }-> f(z - 1, 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0 f(z, z') -{ 1 }-> f(z' - 1, z) :|: z >= 0, z' - 1 >= 0 f(z, z') -{ 1 }-> ack(z, z') :|: z >= 0, z' >= 0 ---------------------------------------- (89) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: none And the following fresh constants: none ---------------------------------------- (90) 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: ack(0, y) -> s(y) [1] ack(s(x), 0) -> ack(x, s(0)) [1] ack(s(x), s(y)) -> ack(x, ack(s(x), y)) [1] f(s(x), y) -> f(x, s(x)) [1] f(x, s(y)) -> f(y, x) [1] f(x, y) -> ack(x, y) [1] ack(s(x), y) -> f(x, x) [1] The TRS has the following type information: ack :: 0:s -> 0:s -> 0:s 0 :: 0:s s :: 0:s -> 0:s f :: 0:s -> 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (91) 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 ---------------------------------------- (92) Obligation: Complexity RNTS consisting of the following rules: ack(z, z') -{ 1 }-> f(x, x) :|: x >= 0, y >= 0, z = 1 + x, z' = y ack(z, z') -{ 1 }-> ack(x, ack(1 + x, y)) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x ack(z, z') -{ 1 }-> ack(x, 1 + 0) :|: x >= 0, z = 1 + x, z' = 0 ack(z, z') -{ 1 }-> 1 + y :|: y >= 0, z = 0, z' = y f(z, z') -{ 1 }-> f(x, 1 + x) :|: x >= 0, y >= 0, z = 1 + x, z' = y f(z, z') -{ 1 }-> f(y, x) :|: z' = 1 + y, x >= 0, y >= 0, z = x f(z, z') -{ 1 }-> ack(x, y) :|: x >= 0, y >= 0, z = x, z' = y Only complete derivations are relevant for the runtime complexity.