---

Step * of Lemma filter-filter

∀[P1,P2,L:Top].  (filter(P2;filter(P1;L)) ~ filter(λt.((P1 t) ∧b (P2 t));L))
BY
{ (RepUR ``band filter reduce`` 0
   THEN MutualFixpointInduction1 `L'
   THEN Reduce 0
   THEN RW (SubC (TryC RecUnfoldTopAbC)) 0) }

1
1. j : ℤ
2. 0 < j
3. ∀P2,P1,L:Base.
     (rec-case(λlist_ind,L. eval v = L in
                            if v is a pair then let a,as' = v 
                                                in if P1 a then [a / (list_ind as')] else list_ind as' fi 
                            otherwise if v = Ax then [] otherwise ⊥^j - 1 
               ⊥ 
               L) of
      [] => []
      a::as' =>
       r.if P2 a then [a / r] else r fi  ≤ rec-case(L) of
                                           [] => []
                                           a::as' =>
                                            r.if if P1 a then P2 a else ff fi  then [a / r] else r fi )
4. P2 : Base
5. P1 : Base
6. L : Base
⊢ eval v = eval v = L in
           if v is a pair then let a,as' = v 
                               in if P1 a
                                  then [a / 
                                        (λlist_ind,L. eval v = L in
                                                      if v is a pair then let a,as' = v 
                                                                          in if P1 a
                                                                             then [a / (list_ind as')]
                                                                             else list_ind as'
                                                                             fi  otherwise if v = Ax then [] otherwise ⊥\000C^j - 1 
                                         ⊥ 
                                         as')]
                                  else λlist_ind,L. eval v = L in
                                                    if v is a pair then let a,as' = v 
                                                                        in if P1 a
                                                                           then [a / (list_ind as')]
                                                                           else list_ind as'
                                                                           fi  otherwise if v = Ax then [] otherwise ⊥^j\000C - 1 
                                       ⊥ 
                                       as'
                                  fi  otherwise if v = Ax then [] otherwise ⊥ in
  if v is a pair then let a,as' = v 
                      in if P2 a
                         then [a / rec-case(as') of [] => [] | h::t => r.if P2 h then [h / r] else r fi ]
                         else rec-case(as') of
                              [] => []
                              h::t =>
                               r.if P2 h then [h / r] else r fi 
                         fi  otherwise if v = Ax then [] otherwise ⊥ ≤ eval v = L in
                                                                       if v is a pair then let a,as' = v 
                                                                                           in if if P1 a
                                                                                                 then P2 a
                                                                                                 else ff
                                                                                                 fi 
                                                                                              then [a / 
                                                                                                    rec-case(as') of
                                                                                                    [] => []
                                                                                                    h::t =>
                                                                                                     r.if if P1 h
                                                                                                          then P2 h
                                                                                                          else ff
                                                                                                          fi 
                                                                                                    then [h / r]
                                                                                                    else r
                                                                                                    fi ]
                                                                                              else rec-case(as') of
                                                                                                   [] => []
                                                                                                   h::t =>
                                                                                                    r.if if P1 h
                                                                                                         then P2 h
                                                                                                         else ff
                                                                                                         fi 
                                                                                                   then [h / r]
                                                                                                   else r
                                                                                                   fi 
                                                                                              fi 
                                                                       otherwise if v = Ax then [] otherwise ⊥

2
1. j : ℤ
2. 0 < j
3. ∀P2,P1,L:Base.
     (λlist_ind,L. eval v = L in
                   if v is a pair then let a,as' = v 
                                       in if if P1 a then P2 a else ff fi 
                                          then [a / (list_ind as')]
                                          else list_ind as'
                                          fi  otherwise if v = Ax then [] otherwise ⊥^j - 1 
      ⊥ 
      L ≤ rec-case(rec-case(L) of
                   [] => []
                   a::as' =>
                    r.if P1 a then [a / r] else r fi ) of
          [] => []
          a::as' =>
           r.if P2 a then [a / r] else r fi )
4. P2 : Base
5. P1 : Base
6. L : Base
⊢ eval v = L in
  if v is a pair then let a,as' = v 
                      in if if P1 a then P2 a else ff fi 
                         then [a / 
                               (λlist_ind,L. eval v = L in
                                             if v is a pair then let a,as' = v 
                                                                 in if if P1 a then P2 a else ff fi 
                                                                    then [a / (list_ind as')]
                                                                    else list_ind as'
                                                                    fi  otherwise if v = Ax then [] otherwise ⊥^j - 1 
                                ⊥ 
                                as')]
                         else λlist_ind,L. eval v = L in
                                           if v is a pair then let a,as' = v 
                                                               in if if P1 a then P2 a else ff fi 
                                                                  then [a / (list_ind as')]
                                                                  else list_ind as'
                                                                  fi  otherwise if v = Ax then [] otherwise ⊥^j - 1 
                              ⊥ 
                              as'
                         fi  otherwise if v = Ax then [] otherwise ⊥ ≤ eval v = rec-case(L) of
                                                                                [] => []
                                                                                a::as' =>
                                                                                 r.if P1 a then [a / r] else r fi  in
                                                                       if v is a pair then let a,as' = v 
                                                                                           in if P2 a
                                                                                              then [a / 
                                                                                                    rec-case(as') of
                                                                                                    [] => []
                                                                                                    h::t =>
                                                                                                     r.if P2 h
                                                                                                    then [h / r]
                                                                                                    else r
                                                                                                    fi ]
                                                                                              else rec-case(as') of
                                                                                                   [] => []
                                                                                                   h::t =>
                                                                                                    r.if P2 h
                                                                                                   then [h / r]
                                                                                                   else r
                                                                                                   fi 
                                                                                              fi 
                                                                       otherwise if v = Ax then [] otherwise ⊥

---

Latex:

---

Latex:
\mforall{}[P1,P2,L:Top].    (filter(P2;filter(P1;L))  \msim{}  filter(\mlambda{}t.((P1  t)  \mwedge{}\msubb{}  (P2  t));L))


By

---

Latex:
(RepUR  ``band  filter  reduce``  0
  THEN  MutualFixpointInduction1  `L'
  THEN  Reduce  0
  THEN  RW  (SubC  (TryC  RecUnfoldTopAbC))  0)

---

Home Index