Nuprl Lemma : deq-mFO_wf
deq-mFO() ∈ EqDecider(mFOL())
Proof
Definitions occuring in Statement :
deq-mFO: deq-mFO(),
mFOL: mFOL(),
deq: EqDecider(T),
member: t ∈ T
Lemmas :
equal_wf,
assert_wf,
all_wf,
mFOL_wf,
iff_wf,
assert-eq_mFO
deq-mFO() \mmember{} EqDecider(mFOL())
Date html generated:
2015_07_17-AM-07_54_11
Last ObjectModification:
2015_01_27-AM-10_06_41
Home
Index