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