---

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


1. T : Type
2. T ⊆r ℤ
3. u : T
4. v : T List
5. sorted([])
6. sorted([u / v])
7. x : T
8. insert-int(x;[]) = insert-int(x;[u / v]) ∈ (T List)
9. ∀[x:T]. [] = v ∈ (T List) supposing insert-int(x;[]) = insert-int(x;v) ∈ (T List) supposing sorted(v)
⊢ [] = [u / v] ∈ (T List)
BY
{ ((ApFunToHypEquands `Z' ⌜||Z||⌝ ⌜ℤ⌝ (-2)⋅ 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.  sorted([])
6.  sorted([u  /  v])
7.  x  :  T
8.  insert-int(x;[])  =  insert-int(x;[u  /  v])
9.  \mforall{}[x:T].  []  =  v  supposing  insert-int(x;[])  =  insert-int(x;v)  supposing  sorted(v)
\mvdash{}  []  =  [u  /  v]


By

---

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

---

Home Index