Nuprl Lemma : sdata-free-from-atom
∀[d:SecurityData]. ∀[a:Atom1]. uiff(a#d:SecurityData;¬(a ∈ sdata-atoms(d)))
Proof
Definitions occuring in Statement :
sdata-atoms: sdata-atoms(d),
sdata: SecurityData,
l_member: (x ∈ l),
free-from-atom: a#x:T,
atom: Atom$n,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
not: ¬A
Lemmas :
tree-induction,
Id_wf,
all_wf,
iff_wf,
free-from-atom_wf,
tree_wf,
not_wf,
l_member_wf,
sdata-atoms_wf,
null_nil_lemma,
btrue_wf,
member-implies-null-eq-bfalse,
nil_wf,
btrue_neq_bfalse,
true_wf,
id-sdata-has-atom,
sdata_wf,
id-sdata_wf,
equal-wf-base,
atom1_subtype_base,
decidable__atom_equal_1,
atom-sdata-has-atom,
member_singleton,
cons_wf,
atom-sdata_wf,
sdata-pair_wf,
append_wf,
or_wf,
iff_transitivity,
iff_weakening_uiff,
sdata-pair-has-atom,
member_append,
decidable__l_member
Latex:
\mforall{}[d:SecurityData]. \mforall{}[a:Atom1]. uiff(a\#d:SecurityData;\mneg{}(a \mmember{} sdata-atoms(d)))
Date html generated:
2015_07_23-PM-00_01_30
Last ObjectModification:
2015_01_29-AM-07_48_21
Home
Index