Step * 2 of Lemma filter-filter

`1. j : ℤ`
`2. 0 < j`
`3. ∀P2,P1,L:Base.`
`     (λlist_ind,L. 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 / (list_ind as')]`
`                                          else list_ind as'`
`                                          fi  otherwise if v = Ax then [] otherwise ⊥^j - 1 `
`      ⊥ `
`      L ≤ rec-case(rec-case(L) of`
`                   [] => []`
`                   a::as' =>`
`                    r.if P1 a then [a / r] else r fi ) of`
`          [] => []`
`          a::as' =>`
`           r.if P2 a then [a / r] else r fi )`
`4. P2 : Base`
`5. P1 : Base`
`6. L : Base`
`⊢ 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 / `
`                               (λlist_ind,L. 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 / (list_ind as')]`
`                                                                    else list_ind as'`
`                                                                    fi  otherwise if v = Ax then [] otherwise ⊥^j - 1 `
`                                ⊥ `
`                                as')]`
`                         else λlist_ind,L. 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 / (list_ind as')]`
`                                                                  else list_ind as'`
`                                                                  fi  otherwise if v = Ax then [] otherwise ⊥^j - 1 `
`                              ⊥ `
`                              as'`
`                         fi  otherwise if v = Ax then [] otherwise ⊥ ≤ eval v = rec-case(L) of`
`                                                                                [] => []`
`                                                                                a::as' =>`
`                                                                                 r.if P1 a then [a / r] else r fi  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 ⊥`
BY
`{ (RW (AddrC [2;1] RecUnfoldTopAbC) 0`
`   THEN RW (AddrC [2] (LiftC false)) 0`
`   THEN UseCbvSqle`
`   THEN HVimplies2 0 [1]`
`   THEN Try (((RWO "-1" 0 THENA MemTop) THEN HVimplies2 0 [1]))`
`   THEN RW (SubC (LiftC true)) 0`
`   THEN Reduce 0`
`   THEN SqLeCD`
`   THEN Try (((InstHyp [⌜P2⌝;⌜P1⌝;⌜snd(L)⌝] 3⋅ THENA Auto) THEN RW (AddrC [2] 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.
(\mlambda{}list\$_{ind}\$,L.  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  /  (list\$_{ind}\$  as')]
else  list\$_{ind}\$  as'
fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1
\mbot{}
L  \mleq{}  rec-case(rec-case(L)  of
[]  =>  []
a::as'  =>
r.if  P1  a  then  [a  /  r]  else  r  fi  )  of
[]  =>  []
a::as'  =>
r.if  P2  a  then  [a  /  r]  else  r  fi  )
4.  P2  :  Base
5.  P1  :  Base
6.  L  :  Base
\mvdash{}  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  /
(\mlambda{}list\$_{ind}\$,L.  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  /  (list\$_{ind\000C}\$  as')]
else  list\$_{ind}\mbackslash{}\000Cff24  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  if  P1  a  then  P2  a  else  ff  fi
then  [a  /  (list\$_{ind\mbackslash{}f\000Cf7d\$  as')]
else  list\$_{ind}\mbackslash{}ff\000C24  as'
fi
otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1
\mbot{}
as'
fi    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}
\mleq{}  eval  v  =  rec-case(L)  of
[]  =>  []
a::as'  =>
r.if  P1  a  then  [a  /  r]  else  r  fi    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{}

By

Latex:
THEN  RW  (AddrC  [2]  (LiftC  false))  0
THEN  UseCbvSqle
THEN  HVimplies2  0  [1]
THEN  Try  (((RWO  "-1"  0  THENA  MemTop)  THEN  HVimplies2  0  [1]))
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  [2]  RecUnfoldTopAbC)  (-1)
THEN  NthHyp  (-1)))
THEN  RepeatFor  3  ((SqLeCD  THEN  Try  (BackThruSomeHyp))))

Home Index