YES proof of Endrullis_06_labeling.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) TransformationProof [EQUIVALENT, 0 ms] (4) QDP (5) TransformationProof [EQUIVALENT, 0 ms] (6) QDP (7) SemLabProof [SOUND, 790 ms] (8) QDP (9) DependencyGraphProof [EQUIVALENT, 0 ms] (10) QDP (11) QDPOrderProof [EQUIVALENT, 198 ms] (12) QDP (13) DependencyGraphProof [EQUIVALENT, 0 ms] (14) AND (15) QDP (16) QDPOrderProof [EQUIVALENT, 21 ms] (17) QDP (18) DependencyGraphProof [EQUIVALENT, 0 ms] (19) QDP (20) QDPOrderProof [EQUIVALENT, 0 ms] (21) QDP (22) DependencyGraphProof [EQUIVALENT, 0 ms] (23) QDP (24) QDPOrderProof [EQUIVALENT, 17 ms] (25) QDP (26) PisEmptyProof [EQUIVALENT, 0 ms] (27) YES (28) QDP (29) QDPOrderProof [EQUIVALENT, 0 ms] (30) QDP (31) DependencyGraphProof [EQUIVALENT, 0 ms] (32) QDP (33) QDPOrderProof [EQUIVALENT, 17 ms] (34) QDP (35) DependencyGraphProof [EQUIVALENT, 0 ms] (36) QDP (37) QDPOrderProof [EQUIVALENT, 0 ms] (38) QDP (39) DependencyGraphProof [EQUIVALENT, 0 ms] (40) TRUE ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: f(f(x, y, a), z, w) -> f(z, w, f(y, x, z)) 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: F(f(x, y, a), z, w) -> F(z, w, f(y, x, z)) F(f(x, y, a), z, w) -> F(y, x, z) The TRS R consists of the following rules: f(f(x, y, a), z, w) -> f(z, w, f(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (3) TransformationProof (EQUIVALENT) By forward instantiating [JAR06] the rule F(f(x, y, a), z, w) -> F(z, w, f(y, x, z)) we obtained the following new rules [LPAR04]: (F(f(x0, x1, a), f(y_0, y_1, a), x3) -> F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a))),F(f(x0, x1, a), f(y_0, y_1, a), x3) -> F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a)))) ---------------------------------------- (4) Obligation: Q DP problem: The TRS P consists of the following rules: F(f(x, y, a), z, w) -> F(y, x, z) F(f(x0, x1, a), f(y_0, y_1, a), x3) -> F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a))) The TRS R consists of the following rules: f(f(x, y, a), z, w) -> f(z, w, f(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (5) TransformationProof (EQUIVALENT) By forward instantiating [JAR06] the rule F(f(x, y, a), z, w) -> F(y, x, z) we obtained the following new rules [LPAR04]: (F(f(x0, f(y_0, y_1, a), a), x2, x3) -> F(f(y_0, y_1, a), x0, x2),F(f(x0, f(y_0, y_1, a), a), x2, x3) -> F(f(y_0, y_1, a), x0, x2)) (F(f(f(y_2, y_3, a), f(y_0, y_1, a), a), x2, x3) -> F(f(y_0, y_1, a), f(y_2, y_3, a), x2),F(f(f(y_2, y_3, a), f(y_0, y_1, a), a), x2, x3) -> F(f(y_0, y_1, a), f(y_2, y_3, a), x2)) ---------------------------------------- (6) Obligation: Q DP problem: The TRS P consists of the following rules: F(f(x0, x1, a), f(y_0, y_1, a), x3) -> F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a))) F(f(x0, f(y_0, y_1, a), a), x2, x3) -> F(f(y_0, y_1, a), x0, x2) F(f(f(y_2, y_3, a), f(y_0, y_1, a), a), x2, x3) -> F(f(y_0, y_1, a), f(y_2, y_3, a), x2) The TRS R consists of the following rules: f(f(x, y, a), z, w) -> f(z, w, f(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (7) 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 f: 0 F: 0 By semantic labelling [SEMLAB] we obtain the following labelled QDP problem. ---------------------------------------- (8) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-1(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-1(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-1(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-1(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-1(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-1(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-1(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-1(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-1(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-1(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-1(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-1(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (9) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 24 less nodes. ---------------------------------------- (10) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-1-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-1-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (11) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F.0-0-0(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO]: POL(F.0-0-0(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(F.0-0-1(x_1, x_2, x_3)) = 1 + x_1 + x_2 POL(F.0-1-0(x_1, x_2, x_3)) = 1 + x_1 + x_3 POL(F.0-1-1(x_1, x_2, x_3)) = 1 + x_1 POL(a.) = 0 POL(f.0-0-0(x_1, x_2, x_3)) = 0 POL(f.0-0-1(x_1, x_2, x_3)) = x_1 + x_2 POL(f.0-1-0(x_1, x_2, x_3)) = 0 POL(f.0-1-1(x_1, x_2, x_3)) = x_3 POL(f.1-0-0(x_1, x_2, x_3)) = 0 POL(f.1-0-1(x_1, x_2, x_3)) = 1 + x_2 POL(f.1-1-0(x_1, x_2, x_3)) = 0 POL(f.1-1-1(x_1, x_2, x_3)) = x_3 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) ---------------------------------------- (12) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-1-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-1-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-1(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (13) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 59 less nodes. ---------------------------------------- (14) Complex Obligation (AND) ---------------------------------------- (15) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (16) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO]: POL(F.0-0-0(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(a.) = 1 POL(f.0-0-0(x_1, x_2, x_3)) = 0 POL(f.0-0-1(x_1, x_2, x_3)) = x_1 + x_2 POL(f.0-1-0(x_1, x_2, x_3)) = 0 POL(f.0-1-1(x_1, x_2, x_3)) = 1 + x_3 POL(f.1-0-0(x_1, x_2, x_3)) = 0 POL(f.1-0-1(x_1, x_2, x_3)) = 1 + x_3 POL(f.1-1-0(x_1, x_2, x_3)) = 0 POL(f.1-1-1(x_1, x_2, x_3)) = 0 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) ---------------------------------------- (17) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (18) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 7 less nodes. ---------------------------------------- (19) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (20) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO]: POL(F.0-0-0(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(a.) = 1 POL(f.0-0-0(x_1, x_2, x_3)) = 0 POL(f.0-0-1(x_1, x_2, x_3)) = x_1 + x_2 POL(f.0-1-0(x_1, x_2, x_3)) = 0 POL(f.0-1-1(x_1, x_2, x_3)) = 0 POL(f.1-0-0(x_1, x_2, x_3)) = 0 POL(f.1-0-1(x_1, x_2, x_3)) = 0 POL(f.1-1-0(x_1, x_2, x_3)) = 0 POL(f.1-1-1(x_1, x_2, x_3)) = x_3 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) ---------------------------------------- (21) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (22) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes. ---------------------------------------- (23) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (24) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2) F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO]: POL(F.0-0-0(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(a.) = 1 POL(f.0-0-0(x_1, x_2, x_3)) = 0 POL(f.0-0-1(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(f.0-1-0(x_1, x_2, x_3)) = 0 POL(f.0-1-1(x_1, x_2, x_3)) = 1 + x_1 + x_3 POL(f.1-0-0(x_1, x_2, x_3)) = 0 POL(f.1-0-1(x_1, x_2, x_3)) = 0 POL(f.1-1-0(x_1, x_2, x_3)) = 0 POL(f.1-1-1(x_1, x_2, x_3)) = 0 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) ---------------------------------------- (25) Obligation: Q DP problem: P is empty. The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (26) PisEmptyProof (EQUIVALENT) The TRS P is empty. Hence, there is no (P,Q,R) chain. ---------------------------------------- (27) YES ---------------------------------------- (28) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (29) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO]: POL(F.0-0-1(x_1, x_2, x_3)) = 1 + x_1 + x_2 POL(F.0-1-0(x_1, x_2, x_3)) = 1 + x_1 + x_3 POL(a.) = 1 POL(f.0-0-0(x_1, x_2, x_3)) = 0 POL(f.0-0-1(x_1, x_2, x_3)) = x_1 + x_2 POL(f.0-1-0(x_1, x_2, x_3)) = x_3 POL(f.0-1-1(x_1, x_2, x_3)) = x_3 POL(f.1-0-0(x_1, x_2, x_3)) = 0 POL(f.1-0-1(x_1, x_2, x_3)) = 0 POL(f.1-1-0(x_1, x_2, x_3)) = 0 POL(f.1-1-1(x_1, x_2, x_3)) = 0 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) ---------------------------------------- (30) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (31) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes. ---------------------------------------- (32) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (33) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO]: POL(F.0-0-1(x_1, x_2, x_3)) = 1 + x_2 POL(F.0-1-0(x_1, x_2, x_3)) = 1 + x_1 + x_3 POL(a.) = 1 POL(f.0-0-0(x_1, x_2, x_3)) = 0 POL(f.0-0-1(x_1, x_2, x_3)) = x_1 + x_2 POL(f.0-1-0(x_1, x_2, x_3)) = 0 POL(f.0-1-1(x_1, x_2, x_3)) = 0 POL(f.1-0-0(x_1, x_2, x_3)) = 0 POL(f.1-0-1(x_1, x_2, x_3)) = 0 POL(f.1-1-0(x_1, x_2, x_3)) = 0 POL(f.1-1-1(x_1, x_2, x_3)) = x_3 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) ---------------------------------------- (34) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (35) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (36) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (37) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) -> F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO]: POL(F.0-0-1(x_1, x_2, x_3)) = 1 + x_1 + x_2 POL(F.0-1-0(x_1, x_2, x_3)) = x_1 POL(a.) = 0 POL(f.0-0-0(x_1, x_2, x_3)) = 0 POL(f.0-0-1(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(f.0-1-0(x_1, x_2, x_3)) = 0 POL(f.0-1-1(x_1, x_2, x_3)) = 0 POL(f.1-0-0(x_1, x_2, x_3)) = 0 POL(f.1-0-1(x_1, x_2, x_3)) = x_2 POL(f.1-1-0(x_1, x_2, x_3)) = 0 POL(f.1-1-1(x_1, x_2, x_3)) = 0 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) ---------------------------------------- (38) Obligation: Q DP problem: The TRS P consists of the following rules: F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2) F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) -> F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2) The TRS R consists of the following rules: f.0-0-0(f.0-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-0-0(y, x, z)) f.0-0-1(f.0-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-0-0(y, x, z)) f.0-1-0(f.0-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-0-1(y, x, z)) f.0-1-1(f.0-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-0-1(y, x, z)) f.0-0-0(f.0-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-0-0(y, x, z)) f.0-0-1(f.0-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-0-0(y, x, z)) f.0-1-0(f.0-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-0-1(y, x, z)) f.0-1-1(f.0-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-0-1(y, x, z)) f.0-0-0(f.1-0-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.0-1-0(y, x, z)) f.0-0-1(f.1-0-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.0-1-0(y, x, z)) f.0-1-0(f.1-0-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.0-1-1(y, x, z)) f.0-1-1(f.1-0-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.0-1-1(y, x, z)) f.0-0-0(f.1-1-1(x, y, a.), z, w) -> f.0-0-0(z, w, f.1-1-0(y, x, z)) f.0-0-1(f.1-1-1(x, y, a.), z, w) -> f.0-1-0(z, w, f.1-1-0(y, x, z)) f.0-1-0(f.1-1-1(x, y, a.), z, w) -> f.1-0-0(z, w, f.1-1-1(y, x, z)) f.0-1-1(f.1-1-1(x, y, a.), z, w) -> f.1-1-0(z, w, f.1-1-1(y, x, z)) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (39) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes. ---------------------------------------- (40) TRUE