Nuprl Lemma : mFOLeffect_wf
∀[sr:mFOL-sequent() × mFOLRule()]. (mFOLeffect(sr) ∈ mFOL-sequent() List?)
Proof
Definitions occuring in Statement : 
mFOLeffect: mFOLeffect(sr)
, 
mFOL-sequent: mFOL-sequent()
, 
mFOLRule: mFOLRule()
, 
list: T List
, 
uall: ∀[x:A]. B[x]
, 
unit: Unit
, 
member: t ∈ T
, 
product: x:A × B[x]
, 
union: left + right
Lemmas : 
mFOLRule_ind_wf_simple, 
list_wf, 
mFOL-sequent_wf, 
unit_wf2, 
mFO-dest-connective_wf, 
cons_wf, 
mFOL_wf, 
nil_wf, 
bl-all_wf, 
l_member_wf, 
bnot_wf, 
deq-member_wf, 
int-deq_wf, 
mFOL-freevars_wf, 
bool_wf, 
eqtt_to_assert, 
iff_transitivity, 
assert_wf, 
l_all_wf2, 
not_wf, 
iff_weakening_uiff, 
assert-bl-all, 
l_all_functionality, 
assert_of_bnot, 
assert-deq-member, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
eqff_to_assert, 
assert-bnot, 
mFO-dest-quantifier_wf, 
mFOL-subst_wf, 
assert_of_band, 
it_wf, 
bfalse_wf, 
deq-mFO_wf, 
lt_int_wf, 
length_wf, 
assert_of_lt_int, 
select_wf, 
sq_stable__le, 
less_than_wf, 
nat_wf, 
btrue_wf, 
mFOLRule_wf
\mforall{}[sr:mFOL-sequent()  \mtimes{}  mFOLRule()].  (mFOLeffect(sr)  \mmember{}  mFOL-sequent()  List?)
Date html generated:
2015_07_17-AM-07_56_43
Last ObjectModification:
2015_01_27-AM-10_06_59
Home
Index