---

Step * of Lemma simple_general_fan_theorem-ext

∀[T:Type]
  (Bounded(T)
  ⇒ (∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]
        (∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ T. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ T. (↓∃n:ℕ. X[n;f])))
BY
{ Extract of Obid: simple_general_fan_theorem
  not unfolding  bar_recursion
  finishing with (RepeatFor 4 (EqCD) THEN Try (Trivial) THEN Try (Fold `bottom` 0) THEN SqReasoning)
  normalizes to:
  
  λmax,d. bar_recursion(d;λn,s,f. 1;λn,s,f. ((max (λt.(f t))) + 1);0;λm.eval x = m in ⊥) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    (Bounded(T)
    {}\mRightarrow{}  (\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}]
                (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}  [(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}k.  X[n;f])]) 
                supposing  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])))


By

---

Latex:
Extract  of  Obid:  simple\_general\_fan\_theorem
not  unfolding    bar\_recursion
finishing  with  (RepeatFor  4  (EqCD)  THEN  Try  (Trivial)  THEN  Try  (Fold  `bottom`  0)  THEN  SqReasoning)
normalizes  to:

\mlambda{}max,d.  bar\_recursion(d;\mlambda{}n,s,f.  1;\mlambda{}n,s,f.  ((max  (\mlambda{}t.(f  t)))  +  1);0;\mlambda{}m.eval  x  =  m  in  \mbot{})

---

Home Index