---

Step * 2 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. (z ∈ insert-combine(cmp;f;x;v))
⇒ ((∃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)))
9. (z ∈ eval tst = cmp x u in
        if (tst =z 0) then [f x u / v]
        if 0 <z tst then [x; [u / v]]
        else [u / insert-combine(cmp;f;x;v)]
        fi )
⊢ (∃l:T List. (l @ [z] ≤ [u / v] ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = [u / 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∈[u / v].cmp x y < 0))
BY
{ (RepUR ``insert-combine`` (-1)
   THEN Fold `insert-combine` (-1)
   THEN (CallByValueReduce (-1) THENA Auto)
   THEN (SplitOnHypITE (-1) THENA Auto)
   THEN Try ((SplitOnHypITE (-2) THENA Auto))
   THEN Try (Complete (((OrRight THENA Auto)
                        THEN (OrLeft THENA Auto)
                        THEN InstConcl [⌜[]⌝;⌜v⌝;⌜u⌝]⋅
                        THEN Reduce 0
                        THEN Auto)))
   THEN SpList (-3)
   THEN (Assert ⌜cmp x u < 0⌝⋅ THENA Auto)
   THEN RepeatFor 2 (Thin (-2))
   THEN DProdsAndUnions
   THEN Try (Complete (((OrLeft THENA Auto)
                        THEN InstConcl [⌜[]⌝]⋅
                        THEN Reduce 0
                        THEN Auto
                        THEN SpList 0
                        THEN Auto'
                        THEN BLemma `nil_iseg`
                        THEN Auto)))
   THEN (D (-3) THENA Auto)
   THEN DProdsAndUnions
   THEN Try (Complete (((OrLeft THENA Auto)
                        THEN InstConcl [⌜[u / l]⌝]⋅
                        THEN Reduce 0
                        THEN Auto
                        THEN SpList 0
                        THEN Auto)))
   THEN Try (Complete (((OrRight THENA Auto)
                        THEN (OrLeft THENA Auto)
                        THEN InstConcl [⌜[u / l]⌝;⌜l'⌝;⌜a⌝]⋅
                        THEN Reduce 0
                        THEN Auto
                        THEN SpList 0
                        THEN Auto)))
   THEN Try (Complete ((RepeatFor 2 ((OrRight THENA Auto)) THEN SpList 0 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.  (z  \mmember{}  insert-combine(cmp;f;x;v))
{}\mRightarrow{}  ((\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)))
9.  (z  \mmember{}  eval  tst  =  cmp  x  u  in
                if  (tst  =\msubz{}  0)  then  [f  x  u  /  v]
                if  0  <z  tst  then  [x;  [u  /  v]]
                else  [u  /  insert-combine(cmp;f;x;v)]
                fi  )
\mvdash{}  (\mexists{}l:T  List.  (l  @  [z]  \mleq{}  [u  /  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'])  =  [u  /  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{}[u  /  v].cmp  x  y  <  0))


By

---

Latex:
(RepUR  ``insert-combine``  (-1)
  THEN  Fold  `insert-combine`  (-1)
  THEN  (CallByValueReduce  (-1)  THENA  Auto)
  THEN  (SplitOnHypITE  (-1)  THENA  Auto)
  THEN  Try  ((SplitOnHypITE  (-2)  THENA  Auto))
  THEN  Try  (Complete  (((OrRight  THENA  Auto)
                                            THEN  (OrLeft  THENA  Auto)
                                            THEN  InstConcl  [\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}
                                            THEN  Reduce  0
                                            THEN  Auto)))
  THEN  SpList  (-3)
  THEN  (Assert  \mkleeneopen{}cmp  x  u  <  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (Thin  (-2))
  THEN  DProdsAndUnions
  THEN  Try  (Complete  (((OrLeft  THENA  Auto)
                                            THEN  InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}
                                            THEN  Reduce  0
                                            THEN  Auto
                                            THEN  SpList  0
                                            THEN  Auto'
                                            THEN  BLemma  `nil\_iseg`
                                            THEN  Auto)))
  THEN  (D  (-3)  THENA  Auto)
  THEN  DProdsAndUnions
  THEN  Try  (Complete  (((OrLeft  THENA  Auto)
                                            THEN  InstConcl  [\mkleeneopen{}[u  /  l]\mkleeneclose{}]\mcdot{}
                                            THEN  Reduce  0
                                            THEN  Auto
                                            THEN  SpList  0
                                            THEN  Auto)))
  THEN  Try  (Complete  (((OrRight  THENA  Auto)
                                            THEN  (OrLeft  THENA  Auto)
                                            THEN  InstConcl  [\mkleeneopen{}[u  /  l]\mkleeneclose{};\mkleeneopen{}l'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
                                            THEN  Reduce  0
                                            THEN  Auto
                                            THEN  SpList  0
                                            THEN  Auto)))
  THEN  Try  (Complete  ((RepeatFor  2  ((OrRight  THENA  Auto))  THEN  SpList  0  THEN  Auto))))

---

Home Index