### Nuprl Lemma : compat-no_repeats_common-member

`∀[T:Type]. ∀[L1,L2:T List].`
`  (∀[i:ℕ||L1||]. ∀[j:ℕ||L2||].  i = j ∈ ℤ supposing L1[i] = L2[j] ∈ T) supposing `
`     ((no_repeats(T;L1) ∧ no_repeats(T;L2)) and `
`     L1 || L2)`

Proof

Definitions occuring in Statement :  compat: `l1 || l2` no_repeats: `no_repeats(T;l)` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` and: `P ∧ Q` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` compat: `l1 || l2` or: `P ∨ Q` iseg: `l1 ≤ l2` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` int_seg: `{i..j-}` decidable: `Dec(P)` no_repeats: `no_repeats(T;l)` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` squash: `↓T` top: `Top` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` ge: `i ≥ j ` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` less_than: `a < b` nat: `ℕ`
Lemmas referenced :  decidable__equal_int int_seg_subtype_nat length_wf false_wf length_wf_nat equal_wf nat_wf less_than_wf squash_wf true_wf length_append subtype_rel_list top_wf iff_weakening_equal non_neg_length int_seg_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermVar_wf itermAdd_wf intformle_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf nat_properties intformeq_wf int_formula_prop_eq_lemma list_wf select_append_front select_wf decidable__le length-append int_seg_wf no_repeats_wf compat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin unionElimination extract_by_obid dependent_functionElimination setElimination rename hypothesisEquality hypothesis isectElimination applyEquality natural_numberEquality cumulativity independent_isectElimination sqequalRule independent_pairFormation lambdaFormation dependent_set_memberEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry intEquality isect_memberEquality voidElimination voidEquality because_Cache imageMemberEquality baseClosed universeEquality independent_functionElimination addEquality dependent_pairFormation int_eqEquality computeAll hyp_replacement applyLambdaEquality axiomEquality productEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].
(\mforall{}[i:\mBbbN{}||L1||].  \mforall{}[j:\mBbbN{}||L2||].    i  =  j  supposing  L1[i]  =  L2[j])  supposing
((no\_repeats(T;L1)  \mwedge{}  no\_repeats(T;L2))  and
L1  ||  L2)

Date html generated: 2018_05_21-PM-06_44_53
Last ObjectModification: 2017_07_26-PM-04_55_21

Theory : general

Home Index