### 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)` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` deq: `EqDecider(T)` 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`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` member: `t ∈ T` pairs-fpf: `fpf(L)` fpf-domain: `fpf-domain(f)` pi1: `fst(t)` top: `Top` iff: `P `⇐⇒` Q` implies: `P `` Q` prop: `ℙ` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` squash: `↓T` pi2: `snd(t)` true: `True` fpf-all: `∀x∈dom(f). v=f(x) ``  P[x; v]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` fpf-ap: `f(x)` eqof: `eqof(d)` deq: `EqDecider(T)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` not: `¬A` false: `False` or: `P ∨ Q` guard: `{T}` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  list_wf deq_wf remove-repeats_property map_wf pi1_wf_top member_map l_member_wf remove-repeats_wf exists_wf equal_wf pi2_wf squash_wf true_wf assert_wf fpf-dom_wf pairs-fpf_wf subtype-fpf2 top_wf list_induction no_repeats_wf reduce_wf ifthenelse_wf insert_wf nil_wf reduce_nil_lemma no_repeats_nil reduce_cons_lemma bool_wf equal-wf-T-base no_repeats-insert bnot_wf not_wf eqof_wf uiff_transitivity eqtt_to_assert safe-assert-deq 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 member-insert subtype_rel_product bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot cons_member cons_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut independent_pairFormation hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin productEquality cumulativity hypothesisEquality universeEquality sqequalRule dependent_functionElimination lambdaEquality productElimination independent_pairEquality isect_memberEquality voidElimination voidEquality allFunctionality independent_functionElimination promote_hyp dependent_pairFormation hyp_replacement equalitySymmetry applyEquality imageElimination equalityTransitivity natural_numberEquality imageMemberEquality baseClosed because_Cache independent_isectElimination setElimination rename unionElimination equalityElimination addLevel impliesFunctionality levelHypothesis inlFormation inrFormation dependent_set_memberEquality applyLambdaEquality orFunctionality instantiate

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

Date html generated: 2018_05_21-PM-09_32_00
Last ObjectModification: 2018_02_09-AM-10_26_47

Theory : finite!partial!functions

Home Index