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)`
`3. [B] : A ⟶ Type`
`4. P : A ⟶ 𝔹`
`5. d : A List`
`6. f1 : x:{x:A| (x ∈ d)}  ⟶ B[x]`
`7. x : A`
`8. v : B[x]`
`9. L : A List`
`10. remove-repeats(eq;d) = L ∈ (A List)`
`⊢ (<x, v> ∈ zip(filter(P;L);map(f1;filter(P;L)))) `⇐⇒` {((↑x ∈b L) ∧ (↑(P x))) ∧ (v = (f1 x) ∈ B[x])}`

Latex:

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

Latex:
(((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