{ 
[x:esharp_exp()]. esharpbasic-val(x) 
Base supposing 
esharpbasic?(x) }
{ Proof }
Definitions occuring in Statement :
esharpbasic-val: esharpbasic-val(x),
esharpbasic?: esharpbasic?(x),
esharp_exp: esharp_exp(),
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
base: Base
Definitions :
true: True,
esharp_exp_ind: esharp_exp_ind,
apply: f a,
it: 
,
false: False,
esharp_exp_ind_esharplet: esharp_exp_ind_esharplet_compseq_tag_def,
esharp_exp_ind_esharplambda: esharp_exp_ind_esharplambda_compseq_tag_def,
esharp_exp_ind_esharpapply: esharp_exp_ind_esharpapply_compseq_tag_def,
esharp_exp_ind_esharpop: esharp_exp_ind_esharpop_compseq_tag_def,
esharp_exp_ind_esharpbasic: esharp_exp_ind_esharpbasic_compseq_tag_def,
esharp_exp_ind_esharpvar: esharp_exp_ind_esharpvar_compseq_tag_def,
esharp-lhs: E#Lhs,
set: {x:A| B[x]} ,
product: x:A 
B[x],
atom: Atom,
union: left + right,
universe: Type,
rec: rec(x.A[x]),
implies: P 
Q,
function: x:A 
B[x],
all: x:A. B[x],
esharpbasic?: esharpbasic?(x),
uall: [x:A]. B[x],
base: Base,
esharpbasic-val: esharpbasic-val(x),
axiom: Ax,
uimplies: b supposing a,
isect: 
x:A. B[x],
assert: b,
prop: 
,
esharp_exp: esharp_exp(),
equal: s = t,
member: t T
Lemmas :
assert_wf,
esharpbasic?_wf,
esharp_exp_wf,
true_wf,
false_wf
\mforall{}[x:esharp\_exp()]. esharpbasic-val(x) \mmember{} Base supposing \muparrow{}esharpbasic?(x)
Date html generated:
2011_08_17-PM-05_16_39
Last ObjectModification:
2011_02_03-PM-04_39_57
Home
Index