Step
*
1
1
1
2
2
1
of Lemma
decidable-bar-rec-equal-spector
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,dec:Base.
(λ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))^j - 1
⊥
n
s ≤ fix((λspector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi ≤z n
then case dec n s of inl(r) => base n s r | inr(x) => ⊥
else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
fi ))
n
s)
4. n : ℕ@i
5. s : Base@i
6. ind : Base@i
7. base : Base@i
8. dec : Base@i
9. is-exception(case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s
(λt.(λ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))^j - 1
⊥
(n + 1)
s.t@n)))
10. is-exception(dec n s)
⊢ case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s
(λt.(λ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))^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.(fix((λ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))))
(n + 1)
s.t@n))
BY
{ (ExceptionSqequal (-1)
THEN RW (AddrC [1;1] (HypC (-1))) 0
THEN RW (AddrC [2;1;1;2;1] (HypC (-1))) 0
THEN Reduce 0
THEN (Assert ⌜if (n) < (exception(u; v)) then tt else ff ~ exception(u; v)⌝⋅
THENA (Refine_exceptionLess THEN Auto)
)
THEN RWO "-1" 0
THEN Reduce 0
THEN Auto) }
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}n:\mBbbN{}. \mforall{}s,ind,base,dec:Base.
(\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))\^{}j - 1
\mbot{}
n
s \mleq{} fix((\mlambda{}spector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi \mleq{}z n
then case dec n s of inl(r) => base n s r | inr(x) => \mbot{}
else ind n s (\mlambda{}t.(spector-bar-rec (n + 1) s.t@n))
fi ))
n
s)
4. n : \mBbbN{}@i
5. s : Base@i
6. ind : Base@i
7. base : Base@i
8. dec : Base@i
9. is-exception(case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s
(\mlambda{}t.(\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))\^{}j - 1
\mbot{}
(n + 1)
s.t@n)))
10. is-exception(dec n s)
\mvdash{} case dec n s
of inl(r) =>
base n s r
| inr(x) =>
ind n s
(\mlambda{}t.(\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))\^{}j - 1
\mbot{}
(n + 1)
s.t@n)) \mleq{} 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.(fix((\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))))
(n + 1)
s.t@n))
By
Latex:
(ExceptionSqequal (-1)
THEN RW (AddrC [1;1] (HypC (-1))) 0
THEN RW (AddrC [2;1;1;2;1] (HypC (-1))) 0
THEN Reduce 0
THEN (Assert \mkleeneopen{}if (n) < (exception(u; v)) then tt else ff \msim{} exception(u; v)\mkleeneclose{}\mcdot{}
THENA (Refine\_exceptionLess THEN Auto)
)
THEN RWO "-1" 0
THEN Reduce 0
THEN Auto)
Home
Index