{ 
[P:st_exp{i:l}() 
{i 2}]
((name:Atom. P[ste_var(name)])
(val:st-constant{i:l}. P[ste_const(val)])
(fun,arg:st_exp{i:l}(). (P[fun] P[arg] P[ste_ap(fun;arg)]))
(bound:Atom. type:SimpleType. body:st_exp{i:l}().
(P[body] P[ste_lambda(bound;type;body)]))
{x:st_exp{i:l}(). P[x]}) }
{ Proof }
Definitions occuring in Statement :
ste_lambda: ste_lambda(bound;type;body),
ste_ap: ste_ap(fun;arg),
ste_const: ste_const(val),
ste_var: ste_var(name),
st_exp: st_exp{i:l}(),
simple_type: SimpleType,
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],
atom: Atom
Definitions :
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,
ste_var: ste_var(name),
ste_const: ste_const(val),
ste_ap: ste_ap(fun;arg),
ste_lambda: ste_lambda(bound;type;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,
simple_type: Error :simple_type,
guard: {T},
uall: [x:A]. B[x],
isect: x:A. B[x],
st_exp: st_exp{i:l}(),
universe: Type,
atom: Atom,
st-constant: st-constant{i:l}(Info),
prop: ,
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
so_apply: x[s],
apply: f a
Lemmas :
Error :simple_type_wf,
st-constant_wf,
uall_wf,
subtype_rel_wf,
type-monotone_wf,
st_exp_wf,
ste_var_wf,
ste_const_wf,
ste_ap_wf,
ste_lambda_wf,
subtype_rel_sum,
subtype_rel_simple_product,
member_wf
\mforall{}[P:st\_exp\{i:l\}() {}\mrightarrow{} \mBbbP{}\{i 2\}]
((\mforall{}name:Atom. P[ste\_var(name)])
{}\mRightarrow{} (\mforall{}val:st-constant\{i:l\}. P[ste\_const(val)])
{}\mRightarrow{} (\mforall{}fun,arg:st\_exp\{i:l\}(). (P[fun] {}\mRightarrow{} P[arg] {}\mRightarrow{} P[ste\_ap(fun;arg)]))
{}\mRightarrow{} (\mforall{}bound:Atom. \mforall{}type:SimpleType. \mforall{}body:st\_exp\{i:l\}().
(P[body] {}\mRightarrow{} P[ste\_lambda(bound;type;body)]))
{}\mRightarrow{} \{\mforall{}x:st\_exp\{i:l\}(). P[x]\})
Date html generated:
2011_08_17-PM-05_03_31
Last ObjectModification:
2011_02_04-AM-11_57_11
Home
Index