Nuprl Lemma : fpf-join-list-ap-disjoint

[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[L:a:A fp-> B[a] List]. ∀[x:A].
  (∀[f:a:A fp-> B[a]]. (⊕(L)(x) f(x) ∈ B[x]) supposing ((↑x ∈ dom(f)) and (f ∈ L))) supposing 
     ((∀f,g∈L.  ∀x:A. ((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))))) and 
     (↑x ∈ dom(⊕(L))))


Definitions occuring in Statement :  fpf-join-list: (L) fpf-ap: f(x) fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] pairwise: (∀x,y∈L.  P[x; y]) l_member: (x ∈ l) list: List deq: EqDecider(T) assert: b uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] not: ¬A and: P ∧ Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] uimplies: supposing a l_exists: (∃x∈L. P[x]) exists: x:A. B[x] and: P ∧ Q prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] top: Top so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] l_member: (x ∈ l) cand: c∧ B int_seg: {i..j-} nat: decidable: Dec(P) or: P ∨ Q pairwise: (∀x,y∈L.  P[x; y]) lelt: i ≤ j < k le: A ≤ B less_than: a < b not: ¬A implies:  Q squash: T true: True guard: {T} uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) false: False ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla)
Lemmas referenced :  fpf-join-list-ap assert_wf fpf-dom_wf subtype-fpf2 top_wf l_member_wf fpf_wf pairwise_wf2 all_wf not_wf fpf-join-list_wf subtype_rel_list list_wf equal_wf fpf-ap_wf decidable__lt lelt_wf length_wf assert_functionality_wrt_uiff squash_wf true_wf deq_wf nat_properties int_seg_properties decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf select_wf le_wf less_than_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_isectElimination productElimination cumulativity applyEquality sqequalRule lambdaEquality functionExtensionality lambdaFormation isect_memberEquality voidElimination voidEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry instantiate productEquality functionEquality universeEquality hyp_replacement applyLambdaEquality setElimination rename unionElimination dependent_set_memberEquality independent_pairFormation independent_functionElimination imageElimination natural_numberEquality imageMemberEquality baseClosed dependent_pairFormation int_eqEquality intEquality computeAll

\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[L:a:A  fp->  B[a]  List].  \mforall{}[x:A].
    (\mforall{}[f:a:A  fp->  B[a]].  (\moplus{}(L)(x)  =  f(x))  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  (f  \mmember{}  L)))  supposing 
          ((\mforall{}f,g\mmember{}L.    \mforall{}x:A.  (\mneg{}((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}x  \mmember{}  dom(g)))))  and 
          (\muparrow{}x  \mmember{}  dom(\moplus{}(L))))

Date html generated: 2018_05_21-PM-09_23_04
Last ObjectModification: 2018_02_09-AM-10_19_03

Theory : finite!partial!functions

Home Index