Step
*
5
1
of Lemma
not-bl-exists-eq-bl-all
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
(λ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 ⊥^j - 1
⊥
L ≤ ¬b(fix((λ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 ⊥))
L))
4. P : Base@i
5. L : Base@i
6. is-exception((¬bP[fst(L)])
∧b (λ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 ⊥^j - 1
⊥
(snd(L))))
7. 0 ≤ 0
8. L ~ <fst(L), snd(L)>
⊢ (¬bP[fst(L)])
∧b (λ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 ⊥^j - 1
⊥
(snd(L))) ≤ ¬b(fix((λ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 ⊥))
<fst(L), snd(L)>)
BY
{ ExceptionCases (-3) }
1
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
(λ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 ⊥^j - 1
⊥
L ≤ ¬b(fix((λ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 ⊥))
L))
4. P : Base@i
5. L : Base@i
6. is-exception(case ¬bP[fst(L)]
of inl() =>
λ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 ⊥^j - 1
⊥
(snd(L))
| inr() =>
ff)
7. 0 ≤ 0
8. L ~ <fst(L), snd(L)>
9. ¬bP[fst(L)] ∈ Top + Top
⊢ (¬bP[fst(L)])
∧b (λ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 ⊥^j - 1
⊥
(snd(L))) ≤ ¬b(fix((λ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 ⊥))
<fst(L), snd(L)>)
2
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
(λ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 ⊥^j - 1
⊥
L ≤ ¬b(fix((λ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 ⊥))
L))
4. P : Base@i
5. L : Base@i
6. is-exception(case ¬bP[fst(L)]
of inl() =>
λ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 ⊥^j - 1
⊥
(snd(L))
| inr() =>
ff)
7. 0 ≤ 0
8. L ~ <fst(L), snd(L)>
9. is-exception(¬bP[fst(L)])
⊢ (¬bP[fst(L)])
∧b (λ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 ⊥^j - 1
⊥
(snd(L))) ≤ ¬b(fix((λ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 ⊥))
<fst(L), snd(L)>)
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}P,L:Base.
(\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{}\^{}j - 1
\mbot{}
L \mleq{} \mneg{}\msubb{}(fix((\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{}))
L))
4. P : Base@i
5. L : Base@i
6. is-exception((\mneg{}\msubb{}P[fst(L)])
\mwedge{}\msubb{} (\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{}\^{}j - 1
\mbot{}
(snd(L))))
7. 0 \mleq{} 0
8. L \msim{} <fst(L), snd(L)>
\mvdash{} (\mneg{}\msubb{}P[fst(L)])
\mwedge{}\msubb{} (\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{}\^{}j - 1
\mbot{}
(snd(L))) \mleq{} \mneg{}\msubb{}(fix((\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}\mbackslash{}ff2\000C4 as')
otherwise if v = Ax then ff otherwise \mbot{}))
<fst(L), snd(L)>)
By
Latex:
ExceptionCases (-3)
Home
Index