{ 
[prg:E#Program]. (compileE#(prg) 
CompilationResult) }
{ Proof }
Definitions occuring in Statement :
compile-esharp-program: compileE#(prg),
esharp-program: E#Program,
compilation-result: CompilationResult,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
compile-esharp-program: compileE#(prg),
all: x:A. B[x],
implies: P 
Q,
so_lambda: 
x y.t[x; y],
so_apply: x[s1;s2],
esharp-program: E#Program,
id-fun: id-fun(T)
Lemmas :
norm-esharp-program_wf,
esharp-program_wf,
list_accum_wf,
esharp-rule_wf,
compilation-result_wf,
trivial-comp-result_wf,
esharp-join_wf,
compile-esharp-rule_wf
\mforall{}[prg:E\#Program]. (compileE\#(prg) \mmember{} CompilationResult)
Date html generated:
2011_08_17-PM-04_39_09
Last ObjectModification:
2011_06_18-AM-11_49_17
Home
Index