Step
*
2
1
1
of Lemma
decidable-bar-rec-equal-spector
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,dec:Base.
(λspector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1
⊥
n
s ≤ fix((λdecidable-bar-rec,n,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))))
n
s)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. dec : Base
9. (case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff of inl() => ff | inr() => tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s
(λt.(λspector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1
⊥
(n + 1)
s.t@n)))↓
10. case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff of inl() => ff | inr() => tt
∈ Top + Top
11. (case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff of inl() => ff | inr() => tt)↓
12. if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff ∈ Top + Top
13. (if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff)↓
14. n ∈ ℤ
15. case dec n s of inl() => 0 | inr() => n + 1 ∈ ℤ
16. (case dec n s of inl() => 0 | inr() => n + 1)↓
17. dec n s ∈ Top + Top
⊢ case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff of inl() => ff | inr() => tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s
(λt.(λspector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1
⊥
(n + 1)
s.t@n)) ≤ case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s
(λt.(fix((λdecidable-bar-rec,n,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))))
(n + 1)
s.t@n))
BY
{ ((GenConclTerm ⌜dec n s⌝⋅ THENA Auto) THEN DVar `v' THEN Reduce 0 THEN AutoSplit) }
1
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,dec:Base.
(λspector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1
⊥
n
s ≤ fix((λdecidable-bar-rec,n,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))))
n
s)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. dec : Base
9. (case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff of inl() => ff | inr() => tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s
(λt.(λspector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1
⊥
(n + 1)
s.t@n)))↓
10. case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff of inl() => ff | inr() => tt
∈ Top + Top
11. (case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff of inl() => ff | inr() => tt)↓
12. if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff ∈ Top + Top
13. (if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff)↓
14. n ∈ ℤ
15. case dec n s of inl() => 0 | inr() => n + 1 ∈ ℤ
16. (case dec n s of inl() => 0 | inr() => n + 1)↓
17. dec n s ∈ Top + Top
18. y : Top
19. (dec n s) = (inr y ) ∈ (Top + Top)
20. n < n + 1
⊢ ind n s
(λt.(λspector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => ⊥
| inr() =>
ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1
⊥
(n + 1)
s.t@n)) ≤ ind n s
(λt.(fix((λdecidable-bar-rec,n,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))))
(n + 1)
s.t@n))
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}n:\mBbbN{}. \mforall{}s,ind,base,dec:Base.
(\mlambda{}spector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1)
then tt
else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => \mbot{}
| inr() =>
ind n s (\mlambda{}t.(spector-bar-rec (n + 1) s.t@n))\^{}j - 1
\mbot{}
n
s \mleq{} fix((\mlambda{}decidable-bar-rec,n,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s (\mlambda{}t.(decidable-bar-rec (n + 1) s.t@n))))
n
s)
4. n : \mBbbN{}
5. s : Base
6. ind : Base
7. base : Base
8. dec : Base
9. (case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => \mbot{}
| inr() =>
ind n s
(\mlambda{}t.(\mlambda{}spector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1)
then tt
else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => \mbot{}
| inr() =>
ind n s (\mlambda{}t.(spector-bar-rec (n + 1) s.t@n))\^{}j - 1
\mbot{}
(n + 1)
s.t@n)))\mdownarrow{}
10. case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt \mmember{} Top + Top
11. (case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt)\mdownarrow{}
12. if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff \mmember{} Top + Top
13. (if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff)\mdownarrow{}
14. n \mmember{} \mBbbZ{}
15. case dec n s of inl() => 0 | inr() => n + 1 \mmember{} \mBbbZ{}
16. (case dec n s of inl() => 0 | inr() => n + 1)\mdownarrow{}
17. dec n s \mmember{} Top + Top
\mvdash{} case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1) then tt else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => \mbot{}
| inr() =>
ind n s
(\mlambda{}t.(\mlambda{}spector-bar-rec,n,s. case case if (n) < (case dec n s of inl() => 0 | inr() => n + 1)
then tt
else ff
of inl() =>
ff
| inr() =>
tt
of inl() =>
case dec n s of inl(r) => base n s r | inr(x) => \mbot{}
| inr() =>
ind n s (\mlambda{}t.(spector-bar-rec (n + 1) s.t@n))\^{}j - 1
\mbot{}
(n + 1)
s.t@n)) \mleq{} case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s
(\mlambda{}t.(fix((\mlambda{}decidable-bar-rec,n,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s (\mlambda{}t.(decidable-bar-rec (n + 1) s.t@n))))
(n + 1)
s.t@n))
By
Latex:
((GenConclTerm \mkleeneopen{}dec n s\mkleeneclose{}\mcdot{} THENA Auto) THEN DVar `v' THEN Reduce 0 THEN AutoSplit)
Home
Index