### Nuprl Lemma : disjoint_sublists_witness

`∀[T:Type]`
`  ∀L1,L2,L:T List.`
`    (disjoint_sublists(T;L1;L2;L)`
`    `` (∃f:ℕ||L1|| + ||L2|| ⟶ ℕ||L||`
`         (Inj(ℕ||L1|| + ||L2||;ℕ||L||;f)`
`         ∧ (∀i:ℕ||L1|| + ||L2||`
`              (L1[i] = L[f i] ∈ T supposing i < ||L1|| ∧ L2[i - ||L1||] = L[f i] ∈ T supposing ||L1|| ≤ i)))))`

Proof

Definitions occuring in Statement :  disjoint_sublists: `disjoint_sublists(T;L1;L2;L)` select: `L[n]` length: `||as||` list: `T List` inject: `Inj(A;B;f)` int_seg: `{i..j-}` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` disjoint_sublists: `disjoint_sublists(T;L1;L2;L)` exists: `∃x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` int_seg: `{i..j-}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` uimplies: `b supposing a` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` bfalse: `ff` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` decidable: `Dec(P)` squash: `↓T` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` cand: `A c∧ B` ge: `i ≥ j ` nat: `ℕ` inject: `Inj(A;B;f)`
Lemmas referenced :  disjoint_sublists_wf list_wf lt_int_wf length_wf bool_wf eqtt_to_assert assert_of_lt_int int_seg_wf lelt_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot less_than_wf subtract_wf int_seg_properties decidable__le add-is-int-iff satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf false_wf decidable__lt itermAdd_wf int_term_value_add_lemma all_wf equal-wf-T-base assert_wf le_int_wf le_wf bnot_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma uiff_transitivity assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int inject_wf select_wf non_neg_length length_wf_nat nat_properties int_subtype_base increasing_inj
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid isectElimination cumulativity hypothesisEquality hypothesis universeEquality dependent_pairFormation lambdaEquality setElimination rename because_Cache unionElimination equalityElimination sqequalRule independent_isectElimination applyEquality functionExtensionality natural_numberEquality dependent_set_memberEquality independent_pairFormation equalityTransitivity equalitySymmetry promote_hyp dependent_functionElimination instantiate independent_functionElimination voidElimination addEquality pointwiseFunctionality imageElimination baseApply closedConclusion baseClosed int_eqEquality intEquality isect_memberEquality voidEquality computeAll independent_pairEquality axiomEquality productEquality isectEquality applyLambdaEquality hyp_replacement

Latex:
\mforall{}[T:Type]
\mforall{}L1,L2,L:T  List.
(disjoint\_sublists(T;L1;L2;L)
{}\mRightarrow{}  (\mexists{}f:\mBbbN{}||L1||  +  ||L2||  {}\mrightarrow{}  \mBbbN{}||L||
(Inj(\mBbbN{}||L1||  +  ||L2||;\mBbbN{}||L||;f)
\mwedge{}  (\mforall{}i:\mBbbN{}||L1||  +  ||L2||
(L1[i]  =  L[f  i]  supposing  i  <  ||L1||
\mwedge{}  L2[i  -  ||L1||]  =  L[f  i]  supposing  ||L1||  \mleq{}  i)))))

Date html generated: 2017_10_01-AM-08_35_44
Last ObjectModification: 2017_07_26-PM-04_25_53

Theory : list!

Home Index