---

Step * of Lemma pairs-fpf_property

∀[A,B:Type].
  ∀eq1:EqDecider(A). ∀eq2:EqDecider(B). ∀L:(A × B) List.
    (no_repeats(A;fpf-domain(fpf(L)))
    ∧ (∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L)))
    ∧ ∀a∈dom(fpf(L)). l=fpf(L)(a) ⇒  no_repeats(B;l) ∧ (∀b:B. ((b ∈ l) ⇐⇒ (<a, b> ∈ L))))
BY
{ ((UnivCD THENA Auto) THEN BetterSplitAndConcl) }

1
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
⊢ no_repeats(A;fpf-domain(fpf(L)))

2
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))

3
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. ∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
⊢ ∀a∈dom(fpf(L)). l=fpf(L)(a) ⇒  no_repeats(B;l) ∧ (∀b:B. ((b ∈ l) ⇐⇒ (<a, b> ∈ L)))

---

Latex:


\mforall{}[A,B:Type].
    \mforall{}eq1:EqDecider(A).  \mforall{}eq2:EqDecider(B).  \mforall{}L:(A  \mtimes{}  B)  List.
        (no\_repeats(A;fpf-domain(fpf(L)))
        \mwedge{}  (\mforall{}a:A.  ((a  \mmember{}  fpf-domain(fpf(L)))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:B.  (<a,  b>  \mmember{}  L)))
        \mwedge{}  \mforall{}a\mmember{}dom(fpf(L)).  l=fpf(L)(a)  {}\mRightarrow{}    no\_repeats(B;l)  \mwedge{}  (\mforall{}b:B.  ((b  \mmember{}  l)  \mLeftarrow{}{}\mRightarrow{}  (<a,  b>  \mmember{}  L))))


By

((UnivCD  THENA  Auto)  THEN  BetterSplitAndConcl)

---

Home Index