---

Step * 2 2 1 1 1 1 of Lemma assert-bag-all


1. T : Type
2. p : T ⟶ 𝔹
3. x : T
4. u : T
5. v : T List
6. (x ∈ v) ⇒ (↑reduce(λx,y. (x ∧b y);tt;map(λx.p[x];v))) ⇒ p[x] = tt
7. (x ∈ [u / v])
8. ↑(p[u] ∧b reduce(λx,y. (x ∧b y);tt;map(λx.p[x];v)))
⊢ p[x] = tt
BY
{ (RW assert_pushdownC (-1) THEN Auto) }

1
1. T : Type
2. p : T ⟶ 𝔹
3. x : T
4. u : T
5. v : T List
6. (x ∈ v) ⇒ (↑reduce(λx,y. (x ∧b y);tt;map(λx.p[x];v))) ⇒ p[x] = tt
7. (x ∈ [u / v])
8. ↑p[u]
9. ↑reduce(λx,y. (x ∧b y);tt;map(λx.p[x];v))
⊢ p[x] = tt

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  u  :  T
5.  v  :  T  List
6.  (x  \mmember{}  v)  {}\mRightarrow{}  (\muparrow{}reduce(\mlambda{}x,y.  (x  \mwedge{}\msubb{}  y);tt;map(\mlambda{}x.p[x];v)))  {}\mRightarrow{}  p[x]  =  tt
7.  (x  \mmember{}  [u  /  v])
8.  \muparrow{}(p[u]  \mwedge{}\msubb{}  reduce(\mlambda{}x,y.  (x  \mwedge{}\msubb{}  y);tt;map(\mlambda{}x.p[x];v)))
\mvdash{}  p[x]  =  tt


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index