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