Nuprl Lemma : imax-list_functionality

[L,L':ℤ List].  (imax-list(L) imax-list(L') ∈ ℤsupposing (set-equal(ℤ;L;L') and 0 < ||L||)


Definitions occuring in Statement :  set-equal: set-equal(T;x;y) imax-list: imax-list(L) length: ||as|| list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  prop: uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] and: P ∧ Q iff: ⇐⇒ Q guard: {T} implies:  Q all: x:A. B[x] l_subset: l_subset(T;as;bs) set-equal: set-equal(T;x;y) true: True subtype_rel: A ⊆B subtract: m uiff: uiff(P;Q) not: ¬A decidable: Dec(P) le: A ≤ B nat: rev_implies:  Q top: Top cons: [a b] false: False less_than': less_than'(a;b) squash: T less_than: a < b or: P ∨ Q exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) ge: i ≥  bfalse: ff btrue: tt ifthenelse: if then else fi  assert: b
Lemmas referenced :  list_wf length_wf less_than_wf set-equal_wf imax-list-subset l_member_wf equal_wf le-add-cancel add-zero add-associates add_functionality_wrt_le add-commutes minus-one-mul-top zero-add minus-one-mul minus-add condition-implies-le not-lt-2 false_wf decidable__lt nat_wf length_wf_nat nil_member cons_member length_of_cons_lemma product_subtype_list length_of_nil_lemma list-cases int_formula_prop_wf int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf itermVar_wf itermAdd_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf full-omega-unsat non_neg_length decidable__le hd_wf btrue_neq_bfalse nil_wf member-implies-null-eq-bfalse btrue_wf null_cons_lemma null_nil_lemma hd_member int_formula_prop_eq_lemma intformeq_wf decidable__equal_int
Rules used in proof :  natural_numberEquality equalitySymmetry equalityTransitivity because_Cache axiomEquality isect_memberEquality sqequalRule intEquality hypothesis independent_isectElimination hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_functionElimination productElimination dependent_functionElimination lambdaFormation minusEquality lambdaEquality applyEquality independent_pairFormation addEquality rename setElimination inlFormation voidEquality hypothesis_subsumption promote_hyp voidElimination imageElimination unionElimination int_eqEquality dependent_pairFormation approximateComputation

\mforall{}[L,L':\mBbbZ{}  List].    (imax-list(L)  =  imax-list(L'))  supposing  (set-equal(\mBbbZ{};L;L')  and  0  <  ||L||)

Date html generated: 2017_09_29-PM-05_57_52
Last ObjectModification: 2017_07_31-PM-02_07_47

Theory : list_1

Home Index