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:
(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 [\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