---

Step * 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
⊢ y before z ∈ L ∨ (z = y ∈ T)
BY
{ (InstLemma `before-adjacent` [⌜T⌝;⌜L⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THENA 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)
⊢ 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
\mvdash{}  y  before  z  \mmember{}  L  \mvee{}  (z  =  y)


By

---

Latex:
(InstLemma  `before-adjacent`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index