### Nuprl Lemma : islist-iff-length-has-value

`∀[T:Type]. ∀[t:colist(T)].  uiff((is-list(t))↓;(||t||)↓)`

Proof

Definitions occuring in Statement :  is-list: `is-list(t)` length: `||as||` colist: `colist(T)` has-value: `(a)↓` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  has-value: `(a)↓` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` is-list-fun: `is-list-fun()` prop: `ℙ` top: `Top` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` ge: `i ≥ j ` false: `False` implies: `P `` Q` nat: `ℕ` is-list: `is-list(t)` is-list-approx: `is-list-approx(j)` or: `P ∨ Q` decidable: `Dec(P)` nat_plus: `ℕ+` ext-eq: `A ≡ B` unit: `Unit` list_ind: list_ind length: `||as||` nil: `[]` it: `⋅` cons: `[a / b]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` pi2: `snd(t)` guard: `{T}` subtype_rel: `A ⊆r B` bool: `𝔹` btrue: `tt` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` bfalse: `ff` ifthenelse: `if b then t else f fi ` compose: `f o g` less_than': `less_than'(a;b)` le: `A ≤ B`
Lemmas referenced :  istype-universe colist_wf subtract-1-ge-0 istype-less_than ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma istype-void int_formula_prop_and_lemma istype-int intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat nat_properties strictness-apply fun_exp0_lemma has-value_wf_base bottom_diverge int_formula_prop_not_lemma intformnot_wf decidable__lt is-list-approx-step colist-ext subtype_rel_b-union-right unit_wf2 b-union_wf subtype_rel_transitivity unit_subtype_colist co-list-cases is-exception_wf length_of_cons_lemma termination nat_wf int-value-type le_wf set-value-type colength_wf length-is-colength value-type-has-value is-list-approx_wf decidable__le has-value_wf-partial bool_wf union-value-type is-list_wf fun_exp_unroll_1 istype-sqequal istype-le int_term_value_subtract_lemma itermSubtract_wf subtract_wf assert_of_bnot eqff_to_assert iff_weakening_uiff iff_transitivity assert_of_eq_int eqtt_to_assert uiff_transitivity int_formula_prop_eq_lemma intformeq_wf istype-assert not_wf bnot_wf assert_wf int_subtype_base equal-wf-base eq_int_wf fun_exp_unroll bottom_wf-partial add-wf-partial-nat istype-false nat-partial-nat
Rules used in proof :  universeEquality instantiate hypothesisEquality thin isectElimination extract_by_obid universeIsType hypothesis axiomSqleEquality sqequalHypSubstitution sqequalRule cut introduction independent_pairFormation isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution inhabitedIsType functionIsTypeImplies equalitySymmetry equalityTransitivity axiomEquality voidElimination isect_memberEquality_alt dependent_functionElimination int_eqEquality lambdaEquality_alt dependent_pairFormation_alt independent_functionElimination approximateComputation independent_isectElimination natural_numberEquality lambdaFormation_alt intWeakElimination rename setElimination compactness lambdaEquality voidEquality isect_memberEquality baseClosed cumulativity because_Cache unionElimination dependent_set_memberEquality_alt productEquality equalityElimination productElimination hypothesis_subsumption sqleReflexivity divergentSqle intEquality closedConclusion applyEquality addEquality equalityIsType1 promote_hyp equalityIstype functionIsType sqequalBase baseApply callbyvalueAdd

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    uiff((is-list(t))\mdownarrow{};(||t||)\mdownarrow{})

Date html generated: 2020_05_20-AM-09_08_02
Last ObjectModification: 2020_02_03-AM-11_34_30

Theory : eval!all

Home Index