---

Step * 3 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. u1 : T
7. v1 : T List
8. sorted([u / v])
9. sorted([u1 / v1])
10. x : T
11. insert-int(x;[u / v]) = insert-int(x;[u1 / 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)
⊢ [u / v] = [u1 / v1] ∈ (T List)
BY
{ ((RWO  "insert-int-cons" (-2) THENA Auto)
   THEN (SplitOnHypITE -2  THENA Auto)
   THEN (SplitOnHypITE -3  THENA Auto)
   THEN FLemma `cons_one_one` [-4]
   THEN Auto
   THEN EqCD
   THEN Auto) }

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)

---

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


By

---

Latex:
((RWO    "insert-int-cons"  (-2)  THENA  Auto)
  THEN  (SplitOnHypITE  -2    THENA  Auto)
  THEN  (SplitOnHypITE  -3    THENA  Auto)
  THEN  FLemma  `cons\_one\_one`  [-4]
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index