---

Step * 4 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. (if L is a pair then let a,as' = L 
                        in (¬bP[a])
                           ∧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 
                               ⊥ 
                               as') otherwise if L = Ax then tt otherwise ⊥)↓
7. (L)↓
⊢ if L is a pair then let a,as' = L 
                      in (¬bP[a])
                         ∧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 
                             ⊥ 
                             as') otherwise if L = Ax then tt otherwise ⊥ ≤ ¬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 ⊥))\000C 
                                                                               L)
BY
{ (Repeat (HVimplies2 0 [1])
   THEN BotDiv
   THEN Try (Complete ((RW UnrollLoopsC 0 THEN Reduce 0 THEN Auto)))
   THEN HasValueD (-3)
   THEN 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.  (if  L  is  a  pair  then  let  a,as'  =  L 
                                                in  (\mneg{}\msubb{}P[a])
                                                      \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$_{in\000Cd}$  as')
                                                                                      otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{}\^{}j  -  1 
                                                              \mbot{} 
                                                              as')  otherwise  if  L  =  Ax  then  tt  otherwise  \mbot{})\mdownarrow{}
7.  (L)\mdownarrow{}
\mvdash{}  if  L  is  a  pair  then  let  a,as'  =  L 
                                            in  (\mneg{}\msubb{}P[a])
                                                  \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\mbackslash{}\000Cff7d$  as')
                                                                                  otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{}\^{}j  -  1 
                                                          \mbot{} 
                                                          as')  otherwise  if  L  =  Ax  then  tt  otherwise  \mbot{} 
    \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)


By

---

Latex:
(Repeat  (HVimplies2  0  [1])
  THEN  BotDiv
  THEN  Try  (Complete  ((RW  UnrollLoopsC  0  THEN  Reduce  0  THEN  Auto)))
  THEN  HasValueD  (-3)
  THEN  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