---

Step * of Lemma filter-map

∀[f,Q,L:Top].  (filter(Q;map(f;L)) ~ map(f;filter(Q o f;L)))
BY
{ (RepUR ``filter map reduce`` 0
   THEN MutualFixpointInduction1 `L'
   THEN Reduce 0
   THEN RW (SubC (TryC RecUnfoldTopAbC)) 0
   THEN RW (AddrC [2;1] (RecUnfoldTopAbC)) 0
   THEN RW (SubC (LiftC true)) 0
   THEN UseCbvSqle
   THEN RW (SubC (LiftC true)) 0
   THEN HVimplies2 0 [1]
   THEN Try (((RWO "-1" 0 THENA MemTop)
              THEN UseCbvSqle
              THEN HasValueD (-1)
              THEN HVimplies2 0 [1;1]
              THEN (RWO "-1" 0 THENA Auto)
              THEN Strictness))) }

1
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 h,t = v 
                                                in [f h / (list_ind t)] otherwise if v = Ax then [] otherwise ⊥^j - 1 
               ⊥ 
               L) of
      [] => []
      a::as' =>
       r.if Q a then [a / r] else r fi  ≤ rec-case(rec-case(L) of
                                                   [] => []
                                                   a::as' =>
                                                    r.if Q (f a) then [a / r] else r fi ) of
                                          [] => []
                                          h::t =>
                                           r.[f h / r])
4. Q : Base@i
5. f : Base@i
6. L : Base@i
7. 0 ≤ 0@i
8. L ~ <fst(L), snd(L)>
⊢ if Q (f (fst(L)))
  then [f (fst(L)) / 
        rec-case(λlist_ind,L. eval v = L in
                              if v is a pair then let h,t = v 
                                                  in [f h / (list_ind t)] otherwise if v = Ax then [] otherwise ⊥^j - 1 
                 ⊥ 
                 (snd(L))) of
        [] => []
        h::t =>
         r.if Q h then [h / r] else r fi ]
  else rec-case(λlist_ind,L. eval v = L in
                             if v is a pair then let h,t = v 
                                                 in [f h / (list_ind t)] otherwise if v = Ax then [] otherwise ⊥^j - 1 
                ⊥ 
                (snd(L))) of
       [] => []
       h::t =>
        r.if Q h then [h / r] else r fi 
  fi  ≤ eval v = if Q (f (fst(L)))
        then [fst(L) / rec-case(snd(L)) of [] => [] | h::t => r.if Q (f h) then [h / r] else r fi ]
        else rec-case(snd(L)) of
             [] => []
             h::t =>
              r.if Q (f h) then [h / r] else r fi 
        fi  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 ⊥

2
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 = if Q (f (fst(L)))
  then [fst(L) / 
        (λ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)))]
  else λ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))
  fi  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 ⊥ 
  ≤ if Q (f (fst(L)))
  then [f (fst(L)) / 
        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 ]
  else 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 
  fi 

---

Latex:

---

Latex:
\mforall{}[f,Q,L:Top].    (filter(Q;map(f;L))  \msim{}  map(f;filter(Q  o  f;L)))


By

---

Latex:
(RepUR  ``filter  map  reduce``  0
  THEN  MutualFixpointInduction1  `L'
  THEN  Reduce  0
  THEN  RW  (SubC  (TryC  RecUnfoldTopAbC))  0
  THEN  RW  (AddrC  [2;1]  (RecUnfoldTopAbC))  0
  THEN  RW  (SubC  (LiftC  true))  0
  THEN  UseCbvSqle
  THEN  RW  (SubC  (LiftC  true))  0
  THEN  HVimplies2  0  [1]
  THEN  Try  (((RWO  "-1"  0  THENA  MemTop)
                        THEN  UseCbvSqle
                        THEN  HasValueD  (-1)
                        THEN  HVimplies2  0  [1;1]
                        THEN  (RWO  "-1"  0  THENA  Auto)
                        THEN  Strictness)))

---

Home Index