---

Step * 1 1 1 of Lemma before-adjacent2


1. [T] : Type
2. L : T List
3. x : T
4. y : T
5. no_repeats(T;L)
6. adjacent(T;L;x;y)
7. z : T
8. x before z ∈ L
9. (x ∈ L)
10. (y ∈ L)
11. (z ∈ L)
12. z before y ∈ L
13. z before x ∈ L ∨ (z = x ∈ T)
14. ¬z before x ∈ L
⊢ y before z ∈ L ∨ (z = y ∈ T)
BY
{ ((RWO "no_repeats_iff" 5 THEN Auto) THEN SplitOrHyps THEN Auto) }

1
1. [T] : Type
2. L : T List
3. x : T
4. y : T
5. ∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ L
6. adjacent(T;L;x;y)
7. z : T
8. x before z ∈ L
9. (x ∈ L)
10. (y ∈ L)
11. (z ∈ L)
12. z before y ∈ L
13. z = x ∈ T
14. ¬z before x ∈ L
⊢ y before z ∈ L ∨ (z = y ∈ T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  x  :  T
4.  y  :  T
5.  no\_repeats(T;L)
6.  adjacent(T;L;x;y)
7.  z  :  T
8.  x  before  z  \mmember{}  L
9.  (x  \mmember{}  L)
10.  (y  \mmember{}  L)
11.  (z  \mmember{}  L)
12.  z  before  y  \mmember{}  L
13.  z  before  x  \mmember{}  L  \mvee{}  (z  =  x)
14.  \mneg{}z  before  x  \mmember{}  L
\mvdash{}  y  before  z  \mmember{}  L  \mvee{}  (z  =  y)


By

---

Latex:
((RWO  "no\_repeats\_iff"  5  THEN  Auto)  THEN  SplitOrHyps  THEN  Auto)

---

Home Index