Step
*
1
1
of Lemma
sq-decider-list-deq
1. eq : Base
2. sq-decider(eq)
3. j : ℤ
4. 0 < j
5. ∀x,y:Base.
((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in λL.(fix((λlist_ind@0,L. eval v = L in
if v is a pair then let b,bs' = v
in (eq a b) ∧b (list_ind as' bs')
otherwise if v = Ax then ff otherwise ⊥))
L) otherwise if v = Ax then λL.null(L) otherwise ⊥^j - 1
⊥
x
y)↓
⇒ (∀z:Base. ((list-deq(eq) x y ~ inl z) ⇒ (Ax ∈ x ~ y))))
6. x : Base
7. y : Base
8. (eval v = x in
if v is a pair
then let a,as' = v
in λL.(fix((λlist_ind@0,L. eval v = L in
if v is a pair
then let b,bs' = v
in (eq a b)
∧b (λlist_ind,L. eval v = L in
if v is a pair
then let a,as' = v
in λL.(fix((λlist_ind@0,L. eval v = L in
if v is a pair
then let b,bs' = v
in (eq a b)
∧b (list_ind as'
bs')
otherwise if v = Ax then ff
otherwise ⊥))
L) otherwise if v = Ax then λL.null(L)
otherwise ⊥^j - 1
⊥
as'
bs') otherwise if v = Ax then ff otherwise ⊥))
L) otherwise if v = Ax then λL.null(L) otherwise ⊥
y)↓
9. z : Base
10. list-deq(eq) x y ~ inl z
⊢ x ~ y
BY
{ (Assert (x)↓ BY
((Assert (list-deq(eq) x y)↓ BY
(HypSubst' (-1) 0 THEN Auto))
THEN RepUR ``list-deq`` -1
THEN RecUnfold `list_ind` (-1)
THEN Reduce (-1)
THEN RepeatFor 2 (HasValueD (-1))
THEN Auto)) }
1
1. eq : Base
2. sq-decider(eq)
3. j : ℤ
4. 0 < j
5. ∀x,y:Base.
((λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in λL.(fix((λlist_ind@0,L. eval v = L in
if v is a pair then let b,bs' = v
in (eq a b) ∧b (list_ind as' bs')
otherwise if v = Ax then ff otherwise ⊥))
L) otherwise if v = Ax then λL.null(L) otherwise ⊥^j - 1
⊥
x
y)↓
⇒ (∀z:Base. ((list-deq(eq) x y ~ inl z) ⇒ (Ax ∈ x ~ y))))
6. x : Base
7. y : Base
8. (eval v = x in
if v is a pair
then let a,as' = v
in λL.(fix((λlist_ind@0,L. eval v = L in
if v is a pair
then let b,bs' = v
in (eq a b)
∧b (λlist_ind,L. eval v = L in
if v is a pair
then let a,as' = v
in λL.(fix((λlist_ind@0,L. eval v = L in
if v is a pair
then let b,bs' = v
in (eq a b)
∧b (list_ind as'
bs')
otherwise if v = Ax then ff
otherwise ⊥))
L) otherwise if v = Ax then λL.null(L)
otherwise ⊥^j - 1
⊥
as'
bs') otherwise if v = Ax then ff otherwise ⊥))
L) otherwise if v = Ax then λL.null(L) otherwise ⊥
y)↓
9. z : Base
10. list-deq(eq) x y ~ inl z
11. (x)↓
⊢ x ~ y
Latex:
Latex:
1. eq : Base
2. sq-decider(eq)
3. j : \mBbbZ{}
4. 0 < j
5. \mforall{}x,y:Base.
((\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in \mlambda{}L.(fix((\mlambda{}list$_{ind@0}$,L. eval v = L\000C in
if v is a pair then let b,bs' = v
in (eq a b)
\mwedge{}\msubb{} (list\mbackslash{}ff2\000C4_{ind}$
as'
bs')
otherwise if v = Ax then ff
otherwise \mbot{}))
L) otherwise if v = Ax then \mlambda{}L.null(L) otherwise \mbot{}\^{}j -\000C 1
\mbot{}
x
y)\mdownarrow{}
{}\mRightarrow{} (\mforall{}z:Base. ((list-deq(eq) x y \msim{} inl z) {}\mRightarrow{} (Ax \mmember{} x \msim{} y))))
6. x : Base
7. y : Base
8. (eval v = x in
if v is a pair
then let a,as' = v
in \mlambda{}L.(fix((\mlambda{}list$_{ind@0}$,L.
eval v = L in
if v is a pair
then let b,bs' = v
in (eq a b)
\mwedge{}\msubb{} (\mlambda{}list$_{ind}$,L.
eval v = L in
if v is a pair
then let a,as' = v
in \mlambda{}L.(fix((\mlambda{}list$_{ind@0\mbackslash{}\000Cff7d$,L. ...))
L)
otherwise if v = Ax then \mlambda{}L.null(L)
otherwise \mbot{}\^{}j - 1
\mbot{}
as'
bs') otherwise if v = Ax then ff otherwise \mbot{}))
L) otherwise if v = Ax then \mlambda{}L.null(L) otherwise \mbot{}
y)\mdownarrow{}
9. z : Base
10. list-deq(eq) x y \msim{} inl z
\mvdash{} x \msim{} y
By
Latex:
(Assert (x)\mdownarrow{} BY
((Assert (list-deq(eq) x y)\mdownarrow{} BY
(HypSubst' (-1) 0 THEN Auto))
THEN RepUR ``list-deq`` -1
THEN RecUnfold `list\_ind` (-1)
THEN Reduce (-1)
THEN RepeatFor 2 (HasValueD (-1))
THEN Auto))
Home
Index