{ SecurityData 
r Base }
{ Proof }
Definitions occuring in Statement :
sdata: SecurityData,
subtype_rel: A r B,
base: Base
Definitions :
atom: Atom$n,
member: t 
T,
equal: s = t,
function: x:A 
B[x],
all: 
x:A. B[x],
Id: Id,
union: left + right,
subtype_rel: A r B,
atom: Atom,
implies: P 
Q,
sdata: SecurityData,
base: Base,
Auto: Error :Auto,
tactic: Error :tactic
Lemmas :
base_wf,
sdata_wf,
subtype_rel_wf,
tree_subtype_base,
union_subtype_base,
atom2_subtype_base,
atom1_subtype_base,
Id_wf
SecurityData \msubseteq{}r Base
Date html generated:
2011_08_17-PM-07_09_57
Last ObjectModification:
2011_06_18-PM-12_53_58
Home
Index