Nuprl Lemma : imax-list-nat
∀L:ℕ List+. (imax-list(L) ∈ ℕ)
Proof
Definitions occuring in Statement :
imax-list: imax-list(L),
listp: A List+,
nat: ℕ,
all: ∀x:A. B[x],
member: t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
listp: A List+,
uall: ∀[x:A]. B[x],
or: P ∨ Q,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
length: ||as||,
list_ind: list_ind,
nil: [],
it: ⋅,
false: False,
and: P ∧ Q,
cons: [a / b],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
nat: ℕ
Lemmas referenced :
nat_wf,
list-cases,
product_subtype_list,
listp_wf,
imax-list-cons-is-nat,
subtype_rel_list
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
setElimination,
thin,
rename,
introduction,
extract_by_obid,
hypothesis,
isectElimination,
dependent_functionElimination,
hypothesisEquality,
unionElimination,
sqequalRule,
imageElimination,
productElimination,
voidElimination,
promote_hyp,
hypothesis_subsumption,
applyEquality,
intEquality,
independent_isectElimination,
lambdaEquality,
because_Cache
Latex:
\mforall{}L:\mBbbN{} List\msupplus{}. (imax-list(L) \mmember{} \mBbbN{})
Date html generated:
2018_05_21-PM-00_32_37
Last ObjectModification:
2018_05_19-AM-06_42_35
Theory : list_1
Home
Index