---

Step * 1 of Lemma fan-realizer_wf

.....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
                      ⊥))↓
BY
{ ((Subst' 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
                              ⊥) ~ fst(((λ%,%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
                                                                                                ⊥)))
                           >) 
                   bar 
                   d)) 0
    THENA (Reduce 0 THEN Trivial)
    )
   THEN GenConclAtAddr [1;1;1;1]
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  \mlambda{}\%,\%1.  <bar\_recursion(\mlambda{}n,s.  (\%1  map(s;upto(n)));
                                                  \mlambda{}n,s,\%2.  1;
                                                  \mlambda{}n,s,\%2.  eval  a  =  \%2  tt  in
                                                                    eval  b  =  \%2  ff  in
                                                                        if  (a)  <  (b)    then  1  +  b    else  (1  +  a);
                                                  0;\mlambda{}m.eval  x  =  m  in
                                                            \mbot{})
                    ,  \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(\%1  map(f;upto(n)));0;bar\_recursion(\mlambda{}n,s.  (\%1  map(s;upto(n)));
                                                                                                                                                    \mlambda{}n,s,\%2.  1;
                                                                                                                                                    \mlambda{}n,s,\%2.  eval  a  =  \%2  tt  in
                                                                                                                                                                      eval  b  =  \%2  ff  in
                                                                                                                                                                          if  (a)  <  (b)
                                                                                                                                                                                then  1  +  b
                                                                                                                                                                                else  (1  +  a)\000C;
                                                                                                                                                    0;\mlambda{}m.eval  x  =  m  in
                                                                                                                                                              \mbot{})))
                    >  \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)))))
2.  X  :  (\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
3.  bar  :  tbar(\mBbbB{};X)
4.  d  :  Decidable(X)
5.  \mlambda{}m.if  (m)  <  (0)    then  \mbot{}    else  \mbot{}  \msim{}  \mlambda{}m.eval  x  =  m  in
                                                                                \mbot{}
\mvdash{}  (bar\_recursion(\mlambda{}n,s.  (d  map(s;upto(n)));
                                  \mlambda{}$_{}$,\_$_{}$,\_\_$_{}$.  \000C1;
                                  \mlambda{}$_{}$,\_$_{}$,e.  eval  a  =  e  tt  in  eval  b  =  \000Ce  ff  in      if  (a)  <  (b)    then  1  +  b    else  (1  +  a);
                                  0;\mlambda{}m.eval  x  =  m  in
                                            \mbot{}))\mdownarrow{}


By

---

Latex:
((Subst'  bar\_recursion(\mlambda{}n,s.  (d  map(s;upto(n)));
                                              \mlambda{}$_{}$,\_$_{}$,\_\_$_{}\mbackslash{}\000Cff24.  1;
                                              \mlambda{}$_{}$,\_$_{}$,e.  eval  a  =  e  tt  in
                                                            eval  b  =  e  ff  in
                                                                if  (a)  <  (b)    then  1  +  b    else  (1  +  a);
                                              0;\mlambda{}m.eval  x  =  m  in
                                                        \mbot{}) 
    \msim{}  fst(((\mlambda{}\%,\%1.
                                <bar\_recursion(\mlambda{}n,s.  (\%1  map(s;upto(n)));
                                                              \mlambda{}n,s,\%2.  1;
                                                              \mlambda{}n,s,\%2.  eval  a  =  \%2  tt  in
                                                                                eval  b  =  \%2  ff  in
                                                                                    if  (a)  <  (b)    then  1  +  b    else  (1  +  a);
                                                              0;\mlambda{}m.eval  x  =  m  in
                                                                        \mbot{})
                                ,  \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(\%1 
                                                                                          map(f;
                                                                                                  upto(n)));0;bar\_recursion(\mlambda{}n,s.  (\%1  map(s;upto(n)))\000C;
                                                                                                                                                      \mlambda{}n,s,\%2.  1;
                                                                                                                                                      \mlambda{}n,s,\%2.  ...;
                                                                                                                                                      0;\mlambda{}m.eval  x  =  m  in
                                                                                                                                                                \mbot{})))
                                >) 
                  bar 
                  d))  0
    THENA  (Reduce  0  THEN  Trivial)
    )
  THEN  GenConclAtAddr  [1;1;1;1]
  THEN  Auto)

---

Home Index