{ ClassProgram 
{i''} }
{ Proof }
Definitions occuring in Statement :
cdv-class-program: ClassProgram,
member: t T,
universe: Type
Definitions :
Message: Message,
eclass: EClass(A[eo; e]),
universe: Type,
member: t T,
all: 
x:A. B[x],
subtype: S 
T,
function: x:A 
B[x],
event_ordering: EO,
event-ordering+: EO+(Info),
equal: s = t,
subtype_rel: A r B,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
dep-isect: Error :dep-isect,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record+: record+,
record: record(x.T[x]),
es-E: E,
record-select: r.x,
lambda: 
x.A[x],
token: "$token",
apply: f a,
top: Top,
ifthenelse: if b then t else f fi ,
atom: Atom,
so_lambda: 
x y.t[x; y],
eclass-program: eclass-program{i:l}(Info),
pair: <a, b>,
defined-class: defined-class(prg),
eclass-program-type: eclass-program-type(prg),
product: x:A 
B[x],
cand: A c
B,
set: {x:A| B[x]} ,
and: P Q,
cdv-class-program: ClassProgram,
Auto: Error :Auto,
Complete: Error :Complete,
Try: Error :Try,
BHyp: Error :BHyp,
CollapseTHEN: Error :CollapseTHEN,
RepeatFor: Error :RepeatFor,
Unfold: Error :Unfold,
ext-eq: A 
B,
implies: P 
Q,
es-E-interface: E(X),
class-program: ClassProgram(T),
union: left + right,
bool: 
,
fpf-cap: f(x)?z,
MaAuto: Error :MaAuto
Lemmas :
es-interface-subtype_rel,
ext-eq_inversion,
subtype_rel_weakening,
ext-eq_weakening,
eclass-program_wf,
defined-class_wf,
eclass-program-type_wf,
es-interface-top,
eclass_wf,
member_wf,
subtype_rel_self,
event_ordering_wf,
event-ordering+_wf,
subtype_rel_wf,
es-E_wf,
Message_wf,
event-ordering+_inc
ClassProgram \mmember{} \mBbbU{}\{i''\}
Date html generated:
2010_08_27-PM-08_14_27
Last ObjectModification:
2010_06_18-PM-11_04_58
Home
Index