---

Step * 5 1 2 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. is-exception(¬bP[fst(L)])
⊢ (¬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
{ (RW (AddrC [2] UnrollLoopsC) 0 THEN Reduce 0) }

1
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. is-exception(¬bP[fst(L)])
⊢ (¬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(P[fst(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 ⊥)) 
     (snd(L))))

---

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.  is-exception(\mneg{}\msubb{}P[fst(L)])
\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:
(RW  (AddrC  [2]  UnrollLoopsC)  0  THEN  Reduce  0)

---

Home Index