Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/lnexp_fnd/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 217 kB

Quelle atanh_series.proof Sprache: unbekannt

USED PATCH 873
-----------------
Starting pvs-allegro6.2 -qq ...
Allegro CL Enterprise Edition
6.2 [Linux (x86)] (Nov 3, 2004 23:30)
Copyright (C) 1985-2002, Franz Inc., Berkeley, CA, USA.  All Rights Reserved.

This dynamic runtime copy of Allegro CL was built by:
   [TC8101] SRI International

;; Optimization settings: safety 1, space 1, speed 3, debug 1.
;; For a complete description of all compiler switches given the
;; current optimization settings evaluate (explain-compiler-settings).
;;---
;; Current reader case mode: :case-sensitive-lower
pvs(1):
pvs(2): nil
pvs(9): nil
pvs(11): ; Loading /home/rwb/pvs-strategies

Defining sqrt-rew.
Defining sqrt-rew$.
Defining sqrt-rew-off.
Defining sqrt-rew-off$.
Installing rewrite rule sq_abs_neg
Installing rewrite rule sq_abs
Installing rewrite rule sq_1
Installing rewrite rule sq_0
Installing rewrite rule sq_sqrt
Installing rewrite rule sqrt_sq_neg
Installing rewrite rule sqrt_sq
Installing rewrite rule sqrt_square
Installing rewrite rule sqrt_1
Installing rewrite rule sqrt_0
Installing rewrite rule sqrt_25
Installing rewrite rule sqrt_16
Installing rewrite rule sqrt_9
Installing rewrite rule sqrt_4
Installing rewrite rule factorial_0
Installing rewrite rule factorial_1
Installing rewrite rule ln_e
Installing rewrite rule ln_1
Installing rewrite rule exp_1
Installing rewrite rule exp_0
Installing rewrite rule Riemann?_Rie
Installing rewrite rule xis_lem
Installing rewrite rule xis?
Installing rewrite rule member
Installing rewrite rule member
Installing rewrite rule finseq_appl
Installing rewrite rule not_one_element
Installing rewrite rule sort_length
Installing rewrite rule not_one_element
Installing rewrite rule set2seq_length
Installing rewrite rule set2part_length
Installing rewrite rule not_one_element
Installing rewrite rule not_one_element
Installing rewrite rule not_one_element
Installing rewrite rule not_one_element

atanh_series :

  |-------
{1}   FORALL (n: nat, z: real_abs_lt1):
        abs(atanh(z) - atanh_series_n(z, n)) <=
         ((1 + z) ^ (2 * n + 3) + (1 - z) ^ (2 * n + 3)) /
          (2 * (2 * n + 3) * (1 - sq(z)) ^ (2 * n + 3))

Rerunning step: (skosimp*)

Repeatedly Skolemizing and flattening,
this simplifies to:
atanh_series :

  |-------
{1}   abs(atanh(z!1) - atanh_series_n(z!1, n!1)) <=
       ((1 + z!1) ^ (2 * n!1 + 3) + (1 - z!1) ^ (2 * n!1 + 3)) /
        (2 * (2 * n!1 + 3) * (1 - sq(z!1)) ^ (2 * n!1 + 3))

Rerunning step: (lemma "atanh_taylors" ("z" "z!1" "n" "n!1"))
Applying atanh_taylors where
  z gets z!1,
  n gets n!1,
this simplifies to:
atanh_series :

{-1}  EXISTS (c: between[real_abs_lt1](0, z!1)):
        atanh(z!1) =
         atanh_series_n(z!1, n!1) +
          nderiv[real_abs_lt1](2 * n!1 + 3, atanh)(c) * z!1 ^ (2 * n!1 + 3)
           / factorial(2 * n!1 + 3)
  |-------
[1]   abs(atanh(z!1) - atanh_series_n(z!1, n!1)) <=
       ((1 + z!1) ^ (2 * n!1 + 3) + (1 - z!1) ^ (2 * n!1 + 3)) /
        (2 * (2 * n!1 + 3) * (1 - sq(z!1)) ^ (2 * n!1 + 3))

Rerunning step: (skosimp*)
Repeatedly Skolemizing and flattening,
this simplifies to:
atanh_series :

{-1}  atanh(z!1) =
       atanh_series_n(z!1, n!1) +
        nderiv[real_abs_lt1](2 * n!1 + 3, atanh)(c!1) * z!1 ^ (2 * n!1 + 3)
         / factorial(2 * n!1 + 3)
  |-------
[1]   abs(atanh(z!1) - atanh_series_n(z!1, n!1)) <=
       ((1 + z!1) ^ (2 * n!1 + 3) + (1 - z!1) ^ (2 * n!1 + 3)) /
        (2 * (2 * n!1 + 3) * (1 - sq(z!1)) ^ (2 * n!1 + 3))

Rerunning step: (replace -1 1)
Replacing using formula -1,
this simplifies to:
atanh_series :

[-1]  atanh(z!1) =
       atanh_series_n(z!1, n!1) +
        nderiv[real_abs_lt1](2 * n!1 + 3, atanh)(c!1) * z!1 ^ (2 * n!1 + 3)
         / factorial(2 * n!1 + 3)
  |-------
{1}   abs(atanh_series_n(z!1, n!1) +
           nderiv[real_abs_lt1](2 * n!1 + 3, atanh)(c!1) *
            z!1 ^ (2 * n!1 + 3)
            / factorial(2 * n!1 + 3)
           - atanh_series_n(z!1, n!1))
       <=
       ((1 + z!1) ^ (2 * n!1 + 3) + (1 - z!1) ^ (2 * n!1 + 3)) /
        (2 * (2 * n!1 + 3) * (1 - sq(z!1)) ^ (2 * n!1 + 3))

Rerunning step: (simplify 1)
Simplifying with decision procedures,
this simplifies to:
atanh_series :

[-1]  atanh(z!1) =
       atanh_series_n(z!1, n!1) +
        nderiv[real_abs_lt1](2 * n!1 + 3, atanh)(c!1) * z!1 ^ (2 * n!1 + 3)
         / factorial(2 * n!1 + 3)
  |-------
{1}   abs((nderiv[real_abs_lt1](3 + 2 * n!1, atanh)(c!1) *
            z!1 ^ (3 + 2 * n!1))
           / factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series :

  |-------
[1]   abs((nderiv[real_abs_lt1](3 + 2 * n!1, atanh)(c!1) *
            z!1 ^ (3 + 2 * n!1))
           / factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (lemma "atanh_nderiv" ("n" "3+2*n!1"))
Applying atanh_nderiv where
  n gets 3 + 2 * n!1,
this simplifies to:
atanh_series :

{-1}  nderiv[real_abs_lt1](3 + 2 * n!1, atanh) =
       IF 3 + 2 * n!1 = 0 THEN atanh
       ELSIF even?(3 + 2 * n!1)
         THEN deriv[real_abs_lt1](atanhND((3 + 2 * n!1) / 2 - 1))
       ELSE atanhND((3 + 2 * n!1 - 1) / 2)
       ENDIF
  |-------
[1]   abs((nderiv[real_abs_lt1](3 + 2 * n!1, atanh)(c!1) *
            z!1 ^ (3 + 2 * n!1))
           / factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (simplify -1)
Simplifying with decision procedures,
this simplifies to:
atanh_series :

{-1}  nderiv[real_abs_lt1](3 + 2 * n!1, atanh) =
          IF even?(3 + 2 * n!1)
         THEN deriv[real_abs_lt1](atanhND((3 + 2 * n!1) / 2 - 1))
       ELSE atanhND((2 + 2 * n!1) / 2)
  |-------
[1]   abs((nderiv[real_abs_lt1](3 + 2 * n!1, atanh)(c!1) *
            z!1 ^ (3 + 2 * n!1))
           / factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (expand "even?" -1)
Expanding the definition of even?,
this simplifies to:
atanh_series :

{-1}  nderiv[real_abs_lt1](3 + 2 * n!1, atanh) = atanhND((2 + 2 * n!1) / 2)
  |-------
[1]   abs((nderiv[real_abs_lt1](3 + 2 * n!1, atanh)(c!1) *
            z!1 ^ (3 + 2 * n!1))
           / factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (lemma "div_cancel1" ("x" "1+n!1" "n0z" "2"))
Applying div_cancel1 where
  x gets 1 + n!1,
  n0z gets 2,
this simplifies to:
atanh_series :

{-1}  2 * ((1 + n!1) / 2) = 1 + n!1
[-2]  nderiv[real_abs_lt1](3 + 2 * n!1, atanh) = atanhND((2 + 2 * n!1) / 2)
  |-------
[1]   abs((nderiv[real_abs_lt1](3 + 2 * n!1, atanh)(c!1) *
            z!1 ^ (3 + 2 * n!1))
           / factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (replace -1 -2)
Replacing using formula -1,
this simplifies to:
atanh_series :

[-1]  2 * ((1 + n!1) / 2) = 1 + n!1
{-2}  nderiv[real_abs_lt1](3 + 2 * n!1, atanh) = atanhND(1 + n!1)
  |-------
[1]   abs((nderiv[real_abs_lt1](3 + 2 * n!1, atanh)(c!1) *
            z!1 ^ (3 + 2 * n!1))
           / factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (replace -2 1)
Replacing using formula -2,
this simplifies to:
atanh_series :

[-1]  2 * ((1 + n!1) / 2) = 1 + n!1
[-2]  nderiv[real_abs_lt1](3 + 2 * n!1, atanh) = atanhND(1 + n!1)
  |-------
{1}   abs((atanhND(1 + n!1)(c!1) * z!1 ^ (3 + 2 * n!1)) /
           factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (hide -1 -2)
Hiding formulas:  -1, -2,
this simplifies to:
atanh_series :

  |-------
[1]   abs((atanhND(1 + n!1)(c!1) * z!1 ^ (3 + 2 * n!1)) /
           factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (case "1-sq(z!1)>0")
Case splitting on
   1 - sq(z!1) > 0,
this yields  2 subgoals:
atanh_series.1 :

{-1}  1 - sq(z!1) > 0
  |-------
[1]   abs((atanhND(1 + n!1)(c!1) * z!1 ^ (3 + 2 * n!1)) /
           factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (case "abs(z!1^(3+2*n!1))<1")
Case splitting on
   abs(z!1 ^ (3 + 2 * n!1)) < 1,
this yields  2 subgoals:
atanh_series.1.1 :

{-1}  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-2]  1 - sq(z!1) > 0
  |-------
[1]   abs((atanhND(1 + n!1)(c!1) * z!1 ^ (3 + 2 * n!1)) /
           factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (rewrite "abs_div" 1)
Found matching substitution:
n0y: nonzero_real gets factorial(3 + 2 * n!1),
x: real gets atanhND(1 + n!1)(c!1) * z!1 ^ (3 + 2 * n!1),
Rewriting using abs_div, matching in 1,
this simplifies to:
atanh_series.1.1 :

[-1]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-2]  1 - sq(z!1) > 0
  |-------
{1}   abs(atanhND(1 + n!1)(c!1) * z!1 ^ (3 + 2 * n!1)) /
       abs(factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (rewrite "abs_mult" 1)
Found matching substitution:
y: real gets z!1 ^ (3 + 2 * n!1),
x gets atanhND(1 + n!1)(c!1),
Rewriting using abs_mult, matching in 1,
this simplifies to:
atanh_series.1.1 :

[-1]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-2]  1 - sq(z!1) > 0
  |-------
{1}   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       abs(factorial(3 + 2 * n!1))
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (expand "abs" 1 3)
Expanding the definition of abs,
this simplifies to:
atanh_series.1.1 :

[-1]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-2]  1 - sq(z!1) > 0
  |-------
{1}   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       factorial(3 + 2 * n!1)
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (lemma "expt_pos" ("px" "1-sq(z!1)" "i" "3+2*n!1"))
Applying expt_pos where
  px gets 1 - sq(z!1),
  i gets 3 + 2 * n!1,
this yields  2 subgoals:
atanh_series.1.1.1 :

{-1}  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-3]  1 - sq(z!1) > 0
  |-------
[1]   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       factorial(3 + 2 * n!1)
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (lemma "posreal_times_posreal_is_posreal"
                 ("px" "6+4*n!1" "py" "(1 - sq(z!1)) ^ (3 + 2 * n!1)"))
Applying posreal_times_posreal_is_posreal where
  px gets 6 + 4 * n!1,
  py gets (1 - sq(z!1)) ^ (3 + 2 * n!1),
this yields  2 subgoals:
atanh_series.1.1.1.1 :

{-1}  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-3]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-4]  1 - sq(z!1) > 0
  |-------
[1]   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       factorial(3 + 2 * n!1)
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (case "atanhND(1 + n!1)(c!1)>0")
Case splitting on
   atanhND(1 + n!1)(c!1) > 0,
this yields  2 subgoals:
atanh_series.1.1.1.1.1 :

{-1}  atanhND(1 + n!1)(c!1) > 0
[-2]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-3]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-4]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-5]  1 - sq(z!1) > 0
  |-------
[1]   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       factorial(3 + 2 * n!1)
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (case "abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1)")
Case splitting on
   abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1),
this yields  2 subgoals:
atanh_series.1.1.1.1.1.1 :

{-1}  abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1)
[-2]  atanhND(1 + n!1)(c!1) > 0
[-3]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-4]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-5]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-6]  1 - sq(z!1) > 0
  |-------
[1]   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       factorial(3 + 2 * n!1)
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (case "atanhND(1 + n!1)(z!1) = factorial(2+2*n!1)*(((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) / (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))")
Case splitting on
   atanhND(1 + n!1)(z!1) =
    factorial(2 + 2 * n!1) *
     (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
       (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1))),
this yields  3 subgoals:
atanh_series.1.1.1.1.1.1.1 :

{-1}  atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
[-2]  abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
[-4]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-5]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  1 - sq(z!1) > 0
  |-------
[1]   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       factorial(3 + 2 * n!1)
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (rewrite "div_mult_pos_le1" 1)
Found matching substitution:
x gets ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1)),
py: posreal gets factorial(3 + 2 * n!1),
z: real gets abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)),
Rewriting using div_mult_pos_le1, matching in 1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

[-1]  atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
[-2]  abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
[-4]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-5]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  1 - sq(z!1) > 0
  |-------
{1}   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
         (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
           4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1)))
        * factorial(3 + 2 * n!1)

Rerunning step: (expand "abs" 1 1)
Expanding the definition of abs,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

[-1]  atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
[-2]  abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
[-4]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-5]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  1 - sq(z!1) > 0
  |-------
{1}   IF atanhND(1 + n!1)(c!1) < 0 THEN -atanhND(1 + n!1)(c!1)
      ELSE atanhND(1 + n!1)(c!1)
      ENDIF
       * abs(z!1 ^ (3 + 2 * n!1))
       <=
       (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
         (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
           4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1)))
        * factorial(3 + 2 * n!1)

Rerunning step: (expand "abs" -2)
Expanding the definition of abs,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

[-1]  atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
{-2}  IF atanhND(1 + n!1)(c!1) < 0 THEN -atanhND(1 + n!1)(c!1)
      ELSE atanhND(1 + n!1)(c!1)
      ENDIF
       <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
[-4]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-5]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  1 - sq(z!1) > 0
  |-------
[1]   IF atanhND(1 + n!1)(c!1) < 0 THEN -atanhND(1 + n!1)(c!1)
      ELSE atanhND(1 + n!1)(c!1)
      ENDIF
       * abs(z!1 ^ (3 + 2 * n!1))
       <=
       (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
         (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
           4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1)))
        * factorial(3 + 2 * n!1)

Rerunning step: (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

[-1]  atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
{-2}  atanhND(1 + n!1)(c!1) <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
{-4}  6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
       4 * ((1 - sq(z!1)) ^ (3 + 2 * n!1) * n!1)
       > 0
[-5]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  1 - sq(z!1) > 0
  |-------
{1}   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
         (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
           4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1)))
        * factorial(3 + 2 * n!1)

Rerunning step: (name-replace "K10" "1 - sq(z!1)")
Using K10 to name and replace 1 - sq(z!1),
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

{-1}  atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * K10 ^ (3 + 2 * n!1)))
[-2]  atanhND(1 + n!1)(c!1) <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
{-4}  6 * K10 ^ (3 + 2 * n!1) + 4 * (K10 ^ (3 + 2 * n!1) * n!1) > 0
{-5}  K10 ^ (3 + 2 * n!1) > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
{-7}  K10 > 0
  |-------
{1}   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
         (6 * K10 ^ (3 + 2 * n!1) + 4 * ((K10 ^ (3 + 2 * n!1)) * n!1)))
        * factorial(3 + 2 * n!1)

Rerunning step: (name-replace "K11" "K10^(3+2*n!1)")
Using K11 to name and replace K10^(3+2*n!1),
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

{-1}  atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * K11))
[-2]  atanhND(1 + n!1)(c!1) <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
{-4}  6 * K11 + 4 * (K11 * n!1) > 0
{-5}  K11 > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  K10 > 0
  |-------
{1}   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
         (6 * K11 + 4 * (K11 * n!1)))
        * factorial(3 + 2 * n!1)

Rerunning step: (name-replace "K12"
                 "(1-z!1)^(3+2*n!1)+(1+z!1)^(3+2*n!1)")
Using K12 to name and replace (1-z!1)^(3+2*n!1)+(1+z!1)^(3+2*n!1),
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

{-1}  atanhND(1 + n!1)(z!1) = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-2]  atanhND(1 + n!1)(c!1) <= atanhND(1 + n!1)(z!1)
[-3]  atanhND(1 + n!1)(c!1) > 0
[-4]  6 * K11 + 4 * (K11 * n!1) > 0
[-5]  K11 > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  K10 > 0
  |-------
{1}   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (K12 / (6 * K11 + 4 * (K11 * n!1))) * factorial(3 + 2 * n!1)

Rerunning step: (replace -1 -2)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

[-1]  atanhND(1 + n!1)(z!1) = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
{-2}  atanhND(1 + n!1)(c!1) <= factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-3]  atanhND(1 + n!1)(c!1) > 0
[-4]  6 * K11 + 4 * (K11 * n!1) > 0
[-5]  K11 > 0
[-6]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-7]  K10 > 0
  |-------
[1]   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (K12 / (6 * K11 + 4 * (K11 * n!1))) * factorial(3 + 2 * n!1)

Rerunning step: (lemma "lt_times_lt_pos1"
                 ("px" "atanhND(1 + n!1)(c!1)" "y"
                  "factorial(2 + 2 * n!1) * (K12 / (2 * K11))" "nnz"
                  "abs(z!1 ^ (3 + 2 * n!1))" "w" "1"))
Applying lt_times_lt_pos1 where
  px gets atanhND(1 + n!1)(c!1),
  y gets factorial(2 + 2 * n!1) * (K12 / (2 * K11)),
  nnz gets abs(z!1 ^ (3 + 2 * n!1)),
  w gets 1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

{-1}  atanhND(1 + n!1)(c!1) <= factorial(2 + 2 * n!1) * (K12 / (2 * K11))
       AND abs(z!1 ^ (3 + 2 * n!1)) < 1
       IMPLIES
       atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <
        factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1
[-2]  atanhND(1 + n!1)(z!1) = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-3]  atanhND(1 + n!1)(c!1) <= factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-4]  atanhND(1 + n!1)(c!1) > 0
[-5]  6 * K11 + 4 * (K11 * n!1) > 0
[-6]  K11 > 0
[-7]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-8]  K10 > 0
  |-------
[1]   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (K12 / (6 * K11 + 4 * (K11 * n!1))) * factorial(3 + 2 * n!1)

Rerunning step: (replace -3)
Replacing using formula -3,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

{-1}  abs(z!1 ^ (3 + 2 * n!1)) < 1 IMPLIES
       atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <
        factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1
[-2]  atanhND(1 + n!1)(z!1) = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-3]  atanhND(1 + n!1)(c!1) <= factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-4]  atanhND(1 + n!1)(c!1) > 0
[-5]  6 * K11 + 4 * (K11 * n!1) > 0
[-6]  K11 > 0
[-7]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-8]  K10 > 0
  |-------
[1]   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (K12 / (6 * K11 + 4 * (K11 * n!1))) * factorial(3 + 2 * n!1)

Rerunning step: (replace -7)
Replacing using formula -7,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

{-1}  atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <
       factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1
[-2]  atanhND(1 + n!1)(z!1) = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-3]  atanhND(1 + n!1)(c!1) <= factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-4]  atanhND(1 + n!1)(c!1) > 0
[-5]  6 * K11 + 4 * (K11 * n!1) > 0
[-6]  K11 > 0
[-7]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-8]  K10 > 0
  |-------
[1]   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       (K12 / (6 * K11 + 4 * (K11 * n!1))) * factorial(3 + 2 * n!1)

Rerunning step: (expand "factorial" 1)
Expanding the definition of factorial,
this simplifies to:
atanh_series.1.1.1.1.1.1.1 :

[-1]  atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <
       factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1
[-2]  atanhND(1 + n!1)(z!1) = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-3]  atanhND(1 + n!1)(c!1) <= factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-4]  atanhND(1 + n!1)(c!1) > 0
[-5]  6 * K11 + 4 * (K11 * n!1) > 0
[-6]  K11 > 0
[-7]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-8]  K10 > 0
  |-------
{1}   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)

Rerunning step: (case-replace
                 "factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1 = 3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)")
Assuming and applying factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1 = 3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1),
this yields  2 subgoals:
atanh_series.1.1.1.1.1.1.1.1 :

{-1}  factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1 =
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)
{-2}  atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)
{-3}  atanhND(1 + n!1)(z!1) =
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)
{-4}  atanhND(1 + n!1)(c!1) <=
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)
[-5]  atanhND(1 + n!1)(c!1) > 0
[-6]  6 * K11 + 4 * (K11 * n!1) > 0
[-7]  K11 > 0
[-8]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-9]  K10 > 0
  |-------
[1]   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)

Rerunning step: (assert)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of atanh_series.1.1.1.1.1.1.1.1.

atanh_series.1.1.1.1.1.1.1.2 :

[-1]  atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <
       factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1
[-2]  atanhND(1 + n!1)(z!1) = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-3]  atanhND(1 + n!1)(c!1) <= factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-4]  atanhND(1 + n!1)(c!1) > 0
[-5]  6 * K11 + 4 * (K11 * n!1) > 0
[-6]  K11 > 0
[-7]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-8]  K10 > 0
  |-------
{1}   factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1 =
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)
[2]   atanhND(1 + n!1)(c!1) * abs(z!1 ^ (3 + 2 * n!1)) <=
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)

Rerunning step: (hide-all-but (-5 -6 1))
Keeping (-5 -6 1) and hiding *,
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2 :

[-1]  6 * K11 + 4 * (K11 * n!1) > 0
[-2]  K11 > 0
  |-------
[1]   factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1 =
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)

Rerunning step: (lemma "div_cancel1"
                 ("x" "factorial(2 + 2 * n!1) * (K12 / (2 * K11))"
                  "n0z" "3+2*n!1"))
Applying div_cancel1 where
  x gets factorial(2 + 2 * n!1) * (K12 / (2 * K11)),
  n0z gets 3 + 2 * n!1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2 :

{-1}  (3 + 2 * n!1) *
       (factorial(2 + 2 * n!1) * (K12 / (2 * K11)) / (3 + 2 * n!1))
       = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-2]  6 * K11 + 4 * (K11 * n!1) > 0
[-3]  K11 > 0
  |-------
[1]   factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1 =
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)

Rerunning step: (replace -1 1 rl)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2 :

[-1]  (3 + 2 * n!1) *
       (factorial(2 + 2 * n!1) * (K12 / (2 * K11)) / (3 + 2 * n!1))
       = factorial(2 + 2 * n!1) * (K12 / (2 * K11))
[-2]  6 * K11 + 4 * (K11 * n!1) > 0
[-3]  K11 > 0
  |-------
{1}   (3 + 2 * n!1) *
       (factorial(2 + 2 * n!1) * (K12 / (2 * K11)) / (3 + 2 * n!1))
       =
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2 :

[-1]  6 * K11 + 4 * (K11 * n!1) > 0
[-2]  K11 > 0
  |-------
[1]   (3 + 2 * n!1) *
       (factorial(2 + 2 * n!1) * (K12 / (2 * K11)) / (3 + 2 * n!1))
       =
       3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 *
         ((factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) *
           n!1)

Rerunning step: (name-replace "K13" "factorial(2 + 2 * n!1)")
Using K13 to name and replace factorial(2 + 2 * n!1),
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2 :

[-1]  6 * K11 + 4 * (K11 * n!1) > 0
[-2]  K11 > 0
  |-------
{1}   (3 + 2 * n!1) * (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1)) =
       3 * (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 * ((K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))) * n!1)

Rerunning step: (case-replace
                 "(K13 * (K12 / (2 * K11)) / (3 + 2 * n!1))=(K13 * (K12 / (6 * K11 + 4 * (K11 * n!1))))")
Assuming and applying (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1))=(K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))),
this yields  2 subgoals:
atanh_series.1.1.1.1.1.1.1.2.1 :

{-1}  (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1)) =
       (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1))))
[-2]  6 * K11 + 4 * (K11 * n!1) > 0
[-3]  K11 > 0
  |-------
{1}   (3 + 2 * n!1) * (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))) =
       3 * (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 * ((K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))) * n!1)

Rerunning step: (assert)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of atanh_series.1.1.1.1.1.1.1.2.1.

atanh_series.1.1.1.1.1.1.1.2.2 :

[-1]  6 * K11 + 4 * (K11 * n!1) > 0
[-2]  K11 > 0
  |-------
{1}   (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1)) =
       (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1))))
[2]   (3 + 2 * n!1) * (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1)) =
       3 * (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))) +
        2 * ((K13 * (K12 / (6 * K11 + 4 * (K11 * n!1)))) * n!1)

Rerunning step: (hide 2)
Hiding formulas:  2,
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2.2 :

[-1]  6 * K11 + 4 * (K11 * n!1) > 0
[-2]  K11 > 0
  |-------
[1]   (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1)) =
       (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1))))

Rerunning step: (lemma "cross_mult"
                 ("x" "K13 * (K12 / (2 * K11))" "n0x" "3+2*n!1" "y"
                  "K13*K12" "n0y" "6 * K11 + 4 * (K11 * n!1)"))
Applying cross_mult where
  x gets K13 * (K12 / (2 * K11)),
  n0x gets 3 + 2 * n!1,
  y gets K13 * K12,
  n0y gets 6 * K11 + 4 * (K11 * n!1),
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2.2 :

{-1}  (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1) =
        K13 * K12 / (6 * K11 + 4 * (K11 * n!1)))
       IFF
       (K13 * (K12 / (2 * K11)) * (6 * K11 + 4 * (K11 * n!1)) =
         K13 * K12 * (3 + 2 * n!1))
[-2]  6 * K11 + 4 * (K11 * n!1) > 0
[-3]  K11 > 0
  |-------
[1]   (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1)) =
       (K13 * (K12 / (6 * K11 + 4 * (K11 * n!1))))

Rerunning step: (replace -1)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2.2 :

[-1]  (K13 * (K12 / (2 * K11)) / (3 + 2 * n!1) =
        K13 * K12 / (6 * K11 + 4 * (K11 * n!1)))
       IFF
       (K13 * (K12 / (2 * K11)) * (6 * K11 + 4 * (K11 * n!1)) =
         K13 * K12 * (3 + 2 * n!1))
[-2]  6 * K11 + 4 * (K11 * n!1) > 0
[-3]  K11 > 0
  |-------
{1}   (K13 * (K12 / (2 * K11)) * (6 * K11 + 4 * (K11 * n!1)) =
        K13 * K12 * (3 + 2 * n!1))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.1.2.2 :

[-1]  6 * K11 + 4 * (K11 * n!1) > 0
[-2]  K11 > 0
  |-------
[1]   (K13 * (K12 / (2 * K11)) * (6 * K11 + 4 * (K11 * n!1)) =
        K13 * K12 * (3 + 2 * n!1))

Rerunning step: (assert)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of atanh_series.1.1.1.1.1.1.1.2.2.

This completes the proof of atanh_series.1.1.1.1.1.1.1.2.

This completes the proof of atanh_series.1.1.1.1.1.1.1.

atanh_series.1.1.1.1.1.1.2 :

[-1]  abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1)
[-2]  atanhND(1 + n!1)(c!1) > 0
[-3]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-4]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-5]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-6]  1 - sq(z!1) > 0
  |-------
{1}   atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
[2]   abs(atanhND(1 + n!1)(c!1)) * abs(z!1 ^ (3 + 2 * n!1)) /
       factorial(3 + 2 * n!1)
       <=
       ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
        (6 * (1 - sq(z!1)) ^ (3 + 2 * n!1) +
          4 * (((1 - sq(z!1)) ^ (3 + 2 * n!1)) * n!1))

Rerunning step: (hide -1 -2 2)
Hiding formulas:  -1, -2, 2,
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

[-1]  (6 + 4 * n!1) * (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-3]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-4]  1 - sq(z!1) > 0
  |-------
[1]   atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

[-1]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-3]  1 - sq(z!1) > 0
  |-------
[1]   atanhND(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))

Rerunning step: (expand "atanhND")
Expanding the definition of atanhND,
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

[-1]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-3]  1 - sq(z!1) > 0
  |-------
{1}   atanhN(1 + n!1)(z!1) / atanhD(1 + n!1)(z!1) =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))

Rerunning step: (expand "atanhN")
Expanding the definition of atanhN,
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

[-1]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-3]  1 - sq(z!1) > 0
  |-------
{1}   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) / atanhD(1 + n!1)(z!1)
       =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))

Rerunning step: (expand "atanhD")
Expanding the definition of atanhD,
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

[-1]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-3]  1 - sq(z!1) > 0
  |-------
{1}   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) /
       (1 - sq(z!1)) ^ (3 + 2 * n!1)
       =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))

Rerunning step: (lemma "cross_mult"
                 ("x" "polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1)"
                  "n0x" "(1 - sq(z!1)) ^ (3 + 2 * n!1)" "y"
                  "factorial(2 + 2 * n!1) * ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))"
                  "n0y" "2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)"))
Applying cross_mult where
  x gets polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1),
  n0x gets (1 - sq(z!1)) ^ (3 + 2 * n!1),
  y gets factorial(2 + 2 * n!1) *
          ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)),
  n0y gets 2 * (1 - sq(z!1)) ^ (3 + 2 * n!1),
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

{-1}  (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) /
        (1 - sq(z!1)) ^ (3 + 2 * n!1)
        =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
         / (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
       IFF
       (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) *
         (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1))
         =
         factorial(2 + 2 * n!1) *
          ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
          * (1 - sq(z!1)) ^ (3 + 2 * n!1))
[-2]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-3]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-4]  1 - sq(z!1) > 0
  |-------
[1]   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) /
       (1 - sq(z!1)) ^ (3 + 2 * n!1)
       =
       factorial(2 + 2 * n!1) *
        (((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) /
          (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))

Rerunning step: (replace -1 1)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

[-1]  (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) /
        (1 - sq(z!1)) ^ (3 + 2 * n!1)
        =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
         / (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))
       IFF
       (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) *
         (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1))
         =
         factorial(2 + 2 * n!1) *
          ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
          * (1 - sq(z!1)) ^ (3 + 2 * n!1))
[-2]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-3]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-4]  1 - sq(z!1) > 0
  |-------
{1}   (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) *
        (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1))
        =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
         * (1 - sq(z!1)) ^ (3 + 2 * n!1))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2 :

[-1]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-3]  1 - sq(z!1) > 0
  |-------
[1]   (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) *
        (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1))
        =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
         * (1 - sq(z!1)) ^ (3 + 2 * n!1))

Rerunning step: (lemma "both_sides_times1"
                 ("x"
                  "polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2"
                  "n0z" "(1 - sq(z!1)) ^ (3 + 2 * n!1)" "y"
                  "factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))"))
Applying both_sides_times1 where
  x gets polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2,
  n0z gets (1 - sq(z!1)) ^ (3 + 2 * n!1),
  y gets factorial(2 + 2 * n!1) *
          ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)),
this yields  2 subgoals:
atanh_series.1.1.1.1.1.1.2.1 :

{-1}  (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 *
        (1 - sq(z!1)) ^ (3 + 2 * n!1)
        =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
         * (1 - sq(z!1)) ^ (3 + 2 * n!1))
       IFF
       polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
[-2]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-3]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-4]  1 - sq(z!1) > 0
  |-------
[1]   (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) *
        (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1))
        =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
         * (1 - sq(z!1)) ^ (3 + 2 * n!1))

Rerunning step: (replace -1 1)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1 :

[-1]  (polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 *
        (1 - sq(z!1)) ^ (3 + 2 * n!1)
        =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
         * (1 - sq(z!1)) ^ (3 + 2 * n!1))
       IFF
       polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
        factorial(2 + 2 * n!1) *
         ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))
[-2]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-3]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-4]  1 - sq(z!1) > 0
  |-------
{1}   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1 :

[-1]  (1 - sq(z!1)) ^ (3 + 2 * n!1) > 0
[-2]  abs(z!1 ^ (3 + 2 * n!1)) < 1
[-3]  1 - sq(z!1) > 0
  |-------
[1]   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))

Rerunning step: (hide -1 -2)
Hiding formulas:  -1, -2,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1 :

[-1]  1 - sq(z!1) > 0
  |-------
[1]   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))

Rerunning step: (lemma "power_polynomial" ("pn" "3+2*n!1"))
Applying power_polynomial where
  pn gets 3 + 2 * n!1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1 :

{-1}  (LAMBDA (x: real): (1 + x) ^ (3 + 2 * n!1)) =
       polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)
[-2]  1 - sq(z!1) > 0
  |-------
[1]   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))

Rerunning step: (lemma "neg_power_polynomial" ("pn" "3+2*n!1"))
Applying neg_power_polynomial where
  pn gets 3 + 2 * n!1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1 :

{-1}  (LAMBDA (x: real): (1 - x) ^ (3 + 2 * n!1)) =
       polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)
[-2]  (LAMBDA (x: real): (1 + x) ^ (3 + 2 * n!1)) =
       polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)
[-3]  1 - sq(z!1) > 0
  |-------
[1]   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))

Rerunning step: (case-replace
                 "(1 - z!1) ^ (3 + 2 * n!1) = polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1)")
Assuming and applying (1 - z!1) ^ (3 + 2 * n!1) = polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1),
this yields  2 subgoals:
atanh_series.1.1.1.1.1.1.2.1.1 :

{-1}  (1 - z!1) ^ (3 + 2 * n!1) =
       polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1)
[-2]  (LAMBDA (x: real): (1 - x) ^ (3 + 2 * n!1)) =
       polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)
[-3]  (LAMBDA (x: real): (1 + x) ^ (3 + 2 * n!1)) =
       polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)
[-4]  1 - sq(z!1) > 0
  |-------
{1}   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        (polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1) +
          (1 + z!1) ^ (3 + 2 * n!1))

Rerunning step: (case-replace
                 "(1 + z!1) ^ (3 + 2 * n!1) = polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1)")
Assuming and applying (1 + z!1) ^ (3 + 2 * n!1) = polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1),
this yields  2 subgoals:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

{-1}  (1 + z!1) ^ (3 + 2 * n!1) =
       polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1)
[-2]  (1 - z!1) ^ (3 + 2 * n!1) =
       polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1)
[-3]  (LAMBDA (x: real): (1 - x) ^ (3 + 2 * n!1)) =
       polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)
[-4]  (LAMBDA (x: real): (1 + x) ^ (3 + 2 * n!1)) =
       polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)
[-5]  1 - sq(z!1) > 0
  |-------
{1}   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        (polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1) +
          polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1))

Rerunning step: (hide -1 -2 -3 -4)
Hiding formulas:  -1, -2, -3, -4,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  1 - sq(z!1) > 0
  |-------
[1]   polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2 =
       factorial(2 + 2 * n!1) *
        (polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1) +
          polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1))

Rerunning step: (expand "polynomial")
Expanding the definition of polynomial,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  1 - sq(z!1) > 0
  |-------
{1}   2 *
       sigma(0, 2 + 2 * n!1,
             LAMBDA (i: nat):
               atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (lemma "sigma_scal[nat]"
                 ("low" "0" "high" "2+2*n!1" "a" "2" "F"
                  "LAMBDA (i: nat):
               atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF)"))
Free variables in expr i
Applying sigma_scal[nat] where
  low gets 0,
  high gets 2 + 2 * n!1,
  a gets 2,
  F gets LAMBDA (i: nat):
           atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF),
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

{-1}  sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       2 *
        sigma(0, 2 + 2 * n!1,
              LAMBDA (i: nat):
                atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
[-2]  1 - sq(z!1) > 0
  |-------
[1]   2 *
       sigma(0, 2 + 2 * n!1,
             LAMBDA (i: nat):
               atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (replace -1 1 rl)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       2 *
        sigma(0, 2 + 2 * n!1,
              LAMBDA (i: nat):
                atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
[-2]  1 - sq(z!1) > 0
  |-------
{1}   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  1 - sq(z!1) > 0
  |-------
[1]   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (lemma "sigma_scal[nat]"
                 ("low" "0" "high" "3+2*n!1" "a"
                  "factorial(2 + 2 * n!1)" "F"
                  "LAMBDA (i: nat):power_fs(3 + 2 * n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF)"))
Free variables in expr i
Ignoring 1 repeated TCCs.
Applying sigma_scal[nat] where
  low gets 0,
  high gets 3 + 2 * n!1,
  a gets factorial(2 + 2 * n!1),
  F gets LAMBDA (i: nat):
           power_fs(3 + 2 * n!1)(i) *
            (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF),
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

{-1}  sigma(0, 3 + 2 * n!1,
            LAMBDA (i_1: nat):
              factorial(2 + 2 * n!1) *
               (LAMBDA (i: nat):
                  power_fs(3 + 2 * n!1)(i) *
                   (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
[-2]  1 - sq(z!1) > 0
  |-------
[1]   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (replace -1 1 rl)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  sigma(0, 3 + 2 * n!1,
            LAMBDA (i_1: nat):
              factorial(2 + 2 * n!1) *
               (LAMBDA (i: nat):
                  power_fs(3 + 2 * n!1)(i) *
                   (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
[-2]  1 - sq(z!1) > 0
  |-------
{1}   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i_1))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  1 - sq(z!1) > 0
  |-------
[1]   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i_1))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (lemma "sigma_scal[nat]"
                 ("low" "0" "high" "3+2*n!1" "a"
                  "factorial(2 + 2 * n!1)" "F"
                  "LAMBDA (i: nat):neg_power_fs(3 + 2 * n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF)"))
Free variables in expr i
Ignoring 1 repeated TCCs.
Applying sigma_scal[nat] where
  low gets 0,
  high gets 3 + 2 * n!1,
  a gets factorial(2 + 2 * n!1),
  F gets LAMBDA (i: nat):
           neg_power_fs(3 + 2 * n!1)(i) *
            (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF),
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

{-1}  sigma(0, 3 + 2 * n!1,
            LAMBDA (i_1: nat):
              factorial(2 + 2 * n!1) *
               (LAMBDA (i: nat):
                  neg_power_fs(3 + 2 * n!1)(i) *
                   (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                neg_power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
[-2]  1 - sq(z!1) > 0
  |-------
[1]   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i_1))
        +
        factorial(2 + 2 * n!1) *
         sigma(0, 3 + 2 * n!1,
               LAMBDA (i: nat):
                 neg_power_fs(3 + 2 * n!1)(i) *
                  (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))

Rerunning step: (replace -1 1 rl)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  sigma(0, 3 + 2 * n!1,
            LAMBDA (i_1: nat):
              factorial(2 + 2 * n!1) *
               (LAMBDA (i: nat):
                  neg_power_fs(3 + 2 * n!1)(i) *
                   (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       factorial(2 + 2 * n!1) *
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i: nat):
                neg_power_fs(3 + 2 * n!1)(i) *
                 (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
[-2]  1 - sq(z!1) > 0
  |-------
{1}   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i_1))
        +
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i_1: nat):
                factorial(2 + 2 * n!1) *
                 (LAMBDA (i: nat):
                    neg_power_fs(3 + 2 * n!1)(i) *
                     (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                     (i_1))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  1 - sq(z!1) > 0
  |-------
[1]   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i_1))
        +
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i_1: nat):
                factorial(2 + 2 * n!1) *
                 (LAMBDA (i: nat):
                    neg_power_fs(3 + 2 * n!1)(i) *
                     (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                     (i_1))

Rerunning step: (lemma "sigma_sum"
                 ("low" "0" "high" "3+2*n!1" "F" "LAMBDA (i: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))(i)" "G"
                  "LAMBDA (i: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   neg_power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))(i)"))
Free variables in expr i
Free variables in expr i
Applying sigma_sum where
  low gets 0,
  high gets 3 + 2 * n!1,
  F gets LAMBDA (i: nat):
           factorial(2 + 2 * n!1) *
            (LAMBDA (i: nat):
               power_fs(3 + 2 * n!1)(i) *
                (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                (i),
  G gets LAMBDA (i: nat):
           factorial(2 + 2 * n!1) *
            (LAMBDA (i: nat):
               neg_power_fs(3 + 2 * n!1)(i) *
                (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                (i),
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

{-1}  sigma(0, 3 + 2 * n!1,
            LAMBDA (i: nat):
              factorial(2 + 2 * n!1) *
               (LAMBDA (i: nat):
                  power_fs(3 + 2 * n!1)(i) *
                   (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i))
       +
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   neg_power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               (LAMBDA (i: nat):
                  factorial(2 + 2 * n!1) *
                   (LAMBDA (i: nat):
                      power_fs(3 + 2 * n!1)(i) *
                       (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                       (i))
                   (i_1)
                +
                (LAMBDA (i: nat):
                   factorial(2 + 2 * n!1) *
                    (LAMBDA (i: nat):
                       neg_power_fs(3 + 2 * n!1)(i) *
                        (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                        (i))
                    (i_1))
[-2]  1 - sq(z!1) > 0
  |-------
[1]   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i_1))
        +
        sigma(0, 3 + 2 * n!1,
              LAMBDA (i_1: nat):
                factorial(2 + 2 * n!1) *
                 (LAMBDA (i: nat):
                    neg_power_fs(3 + 2 * n!1)(i) *
                     (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                     (i_1))

Rerunning step: (replace -1 1)
Replacing using formula -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  sigma(0, 3 + 2 * n!1,
            LAMBDA (i: nat):
              factorial(2 + 2 * n!1) *
               (LAMBDA (i: nat):
                  power_fs(3 + 2 * n!1)(i) *
                   (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i))
       +
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i: nat):
               factorial(2 + 2 * n!1) *
                (LAMBDA (i: nat):
                   neg_power_fs(3 + 2 * n!1)(i) *
                    (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                    (i))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               (LAMBDA (i: nat):
                  factorial(2 + 2 * n!1) *
                   (LAMBDA (i: nat):
                      power_fs(3 + 2 * n!1)(i) *
                       (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                       (i))
                   (i_1)
                +
                (LAMBDA (i: nat):
                   factorial(2 + 2 * n!1) *
                    (LAMBDA (i: nat):
                       neg_power_fs(3 + 2 * n!1)(i) *
                        (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                        (i))
                    (i_1))
[-2]  1 - sq(z!1) > 0
  |-------
{1}   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               (LAMBDA (i: nat):
                  factorial(2 + 2 * n!1) *
                   (LAMBDA (i: nat):
                      power_fs(3 + 2 * n!1)(i) *
                       (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                       (i))
                   (i_1)
                +
                (LAMBDA (i: nat):
                   factorial(2 + 2 * n!1) *
                    (LAMBDA (i: nat):
                       neg_power_fs(3 + 2 * n!1)(i) *
                        (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                        (i))
                    (i_1))

Rerunning step: (hide -1)
Hiding formulas:  -1,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  1 - sq(z!1) > 0
  |-------
[1]   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (LAMBDA (i: nat):
                  atanhF(1 + n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                   (i_1))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               (LAMBDA (i: nat):
                  factorial(2 + 2 * n!1) *
                   (LAMBDA (i: nat):
                      power_fs(3 + 2 * n!1)(i) *
                       (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                       (i))
                   (i_1)
                +
                (LAMBDA (i: nat):
                   factorial(2 + 2 * n!1) *
                    (LAMBDA (i: nat):
                       neg_power_fs(3 + 2 * n!1)(i) *
                        (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))
                        (i))
                    (i_1))

Rerunning step: (simplify 1)
Simplifying with decision procedures,
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

[-1]  1 - sq(z!1) > 0
  |-------
{1}   sigma(0, 2 + 2 * n!1,
            LAMBDA (i_1: nat):
              2 *
               (atanhF(1 + n!1)(i_1) *
                 (IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF)))
       =
       sigma(0, 3 + 2 * n!1,
             LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (power_fs(3 + 2 * n!1)(i_1) *
                  (IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))
                +
                factorial(2 + 2 * n!1) *
                 (neg_power_fs(3 + 2 * n!1)(i_1) *
                   (IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF)))

Rerunning step: (lemma "sigma_last"
                 ("low" "0" "high" "3+2*n!1" "F" "LAMBDA (i_1: nat):
               factorial(2 + 2 * n!1) *
                (power_fs(3 + 2 * n!1)(i_1) *
                  (IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))
                +
                factorial(2 + 2 * n!1) *
                 (neg_power_fs(3 + 2 * n!1)(i_1) *
                   (IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))"))
Free variables in expr i_1
Free variables in expr i_1
Ignoring 1 repeated TCCs.
Applying sigma_last where
  low gets 0,
  high gets 3 + 2 * n!1,
  F gets LAMBDA (i_1: nat):
           factorial(2 + 2 * n!1) *
            (power_fs(3 + 2 * n!1)(i_1) *
              (IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))
            +
            factorial(2 + 2 * n!1) *
             (neg_power_fs(3 + 2 * n!1)(i_1) *
               (IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF)),
this simplifies to:
atanh_series.1.1.1.1.1.1.2.1.1.1 :

{-1}  3 + 2 * n!1 > 0 IMPLIES
       sigma(0, 3 + 2 * n!1,
--> --------------------

--> maximum size reached

--> --------------------