Step
*
2
of Lemma
decidable-bar-rec-equal-spector
1. n : ℕ
2. s : Base
3. ind : Base
4. base : Base
5. dec : Base
⊢ spector-bar-rec(λn,s. if dec n s then 0 else n + 1 fi ;λn,s. case dec n s of inl(r) => base n s r | inr(x) => ⊥;ind;n;\000Cs)
≤ decidable-bar-rec(dec;base;ind;n;s)
BY
{ (RepUR ``decidable-bar-rec decidable-bar-rec-spec spector-bar-rec ifthenelse le_int bnot lt_int`` 0
THEN ProveSqFixpointsLe
THEN AssumeHasValue) }
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)))↓
⊢ 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))
2
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. is-exception(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 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))
Latex:
Latex:
1. n : \mBbbN{}
2. s : Base
3. ind : Base
4. base : Base
5. dec : Base
\mvdash{} spector-bar-rec(\mlambda{}n,s. if dec n s then 0 else n + 1 fi ;\mlambda{}n,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
\mbot{};ind;n;s)
\mleq{} decidable-bar-rec(dec;base;ind;n;s)
By
Latex:
(RepUR ``decidable-bar-rec decidable-bar-rec-spec spector-bar-rec ifthenelse le\_int bnot lt\_int`` 0
THEN ProveSqFixpointsLe
THEN AssumeHasValue)
Home
Index