Nuprl Lemma : has-value-length-member-int
∀[l:Base]. ||l|| ∈ ℤ supposing (||l||)↓
Proof
Definitions occuring in Statement :
length: ||as||,
has-value: (a)↓,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ,
base: Base
Lemmas referenced :
length-wf-has-value
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}[l:Base]. ||l|| \mmember{} \mBbbZ{} supposing (||l||)\mdownarrow{}
Date html generated:
2016_05_15-PM-10_04_28
Last ObjectModification:
2016_01_06-AM-00_48_42
Theory : bar!type
Home
Index