Step * 1 of Lemma filter-filter

`1. j : ℤ`
`2. 0 < j`
`3. ∀P2,P1,L:Base.`
`     (rec-case(λlist_ind,L. eval v = L in`
`                            if v is a pair then let a,as' = v `
`                                                in if P1 a then [a / (list_ind as')] else list_ind as' fi `
`                            otherwise if v = Ax then [] otherwise ⊥^j - 1 `
`               ⊥ `
`               L) of`
`      [] => []`
`      a::as' =>`
`       r.if P2 a then [a / r] else r fi  ≤ rec-case(L) of`
`                                           [] => []`
`                                           a::as' =>`
`                                            r.if if P1 a then P2 a else ff fi  then [a / r] else r fi )`
`4. P2 : Base`
`5. P1 : Base`
`6. L : Base`
`⊢ eval v = eval v = L in`
`           if v is a pair then let a,as' = v `
`                               in if P1 a`
`                                  then [a / `
`                                        (λlist_ind,L. eval v = L in`
`                                                      if v is a pair then let a,as' = v `
`                                                                          in if P1 a`
`                                                                             then [a / (list_ind as')]`
`                                                                             else list_ind as'`
`                                                                             fi  otherwise if v = Ax then [] otherwise ⊥\000C^j - 1 `
`                                         ⊥ `
`                                         as')]`
`                                  else λlist_ind,L. eval v = L in`
`                                                    if v is a pair then let a,as' = v `
`                                                                        in if P1 a`
`                                                                           then [a / (list_ind as')]`
`                                                                           else list_ind as'`
`                                                                           fi  otherwise if v = Ax then [] otherwise ⊥^j\000C - 1 `
`                                       ⊥ `
`                                       as'`
`                                  fi  otherwise if v = Ax then [] otherwise ⊥ in`
`  if v is a pair then let a,as' = v `
`                      in if P2 a`
`                         then [a / rec-case(as') of [] => [] | h::t => r.if P2 h then [h / r] else r fi ]`
`                         else rec-case(as') of`
`                              [] => []`
`                              h::t =>`
`                               r.if P2 h then [h / r] else r fi `
`                         fi  otherwise if v = Ax then [] otherwise ⊥ ≤ eval v = L in`
`                                                                       if v is a pair then let a,as' = v `
`                                                                                           in if if P1 a`
`                                                                                                 then P2 a`
`                                                                                                 else ff`
`                                                                                                 fi `
`                                                                                              then [a / `
`                                                                                                    rec-case(as') of`
`                                                                                                    [] => []`
`                                                                                                    h::t =>`
`                                                                                                     r.if if P1 h`
`                                                                                                          then P2 h`
`                                                                                                          else ff`
`                                                                                                          fi `
`                                                                                                    then [h / r]`
`                                                                                                    else r`
`                                                                                                    fi ]`
`                                                                                              else rec-case(as') of`
`                                                                                                   [] => []`
`                                                                                                   h::t =>`
`                                                                                                    r.if if P1 h`
`                                                                                                         then P2 h`
`                                                                                                         else ff`
`                                                                                                         fi `
`                                                                                                   then [h / r]`
`                                                                                                   else r`
`                                                                                                   fi `
`                                                                                              fi `
`                                                                       otherwise if v = Ax then [] otherwise ⊥`
BY
`{ (RW (AddrC [1] (LiftC false)) 0`
`   THEN UseCbvSqle`
`   THEN HVimplies2 0 [2]`
`   THEN Try (((RWO "-1" 0 THENA MemTop) THEN HVimplies2 0 [2]))`
`   THEN RW (SubC (LiftC true)) 0`
`   THEN Reduce 0`
`   THEN SqLeCD`
`   THEN Try (((InstHyp [⌜P2⌝;⌜P1⌝;⌜snd(L)⌝] 3⋅ THENA Auto) THEN RW (AddrC [1] RecUnfoldTopAbC) (-1) THEN NthHyp (-1)))`
`   THEN RepeatFor 3 ((SqLeCD THEN Try (BackThruSomeHyp)))) }`

Latex:

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}P2,P1,L:Base.
(rec-case(\mlambda{}list\$_{ind}\$,L.  eval  v  =  L  in
if  v  is  a  pair  then  let  a,as'  =  v
in  if  P1  a
then  [a  /  (list\$_{ind}\$  as')]
else  list\$_{ind}\$  as'
fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1
\mbot{}
L)  of
[]  =>  []
a::as'  =>
r.if  P2  a  then  [a  /  r]  else  r  fi    \mleq{}  rec-case(L)  of
[]  =>  []
a::as'  =>
r.if  if  P1  a  then  P2  a  else  ff  fi
then  [a  /  r]
else  r
fi  )
4.  P2  :  Base
5.  P1  :  Base
6.  L  :  Base
\mvdash{}  eval  v  =  eval  v  =  L  in
if  v  is  a  pair  then  let  a,as'  =  v
in  if  P1  a
then  [a  /
(\mlambda{}list\$_{ind}\$,L.  eval  v  =  L  in
if  v  is  a  pair  then  let  a,as'  =  v
in  if  P1  a
then  [a  /  (list\$\mbackslash{}ff5\000Cf{ind}\$  as')]
else  list\$_{\000Cind}\$  as'
fi
otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1
\mbot{}
as')]
else  \mlambda{}list\$_{ind}\$,L.  eval  v  =  L  in
if  v  is  a  pair  then  let  a,as'  =  v
in  if  P1  a
then  [a  /  (list\$_\mbackslash{}\000Cff7bind}\$  as')]
else  list\$_{in\000Cd}\$  as'
fi
otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1
\mbot{}
as'
fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}  in
if  v  is  a  pair  then  let  a,as'  =  v
in  if  P2  a
then  [a  /
rec-case(as')  of
[]  =>  []
h::t  =>
r.if  P2  h  then  [h  /  r]  else  r  fi  ]
else  rec-case(as')  of
[]  =>  []
h::t  =>
r.if  P2  h  then  [h  /  r]  else  r  fi
fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}
\mleq{}  eval  v  =  L  in
if  v  is  a  pair  then  let  a,as'  =  v
in  if  if  P1  a  then  P2  a  else  ff  fi
then  [a  /
rec-case(as')  of
[]  =>  []
h::t  =>
r.if  if  P1  h  then  P2  h  else  ff  fi    then  [h  /  r]  else  r  fi  ]
else  rec-case(as')  of
[]  =>  []
h::t  =>
r.if  if  P1  h  then  P2  h  else  ff  fi    then  [h  /  r]  else  r  fi
fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}

By

Latex:
(RW  (AddrC  [1]  (LiftC  false))  0
THEN  UseCbvSqle
THEN  HVimplies2  0  [2]
THEN  Try  (((RWO  "-1"  0  THENA  MemTop)  THEN  HVimplies2  0  [2]))
THEN  RW  (SubC  (LiftC  true))  0
THEN  Reduce  0
THEN  SqLeCD
THEN  Try  (((InstHyp  [\mkleeneopen{}P2\mkleeneclose{};\mkleeneopen{}P1\mkleeneclose{};\mkleeneopen{}snd(L)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  (-1)
THEN  NthHyp  (-1)))
THEN  RepeatFor  3  ((SqLeCD  THEN  Try  (BackThruSomeHyp))))

Home Index