Step * 2 of Lemma filter_append_sq


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