Step
*
2
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 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 
BY
{ (RW (AddrC [1] (LiftC true)) 0
   THEN Reduce 0
   THEN Repeat ((SqLeCD THEN Try (BackThruSomeHyp)))
   THEN (InstHyp [⌜P⌝;⌜B⌝;⌜snd(A)⌝] 3⋅ THENA Auto)
   THEN RW (AddrC [1] 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  if  P  a
                                                                                                    then  [a  /  (list$_{ind}$  as')]
                                                                                                    else  list$_{ind}$  as'
                                                                                                    fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
                              \mbot{} 
                              A)  of
            []  =>  rec-case(B)  of
                        []  =>  []
                        a::as'  =>
                          r.if  P  a  then  [a  /  r]  else  r  fi 
            a::as'  =>
              r.[a  /  r]  \mleq{}  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  \mleq{}  0@i
8.  A  \msim{}  <fst(A),  snd(A)>
\mvdash{}  eval  v  =  if  P  (fst(A))
    then  [fst(A)  / 
                (\mlambda{}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')]\000C  else  list$_{ind}$  as'  fi 
                                          otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
                  \mbot{} 
                  (snd(A)))]
    else  \mlambda{}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')]  e\000Clse  list$_{ind}$  as'  fi 
                                      otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
              \mbot{} 
              (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  \mbot{}  \mleq{}  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 
By
Latex:
(RW  (AddrC  [1]  (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  [1]  RecUnfoldTopAbC)  (-1)
  THEN  NthHyp  (-1))
Home
Index