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

y * recdown([*], x, y1, a) ≻ y * (x * recdown([*], x1, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1

If we replace it by the more general requirement 

recdown([*], x, y1, a) ≻ x * recdown([*], x1, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1

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


Remark 2
==================================================================
The proof uses the following lemma 

recup(helper, x, y - 1, y) [=] recup(helper, x, y, 1) | x <= y

which does not follow from an existing lemma generation technique.

However, considering the conceptual structure of recup and that
helper is actually (reverse) multiplication: we have a neutral element 
1 (i.e. helper(1, x) = helper(x, 1)=x for all x), so this is a reasonable
lemma to suggest. 

For example, by similar reasoning we could propose a lemma 
recup([+], x, y - 1, y) [=] recup([+], x, y, 0) | x <= y
in a + related example. 
==================================================================


We start the process with the following equations:

  E1: (• , factRU(x) ≈ factRD(x) | x ≥ 1 , •)

We apply POSTULATE to add the lemma equation U(i, x) ≈ recup(helper, i, x - 1, x) to the current proof state.

This yields E2: (• , U(i, x) ≈ recup(helper, i, x - 1, x) , •)

We use CALC at the only position where it is possible.

This yields E3: (• , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 , •)

We apply INDUCT to E3, which causes U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 to be added to the set H of induction hypotheses.

This yields E4: (U(i, x) , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 , recup(helper, i, x1, x))

We apply CASE on the constraint i > x - 1.

This yields the following new equations:

  E5: (U(i, x) , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ i > x - 1 , recup(helper, i, x1, x))
  E6: (U(i, x) , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ ¬(i > x - 1) , recup(helper, i, x1, x))

We apply SIMPLIFICATION to E6 with rule R3 and substitution [i := i, x := x].

This yields E7: (U(i, x) , i * U(i + 1, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ ¬(i > x - 1) , recup(helper, i, x1, x))

We use ALTER to add i1 = i + 1 to the constraint, and then use CALC at position l2.1.

This yields E8: (U(i, x) , i * U(i1, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ ¬(i > x - 1) ∧ i1 = i + 1 , recup(helper, i, x1, x))

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

This yields E9: (U(i, x) , i * U(i1, x) ≈ helper(recup(helper, i + 1, x1, x), i) | x1 = x - 1 ∧ ¬(i > x - 1) ∧ i1 = i + 1 , recup(helper, i, x1, x))

We use CALC at position r1.2.

This yields E10: (U(i, x) , i * U(i1, x) ≈ helper(recup(helper, i1, x1, x), i) | x1 = x - 1 ∧ ¬(i > x - 1) ∧ i1 = i + 1 , recup(helper, i, x1, x))

We apply SIMPLIFICATION to E10 with rule R10 and substitution [x := recup(helper, i1, x1, x), y := i].

This yields E11: (U(i, x) , i * U(i1, x) ≈ i * recup(helper, i1, x1, x) | x1 = x - 1 ∧ ¬(i > x - 1) ∧ i1 = i + 1 , recup(helper, i, x1, x))

We apply HDELETE to E11 with induction hypothesis H3 and substitution [i := i1, x := x, x1 := x1].

We apply SIMPLIFICATION to E5 with rule R2 and substitution [i := i, x := x].

This yields E12: (U(i, x) , x ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ i > x - 1 , recup(helper, i, x1, x))

We apply SIMPLIFICATION to E12 with rule R6 and substitution [F := helper, a := x, i := i, y := x1].

This yields E13: (U(i, x) , x ≈ x | x1 = x - 1 ∧ i > x - 1 , recup(helper, i, x1, x))

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

We apply POSTULATE to add the lemma equation factRD(x) ≈ recdown([*], 2, x, 1) to the current proof state.

This yields E14: (• , factRD(x) ≈ recdown([*], 2, x, 1) , •)

We apply INDUCT to E14, which causes factRD(x) ≈ recdown([*], 2, x, 1) to be added to the set H of induction hypotheses.

This yields E15: (factRD(x) , factRD(x) ≈ recdown([*], 2, x, 1) , recdown([*], 2, x, 1))

We apply CASE on the constraint x > 1.

This yields the following new equations:

  E16: (factRD(x) , factRD(x) ≈ recdown([*], 2, x, 1) | x > 1 , recdown([*], 2, x, 1))
  E17: (factRD(x) , factRD(x) ≈ recdown([*], 2, x, 1) | ¬(x > 1) , recdown([*], 2, x, 1))

We apply SIMPLIFICATION to E17 with rule R4 and substitution [x := x].

This yields E18: (factRD(x) , 1 ≈ recdown([*], 2, x, 1) | ¬(x > 1) , recdown([*], 2, x, 1))

We apply SIMPLIFICATION to E18 with rule R8 and substitution [F := [*], a := 1, i := x, x := 2].

This yields E19: (factRD(x) , 1 ≈ 1 | ¬(x > 1) , recdown([*], 2, x, 1))

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

We apply SIMPLIFICATION to E16 with rule R5 and substitution [x := x].

This yields E20: (factRD(x) , x * factRD(x - 1) ≈ recdown([*], 2, x, 1) | x > 1 , recdown([*], 2, x, 1))

We use ALTER to add x1 = x - 1 to the constraint, and then use CALC at position l2.1.

This yields E21: (factRD(x) , x * factRD(x1) ≈ recdown([*], 2, x, 1) | x > 1 ∧ x1 = x - 1 , recdown([*], 2, x, 1))

We apply SIMPLIFICATION to E21 with rule R9 and substitution [F := [*], a := 1, i := x, x := 2].

This yields E22: (factRD(x) , x * factRD(x1) ≈ x * recdown([*], 2, x - 1, 1) | x > 1 ∧ x1 = x - 1 , recdown([*], 2, x, 1))

We use CALC at position r2.3.

This yields E23: (factRD(x) , x * factRD(x1) ≈ x * recdown([*], 2, x1, 1) | x > 1 ∧ x1 = x - 1 , recdown([*], 2, x, 1))

We apply HDELETE to E23 with induction hypothesis H14 and substitution [x := x1].

We apply POSTULATE to add the lemma equation recup(helper, x, y, a) ≈ recdown([*], x, y, a) to the current proof state.

This yields E24: (• , recup(helper, x, y, a) ≈ recdown([*], x, y, a) , •)

We apply INDUCT to E24, which causes recup(helper, x, y, a) ≈ recdown([*], x, y, a) to be added to the set H of induction hypotheses.

This yields E25: (recup(helper, x, y, a) , recup(helper, x, y, a) ≈ recdown([*], x, y, a) , recdown([*], x, y, a))

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

  E26: (recup(helper, x, y, a) , recup(helper, x, y, a) ≈ recdown([*], x, y, a) | x ≤ y , recdown([*], x, y, a))
  E27: (recup(helper, x, y, a) , recup(helper, x, y, a) ≈ recdown([*], x, y, a) | ¬(x ≤ y) , recdown([*], x, y, a))

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

This yields E28: (recup(helper, x, y, a) , a ≈ recdown([*], x, y, a) | ¬(x ≤ y) , recdown([*], x, y, a))

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

This yields E29: (recup(helper, x, y, a) , a ≈ a | ¬(x ≤ y) , recdown([*], x, y, a))

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

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

This yields E30: (recup(helper, x, y, a) , helper(recup(helper, x + 1, y, a), x) ≈ recdown([*], x, y, a) | x ≤ y , recdown([*], x, y, a))

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

This yields E31: (recup(helper, x, y, a) , helper(recup(helper, x1, y, a), x) ≈ recdown([*], x, y, a) | x ≤ y ∧ x1 = x + 1 , recdown([*], x, y, a))

We apply SIMPLIFICATION to E31 with rule R10 and substitution [x := recup(helper, x1, y, a), y := x].

This yields E32: (recup(helper, x, y, a) , x * recup(helper, x1, y, a) ≈ recdown([*], x, y, a) | x ≤ y ∧ x1 = x + 1 , recdown([*], x, y, a))

We apply SIMPLIFICATION to E32 with rule R9 and substitution [F := [*], a := a, i := y, x := x].

This yields E33: (recup(helper, x, y, a) , x * recup(helper, x1, y, a) ≈ y * recdown([*], x, y - 1, a) | x ≤ y ∧ x1 = x + 1 , recdown([*], x, y, a))

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

This yields E34: (recup(helper, x, y, a) , x * recup(helper, x1, y, a) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , recdown([*], x, y, a))

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

This yields E35: (recup(helper, x, y, a) , x * recdown([*], x1, y, a) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , recdown([*], x, y, a))

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

This yields E36: (x * recdown([*], x1, y, a) , x * recdown([*], x1, y, a) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , y * recdown([*], x, y1, a))

We apply CASE on the constraint x1 ≤ y.

This yields the following new equations:

  E37: (x * recdown([*], x1, y, a) , x * recdown([*], x1, y, a) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , y * recdown([*], x, y1, a))
  E38: (x * recdown([*], x1, y, a) , x * recdown([*], x1, y, a) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , y * recdown([*], x, y1, a))

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

This yields E39: (x * recdown([*], x1, y, a) , x * a ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , y * recdown([*], x, y1, a))

We use ALTER to add i1 = x * a to the constraint, and then use CALC at position l.

This yields E40: (x * recdown([*], x1, y, a) , i1 ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) ∧ i1 = x * a , y * recdown([*], x, y1, a))

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

This yields E41: (x * recdown([*], x1, y, a) , i1 ≈ y * a | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) ∧ i1 = x * a , y * recdown([*], x, y1, a))

We use ALTER to add i2 = y * a to the constraint, and then use CALC at position r.

This yields E42: (x * recdown([*], x1, y, a) , i1 ≈ i2 | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) ∧ i1 = x * a ∧ i2 = y * a , y * recdown([*], x, y1, a))

We observe that x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) ∧ i1 = x * a ∧ i2 = y * a ⊨ i1 = i2, and may therefore apply EQ-DELETION to remove E42 from the proof state.

We apply SIMPLIFICATION to E37 with rule R9 and substitution [F := [*], a := a, i := y, x := x1].

This yields E43: (x * recdown([*], x1, y, a) , x * (y * recdown([*], x1, y - 1, a)) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , y * recdown([*], x, y1, a))

We use CALC at position l2.2.3.

This yields E44: (x * recdown([*], x1, y, a) , x * (y * recdown([*], x1, y1, a)) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , y * recdown([*], x, y1, a))

We apply SIMPLIFICATION to E44 with rule R9 and substitution [F := [*], a := a, i := y1, x := x].

This yields E45: (x * recdown([*], x1, y, a) , x * (y * recdown([*], x1, y1, a)) ≈ y * (y1 * recdown([*], x, y1 - 1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , y * recdown([*], 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 E46: (x * recdown([*], x1, y, a) , x * (y * recdown([*], x1, y1, a)) ≈ y * (y1 * recdown([*], x, y2, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1 , y * recdown([*], x, y1, a))

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

This yields E47: (x * recdown([*], x1, y, a) , x * (y * recdown([*], x1, y1, a)) ≈ y * (x * recdown([*], x1, y1, a)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1 , y * recdown([*], x, y1, a))

We apply POSTULATE to add the lemma equation x * (y * z) ≈ y * (x * z) to the current proof state.

This yields E48: (• , x * (y * z) ≈ y * (x * z) , •)

We apply INDUCT to E48, which causes x * (y * z) ≈ y * (x * z) to be added to the set H of induction hypotheses.

This yields E49: (x * (y * z) , x * (y * z) ≈ y * (x * z) , y * (x * z))

We use ALTER to add i1 = y * z to the constraint, and then use CALC at position l2.

This yields E50: (x * (y * z) , x * i1 ≈ y * (x * z) | i1 = y * z , y * (x * z))

We use ALTER to add i2 = x * i1 to the constraint, and then use CALC at position l.

This yields E51: (x * (y * z) , i2 ≈ y * (x * z) | i1 = y * z ∧ i2 = x * i1 , y * (x * z))

We use ALTER to add i3 = x * z to the constraint, and then use CALC at position r2.

This yields E52: (x * (y * z) , i2 ≈ y * i3 | i1 = y * z ∧ i2 = x * i1 ∧ i3 = x * z , y * (x * z))

We use ALTER to add i4 = y * i3 to the constraint, and then use CALC at position r.

This yields E53: (x * (y * z) , i2 ≈ i4 | i1 = y * z ∧ i2 = x * i1 ∧ i3 = x * z ∧ i4 = y * i3 , y * (x * z))

We observe that i1 = y * z ∧ i2 = x * i1 ∧ i3 = x * z ∧ i4 = y * i3 ⊨ i2 = i4, and may therefore apply EQ-DELETION to remove E53 from the proof state.

We apply HDELETE to E47 with induction hypothesis H48 and substitution [x := x, y := y, z := recdown([*], x1, y1, a)].

We apply INDUCT to E1, which causes factRU(x) ≈ factRD(x) | x ≥ 1 to be added to the set H of induction hypotheses.

This yields E54: (factRU(x) , factRU(x) ≈ factRD(x) | x ≥ 1 , factRD(x))

We apply SIMPLIFICATION to E54 with rule R1 and substitution [x := x].

This yields E55: (factRU(x) , U(1, x) ≈ factRD(x) | x ≥ 1 , factRD(x))

We apply ALTER to add x1 = x - 1 to the constraint of E55.

This yields E56: (factRU(x) , U(1, x) ≈ factRD(x) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We apply HYPOTHESIS to E56 with induction hypothesis H3 and substitution [i := 1, x := x, x1 := x1].  To this end, we impose the requirement that factRU(x) ≻ recup(helper, 1, x1, x) | x ≥ 1 ∧ x1 = x - 1.

This yields E57: (factRU(x) , recup(helper, 1, x1, x) ≈ factRD(x) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We apply HYPOTHESIS to E57 with induction hypothesis H14 and substitution [x := x].  To this end, we impose the requirements that factRD(x) ≻ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 and factRU(x) ≻ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1.

This yields E58: (factRU(x) , recup(helper, 1, x1, x) ≈ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We apply POSTULATE to add the lemma equation recup(helper, x, y - 1, y) ≈ recup(helper, x, y, 1) | x ≤ y to the current proof state.

This yields E59: (• , recup(helper, x, y - 1, y) ≈ recup(helper, x, y, 1) | x ≤ y , •)

We use CALC at the only position where it is possible.

This yields E60: (• , recup(helper, x, y1, y) ≈ recup(helper, x, y, 1) | x ≤ y ∧ y1 = y - 1 , •)

We apply INDUCT to E60, which causes recup(helper, x, y1, y) ≈ recup(helper, x, y, 1) | x ≤ y ∧ y1 = y - 1 to be added to the set H of induction hypotheses.

This yields E61: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ recup(helper, x, y, 1) | x ≤ y ∧ y1 = y - 1 , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E61 with rule R7 and substitution [F := helper, a := 1, i := x, y := y].

This yields E62: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ helper(recup(helper, x + 1, y, 1), x) | x ≤ y ∧ y1 = y - 1 , recup(helper, x, y, 1))

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

This yields E63: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ helper(recup(helper, x1, y, 1), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E63 with rule R10 and substitution [x := recup(helper, x1, y, 1), y := x].

This yields E64: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 , recup(helper, x, y, 1))

We apply CASE on the constraint x ≤ y1.

This yields the following new equations:

  E65: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))
  E66: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E66 with rule R6 and substitution [F := helper, a := y, i := x, y := y1].

This yields E67: (recup(helper, x, y1, y) , y ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E67 with rule R6 and substitution [F := helper, a := 1, i := x1, y := y].

This yields E68: (recup(helper, x, y1, y) , y ≈ x * 1 | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , recup(helper, x, y, 1))

We use ALTER to add x2 = x * 1 to the constraint, and then use CALC at position r.

This yields E69: (recup(helper, x, y1, y) , y ≈ x2 | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) ∧ x2 = x * 1 , recup(helper, x, y, 1))

We observe that x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) ∧ x2 = x * 1 ⊨ y = x2, and may therefore apply EQ-DELETION to remove E69 from the proof state.

We apply SIMPLIFICATION to E65 with rule R7 and substitution [F := helper, a := y, i := x, y := y1].

This yields E70: (recup(helper, x, y1, y) , helper(recup(helper, x + 1, y1, y), x) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))

We use CALC at position l1.2.

This yields E71: (recup(helper, x, y1, y) , helper(recup(helper, x1, y1, y), x) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E71 with rule R10 and substitution [x := recup(helper, x1, y1, y), y := x].

This yields E72: (recup(helper, x, y1, y) , x * recup(helper, x1, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))

We apply HDELETE to E72 with induction hypothesis H60 and substitution [x := x1, y := y, y1 := y1].

We apply HYPOTHESIS to E58 with induction hypothesis H60 and substitution [x := 1, y := x, y1 := x1].  To this end, we impose the requirement that factRU(x) ≻ recup(helper, 1, x, 1) | x ≥ 1 ∧ x1 = x - 1.

This yields E73: (factRU(x) , recup(helper, 1, x, 1) ≈ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We apply SIMPLIFICATION to E73 with rule R7 and substitution [F := helper, a := 1, i := 1, y := x].

This yields E74: (factRU(x) , helper(recup(helper, 1 + 1, x, 1), 1) ≈ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We use CALC at position l1.2.

This yields E75: (factRU(x) , helper(recup(helper, 2, x, 1), 1) ≈ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We apply SIMPLIFICATION to E75 with rule R10 and substitution [x := recup(helper, 2, x, 1), y := 1].

This yields E76: (factRU(x) , 1 * recup(helper, 2, x, 1) ≈ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We apply POSTULATE to add the lemma equation 1 * x ≈ x to the current proof state.

This yields E77: (• , 1 * x ≈ x , •)

We apply INDUCT to E77, which causes 1 * x ≈ x to be added to the set H of induction hypotheses.

This yields E78: (1 * x , 1 * x ≈ x , x)

We use ALTER to add x1 = 1 * x to the constraint, and then use CALC at position l.

This yields E79: (1 * x , x1 ≈ x | x1 = 1 * x , x)

We observe that x1 = 1 * x ⊨ x1 = x, and may therefore apply EQ-DELETION to remove E79 from the proof state.

We apply HYPOTHESIS to E76 with induction hypothesis H77 and substitution [x := recup(helper, 2, x, 1)].  To this end, we impose the requirement that factRU(x) ≻ recup(helper, 2, x, 1) | x ≥ 1 ∧ x1 = x - 1.

This yields E80: (factRU(x) , recup(helper, 2, x, 1) ≈ recdown([*], 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRD(x))

We apply HDELETE to E80 with induction hypothesis H24 and substitution [a := 1, x := 2, y := x].

All equations have been removed, so the proof is complete: the original equations are inductive theorems, provided the underlying ordering requirements can be satisfied.  Unfortunately, the existence of a suitable ordering has not yet been proved.