Nuprl Lemma : set-equal-no_repeats-length

[T:Type]. ∀[as,bs:T List].
  (||as|| ||bs|| ∈ ℤsupposing (set-equal(T;as;bs) and no_repeats(T;bs) and no_repeats(T;as))


Definitions occuring in Statement :  set-equal: set-equal(T;x;y) no_repeats: no_repeats(T;l) length: ||as|| list: List uimplies: supposing a uall: [x:A]. B[x] int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q cand: c∧ B implies:  Q decidable: Dec(P) or: P ∨ Q le: A ≤ B satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top prop:
Lemmas referenced :  no_repeats_wf set-equal_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf itermVar_wf intformeq_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__equal_int l_contains-no_repeats-length set-equal-l_contains
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination productElimination independent_functionElimination hypothesis independent_pairFormation because_Cache independent_isectElimination unionElimination natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll axiomEquality equalityTransitivity equalitySymmetry

\mforall{}[T:Type].  \mforall{}[as,bs:T  List].
    (||as||  =  ||bs||)  supposing  (set-equal(T;as;bs)  and  no\_repeats(T;bs)  and  no\_repeats(T;as))

Date html generated: 2016_05_14-PM-01_39_25
Last ObjectModification: 2016_01_15-AM-08_25_04

Theory : list_1

Home Index