We consider the system 520. Alphabet: 0 : [string] --> string 1 : [string] --> string false : [] --> bool fold : [bool -> bool * bool -> bool * bool * string] --> bool nil : [] --> string not : [bool] --> bool true : [] --> bool Rules: not(true) => false not(false) => true fold(/\x.X(x), /\y.Y(y), Z, nil) => Z fold(/\x.X(x), /\y.Y(y), Z, 0(U)) => fold(/\z.X(z), /\u.Y(u), X(Z), U) fold(/\x.X(x), /\y.Y(y), Z, 1(U)) => fold(/\z.X(z), /\u.Y(u), Y(Z), U) 0(1(X)) => 1(0(X)) We observe that the rules contain a first-order subset: not(true) => false not(false) => true 0(1(X)) => 1(0(X)) Moreover, the system is finitely branching. Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS. According to the external first-order termination prover, this system is indeed Ce-terminating: || proof of resources/system.trs || # AProVE Commit ID: d84c10301d352dfd14de2104819581f4682260f5 fuhs 20130616 || || || Termination w.r.t. Q of the given QTRS could be proven: || || (0) QTRS || (1) QTRSRRRProof [EQUIVALENT] || (2) QTRS || (3) RisEmptyProof [EQUIVALENT] || (4) YES || || || ---------------------------------------- || || (0) || Obligation: || Q restricted rewrite system: || The TRS R consists of the following rules: || || not(true) -> false || not(false) -> true || 0(1(%X)) -> 1(0(%X)) || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || Q is empty. || || ---------------------------------------- || || (1) QTRSRRRProof (EQUIVALENT) || Used ordering: || Polynomial interpretation [POLO]: || || POL(0(x_1)) = 2 + 2*x_1 || POL(1(x_1)) = 1 + x_1 || POL(false) = 2 || POL(not(x_1)) = 2 + 2*x_1 || POL(true) = 1 || POL(~PAIR(x_1, x_2)) = 2 + x_1 + x_2 || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: || || not(true) -> false || not(false) -> true || 0(1(%X)) -> 1(0(%X)) || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || || || || ---------------------------------------- || || (2) || Obligation: || Q restricted rewrite system: || R is empty. || Q is empty. || || ---------------------------------------- || || (3) RisEmptyProof (EQUIVALENT) || The TRS R is empty. Hence, termination is trivially proven. || ---------------------------------------- || || (4) || YES || We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs. We thus obtain the following dependency pair problem (P_0, R_0, minimal, formative): Dependency Pairs P_0: 0] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> fold#(/\z.X(z), /\u.Y(u), X(Z), U) 1] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> X(z) 2] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> Y(z) 3] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> X(Z) 4] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) =#> fold#(/\z.X(z), /\u.Y(u), Y(Z), U) 5] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) =#> X(z) 6] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) =#> Y(z) 7] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) =#> Y(Z) Rules R_0: not(true) => false not(false) => true fold(/\x.X(x), /\y.Y(y), Z, nil) => Z fold(/\x.X(x), /\y.Y(y), Z, 0(U)) => fold(/\z.X(z), /\u.Y(u), X(Z), U) fold(/\x.X(x), /\y.Y(y), Z, 1(U)) => fold(/\z.X(z), /\u.Y(u), Y(Z), U) 0(1(X)) => 1(0(X)) Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_0, R_0, minimal, formative). The formative rules of (P_0, R_0) are R_1 ::= 0(1(X)) => 1(0(X)) By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_0, R_0, minimal, formative) by (P_0, R_1, minimal, formative). Thus, the original system is terminating if (P_0, R_1, minimal, formative) is finite. We consider the dependency pair problem (P_0, R_1, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >? fold#(/\z.X(z), /\u.Y(u), X(Z), U) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >? X(~c0) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >? Y(~c1) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >? X(Z) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >? fold#(/\z.X(z), /\u.Y(u), Y(Z), U) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >? X(~c2) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >? Y(~c3) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >? Y(Z) 0(1(X)) >= 1(0(X)) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[fold#(x_1, x_2, x_3, x_4)]] = fold#(x_4, x_1, x_2, x_3) [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ [[~c3]] = _|_ We choose Lex = {fold#} and Mul = {0, 1}, and the following precedence: 0 > 1 > fold# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= fold#(/\x.X(x), /\y.Y(y), X(Z), U) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(_|_) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Y(_|_) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) > X(Z) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold#(/\x.X(x), /\y.Y(y), Y(Z), U) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > X(_|_) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > Y(_|_) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > Y(Z) 0(1(X)) >= 1(0(X)) With these choices, we have: 1] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= fold#(/\x.X(x), /\y.Y(y), X(Z), U) because [2], by (Star) 2] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= fold#(/\x.X(x), /\y.Y(y), X(Z), U) because [3], [6], [11], [16] and [20], by (Stat) 3] 0(U) > U because [4], by definition 4] 0*(U) >= U because [5], by (Select) 5] U >= U by (Meta) 6] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= /\x.X(x) because [7], by (F-Abs) 7] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U), z) >= X(z) because [8], by (Select) 8] X(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U), z)) >= X(z) because [9], by (Meta) 9] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U), z) >= z because [10], by (Select) 10] z >= z by (Var) 11] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= /\x.Y(x) because [12], by (F-Abs) 12] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U), u) >= Y(u) because [13], by (Select) 13] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U), u)) >= Y(u) because [14], by (Meta) 14] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U), u) >= u because [15], by (Select) 15] u >= u by (Var) 16] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(Z) because [17], by (Select) 17] X(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= X(Z) because [18], by (Meta) 18] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Z because [19], by (Select) 19] Z >= Z by (Meta) 20] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= U because [21], by (Select) 21] 0(U) >= U because [4], by (Star) 22] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(_|_) because [23], by (Star) 23] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(_|_) because [24], by (Select) 24] X(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= X(_|_) because [25], by (Meta) 25] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= _|_ by (Bot) 26] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Y(_|_) because [27], by (Star) 27] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Y(_|_) because [28], by (Select) 28] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= Y(_|_) because [29], by (Meta) 29] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= _|_ by (Bot) 30] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) > X(Z) because [16], by definition 31] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold#(/\x.X(x), /\y.Y(y), Y(Z), U) because [32], by (Star) 32] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold#(/\x.X(x), /\y.Y(y), Y(Z), U) because [33], [36], [41], [45] and [49], by (Stat) 33] 1(U) > U because [34], by definition 34] 1*(U) >= U because [35], by (Select) 35] U >= U by (Meta) 36] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.X(x) because [37], by (F-Abs) 37] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= X(z) because [38], by (Select) 38] X(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), z)) >= X(z) because [39], by (Meta) 39] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= z because [40], by (Select) 40] z >= z by (Var) 41] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.Y(x) because [42], by (Select) 42] /\y.Y(y) >= /\y.Y(y) because [43], by (Abs) 43] Y(x) >= Y(x) because [44], by (Meta) 44] x >= x by (Var) 45] fold#*(/\y.X(y), /\u.Y(u), Z, 1(U)) >= Y(Z) because [46], by (Select) 46] Y(fold#*(/\y.X(y), /\u.Y(u), Z, 1(U))) >= Y(Z) because [47], by (Meta) 47] fold#*(/\y.X(y), /\u.Y(u), Z, 1(U)) >= Z because [48], by (Select) 48] Z >= Z by (Meta) 49] fold#*(/\y.X(y), /\u.Y(u), Z, 1(U)) >= U because [50], by (Select) 50] 1(U) >= U because [34], by (Star) 51] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > X(_|_) because [52], by definition 52] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= X(_|_) because [53], by (Select) 53] X(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= X(_|_) because [54], by (Meta) 54] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= _|_ by (Bot) 55] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > Y(_|_) because [56], by definition 56] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Y(_|_) because [57], by (Select) 57] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= Y(_|_) because [58], by (Meta) 58] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= _|_ by (Bot) 59] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > Y(Z) because [45], by definition 60] 0(1(X)) >= 1(0(X)) because [61], by (Star) 61] 0*(1(X)) >= 1(0(X)) because 0 > 1 and [62], by (Copy) 62] 0*(1(X)) >= 0(X) because 0 in Mul and [63], by (Stat) 63] 1(X) > X because [64], by definition 64] 1*(X) >= X because [65], by (Select) 65] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_1, minimal, formative) by (P_1, R_1, minimal, formative), where P_1 consists of: fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> fold#(/\z.X(z), /\u.Y(u), X(Z), U) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> X(z) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> Y(z) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) =#> fold#(/\z.X(z), /\u.Y(u), Y(Z), U) Thus, the original system is terminating if (P_1, R_1, minimal, formative) is finite. We consider the dependency pair problem (P_1, R_1, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >? fold#(/\z.X(z), /\u.Y(u), X(Z), U) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >? X(~c0) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >? Y(~c1) fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >? fold#(/\z.X(z), /\u.Y(u), Y(Z), U) 0(1(X)) >= 1(0(X)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = \y0.2 + 3y0 1 = \y0.3 + 2y0 fold# = \G0G1y2y3.3 + y3 + G0(0) + G1(0) ~c0 = 0 ~c1 = 0 Using this interpretation, the requirements translate to: [[fold#(/\x._x0(x), /\y._x1(y), _x2, 0(_x3))]] = 5 + 3x3 + F0(0) + F1(0) > 3 + x3 + F0(0) + F1(0) = [[fold#(/\x._x0(x), /\y._x1(y), _x0(_x2), _x3)]] [[fold#(/\x._x0(x), /\y._x1(y), _x2, 0(_x3))]] = 5 + 3x3 + F0(0) + F1(0) > F0(0) = [[_x0(~c0)]] [[fold#(/\x._x0(x), /\y._x1(y), _x2, 0(_x3))]] = 5 + 3x3 + F0(0) + F1(0) > F1(0) = [[_x1(~c1)]] [[fold#(/\x._x0(x), /\y._x1(y), _x2, 1(_x3))]] = 6 + 2x3 + F0(0) + F1(0) > 3 + x3 + F0(0) + F1(0) = [[fold#(/\x._x0(x), /\y._x1(y), _x1(_x2), _x3)]] [[0(1(_x0))]] = 11 + 6x0 >= 7 + 6x0 = [[1(0(_x0))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_1, R_1) by ({}, R_1). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.