Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
indexed_sets_extra.prf
Sprache: Lisp
Untersuchungsergebnis.proof Download desText {Text[113] Latech[139] Fortran[272]}zum Wurzelverzeichnis wechseln
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
--> --------------------
[ zur Elbe Produktseite wechseln0.327Quellennavigators
]
|
|
