Remark
==================================================================
Unfortunately, Cora cannot find a suitable ordering. This is due to the requirement 

g(y, recdown(g, x, y1, a)) ≻ g(y, f(recdown(g, x1, y1, a), x)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 ∧ y2 = y1 - 1

If we replace it by the more general requirement  

recdown(g, x, y1, a) ≻  f(recdown(g, x1, y1, a), x) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 ∧ y2 = y1 - 1

then Cora is able to find an ordering. 
==================================================================


We start the process with the following equations:

  E1: (• , recup(f, x, y, a) ≈ recdown(g, x, y, a) , •)

We apply INDUCT to E1, which causes recup(f, x, y, a) ≈ recdown(g, x, y, a) to be added to the set H of induction hypotheses.

This yields E2: (recup(f, x, y, a) , recup(f, x, y, a) ≈ recdown(g, x, y, a) , recdown(g, x, y, a))

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

  E3: (recup(f, x, y, a) , recup(f, x, y, a) ≈ recdown(g, x, y, a) | x ≤ y , recdown(g, x, y, a))
  E4: (recup(f, x, y, a) , recup(f, x, y, a) ≈ recdown(g, x, y, a) | ¬(x ≤ y) , recdown(g, x, y, a))

We apply SIMPLIFICATION to E4 with rule R5 and substitution [F := f, i := x, y := y, z := a].

This yields E5: (recup(f, x, y, a) , a ≈ recdown(g, x, y, a) | ¬(x ≤ y) , recdown(g, x, y, a))

We apply SIMPLIFICATION to E5 with rule R7 and substitution [F := g, i := y, x := x, z := a].

This yields E6: (recup(f, x, y, a) , a ≈ a | ¬(x ≤ y) , recdown(g, x, y, a))

We apply DELETION to E6 because both sides are equal.  Thus, we may remove this equation from the proof state.

We apply SIMPLIFICATION to E3 with rule R6 and substitution [F := f, i := x, y := y, z := a].

This yields E7: (recup(f, x, y, a) , f(recup(f, x + 1, y, a), x) ≈ recdown(g, x, y, a) | x ≤ y , recdown(g, x, y, a))

We use ALTER to add x1 = x + 1 to the constraint, and then use CALC at position l1.2.

This yields E8: (recup(f, x, y, a) , f(recup(f, x1, y, a), x) ≈ recdown(g, x, y, a) | x ≤ y ∧ x1 = x + 1 , recdown(g, x, y, a))

We apply SIMPLIFICATION to E8 with rule R8 and substitution [F := g, i := y, x := x, z := a].

This yields E9: (recup(f, x, y, a) , f(recup(f, x1, y, a), x) ≈ g(y, recdown(g, x, y - 1, a)) | x ≤ y ∧ x1 = x + 1 , recdown(g, x, y, a))

We use ALTER to add y1 = y - 1 to the constraint, and then use CALC at position r2.3.

This yields E10: (recup(f, x, y, a) , f(recup(f, x1, y, a), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , recdown(g, x, y, a))

We apply HYPOTHESIS to E10 with induction hypothesis H1 and substitution [a := a, x := x1, y := y].  To this end, we impose the requirement that recup(f, x, y, a) ≻ f(recdown(g, x1, y, a), x) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1.

This yields E11: (recup(f, x, y, a) , f(recdown(g, x1, y, a), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , recdown(g, x, y, a))

We apply INDUCT to E11, which causes f(recdown(g, x1, y, a), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 to be added to the set H of induction hypotheses.

This yields E12: (f(recdown(g, x1, y, a), x) , f(recdown(g, x1, y, a), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , g(y, recdown(g, x, y1, a)))

We apply CASE on the constraint y ≥ x1.

This yields the following new equations:

  E13: (f(recdown(g, x1, y, a), x) , f(recdown(g, x1, y, a), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 , g(y, recdown(g, x, y1, a)))
  E14: (f(recdown(g, x1, y, a), x) , f(recdown(g, x1, y, a), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(y ≥ x1) , g(y, recdown(g, x, y1, a)))

We apply SIMPLIFICATION to E14 with rule R7 and substitution [F := g, i := y, x := x1, z := a].

This yields E15: (f(recdown(g, x1, y, a), x) , f(a, x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(y ≥ x1) , g(y, recdown(g, x, y1, a)))

We apply SIMPLIFICATION to E15 with rule R7 and substitution [F := g, i := y1, x := x, z := a].

This yields E16: (f(recdown(g, x1, y, a), x) , f(a, x) ≈ g(y, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(y ≥ x1) , g(y, recdown(g, x, y1, a)))

We apply SKIP, which does not change the existing equations, but does allow us to focus on a different one.

We apply SIMPLIFICATION to E13 with rule R8 and substitution [F := g, i := y, x := x1, z := a].

This yields E17: (f(recdown(g, x1, y, a), x) , f(g(y, recdown(g, x1, y - 1, a)), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 , g(y, recdown(g, x, y1, a)))

We use CALC at position l1.2.3.

This yields E18: (f(recdown(g, x1, y, a), x) , f(g(y, recdown(g, x1, y1, a)), x) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 , g(y, recdown(g, x, y1, a)))

We apply SIMPLIFICATION to E18 with rule R8 and substitution [F := g, i := y1, x := x, z := a].

This yields E19: (f(recdown(g, x1, y, a), x) , f(g(y, recdown(g, x1, y1, a)), x) ≈ g(y, g(y1, recdown(g, x, y1 - 1, a))) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 , g(y, recdown(g, x, y1, a)))

We use ALTER to add y2 = y1 - 1 to the constraint, and then use CALC at position r2.2.3.

This yields E20: (f(recdown(g, x1, y, a), x) , f(g(y, recdown(g, x1, y1, a)), x) ≈ g(y, g(y1, recdown(g, x, y2, a))) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 ∧ y2 = y1 - 1 , g(y, recdown(g, x, y1, a)))

We apply HYPOTHESIS to E20 with induction hypothesis H11^{-1} and substitution [a := a, x := x, x1 := x1, y := y1, y1 := y2].  To this end, we impose the requirement that g(y, recdown(g, x, y1, a)) ≻ g(y, f(recdown(g, x1, y1, a), x)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 ∧ y2 = y1 - 1.

This yields E21: (f(recdown(g, x1, y, a), x) , f(g(y, recdown(g, x1, y1, a)), x) ≈ g(y, f(recdown(g, x1, y1, a), x)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 ∧ y2 = y1 - 1 , g(y, recdown(g, x, y1, a)))

We apply GENERALISE to replace the equation context E21 by E22: (f(g(y, z), x) , f(g(y, z), x) ≈ g(y, f(z, x)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 ∧ y2 = y1 - 1 , g(y, f(z, x))).

This yields E22: (f(g(y, z), x) , f(g(y, z), x) ≈ g(y, f(z, x)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ y ≥ x1 ∧ y2 = y1 - 1 , g(y, f(z, x)))