Step
*
1
of Lemma
no_repeats-before-equality
1. T : Type
2. as : T List
3. bs : T List
4. no_repeats(T;as)
5. no_repeats(T;bs)
6. ∀x:T. ((x ∈ as) 
⇐⇒ (x ∈ bs))
7. ∀x,y:T.  (x before y ∈ as 
⇐⇒ x before y ∈ bs)
⊢ as = bs ∈ (T List)
BY
{ xxx((RepeatFor 5 ((MoveToConcl (-1))))⋅ THEN (ListInd (-1)) THEN InductionOnList THEN Auto)xxx }
1
1. T : Type
2. u : T
3. v : T List
4. no_repeats(T;[])
5. no_repeats(T;[u / v])
6. ∀x:T. ((x ∈ []) 
⇐⇒ (x ∈ [u / v]))
7. ∀x,y:T.  (x before y ∈ [] 
⇐⇒ x before y ∈ [u / v])
8. no_repeats(T;v)
⇒ (∀x:T. ((x ∈ []) 
⇐⇒ (x ∈ v)))
⇒ (∀x,y:T.  (x before y ∈ [] 
⇐⇒ x before y ∈ v))
⇒ ([] = v ∈ (T List))
⊢ [] = [u / v] ∈ (T List)
2
1. T : Type
2. u : T
3. v : T List
4. ∀bs:T List
     (no_repeats(T;v)
     
⇒ no_repeats(T;bs)
     
⇒ (∀x:T. ((x ∈ v) 
⇐⇒ (x ∈ bs)))
     
⇒ (∀x,y:T.  (x before y ∈ v 
⇐⇒ x before y ∈ bs))
     
⇒ (v = bs ∈ (T List)))
5. no_repeats(T;[u / v])
6. no_repeats(T;[])
7. ∀x:T. ((x ∈ [u / v]) 
⇐⇒ (x ∈ []))
8. ∀x,y:T.  (x before y ∈ [u / v] 
⇐⇒ x before y ∈ [])
⊢ [u / v] = [] ∈ (T List)
3
1. T : Type
2. u : T
3. v : T List
4. ∀bs:T List
     (no_repeats(T;v)
     
⇒ no_repeats(T;bs)
     
⇒ (∀x:T. ((x ∈ v) 
⇐⇒ (x ∈ bs)))
     
⇒ (∀x,y:T.  (x before y ∈ v 
⇐⇒ x before y ∈ bs))
     
⇒ (v = bs ∈ (T List)))
5. u1 : T
6. v1 : T List
7. no_repeats(T;[u / v])
8. no_repeats(T;[u1 / v1])
9. ∀x:T. ((x ∈ [u / v]) 
⇐⇒ (x ∈ [u1 / v1]))
10. ∀x,y:T.  (x before y ∈ [u / v] 
⇐⇒ x before y ∈ [u1 / v1])
11. no_repeats(T;v1)
⇒ (∀x:T. ((x ∈ [u / v]) 
⇐⇒ (x ∈ v1)))
⇒ (∀x,y:T.  (x before y ∈ [u / v] 
⇐⇒ x before y ∈ v1))
⇒ ([u / v] = v1 ∈ (T List))
⊢ [u / v] = [u1 / v1] ∈ (T List)
Latex:
Latex:
1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  no\_repeats(T;as)
5.  no\_repeats(T;bs)
6.  \mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs))
7.  \mforall{}x,y:T.    (x  before  y  \mmember{}  as  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  bs)
\mvdash{}  as  =  bs
By
Latex:
xxx((RepeatFor  5  ((MoveToConcl  (-1))))\mcdot{}  THEN  (ListInd  (-1))  THEN  InductionOnList  THEN  Auto)xxx
Home
Index