---

Step * 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)))
⊢ ∀sb:T List
    ((∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
    ⇒ sorted-by(R;[u / v])
    ⇒ sorted-by(R;sb)
    ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ [u / v] @ sb)))
BY
{ (InductionOnList
   THEN Try ((Auto
              THEN Reduce 0
              THEN With ⌜[u / v]⌝ (D 0)⋅
              THEN Auto
              THEN (RWW "append-nil" 0 THENA Auto)
              THEN Try ((BLemma `l_contains_nil` THEN Auto))
              THEN BLemma `l_contains_weakening`
              THEN Complete (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))
⊢ (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a))))
⇒ sorted-by(R;[u / v])
⇒ sorted-by(R;[u1 / v1])
⇒ (∃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)))
\mvdash{}  \mforall{}sb:T  List
        ((\mforall{}a,b:T.    ((a  \mmember{}  [u  /  v])  {}\mRightarrow{}  (b  \mmember{}  sb)  {}\mRightarrow{}  ((R  a  b)  \mvee{}  (R  b  a))))
        {}\mRightarrow{}  sorted-by(R;[u  /  v])
        {}\mRightarrow{}  sorted-by(R;sb)
        {}\mRightarrow{}  (\mexists{}sc:T  List.  (sorted-by(R;sc)  \mwedge{}  [u  /  v]  \msubseteq{}  sc  \mwedge{}  sb  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  [u  /  v]  @  sb)))


By

---

Latex:
(InductionOnList
  THEN  Try  ((Auto
                        THEN  Reduce  0
                        THEN  With  \mkleeneopen{}[u  /  v]\mkleeneclose{}  (D  0)\mcdot{}
                        THEN  Auto
                        THEN  (RWW  "append-nil"  0  THENA  Auto)
                        THEN  Try  ((BLemma  `l\_contains\_nil`  THEN  Auto))
                        THEN  BLemma  `l\_contains\_weakening`
                        THEN  Complete  (Auto)))
  )

---

Home Index