We consider the system sdu.

  Alphabet:

    casea : [u * a -> a * b -> a] --> a 
    caseb : [u * a -> b * b -> b] --> b 
    caseu : [u * a -> u * b -> u] --> u 
    inl : [a] --> u 
    inr : [b] --> u 

  Rules:

    casea(inl(x), f, g) => f x 
    casea(inr(x), f, g) => g x 
    casea(x, /\y.f inl(y), /\z.f inr(z)) => f x 
    caseb(inl(x), f, g) => f x 
    caseb(inr(x), f, g) => g x 
    caseb(x, /\y.f inl(y), /\z.f inr(z)) => f x 
    caseu(inl(x), f, g) => f x 
    caseu(inr(x), f, g) => g x 
    caseu(x, /\y.f inl(y), /\z.f inr(z)) => f x 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    casea : [u * a -> a * b -> a] --> a 
    caseb : [u * a -> b * b -> b] --> b 
    caseu : [u * a -> u * b -> u] --> u 
    inl : [a] --> u 
    inr : [b] --> u 
    ~AP1 : [u -> a * u] --> a 
    ~AP2 : [u -> b * u] --> b 
    ~AP3 : [u -> u * u] --> u 

  Rules:

    casea(inl(X), F, G) => F X 
    casea(inr(X), F, G) => G X 
    casea(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))) => ~AP1(F, X) 
    caseb(inl(X), F, G) => F X 
    caseb(inr(X), F, G) => G X 
    caseb(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) => ~AP2(F, X) 
    caseu(inl(X), F, G) => F X 
    caseu(inr(X), F, G) => G X 
    caseu(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))) => ~AP3(F, X) 
    ~AP1(F, X) => F X 
    ~AP2(F, X) => F X 
    ~AP3(F, X) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  casea(inl(X), F, G) >? F X 
  casea(inr(X), F, G) >? G X 
  casea(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))) >? ~AP1(F, X) 
  caseb(inl(X), F, G) >? F X 
  caseb(inr(X), F, G) >? G X 
  caseb(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) >? ~AP2(F, X) 
  caseu(inl(X), F, G) >? F X 
  caseu(inr(X), F, G) >? G X 
  caseu(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))) >? ~AP3(F, X) 
  ~AP1(F, X) >? F X 
  ~AP2(F, X) >? F X 
  ~AP3(F, X) >? F X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

We choose Lex = {} and Mul = {@_{o -> o}, casea, caseb, caseu, inl, inr, ~AP1, ~AP2, ~AP3}, and the following precedence: caseb > inr > ~AP2 > ~AP1 > casea > caseu > inl > ~AP3 > @_{o -> o}

With these choices, we have:

  1] casea(inl(X), F, G) > @_{o -> o}(F, X)  because [2], by definition 
  2] casea*(inl(X), F, G) >= @_{o -> o}(F, X)  because casea > @_{o -> o}, [3] and [5], by (Copy) 
  3] casea*(inl(X), F, G) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] casea*(inl(X), F, G) >= X  because [6], by (Select) 
  6] inl(X) >= X  because [7], by (Star) 
  7] inl*(X) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

  9] casea(inr(X), F, G) >= @_{o -> o}(G, X)  because [10], by (Star) 
  10] casea*(inr(X), F, G) >= @_{o -> o}(G, X)  because casea > @_{o -> o}, [11] and [13], by (Copy) 
  11] casea*(inr(X), F, G) >= G  because [12], by (Select) 
  12] G >= G  by (Meta) 
  13] casea*(inr(X), F, G) >= X  because [14], by (Select) 
  14] inr(X) >= X  because [15], by (Star) 
  15] inr*(X) >= X  because [16], by (Select) 
  16] X >= X  by (Meta) 

  17] casea(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))) > ~AP1(F, X)  because [18], by definition 
  18] casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))) >= ~AP1(F, X)  because [19], by (Select) 
  19] ~AP1(F, inr(casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))))) >= ~AP1(F, X)  because [20], by (Star) 
  20] ~AP1*(F, inr(casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))))) >= ~AP1(F, X)  because [21], by (Select) 
  21] inr(casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y)))) >= ~AP1(F, X)  because [22], by (Star) 
  22] inr*(casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y)))) >= ~AP1(F, X)  because [23], by (Select) 
  23] casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))) >= ~AP1(F, X)  because [24], by (Select) 
  24] ~AP1(F, inl(casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))))) >= ~AP1(F, X)  because ~AP1 in Mul, [25] and [26], by (Fun) 
  25] F >= F  by (Meta) 
  26] inl(casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y)))) >= X  because [27], by (Star) 
  27] inl*(casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y)))) >= X  because [28], by (Select) 
  28] casea*(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))) >= X  because [29], by (Select) 
  29] X >= X  by (Meta) 

  30] caseb(inl(X), F, G) >= @_{o -> o}(F, X)  because [31], by (Star) 
  31] caseb*(inl(X), F, G) >= @_{o -> o}(F, X)  because caseb > @_{o -> o}, [32] and [34], by (Copy) 
  32] caseb*(inl(X), F, G) >= F  because [33], by (Select) 
  33] F >= F  by (Meta) 
  34] caseb*(inl(X), F, G) >= X  because [35], by (Select) 
  35] inl(X) >= X  because [36], by (Star) 
  36] inl*(X) >= X  because [37], by (Select) 
  37] X >= X  by (Meta) 

  38] caseb(inr(X), F, G) >= @_{o -> o}(G, X)  because [39], by (Star) 
  39] caseb*(inr(X), F, G) >= @_{o -> o}(G, X)  because caseb > @_{o -> o}, [40] and [42], by (Copy) 
  40] caseb*(inr(X), F, G) >= G  because [41], by (Select) 
  41] G >= G  by (Meta) 
  42] caseb*(inr(X), F, G) >= X  because [43], by (Select) 
  43] inr(X) >= X  because [44], by (Star) 
  44] inr*(X) >= X  because [45], by (Select) 
  45] X >= X  by (Meta) 

  46] caseb(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) >= ~AP2(F, X)  because [47], by (Star) 
  47] caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) >= ~AP2(F, X)  because [48], by (Select) 
  48] ~AP2(F, inl(caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))))) >= ~AP2(F, X)  because ~AP2 in Mul, [49] and [50], by (Fun) 
  49] F >= F  by (Meta) 
  50] inl(caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y)))) >= X  because [51], by (Star) 
  51] inl*(caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y)))) >= X  because [52], by (Select) 
  52] caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) >= X  because [53], by (Select) 
  53] X >= X  by (Meta) 

  54] caseu(inl(X), F, G) > @_{o -> o}(F, X)  because [55], by definition 
  55] caseu*(inl(X), F, G) >= @_{o -> o}(F, X)  because caseu > @_{o -> o}, [56] and [58], by (Copy) 
  56] caseu*(inl(X), F, G) >= F  because [57], by (Select) 
  57] F >= F  by (Meta) 
  58] caseu*(inl(X), F, G) >= X  because [59], by (Select) 
  59] inl(X) >= X  because [60], by (Star) 
  60] inl*(X) >= X  because [61], by (Select) 
  61] X >= X  by (Meta) 

  62] caseu(inr(X), F, G) > @_{o -> o}(G, X)  because [63], by definition 
  63] caseu*(inr(X), F, G) >= @_{o -> o}(G, X)  because caseu > @_{o -> o}, [64] and [66], by (Copy) 
  64] caseu*(inr(X), F, G) >= G  because [65], by (Select) 
  65] G >= G  by (Meta) 
  66] caseu*(inr(X), F, G) >= X  because [67], by (Select) 
  67] inr(X) >= X  because [68], by (Star) 
  68] inr*(X) >= X  because [69], by (Select) 
  69] X >= X  by (Meta) 

  70] caseu(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))) > ~AP3(F, X)  because [71], by definition 
  71] caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))) >= ~AP3(F, X)  because [72], by (Select) 
  72] ~AP3(F, inl(caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))))) >= ~AP3(F, X)  because ~AP3 in Mul, [73] and [74], by (Fun) 
  73] F >= F  by (Meta) 
  74] inl(caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y)))) >= X  because [75], by (Star) 
  75] inl*(caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y)))) >= X  because [76], by (Select) 
  76] caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))) >= X  because [77], by (Select) 
  77] ~AP3(F, inl(caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))))) >= X  because [78], by (Star) 
  78] ~AP3*(F, inl(caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))))) >= X  because [79], by (Select) 
  79] inl(caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y)))) >= X  because [80], by (Star) 
  80] inl*(caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y)))) >= X  because [81], by (Select) 
  81] caseu*(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))) >= X  because [82], by (Select) 
  82] X >= X  by (Meta) 

  83] ~AP1(F, X) >= @_{o -> o}(F, X)  because [84], by (Star) 
  84] ~AP1*(F, X) >= @_{o -> o}(F, X)  because ~AP1 > @_{o -> o}, [85] and [87], by (Copy) 
  85] ~AP1*(F, X) >= F  because [86], by (Select) 
  86] F >= F  by (Meta) 
  87] ~AP1*(F, X) >= X  because [88], by (Select) 
  88] X >= X  by (Meta) 

  89] ~AP2(F, X) > @_{o -> o}(F, X)  because [90], by definition 
  90] ~AP2*(F, X) >= @_{o -> o}(F, X)  because ~AP2 > @_{o -> o}, [91] and [93], by (Copy) 
  91] ~AP2*(F, X) >= F  because [92], by (Select) 
  92] F >= F  by (Meta) 
  93] ~AP2*(F, X) >= X  because [94], by (Select) 
  94] X >= X  by (Meta) 

  95] ~AP3(F, X) > @_{o -> o}(F, X)  because [96], by definition 
  96] ~AP3*(F, X) >= @_{o -> o}(F, X)  because ~AP3 > @_{o -> o}, [97] and [99], by (Copy) 
  97] ~AP3*(F, X) >= F  because [98], by (Select) 
  98] F >= F  by (Meta) 
  99] ~AP3*(F, X) >= X  because [100], by (Select) 
  100] X >= X  by (Meta) 

We can thus remove the following rules:

  casea(inl(X), F, G) => F X 
  casea(X, /\x.~AP1(F, inl(x)), /\y.~AP1(F, inr(y))) => ~AP1(F, X) 
  caseu(inl(X), F, G) => F X 
  caseu(inr(X), F, G) => G X 
  caseu(X, /\x.~AP3(F, inl(x)), /\y.~AP3(F, inr(y))) => ~AP3(F, X) 
  ~AP2(F, X) => F X 
  ~AP3(F, X) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  casea(inr(X), F, G) >? G X 
  caseb(inl(X), F, G) >? F X 
  caseb(inr(X), F, G) >? G X 
  caseb(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) >? ~AP2(F, X) 
  ~AP1(F, X) >? F X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

We choose Lex = {} and Mul = {@_{o -> o}, casea, caseb, inl, inr, ~AP1, ~AP2}, and the following precedence: casea > inl > ~AP2 > ~AP1 > caseb > @_{o -> o} > inr

With these choices, we have:

  1] casea(inr(X), F, G) >= @_{o -> o}(G, X)  because [2], by (Star) 
  2] casea*(inr(X), F, G) >= @_{o -> o}(G, X)  because casea > @_{o -> o}, [3] and [5], by (Copy) 
  3] casea*(inr(X), F, G) >= G  because [4], by (Select) 
  4] G >= G  by (Meta) 
  5] casea*(inr(X), F, G) >= X  because [6], by (Select) 
  6] inr(X) >= X  because [7], by (Star) 
  7] inr*(X) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

  9] caseb(inl(X), F, G) >= @_{o -> o}(F, X)  because [10], by (Star) 
  10] caseb*(inl(X), F, G) >= @_{o -> o}(F, X)  because caseb > @_{o -> o}, [11] and [13], by (Copy) 
  11] caseb*(inl(X), F, G) >= F  because [12], by (Select) 
  12] F >= F  by (Meta) 
  13] caseb*(inl(X), F, G) >= X  because [14], by (Select) 
  14] inl(X) >= X  because [15], by (Star) 
  15] inl*(X) >= X  because [16], by (Select) 
  16] X >= X  by (Meta) 

  17] caseb(inr(X), F, G) >= @_{o -> o}(G, X)  because [18], by (Star) 
  18] caseb*(inr(X), F, G) >= @_{o -> o}(G, X)  because caseb > @_{o -> o}, [19] and [21], by (Copy) 
  19] caseb*(inr(X), F, G) >= G  because [20], by (Select) 
  20] G >= G  by (Meta) 
  21] caseb*(inr(X), F, G) >= X  because [22], by (Select) 
  22] inr(X) >= X  because [23], by (Star) 
  23] inr*(X) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 

  25] caseb(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) > ~AP2(F, X)  because [26], by definition 
  26] caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) >= ~AP2(F, X)  because [27], by (Select) 
  27] ~AP2(F, inl(caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))))) >= ~AP2(F, X)  because [28], by (Star) 
  28] ~AP2*(F, inl(caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))))) >= ~AP2(F, X)  because ~AP2 in Mul, [29] and [30], by (Stat) 
  29] F >= F  by (Meta) 
  30] inl(caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y)))) > X  because [31], by definition 
  31] inl*(caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y)))) >= X  because [32], by (Select) 
  32] caseb*(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) >= X  because [33], by (Select) 
  33] X >= X  by (Meta) 

  34] ~AP1(F, X) >= @_{o -> o}(F, X)  because [35], by (Star) 
  35] ~AP1*(F, X) >= @_{o -> o}(F, X)  because ~AP1 > @_{o -> o}, [36] and [38], by (Copy) 
  36] ~AP1*(F, X) >= F  because [37], by (Select) 
  37] F >= F  by (Meta) 
  38] ~AP1*(F, X) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 

We can thus remove the following rules:

  caseb(X, /\x.~AP2(F, inl(x)), /\y.~AP2(F, inr(y))) => ~AP2(F, X) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  casea(inr(X), F, G) >? G X 
  caseb(inl(X), F, G) >? F X 
  caseb(inr(X), F, G) >? G X 
  ~AP1(F, X) >? F X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

We choose Lex = {} and Mul = {@_{o -> o}, casea, caseb, inl, inr, ~AP1}, and the following precedence: ~AP1 > inl > inr > caseb > casea > @_{o -> o}

With these choices, we have:

  1] casea(inr(X), F, G) > @_{o -> o}(G, X)  because [2], by definition 
  2] casea*(inr(X), F, G) >= @_{o -> o}(G, X)  because casea > @_{o -> o}, [3] and [5], by (Copy) 
  3] casea*(inr(X), F, G) >= G  because [4], by (Select) 
  4] G >= G  by (Meta) 
  5] casea*(inr(X), F, G) >= X  because [6], by (Select) 
  6] inr(X) >= X  because [7], by (Star) 
  7] inr*(X) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

  9] caseb(inl(X), F, G) >= @_{o -> o}(F, X)  because [10], by (Star) 
  10] caseb*(inl(X), F, G) >= @_{o -> o}(F, X)  because caseb > @_{o -> o}, [11] and [13], by (Copy) 
  11] caseb*(inl(X), F, G) >= F  because [12], by (Select) 
  12] F >= F  by (Meta) 
  13] caseb*(inl(X), F, G) >= X  because [14], by (Select) 
  14] inl(X) >= X  because [15], by (Star) 
  15] inl*(X) >= X  because [16], by (Select) 
  16] X >= X  by (Meta) 

  17] caseb(inr(X), F, G) >= @_{o -> o}(G, X)  because [18], by (Star) 
  18] caseb*(inr(X), F, G) >= @_{o -> o}(G, X)  because caseb > @_{o -> o}, [19] and [21], by (Copy) 
  19] caseb*(inr(X), F, G) >= G  because [20], by (Select) 
  20] G >= G  by (Meta) 
  21] caseb*(inr(X), F, G) >= X  because [22], by (Select) 
  22] inr(X) >= X  because [23], by (Star) 
  23] inr*(X) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 

  25] ~AP1(F, X) >= @_{o -> o}(F, X)  because [26], by (Star) 
  26] ~AP1*(F, X) >= @_{o -> o}(F, X)  because ~AP1 > @_{o -> o}, [27] and [29], by (Copy) 
  27] ~AP1*(F, X) >= F  because [28], by (Select) 
  28] F >= F  by (Meta) 
  29] ~AP1*(F, X) >= X  because [30], by (Select) 
  30] X >= X  by (Meta) 

We can thus remove the following rules:

  casea(inr(X), F, G) => G X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  caseb(inl(X), F, G) >? F X 
  caseb(inr(X), F, G) >? G X 
  ~AP1(F, X) >? F X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[inl(x_1)]] = x_1 

We choose Lex = {} and Mul = {@_{o -> o}, caseb, inr, ~AP1}, and the following precedence: caseb > ~AP1 > inr > @_{o -> o}

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  caseb(X, F, G) >= @_{o -> o}(F, X) 
  caseb(inr(X), F, G) >= @_{o -> o}(G, X) 
  ~AP1(F, X) > @_{o -> o}(F, X) 

With these choices, we have:

  1] caseb(X, F, G) >= @_{o -> o}(F, X)  because [2], by (Star) 
  2] caseb*(X, F, G) >= @_{o -> o}(F, X)  because caseb > @_{o -> o}, [3] and [5], by (Copy) 
  3] caseb*(X, F, G) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] caseb*(X, F, G) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] caseb(inr(X), F, G) >= @_{o -> o}(G, X)  because [8], by (Star) 
  8] caseb*(inr(X), F, G) >= @_{o -> o}(G, X)  because caseb > @_{o -> o}, [9] and [11], by (Copy) 
  9] caseb*(inr(X), F, G) >= G  because [10], by (Select) 
  10] G >= G  by (Meta) 
  11] caseb*(inr(X), F, G) >= X  because [12], by (Select) 
  12] inr(X) >= X  because [13], by (Star) 
  13] inr*(X) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 

  15] ~AP1(F, X) > @_{o -> o}(F, X)  because [16], by definition 
  16] ~AP1*(F, X) >= @_{o -> o}(F, X)  because ~AP1 > @_{o -> o}, [17] and [19], by (Copy) 
  17] ~AP1*(F, X) >= F  because [18], by (Select) 
  18] F >= F  by (Meta) 
  19] ~AP1*(F, X) >= X  because [20], by (Select) 
  20] X >= X  by (Meta) 

We can thus remove the following rules:

  ~AP1(F, X) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  caseb(inl(X), F, G) >? F X 
  caseb(inr(X), F, G) >? G X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[inl(x_1)]] = x_1 

We choose Lex = {} and Mul = {@_{o -> o}, caseb, inr}, and the following precedence: caseb > @_{o -> o} > inr

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  caseb(X, F, G) > @_{o -> o}(F, X) 
  caseb(inr(X), F, G) >= @_{o -> o}(G, X) 

With these choices, we have:

  1] caseb(X, F, G) > @_{o -> o}(F, X)  because [2], by definition 
  2] caseb*(X, F, G) >= @_{o -> o}(F, X)  because caseb > @_{o -> o}, [3] and [5], by (Copy) 
  3] caseb*(X, F, G) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] caseb*(X, F, G) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] caseb(inr(X), F, G) >= @_{o -> o}(G, X)  because [8], by (Star) 
  8] caseb*(inr(X), F, G) >= @_{o -> o}(G, X)  because caseb > @_{o -> o}, [9] and [11], by (Copy) 
  9] caseb*(inr(X), F, G) >= G  because [10], by (Select) 
  10] G >= G  by (Meta) 
  11] caseb*(inr(X), F, G) >= X  because [12], by (Select) 
  12] inr(X) >= X  because [13], by (Star) 
  13] inr*(X) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 

We can thus remove the following rules:

  caseb(inl(X), F, G) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  caseb(inr(X), F, G) >? G X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

We choose Lex = {} and Mul = {@_{o -> o}, caseb, inr}, and the following precedence: caseb > @_{o -> o} > inr

With these choices, we have:

  1] caseb(inr(X), F, G) > @_{o -> o}(G, X)  because [2], by definition 
  2] caseb*(inr(X), F, G) >= @_{o -> o}(G, X)  because caseb > @_{o -> o}, [3] and [5], by (Copy) 
  3] caseb*(inr(X), F, G) >= G  because [4], by (Select) 
  4] G >= G  by (Meta) 
  5] caseb*(inr(X), F, G) >= X  because [6], by (Select) 
  6] inr(X) >= X  because [7], by (Star) 
  7] inr*(X) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

We can thus remove the following rules:

  caseb(inr(X), F, G) => G X 

All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.


+++ Citations +++

[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.