Step
*
2
of Lemma
filter-map
1. j : ℤ
2. 0 < j
3. ∀Q,f,L:Base.
(rec-case(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a) then [a / (list_ind as')] else list_ind as' fi
otherwise if v = Ax then [] otherwise ⊥^j - 1
⊥
L) of
[] => []
h::t =>
r.[f h / r] ≤ rec-case(rec-case(L) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
a::as' =>
r.if Q a then [a / r] else r fi )
4. Q : Base@i
5. f : Base@i
6. L : Base@i
7. 0 ≤ 0@i
8. L ~ <fst(L), snd(L)>
⊢ eval v = if Q (f (fst(L)))
then [fst(L) /
(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a) then [a / (list_ind as')] else list_ind as' fi
otherwise if v = Ax then [] otherwise ⊥^j - 1
⊥
(snd(L)))]
else λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a) then [a / (list_ind as')] else list_ind as' fi
otherwise if v = Ax then [] otherwise ⊥^j - 1
⊥
(snd(L))
fi in
if v is a pair then let h,t = v
in [f h / rec-case(t) of [] => [] | h::t => r.[f h / r]] otherwise if v = Ax then [] otherwise ⊥
≤ if Q (f (fst(L)))
then [f (fst(L)) /
rec-case(rec-case(snd(L)) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
h::t =>
r.if Q h then [h / r] else r fi ]
else rec-case(rec-case(snd(L)) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
h::t =>
r.if Q h then [h / r] else r fi
fi
BY
{ (RW (AddrC [1] (LiftC true)) 0 THEN Reduce 0 THEN Repeat ((SqLeCD THEN Try (BackThruSomeHyp)))) }
1
1. j : ℤ
2. 0 < j
3. ∀Q,f,L:Base.
(rec-case(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a) then [a / (list_ind as')] else list_ind as' fi
otherwise if v = Ax then [] otherwise ⊥^j - 1
⊥
L) of
[] => []
h::t =>
r.[f h / r] ≤ rec-case(rec-case(L) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
a::as' =>
r.if Q a then [a / r] else r fi )
4. Q : Base@i
5. f : Base@i
6. L : Base@i
7. 0 ≤ 0@i
8. L ~ <fst(L), snd(L)>
⊢ eval v = λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a) then [a / (list_ind as')] else list_ind as' fi
otherwise if v = Ax then [] otherwise ⊥^j - 1
⊥
(snd(L)) in
if v is a pair then let h,t = v
in [f h / rec-case(t) of [] => [] | h::t => r.[f h / r]] otherwise if v = Ax then [] otherwise ⊥
≤ rec-case(rec-case(snd(L)) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
h::t =>
r.if Q h then [h / r] else r fi
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}Q,f,L:Base.
(rec-case(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a)
then [a / (list$_{ind}$ as')]
else list$_{ind}$ as'
fi otherwise if v = Ax then [] otherwise \mbot{}\^{}j - 1
\mbot{}
L) of
[] => []
h::t =>
r.[f h / r] \mleq{} rec-case(rec-case(L) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
a::as' =>
r.if Q a then [a / r] else r fi )
4. Q : Base@i
5. f : Base@i
6. L : Base@i
7. 0 \mleq{} 0@i
8. L \msim{} <fst(L), snd(L)>
\mvdash{} eval v = if Q (f (fst(L)))
then [fst(L) /
(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a) then [a / (list$_{ind}$ a\000Cs')] else list$_{ind}$ as' fi
otherwise if v = Ax then [] otherwise \mbot{}\^{}j - 1
\mbot{}
(snd(L)))]
else \mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in if Q (f a) then [a / (list$_{ind}$ as'\000C)] else list$_{ind}$ as' fi
otherwise if v = Ax then [] otherwise \mbot{}\^{}j - 1
\mbot{}
(snd(L))
fi in
if v is a pair then let h,t = v
in [f h / rec-case(t) of [] => [] | h::t => r.[f h / r]]
otherwise if v = Ax then [] otherwise \mbot{} \mleq{} if Q (f (fst(L)))
then [f (fst(L)) /
rec-case(rec-case(snd(L)) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
h::t =>
r.if Q h then [h / r] else r fi ]
else rec-case(rec-case(snd(L)) of
[] => []
h::t =>
r.[f h / r]) of
[] => []
h::t =>
r.if Q 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))))
Home
Index