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