Nuprl Lemma : assert-eq_mFO
∀[x,y:mFOL()]. uiff(↑eq_mFO(x;y);x = y ∈ mFOL())
Proof
Definitions occuring in Statement :
eq_mFO: eq_mFO(x;y),
mFOL: mFOL(),
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
mFOL-induction,
all_wf,
uiff_wf,
assert_wf,
eq_mFO_wf,
equal_wf,
mFOatomic_wf,
equal-wf-base-T,
list_subtype_base,
int_subtype_base,
atom_subtype_base,
false_wf,
btrue_wf,
and_wf,
mFOL_wf,
mFOconnect?_wf,
bfalse_wf,
btrue_neq_bfalse,
mFOconnect_wf,
mFOquant?_wf,
mFOquant_wf,
bool_wf,
list_wf,
equal-wf-T-base,
assert_witness,
eq_atom_wf,
eqtt_to_assert,
assert_of_eq_atom,
list-deq_wf,
int-deq_wf,
deq_wf,
iff_transitivity,
equal-wf-base,
iff_weakening_uiff,
assert_of_band,
mFOatomic-name_wf,
mFOatomic?_wf,
deq_property,
subtype_base_sq,
mFOatomic-vars_wf,
mFOconnect-right_wf,
eqff_to_assert,
bool_cases_sqequal,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
mFOconnect-knd_wf,
eq_bool_wf,
assert_of_eq_bool,
mFOquant-isall_wf,
mFOquant-body_wf,
assert_of_eq_int
\mforall{}[x,y:mFOL()]. uiff(\muparrow{}eq\_mFO(x;y);x = y)
Date html generated:
2015_07_17-AM-07_54_10
Last ObjectModification:
2015_01_27-AM-10_07_27
Home
Index