We consider the system 519. 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) We observe that the rules contain a first-order subset: not(true) => false not(false) => true Moreover, the system is orthogonal. 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 terminating when seen as a many-sorted first-order TRS. According to the external first-order termination prover, this system is indeed 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) RFCMatchBoundsTRSProof [EQUIVALENT] || (2) YES || || || ---------------------------------------- || || (0) || Obligation: || Q restricted rewrite system: || The TRS R consists of the following rules: || || not(true) -> false || not(false) -> true || || Q is empty. || || ---------------------------------------- || || (1) RFCMatchBoundsTRSProof (EQUIVALENT) || Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 0. This implies Q-termination of R. || The following rules were used to construct the certificate: || || not(true) -> false || not(false) -> true || || The certificate found is represented by the following graph. || The certificate consists of the following enumerated nodes: || 2, 3 || || Node 2 is start node and node 3 is final node. || || Those nodes are connected through the following edges: || || * 2 to 3 labelled false(0), true(0)* 3 to 3 labelled #_1(0) || || || ---------------------------------------- || || (2) || 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) 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). This combination (P_0, R_0) has no formative rules! We will name the empty set of rules:R_1. 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) 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_3, x_1, x_2) [[~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) 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 definition 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 (Star) 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], [46] and [50], 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 (F-Abs) 42] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), u) >= Y(u) because [43], by (Select) 43] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), u)) >= Y(u) because [44], by (Meta) 44] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), u) >= u because [45], by (Select) 45] u >= u by (Var) 46] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Y(Z) because [47], by (Select) 47] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= Y(Z) because [48], by (Meta) 48] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Z because [49], by (Select) 49] Z >= Z by (Meta) 50] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= U because [51], by (Select) 51] 1(U) >= U because [34], by (Star) 52] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > X(_|_) because [53], by definition 53] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= X(_|_) because [54], by (Select) 54] X(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= X(_|_) because [55], by (Meta) 55] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= _|_ by (Bot) 56] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Y(_|_) because [57], by (Star) 57] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Y(_|_) because [58], by (Select) 58] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= Y(_|_) because [59], by (Meta) 59] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= _|_ by (Bot) 60] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > Y(Z) because [46], by definition 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)) =#> X(z) fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) =#> Y(z) 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)) =#> Y(z) 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)) >? 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)) >? Y(~c2) 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_3, x_2) [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ 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)) >= 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)) > Y(_|_) With these choices, we have: 1] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(_|_) because [2], by (Star) 2] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(_|_) because [3], by (Select) 3] X(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= X(_|_) because [4], by (Meta) 4] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= _|_ by (Bot) 5] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Y(_|_) because [6], by (Star) 6] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Y(_|_) because [7], by (Select) 7] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= Y(_|_) because [8], by (Meta) 8] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= _|_ by (Bot) 9] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(Z) because [10], by (Star) 10] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(Z) because [11], by (Select) 11] X(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= X(Z) because [12], by (Meta) 12] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Z because [13], by (Select) 13] Z >= Z by (Meta) 14] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold#(/\x.X(x), /\y.Y(y), Y(Z), U) because [15], by (Star) 15] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold#(/\x.X(x), /\y.Y(y), Y(Z), U) because [16], [19], [24], [29] and [33], by (Stat) 16] 1(U) > U because [17], by definition 17] 1*(U) >= U because [18], by (Select) 18] U >= U by (Meta) 19] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.X(x) because [20], by (F-Abs) 20] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= X(z) because [21], by (Select) 21] X(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), z)) >= X(z) because [22], by (Meta) 22] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= z because [23], by (Select) 23] z >= z by (Var) 24] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.Y(x) because [25], by (F-Abs) 25] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), u) >= Y(u) because [26], by (Select) 26] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), u)) >= Y(u) because [27], by (Meta) 27] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U), u) >= u because [28], by (Select) 28] u >= u by (Var) 29] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Y(Z) because [30], by (Select) 30] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= Y(Z) because [31], by (Meta) 31] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Z because [32], by (Select) 32] Z >= Z by (Meta) 33] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= U because [34], by (Select) 34] 1(U) >= U because [17], by (Star) 35] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) > Y(_|_) because [36], by definition 36] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Y(_|_) because [37], by (Select) 37] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= Y(_|_) because [38], by (Meta) 38] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= _|_ by (Bot) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_1, minimal, formative) by (P_2, R_1, minimal, formative), where P_2 consists of: 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, 0(U)) =#> X(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_2, R_1, minimal, formative) is finite. We consider the dependency pair problem (P_2, 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)) >? 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) 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_3, x_2, x_1) [[~c0]] = _|_ [[~c1]] = _|_ 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)) >= 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) With these choices, we have: 1] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(_|_) because [2], by (Star) 2] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(_|_) because [3], by (Select) 3] X(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= X(_|_) because [4], by (Meta) 4] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= _|_ by (Bot) 5] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Y(_|_) because [6], by (Star) 6] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Y(_|_) because [7], by (Select) 7] Y(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= Y(_|_) because [8], by (Meta) 8] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= _|_ by (Bot) 9] fold#(/\x.X(x), /\y.Y(y), Z, 0(U)) > X(Z) because [10], by definition 10] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= X(Z) because [11], by (Select) 11] X(fold#*(/\x.X(x), /\y.Y(y), Z, 0(U))) >= X(Z) because [12], by (Meta) 12] fold#*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= Z because [13], by (Select) 13] Z >= Z by (Meta) 14] fold#(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold#(/\x.X(x), /\y.Y(y), Y(Z), U) because [15], by (Star) 15] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold#(/\x.X(x), /\y.Y(y), Y(Z), U) because [16], [19], [23], [27] and [31], by (Stat) 16] 1(U) > U because [17], by definition 17] 1*(U) >= U because [18], by (Select) 18] U >= U by (Meta) 19] fold#*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.X(x) because [20], by (Select) 20] /\y.X(y) >= /\y.X(y) because [21], by (Abs) 21] X(x) >= X(x) because [22], by (Meta) 22] x >= x by (Var) 23] fold#*(/\y.X(y), /\z.Y(z), Z, 1(U)) >= /\y.Y(y) because [24], by (Select) 24] /\z.Y(z) >= /\z.Y(z) because [25], by (Abs) 25] Y(y) >= Y(y) because [26], by (Meta) 26] y >= y by (Var) 27] fold#*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= Y(Z) because [28], by (Select) 28] Y(fold#*(/\z.X(z), /\u.Y(u), Z, 1(U))) >= Y(Z) because [29], by (Meta) 29] fold#*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= Z because [30], by (Select) 30] Z >= Z by (Meta) 31] fold#*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= U because [32], by (Select) 32] 1(U) >= U because [17], by (Star) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_1, minimal, formative) by (P_3, R_1, minimal, formative), where P_3 consists of: 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_3, R_1, minimal, formative) is finite. We consider the dependency pair problem (P_3, 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)) >? 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) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = \y0.3 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))]] = 6 + F0(0) + F1(0) > F0(0) = [[_x0(~c0)]] [[fold#(/\x._x0(x), /\y._x1(y), _x2, 0(_x3))]] = 6 + 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)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_3, 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.