Step
*
1
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. ((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)>
BY
{ Subst' list-deq(eq) <fst(x), snd(x)> <fst(y), snd(y)> ~ (eq (fst(x)) (fst(y))) ∧b (list-deq(eq) (snd(x)) (snd(y))) 10 \000C}
1
.....equality.....
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)>
⊢ list-deq(eq) <fst(x), snd(x)> <fst(y), snd(y)> ~ (eq (fst(x)) (fst(y))) ∧b (list-deq(eq) (snd(x)) (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. ((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. (eq (fst(x)) (fst(y))) ∧b (list-deq(eq) (snd(x)) (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)>
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. ((eq (fst(x)) (fst(y)))
\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. eval v = L in
if v is a pair then let b,bs' = v
in (eq a b) \mwedge{}\msubb{} (list$_\mbackslash{}ff\000C7bind}$ 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))
(snd(y))))\mdownarrow{}
9. z : Base
10. list-deq(eq) <fst(x), snd(x)> <fst(y), snd(y)> \msim{} inl z
11. 0 \mleq{} 0
12. x \msim{} <fst(x), snd(x)>
13. 0 \mleq{} 0
14. y \msim{} <fst(y), snd(y)>
\mvdash{} <fst(x), snd(x)> \msim{} <fst(y), snd(y)>
By
Latex:
Subst' list-deq(eq) <fst(x), snd(x)> <fst(y), snd(y)> \msim{} (eq (fst(x)) (fst(y))) \mwedge{}\msubb{} (list-deq(eq) (snd\000C(x)) (snd(y))) 10
Home
Index