---

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

.....subterm..... T:t
2:n
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. u1 : T
7. v1 : T List
8. sorted([u / v])
9. sorted([u1 / v1])
10. x : T
11. [u / insert-int(x;v)] = [u1 / insert-int(x;v1)] ∈ (T List)
12. ∀[x:T]. [u / v] = v1 ∈ (T List) supposing insert-int(x;[u / v]) = insert-int(x;v1) ∈ (T List) supposing sorted(v1)
13. u < x
14. u1 < x
15. u = u1 ∈ T
16. insert-int(x;v) = insert-int(x;v1) ∈ (T List)
⊢ v = v1 ∈ (T List)
BY
{ (∀h:hyp. FLemma `sorted-cons` [h]  THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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.  u1  :  T
7.  v1  :  T  List
8.  sorted([u  /  v])
9.  sorted([u1  /  v1])
10.  x  :  T
11.  [u  /  insert-int(x;v)]  =  [u1  /  insert-int(x;v1)]
12.  \mforall{}[x:T].  [u  /  v]  =  v1  supposing  insert-int(x;[u  /  v])  =  insert-int(x;v1)  supposing  sorted(v1)
13.  u  <  x
14.  u1  <  x
15.  u  =  u1
16.  insert-int(x;v)  =  insert-int(x;v1)
\mvdash{}  v  =  v1


By

---

Latex:
(\mforall{}h:hyp.  FLemma  `sorted-cons`  [h]    THEN  Auto)

---

Home Index