Step
*
1
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. (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
BY
{ (HasValueD 8 THEN HVimplies2 8 [1]) }
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. ((eq (fst(x)) (fst(y)))
∧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))
(snd(y))))↓
9. z : Base
10. list-deq(eq) <fst(x), snd(x)> <fst(y), snd(y)> ~ inl z
11. 0 ≤ 0
12. x ~ <fst(x), snd(x)>
13. 0 ≤ 0
14. y ~ <fst(y), snd(y)>
⊢ <fst(x), snd(x)> ~ <fst(y), snd(y)>
2
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. (if y = 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)>
13. (y)↓
14. ∀a,b:Top. (if y is a pair then a otherwise b ~ b)
⊢ <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. (eval v = y 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}$,L. e\000Cval v = L in
if v is a pair
then let b,bs' = v
in (eq a b)
\mwedge{}\msubb{} (list$_\000C{ind}$ as'
bs')
otherwise if v = Ax
then ff
otherwise \mbot{}))
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{})\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:
(HasValueD 8 THEN HVimplies2 8 [1])
Home
Index