---

Step * 3 1 1 1 2 of Lemma not-bl-exists-eq-bl-all


1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
     (¬b(λ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 ⊥^j - 1 
         ⊥ 
         L) ≤ fix((λ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 ⊥)) 
              L)
4. P : Base@i
5. L : Base@i
6. is-exception(case P[fst(L)]
                     ∨b(λ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 ⊥^j - 1 
                        ⊥ 
                        (snd(L)))
 of inl() =>
 ff
 | inr() =>
 tt)
7. is-exception(case P[fst(L)]
 of inl() =>
 tt
 | inr() =>
 λ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 ⊥^j - 1 
 ⊥ 
 (snd(L)))
8. 0 ≤ 0
9. L ~ <fst(L), snd(L)>
10. is-exception(P[fst(L)])
⊢ ¬b(P[fst(L)]
  ∨b(λ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 ⊥^j - 1 
     ⊥ 
     (snd(L)))) ≤ (¬bP[fst(L)])
  ∧b (fix((λ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 ⊥)) 
      (snd(L)))
BY
{ ComputeSameException 200 }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}P,L:Base.
          (\mneg{}\msubb{}(\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{}\^{}j  -  1 
                  \mbot{} 
                  L)  \mleq{}  fix((\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}$  \000Cas')
                                                              otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{})) 
                            L)
4.  P  :  Base@i
5.  L  :  Base@i
6.  is-exception(case  P[fst(L)]
                                          \mvee{}\msubb{}(\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}$  \000Cas')
                                                                        otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{}\^{}j  -  1 
                                                \mbot{} 
                                                (snd(L)))
  of  inl()  =>
  ff
  |  inr()  =>
  tt)
7.  is-exception(case  P[fst(L)]
  of  inl()  =>
  tt
  |  inr()  =>
  \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  =  A\000Cx  then  ff  otherwise  \mbot{}\^{}j  -  1 
  \mbot{} 
  (snd(L)))
8.  0  \mleq{}  0
9.  L  \msim{}  <fst(L),  snd(L)>
10.  is-exception(P[fst(L)])
\mvdash{}  \mneg{}\msubb{}(P[fst(L)]
    \mvee{}\msubb{}(\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\000C  =  Ax  then  ff  otherwise  \mbot{}\^{}j  -  1 
          \mbot{} 
          (snd(L))))  \mleq{}  (\mneg{}\msubb{}P[fst(L)])
    \mwedge{}\msubb{}  (fix((\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{})) 
            (snd(L)))


By

---

Latex:
ComputeSameException  200

---

Home Index