---

Step * 2 of Lemma pairs-fpf_property


1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
6. no_repeats(A;fpf-domain(fpf(L)))
⊢ ∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
BY
{ ((Unfolds ``fpf-domain pairs-fpf`` 0
    THEN Reduce 0
    THEN (InstLemma `remove-repeats_property` [⌈A⌉; ⌈eq1⌉; ⌈map(λp.(fst(p));L)⌉])⋅)
   THENA Auto
   ) }

1
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
6. no_repeats(A;fpf-domain(fpf(L)))
7. no_repeats(A;remove-repeats(eq1;map(λp.(fst(p));L)))
∧ (∀a:A. ((a ∈ remove-repeats(eq1;map(λp.(fst(p));L))) ⇐⇒ (a ∈ map(λp.(fst(p));L))))
⊢ ∀a:A. ((a ∈ remove-repeats(eq1;map(λp.(fst(p));L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))

---

Latex:



1.  [A]  :  Type
2.  [B]  :  Type
3.  eq1  :  EqDecider(A)@i
4.  eq2  :  EqDecider(B)@i
5.  L  :  (A  \mtimes{}  B)  List@i
6.  no\_repeats(A;fpf-domain(fpf(L)))
\mvdash{}  \mforall{}a:A.  ((a  \mmember{}  fpf-domain(fpf(L)))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:B.  (<a,  b>  \mmember{}  L))


By

((Unfolds  ``fpf-domain  pairs-fpf``  0
    THEN  Reduce  0
    THEN  (InstLemma  `remove-repeats\_property`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}eq1\mkleeneclose{};  \mkleeneopen{}map(\mlambda{}p.(fst(p));L)\mkleeneclose{}])\mcdot{})
  THENA  Auto
  )

---

Home Index