### Nuprl Lemma : separated-partitions-have-common-refinement

`∀I:Interval`
`  ∀P,Q:partition(I).`
`    (separated-partitions(P;Q) `` (∃R:partition(I). (frs-increasing(R) ∧ frs-refines(R;P) ∧ frs-refines(R;Q)))) `
`  supposing icompact(I)`

Proof

Definitions occuring in Statement :  separated-partitions: `separated-partitions(P;Q)` partition: `partition(I)` frs-increasing: `frs-increasing(p)` frs-refines: `frs-refines(p;q)` icompact: `icompact(I)` interval: `Interval` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q`
Definitions unfolded in proof :  bfalse: `ff` cons: `[a / b]` btrue: `tt` ifthenelse: `if b then t else f fi ` assert: `↑b` last: `last(L)` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` squash: `↓T` less_than: `a < b` decidable: `Dec(P)` rbetween: `x≤y≤z` guard: `{T}` or: `P ∨ Q` icompact: `icompact(I)` rev_uimplies: `rev_uimplies(P;Q)` uiff: `uiff(P;Q)` iff: `P `⇐⇒` Q` so_apply: `x[s]` so_lambda: `λ2x.t[x]` not: `¬A` false: `False` less_than': `less_than'(a;b)` le: `A ≤ B` lelt: `i ≤ j < k` int_seg: `{i..j-}` l_all: `(∀x∈L.P[x])` frs-refines: `frs-refines(p;q)` separated-partitions: `separated-partitions(P;Q)` cand: `A c∧ B` prop: `ℙ` uall: `∀[x:A]. B[x]` partitions: `partitions(I;p)` and: `P ∧ Q` exists: `∃x:A. B[x]` partition: `partition(I)` member: `t ∈ T` implies: `P `` Q` uimplies: `b supposing a` all: `∀x:A. B[x]`
Lemmas referenced :  right-endpoint_wf length_of_cons_lemma null_cons_lemma product_subtype_list length_of_nil_lemma null_nil_lemma list-cases last_wf decidable__lt int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_subtract_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 itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat subtract_wf decidable__le i-member-compact member_append i-member_wf l_all_iff partition-point-member req_weakening rleq_functionality left-endpoint_wf select_wf req_wf l_member_wf append_wf l_exists_iff lelt_wf false_wf real_wf length_wf less_than_wf interval_wf icompact_wf partition_wf separated-partitions_wf frs-refines_wf frs-increasing_wf partitions_wf frs-increasing-non-dec frs-increasing-separated-common-refinement
Rules used in proof :  hypothesis_subsumption promote_hyp voidEquality voidElimination isect_memberEquality intEquality int_eqEquality approximateComputation imageElimination unionElimination setEquality lambdaEquality sqequalRule natural_numberEquality productEquality independent_isectElimination because_Cache isectElimination independent_pairFormation dependent_set_memberEquality dependent_pairFormation productElimination independent_functionElimination hypothesis hypothesisEquality rename setElimination thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut isect_memberFormation lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}I:Interval
\mforall{}P,Q:partition(I).
(separated-partitions(P;Q)
{}\mRightarrow{}  (\mexists{}R:partition(I).  (frs-increasing(R)  \mwedge{}  frs-refines(R;P)  \mwedge{}  frs-refines(R;Q))))
supposing  icompact(I)

Date html generated: 2018_05_22-PM-02_21_54
Last ObjectModification: 2018_05_21-AM-00_41_51

Theory : reals

Home Index