---

Step * of Lemma frs-increasing-separated-common-refinement

∀p,q:ℝ List.
  (frs-increasing(p)
  ⇒ frs-increasing(q)
  ⇒ frs-separated(p;q)
  ⇒ (∃r:ℝ List. (frs-increasing(r) ∧ frs-refines(r;p) ∧ frs-refines(r;q) ∧ frs-refines(p @ q;r))))
BY
{ (Auto
   THEN (InstLemma `merge-strict-exists` [⌜ℝ⌝;⌜λ2x y.x < y⌝;⌜p⌝]⋅ THENA (Auto THEN D 0 THEN Auto THEN RelRST THEN Auto))
   THEN InstHyp [⌜q⌝] (-1)⋅
   THEN Auto
   THEN RWW "frs-increasing-sorted-by<" 0
   THEN Auto) }

1
1. p : ℝ List
2. q : ℝ List
3. frs-increasing(p)
4. frs-increasing(q)
5. frs-separated(p;q)
6. ∀sb:ℝ List
     ((∀a,b:ℝ.  ((a ∈ p) ⇒ (b ∈ sb) ⇒ ((a < b) ∨ (b < a))))
     ⇒ sorted-by(λ2x y.x < y;p)
     ⇒ sorted-by(λ2x y.x < y;sb)
     ⇒ (∃sc:ℝ List. (sorted-by(λ2x y.x < y;sc) ∧ p ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ p @ sb)))
7. a : ℝ
8. b : ℝ
9. (a ∈ p)
10. (b ∈ q)
⊢ (a < b) ∨ (b < a)

2
1. p : ℝ List
2. q : ℝ List
3. frs-increasing(p)
4. frs-increasing(q)
5. frs-separated(p;q)
6. ∀sb:ℝ List
     ((∀a,b:ℝ.  ((a ∈ p) ⇒ (b ∈ sb) ⇒ ((a < b) ∨ (b < a))))
     ⇒ sorted-by(λ2x y.x < y;p)
     ⇒ sorted-by(λ2x y.x < y;sb)
     ⇒ (∃sc:ℝ List. (sorted-by(λ2x y.x < y;sc) ∧ p ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ p @ sb)))
7. ∃sc:ℝ List. (sorted-by(λ2x y.x < y;sc) ∧ p ⊆ sc ∧ q ⊆ sc ∧ sc ⊆ p @ q)
⊢ ∃r:ℝ List. (frs-increasing(r) ∧ frs-refines(r;p) ∧ frs-refines(r;q) ∧ frs-refines(p @ q;r))

---

Latex:

---

Latex:
\mforall{}p,q:\mBbbR{}  List.
    (frs-increasing(p)
    {}\mRightarrow{}  frs-increasing(q)
    {}\mRightarrow{}  frs-separated(p;q)
    {}\mRightarrow{}  (\mexists{}r:\mBbbR{}  List.  (frs-increasing(r)  \mwedge{}  frs-refines(r;p)  \mwedge{}  frs-refines(r;q)  \mwedge{}  frs-refines(p  @  q;r))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `merge-strict-exists`  [\mkleeneopen{}\mBbbR{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  <  y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Auto  THEN  RelRST  THEN  Auto)
              )
  THEN  InstHyp  [\mkleeneopen{}q\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  RWW  "frs-increasing-sorted-by<"  0
  THEN  Auto)

---

Home Index