Step
*
1
of Lemma
howard-bar-rec-equal-spector
1. n : ℕ
2. s : Base
3. ind : Base
4. base : Base
5. mon : Base
6. M : Base
⊢ howard-bar-rec(M;mon;base;ind;n;s) ≤ spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n s
of inl(x) =>
let k,p = x
in base n s (mon n k s p)
| inr(x) =>
⊥;ind;n;s)
BY
{ RepUR ``howard-bar-rec spector-bar-rec`` 0 }
1
1. n : ℕ
2. s : Base
3. ind : Base
4. base : Base
5. mon : Base
6. M : Base
⊢ fix((λhoward-bar-rec,n,s. case M n s
of inl(x) =>
let k,p = x
in base n s (mon n k s p)
| inr(x) =>
ind n s (λt.(howard-bar-rec (n + 1) s.t@n))))
n
s ≤ fix((λspector-bar-rec,n,s. if if M n s then 0 else n + 1 fi ≤z n
then case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
fi ))
n
s
Latex:
Latex:
1. n : \mBbbN{}
2. s : Base
3. ind : Base
4. base : Base
5. mon : Base
6. M : Base
\mvdash{} howard-bar-rec(M;mon;base;ind;n;s)
\mleq{} spector-bar-rec(\mlambda{}n,s. if M n s then 0 else n + 1 fi ;\mlambda{}n,s. case M n s
of inl(x) =>
let k,p = x
in base n s (mon n k s p)
| inr(x) =>
\mbot{};ind;n;s)
By
Latex:
RepUR ``howard-bar-rec spector-bar-rec`` 0
Home
Index