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