### Nuprl Lemma : imax-list_functionality

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

Proof

Definitions occuring in Statement :  set-equal: `set-equal(T;x;y)` imax-list: `imax-list(L)` length: `||as||` list: `T List` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  prop: `ℙ` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` and: `P ∧ Q` iff: `P `⇐⇒` Q` guard: `{T}` implies: `P `` 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 ⊆r B` subtract: `n - m` uiff: `uiff(P;Q)` not: `¬A` decidable: `Dec(P)` le: `A ≤ B` nat: `ℕ` rev_implies: `P `` 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 ≥ j ` bfalse: `ff` btrue: `tt` ifthenelse: `if b then t else f 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

Latex:
\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