---

Step * 1 1 1 of Lemma list-if-has-value-list_ind


1. b : Base@i
2. f : Base@i
3. ∀x:Base. strict(λu.f[x;u])
4. j : ℤ
5. 0 < j
6. ∀l:Base
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let a,b = v 
                                        in f[a;list_ind b] otherwise if v = Ax then b otherwise ⊥^j - 1 
       ⊥ 
       l)↓
     ⇒ (l ∈ Base List))
7. l : Base@i
8. (f[fst(l);λlist_ind,L. eval v = L in
                          if v is a pair then let a,b = v 
                                              in f[a;list_ind b] otherwise if v = Ax then b otherwise ⊥^j - 1 
             ⊥ 
             (snd(l))])↓@i
9. 0 ≤ 0
10. l ~ <fst(l), snd(l)>
11. ∀x:Base. (((λu.f[fst(l);u]) x)↓ ⇒ (x)↓)
12. ∀u,v:Base.  ((λu.f[fst(l);u]) (exception(u; v)) ~ exception(u; v))
13. ∀z:Base. (is-exception((λu.f[fst(l);u]) z) ⇒ is-exception(z))
⊢ (λlist_ind,L. eval v = L in if v is a pair then let a,b = v in f[a;list_ind b] otherwise if v = Ax then b otherwise ⊥^\000Cj - 1 ⊥ 
   (snd(l)))↓
BY
{ (All Reduce THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  Base@i
2.  f  :  Base@i
3.  \mforall{}x:Base.  strict(\mlambda{}u.f[x;u])
4.  j  :  \mBbbZ{}
5.  0  <  j
6.  \mforall{}l:Base
          ((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  a,b  =  v 
                                                                              in  f[a;list$_{ind}$  b]  otherwise  if  v  =  A\000Cx  then  b  otherwise  \mbot{}\^{}j  -  1 
              \mbot{} 
              l)\mdownarrow{}
          {}\mRightarrow{}  (l  \mmember{}  Base  List))
7.  l  :  Base@i
8.  (f[fst(l);\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                  if  v  is  a  pair  then  let  a,b  =  v 
                                                                                          in  f[a;list$_{ind}$  b]
                                                  otherwise  if  v  =  Ax  then  b  otherwise  \mbot{}\^{}j  -  1 
                          \mbot{} 
                          (snd(l))])\mdownarrow{}@i
9.  0  \mleq{}  0
10.  l  \msim{}  <fst(l),  snd(l)>
11.  \mforall{}x:Base.  (((\mlambda{}u.f[fst(l);u])  x)\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{})
12.  \mforall{}u,v:Base.    ((\mlambda{}u.f[fst(l);u])  (exception(u;  v))  \msim{}  exception(u;  v))
13.  \mforall{}z:Base.  (is-exception((\mlambda{}u.f[fst(l);u])  z)  {}\mRightarrow{}  is-exception(z))
\mvdash{}  (\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                              if  v  is  a  pair  then  let  a,b  =  v 
                                                                      in  f[a;list$_{ind}$  b]  otherwise  if  v  =  Ax  th\000Cen  b  otherwise  \mbot{}\^{}j  -  1 
      \mbot{} 
      (snd(l)))\mdownarrow{}


By

---

Latex:
(All  Reduce  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index