Step
*
3
1
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 eval v = L in
                     if v is a pair then let a,as' = v 
                                         in P[a]
                                            ∨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 
                                               ⊥ 
                                               as') otherwise if v = Ax then ff otherwise ⊥
 of inl() =>
 ff
 | inr() =>
 tt)
7. is-exception(eval v = L in
                if v is a pair then let a,as' = v 
                                    in P[a]
                                       ∨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 
                                          ⊥ 
                                          as') otherwise if v = Ax then ff otherwise ⊥)
8. (L)↓
⊢ ¬beval v = L in
    if v is a pair then let a,as' = v 
                        in P[a]
                           ∨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 
                              ⊥ 
                              as') otherwise if v = Ax then ff otherwise ⊥ ≤ 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
BY
{ ((RW (AddrC [2] UnrollLoopsC) 0 THEN Reduce 0) THEN (CallByValueReduceOn ⌜L⌝ 0⋅ THENA Auto)) }
1
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 eval v = L in
                     if v is a pair then let a,as' = v 
                                         in P[a]
                                            ∨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 
                                               ⊥ 
                                               as') otherwise if v = Ax then ff otherwise ⊥
 of inl() =>
 ff
 | inr() =>
 tt)
7. is-exception(eval v = L in
                if v is a pair then let a,as' = v 
                                    in P[a]
                                       ∨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 
                                          ⊥ 
                                          as') otherwise if v = Ax then ff otherwise ⊥)
8. (L)↓
⊢ ¬bif L is a pair then let a,as' = L 
                        in P[a]
                           ∨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 
                              ⊥ 
                              as') otherwise if L = Ax then ff otherwise ⊥ 
  ≤ if L is a pair then let a,as' = L 
                        in (¬bP[a])
                           ∧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 ⊥)) 
                               as') otherwise if L = Ax then tt otherwise ⊥
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  eval  v  =  L  in
                                          if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                  in  P[a]
                                                                                        \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$_\mbackslash{}\000Cff7bind}$  as')
                                                                                                                      otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{}\^{}j\000C  -  1 
                                                                                              \mbot{} 
                                                                                              as')  otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{}
  of  inl()  =>
  ff
  |  inr()  =>
  tt)
7.  is-exception(eval  v  =  L  in
                                if  v  is  a  pair  then  let  a,as'  =  v 
                                                                        in  P[a]
                                                                              \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$_\mbackslash{}\000Cff7bind}$  as')
                                                                                                            otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{}\^{}j  -  1 
                                                                                    \mbot{} 
                                                                                    as')  otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{})
8.  (L)\mdownarrow{}
\mvdash{}  \mneg{}\msubb{}eval  v  =  L  in
        if  v  is  a  pair  then  let  a,as'  =  v 
                                                in  P[a]
                                                      \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}\000C$  as')
                                                                                    otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{}\^{}j  -  1 
                                                            \mbot{} 
                                                            as')  otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{} 
    \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}$  as')
                                          otherwise  if  v  =  Ax  then  tt  otherwise  \mbot{})) 
        L
By
Latex:
((RW  (AddrC  [2]  UnrollLoopsC)  0  THEN  Reduce  0)  THEN  (CallByValueReduceOn  \mkleeneopen{}L\mkleeneclose{}  0\mcdot{}  THENA  Auto))
Home
Index