---

Step * 2 1 of Lemma filter-map


1. j : ℤ
2. 0 < j
3. ∀Q,f,L:Base.
     (rec-case(λlist_ind,L. eval v = L in
                            if v is a pair then let a,as' = v 
                                                in if Q (f a) then [a / (list_ind as')] else list_ind as' fi 
                            otherwise if v = Ax then [] otherwise ⊥^j - 1 
               ⊥ 
               L) of
      [] => []
      h::t =>
       r.[f h / r] ≤ rec-case(rec-case(L) of
                              [] => []
                              h::t =>
                               r.[f h / r]) of
                     [] => []
                     a::as' =>
                      r.if Q a then [a / r] else r fi )
4. Q : Base@i
5. f : Base@i
6. L : Base@i
7. 0 ≤ 0@i
8. L ~ <fst(L), snd(L)>
⊢ eval v = λlist_ind,L. eval v = L in
                        if v is a pair then let a,as' = v 
                                            in if Q (f a) then [a / (list_ind as')] else list_ind as' fi 
                        otherwise if v = Ax then [] otherwise ⊥^j - 1 
           ⊥ 
           (snd(L)) in
  if v is a pair then let h,t = v 
                      in [f h / rec-case(t) of [] => [] | h::t => r.[f h / r]] otherwise if v = Ax then [] otherwise ⊥ 
  ≤ rec-case(rec-case(snd(L)) of
             [] => []
             h::t =>
              r.[f h / r]) of
    [] => []
    h::t =>
     r.if Q h then [h / r] else r fi 
BY
{ ((InstHyp [⌜Q⌝;⌜f⌝;⌜snd(L)⌝] 3⋅ THENA Auto) THEN RW (AddrC [1] RecUnfoldTopAbC) (-1) THEN NthHyp (-1)) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}Q,f,L:Base.
          (rec-case(\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                      if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                              in  if  Q  (f  a)
                                                                                                    then  [a  /  (list$_{ind}$  as')]
                                                                                                    else  list$_{ind}$  as'
                                                                                                    fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
                              \mbot{} 
                              L)  of
            []  =>  []
            h::t  =>
              r.[f  h  /  r]  \mleq{}  rec-case(rec-case(L)  of
                                                            []  =>  []
                                                            h::t  =>
                                                              r.[f  h  /  r])  of
                                          []  =>  []
                                          a::as'  =>
                                            r.if  Q  a  then  [a  /  r]  else  r  fi  )
4.  Q  :  Base@i
5.  f  :  Base@i
6.  L  :  Base@i
7.  0  \mleq{}  0@i
8.  L  \msim{}  <fst(L),  snd(L)>
\mvdash{}  eval  v  =  \mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                              if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                      in  if  Q  (f  a)
                                                                                            then  [a  /  (list$_{ind}$  as')]
                                                                                            else  list$_{ind}$  as'
                                                                                            fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
                      \mbot{} 
                      (snd(L))  in
    if  v  is  a  pair  then  let  h,t  =  v 
                                            in  [f  h  /  rec-case(t)  of  []  =>  []  |  h::t  =>  r.[f  h  /  r]]
    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}  \mleq{}  rec-case(rec-case(snd(L))  of
                                                                                                          []  =>  []
                                                                                                          h::t  =>
                                                                                                            r.[f  h  /  r])  of
                                                                                        []  =>  []
                                                                                        h::t  =>
                                                                                          r.if  Q  h  then  [h  /  r]  else  r  fi 


By

---

Latex:
((InstHyp  [\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}snd(L)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  (-1)
  THEN  NthHyp  (-1))

---

Home Index