---

Step * of Lemma fan-realizer_wf

No Annotations
fan-realizer ∈ ∀[X:(𝔹 List) ⟶ ℙ]. (tbar(𝔹;X) ⇒ Decidable(X) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))))
BY
{ (EqualsNormalizedExtract (ioid Obid: fan-theorem) 100 ``bar_recursion int_seg_decide upto map imax bfalse btrue outl``
   ⋅
   THEN Unfolds ``uall implies fan-realizer`` 0
   THEN (EqTypeCD THENA Auto)
   THEN RepeatFor 2 ((EqCD THENA Auto)⋅)
   THEN (Assert λm.if (m) < (0)  then ⊥  else ⊥ ~ λm.eval x = m in
                                                     ⊥ BY
               (All Thin
                THEN EqCD
                THEN SqReasoning
                THEN (Assert exception(u; v) ≤ ⊥ BY
                            (RevHypSubst' (-1) 0 THEN Auto))
                THEN FLemma `exception-not-bottom` [-1]
                THEN Auto))
   THEN HypSubst' (-1) 0
   THEN HypSubst' (-1) 1
   THEN (RW (AddrC [2] (CallByValueC)) 0 THENM Fold `member` 0)) }

1
.....aux..... 
1. λ%,%1. <bar_recursion(λn,s. (%1 map(s;upto(n)));
                         λn,s,%2. 1;
                         λn,s,%2. eval a = %2 tt in eval b = %2 ff in   if (a) < (b)  then 1 + b  else (1 + a);
                         0;λm.eval x = m in
                              ⊥)
          , λf.outl(int_seg_decide(λn.(%1 map(f;upto(n)));0;bar_recursion(λn,s. (%1 map(s;upto(n)));
                                                                          λn,s,%2. 1;
                                                                          λn,s,%2. eval a = %2 tt in
                                                                                   eval b = %2 ff in
                                                                                     if (a) < (b)
                                                                                        then 1 + b
                                                                                        else (1 + a);
                                                                          0;λm.eval x = m in
                                                                               ⊥)))
          > ∈ ∀[X:(𝔹 List) ⟶ ℙ]. (tbar(𝔹;X) ⇒ Decidable(X) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))))
2. X : (𝔹 List) ⟶ ℙ
3. bar : tbar(𝔹;X)
4. d : Decidable(X)
5. λm.if (m) < (0)  then ⊥  else ⊥ ~ λm.eval x = m in
                                        ⊥
⊢ (bar_recursion(λn,s. (d map(s;upto(n)));
                 λ_,__,___. 1;
                 λ_,__,e. eval a = e tt in eval b = e ff in   if (a) < (b)  then 1 + b  else (1 + a);
                 0;λm.eval x = m in
                      ⊥))↓

2
1. λ%,%1. <bar_recursion(λn,s. (%1 map(s;upto(n)));
                         λn,s,%2. 1;
                         λn,s,%2. eval a = %2 tt in eval b = %2 ff in   if (a) < (b)  then 1 + b  else (1 + a);
                         0;λm.eval x = m in
                              ⊥)
          , λf.outl(int_seg_decide(λn.(%1 map(f;upto(n)));0;bar_recursion(λn,s. (%1 map(s;upto(n)));
                                                                          λn,s,%2. 1;
                                                                          λn,s,%2. eval a = %2 tt in
                                                                                   eval b = %2 ff in
                                                                                     if (a) < (b)
                                                                                        then 1 + b
                                                                                        else (1 + a);
                                                                          0;λm.eval x = m in
                                                                               ⊥)))
          > ∈ ∀[X:(𝔹 List) ⟶ ℙ]. (tbar(𝔹;X) ⇒ Decidable(X) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))))
2. X : (𝔹 List) ⟶ ℙ
3. bar : tbar(𝔹;X)
4. d : Decidable(X)
5. λm.if (m) < (0)  then ⊥  else ⊥ ~ λm.eval x = m in
                                        ⊥
⊢ <bar_recursion(λn,s. (d map(s;upto(n)));
                 λn,s,%2. 1;
                 λn,s,%2. eval a = %2 tt in eval b = %2 ff in   if (a) < (b)  then 1 + b  else (1 + a);
                 0;λm.eval x = m in
                      ⊥)
  , λf.outl(int_seg_decide(λn.(d map(f;upto(n)));0;bar_recursion(λn,s. (d map(s;upto(n)));
                                                                 λn,s,%2. 1;
                                                                 λn,s,%2. eval a = %2 tt in
                                                                          eval b = %2 ff in
                                                                            if (a) < (b)  then 1 + b  else (1 + a);
                                                                 0;λm.eval x = m in
                                                                      ⊥)))
  > ∈ ∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))

---

Latex:

---

Latex:
No  Annotations
fan-realizer  \mmember{}  \mforall{}[X:(\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}]
                                  (tbar(\mBbbB{};X)  {}\mRightarrow{}  Decidable(X)  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  (X  map(f;upto(n)))))


By

---

Latex:
(EqualsNormalizedExtract  (ioid  Obid:  fan-theorem
  )  100  ``bar\_recursion  int\_seg\_decide  upto  map  imax  bfalse  btrue  outl``\mcdot{}
  THEN  Unfolds  ``uall  implies  fan-realizer``  0
  THEN  (EqTypeCD  THENA  Auto)
  THEN  RepeatFor  2  ((EqCD  THENA  Auto)\mcdot{})
  THEN  (Assert  \mlambda{}m.if  (m)  <  (0)    then  \mbot{}    else  \mbot{}  \msim{}  \mlambda{}m.eval  x  =  m  in
                                                                                                      \mbot{}  BY
                          (All  Thin
                            THEN  EqCD
                            THEN  SqReasoning
                            THEN  (Assert  exception(u;  v)  \mleq{}  \mbot{}  BY
                                                    (RevHypSubst'  (-1)  0  THEN  Auto))
                            THEN  FLemma  `exception-not-bottom`  [-1]
                            THEN  Auto))
  THEN  HypSubst'  (-1)  0
  THEN  HypSubst'  (-1)  1
  THEN  (RW  (AddrC  [2]  (CallByValueC))  0  THENM  Fold  `member`  0))

---

Home Index