---

Step * 7 of Lemma member-insert-combine2


1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. v : T List
8. ((∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = v ∈ (T List))
     ∧ (∀y∈l.cmp x y < 0)
     ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))
∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
⇒ (z ∈ insert-combine(cmp;f;x;v))
9. l : T List
10. l @ [z] ≤ [u / v]
11. (∀y∈l.cmp x y < 0)
12. cmp x z < 0
⊢ (z ∈ insert-combine(cmp;f;x;[u / v]))
BY
{ (RepUR ``insert-combine`` 0
   THEN Fold `insert-combine` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (AutoSplit)
   THEN SpList 0
   THEN Try (Complete (((Assert ⌜(u ∈ l @ [z])⌝⋅ THENA (DVar `l' THEN AllReduce THEN SpList (-4) THEN Auto))
                        THEN SpList (-1)
                        THEN D (-1)
                        THEN Try (Complete ((SimpleSubstVar `u' (-2) THEN Auto)))
                        THEN (RWO "l_all_iff" (-4) THENA Auto)
                        THEN InstHyp [⌜u⌝] (-4)⋅
                        THEN Auto)))
   THEN (DVar `l' THEN AllReduce)
   THEN SpList (-3)
   THEN Auto
   THEN SpList (-2)
   THEN RepD
   THEN (OrRight THENA Auto)
   THEN BackThruSomeHyp
   THEN (OrLeft THENA Auto)
   THEN InstConcl [⌜v1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
4.  x  :  T
5.  z  :  T
6.  u  :  T
7.  v  :  T  List
8.  ((\mexists{}l:T  List.  (l  @  [z]  \mleq{}  v  \mwedge{}  (\mforall{}y\mmember{}l.cmp  x  y  <  0)  \mwedge{}  cmp  x  z  <  0))
\mvee{}  (\mexists{}l,l':T  List
        \mexists{}a:T
          (((l  @  [a  /  l'])  =  v)
          \mwedge{}  (\mforall{}y\mmember{}l.cmp  x  y  <  0)
          \mwedge{}  ((0  <  cmp  x  a  \mwedge{}  (z  \mmember{}  [x;  [a  /  l']]))  \mvee{}  (((cmp  x  a)  =  0)  \mwedge{}  (z  \mmember{}  [f  x  a  /  l'])))))
\mvee{}  ((z  =  x)  \mwedge{}  (\mforall{}y\mmember{}v.cmp  x  y  <  0)))
{}\mRightarrow{}  (z  \mmember{}  insert-combine(cmp;f;x;v))
9.  l  :  T  List
10.  l  @  [z]  \mleq{}  [u  /  v]
11.  (\mforall{}y\mmember{}l.cmp  x  y  <  0)
12.  cmp  x  z  <  0
\mvdash{}  (z  \mmember{}  insert-combine(cmp;f;x;[u  /  v]))


By

---

Latex:
(RepUR  ``insert-combine``  0
  THEN  Fold  `insert-combine`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (AutoSplit)
  THEN  SpList  0
  THEN  Try  (Complete  (((Assert  \mkleeneopen{}(u  \mmember{}  l  @  [z])\mkleeneclose{}\mcdot{}
                                              THENA  (DVar  `l'  THEN  AllReduce  THEN  SpList  (-4)  THEN  Auto)
                                              )
                                            THEN  SpList  (-1)
                                            THEN  D  (-1)
                                            THEN  Try  (Complete  ((SimpleSubstVar  `u'  (-2)  THEN  Auto)))
                                            THEN  (RWO  "l\_all\_iff"  (-4)  THENA  Auto)
                                            THEN  InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-4)\mcdot{}
                                            THEN  Auto)))
  THEN  (DVar  `l'  THEN  AllReduce)
  THEN  SpList  (-3)
  THEN  Auto
  THEN  SpList  (-2)
  THEN  RepD
  THEN  (OrRight  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  (OrLeft  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index