---

Step * of Lemma insert-int-1-1

∀[T:Type]
  ∀[as,bs:T List].
    (∀[x:T]. as = bs ∈ (T List) supposing insert-int(x;as) = insert-int(x;bs) ∈ (T List)) supposing 
       (sorted(bs) and 
       sorted(as)) 
  supposing T ⊆r ℤ
BY
{ (RepeatFor 2 (InductionOnList) THEN Auto) }

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)

2
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)

3
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)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[as,bs:T  List].
        (\mforall{}[x:T].  as  =  bs  supposing  insert-int(x;as)  =  insert-int(x;bs))  supposing 
              (sorted(bs)  and 
              sorted(as)) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Auto)

---

Home Index