---

Step * of Lemma genfact-inv_wf

∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℕ+]. ∀[N:ℤ].  (genfact-inv(N;b;m.f[m]) ∈ {n:ℕ| N ≤ genfact(n;b;m.f[m])} ) supposing ∀m:ℕ+. 1 < f[m]
BY
{ (Auto
   THEN Fold `sq_exists` 0
   THEN (Subst' genfact-inv(N;b;m.f[m]) ~ TERMOF{genfact-unbounded-ext:o, \\v:l} f b N 0
         THENA (Computation THEN RepUR ``so_apply`` 0 THEN Auto)
         )
   THEN (GenConclAtAddr [2;1;1;1] THENA Auto)
   THEN (D -2 With ⌜f⌝  THENA Auto)
   THEN RenameVar `x' 2
   THEN D -2 With ⌜x⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[b:\mBbbN{}\msupplus{}].  \mforall{}[N:\mBbbZ{}].    (genfact-inv(N;b;m.f[m])  \mmember{}  \{n:\mBbbN{}|  N  \mleq{}  genfact(n;b;m.f[m])\}  )  supposin\000Cg  \mforall{}m:\mBbbN{}\msupplus{}.  1  <  f[m]


By

---

Latex:
(Auto
  THEN  Fold  `sq\_exists`  0
  THEN  (Subst'  genfact-inv(N;b;m.f[m])  \msim{}  TERMOF\{genfact-unbounded-ext:o,  \mbackslash{}\mbackslash{}v:l\}  f  b  N  0
              THENA  (Computation  THEN  RepUR  ``so\_apply``  0  THEN  Auto)
              )
  THEN  (GenConclAtAddr  [2;1;1;1]  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  RenameVar  `x'  2
  THEN  D  -2  With  \mkleeneopen{}x\mkleeneclose{} 
  THEN  Auto)

---

Home Index