Nuprl Lemma : finite-nat-seq-to-list_wf
∀[f:finite-nat-seq()]. (finite-nat-seq-to-list(f) ∈ ℕ List)
Proof
Definitions occuring in Statement :
finite-nat-seq-to-list: finite-nat-seq-to-list(f),
finite-nat-seq: finite-nat-seq(),
list: T List,
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
finite-nat-seq-to-list: finite-nat-seq-to-list(f),
finite-nat-seq: finite-nat-seq(),
nat: ℕ
Lemmas referenced :
finite-nat-seq_wf,
int_seg_wf,
cons_wf,
append_wf,
nil_wf,
nat_wf,
list_wf,
primrec_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
spreadEquality,
sqequalHypSubstitution,
hypothesisEquality,
lemma_by_obid,
isectElimination,
thin,
hypothesis,
lambdaEquality,
applyEquality,
natural_numberEquality,
setElimination,
rename,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[f:finite-nat-seq()]. (finite-nat-seq-to-list(f) \mmember{} \mBbbN{} List)
Date html generated:
2016_05_14-PM-09_54_48
Last ObjectModification:
2016_01_15-AM-09_32_01
Theory : continuity
Home
Index