---

Step * 2 of Lemma member-fpf-vals2


1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. f : x:A fp-> B[x]
6. x : {a:A| ↑(P a)} 
7. v : B[x]
8. (<x, v> ∈ fpf-vals(eq;P;f))
9. {((↑x ∈ dom(f)) ∧ (↑(P x))) ∧ (v = f(x) ∈ B[x])}
⊢ <Ax, Ax> ∈ {(↑x ∈ dom(f)) ∧ (v = f(x) ∈ B[x])}
BY
{ (DVar `x' THEN D (-1) THEN Unfold `guard` 0 THEN Auto) }

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  B  :  A  {}\mrightarrow{}  Type
4.  P  :  A  {}\mrightarrow{}  \mBbbB{}
5.  f  :  x:A  fp->  B[x]
6.  x  :  \{a:A|  \muparrow{}(P  a)\} 
7.  v  :  B[x]
8.  (<x,  v>  \mmember{}  fpf-vals(eq;P;f))
9.  \{((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}(P  x)))  \mwedge{}  (v  =  f(x))\}
\mvdash{}  <Ax,  Ax>  \mmember{}  \{(\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (v  =  f(x))\}


By

(DVar  `x'  THEN  D  (-1)  THEN  Unfold  `guard`  0  THEN  Auto)

---

Home Index