YES proof of Secret_07_TRS_4.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished Termination w.r.t. Q of the given QTRS could be proven: (0) QTRS (1) DependencyPairsProof [EQUIVALENT, 0 ms] (2) QDP (3) DependencyGraphProof [EQUIVALENT, 0 ms] (4) AND (5) QDP (6) UsableRulesProof [EQUIVALENT, 0 ms] (7) QDP (8) MRRProof [EQUIVALENT, 8 ms] (9) QDP (10) DependencyGraphProof [EQUIVALENT, 0 ms] (11) AND (12) QDP (13) TransformationProof [EQUIVALENT, 0 ms] (14) QDP (15) DependencyGraphProof [EQUIVALENT, 0 ms] (16) TRUE (17) QDP (18) TransformationProof [EQUIVALENT, 0 ms] (19) QDP (20) TransformationProof [EQUIVALENT, 0 ms] (21) QDP (22) TransformationProof [EQUIVALENT, 0 ms] (23) QDP (24) TransformationProof [EQUIVALENT, 0 ms] (25) QDP (26) DependencyGraphProof [EQUIVALENT, 0 ms] (27) QDP (28) TransformationProof [EQUIVALENT, 0 ms] (29) QDP (30) DependencyGraphProof [EQUIVALENT, 0 ms] (31) QDP (32) TransformationProof [EQUIVALENT, 0 ms] (33) QDP (34) DependencyGraphProof [EQUIVALENT, 0 ms] (35) QDP (36) SplitQDPProof [EQUIVALENT, 0 ms] (37) AND (38) QDP (39) SemLabProof [SOUND, 0 ms] (40) QDP (41) DependencyGraphProof [EQUIVALENT, 0 ms] (42) QDP (43) UsableRulesReductionPairsProof [EQUIVALENT, 10 ms] (44) QDP (45) MRRProof [EQUIVALENT, 0 ms] (46) QDP (47) PisEmptyProof [SOUND, 0 ms] (48) TRUE (49) QDP (50) UsableRulesReductionPairsProof [EQUIVALENT, 0 ms] (51) QDP (52) RFCMatchBoundsDPProof [EQUIVALENT, 0 ms] (53) YES (54) QDP (55) TransformationProof [EQUIVALENT, 0 ms] (56) QDP (57) SplitQDPProof [EQUIVALENT, 0 ms] (58) AND (59) QDP (60) SemLabProof [SOUND, 0 ms] (61) QDP (62) DependencyGraphProof [EQUIVALENT, 0 ms] (63) QDP (64) UsableRulesReductionPairsProof [EQUIVALENT, 7 ms] (65) QDP (66) PisEmptyProof [SOUND, 0 ms] (67) TRUE (68) QDP (69) QDPOrderProof [EQUIVALENT, 95 ms] (70) QDP (71) PisEmptyProof [EQUIVALENT, 0 ms] (72) YES ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) f(g(x, y)) -> g(y, g(f(f(x)), a)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. ---------------------------------------- (1) DependencyPairsProof (EQUIVALENT) Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem. ---------------------------------------- (2) Obligation: Q DP problem: The TRS P consists of the following rules: G(c, g(c, x)) -> G(e, g(d, x)) G(c, g(c, x)) -> G(d, x) G(d, g(d, x)) -> G(c, g(e, x)) G(d, g(d, x)) -> G(e, x) G(e, g(e, x)) -> G(d, g(c, x)) G(e, g(e, x)) -> G(c, x) F(g(x, y)) -> G(y, g(f(f(x)), a)) F(g(x, y)) -> G(f(f(x)), a) F(g(x, y)) -> F(f(x)) F(g(x, y)) -> F(x) G(x, g(y, g(x, y))) -> G(a, g(x, g(y, b))) G(x, g(y, g(x, y))) -> G(x, g(y, b)) G(x, g(y, g(x, y))) -> G(y, b) The TRS R consists of the following rules: g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) f(g(x, y)) -> g(y, g(f(f(x)), a)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (3) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 3 less nodes. ---------------------------------------- (4) Complex Obligation (AND) ---------------------------------------- (5) Obligation: Q DP problem: The TRS P consists of the following rules: G(e, g(e, x)) -> G(d, g(c, x)) G(d, g(d, x)) -> G(c, g(e, x)) G(c, g(c, x)) -> G(e, g(d, x)) G(e, g(e, x)) -> G(c, x) G(c, g(c, x)) -> G(d, x) G(d, g(d, x)) -> G(e, x) G(x, g(y, g(x, y))) -> G(a, g(x, g(y, b))) G(x, g(y, g(x, y))) -> G(x, g(y, b)) The TRS R consists of the following rules: g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) f(g(x, y)) -> g(y, g(f(f(x)), a)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (6) UsableRulesProof (EQUIVALENT) We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R. ---------------------------------------- (7) Obligation: Q DP problem: The TRS P consists of the following rules: G(e, g(e, x)) -> G(d, g(c, x)) G(d, g(d, x)) -> G(c, g(e, x)) G(c, g(c, x)) -> G(e, g(d, x)) G(e, g(e, x)) -> G(c, x) G(c, g(c, x)) -> G(d, x) G(d, g(d, x)) -> G(e, x) G(x, g(y, g(x, y))) -> G(a, g(x, g(y, b))) G(x, g(y, g(x, y))) -> G(x, g(y, b)) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (8) MRRProof (EQUIVALENT) By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented. Strictly oriented dependency pairs: G(e, g(e, x)) -> G(c, x) G(c, g(c, x)) -> G(d, x) G(d, g(d, x)) -> G(e, x) G(x, g(y, g(x, y))) -> G(x, g(y, b)) Used ordering: Polynomial interpretation [POLO]: POL(G(x_1, x_2)) = 2*x_1 + x_2 POL(a) = 0 POL(b) = 0 POL(c) = 2 POL(d) = 2 POL(e) = 2 POL(g(x_1, x_2)) = 1 + 2*x_1 + x_2 ---------------------------------------- (9) Obligation: Q DP problem: The TRS P consists of the following rules: G(e, g(e, x)) -> G(d, g(c, x)) G(d, g(d, x)) -> G(c, g(e, x)) G(c, g(c, x)) -> G(e, g(d, x)) G(x, g(y, g(x, y))) -> G(a, g(x, g(y, b))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (10) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs. ---------------------------------------- (11) Complex Obligation (AND) ---------------------------------------- (12) Obligation: Q DP problem: The TRS P consists of the following rules: G(x, g(y, g(x, y))) -> G(a, g(x, g(y, b))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (13) TransformationProof (EQUIVALENT) By instantiating [LPAR04] the rule G(x, g(y, g(x, y))) -> G(a, g(x, g(y, b))) we obtained the following new rules [LPAR04]: (G(a, g(x1, g(a, x1))) -> G(a, g(a, g(x1, b))),G(a, g(x1, g(a, x1))) -> G(a, g(a, g(x1, b)))) ---------------------------------------- (14) Obligation: Q DP problem: The TRS P consists of the following rules: G(a, g(x1, g(a, x1))) -> G(a, g(a, g(x1, b))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (15) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node. ---------------------------------------- (16) TRUE ---------------------------------------- (17) Obligation: Q DP problem: The TRS P consists of the following rules: G(d, g(d, x)) -> G(c, g(e, x)) G(c, g(c, x)) -> G(e, g(d, x)) G(e, g(e, x)) -> G(d, g(c, x)) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (18) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule G(d, g(d, x)) -> G(c, g(e, x)) at position [1] we obtained the following new rules [LPAR04]: (G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))),G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0)))) (G(d, g(d, g(x1, g(e, x1)))) -> G(c, g(a, g(e, g(x1, b)))),G(d, g(d, g(x1, g(e, x1)))) -> G(c, g(a, g(e, g(x1, b))))) ---------------------------------------- (19) Obligation: Q DP problem: The TRS P consists of the following rules: G(c, g(c, x)) -> G(e, g(d, x)) G(e, g(e, x)) -> G(d, g(c, x)) G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(d, g(d, g(x1, g(e, x1)))) -> G(c, g(a, g(e, g(x1, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (20) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule G(c, g(c, x)) -> G(e, g(d, x)) at position [1] we obtained the following new rules [LPAR04]: (G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))),G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0)))) (G(c, g(c, g(x1, g(d, x1)))) -> G(e, g(a, g(d, g(x1, b)))),G(c, g(c, g(x1, g(d, x1)))) -> G(e, g(a, g(d, g(x1, b))))) ---------------------------------------- (21) Obligation: Q DP problem: The TRS P consists of the following rules: G(e, g(e, x)) -> G(d, g(c, x)) G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(d, g(d, g(x1, g(e, x1)))) -> G(c, g(a, g(e, g(x1, b)))) G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(c, g(c, g(x1, g(d, x1)))) -> G(e, g(a, g(d, g(x1, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (22) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule G(e, g(e, x)) -> G(d, g(c, x)) at position [1] we obtained the following new rules [LPAR04]: (G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))),G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0)))) (G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b)))),G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b))))) ---------------------------------------- (23) Obligation: Q DP problem: The TRS P consists of the following rules: G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(d, g(d, g(x1, g(e, x1)))) -> G(c, g(a, g(e, g(x1, b)))) G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(c, g(c, g(x1, g(d, x1)))) -> G(e, g(a, g(d, g(x1, b)))) G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (24) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule G(d, g(d, g(x1, g(e, x1)))) -> G(c, g(a, g(e, g(x1, b)))) at position [1] we obtained the following new rules [LPAR04]: (G(d, g(d, g(e, g(e, e)))) -> G(c, g(a, g(d, g(c, b)))),G(d, g(d, g(e, g(e, e)))) -> G(c, g(a, g(d, g(c, b))))) ---------------------------------------- (25) Obligation: Q DP problem: The TRS P consists of the following rules: G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(c, g(c, g(x1, g(d, x1)))) -> G(e, g(a, g(d, g(x1, b)))) G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b)))) G(d, g(d, g(e, g(e, e)))) -> G(c, g(a, g(d, g(c, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (26) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (27) Obligation: Q DP problem: The TRS P consists of the following rules: G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(c, g(c, g(x1, g(d, x1)))) -> G(e, g(a, g(d, g(x1, b)))) G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (28) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule G(c, g(c, g(x1, g(d, x1)))) -> G(e, g(a, g(d, g(x1, b)))) at position [1] we obtained the following new rules [LPAR04]: (G(c, g(c, g(d, g(d, d)))) -> G(e, g(a, g(c, g(e, b)))),G(c, g(c, g(d, g(d, d)))) -> G(e, g(a, g(c, g(e, b))))) ---------------------------------------- (29) Obligation: Q DP problem: The TRS P consists of the following rules: G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b)))) G(c, g(c, g(d, g(d, d)))) -> G(e, g(a, g(c, g(e, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (30) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (31) Obligation: Q DP problem: The TRS P consists of the following rules: G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (32) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule G(e, g(e, g(x1, g(c, x1)))) -> G(d, g(a, g(c, g(x1, b)))) at position [1] we obtained the following new rules [LPAR04]: (G(e, g(e, g(c, g(c, c)))) -> G(d, g(a, g(e, g(d, b)))),G(e, g(e, g(c, g(c, c)))) -> G(d, g(a, g(e, g(d, b))))) ---------------------------------------- (33) Obligation: Q DP problem: The TRS P consists of the following rules: G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(e, g(e, g(c, g(c, c)))) -> G(d, g(a, g(e, g(d, b)))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (34) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (35) Obligation: Q DP problem: The TRS P consists of the following rules: G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (36) SplitQDPProof (EQUIVALENT) We show in the first subproof that some pairs and rules can be removed, afterwards, we continue with the remaining DP-Problem ---------------------------------------- (37) Complex Obligation (AND) ---------------------------------------- (38) Obligation: Q DP problem: The TRS P consists of the following rules: G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) The TRS R consists of the following rules: g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (39) SemLabProof (SOUND) We found the following model for the rules of the TRSs R and P. Interpretation over the domain with elements from 0 to 1. a: 0 b: 1 c: 0 G: 0 d: 0 e: 0 g: 0 By semantic labelling [SEMLAB] we obtain the following labelled QDP problem. ---------------------------------------- (40) Obligation: Q DP problem: The TRS P consists of the following rules: G.0-0(d., g.0-0(d., g.0-0(e., x0))) -> G.0-0(c., g.0-0(d., g.0-0(c., x0))) G.0-0(c., g.0-0(c., g.0-0(d., x0))) -> G.0-0(e., g.0-0(c., g.0-0(e., x0))) G.0-0(c., g.0-0(c., g.0-1(d., x0))) -> G.0-0(e., g.0-0(c., g.0-1(e., x0))) G.0-0(d., g.0-0(d., g.0-1(e., x0))) -> G.0-0(c., g.0-0(d., g.0-1(c., x0))) G.0-0(e., g.0-0(e., g.0-0(c., x0))) -> G.0-0(d., g.0-0(e., g.0-0(d., x0))) G.0-0(e., g.0-0(e., g.0-1(c., x0))) -> G.0-0(d., g.0-0(e., g.0-1(d., x0))) The TRS R consists of the following rules: g.0-0(e., g.0-0(e., x)) -> g.0-0(d., g.0-0(c., x)) g.0-0(e., g.0-1(e., x)) -> g.0-0(d., g.0-1(c., x)) g.0-0(d., g.0-0(d., x)) -> g.0-0(c., g.0-0(e., x)) g.0-0(d., g.0-1(d., x)) -> g.0-0(c., g.0-1(e., x)) g.0-0(c., g.0-0(c., x)) -> g.0-0(e., g.0-0(d., x)) g.0-0(c., g.0-1(c., x)) -> g.0-0(e., g.0-1(d., x)) g.0-0(x, g.0-0(y, g.0-0(x, y))) -> g.0-0(a., g.0-0(x, g.0-1(y, b.))) g.0-0(x, g.1-0(y, g.0-1(x, y))) -> g.0-0(a., g.0-0(x, g.1-1(y, b.))) g.1-0(x, g.0-0(y, g.1-0(x, y))) -> g.0-0(a., g.1-0(x, g.0-1(y, b.))) g.1-0(x, g.1-0(y, g.1-1(x, y))) -> g.0-0(a., g.1-0(x, g.1-1(y, b.))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (41) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes. ---------------------------------------- (42) Obligation: Q DP problem: The TRS P consists of the following rules: G.0-0(c., g.0-0(c., g.0-0(d., x0))) -> G.0-0(e., g.0-0(c., g.0-0(e., x0))) G.0-0(e., g.0-0(e., g.0-0(c., x0))) -> G.0-0(d., g.0-0(e., g.0-0(d., x0))) G.0-0(d., g.0-0(d., g.0-0(e., x0))) -> G.0-0(c., g.0-0(d., g.0-0(c., x0))) The TRS R consists of the following rules: g.0-0(e., g.0-0(e., x)) -> g.0-0(d., g.0-0(c., x)) g.0-0(e., g.0-1(e., x)) -> g.0-0(d., g.0-1(c., x)) g.0-0(d., g.0-0(d., x)) -> g.0-0(c., g.0-0(e., x)) g.0-0(d., g.0-1(d., x)) -> g.0-0(c., g.0-1(e., x)) g.0-0(c., g.0-0(c., x)) -> g.0-0(e., g.0-0(d., x)) g.0-0(c., g.0-1(c., x)) -> g.0-0(e., g.0-1(d., x)) g.0-0(x, g.0-0(y, g.0-0(x, y))) -> g.0-0(a., g.0-0(x, g.0-1(y, b.))) g.0-0(x, g.1-0(y, g.0-1(x, y))) -> g.0-0(a., g.0-0(x, g.1-1(y, b.))) g.1-0(x, g.0-0(y, g.1-0(x, y))) -> g.0-0(a., g.1-0(x, g.0-1(y, b.))) g.1-0(x, g.1-0(y, g.1-1(x, y))) -> g.0-0(a., g.1-0(x, g.1-1(y, b.))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (43) UsableRulesReductionPairsProof (EQUIVALENT) By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well. No dependency pairs are removed. The following rules are removed from R: g.0-0(x, g.1-0(y, g.0-1(x, y))) -> g.0-0(a., g.0-0(x, g.1-1(y, b.))) g.1-0(x, g.0-0(y, g.1-0(x, y))) -> g.0-0(a., g.1-0(x, g.0-1(y, b.))) g.1-0(x, g.1-0(y, g.1-1(x, y))) -> g.0-0(a., g.1-0(x, g.1-1(y, b.))) Used ordering: POLO with Polynomial interpretation [POLO]: POL(G.0-0(x_1, x_2)) = x_1 + x_2 POL(a.) = 0 POL(b.) = 0 POL(c.) = 0 POL(d.) = 0 POL(e.) = 0 POL(g.0-0(x_1, x_2)) = x_1 + x_2 POL(g.0-1(x_1, x_2)) = x_1 + x_2 POL(g.1-0(x_1, x_2)) = 1 + x_1 + x_2 POL(g.1-1(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (44) Obligation: Q DP problem: The TRS P consists of the following rules: G.0-0(c., g.0-0(c., g.0-0(d., x0))) -> G.0-0(e., g.0-0(c., g.0-0(e., x0))) G.0-0(e., g.0-0(e., g.0-0(c., x0))) -> G.0-0(d., g.0-0(e., g.0-0(d., x0))) G.0-0(d., g.0-0(d., g.0-0(e., x0))) -> G.0-0(c., g.0-0(d., g.0-0(c., x0))) The TRS R consists of the following rules: g.0-0(d., g.0-0(d., x)) -> g.0-0(c., g.0-0(e., x)) g.0-0(c., g.0-0(c., x)) -> g.0-0(e., g.0-0(d., x)) g.0-0(e., g.0-0(e., x)) -> g.0-0(d., g.0-0(c., x)) g.0-0(c., g.0-1(c., x)) -> g.0-0(e., g.0-1(d., x)) g.0-0(x, g.0-0(y, g.0-0(x, y))) -> g.0-0(a., g.0-0(x, g.0-1(y, b.))) g.0-0(d., g.0-1(d., x)) -> g.0-0(c., g.0-1(e., x)) g.0-0(e., g.0-1(e., x)) -> g.0-0(d., g.0-1(c., x)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (45) MRRProof (EQUIVALENT) By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented. Strictly oriented rules of the TRS R: g.0-0(x, g.0-0(y, g.0-0(x, y))) -> g.0-0(a., g.0-0(x, g.0-1(y, b.))) Used ordering: Polynomial interpretation [POLO]: POL(G.0-0(x_1, x_2)) = x_1 + x_2 POL(a.) = 0 POL(b.) = 0 POL(c.) = 0 POL(d.) = 0 POL(e.) = 0 POL(g.0-0(x_1, x_2)) = 1 + x_1 + x_2 POL(g.0-1(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (46) Obligation: Q DP problem: The TRS P consists of the following rules: G.0-0(c., g.0-0(c., g.0-0(d., x0))) -> G.0-0(e., g.0-0(c., g.0-0(e., x0))) G.0-0(e., g.0-0(e., g.0-0(c., x0))) -> G.0-0(d., g.0-0(e., g.0-0(d., x0))) G.0-0(d., g.0-0(d., g.0-0(e., x0))) -> G.0-0(c., g.0-0(d., g.0-0(c., x0))) The TRS R consists of the following rules: g.0-0(d., g.0-0(d., x)) -> g.0-0(c., g.0-0(e., x)) g.0-0(c., g.0-0(c., x)) -> g.0-0(e., g.0-0(d., x)) g.0-0(e., g.0-0(e., x)) -> g.0-0(d., g.0-0(c., x)) g.0-0(c., g.0-1(c., x)) -> g.0-0(e., g.0-1(d., x)) g.0-0(d., g.0-1(d., x)) -> g.0-0(c., g.0-1(e., x)) g.0-0(e., g.0-1(e., x)) -> g.0-0(d., g.0-1(c., x)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (47) PisEmptyProof (SOUND) The TRS P is empty. Hence, there is no (P,Q,R) chain. ---------------------------------------- (48) TRUE ---------------------------------------- (49) Obligation: Q DP problem: The TRS P consists of the following rules: G(c, g(c, g(d, x0))) -> G(e, g(c, g(e, x0))) G(e, g(e, g(c, x0))) -> G(d, g(e, g(d, x0))) G(d, g(d, g(e, x0))) -> G(c, g(d, g(c, x0))) The TRS R consists of the following rules: g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(e, g(e, x)) -> g(d, g(c, x)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (50) UsableRulesReductionPairsProof (EQUIVALENT) First, we A-transformed [FROCOS05] the QDP-Problem. Then we obtain the following A-transformed DP problem. The pairs P are: c1(c(d(x0))) -> e1(c(e(x0))) e1(e(c(x0))) -> d1(e(d(x0))) d1(d(e(x0))) -> c1(d(c(x0))) and the Q and R are: Q restricted rewrite system: The TRS R consists of the following rules: c(c(x)) -> e(d(x)) e(e(x)) -> d(c(x)) d(d(x)) -> c(e(x)) Q is empty. By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well. No dependency pairs are removed. The following rules are removed from R: g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) g(e, g(e, x)) -> g(d, g(c, x)) Used ordering: POLO with Polynomial interpretation [POLO]: POL(c(x_1)) = 2*x_1 POL(c1(x_1)) = 2*x_1 POL(d(x_1)) = 2*x_1 POL(d1(x_1)) = 2*x_1 POL(e(x_1)) = 2*x_1 POL(e1(x_1)) = 2*x_1 ---------------------------------------- (51) Obligation: Q DP problem: The TRS P consists of the following rules: c1(c(d(x0))) -> e1(c(e(x0))) e1(e(c(x0))) -> d1(e(d(x0))) d1(d(e(x0))) -> c1(d(c(x0))) The TRS R consists of the following rules: c(c(x)) -> e(d(x)) e(e(x)) -> d(c(x)) d(d(x)) -> c(e(x)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (52) RFCMatchBoundsDPProof (EQUIVALENT) Finiteness of the DP problem can be shown by a matchbound of 1. As the DP problem is minimal we only have to initialize the certificate graph by the rules of P: c1(c(d(x0))) -> e1(c(e(x0))) e1(e(c(x0))) -> d1(e(d(x0))) d1(d(e(x0))) -> c1(d(c(x0))) To find matches we regarded all rules of R and P: c(c(x)) -> e(d(x)) e(e(x)) -> d(c(x)) d(d(x)) -> c(e(x)) c1(c(d(x0))) -> e1(c(e(x0))) e1(e(c(x0))) -> d1(e(d(x0))) d1(d(e(x0))) -> c1(d(c(x0))) The certificate found is represented by the following graph. The certificate consists of the following enumerated nodes: 377, 378, 379, 380, 381, 382, 383, 384, 385, 386, 387 Node 377 is start node and node 378 is final node. Those nodes are connected through the following edges: * 377 to 379 labelled e1_1(0)* 377 to 381 labelled d1_1(0)* 377 to 383 labelled c1_1(0)* 378 to 378 labelled #_1(0)* 379 to 380 labelled c_1(0)* 380 to 378 labelled e_1(0)* 380 to 385 labelled d_1(1)* 381 to 382 labelled e_1(0)* 382 to 378 labelled d_1(0)* 382 to 386 labelled c_1(1)* 383 to 384 labelled d_1(0)* 384 to 378 labelled c_1(0)* 384 to 387 labelled e_1(1)* 385 to 378 labelled c_1(1)* 385 to 387 labelled e_1(1)* 386 to 378 labelled e_1(1)* 386 to 385 labelled d_1(1)* 387 to 378 labelled d_1(1)* 387 to 386 labelled c_1(1) ---------------------------------------- (53) YES ---------------------------------------- (54) Obligation: Q DP problem: The TRS P consists of the following rules: F(g(x, y)) -> F(x) F(g(x, y)) -> F(f(x)) The TRS R consists of the following rules: g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) f(g(x, y)) -> g(y, g(f(f(x)), a)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (55) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule F(g(x, y)) -> F(f(x)) at position [0] we obtained the following new rules [LPAR04]: (F(g(g(x0, x1), y1)) -> F(g(x1, g(f(f(x0)), a))),F(g(g(x0, x1), y1)) -> F(g(x1, g(f(f(x0)), a)))) ---------------------------------------- (56) Obligation: Q DP problem: The TRS P consists of the following rules: F(g(x, y)) -> F(x) F(g(g(x0, x1), y1)) -> F(g(x1, g(f(f(x0)), a))) The TRS R consists of the following rules: g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) f(g(x, y)) -> g(y, g(f(f(x)), a)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (57) SplitQDPProof (EQUIVALENT) We show in the first subproof that some pairs and rules can be removed, afterwards, we continue with the remaining DP-Problem ---------------------------------------- (58) Complex Obligation (AND) ---------------------------------------- (59) Obligation: Q DP problem: The TRS P consists of the following rules: F(g(x, y)) -> F(x) F(g(g(x0, x1), y1)) -> F(g(x1, g(f(f(x0)), a))) The TRS R consists of the following rules: g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) f(g(x, y)) -> g(y, g(f(f(x)), a)) g(x, g(y, g(x, y))) -> g(a, g(x, g(y, b))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (60) SemLabProof (SOUND) We found the following model for the rules of the TRSs R and P. Interpretation over the domain with elements from 0 to 1. a: 1 b: 0 c: 0 d: 0 f: 0 F: 0 e: 0 g: 0 By semantic labelling [SEMLAB] we obtain the following labelled QDP problem. ---------------------------------------- (61) Obligation: Q DP problem: The TRS P consists of the following rules: F.0(g.0-0(x, y)) -> F.0(x) F.0(g.0-1(x, y)) -> F.0(x) F.0(g.1-0(x, y)) -> F.1(x) F.0(g.1-1(x, y)) -> F.1(x) F.0(g.0-0(g.0-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-1(g.0-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-0(g.0-1(x0, x1), y1)) -> F.0(g.1-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-1(g.0-1(x0, x1), y1)) -> F.0(g.1-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-0(g.1-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.))) F.0(g.0-1(g.1-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.))) F.0(g.0-0(g.1-1(x0, x1), y1)) -> F.0(g.1-0(x1, g.0-1(f.0(f.1(x0)), a.))) F.0(g.0-1(g.1-1(x0, x1), y1)) -> F.0(g.1-0(x1, g.0-1(f.0(f.1(x0)), a.))) The TRS R consists of the following rules: g.0-0(c., g.0-0(c., x)) -> g.0-0(e., g.0-0(d., x)) g.0-0(c., g.0-1(c., x)) -> g.0-0(e., g.0-1(d., x)) g.0-0(d., g.0-0(d., x)) -> g.0-0(c., g.0-0(e., x)) g.0-0(d., g.0-1(d., x)) -> g.0-0(c., g.0-1(e., x)) g.0-0(e., g.0-0(e., x)) -> g.0-0(d., g.0-0(c., x)) g.0-0(e., g.0-1(e., x)) -> g.0-0(d., g.0-1(c., x)) f.0(g.0-0(x, y)) -> g.0-0(y, g.0-1(f.0(f.0(x)), a.)) f.0(g.0-1(x, y)) -> g.1-0(y, g.0-1(f.0(f.0(x)), a.)) f.0(g.1-0(x, y)) -> g.0-0(y, g.0-1(f.0(f.1(x)), a.)) f.0(g.1-1(x, y)) -> g.1-0(y, g.0-1(f.0(f.1(x)), a.)) g.0-0(x, g.0-0(y, g.0-0(x, y))) -> g.1-0(a., g.0-0(x, g.0-0(y, b.))) g.0-0(x, g.1-0(y, g.0-1(x, y))) -> g.1-0(a., g.0-0(x, g.1-0(y, b.))) g.1-0(x, g.0-0(y, g.1-0(x, y))) -> g.1-0(a., g.1-0(x, g.0-0(y, b.))) g.1-0(x, g.1-0(y, g.1-1(x, y))) -> g.1-0(a., g.1-0(x, g.1-0(y, b.))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (62) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 6 less nodes. ---------------------------------------- (63) Obligation: Q DP problem: The TRS P consists of the following rules: F.0(g.0-0(x, y)) -> F.0(x) F.0(g.0-1(x, y)) -> F.0(x) F.0(g.0-0(g.0-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-0(g.1-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.))) F.0(g.0-1(g.0-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-1(g.1-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.))) The TRS R consists of the following rules: g.0-0(c., g.0-0(c., x)) -> g.0-0(e., g.0-0(d., x)) g.0-0(c., g.0-1(c., x)) -> g.0-0(e., g.0-1(d., x)) g.0-0(d., g.0-0(d., x)) -> g.0-0(c., g.0-0(e., x)) g.0-0(d., g.0-1(d., x)) -> g.0-0(c., g.0-1(e., x)) g.0-0(e., g.0-0(e., x)) -> g.0-0(d., g.0-0(c., x)) g.0-0(e., g.0-1(e., x)) -> g.0-0(d., g.0-1(c., x)) f.0(g.0-0(x, y)) -> g.0-0(y, g.0-1(f.0(f.0(x)), a.)) f.0(g.0-1(x, y)) -> g.1-0(y, g.0-1(f.0(f.0(x)), a.)) f.0(g.1-0(x, y)) -> g.0-0(y, g.0-1(f.0(f.1(x)), a.)) f.0(g.1-1(x, y)) -> g.1-0(y, g.0-1(f.0(f.1(x)), a.)) g.0-0(x, g.0-0(y, g.0-0(x, y))) -> g.1-0(a., g.0-0(x, g.0-0(y, b.))) g.0-0(x, g.1-0(y, g.0-1(x, y))) -> g.1-0(a., g.0-0(x, g.1-0(y, b.))) g.1-0(x, g.0-0(y, g.1-0(x, y))) -> g.1-0(a., g.1-0(x, g.0-0(y, b.))) g.1-0(x, g.1-0(y, g.1-1(x, y))) -> g.1-0(a., g.1-0(x, g.1-0(y, b.))) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (64) UsableRulesReductionPairsProof (EQUIVALENT) By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well. No dependency pairs are removed. The following rules are removed from R: g.0-0(c., g.0-0(c., x)) -> g.0-0(e., g.0-0(d., x)) g.0-0(d., g.0-0(d., x)) -> g.0-0(c., g.0-0(e., x)) g.0-0(e., g.0-0(e., x)) -> g.0-0(d., g.0-0(c., x)) f.0(g.1-1(x, y)) -> g.1-0(y, g.0-1(f.0(f.1(x)), a.)) g.0-0(x, g.0-0(y, g.0-0(x, y))) -> g.1-0(a., g.0-0(x, g.0-0(y, b.))) g.0-0(x, g.1-0(y, g.0-1(x, y))) -> g.1-0(a., g.0-0(x, g.1-0(y, b.))) g.1-0(x, g.0-0(y, g.1-0(x, y))) -> g.1-0(a., g.1-0(x, g.0-0(y, b.))) g.1-0(x, g.1-0(y, g.1-1(x, y))) -> g.1-0(a., g.1-0(x, g.1-0(y, b.))) Used ordering: POLO with Polynomial interpretation [POLO]: POL(F.0(x_1)) = x_1 POL(a.) = 0 POL(c.) = 0 POL(d.) = 0 POL(e.) = 0 POL(f.0(x_1)) = x_1 POL(f.1(x_1)) = x_1 POL(g.0-0(x_1, x_2)) = x_1 + x_2 POL(g.0-1(x_1, x_2)) = x_1 + x_2 POL(g.1-0(x_1, x_2)) = x_1 + x_2 POL(g.1-1(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (65) Obligation: Q DP problem: The TRS P consists of the following rules: F.0(g.0-0(x, y)) -> F.0(x) F.0(g.0-1(x, y)) -> F.0(x) F.0(g.0-0(g.0-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-0(g.1-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.))) F.0(g.0-1(g.0-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.))) F.0(g.0-1(g.1-0(x0, x1), y1)) -> F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.))) The TRS R consists of the following rules: f.0(g.0-0(x, y)) -> g.0-0(y, g.0-1(f.0(f.0(x)), a.)) f.0(g.0-1(x, y)) -> g.1-0(y, g.0-1(f.0(f.0(x)), a.)) f.0(g.1-0(x, y)) -> g.0-0(y, g.0-1(f.0(f.1(x)), a.)) g.0-0(c., g.0-1(c., x)) -> g.0-0(e., g.0-1(d., x)) g.0-0(d., g.0-1(d., x)) -> g.0-0(c., g.0-1(e., x)) g.0-0(e., g.0-1(e., x)) -> g.0-0(d., g.0-1(c., x)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (66) PisEmptyProof (SOUND) The TRS P is empty. Hence, there is no (P,Q,R) chain. ---------------------------------------- (67) TRUE ---------------------------------------- (68) Obligation: Q DP problem: The TRS P consists of the following rules: F(g(x, y)) -> F(x) F(g(g(x0, x1), y1)) -> F(g(x1, g(f(f(x0)), a))) The TRS R consists of the following rules: f(g(x, y)) -> g(y, g(f(f(x)), a)) g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (69) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F(g(x, y)) -> F(x) F(g(g(x0, x1), y1)) -> F(g(x1, g(f(f(x0)), a))) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) : <<< POL(F(x_1)) = [[1]] + [[2, 0]] * x_1 >>> <<< POL(g(x_1, x_2)) = [[1], [1]] + [[1, 1], [0, 0]] * x_1 + [[0, 0], [1, 1]] * x_2 >>> <<< POL(f(x_1)) = [[0], [0]] + [[0, 1], [3, 0]] * x_1 >>> <<< POL(a) = [[0], [0]] >>> <<< POL(e) = [[0], [0]] >>> <<< POL(d) = [[0], [0]] >>> <<< POL(c) = [[0], [0]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f(g(x, y)) -> g(y, g(f(f(x)), a)) g(e, g(e, x)) -> g(d, g(c, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(c, g(c, x)) -> g(e, g(d, x)) ---------------------------------------- (70) Obligation: Q DP problem: P is empty. The TRS R consists of the following rules: f(g(x, y)) -> g(y, g(f(f(x)), a)) g(c, g(c, x)) -> g(e, g(d, x)) g(d, g(d, x)) -> g(c, g(e, x)) g(e, g(e, x)) -> g(d, g(c, x)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (71) PisEmptyProof (EQUIVALENT) The TRS P is empty. Hence, there is no (P,Q,R) chain. ---------------------------------------- (72) YES