---

Step * 2 of Lemma not_mem_remove1


1. s : DSet
2. a : |s|
3. u : |s|
4. v : |s| List
5. (¬↑(a ∈b v)) ⇒ ((v \ a) = v ∈ (|s| List))
⊢ (¬↑((u (=b) a) ∨b(a ∈b v))) ⇒ (if u (=b) a then v else [u / (v \ a)] fi  = [u / v] ∈ (|s| List))
BY
{ (((SplitOnConclITE) THENA Auto)  THEN AbReduce 0 THEN ((D 0) THENA Auto) THEN Try (EqCD) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  u  :  |s|
4.  v  :  |s|  List
5.  (\mneg{}\muparrow{}(a  \mmember{}\msubb{}  v))  {}\mRightarrow{}  ((v  \mbackslash{}  a)  =  v)
\mvdash{}  (\mneg{}\muparrow{}((u  (=\msubb{})  a)  \mvee{}\msubb{}(a  \mmember{}\msubb{}  v)))  {}\mRightarrow{}  (if  u  (=\msubb{})  a  then  v  else  [u  /  (v  \mbackslash{}  a)]  fi    =  [u  /  v])


By

---

Latex:
(((SplitOnConclITE)  THENA  Auto)    THEN  AbReduce  0  THEN  ((D  0)  THENA  Auto)  THEN  Try  (EqCD)  THEN  Auto)

---

Home Index