We start the process with the following equations:

  E1: (• , funfactTU(h, x) ≈ funfactTD(h, x) , •)

We apply POSTULATE to add the lemma equation u(h, x, i, a) ≈ tailup(helperF(h), i, x, a) to the current proof state.

This yields E2: (• , u(h, x, i, a) ≈ tailup(helperF(h), i, x, a) , •)

We apply INDUCT to E2, which causes u(h, x, i, a) ≈ tailup(helperF(h), i, x, a) to be added to the set H of induction hypotheses.

This yields E3: (u(h, x, i, a) , u(h, x, i, a) ≈ tailup(helperF(h), i, x, a) , tailup(helperF(h), i, x, a))

We apply CASE on the constraint i ≤ x.

This yields the following new equations:

  E4: (u(h, x, i, a) , u(h, x, i, a) ≈ tailup(helperF(h), i, x, a) | i ≤ x , tailup(helperF(h), i, x, a))
  E5: (u(h, x, i, a) , u(h, x, i, a) ≈ tailup(helperF(h), i, x, a) | ¬(i ≤ x) , tailup(helperF(h), i, x, a))

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

This yields E6: (u(h, x, i, a) , a ≈ tailup(helperF(h), i, x, a) | ¬(i ≤ x) , tailup(helperF(h), i, x, a))

We apply SIMPLIFICATION to E6 with rule R7 and substitution [F := helperF(h), a := a, i := i, y := x].

This yields E7: (u(h, x, i, a) , a ≈ a | ¬(i ≤ x) , tailup(helperF(h), i, x, a))

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

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

This yields E8: (u(h, x, i, a) , u(h, x, i + 1, h(i) * a) ≈ tailup(helperF(h), i, x, a) | i ≤ x , tailup(helperF(h), i, x, a))

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

This yields E9: (u(h, x, i, a) , u(h, x, i1, h(i) * a) ≈ tailup(helperF(h), i, x, a) | i ≤ x ∧ i1 = i + 1 , tailup(helperF(h), i, x, a))

We apply SIMPLIFICATION to E9 with rule R8 and substitution [F := helperF(h), a := a, i := i, y := x].

This yields E10: (u(h, x, i, a) , u(h, x, i1, h(i) * a) ≈ tailup(helperF(h), i + 1, x, helperF(h, i, a)) | i ≤ x ∧ i1 = i + 1 , tailup(helperF(h), i, x, a))

We use CALC at position r2.

This yields E11: (u(h, x, i, a) , u(h, x, i1, h(i) * a) ≈ tailup(helperF(h), i1, x, helperF(h, i, a)) | i ≤ x ∧ i1 = i + 1 , tailup(helperF(h), i, x, a))

We apply SIMPLIFICATION to E11 with rule R11 and substitution [h := h, x1 := i, x2 := a].

This yields E12: (u(h, x, i, a) , u(h, x, i1, h(i) * a) ≈ tailup(helperF(h), i1, x, h(i) * a) | i ≤ x ∧ i1 = i + 1 , tailup(helperF(h), i, x, a))

We apply HDELETE to E12 with induction hypothesis H2 and substitution [a := h(i) * a, h := h, i := i1, x := x].

We apply POSTULATE to add the lemma equation d(h, i, a) ≈ taildown(helperG(h), 1, i, a) to the current proof state.

This yields E13: (• , d(h, i, a) ≈ taildown(helperG(h), 1, i, a) , •)

We apply INDUCT to E13, which causes d(h, i, a) ≈ taildown(helperG(h), 1, i, a) to be added to the set H of induction hypotheses.

This yields E14: (d(h, i, a) , d(h, i, a) ≈ taildown(helperG(h), 1, i, a) , taildown(helperG(h), 1, i, a))

We apply CASE on the constraint i ≥ 1.

This yields the following new equations:

  E15: (d(h, i, a) , d(h, i, a) ≈ taildown(helperG(h), 1, i, a) | i ≥ 1 , taildown(helperG(h), 1, i, a))
  E16: (d(h, i, a) , d(h, i, a) ≈ taildown(helperG(h), 1, i, a) | ¬(i ≥ 1) , taildown(helperG(h), 1, i, a))

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

This yields E17: (d(h, i, a) , a ≈ taildown(helperG(h), 1, i, a) | ¬(i ≥ 1) , taildown(helperG(h), 1, i, a))

We apply SIMPLIFICATION to E17 with rule R9 and substitution [F := helperG(h), a := a, i := i, x := 1].

This yields E18: (d(h, i, a) , a ≈ a | ¬(i ≥ 1) , taildown(helperG(h), 1, i, a))

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

We apply SIMPLIFICATION to E15 with rule R6 and substitution [a := a, h := h, x := i].

This yields E19: (d(h, i, a) , d(h, i - 1, a * h(i)) ≈ taildown(helperG(h), 1, i, a) | i ≥ 1 , taildown(helperG(h), 1, i, a))

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

This yields E20: (d(h, i, a) , d(h, i1, a * h(i)) ≈ taildown(helperG(h), 1, i, a) | i ≥ 1 ∧ i1 = i - 1 , taildown(helperG(h), 1, i, a))

We apply SIMPLIFICATION to E20 with rule R10 and substitution [F := helperG(h), a := a, i := i, x := 1].

This yields E21: (d(h, i, a) , d(h, i1, a * h(i)) ≈ taildown(helperG(h), 1, i - 1, helperG(h, a, i)) | i ≥ 1 ∧ i1 = i - 1 , taildown(helperG(h), 1, i, a))

We use CALC at position r3.

This yields E22: (d(h, i, a) , d(h, i1, a * h(i)) ≈ taildown(helperG(h), 1, i1, helperG(h, a, i)) | i ≥ 1 ∧ i1 = i - 1 , taildown(helperG(h), 1, i, a))

We apply SIMPLIFICATION to E22 with rule R12 and substitution [h := h, x1 := a, x2 := i].

This yields E23: (d(h, i, a) , d(h, i1, a * h(i)) ≈ taildown(helperG(h), 1, i1, a * h(i)) | i ≥ 1 ∧ i1 = i - 1 , taildown(helperG(h), 1, i, a))

We apply HDELETE to E23 with induction hypothesis H13 and substitution [a := a * h(i), h := h, i := i1].

We apply POSTULATE to add the lemma equation tailup(helperF(h), x, y, a) ≈ taildown(helperG(h), x, y, a) to the current proof state.

This yields E24: (• , tailup(helperF(h), x, y, a) ≈ taildown(helperG(h), x, y, a) , •)

We apply INDUCT to E24, which causes tailup(helperF(h), x, y, a) ≈ taildown(helperG(h), x, y, a) to be added to the set H of induction hypotheses.

This yields E25: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x, y, a) ≈ taildown(helperG(h), x, y, a) , taildown(helperG(h), x, y, a))

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

  E26: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x, y, a) ≈ taildown(helperG(h), x, y, a) | x ≤ y , taildown(helperG(h), x, y, a))
  E27: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x, y, a) ≈ taildown(helperG(h), x, y, a) | ¬(x ≤ y) , taildown(helperG(h), x, y, a))

We apply SIMPLIFICATION to E27 with rule R7 and substitution [F := helperF(h), a := a, i := x, y := y].

This yields E28: (tailup(helperF(h), x, y, a) , a ≈ taildown(helperG(h), x, y, a) | ¬(x ≤ y) , taildown(helperG(h), x, y, a))

We apply SIMPLIFICATION to E28 with rule R9 and substitution [F := helperG(h), a := a, i := y, x := x].

This yields E29: (tailup(helperF(h), x, y, a) , a ≈ a | ¬(x ≤ y) , taildown(helperG(h), 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 R8 and substitution [F := helperF(h), a := a, i := x, y := y].

This yields E30: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x + 1, y, helperF(h, x, a)) ≈ taildown(helperG(h), x, y, a) | x ≤ y , taildown(helperG(h), x, y, a))

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

This yields E31: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x1, y, helperF(h, x, a)) ≈ taildown(helperG(h), x, y, a) | x ≤ y ∧ x1 = x + 1 , taildown(helperG(h), x, y, a))

We apply SIMPLIFICATION to E31 with rule R11 and substitution [h := h, x1 := x, x2 := a].

This yields E32: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y, a) | x ≤ y ∧ x1 = x + 1 , taildown(helperG(h), x, y, a))

We apply SIMPLIFICATION to E32 with rule R10 and substitution [F := helperG(h), a := a, i := y, x := x].

This yields E33: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y - 1, helperG(h, a, y)) | x ≤ y ∧ x1 = x + 1 , taildown(helperG(h), x, y, a))

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

This yields E34: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y1, helperG(h, a, y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , taildown(helperG(h), x, y, a))

We apply SIMPLIFICATION to E34 with rule R12 and substitution [h := h, x1 := a, x2 := y].

This yields E35: (tailup(helperF(h), x, y, a) , tailup(helperF(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , taildown(helperG(h), x, y, a))

We apply HYPOTHESIS to E35 with induction hypothesis H24 and substitution [a := h(x) * a, h := h, x := x1, y := y].  To this end, we impose the requirement that tailup(helperF(h), x, y, a) ≻ taildown(helperG(h), x1, y, h(x) * a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1.

This yields E36: (tailup(helperF(h), x, y, a) , taildown(helperG(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , taildown(helperG(h), x, y, a))

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

This yields E37: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 , taildown(helperG(h), x, y1, a * h(y)))

We apply CASE on the constraint x1 ≤ y.

This yields the following new equations:

  E38: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , taildown(helperG(h), x, y1, a * h(y)))
  E39: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y, h(x) * a) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , taildown(helperG(h), x, y1, a * h(y)))

We apply SIMPLIFICATION to E39 with rule R9 and substitution [F := helperG(h), a := h(x) * a, i := y, x := x1].

This yields E40: (taildown(helperG(h), x1, y, h(x) * a) , h(x) * a ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , taildown(helperG(h), x, y1, a * h(y)))

We apply SIMPLIFICATION to E40 with rule R9 and substitution [F := helperG(h), a := a * h(y), i := y1, x := x].

This yields E41: (taildown(helperG(h), x1, y, h(x) * a) , h(x) * a ≈ a * h(y) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , taildown(helperG(h), x, y1, a * h(y)))

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

This yields E42: (• , x * y ≈ y * x , •)

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

This yields E43: (x * y , x * y ≈ y * x , y * x)

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

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

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

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

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

We apply HYPOTHESIS to E41 with induction hypothesis H42 and substitution [x := h(x), y := a].  To this end, we impose the requirement that taildown(helperG(h), x1, y, h(x) * a) ≻ a * h(x) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y).

This yields E46: (taildown(helperG(h), x1, y, h(x) * a) , a * h(x) ≈ a * h(y) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , taildown(helperG(h), x, y1, a * h(y)))

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

We apply SIMPLIFICATION to E38 with rule R10 and substitution [F := helperG(h), a := h(x) * a, i := y, x := x1].

This yields E47: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y - 1, helperG(h, h(x) * a, y)) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , taildown(helperG(h), x, y1, a * h(y)))

We use CALC at position l3.

This yields E48: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y1, helperG(h, h(x) * a, y)) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , taildown(helperG(h), x, y1, a * h(y)))

We apply SIMPLIFICATION to E48 with rule R12 and substitution [h := h, x1 := h(x) * a, x2 := y].

This yields E49: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y1, h(x) * a * h(y)) ≈ taildown(helperG(h), x, y1, a * h(y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , taildown(helperG(h), x, y1, a * h(y)))

We apply SIMPLIFICATION to E49 with rule R10 and substitution [F := helperG(h), a := a * h(y), i := y1, x := x].

This yields E50: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y1, h(x) * a * h(y)) ≈ taildown(helperG(h), x, y1 - 1, helperG(h, a * h(y), y1)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , taildown(helperG(h), x, y1, a * h(y)))

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

This yields E51: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y1, h(x) * a * h(y)) ≈ taildown(helperG(h), x, y2, helperG(h, a * h(y), y1)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1 , taildown(helperG(h), x, y1, a * h(y)))

We apply SIMPLIFICATION to E51 with rule R12 and substitution [h := h, x1 := a * h(y), x2 := y1].

This yields E52: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y1, h(x) * a * h(y)) ≈ taildown(helperG(h), x, y2, a * h(y) * h(y1)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1 , taildown(helperG(h), x, y1, a * h(y)))

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

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

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

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

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

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

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

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

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

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

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

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

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

We apply HYPOTHESIS to E52 with induction hypothesis H53 and substitution [x := h(x), y := a, z := h(y)].  To this end, we impose the requirement that taildown(helperG(h), x1, y, h(x) * a) ≻ taildown(helperG(h), x1, y1, h(x) * (a * h(y))) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1.

This yields E59: (taildown(helperG(h), x1, y, h(x) * a) , taildown(helperG(h), x1, y1, h(x) * (a * h(y))) ≈ taildown(helperG(h), x, y2, a * h(y) * h(y1)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1 , taildown(helperG(h), x, y1, a * h(y)))

We apply HDELETE to E59 with induction hypothesis H36 and substitution [a := a * h(y), h := h, x := x, x1 := x1, y := y1, y1 := y2].

We apply INDUCT to E1, which causes funfactTU(h, x) ≈ funfactTD(h, x) to be added to the set H of induction hypotheses.

This yields E60: (funfactTU(h, x) , funfactTU(h, x) ≈ funfactTD(h, x) , funfactTD(h, x))

We apply SIMPLIFICATION to E60 with rule R1 and substitution [h := h, x := x].

This yields E61: (funfactTU(h, x) , u(h, x, 1, 1) ≈ funfactTD(h, x) , funfactTD(h, x))

We apply SIMPLIFICATION to E61 with rule R4 and substitution [h := h, x := x].

This yields E62: (funfactTU(h, x) , u(h, x, 1, 1) ≈ d(h, x, 1) , funfactTD(h, x))

We apply HYPOTHESIS to E62 with induction hypothesis H13 and substitution [a := 1, h := h, i := x].  To this end, we impose the requirement that funfactTD(h, x) ≻ taildown(helperG(h), 1, x, 1).

This yields E63: (funfactTU(h, x) , u(h, x, 1, 1) ≈ taildown(helperG(h), 1, x, 1) , funfactTD(h, x))

We apply HYPOTHESIS to E63 with induction hypothesis H2 and substitution [a := 1, h := h, i := 1, x := x].  To this end, we impose the requirement that funfactTU(h, x) ≻ tailup(helperF(h), 1, x, 1).

This yields E64: (funfactTU(h, x) , tailup(helperF(h), 1, x, 1) ≈ taildown(helperG(h), 1, x, 1) , funfactTD(h, x))

We apply HDELETE to E64 with induction hypothesis H24 and substitution [a := 1, h := h, x := 1, 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.