Step
*
3
of Lemma
not-bl-exists-eq-bl-all
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
(¬b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
L) ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in (¬bP[a]) ∧b (list_ind as')
otherwise if v = Ax then tt otherwise ⊥))
L)
4. P : Base@i
5. L : Base@i
6. is-exception(case eval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥
of inl() =>
ff
| inr() =>
tt)
7. is-exception(eval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥)
⊢ ¬beval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
if v is a pair
then let a,as' = v
in (¬bP[a])
∧b (list_ind as')
otherwise if v = Ax then tt
otherwise ⊥))
L
BY
{ ExceptionCases (-1) }
1
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
(¬b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
L) ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in (¬bP[a]) ∧b (list_ind as')
otherwise if v = Ax then tt otherwise ⊥))
L)
4. P : Base@i
5. L : Base@i
6. is-exception(case eval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥
of inl() =>
ff
| inr() =>
tt)
7. is-exception(eval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥)
8. (L)↓
⊢ ¬beval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
if v is a pair
then let a,as' = v
in (¬bP[a])
∧b (list_ind as')
otherwise if v = Ax then tt
otherwise ⊥))
L
2
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
(¬b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
L) ≤ fix((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in (¬bP[a]) ∧b (list_ind as')
otherwise if v = Ax then tt otherwise ⊥))
L)
4. P : Base@i
5. L : Base@i
6. is-exception(case eval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥
of inl() =>
ff
| inr() =>
tt)
7. is-exception(eval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥)
8. is-exception(L)
⊢ ¬beval v = L in
if v is a pair then let a,as' = v
in P[a]
∨b(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] ∨b(list_ind as')
otherwise if v = Ax then ff otherwise ⊥^j - 1
⊥
as') otherwise if v = Ax then ff otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
if v is a pair
then let a,as' = v
in (¬bP[a])
∧b (list_ind as')
otherwise if v = Ax then tt
otherwise ⊥))
L
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}P,L:Base.
(\mneg{}\msubb{}(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] \mvee{}\msubb{}(list$_{ind}$ as')
otherwise if v = Ax then ff otherwise \mbot{}\^{}j - 1
\mbot{}
L) \mleq{} fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in (\mneg{}\msubb{}P[a]) \mwedge{}\msubb{} (list$_{ind}$ \000Cas')
otherwise if v = Ax then tt otherwise \mbot{}))
L)
4. P : Base@i
5. L : Base@i
6. is-exception(case eval v = L in
if v is a pair then let a,as' = v
in P[a]
\mvee{}\msubb{}(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in P[a]
\mvee{}\msubb{}(list$_\mbackslash{}\000Cff7bind}$ as')
otherwise if v = Ax then ff otherwise \mbot{}\^{}j\000C - 1
\mbot{}
as') otherwise if v = Ax then ff otherwise \mbot{}
of inl() =>
ff
| inr() =>
tt)
7. is-exception(eval v = L in
if v is a pair then let a,as' = v
in P[a]
\mvee{}\msubb{}(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] \mvee{}\msubb{}(list$_\mbackslash{}\000Cff7bind}$ as')
otherwise if v = Ax then ff otherwise \mbot{}\^{}j - 1
\mbot{}
as') otherwise if v = Ax then ff otherwise \mbot{})
\mvdash{} \mneg{}\msubb{}eval v = L in
if v is a pair then let a,as' = v
in P[a]
\mvee{}\msubb{}(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in P[a] \mvee{}\msubb{}(list$_{ind}\000C$ as')
otherwise if v = Ax then ff otherwise \mbot{}\^{}j - 1
\mbot{}
as') otherwise if v = Ax then ff otherwise \mbot{}
\mleq{} fix((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in (\mneg{}\msubb{}P[a]) \mwedge{}\msubb{} (list$_{ind}$ as')
otherwise if v = Ax then tt otherwise \mbot{}))
L
By
Latex:
ExceptionCases (-1)
Home
Index