Nuprl Lemma : atom-sdata-has-atom
[a,b:Atom1]. uiff(data(a):SecurityData||b;
(a = b))
Proof not projected
Definitions occuring in Statement :
atom-sdata: data(a),
sdata: SecurityData,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
not: A,
equal: s = t,
free-from-atom: x:T||a,
atom: Atom$n
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
not: A,
member: t 
T,
and: P 
Q,
uimplies: b supposing a,
implies: P 
Q,
false: False,
exists: 
x:A. B[x],
all: x:A. B[x],
so_lambda: 
x.t[x],
tree: Tree(E),
Id: Id,
assert: 
b,
outl: outl(x),
isl: isl(x),
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
is_leaf: is_leaf(t),
case: case,
case_tree_leaf: case_tree_leaf,
guard: {T},
leaf_value: leaf_value(t),
bnot: 
b,
bfalse: ff,
prop: 
,
sq_type: SQType(T),
sdata: SecurityData,
so_apply: x[s],
atom-sdata: data(a),
tree_con: tree_con(E;T),
tree_leaf: tree_leaf(x),
outr: outr(x)
Lemmas :
free-from-atom_wf,
sdata_wf,
atom-sdata_wf,
not_wf,
equal_wf,
subtype_base_sq,
atom1_subtype_base,
exists_wf,
leaf_value_wf,
Id_wf,
tree_wf,
outr_wf,
sdata_subtype_base,
outl_wf,
union_subtype_base,
atom2_subtype_base,
product_subtype_base,
tree_subtype_base
\mforall{}[a,b:Atom1]. uiff(data(a):SecurityData||b;\mneg{}(a = b))
Date html generated:
2012_01_23-PM-01_35_08
Last ObjectModification:
2012_01_05-PM-04_29_00
Home
Index