Nuprl Lemma : compat-no_repeats_common-member

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


Definitions occuring in Statement :  compat: l1 || l2 no_repeats: no_repeats(T;l) select: L[n] length: ||as|| list: List int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] and: P ∧ Q natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: 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 ⊆B le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: squash: T top: Top true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q ge: i ≥  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

\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