### 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