---

Step * 2 of Lemma insert-int-1-1


1. T : Type
2. T ⊆r ℤ
3. u : T
4. v : T List
5. ∀[bs:T List]
     (∀[x:T]. v = bs ∈ (T List) supposing insert-int(x;v) = insert-int(x;bs) ∈ (T List)) supposing 
        (sorted(bs) and 
        sorted(v))
6. sorted([u / v])
7. sorted([])
8. x : T
9. insert-int(x;[u / v]) = insert-int(x;[]) ∈ (T List)
⊢ [u / v] = [] ∈ (T List)
BY
{ ((ApFunToHypEquands `Z' ⌜||Z||⌝ ⌜ℤ⌝ (-1)⋅ THENA Auto)
   THEN (RWO "length-insert-int" (-1) THENA Auto)
   THEN Reduce  (-1)
   THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  \mBbbZ{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[bs:T  List]
          (\mforall{}[x:T].  v  =  bs  supposing  insert-int(x;v)  =  insert-int(x;bs))  supposing 
                (sorted(bs)  and 
                sorted(v))
6.  sorted([u  /  v])
7.  sorted([])
8.  x  :  T
9.  insert-int(x;[u  /  v])  =  insert-int(x;[])
\mvdash{}  [u  /  v]  =  []


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}||Z||\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO  "length-insert-int"  (-1)  THENA  Auto)
  THEN  Reduce    (-1)
  THEN  Auto')

---

Home Index