{ SQType(Key) }
{ Proof }
Definitions occuring in Statement :
encryption-key: Key,
sq_type: SQType(T)
Definitions :
sqequal: s ~ t,
guard: {T},
atom: Atom,
equal: s = t,
function: x:A 
B[x],
implies: P 
Q,
all: 
x:A. B[x],
atom: Atom$n,
sq_type: SQType(T),
Id: Id,
union: left + right,
inr: inr x ,
universe: Type,
member: t 
T,
lambda: 
x.A[x],
so_lambda: 
x.t[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
false: False,
assert: 
b,
inl: inl x ,
bool: 
,
prop: 
,
bfalse: ff,
btrue: tt,
true: True,
limited-type: LimitedType,
encryption-key: Key,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic
Lemmas :
Id_wf,
Id_sq,
btrue_wf,
bfalse_wf,
bool_wf,
assert_wf,
decide_wf,
atom1_sq,
atom_sq
SQType(Key)
Date html generated:
2010_08_28-AM-01_49_31
Last ObjectModification:
2010_03_11-PM-03_46_24
Home
Index