Nuprl Lemma : pi-rank-choices_wf
∀[compList:(pi_prefix() × pi_term()) List]. (pi-rank-choices(compList) ∈ ℕ)
Proof
Definitions occuring in Statement :
pi-rank-choices: pi-rank-choices(compList),
pi_term: pi_term(),
pi_prefix: pi_prefix(),
list: T List,
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
product: x:A × B[x]
Lemmas :
eq_int_wf,
length_wf,
pi_prefix_wf,
pi_term_wf,
bool_wf,
uiff_transitivity,
equal-wf-T-base,
assert_wf,
equal-wf-base-T,
eqtt_to_assert,
assert_of_eq_int,
false_wf,
le_wf,
iff_transitivity,
bnot_wf,
not_wf,
iff_weakening_uiff,
eqff_to_assert,
assert_of_bnot,
imax-list_wf,
map_wf,
pi-rank_wf,
nat_wf,
non_neg_length,
map_length,
length_wf_nat,
imax-list-ub,
list_wf,
l_exists_map,
list-cases,
length_of_nil_lemma,
product_subtype_list,
length_of_cons_lemma,
l_exists_cons,
zero-le-nat,
l_exists_wf,
l_member_wf
Latex:
\mforall{}[compList:(pi\_prefix() \mtimes{} pi\_term()) List]. (pi-rank-choices(compList) \mmember{} \mBbbN{})
Date html generated:
2015_07_23-AM-11_33_22
Last ObjectModification:
2015_01_29-AM-00_55_34
Home
Index