---

Step * 5 1 1 of Lemma not-bl-exists-eq-bl-all


1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
     (λlist_ind,L. eval v = L in
                   if v is a pair then let a,as' = v 
                                       in (¬bP[a]) ∧b (list_ind as') otherwise if v = Ax then tt otherwise ⊥^j - 1 
      ⊥ 
      L ≤ ¬b(fix((λlist_ind,L. eval v = L in
                               if v is a pair then let a,as' = v 
                                                   in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥)) 
             L))
4. P : Base@i
5. L : Base@i
6. is-exception(case ¬bP[fst(L)]
 of inl() =>
 λlist_ind,L. eval v = L in
              if v is a pair then let a,as' = v 
                                  in (¬bP[a]) ∧b (list_ind as') otherwise if v = Ax then tt otherwise ⊥^j - 1 
 ⊥ 
 (snd(L))
 | inr() =>
 ff)
7. 0 ≤ 0
8. L ~ <fst(L), snd(L)>
9. ¬bP[fst(L)] ∈ Top + Top
⊢ (¬bP[fst(L)])
  ∧b (λlist_ind,L. eval v = L in
                   if v is a pair then let a,as' = v 
                                       in (¬bP[a]) ∧b (list_ind as') otherwise if v = Ax then tt otherwise ⊥^j - 1 
      ⊥ 
      (snd(L))) ≤ ¬b(fix((λlist_ind,L. eval v = L in
                                       if v is a pair then let a,as' = v 
                                                           in P[a] ∨b(list_ind as')
                                       otherwise if v = Ax then ff otherwise ⊥)) 
                     <fst(L), snd(L)>)
BY
{ (GenerateHasValue [2] (-1)
   THEN HasValueD (-1)
   THEN RW (AddrC [2] UnrollLoopsC) 0
   THEN Reduce 0
   THEN InstEta (-1)
   THEN AllReduce
   THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}P,L:Base.
          (\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                    if  v  is  a  pair  then  let  a,as'  =  v 
                                                                            in  (\mneg{}\msubb{}P[a])  \mwedge{}\msubb{}  (list$_{ind}$  as')
                                    otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{}\^{}j  -  1 
            \mbot{} 
            L  \mleq{}  \mneg{}\msubb{}(fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                            if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                                    in  P[a]  \mvee{}\msubb{}(list$_{ind}$  as')
                                                            otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{})) 
                          L))
4.  P  :  Base@i
5.  L  :  Base@i
6.  is-exception(case  \mneg{}\msubb{}P[fst(L)]
  of  inl()  =>
  \mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                          if  v  is  a  pair  then  let  a,as'  =  v 
                                                                  in  (\mneg{}\msubb{}P[a])  \mwedge{}\msubb{}  (list$_{ind}$  as')
                          otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{}\^{}j  -  1 
  \mbot{} 
  (snd(L))
  |  inr()  =>
  ff)
7.  0  \mleq{}  0
8.  L  \msim{}  <fst(L),  snd(L)>
9.  \mneg{}\msubb{}P[fst(L)]  \mmember{}  Top  +  Top
\mvdash{}  (\mneg{}\msubb{}P[fst(L)])
    \mwedge{}\msubb{}  (\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                    if  v  is  a  pair  then  let  a,as'  =  v 
                                                                            in  (\mneg{}\msubb{}P[a])  \mwedge{}\msubb{}  (list$_{ind}$  as')
                                    otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{}\^{}j  -  1 
            \mbot{} 
            (snd(L)))  \mleq{}  \mneg{}\msubb{}(fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                            if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                                                    in  P[a]  \mvee{}\msubb{}(list$_{ind}\mbackslash{}ff2\000C4  as')
                                                                            otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{})) 
                                          <fst(L),  snd(L)>)


By

---

Latex:
(GenerateHasValue  [2]  (-1)
  THEN  HasValueD  (-1)
  THEN  RW  (AddrC  [2]  UnrollLoopsC)  0
  THEN  Reduce  0
  THEN  InstEta  (-1)
  THEN  AllReduce
  THEN  Try  (Complete  (Auto)))

---

Home Index