Nuprl Lemma : mRuleallE-hypnum_wf
∀[v:mFOLRule()]. mRuleallE-hypnum(v) ∈ ℕ supposing ↑mRuleallE?(v)
Proof
Definitions occuring in Statement : 
mRuleallE-hypnum: mRuleallE-hypnum(v)
, 
mRuleallE?: mRuleallE?(v)
, 
mFOLRule: mFOLRule()
, 
nat: ℕ
, 
assert: ↑b
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Lemmas : 
mFOLRule-ext, 
eq_atom_wf, 
bool_wf, 
eqtt_to_assert, 
assert_of_eq_atom, 
subtype_base_sq, 
atom_subtype_base, 
unit_wf2, 
unit_subtype_base, 
it_wf, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_atom, 
assert_wf, 
mRuleallE?_wf, 
mFOLRule_wf
\mforall{}[v:mFOLRule()].  mRuleallE-hypnum(v)  \mmember{}  \mBbbN{}  supposing  \muparrow{}mRuleallE?(v)
Date html generated:
2015_07_17-AM-07_56_02
Last ObjectModification:
2015_01_27-AM-10_05_37
Home
Index