---

Step * of Lemma member-fpf-vals

∀[A:Type]
  ∀eq:EqDecider(A)
    ∀[B:A ─→ Type]
      ∀P:A ─→ 𝔹. ∀f:x:A fp-> B[x]. ∀x:A. ∀v:B[x].
        ((<x, v> ∈ fpf-vals(eq;P;f)) ⇐⇒ {((↑x ∈ dom(f)) ∧ (↑(P x))) ∧ (v = f(x) ∈ B[x])})
BY
{ (((UnivCD THENA Auto)
    THEN DVar `f'
    THEN RepUR ``fpf-vals let fpf-dom fpf-ap`` 0
    THEN Subst ⌈x ∈b d) ~ x ∈b remove-repeats(eq;d))⌉ 0⋅)
   THENL [(Auto
           THEN (BLemma `iff_imp_equal_bool` THENM RW assert_pushdownC 0 THENM (RWO "member-remove-repeats" 0)⋅)
           THEN Auto)
         ; (GenConcl ⌈remove-repeats(eq;d) = L ∈ (A List)⌉⋅ THENA Auto)]
) }

1
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. P : A ─→ 𝔹@i
5. d : A List@i
6. f1 : x:{x:A| (x ∈ d)}  ─→ B[x]@i
7. x : A@i
8. v : B[x]@i
9. L : A List@i
10. remove-repeats(eq;d) = L ∈ (A List)@i
⊢ (<x, v> ∈ zip(filter(P;L);map(f1;filter(P;L)))) ⇐⇒ {((↑x ∈b L)) ∧ (↑(P x))) ∧ (v = (f1 x) ∈ B[x])}

---

Latex:


\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A)
        \mforall{}[B:A  {}\mrightarrow{}  Type]
            \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:x:A  fp->  B[x].  \mforall{}x:A.  \mforall{}v:B[x].
                ((<x,  v>  \mmember{}  fpf-vals(eq;P;f))  \mLeftarrow{}{}\mRightarrow{}  \{((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}(P  x)))  \mwedge{}  (v  =  f(x))\})


By

(((UnivCD  THENA  Auto)
    THEN  DVar  `f'
    THEN  RepUR  ``fpf-vals  let  fpf-dom  fpf-ap``  0
    THEN  Subst  \mkleeneopen{}x  \mmember{}\msubb{}  d)  \msim{}  x  \mmember{}\msubb{}  remove-repeats(eq;d))\mkleeneclose{}  0\mcdot{})
  THENL  [(Auto
                  THEN  (BLemma  `iff\_imp\_equal\_bool`
                              THENM  RW  assert\_pushdownC  0
                              THENM  (RWO  "member-remove-repeats"  0)\mcdot{})
                  THEN  Auto)
              ;  (GenConcl  \mkleeneopen{}remove-repeats(eq;d)  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)]
)

---

Home Index