### Nuprl Lemma : length_zero

`∀[T:Type]. ∀[l:T List].  uiff(||l|| = 0 ∈ ℤ;l = [] ∈ (T List))`

Proof

Definitions occuring in Statement :  length: `||as||` nil: `[]` list: `T List` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` all: `∀x:A. B[x]` or: `P ∨ Q` cons: `[a / b]` top: `Top` prop: `ℙ` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` ge: `i ≥ j ` decidable: `Dec(P)` false: `False` le: `A ≤ B` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]`
Lemmas referenced :  list-cases length_of_nil_lemma nil_wf product_subtype_list length_of_cons_lemma equal-wf-T-base length_wf equal_wf squash_wf true_wf length_of_null_list subtype_rel_self iff_weakening_equal list_wf le_weakening2 non_neg_length decidable__lt full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut independent_pairFormation hypothesisEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis dependent_functionElimination unionElimination sqequalRule promote_hyp hypothesis_subsumption productElimination isect_memberEquality voidElimination voidEquality Error :universeIsType,  intEquality baseClosed applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality because_Cache independent_isectElimination natural_numberEquality imageMemberEquality instantiate independent_functionElimination independent_pairEquality axiomEquality approximateComputation dependent_pairFormation int_eqEquality

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].    uiff(||l||  =  0;l  =  [])

Date html generated: 2019_06_20-PM-01_20_09
Last ObjectModification: 2018_09_26-PM-05_20_46

Theory : list_1

Home Index