Nuprl Lemma : fpf-vals-nil

[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]]. ∀[a:A].
  (fpf-vals(eq;P;f) []) supposing ((∀b:A. (↑(P b) ⇐⇒ a ∈ A)) and (¬↑a ∈ dom(f)))


Definitions occuring in Statement :  fpf-vals: fpf-vals(eq;P;f) fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] nil: [] deq: EqDecider(T) assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A apply: a function: x:A ⟶ B[x] universe: Type sqequal: t equal: t ∈ T
Definitions unfolded in proof :  fpf-vals: fpf-vals(eq;P;f) let: let fpf: a:A fp-> B[a] pi1: fst(t) pi2: snd(t) member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B uimplies: supposing a all: x:A. B[x] top: Top prop: implies:  Q bool: 𝔹 unit: Unit it: btrue: tt iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q ifthenelse: if then else fi  bfalse: ff not: ¬A false: False uiff: uiff(P;Q) exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b fpf-dom: x ∈ dom(f) cons: [a b]
Lemmas referenced :  all_wf iff_wf assert_wf equal_wf not_wf fpf-dom_wf subtype-fpf2 top_wf fpf_wf bool_wf deq_wf deq-member_wf equal-wf-T-base l_member_wf bnot_wf cons_wf nil_wf iff_transitivity iff_weakening_uiff eqtt_to_assert assert-deq-member eqff_to_assert assert_of_bnot list_wf nil_member false_wf filter_nil_lemma no_repeats_wf cons_member filter_cons_lemma no_repeats_cons uiff_transitivity or_wf list_induction filter_wf5 subtype_rel_dep_function subtype_rel_self set_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot and_wf remove-repeats_wf remove-repeats-no_repeats remove-repeats_property zip_nil_lemma list-cases equal-wf-base product_subtype_list null_nil_lemma btrue_wf null_wf3 subtype_rel_list null_cons_lemma bfalse_wf btrue_neq_bfalse
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalHypSubstitution productElimination thin sqequalRule cut introduction extract_by_obid isectElimination cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality hypothesis because_Cache independent_isectElimination lambdaFormation isect_memberEquality voidElimination voidEquality functionEquality universeEquality isect_memberFormation sqequalAxiom equalityTransitivity equalitySymmetry baseClosed unionElimination equalityElimination independent_functionElimination independent_pairFormation dependent_functionElimination impliesFunctionality hyp_replacement applyLambdaEquality promote_hyp setEquality setElimination rename dependent_pairFormation instantiate dependent_set_memberEquality inrFormation inlFormation hypothesis_subsumption

\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:x:A  fp->  B[x]].  \mforall{}[a:A].
    (fpf-vals(eq;P;f)  \msim{}  [])  supposing  ((\mforall{}b:A.  (\muparrow{}(P  b)  \mLeftarrow{}{}\mRightarrow{}  b  =  a))  and  (\mneg{}\muparrow{}a  \mmember{}  dom(f)))

Date html generated: 2018_05_21-PM-09_26_18
Last ObjectModification: 2018_02_09-AM-10_21_46

Theory : finite!partial!functions

Home Index