---

Step * 1 of Lemma assert_of_bpermr


1. s : DSet
2. as : |s| List
⊢ ∀bs:|s| List. (↑(as ≡b bs) ⇐⇒ as ≡(|s|) bs)
BY
{ ((New [`a'; `as\''] (ListInd 2) THEN RecCaseSplit `bpermr`) THEN (D 0 THENA Auto)) }

1
1. s : DSet
2. bs : |s| List
⊢ ↑null(bs) ⇐⇒ [] ≡(|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
⊢ ↑((a1 ∈b bs) ∧b (as' ≡b (bs \ a1))) ⇐⇒ [a1 / as'] ≡(|s|) bs

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  |s|  List
\mvdash{}  \mforall{}bs:|s|  List.  (\muparrow{}(as  \mequiv{}\msubb{}  bs)  \mLeftarrow{}{}\mRightarrow{}  as  \mequiv{}(|s|)  bs)


By

---

Latex:
((New  [`a';  `as\mbackslash{}'']  (ListInd  2)  THEN  RecCaseSplit  `bpermr`)  THEN  (D  0  THENA  Auto))

---

Home Index