Step
*
2
of Lemma
fan-realizer_wf
1. λ%,%1. <bar_recursion(λn,s. (%1 map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in eval b = %2 ff in if (a) < (b) then 1 + b else (1 + a);
0;λm.eval x = m in
⊥)
, λf.outl(int_seg_decide(λn.(%1 map(f;upto(n)));0;bar_recursion(λn,s. (%1 map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in
eval b = %2 ff in
if (a) < (b)
then 1 + b
else (1 + a);
0;λm.eval x = m in
⊥)))
> ∈ ∀[X:(𝔹 List) ⟶ ℙ]. (tbar(𝔹;X) ⇒ Decidable(X) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))))
2. X : (𝔹 List) ⟶ ℙ
3. bar : tbar(𝔹;X)
4. d : Decidable(X)
5. λm.if (m) < (0) then ⊥ else ⊥ ~ λm.eval x = m in
⊥
⊢ <bar_recursion(λn,s. (d map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in eval b = %2 ff in if (a) < (b) then 1 + b else (1 + a);
0;λm.eval x = m in
⊥)
, λf.outl(int_seg_decide(λn.(d map(f;upto(n)));0;bar_recursion(λn,s. (d map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in
eval b = %2 ff in
if (a) < (b) then 1 + b else (1 + a);
0;λm.eval x = m in
⊥)))
> ∈ ∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))
BY
{ ((Subst <bar_recursion(λn,s. (d map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in eval b = %2 ff in if (a) < (b) then 1 + b else (1 + a);
0;λm.eval x = m in
⊥)
, λf.outl(int_seg_decide(λn.(d map(f;upto(n)));0;bar_recursion(λn,s. (d map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in
eval b = %2 ff in
if (a) < (b)
then 1 + b
else (1 + a);
0;λm.eval x = m in
⊥)))
> ~ (λ%,%1. <bar_recursion(λn,s. (%1 map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in eval b = %2 ff in if (a) < (b) then 1 + b else (1 + a);
0;λm.eval x = m in
⊥)
, λf.outl(int_seg_decide(λn.(%1 map(f;upto(n)));0;bar_recursion(λn,s. (%1 map(s;upto(n)));
λn,s,%2. 1;
λn,s,%2. eval a = %2 tt in
eval b = %2 ff in
if (a) < (b)
then 1 + b
else (1 + a);
0;λm.eval x = m in
⊥)))
>)
bar
d 0⋅
THENA (Reduce 0 THEN Trivial)
)
THEN GenConclAtAddr [2;1;1]
THEN Auto) }
Latex:
Latex:
1. \mlambda{}\%,\%1. <bar\_recursion(\mlambda{}n,s. (\%1 map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b) then 1 + b else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{})
, \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(\%1 map(f;upto(n)));0;bar\_recursion(\mlambda{}n,s. (\%1 map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b)
then 1 + b
else (1 + a)\000C;
0;\mlambda{}m.eval x = m in
\mbot{})))
> \mmember{} \mforall{}[X:(\mBbbB{} List) {}\mrightarrow{} \mBbbP{}]
(tbar(\mBbbB{};X) {}\mRightarrow{} Decidable(X) {}\mRightarrow{} (\mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}k. (X map(f;upto(n)))))
2. X : (\mBbbB{} List) {}\mrightarrow{} \mBbbP{}
3. bar : tbar(\mBbbB{};X)
4. d : Decidable(X)
5. \mlambda{}m.if (m) < (0) then \mbot{} else \mbot{} \msim{} \mlambda{}m.eval x = m in
\mbot{}
\mvdash{} <bar\_recursion(\mlambda{}n,s. (d map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b) then 1 + b else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{})
, \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(d map(f;upto(n)));0;bar\_recursion(\mlambda{}n,s. (d map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b)
then 1 + b
else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{})))
> \mmember{} \mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}k. (X map(f;upto(n)))
By
Latex:
((Subst
<bar\_recursion(\mlambda{}n,s. (d map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b) then 1 + b else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{})
, \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(d map(f;upto(n)));0;bar\_recursion(\mlambda{}n,s. (d map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b)
then 1 + b
else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{})))
>
\msim{} (\mlambda{}\%,\%1. <bar\_recursion(\mlambda{}n,s. (\%1 map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b) then 1 + b else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{})
, \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(\%1
map(f;upto(n)));0;bar\_recursion(\mlambda{}n,s. (\%1 map(s;upto(n)));
\mlambda{}n,s,\%2. 1;
\mlambda{}n,s,\%2. eval a = \%2 tt in
eval b = \%2 ff in
if (a) < (b)
then 1 + b
else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{})))
>)
bar
d 0\mcdot{}
THENA (Reduce 0 THEN Trivial)
)
THEN GenConclAtAddr [2;1;1]
THEN Auto)
Home
Index