---

Step * 1 2 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) ∧b (as' ≡b (bs \ a1))) ⇐⇒ [a1 / as'] ≡(|s|) bs
BY
{ ((RW assert_pushdownC 0 THENA Auto) THEN (RWH (HypC 4) 0 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
⊢ (↑(a1 ∈b bs)) ∧ (as' ≡(|s|) (bs \ a1)) ⇐⇒ [a1 / as'] ≡(|s|) bs

---

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{}\msubb{}  (as'  \mequiv{}\msubb{}  (bs  \mbackslash{}  a1)))  \mLeftarrow{}{}\mRightarrow{}  [a1  /  as']  \mequiv{}(|s|)  bs


By

---

Latex:
((RW  assert\_pushdownC  0  THENA  Auto)  THEN  (RWH  (HypC  4)  0  THENA  Auto))

---

Home Index