---

Step * 1 1 1 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;[u / v])
⇒ 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;[u / v])
12. sorted-by(R;[u1 / v1])
⊢ ∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ [u1 / v1] ⊆ sc ∧ sc ⊆ [u / v] @ [u1 / v1])
BY
{ ((InstHyp [⌜u⌝;⌜u1⌝] (-3)⋅ THENM D -1) THENA (Auto THEN With ⌜0⌝ (D 0)⋅ THEN Auto THEN Reduce 0 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;[u / v])
⇒ 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;[u / v])
12. sorted-by(R;[u1 / v1])
13. R u u1
⊢ ∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ [u1 / v1] ⊆ sc ∧ sc ⊆ [u / v] @ [u1 / v1])

2
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;[u / v])
⇒ 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;[u / v])
12. sorted-by(R;[u1 / v1])
13. R u1 u
⊢ ∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ [u1 / v1] ⊆ sc ∧ sc ⊆ [u / v] @ [u1 / v1])

---

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;[u  /  v])
{}\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;[u  /  v])
12.  sorted-by(R;[u1  /  v1])
\mvdash{}  \mexists{}sc:T  List.  (sorted-by(R;sc)  \mwedge{}  [u  /  v]  \msubseteq{}  sc  \mwedge{}  [u1  /  v1]  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  [u  /  v]  @  [u1  /  v1])


By

---

Latex:
((InstHyp  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}u1\mkleeneclose{}]  (-3)\mcdot{}  THENM  D  -1)
  THENA  (Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  Auto')
  )

---

Home Index