---

Step * of Lemma Legendre-roots-rless

∀n:ℕ. ∀i,j:ℕn.  (i < j ⇒ (Legendre-root(n;i) < Legendre-root(n;j)))
BY
{ (Intros
   THEN Unfold `Legendre-root` 0
   THEN (Subst' primrec(n;λi.r0;λi,x. if i + 1=1
                                      then λi.r0
                                      else (λi@0.rational_fun_zero(λx.ratLegendre(i
                                                                      + 1;x);if i@0=0
                                                                             then r(-1)
                                                                             else (x (i@0 - 1));if i@0=(i + 1) - 1
                                                                                                then r1
                                                                                                else (x i@0)))) 
         ~ TERMOF{Legendre-roots-ext:o, \\v:l} n 0
         THENA (RW (AddrC [2] (TagC (mk_tag_term 2))) 0 THEN Auto)
         )
   THEN GenConclAtAddr [2;1]
   THEN Thin (-1)
   THEN D -1
   THEN (Unhide THEN Auto)
   THEN (InstLemma `sorted-seq-iff` [⌜ℝ⌝;⌜λ2x y.x < y⌝;⌜<n, v>⌝]⋅ THENA (Auto THEN D 0 THEN Reduce 0 THEN Auto))
   THEN (RepeatFor 2 (D -1) THENA (RepUR ``seq-len seq-item`` 0 THEN Trivial))
   THEN RepUR ``sorted-seq seq-len seq-item`` -1
   THEN BHyp -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}i,j:\mBbbN{}n.    (i  <  j  {}\mRightarrow{}  (Legendre-root(n;i)  <  Legendre-root(n;j)))


By

---

Latex:
(Intros
  THEN  Unfold  `Legendre-root`  0
  THEN  (Subst'  primrec(n;\mlambda{}i.r0;\mlambda{}i,x.  if  i  +  1=1
                                                                        then  \mlambda{}i.r0
                                                                        else  (\mlambda{}i@0.rational\_fun\_zero(\mlambda{}x.ratLegendre(i
                                                                                                                                        +  1;x);if  i@0=0
                                                                                                                                                      then  r(-1)
                                                                                                                                                      else  (x 
                                                                                                                                                                  (i@0 
                                                                                                                                                                  -  1));if  i@0=(i
                                                                                                                                                                              +  1)  -  1
                                                                                                                                                                              then  r1
                                                                                                                                                                              else  (x 
                                                                                                                                                                                          i@0))))\000C 
              \msim{}  TERMOF\{Legendre-roots-ext:o,  \mbackslash{}\mbackslash{}v:l\}  n  0
              THENA  (RW  (AddrC  [2]  (TagC  (mk\_tag\_term  2)))  0  THEN  Auto)
              )
  THEN  GenConclAtAddr  [2;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (Unhide  THEN  Auto)
  THEN  (InstLemma  `sorted-seq-iff`  [\mkleeneopen{}\mBbbR{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  <  y\mkleeneclose{};\mkleeneopen{}<n,  v>\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto)
              )
  THEN  (RepeatFor  2  (D  -1)  THENA  (RepUR  ``seq-len  seq-item``  0  THEN  Trivial))
  THEN  RepUR  ``sorted-seq  seq-len  seq-item``  -1
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index