---

Step * 1 2 1 of Lemma assert_of_bpermr


1. s : DSet
2. a1 : |s|
3. as' : |s| List
4. a : ∀bs:|s| List. (↑(as' ≡b bs) ⇐⇒ as' ≡(|s|) bs)
5. bs : |s| List
⊢ (↑(a1 ∈b bs)) ∧ (as' ≡(|s|) (bs \ a1)) ⇐⇒ [a1 / as'] ≡(|s|) bs
BY
{ ((Unfold `and` 0 THEN Fold `cand` 0) THEN ((D 0 THEN UnivCD) THENA Auto)) }

1
1. s : DSet
2. a1 : |s|
3. as' : |s| List
4. a : ∀bs:|s| List. (↑(as' ≡b bs) ⇐⇒ as' ≡(|s|) bs)
5. bs : |s| List
6. (↑(a1 ∈b bs)) c∧ (as' ≡(|s|) (bs \ a1))
⊢ [a1 / as'] ≡(|s|) bs

2
1. s : DSet
2. a1 : |s|
3. as' : |s| List
4. a : ∀bs:|s| List. (↑(as' ≡b bs) ⇐⇒ as' ≡(|s|) bs)
5. bs : |s| List
6. [a1 / as'] ≡(|s|) bs
⊢ (↑(a1 ∈b bs)) c∧ (as' ≡(|s|) (bs \ a1))

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a1  :  |s|
3.  as'  :  |s|  List
4.  a  :  \mforall{}bs:|s|  List.  (\muparrow{}(as'  \mequiv{}\msubb{}  bs)  \mLeftarrow{}{}\mRightarrow{}  as'  \mequiv{}(|s|)  bs)
5.  bs  :  |s|  List
\mvdash{}  (\muparrow{}(a1  \mmember{}\msubb{}  bs))  \mwedge{}  (as'  \mequiv{}(|s|)  (bs  \mbackslash{}  a1))  \mLeftarrow{}{}\mRightarrow{}  [a1  /  as']  \mequiv{}(|s|)  bs


By

---

Latex:
((Unfold  `and`  0  THEN  Fold  `cand`  0)  THEN  ((D  0  THEN  UnivCD)  THENA  Auto))

---

Home Index