Step
*
1
1
1
of Lemma
howard-bar-rec-equal-spector
.....failed on: 16.....
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
(λ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))^j - 1
⊥
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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
⊢ 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,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))^j - 1
⊥
(n + 1)
s.t@n)) ≤ 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.(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 + 1)
s.t@n))
fi
BY
{ AssumeHasValue }
1
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
(λ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))^j - 1
⊥
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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
10. (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,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))^j - 1
⊥
(n + 1)
s.t@n)))↓
⊢ 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,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))^j - 1
⊥
(n + 1)
s.t@n)) ≤ 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.(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 + 1)
s.t@n))
fi
2
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
(λ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))^j - 1
⊥
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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
10. is-exception(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,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))^j - 1
⊥
(n + 1)
s.t@n)))
⊢ 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,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))^j - 1
⊥
(n + 1)
s.t@n)) ≤ 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.(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 + 1)
s.t@n))
fi
Latex:
Latex:
.....failed on: 16.....
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}n:\mBbbN{}. \mforall{}s,ind,base,mon,M:Base.
(\mlambda{}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 (\mlambda{}t.(howard-bar-rec (n + 1) s.t@n))\^{}j - 1
\mbot{}
n
s \mleq{} fix((\mlambda{}spector-bar-rec,n,s. if if M n s then 0 else n + 1 fi \mleq{}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) =>
\mbot{}
else ind n s (\mlambda{}t.(spector-bar-rec (n + 1) s.t@n))
fi ))
n
s)
4. n : \mBbbN{}
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
\mvdash{} 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
(\mlambda{}t.(\mlambda{}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 (\mlambda{}t.(howard-bar-rec (n + 1) s.t@n))\^{}j - 1
\mbot{}
(n + 1)
s.t@n)) \mleq{} if if M n s then 0 else n + 1 fi \mleq{}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) => \mbot{}
else ind n s
(\mlambda{}t.(fix((\mlambda{}spector-bar-rec,n,s. if if M n s then 0 else n + 1 fi \mleq{}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) =>
\mbot{}
else ind n s (\mlambda{}t.(spector-bar-rec (n + 1) s.t@n))
fi ))
(n + 1)
s.t@n))
fi
By
Latex:
AssumeHasValue
Home
Index