{ 
[x,y:CompilationResult]. (x + y 
CompilationResult) }
{ Proof }
Definitions occuring in Statement :
esharp-join: x + y,
compilation-result: CompilationResult,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
compilation-result: CompilationResult,
member: t T,
esharp-join: x + y,
prop: 
,
and: P 
Q,
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
all: x:A. B[x],
implies: P 
Q,
InitSys: InitSys,
Sys: Sys,
std-initial: std-initial(S),
pi2: snd(t),
system-append: S1 @ S2,
pi1: fst(t),
top: Top,
subtype: S 
T,
so_apply: x[s1;s2],
so_apply: x[s],
System: System(P.M[P]),
ldag: LabeledDAG(T),
iff: P 
Q,
rev_implies: P Q,
pInTransit: pInTransit(P.M[P])
Lemmas :
event-ordering+_wf,
Message_wf,
InitSys_wf,
strong-realizes_wf,
std-n2m_wf,
std-l2m_wf,
reliable-env_wf2,
RunType_wf,
EnvType_wf,
system-append_wf,
name_wf,
mData_wf,
lg-all-append,
pInTransit_wf,
pi1_wf_top,
Id_wf,
std-initial_wf,
strong-realizes-and
\mforall{}[x,y:CompilationResult]. (x + y \mmember{} CompilationResult)
Date html generated:
2011_08_17-PM-04_38_41
Last ObjectModification:
2011_06_18-AM-11_49_05
Home
Index