---

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


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))
BY
{ (ParallelLast
   THEN RWW "frs-increasing-sorted-by<" (-1)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN OnMaybeHyp 9 (\h. ((With ⌜i⌝ (D h)⋅ THENA Auto)
                           THEN D (-1)
                           THEN RenameVar `j' (-2)
                           THEN (With ⌜j⌝ (D 0)⋅ THENM D -1)
                           THEN Auto
                           THEN RelRST
                           THEN Auto))) }

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}  List
2.  q  :  \mBbbR{}  List
3.  frs-increasing(p)
4.  frs-increasing(q)
5.  frs-separated(p;q)
6.  \mforall{}sb:\mBbbR{}  List
          ((\mforall{}a,b:\mBbbR{}.    ((a  \mmember{}  p)  {}\mRightarrow{}  (b  \mmember{}  sb)  {}\mRightarrow{}  ((a  <  b)  \mvee{}  (b  <  a))))
          {}\mRightarrow{}  sorted-by(\mlambda{}\msubtwo{}x  y.x  <  y;p)
          {}\mRightarrow{}  sorted-by(\mlambda{}\msubtwo{}x  y.x  <  y;sb)
          {}\mRightarrow{}  (\mexists{}sc:\mBbbR{}  List.  (sorted-by(\mlambda{}\msubtwo{}x  y.x  <  y;sc)  \mwedge{}  p  \msubseteq{}  sc  \mwedge{}  sb  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  p  @  sb)))
7.  \mexists{}sc:\mBbbR{}  List.  (sorted-by(\mlambda{}\msubtwo{}x  y.x  <  y;sc)  \mwedge{}  p  \msubseteq{}  sc  \mwedge{}  q  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  p  @  q)
\mvdash{}  \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:
(ParallelLast
  THEN  RWW  "frs-increasing-sorted-by<"  (-1)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  OnMaybeHyp  9  (\mbackslash{}h.  ((With  \mkleeneopen{}i\mkleeneclose{}  (D  h)\mcdot{}  THENA  Auto)
                                                  THEN  D  (-1)
                                                  THEN  RenameVar  `j'  (-2)
                                                  THEN  (With  \mkleeneopen{}j\mkleeneclose{}  (D  0)\mcdot{}  THENM  D  -1)
                                                  THEN  Auto
                                                  THEN  RelRST
                                                  THEN  Auto)))

---

Home Index