---

Step * 1 of Lemma filter_append_sq


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 ⊥
BY
{ (RW (AddrC [2] (LiftC true)) 0
   THEN Reduce 0
   THEN Repeat ((SqLeCD THEN Try (BackThruSomeHyp)))
   THEN (InstHyp [⌜P⌝;⌜B⌝;⌜snd(A)⌝] 3⋅ THENA Auto)
   THEN RW (AddrC [2] RecUnfoldTopAbC) (-1)
   THEN NthHyp (-1)) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}P,B,A:Base.
          (rec-case(\mlambda{}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  \mbot{}\^{}j  -  1 
                              \mbot{} 
                              A)  of
            []  =>  []
            a::as'  =>
              r.if  P  a  then  [a  /  r]  else  r  fi    \mleq{}  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  \mleq{}  0@i
8.  A  \msim{}  <fst(A),  snd(A)>
\mvdash{}  if  P  (fst(A))
    then  [fst(A)  / 
                rec-case(\mlambda{}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  \mbot{}\^{}j  -  1 
                                  \mbot{} 
                                  (snd(A)))  of
                []  =>  []
                h::t  =>
                  r.if  P  h  then  [h  /  r]  else  r  fi  ]
    else  rec-case(\mlambda{}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  \mbot{}\^{}j  -  1 
                                \mbot{} 
                                (snd(A)))  of
              []  =>  []
              h::t  =>
                r.if  P  h  then  [h  /  r]  else  r  fi 
    fi    \mleq{}  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  \mbot{}


By

---

Latex:
(RW  (AddrC  [2]  (LiftC  true))  0
  THEN  Reduce  0
  THEN  Repeat  ((SqLeCD  THEN  Try  (BackThruSomeHyp)))
  THEN  (InstHyp  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}snd(A)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [2]  RecUnfoldTopAbC)  (-1)
  THEN  NthHyp  (-1))

---

Home Index