Nuprl Lemma : non_neg_length

[A:Type]. ∀[l:A List].  (||l|| ≥ )


Proof




Definitions occuring in Statement :  length: ||as|| list: List uall: [x:A]. B[x] ge: i ≥  natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q ge: i ≥  le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A prop: all: x:A. B[x] top: Top decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) uimplies: supposing a subtract: m subtype_rel: A ⊆B true: True
Lemmas referenced :  list_induction ge_wf length_wf list_wf length_of_nil_lemma false_wf length_of_cons_lemma decidable__le not-ge-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality hypothesis natural_numberEquality independent_functionElimination independent_pairFormation lambdaFormation rename dependent_functionElimination isect_memberEquality voidElimination voidEquality addEquality unionElimination productElimination independent_isectElimination applyEquality intEquality because_Cache minusEquality independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].    (||l||  \mgeq{}  0  )



Date html generated: 2016_05_14-AM-06_33_01
Last ObjectModification: 2015_12_26-PM-00_37_49

Theory : list_0


Home Index