---

Step * of Lemma Legendre_changes_wf

∀[n:ℕ+]
  (Legendre_changes(n) ∈ {L:(ℤ × ℕ+) List| (||L|| = (n - 1) ∈ ℤ) ∧ rat-sign-change-list(λx.ratLegendre(n;x);<-1, 1>;<1, \000C1>;L)} )
BY
{ (Intro
   THEN (Subst' Legendre_changes(n) ~ TERMOF{Legendre-sign-changes-ext:o, \\v:l} n 0 THENA (Computation THEN Auto))
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}]
    (Legendre\_changes(n)  \mmember{}  \{L:(\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  List| 
                                                    (||L||  =  (n  -  1))  \mwedge{}  rat-sign-change-list(\mlambda{}x.ratLegendre(n;x);<-1,  1>ə,  1\000C>L)\}  )


By

---

Latex:
(Intro
  THEN  (Subst'  Legendre\_changes(n)  \msim{}  TERMOF\{Legendre-sign-changes-ext:o,  \mbackslash{}\mbackslash{}v:l\}  n  0
              THENA  (Computation  THEN  Auto)
              )
  THEN  DoSubsume
  THEN  Auto)

---

Home Index