---

Step * 2 1 of Lemma rinv_wf


1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ eval n = mu-ge(λn.4 <z |x n|;1) in
  if (n =z 1)
  then accelerate(5;reg-seq-inv(x))
  else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;x)))
  fi  ∈ ℝ
BY
{ ((Assert ∃n:{1...}. (↑4 <z |x n|) BY
          (ExRepD THEN With ⌜n⌝ (D 0)⋅ THEN Auto))
   THEN (InstLemma `mu-ge-property` [⌜1⌝;⌜λn.4 <z |x n|⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜mu-ge(λn.4 <z |x n|;1)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (Thin 2)
   THEN RenameVar `a' 2
   THEN (D 0 THENA Auto)
   THEN (D -1 THEN (RW assert_pushdownC (-2) THENA Auto))
   THEN ((Assert ∀[i:ℕ+a]. (¬4 < |x i|) BY (ParallelLast THEN RW assert_pushdownC (-1) THEN Auto)) THEN Thin (-2))
   THEN InstLemma `rnonzero-lemma1` [⌜x⌝;⌜a⌝]⋅
   THEN Auto)⋅ }

1
1. x : ℝ
2. a : {1...}
3. mu-ge(λn.4 <z |x n|;1) = a ∈ {1...}
4. 4 < |x a|
5. ∀[i:ℕ+a]. (¬4 < |x i|)
6. ∀m:ℕ+. ((a ≤ m) ⇒ (m ≤ (a * |x m|)))
7. a = 1 ∈ ℤ
⊢ reg-seq-inv(x) ∈ {f:ℕ+ ⟶ ℤ| 5-regular-seq(f)} 

2
1. x : ℝ
2. a : {2...}
3. mu-ge(λn.4 <z |x n|;1) = a ∈ {1...}
4. 4 < |x a|
5. ∀[i:ℕ+a]. (¬4 < |x i|)
6. ∀m:ℕ+. ((a ≤ m) ⇒ (m ≤ (a * |x m|)))
⊢ reg-seq-inv(reg-seq-adjust(a;x)) ∈ {f:ℕ+ ⟶ ℤ| 4 * ((4 * a * a) + 1)-regular-seq(f)} 

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  \mexists{}n:\mBbbN{}\msupplus{}.  4  <  |x  n|
\mvdash{}  eval  n  =  mu-ge(\mlambda{}n.4  <z  |x  n|;1)  in
    if  (n  =\msubz{}  1)
    then  accelerate(5;reg-seq-inv(x))
    else  accelerate(4  *  ((4  *  n  *  n)  +  1);reg-seq-inv(reg-seq-adjust(n;x)))
    fi    \mmember{}  \mBbbR{}


By

---

Latex:
((Assert  \mexists{}n:\{1...\}.  (\muparrow{}4  <z  |x  n|)  BY
                (ExRepD  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `mu-ge-property`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}\mlambda{}n.4  <z  |x  n|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}mu-ge(\mlambda{}n.4  <z  |x  n|;1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (Thin  2)
  THEN  RenameVar  `a'  2
  THEN  (D  0  THENA  Auto)
  THEN  (D  -1  THEN  (RW  assert\_pushdownC  (-2)  THENA  Auto))
  THEN  ((Assert  \mforall{}[i:\mBbbN{}\msupplus{}a].  (\mneg{}4  <  |x  i|)  BY
                            (ParallelLast  THEN  RW  assert\_pushdownC  (-1)  THEN  Auto))
              THEN  Thin  (-2)
              )
  THEN  InstLemma  `rnonzero-lemma1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index