Step
*
2
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. 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 ⊥ ∈ Top + Top
⊢ ¬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
{ (GenerateHasValue [2] (-1)
THEN HasValueD (-1)
THEN Repeat (HVimplies2 0 [1;1])
THEN BotDiv
THEN Try (Complete ((RW UnrollLoopsC 0 THEN Reduce 0 THEN Auto)))
THEN HasValueD (-3)
THEN RW (AddrC [2] UnrollLoopsC) 0
THEN Reduce 0
THEN InstEta (-1)
THEN AllReduce
THEN Try (Complete (Auto))) }
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. 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}\mbackslash{}\000Cff24 as')
otherwise if v = Ax then ff otherwise \mbot{}\^{}j - 1
\mbot{}
as') otherwise if v = Ax then ff otherwise \mbot{} \mmember{} Top + Top
\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:
(GenerateHasValue [2] (-1)
THEN HasValueD (-1)
THEN Repeat (HVimplies2 0 [1;1])
THEN BotDiv
THEN Try (Complete ((RW UnrollLoopsC 0 THEN Reduce 0 THEN Auto)))
THEN HasValueD (-3)
THEN RW (AddrC [2] UnrollLoopsC) 0
THEN Reduce 0
THEN InstEta (-1)
THEN AllReduce
THEN Try (Complete (Auto)))
Home
Index