Step
*
1
2
1
2
of Lemma
remove-first-no_repeats-member
1. [T] : Type
2. P : T ⟶ 𝔹@i
3. ∀a,b:T.  ((↑(P a)) 
⇒ (↑(P b)) 
⇒ (a = b ∈ T))
4. u : T@i
5. ¬↑(P u)
6. v : T List@i
7. no_repeats(T;v) ∧ (¬(u ∈ v))
8. x : T@i
9. (x ∈ remove-first(P;v)) 
⇐⇒ (x ∈ v) ∧ (↑¬b(P x))
⊢ (x ∈ [u / remove-first(P;v)]) 
⇐⇒ (x ∈ [u / v]) ∧ (↑¬b(P x))
BY
{ (RWO "cons_member" 0 THEN Auto)⋅ }
1
1. [T] : Type
2. P : T ⟶ 𝔹@i
3. ∀a,b:T.  ((↑(P a)) 
⇒ (↑(P b)) 
⇒ (a = b ∈ T))
4. u : T@i
5. ¬↑(P u)
6. v : T List@i
7. no_repeats(T;v)
8. ¬(u ∈ v)
9. x : T@i
10. (x ∈ remove-first(P;v)) 
⇒ ((x ∈ v) ∧ (↑¬b(P x)))
11. (x ∈ remove-first(P;v)) 
⇐ (x ∈ v) ∧ (↑¬b(P x))
12. (x = u ∈ T) ∨ (x ∈ remove-first(P;v))
⊢ (x = u ∈ T) ∨ (x ∈ v)
2
1. T : Type
2. P : T ⟶ 𝔹@i
3. ∀a,b:T.  ((↑(P a)) 
⇒ (↑(P b)) 
⇒ (a = b ∈ T))
4. u : T@i
5. ¬↑(P u)
6. v : T List@i
7. no_repeats(T;v)
8. ¬(u ∈ v)
9. x : T@i
10. (x ∈ remove-first(P;v)) 
⇒ ((x ∈ v) ∧ (↑¬b(P x)))
11. (x ∈ remove-first(P;v)) 
⇐ (x ∈ v) ∧ (↑¬b(P x))
12. (x = u ∈ T) ∨ (x ∈ remove-first(P;v))
⊢ ¬↑(P x)
3
1. [T] : Type
2. P : T ⟶ 𝔹@i
3. ∀a,b:T.  ((↑(P a)) 
⇒ (↑(P b)) 
⇒ (a = b ∈ T))
4. u : T@i
5. ¬↑(P u)
6. v : T List@i
7. no_repeats(T;v)
8. ¬(u ∈ v)
9. x : T@i
10. (x ∈ remove-first(P;v)) 
⇒ ((x ∈ v) ∧ (↑¬b(P x)))
11. (x ∈ remove-first(P;v)) 
⇐ (x ∈ v) ∧ (↑¬b(P x))
12. (x = u ∈ T) ∨ (x ∈ v)
13. ↑¬b(P x)
⊢ (x = u ∈ T) ∨ (x ∈ remove-first(P;v))
Latex:
Latex:
1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}@i
3.  \mforall{}a,b:T.    ((\muparrow{}(P  a))  {}\mRightarrow{}  (\muparrow{}(P  b))  {}\mRightarrow{}  (a  =  b))
4.  u  :  T@i
5.  \mneg{}\muparrow{}(P  u)
6.  v  :  T  List@i
7.  no\_repeats(T;v)  \mwedge{}  (\mneg{}(u  \mmember{}  v))
8.  x  :  T@i
9.  (x  \mmember{}  remove-first(P;v))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  v)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x))
\mvdash{}  (x  \mmember{}  [u  /  remove-first(P;v)])  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  [u  /  v])  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x))
By
Latex:
(RWO  "cons\_member"  0  THEN  Auto)\mcdot{}
Home
Index