Nuprl Lemma : fpf-decompose

∀[A:Type]
  ∀eq:EqDecider(A)
    ∀[B:A ⟶ Type]
      ∀f:a:A fp-> B[a]
        ∃g:a:A fp-> B[a]
         ∃a:A
          ∃b:B[a]
           ((f ⊆ g ⊕ a : b ∧ g ⊕ a : b ⊆ f)
           ∧ (∀a':A. ¬(a' = a ∈ A) supposing ↑a' ∈ dom(g))
           ∧ ||fpf-domain(g)|| < ||fpf-domain(f)||) 
        supposing 0 < ||fpf-domain(f)||


Proof



Definitions occuring in Statement :  fpf-single: x : v,  fpf-join: f ⊕ g,  fpf-sub: f ⊆ g,  fpf-domain: fpf-domain(f),  fpf-dom: x ∈ dom(f),  fpf: a:A fp-> B[a],  length: ||as||,  deq: EqDecider(T),  assert: ↑b,  less_than: a < b,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  so_apply: x[s],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  not: ¬A,  and: P ∧ Q,  function: x:A ⟶ B[x],  natural_number: $n,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  rev_implies: P ⇐ Q,  uiff: uiff(P;Q),  iff: P ⇐⇒ Q,  cons: [a / b],  less_than': less_than'(a;b),  bfalse: ff,  ifthenelse: if b then t else f fi ,  assert: ↑b,  fpf-dom: x ∈ dom(f),  eqof: eqof(d),  pi1: fst(t),  fpf-domain: fpf-domain(f),  fpf: a:A fp-> B[a],  le: A ≤ B,  prop: ℙ,  false: False,  exists: ∃x:A. B[x],  satisfiable_int_formula: satisfiable_int_formula(fmla),  implies: P ⇒ Q,  not: ¬A,  and: P ∧ Q,  squash: ↓T,  less_than: a < b,  or: P ∨ Q,  decidable: Dec(P),  ge: i ≥ j ,  top: Top,  so_apply: x[s],  so_lambda: λ2x.t[x],  subtype_rel: A ⊆r B,  member: t ∈ T,  uimplies: b supposing a,  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  fpf-compatible: f || g,  rev_uimplies: rev_uimplies(P;Q),  cand: A c∧ B,  fpf-sub: f ⊆ g,  btrue: tt,  sq_type: SQType(T),  guard: {T},  true: True,  fpf-cap: f(x)?z,  fpf-join: f ⊕ g
Lemmas referenced :  deq_wf,  fpf_wf,  exists_wf,  not_wf,  fpf-dom_wf,  all_wf,  fpf-single_wf,  fpf-join_wf,  fpf-sub_wf,  fpf-ap_wf,  assert-deq-member,  safe-assert-deq,  assert_of_bor,  iff_weakening_uiff,  member_wf,  or_wf,  deq-member_wf,  bor_wf,  iff_transitivity,  l_member_wf,  deq_member_cons_lemma,  length_of_cons_lemma,  reduce_hd_cons_lemma,  product_subtype_list,  deq_member_nil_lemma,  length_of_nil_lemma,  list-cases,  equal_wf,  less_than_wf,  less_than'_wf,  list_wf,  decidable__assert,  int_formula_prop_wf,  int_formula_prop_less_lemma,  int_term_value_var_lemma,  int_term_value_constant_lemma,  int_formula_prop_le_lemma,  int_formula_prop_not_lemma,  int_formula_prop_and_lemma,  intformless_wf,  itermVar_wf,  itermConstant_wf,  intformle_wf,  intformnot_wf,  intformand_wf,  full-omega-unsat,  decidable__le,  hd_wf,  eqof_wf,  bnot_wf,  assert_wf,  fpf-split,  top_wf,  subtype-fpf2,  fpf-domain_wf,  length_wf,  member-less_than,  fpf-join-sub,  fpf-sub_transitivity,  fpf-sub-reflexive,  assert_of_bnot,  fpf_ap_single_lemma,  fpf-single-dom,  decidable-equal-deq,  eqff_to_assert,  eqtt_to_assert,  bool_subtype_base,  bool_wf,  subtype_base_sq,  bool_cases,  fpf-join-ap-sq,  true_wf,  squash_wf,  assert_functionality_wrt_uiff,  subtype_rel-equal,  istype-universe,  assert_elim,  fpf-single-dom-sq,  fpf-join-dom,  subtype_rel_self,  iff_weakening_equal,  assert_witness,  istype-assert,  and_wf,  fpf_ap_pair_lemma,  int_formula_prop_eq_lemma,  intformeq_wf,  decidable__lt,  proper_sublist_length,  decidable__equal_int,  length_sublist,  member-fpf-domain
Rules used in proof :  universeEquality,  functionEquality,  isectEquality,  instantiate,  functionExtensionality,  productEquality,  orFunctionality,  addLevel,  inlFormation,  hypothesis_subsumption,  promote_hyp,  equalitySymmetry,  equalityTransitivity,  axiomEquality,  independent_pairEquality,  independent_pairFormation,  intEquality,  int_eqEquality,  dependent_pairFormation,  independent_functionElimination,  approximateComputation,  productElimination,  imageElimination,  unionElimination,  cumulativity,  dependent_functionElimination,  rename,  because_Cache,  voidEquality,  voidElimination,  isect_memberEquality,  independent_isectElimination,  hypothesis,  lambdaEquality,  sqequalRule,  applyEquality,  hypothesisEquality,  natural_numberEquality,  thin,  isectElimination,  sqequalHypSubstitution,  extract_by_obid,  introduction,  cut,  lambdaFormation,  isect_memberFormation,  sqequalReflexivity,  computationStep,  sqequalTransitivity,  sqequalSubstitution,  impliesFunctionality,  baseClosed,  imageMemberEquality,  dependent_set_memberEquality_alt,  equalityIstype,  universeIsType,  lambdaEquality_alt,  inhabitedIsType,  lambdaFormation_alt,  Error :memTop,  productIsType,  applyLambdaEquality,  setElimination,  hyp_replacement,  functionIsType,  dependent_set_memberEquality
Latex:
\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A)
        \mforall{}[B:A  {}\mrightarrow{}  Type]
            \mforall{}f:a:A  fp->  B[a]
                \mexists{}g:a:A  fp->  B[a]
                  \mexists{}a:A
                    \mexists{}b:B[a]
                      ((f  \msubseteq{}  g  \moplus{}  a  :  b  \mwedge{}  g  \moplus{}  a  :  b  \msubseteq{}  f)
                      \mwedge{}  (\mforall{}a':A.  \mneg{}(a'  =  a)  supposing  \muparrow{}a'  \mmember{}  dom(g))
                      \mwedge{}  ||fpf-domain(g)||  <  ||fpf-domain(f)||) 
                supposing  0  <  ||fpf-domain(f)||


Date html generated: 2020_05_20-AM-09_03_14
Last ObjectModification: 2020_01_27-PM-04_20_44

Theory : finite!partial!functions


Home Index