### Nuprl Lemma : has-value-is-list-approx-is-type

`∀[T:Type]. ∀[t:colist(T)]. ∀[n:ℕ].`
`  ((λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise ⊥^n ⊥ t)↓ ∈ Typ\000Ce)`

Proof

Definitions occuring in Statement :  colist: `colist(T)` fun_exp: `f^n` nat: `ℕ` has-value: `(a)↓` callbyvalue: callbyvalue bottom: `⊥` btrue: `tt` uall: `∀[x:A]. B[x]` pi2: `snd(t)` ispair: `if z is a pair then a otherwise b` isaxiom: `if z = Ax then a otherwise b` member: `t ∈ T` apply: `f a` lambda: `λx.A[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` decidable: `Dec(P)` or: `P ∨ Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` compose: `f o g` has-value: `(a)↓` pi2: `snd(t)` ext-eq: `A ≡ B`
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than fun_exp0_lemma strictness-apply has-value_wf_base subtract-1-ge-0 fun_exp_unroll decidable__le intformnot_wf int_formula_prop_not_lemma istype-le eq_int_wf eqtt_to_assert assert_of_eq_int intformeq_wf int_formula_prop_eq_lemma eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int value-type-has-value colist_wf colist-value-type co-list-cases unit_subtype_colist sqle_wf_base subtype_rel_transitivity b-union_wf unit_wf2 subtype_rel_b-union-right colist-ext istype-nat istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename sqequalRule intWeakElimination lambdaFormation_alt natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination isect_memberEquality_alt voidElimination independent_pairFormation universeIsType axiomEquality equalityTransitivity equalitySymmetry functionIsTypeImplies inhabitedIsType baseClosed because_Cache dependent_set_memberEquality_alt unionElimination equalityElimination productElimination equalityIstype promote_hyp instantiate cumulativity callbyvalueReduce hypothesis_subsumption productEquality isectIsTypeImplies universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].  \mforall{}[n:\mBbbN{}].
((\mlambda{}is-list,t.  eval  u  =  t  in
if  u  is  a  pair  then  is-list  (snd(u))  otherwise  if  u  =  Ax  then  tt  otherwise  \mbot{}\^{}n
\mbot{}
t)\mdownarrow{}  \mmember{}  Type)

Date html generated: 2019_10_16-AM-11_38_22
Last ObjectModification: 2019_06_26-PM-05_07_14

Theory : eval!all

Home Index