Step
*
5
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(eval v = L in
if v is a pair then let a,as' = v
in (¬bP[a])
∧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
⊥
as') otherwise if v = Ax then tt otherwise ⊥)
7. (L)↓
⊢ eval v = L in
if v is a pair then let a,as' = v
in (¬bP[a])
∧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
⊥
as') otherwise if v = Ax then tt otherwise ⊥ ≤ ¬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 ⊥))\000C
L)
BY
{ ((CallByValueReduceOn ⌜L⌝ 0⋅ THENA Auto)
THEN Repeat (HVimplies2 0 [1])
THEN Try (Complete ((RW UnrollLoopsC 0 THEN Reduce 0 THEN Auto)))) }
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((¬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)>)
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(eval v = L in
if v is a pair then let a,as' = v
in (\mneg{}\msubb{}P[a])
\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$_\mbackslash{}ff7\000Cbind}$ as')
otherwise if v = Ax then tt otherwise \mbot{}\^{}j - 1\000C
\mbot{}
as') otherwise if v = Ax then tt otherwise \mbot{})
7. (L)\mdownarrow{}
\mvdash{} eval v = L in
if v is a pair then let a,as' = v
in (\mneg{}\msubb{}P[a])
\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\mbackslash{}\000Cff7d$ as')
otherwise if v = Ax then tt otherwise \mbot{}\^{}j - 1
\mbot{}
as') otherwise if v = Ax then tt otherwise \mbot{}
\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)
By
Latex:
((CallByValueReduceOn \mkleeneopen{}L\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN Repeat (HVimplies2 0 [1])
THEN Try (Complete ((RW UnrollLoopsC 0 THEN Reduce 0 THEN Auto))))
Home
Index