Step
*
1
1
1
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. (fix((λlist_ind@0,L. eval v = L in
if v is a pair
then let b,bs' = v
in (eq (fst(x)) 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 ⊥\000C))
L) otherwise if v = Ax then λL.null(L) otherwise ⊥^j - 1
⊥
(snd(x))
bs') otherwise if v = Ax then ff otherwise ⊥))
y)↓
9. z : Base
10. list-deq(eq) <fst(x), snd(x)> y ~ inl z
11. 0 ≤ 0
12. x ~ <fst(x), snd(x)>
⊢ <fst(x), snd(x)> ~ y
BY
{ (RW (AddrC [1] UnrollRecursionC) 8 THEN Reduce 8) }
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 = y in
if v is a pair then let b,bs' = v
in (eq (fst(x)) 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
⊥
(snd(x))
bs') otherwise if v = Ax then ff otherwise ⊥)↓
9. z : Base
10. list-deq(eq) <fst(x), snd(x)> y ~ inl z
11. 0 ≤ 0
12. x ~ <fst(x), snd(x)>
⊢ <fst(x), snd(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. (fix((\mlambda{}list$_{ind@0}$,L. eval v = L in
if v is a pair
then let b,bs' = v
in (eq (fst(x)) 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}$,\000CL. eval v = L in
if v is a pair
then let b,bs' = v
in (eq a b)
\mwedge{}\msubb{} (list$\mbackslash{}\000Cff5f{ind}$
as'
bs')
otherwise if v = Ax
then ff
otherwise \mbot{})\000C)
L) otherwise if v = Ax then \mlambda{}L.null(L)
otherwise \mbot{}\^{}j - 1
\mbot{}
(snd(x))
bs') otherwise if v = Ax then ff otherwise \mbot{}))
y)\mdownarrow{}
9. z : Base
10. list-deq(eq) <fst(x), snd(x)> y \msim{} inl z
11. 0 \mleq{} 0
12. x \msim{} <fst(x), snd(x)>
\mvdash{} <fst(x), snd(x)> \msim{} y
By
Latex:
(RW (AddrC [1] UnrollRecursionC) 8 THEN Reduce 8)
Home
Index