---

Step * 1 1 1 1 2 1 2 of Lemma merge-strict-exists


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
7. u1 : T
8. v1 : T List
9. (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ v1) ⇒ ((R a b) ∨ (R b a))))
⇒ (sorted-by(R;v) ∧ (∀z∈v.R u z))
⇒ sorted-by(R;v1)
⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ v1 ⊆ sc ∧ sc ⊆ [u / v] @ v1))
10. ∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a)))
11. sorted-by(R;v)
12. (∀z∈v.R u z)
13. sorted-by(R;v1)
14. (∀z∈v1.R u1 z)
15. R u u1
16. sc : T List
17. sorted-by(R;sc)
18. v ⊆ sc
19. [u1 / v1] ⊆ sc
20. sorted-by(R;sc)
21. i : ℕ||sc||
22. (sc[i] ∈ [u1 / v1])
⊢ R u sc[i]
BY
{ ((RWO "cons_member" (-1) THENM D -1) THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
7. u1 : T
8. v1 : T List
9. (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ v1) ⇒ ((R a b) ∨ (R b a))))
⇒ (sorted-by(R;v) ∧ (∀z∈v.R u z))
⇒ sorted-by(R;v1)
⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ v1 ⊆ sc ∧ sc ⊆ [u / v] @ v1))
10. ∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a)))
11. sorted-by(R;v)
12. (∀z∈v.R u z)
13. sorted-by(R;v1)
14. (∀z∈v1.R u1 z)
15. R u u1
16. sc : T List
17. sorted-by(R;sc)
18. v ⊆ sc
19. [u1 / v1] ⊆ sc
20. sorted-by(R;sc)
21. i : ℕ||sc||
22. (sc[i] ∈ v1)
⊢ R u sc[i]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  Trans(T;a,b.R  a  b)
4.  u  :  T
5.  v  :  T  List
6.  \mforall{}sb:T  List
          ((\mforall{}a,b:T.    ((a  \mmember{}  v)  {}\mRightarrow{}  (b  \mmember{}  sb)  {}\mRightarrow{}  ((R  a  b)  \mvee{}  (R  b  a))))
          {}\mRightarrow{}  sorted-by(R;v)
          {}\mRightarrow{}  sorted-by(R;sb)
          {}\mRightarrow{}  (\mexists{}sc:T  List.  (sorted-by(R;sc)  \mwedge{}  v  \msubseteq{}  sc  \mwedge{}  sb  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  v  @  sb)))
7.  u1  :  T
8.  v1  :  T  List
9.  (\mforall{}a,b:T.    ((a  \mmember{}  [u  /  v])  {}\mRightarrow{}  (b  \mmember{}  v1)  {}\mRightarrow{}  ((R  a  b)  \mvee{}  (R  b  a))))
{}\mRightarrow{}  (sorted-by(R;v)  \mwedge{}  (\mforall{}z\mmember{}v.R  u  z))
{}\mRightarrow{}  sorted-by(R;v1)
{}\mRightarrow{}  (\mexists{}sc:T  List.  (sorted-by(R;sc)  \mwedge{}  [u  /  v]  \msubseteq{}  sc  \mwedge{}  v1  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  [u  /  v]  @  v1))
10.  \mforall{}a,b:T.    ((a  \mmember{}  [u  /  v])  {}\mRightarrow{}  (b  \mmember{}  [u1  /  v1])  {}\mRightarrow{}  ((R  a  b)  \mvee{}  (R  b  a)))
11.  sorted-by(R;v)
12.  (\mforall{}z\mmember{}v.R  u  z)
13.  sorted-by(R;v1)
14.  (\mforall{}z\mmember{}v1.R  u1  z)
15.  R  u  u1
16.  sc  :  T  List
17.  sorted-by(R;sc)
18.  v  \msubseteq{}  sc
19.  [u1  /  v1]  \msubseteq{}  sc
20.  sorted-by(R;sc)
21.  i  :  \mBbbN{}||sc||
22.  (sc[i]  \mmember{}  [u1  /  v1])
\mvdash{}  R  u  sc[i]


By

---

Latex:
((RWO  "cons\_member"  (-1)  THENM  D  -1)  THEN  Auto)

---

Home Index