Nuprl Lemma : ranked-eo-first
∀[L,rk:Top]. ∀[e:Id × ℤ]. (first(e) ~ (snd(e) =z 0))
Proof
Definitions occuring in Statement :
ranked-eo: ranked-eo(L;rk),
es-first: first(e),
Id: Id,
eq_int: (i =z j),
uall: ∀[x:A]. B[x],
top: Top,
pi2: snd(t),
product: x:A × B[x],
natural_number: $n,
int: ℤ,
sqequal: s ~ t
Lemmas :
Id_wf,
top_wf,
ranked-eo-dom,
ranked-eo-pred,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
ranked-eo-eq-E,
subtract_wf,
iff_imp_equal_bool,
bor_wf,
eq_id_wf,
assert-eq-id,
not-equal-2,
le_antisymmetry_iff,
condition-implies-le,
add-associates,
minus-one-mul,
add-mul-special,
zero-mul,
add-zero,
add-swap,
le-add-cancel-alt,
or_wf,
member_wf,
equal-wf-base,
int_subtype_base,
iff_transitivity,
assert_wf,
iff_weakening_uiff,
assert_of_bor,
assert_of_band,
iff_wf,
true_wf
Latex:
\mforall{}[L,rk:Top]. \mforall{}[e:Id \mtimes{} \mBbbZ{}]. (first(e) \msim{} (snd(e) =\msubz{} 0))
Date html generated:
2015_07_21-PM-04_44_36
Last ObjectModification:
2015_01_27-PM-04_59_29
Home
Index