---

Step * 1 of Lemma iseg-transition-lemma


1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. L : T List
4. x : T
5. ∃L1:T List. (L1 ≤ L @ [x] ∧ P[L1])
6. ¬(∃L1:T List. (L1 ≤ L ∧ P[L1]))
⊢ P[L @ [x]]
BY
{ (((ExRepD THEN (RWO "iseg_append_iff" (-3))) THENA Auto) THEN (D (-3))) }

1
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. L : T List
4. x : T
5. L1 : T List
6. L1 ≤ L
7. P[L1]
8. ¬(∃L1:T List. (L1 ≤ L ∧ P[L1]))
⊢ P[L @ [x]]

2
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. L : T List
4. x : T
5. L1 : T List
6. ∃l:T List. (0 < ||l|| ∧ (L1 = (L @ l) ∈ (T List)) ∧ l ≤ [x])
7. P[L1]
8. ¬(∃L1:T List. (L1 ≤ L ∧ P[L1]))
⊢ P[L @ [x]]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  L  :  T  List
4.  x  :  T
5.  \mexists{}L1:T  List.  (L1  \mleq{}  L  @  [x]  \mwedge{}  P[L1])
6.  \mneg{}(\mexists{}L1:T  List.  (L1  \mleq{}  L  \mwedge{}  P[L1]))
\mvdash{}  P[L  @  [x]]


By

---

Latex:
(((ExRepD  THEN  (RWO  "iseg\_append\_iff"  (-3)))  THENA  Auto)  THEN  (D  (-3)))

---

Home Index