Step
*
4
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. (if L is a pair then let a,as' = L
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 L = Ax then tt otherwise ⊥)↓
7. (L)↓
⊢ if L is a pair then let a,as' = L
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 L = 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
{ (Repeat (HVimplies2 0 [1])
THEN BotDiv
THEN Try (Complete ((RW UnrollLoopsC 0 THEN Reduce 0 THEN Auto)))
THEN HasValueD (-3)
THEN GenerateHasValue [2] (-1)
THEN HasValueD (-1)
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.
(\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. (if L is a pair then let a,as' = L
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$_{in\000Cd}$ as')
otherwise if v = Ax then tt otherwise \mbot{}\^{}j - 1
\mbot{}
as') otherwise if L = Ax then tt otherwise \mbot{})\mdownarrow{}
7. (L)\mdownarrow{}
\mvdash{} if L is a pair then let a,as' = L
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 L = 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:
(Repeat (HVimplies2 0 [1])
THEN BotDiv
THEN Try (Complete ((RW UnrollLoopsC 0 THEN Reduce 0 THEN Auto)))
THEN HasValueD (-3)
THEN GenerateHasValue [2] (-1)
THEN HasValueD (-1)
THEN RW (AddrC [2] UnrollLoopsC) 0
THEN Reduce 0
THEN InstEta (-1)
THEN AllReduce
THEN Try (Complete (Auto)))
Home
Index