Nuprl Lemma : id-sdata-one-one
∀[a,b:Id]. uiff(data(a) = data(b) ∈ SecurityData;a = b ∈ Id)
Proof
Definitions occuring in Statement :
id-sdata: data(x),
sdata: SecurityData,
Id: Id,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
equal_wf,
sdata_wf,
id-sdata_wf,
and_wf,
Id_wf,
tree_leaf?_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,
outl_wf,
isl_wf
Latex:
\mforall{}[a,b:Id]. uiff(data(a) = data(b);a = b)
Date html generated:
2015_07_23-PM-00_00_49
Last ObjectModification:
2015_01_29-AM-07_43_37
Home
Index