### Nuprl Lemma : colength-zero

[L:Top List]. ((colength(L) 0 ∈ ℤ (L []))

Proof

Definitions occuring in Statement :  nil: [] list: List colength: colength(L) uall: [x:A]. B[x] top: Top implies:  Q natural_number: \$n int: sqequal: t equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q list: List ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uimplies: supposing a nil: [] bfalse: ff cons: [a b] prop: nat: false: False colength: colength(L) so_lambda: λ2x.t[x] so_apply: x[s] has-value: (a)↓ exists: x:A. B[x] squash: T uiff: uiff(P;Q) guard: {T} sq_stable: SqStable(P) top: Top le: A ≤ B not: ¬A less_than': less_than'(a;b) true: True subtract: m sq_type: SQType(T) ge: i ≥
Lemmas referenced :  colist-ext top_wf isaxiom_wf_listunion colist_wf bool_wf subtype_rel_b-union-left unit_wf2 axiom-listunion subtype_rel_b-union-right non-axiom-listunion equal_wf equal-wf-T-base colength_wf_list nat_wf list_wf colength_wf subtype_partial_sqtype_base set_subtype_base le_wf int_subtype_base termination set-value-type int-value-type value-type-has-value subtype_rel-equal base_wf le_antisymmetry_iff sq_stable__le add_functionality_wrt_le add-associates zero-add add-swap add-zero add-commutes le-add-cancel nat_properties subtract_wf minus-zero subtype_base_sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution setElimination thin rename extract_by_obid isectElimination hypothesis promote_hyp productElimination hypothesis_subsumption hypothesisEquality applyEquality sqequalRule unionElimination equalityElimination productEquality independent_isectElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination intEquality lambdaEquality baseClosed sqequalAxiom because_Cache voidElimination natural_numberEquality callbyvalueAdd dependent_pairFormation sqequalIntensionalEquality applyLambdaEquality imageMemberEquality imageElimination addEquality isect_memberEquality voidEquality minusEquality instantiate cumulativity

Latex:
\mforall{}[L:Top  List].  ((colength(L)  =  0)  {}\mRightarrow{}  (L  \msim{}  []))

Date html generated: 2017_04_14-AM-07_54_17
Last ObjectModification: 2017_02_27-PM-03_21_23

Theory : list_0

Home Index