Nuprl Lemma : sdata-pair-free-from-atom
[b:Atom1]. [d1,d2:SecurityData]. uiff(<d1, d2>:SecurityData||b;d1:SecurityData||b 
d2:SecurityData||b)
Proof not projected
Definitions occuring in Statement :
sdata-pair: <d1, d2>,
sdata: SecurityData,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
and: P Q,
free-from-atom: x:T||a,
atom: Atom$n
Definitions :
uall: [x:A]. B[x],
member: t 
T,
uiff: uiff(P;Q),
and: P Q,
uimplies: b supposing a,
not: 
A,
implies: P 
Q,
or: P 
Q,
guard: {T},
prop: 
,
false: False,
all: x:A. B[x],
iff: P 
Q,
rev_implies: P Q
Lemmas :
sdata_wf,
pair_wf,
free-from-atom_wf,
sdata-pair_wf,
and_wf,
sdata-free-from-atom,
member_append,
sdata-atoms_wf,
l_member_wf
\mforall{}[b:Atom1]. \mforall{}[d1,d2:SecurityData].
uiff(<d1, d2>:SecurityData||b;d1:SecurityData||b \mwedge{} d2:SecurityData||b)
Date html generated:
2012_01_23-PM-01_35_28
Last ObjectModification:
2012_01_05-PM-04_31_26
Home
Index