---

Step * of Lemma Legendre-sign-changes-ext

∀n:ℕ. ∃L:(ℤ × ℕ+) List [((||L|| = (n - 1) ∈ ℤ) ∧ rat-sign-change-list(λx.ratLegendre(n;x);<-1, 1>;<1, 1>;L))] supposing \000C0 < n
BY
{ Extract of Obid: Legendre-sign-changes
  not unfolding  primrec ratLegendre ratsign find_rational eval-mklist select  exp nil
  finishing with (Unfold `Legendre_changes` 0
                  THEN RepUR ``let subtract`` 0
                  THEN Repeat (If (\p. opid_of_term (subtermn 1 (concl p)) = `add`) Trivial EqCD)
                  THEN Try (Complete ((RWW "add-associates" 0 THEN Auto)))
                  THEN Try (((Subst' ((n@0 + 1) + (-1)) + (-i) ~ (n@0 + 0) + (-i) 0
                              THENA (EqCD THEN RWW "add-associates" 0 THEN Auto)
                              )
                             THEN RWO  "zero-add-sq<" 0
                             THEN Auto)))
  normalizes to:
  
  λn.Legendre_changes(n) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  Legendre-sign-changes
not  unfolding    primrec  ratLegendre  ratsign  find\_rational  eval-mklist  select    exp  nil
finishing  with  (Unfold  `Legendre\_changes`  0
                                THEN  RepUR  ``let  subtract``  0
                                THEN  Repeat  (If  (\mbackslash{}p.  opid\_of\_term  (subtermn  1  (concl  p))  =  `add`)  Trivial  EqCD)
                                THEN  Try  (Complete  ((RWW  "add-associates"  0  THEN  Auto)))
                                THEN  Try  (((Subst'  ((n@0  +  1)  +  (-1))  +  (-i)  \msim{}  (n@0  +  0)  +  (-i)  0
                                                        THENA  (EqCD  THEN  RWW  "add-associates"  0  THEN  Auto)
                                                        )
                                                      THEN  RWO    "zero-add-sq<"  0
                                                      THEN  Auto)))
normalizes  to:

\mlambda{}n.Legendre\_changes(n)

---

Home Index