{ 
[P:esharp_exp() 
]
((name:Atom. P[esharpvar(name)])
(val:Base. P[esharpbasic(val)])
(name:Atom. P[esharpop(name)])
(fun,arg:esharp_exp(). (P[fun] P[arg] P[esharpapply(fun;arg)]))
(var:Atom. body:esharp_exp(). (P[body] P[esharplambda(var;body)]))
(lhs:E#Lhs. rsh,body:esharp_exp().
(P[rsh] P[body] P[esharplet(lhs;rsh;body)]))
{x:esharp_exp(). P[x]}) }
{ Proof }
Definitions occuring in Statement :
esharplet: esharplet(lhs;rsh;body),
esharplambda: esharplambda(var;body),
esharpapply: esharpapply(fun;arg),
esharpop: esharpop(name),
esharpbasic: esharpbasic(val),
esharpvar: esharpvar(name),
esharp_exp: esharp_exp(),
esharp-lhs: E#Lhs,
uall: [x:A]. B[x],
prop: ,
guard: {T},
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
base: Base,
atom: Atom
Definitions :
type-expr: Error :type-expr,
inr: inr x ,
fpf: a:A fp-> B[a],
decision: Decision,
inl: inl x ,
tag-by: z
T,
ldag: LabeledDAG(T),
labeled-graph: LabeledGraph(T),
record+: record+,
record: record(x.T[x]),
eclass: EClass(A[eo; e]),
fset: FSet{T},
dataflow: dataflow(A;B),
isect2: T1 
T2,
b-union: A 
B,
rev_implies: P 
Q,
or: P 
Q,
iff: P Q,
bag: bag(T),
list: type List,
set: {x:A| B[x]} ,
top: Top,
true: True,
so_lambda: 
x.t[x],
type-monotone: Monotone(T.F[T]),
union: left + right,
esharpvar: esharpvar(name),
esharpbasic: esharpbasic(val),
esharpop: esharpop(name),
esharpapply: esharpapply(fun;arg),
esharplambda: esharplambda(var;body),
esharplet: esharplet(lhs;rsh;body),
equal: s = t,
member: t 
T,
rec: rec(x.A[x]),
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
product: x:A B[x],
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
esharp-lhs: E#Lhs,
guard: {T},
uall: [x:A]. B[x],
isect: x:A. B[x],
esharp_exp: esharp_exp(),
universe: Type,
base: Base,
so_apply: x[s],
apply: f a,
atom: Atom,
prop: ,
implies: P Q,
all: x:A. B[x],
function: x:A B[x]
Lemmas :
base_wf,
esharp-lhs_wf,
uall_wf,
subtype_rel_wf,
type-monotone_wf,
esharp_exp_wf,
esharpvar_wf,
esharpbasic_wf,
esharpop_wf,
esharpapply_wf,
esharplambda_wf,
esharplet_wf,
subtype_rel_sum,
subtype_rel_simple_product,
member_wf
\mforall{}[P:esharp\_exp() {}\mrightarrow{} \mBbbP{}]
((\mforall{}name:Atom. P[esharpvar(name)])
{}\mRightarrow{} (\mforall{}val:Base. P[esharpbasic(val)])
{}\mRightarrow{} (\mforall{}name:Atom. P[esharpop(name)])
{}\mRightarrow{} (\mforall{}fun,arg:esharp\_exp(). (P[fun] {}\mRightarrow{} P[arg] {}\mRightarrow{} P[esharpapply(fun;arg)]))
{}\mRightarrow{} (\mforall{}var:Atom. \mforall{}body:esharp\_exp(). (P[body] {}\mRightarrow{} P[esharplambda(var;body)]))
{}\mRightarrow{} (\mforall{}lhs:E\#Lhs. \mforall{}rsh,body:esharp\_exp(). (P[rsh] {}\mRightarrow{} P[body] {}\mRightarrow{} P[esharplet(lhs;rsh;body)]))
{}\mRightarrow{} \{\mforall{}x:esharp\_exp(). P[x]\})
Date html generated:
2011_08_17-PM-05_14_38
Last ObjectModification:
2011_02_03-PM-04_33_24
Home
Index