---

Step * 1 1 1 1 1 2 2 1 2 of Lemma assert-nonneg-monomial


1. n : ℕ
2. u : ℤ
3. u1 : ℤ
4. v : ℤ List
5. ∀L1:ℤ List
     (||L1|| < ||[u; [u1 / v]]||
     ⇒ sorted(L1)
     ⇒ (↑even-int-list(L1))
     ⇒ (∃u:{vs:ℤ List| sorted(vs)} . (L1 = merge-int-accum(u;u) ∈ (ℤ List))))
6. sorted([u; [u1 / v]])
7. u = u1 ∈ ℤ
8. ↑even-int-list(v)
9. ∃u:{vs:ℤ List| sorted(vs)} . (v = merge-int-accum(u;u) ∈ (ℤ List))
⊢ ∃u@0:{vs:ℤ List| sorted(vs)} . ([u; [u1 / v]] = merge-int-accum(u@0;u@0) ∈ (ℤ List))
BY
{ (D -1
   THEN (Assert [u / u2] ∈ {vs:ℤ List| sorted(vs)}  BY
               ((D -2 THEN MemTypeCD THEN Auto)
                THEN RWO "sorted-cons" 0
                THEN Auto
                THEN (Assert (∀z∈v.u ≤ z) BY
                            (HypSubst' 7 0 THEN RWW  "sorted-cons" 6 THEN Auto))
                THEN (RWO "l_all_iff" (-1) THENA Auto)
                THEN (RWO "l_all_iff" 0 THENA Auto)
                THEN RepeatFor 2 (ParallelLast)
                THEN HypSubst' (-5) 0
                THEN Lemmaize [-1]
                THEN Auto
                THEN (RWO "merge-int-accum-sq" 0 THENA Auto)
                THEN BLemma `member-merge-int`
                THEN Auto))
   THEN D 0 With ⌜[u / u2]⌝ 
   THEN Auto
   THEN HypSubst' (-2) 0
   THEN RevHypSubst' (-5) 0) }

1
1. n : ℕ
2. u : ℤ
3. u1 : ℤ
4. v : ℤ List
5. ∀L1:ℤ List
     (||L1|| < ||[u; [u1 / v]]||
     ⇒ sorted(L1)
     ⇒ (↑even-int-list(L1))
     ⇒ (∃u:{vs:ℤ List| sorted(vs)} . (L1 = merge-int-accum(u;u) ∈ (ℤ List))))
6. sorted([u; [u1 / v]])
7. u = u1 ∈ ℤ
8. ↑even-int-list(v)
9. u2 : {vs:ℤ List| sorted(vs)} 
10. v = merge-int-accum(u2;u2) ∈ (ℤ List)
11. [u / u2] ∈ {vs:ℤ List| sorted(vs)} 
⊢ [u; [u / merge-int-accum(u2;u2)]] = merge-int-accum([u / u2];[u / u2]) ∈ (ℤ List)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  u  :  \mBbbZ{}
3.  u1  :  \mBbbZ{}
4.  v  :  \mBbbZ{}  List
5.  \mforall{}L1:\mBbbZ{}  List
          (||L1||  <  ||[u;  [u1  /  v]]||
          {}\mRightarrow{}  sorted(L1)
          {}\mRightarrow{}  (\muparrow{}even-int-list(L1))
          {}\mRightarrow{}  (\mexists{}u:\{vs:\mBbbZ{}  List|  sorted(vs)\}  .  (L1  =  merge-int-accum(u;u))))
6.  sorted([u;  [u1  /  v]])
7.  u  =  u1
8.  \muparrow{}even-int-list(v)
9.  \mexists{}u:\{vs:\mBbbZ{}  List|  sorted(vs)\}  .  (v  =  merge-int-accum(u;u))
\mvdash{}  \mexists{}u@0:\{vs:\mBbbZ{}  List|  sorted(vs)\}  .  ([u;  [u1  /  v]]  =  merge-int-accum(u@0;u@0))


By

---

Latex:
(D  -1
  THEN  (Assert  [u  /  u2]  \mmember{}  \{vs:\mBbbZ{}  List|  sorted(vs)\}    BY
                          ((D  -2  THEN  MemTypeCD  THEN  Auto)
                            THEN  RWO  "sorted-cons"  0
                            THEN  Auto
                            THEN  (Assert  (\mforall{}z\mmember{}v.u  \mleq{}  z)  BY
                                                    (HypSubst'  7  0  THEN  RWW    "sorted-cons"  6  THEN  Auto))
                            THEN  (RWO  "l\_all\_iff"  (-1)  THENA  Auto)
                            THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  HypSubst'  (-5)  0
                            THEN  Lemmaize  [-1]
                            THEN  Auto
                            THEN  (RWO  "merge-int-accum-sq"  0  THENA  Auto)
                            THEN  BLemma  `member-merge-int`
                            THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}[u  /  u2]\mkleeneclose{} 
  THEN  Auto
  THEN  HypSubst'  (-2)  0
  THEN  RevHypSubst'  (-5)  0)

---

Home Index