Step
*
1
1
1
1
1
3
1
of Lemma
cWO-induction-extract-sqequal
1. f : Base
2. G : Base
3. G ~ λf,bar_recursion,n,s. case if (0) < (n)
then if s (n - 1) then inr (λp.let _,_ = p in Ax) else inl <Ax, Ax> fi
else (inr (λp.let _,_ = p
in Ax) )
of inl(r) =>
λa.let _,_ = r
in Ax
| inr(r) =>
λa.(f a (λs1.(bar_recursion (n + 1) (λm.if m=n then inl a else (s m)) s1)))
4. j : ℤ
5. t : Base
6. s1 : Base
7. n : ℕ+
8. x : Base
⊢ f s1 ⊥ ≤ case if (0) < (n) then inr (λp.let _,_ = p in Ax) else (inr (λp.let _,_ = p in Ax) )
of inl(r) =>
λa.let _,_ = r
in Ax
| inr(r) =>
λa.(f a
(λs1.(fix((λbar_recursion,n,s. case if (0) < (n)
then if s (n - 1)
then inr (λp.let _,_ = p
in Ax)
else inl <Ax, Ax>
fi
else (inr (λp.let _,_ = p
in Ax) )
of inl(r) =>
λa.let _,_ = r
in Ax
| inr(r) =>
λa.(f a
(λs1.(bar_recursion (n + 1) (λm.if m=n then inl a else (s m)) s1)))\000C))
(n + 1)
(λm.if m=n then inl a else if m=n - 1 then inl t else (x m))
s1)))
s1
BY
{ AbbreviateTerm ⌜λa.(f a
(λs1.(fix((λbar_recursion,n,s. case if (0) < (n)
then if s (n - 1)
then inr (λp.let _,_ = p
in Ax)
else inl <Ax, Ax>
fi
else (inr (λp.let _,_ = p
in Ax) )
of inl(r) =>
λa.let _,_ = r
in Ax
| inr(r) =>
λa.(f a
(λs1.(bar_recursion (n + 1)
(λm.if m=n then inl a else (s m))
s1)))))
(n + 1)
(λm.if m=n then inl a else if m=n - 1 then inl t else (x m))
s1)))⌝ `X'⋅ }
1
1. f : Base
2. G : Base
3. G ~ λf,bar_recursion,n,s. case if (0) < (n)
then if s (n - 1) then inr (λp.let _,_ = p in Ax) else inl <Ax, Ax> fi
else (inr (λp.let _,_ = p
in Ax) )
of inl(r) =>
λa.let _,_ = r
in Ax
| inr(r) =>
λa.(f a (λs1.(bar_recursion (n + 1) (λm.if m=n then inl a else (s m)) s1)))
4. j : ℤ
5. t : Base
6. s1 : Base
7. n : ℕ+
8. x : Base
9. X : Base
10. X ~ λx,t,n,f,a. (f a
(λs1.(fix((λbar_recursion,n,s. case if (0) < (n)
then if s (n - 1)
then inr (λp.let _,_ = p
in Ax)
else inl <Ax, Ax>
fi
else (inr (λp.let _,_ = p
in Ax) )
of inl(r) =>
λa.let _,_ = r
in Ax
| inr(r) =>
λa.(f a
(λs1.(bar_recursion (n + 1) (λm.if m=n then inl a else (s m))
s1)))))
(n + 1)
(λm.if m=n then inl a else if m=n - 1 then inl t else (x m))
s1)))
⊢ f s1 ⊥ ≤ case if (0) < (n) then inr (λp.let _,_ = p in Ax) else (inr (λp.let _,_ = p in Ax) )
of inl(r) =>
λa.let _,_ = r
in Ax
| inr(r) =>
X x t n f
s1
Latex:
Latex:
1. f : Base
2. G : Base
3. G \msim{} \mlambda{}f,bar$_{recursion}$,n,s. case if (0) < (n)
then if s (n - 1)
then inr (\mlambda{}p.let $_{}$,$_{\mbackslash{}\000Cff7d$ = p
in Ax)
else inl <Ax, Ax>
fi
else (inr (\mlambda{}p.let $_{}$,$_{}\000C$ = p
in Ax) )
of inl(r) =>
\mlambda{}a.let $_{}$,$_{}$ = r
in Ax
| inr(r) =>
\mlambda{}a.(f a
(\mlambda{}s1.(bar$_{recursion}$ (n + 1) (\mlambda{}m.if m=n then\000C inl a else (s m)) s1)))
4. j : \mBbbZ{}
5. t : Base
6. s1 : Base
7. n : \mBbbN{}\msupplus{}
8. x : Base
\mvdash{} f s1 \mbot{} \mleq{} case if (0) < (n) then inr (\mlambda{}p.let $_{}$,$_{}$ =\000C p in Ax) else (inr (\mlambda{}p.let $_{}$,$_{}$ = p in Ax) )
of inl(r) =>
\mlambda{}a.let $_{}$,$_{}$ = r
in Ax
| inr(r) =>
\mlambda{}a.(f a
(\mlambda{}s1.(fix((\mlambda{}bar$_{recursion}$,n,s. case if (0) < (n)
then if s (n - 1)
then inr (\mlambda{}p.let $_{}\mbackslash{}ff2\000C4,$_{}$ = p
in Ax)
else inl <Ax, Ax>
fi
else (inr (\mlambda{}p.let $_{}$,\mbackslash{}f\000Cf24_{}$ = p
in Ax) )
of inl(r) =>
\mlambda{}a.let $_{}$,$_{}\mbackslash{}\000Cff24 = r
in Ax
| inr(r) =>
\mlambda{}a.(f a
(\mlambda{}s1.(bar$_{recursion}$ (n + 1\000C)
(\mlambda{}m.if m=n then inl a else (s m))
s1)))))
(n + 1)
(\mlambda{}m.if m=n then inl a else if m=n - 1 then inl t else (x m))
s1)))
s1
By
Latex:
AbbreviateTerm \mkleeneopen{}\mlambda{}a.(f a
(\mlambda{}s1.(fix((\mlambda{}bar$_{recursion}$,n,s. case if (0) < (n)
then if s (n - 1)
then inr (\mlambda{}p.let $_{}\000C$,$_{}$ = p
in Ax)
else inl <Ax, Ax>
fi
else (inr (\mlambda{}p.let $_{}\mbackslash{}ff2\000C4,$_{}$ = p
in Ax) )
of inl(r) =>
\mlambda{}a.let $_{}$,$_{\mbackslash{}f\000Cf7d$ = r
in Ax
| inr(r) =>
\mlambda{}a.(f a
(\mlambda{}s1.(bar$_{recursion}$ (n\000C + 1)
(\mlambda{}m.if m=n then inl a else (s m))
s1)))))
(n + 1)
(\mlambda{}m.if m=n then inl a else if m=n - 1 then inl t else (x m))
s1)))\mkleeneclose{} `X'\mcdot{}
Home
Index