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 (InductionOnList) THEN Auto) }

1
1. Type
2. T ⊆r ℤ
3. T
4. List
5. sorted([])
6. sorted([u v])
7. 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. Type
2. T ⊆r ℤ
3. T
4. List
5. ∀[bs:T List]
     (∀[x:T]. 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. T
9. insert-int(x;[u v]) insert-int(x;[]) ∈ (T List)
⊢ [u v] [] ∈ (T List)

3
1. Type
2. T ⊆r ℤ
3. T
4. List
5. ∀[bs:T List]
     (∀[x:T]. 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 List
8. sorted([u v])
9. sorted([u1 v1])
10. 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