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