### Nuprl 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))))`

Proof

Definitions occuring in Statement :  pairs-fpf: `fpf(L)` fpf-all: `∀x∈dom(f). v=f(x) ``  P[x; v]` fpf-domain: `fpf-domain(f)` deq: `EqDecider(T)` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` pair: `<a, b>` product: `x:A × B[x]` universe: `Type`
Lemmas :  list_wf deq_wf remove-repeats_property map_wf member_map l_member_wf remove-repeats_wf exists_wf squash_wf true_wf assert_wf fpf-dom_wf pairs-fpf_wf subtype-fpf2 top_wf subtype_top list_induction no_repeats_wf reduce_wf bool_wf eqtt_to_assert safe-assert-deq insert_wf nil_wf reduce_nil_lemma no_repeats_nil reduce_cons_lemma equal-wf-T-base equal_wf no_repeats-insert bnot_wf not_wf eqof_wf uiff_transitivity iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot all_wf iff_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse or_wf and_wf pi2_wf member-insert pi1_wf_top subtype_rel_product bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot cons_member cons_wf
\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))))

Date html generated: 2015_07_17-AM-11_16_34
Last ObjectModification: 2015_01_28-AM-07_39_13

Home Index