Nuprl Lemma : imax-list-subset

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


Definitions occuring in Statement :  l_subset: l_subset(T;as;bs) imax-list: imax-list(L) length: ||as|| list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q le: A ≤ B not: ¬A implies:  Q false: False prop: all: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q rev_implies:  Q exists: x:A. B[x] cand: c∧ B decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top guard: {T} l_subset: l_subset(T;as;bs)
Lemmas referenced :  and_wf int_formula_prop_wf int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma itermVar_wf intformle_wf intformnot_wf satisfiable-full-omega-tt decidable__le l_exists_iff imax-list-ub l_member_wf le_wf l_all_iff list_wf length_wf less_than_wf l_subset_wf less_than'_wf imax-list_wf imax-list-lb l_subset_pos_length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality independent_isectElimination hypothesis because_Cache productElimination sqequalRule independent_pairEquality lambdaEquality dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality natural_numberEquality voidElimination setElimination rename setEquality independent_functionElimination lambdaFormation dependent_pairFormation independent_pairFormation unionElimination int_eqEquality voidEquality computeAll

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

Date html generated: 2016_05_14-PM-01_41_56
Last ObjectModification: 2016_01_15-AM-08_23_19

Theory : list_1

Home Index