Nuprl Lemma : atom-sdata-one-one
∀[a,b:Atom1]. uiff(data(a) = data(b) ∈ SecurityData;a = b ∈ Atom1)
Proof
Definitions occuring in Statement :
atom-sdata: data(a),
sdata: SecurityData,
atom: Atom$n,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
equal-wf-base,
sdata_wf,
atom1_subtype_base,
and_wf,
equal_wf,
atom-sdata_wf,
tree_leaf?_wf,
Id_wf,
bool_wf,
eqtt_to_assert,
tree_leaf-value_wf,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
tree_wf,
assert_wf,
outr_wf,
bnot_wf,
isl_wf
Latex:
\mforall{}[a,b:Atom1]. uiff(data(a) = data(b);a = b)
Date html generated:
2015_07_23-PM-00_00_52
Last ObjectModification:
2015_01_29-AM-07_43_27
Home
Index