---

Step * of Lemma filter_append_sq

∀[P,A,B:Top].  (filter(P;A @ B) ~ filter(P;A) @ filter(P;B))
BY
{ (RepUR ``filter append reduce`` 0
   THEN MutualFixpointInduction1 `A'
   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 RW (SubC (LiftC true)) 0
              THEN HVimplies2 0 [1]
              THEN RW (SubC (TryC RecUnfoldTopAbC)) 0
              THEN Auto))) }

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

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

---

Latex:

---

Latex:
\mforall{}[P,A,B:Top].    (filter(P;A  @  B)  \msim{}  filter(P;A)  @  filter(P;B))


By

---

Latex:
(RepUR  ``filter  append  reduce``  0
  THEN  MutualFixpointInduction1  `A'
  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  RW  (SubC  (LiftC  true))  0
                        THEN  HVimplies2  0  [1]
                        THEN  RW  (SubC  (TryC  RecUnfoldTopAbC))  0
                        THEN  Auto)))

---

Home Index