---

Step * 3 1 of Lemma pairs-fpf_property


1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)
4. eq2 : EqDecider(B)
5. L : (A × B) List
6. no_repeats(A;fpf-domain(fpf(L)))
7. ∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
8. a : A
9. ↑a ∈ dom(fpf(L))
⊢ no_repeats(B;fpf(L)(a))
BY
{ xxx(Unfolds ``fpf-ap pairs-fpf`` 0 THEN Reduce 0)xxx }

1
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)
4. eq2 : EqDecider(B)
5. L : (A × B) List
6. no_repeats(A;fpf-domain(fpf(L)))
7. ∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
8. a : A
9. ↑a ∈ dom(fpf(L))
⊢ no_repeats(B;reduce(λp,l. if eqof(eq1) (fst(p)) a then insert(snd(p);l) else l fi ;[];L))

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(Unfolds  ``fpf-ap  pairs-fpf``  0  THEN  Reduce  0)xxx

---

Home Index