---

Step * 1 1 1 of Lemma detach_msubset


1. s : DSet
2. a : MSet{s}
3. b : MSet{s}
4. ∀x:|s|. ((x #∈ a) ≤ (x #∈ b))
5. x : |s|
⊢ (x #∈ b) = imax(x #∈ b;x #∈ a) ∈ ℤ
BY
{ ((With x (D 4)  
THENM RWO "imax_unfold" 0 
THENM SplitOnConclITE) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  MSet\{s\}
3.  b  :  MSet\{s\}
4.  \mforall{}x:|s|.  ((x  \#\mmember{}  a)  \mleq{}  (x  \#\mmember{}  b))
5.  x  :  |s|
\mvdash{}  (x  \#\mmember{}  b)  =  imax(x  \#\mmember{}  b;x  \#\mmember{}  a)


By

---

Latex:
((With  x  (D  4)   
THENM  RWO  "imax\_unfold"  0 
THENM  SplitOnConclITE)  THEN  Auto)

---

Home Index