Step
*
1
2
of Lemma
member-insert
1. [T] : Type
2. eq : EqDecider(T)
3. a : T
4. L : T List
5. b : T
6. ¬(a ∈ L)
⊢ (b ∈ insert(a;L))
⇐⇒ (b = a ∈ T) ∨ (b ∈ L)
BY
{ Subst ⌜insert(a;L) ~ [a / L]⌝ 0⋅ }
1
.....equality.....
1. T : Type
2. eq : EqDecider(T)
3. a : T
4. L : T List
5. b : T
6. ¬(a ∈ L)
⊢ insert(a;L) ~ [a / L]
2
1. [T] : Type
2. eq : EqDecider(T)
3. a : T
4. L : T List
5. b : T
6. ¬(a ∈ L)
⊢ (b ∈ [a / L])
⇐⇒ (b = a ∈ T) ∨ (b ∈ L)
Latex:
Latex:
1. [T] : Type
2. eq : EqDecider(T)
3. a : T
4. L : T List
5. b : T
6. \mneg{}(a \mmember{} L)
\mvdash{} (b \mmember{} insert(a;L)) \mLeftarrow{}{}\mRightarrow{} (b = a) \mvee{} (b \mmember{} L)
By
Latex:
Subst \mkleeneopen{}insert(a;L) \msim{} [a / L]\mkleeneclose{} 0\mcdot{}
Home
Index