---

Step * 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)
⊢ y before z ∈ L ∨ (z = y ∈ T)
BY
{ (FLemma `l_before_antisymmetry` [8] THEN Auto) }

1
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)

---

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)
\mvdash{}  y  before  z  \mmember{}  L  \mvee{}  (z  =  y)


By

---

Latex:
(FLemma  `l\_before\_antisymmetry`  [8]  THEN  Auto)

---

Home Index