DISP	exp_value_df	ExpValue( < t:jtype:* > ; < f:f:* > ; < s:spec:* > )== ExpValue( < t > ) ExpValue( < t:jtype:* > )== ExpValue( < t > )
ABS	exp_value	ExpValue(t) == Env (J(Exception) + J(t))
THM	exp_value_wf	f:Atom . s:Spec. t:Type. ExpValue(t)
THM	exp_value_total	f:Atom . s:Spec. t:Type. ExpValue(t) total
DISP	exp_value_exc_df	ExpValueExc( < en:env:* > ; < ex:exc:* > )== ExpValueExc( < en > ; < ex > )
ABS	exp_value_exc	ExpValueExc(en;ex) == < en, inl ex >
THM	exp_value_exc_wf	f:Atom . s:Spec. t:Type. en:Env. ex:J(Exception). ExpValueExc(en;ex) ExpValue(t)
DISP	exp_value_make_df	ExpValueMake( < en:en:* > ; < x:x:* > )== ExpValueMake( < en > ; < x > )
ABS	exp_value_make	ExpValueMake(en;x) == < en, inr x >
THM	exp_value_make_wf	f:Atom . s:Spec. en:Env. t:Type. x:J(t). ExpValueMake(en;x) ExpValue(t)
THM	exp_value_make_inj	f:Atom . s:Spec. en1,en2:Env. t:Type. o1,o2:J(t). ExpValueMake(en1;o1) = ExpValueMake(en2;o2) en1 = en2
DISP	exp_value_cases_df	{[SOFT}{- > 0}case < ev:ev:* > {\\}of Exc( < en1:en-var > , < ex:ex-var > ) - > < exc:term:* > {\\} | Make( < en2:en-var > , < x:obj-var > ) - > < mk:term:* > {\\} { < -}{]} == case < ev > of Exc( < en1 > , < ex > ) - > < exc > | Make( < en2 > , < x > ) - > < mk >
ABS	exp_value_cases	case ev of Exc(en1,ex) - > exc[en1; ex] | Make(en2,x) - > mk[en2; x] == let < en,et > = ev in case et of inl(ex) = > exc[en; ex] | inr(x) = > mk[en; x]
THM	exp_value_cases_wf	f:Atom . s:Spec. t:Type. T:. exc:Env J(Exception) T. mk:Env J(t) T. ev:ExpValue(t). case ev of Exc(en,ex) - > exc[en;ex] | Make(en,x) - > mk[en;x] T
THM	exp_value_cases_wf_bar	f:Atom . s:Spec. t,t':Type. exc:Env J(Exception) bar(ExpValue(t')). mk:Env J(t) bar(ExpValue(t')). ev:bar(ExpValue(t)). case ev of Exc(en,ex) - > exc[en;ex] | Make(en,x) - > mk[en;x] bar(ExpValue(t'))
THM	exp_value_cases_wf_bar2	f:Atom . s:Spec. t:Type. exc:Env J(Exception) bar(StmtValue(f;s)). mk:Env J(t) bar(StmtValue(f;s)). ev:bar(ExpValue(t)). case ev of Exc(en,ex) - > exc[en;ex] | Make(en,x) - > mk[en;x] bar(StmtValue(f;s))
ML	exp_value_cases_eval	let exp_value_cases_makeC = SimpleMacroC `exp_value_cases_make` case ExpValueMake(en;o) of Exc(en',ex') - > E[en'; ex'] | Make(en'',o'') - > M[en''; o''] M[en; o] ``exp_value_cases exp_value_make``;; let exp_value_cases_excC = SimpleMacroC `exp_value_cases_exc` case ExpValueExc(en;ex) of Exc(en',ex') - > E[en'; ex'] | Make(en'',o'') - > M[en''; o''] E[en; ex] ``exp_value_cases exp_value_exc``;; let exp_value_casesC = FirstC [exp_value_cases_makeC; exp_value_cases_excC] ;; add_AbReduce_conv `exp_value_cases` exp_value_casesC;;
DISP	exp_df	Exp( < t:jtype:* > ; < f:f:* > ; < s:spec:* > )== Exp( < t > ) Exp( < t:jtype:* > )== Exp( < t > )
ABS	exp	Exp(t) == Env bar(ExpValue(t))
ML	exp_soft	add_soft_abs ``exp``;;
DISP	init_df	init < t:jtype:* > == init < t >
ABS	init	init t == en.ExpValueMake(en;t)
THM	init_wf	f:Atom . s:Spec. t:Type. init t Exp(t)
COM	init_com	" init " is similar too " new " constructor but it returns the same object each time when it applied.
DISP	const_exp_df	const_exp( < c:c:* > ; < t:t:* > )== const_exp( < c > ; < t > )
ABS	const_exp	const_exp(c;t) == en.ExpValueMake(en;JConst(c;t))
THM	const_exp_wf	f:Atom . s:Spec. t:Type. c:JActCor(t). const_exp(c;t) Exp(t)
DISP	int_const_df	( < z:int:* > )== ( < z > )
ABS	int_const	(z) == const_exp(z;int)
THM	int_const_wf	f:Atom . s:Spec. z:. (z) Exp(int)
DISP	bool_const_df	( < b:bool:* > )== ( < b > )
ABS	bool_const	(b) == const_exp(b;boolean)
THM	bool_const_wf	f:Atom . s:Spec. b:. (b) Exp(boolean)
DISP	exc_const_df	( < a:atom:* > )== ( < a > )
ABS	exc_const	(a) == const_exp(a;Exception)
THM	exc_const_wf	f:Atom . s:Spec. a:Atom. (a) Exp(Exception)
DISP	simple_exp2_df	simple_exp2( < u:var > , < v:var > . < op:op:* > ; < x:x:* > ; < y:y:* > ; < f:f:* > ; < s:s:* > ; < t:t:* > ) == simple_exp2( < u > , < v > . < op > ; < x > ; < y > ; < f > ; < s > ; < t > )
ABS	simple_exp2	simple_exp2(u,v.op[u; v];x;y;f;s;t) == en.case x en of Exc(en',ex) - > ExpValueExc(en';ex) | Make(en',vx) - > case y en' of Exc(en'',ex) - > ExpValueExc(en'';ex) | Make(en'',vy) - > ExpValueMake(en'';simple_ obj_oper2(u,v.op[u; v];vx;vy;f;s;t))
THM	simple_exp2_wf	f:Atom . s:Spec. t:Type. op:JActCor(t) JActCor(t) JActCor(t). x,y:Exp(t). simple_exp2(u,v.op[u;v];x;y;f;s;t) Exp(t)
DISP	add_exp_df	( < x:exp:* > + < y:exp:* > wrt < f:f:* > ; < s:s:* > )== ( < x > + < y > ) ( < x:exp:* > + < y:exp:* > )== ( < x > + < y > )
ABS	add_exp	(x + y) == simple_exp2(u,v.u + v;x;y;f;s;int)
THM	add_exp_wf	f:Atom . s:Spec. x,y:Exp(int). (x + y) Exp(int)
DISP	sub_exp_df	( < x:x:* > - < y:y:* > wrt < f:f:* > ; < s:s:* > )== ( < x > - < y > ) ( < x:x:* > - < y:y:* > )== ( < x > - < y > )
ABS	sub_exp	(x - y) == simple_exp2(u,v.u - v;x;y;f;s;int)
THM	sub_exp_wf	f:Atom . s:Spec. x,y:Exp(int). (x - y) Exp(int)
DISP	mul_exp_df	( < x:x:* > < y:y:* > wrt < f:f:* > ; < s:s:* > )== ( < x > < y > ) ( < x:x:* > < y:y:* > )== ( < x > < y > )
ABS	mul_exp	(x y) == simple_exp2(u,v.u * v;x;y;f;s;int)
THM	mul_exp_wf	f:Atom . s:Spec. x,y:Exp(int). (x y) Exp(int)
DISP	and_exp_df	( < x:x:* > & < y:y:* > wrt < f:f:* > ; < s:s:* > )== ( < x > & < y > ) ( < x:x:* > & < y:y:* > )== ( < x > & < y > )
ABS	and_exp	(x & y) == simple_exp2(u,v.u v;x;y;f;s;boolean)
THM	and_exp_wf	f:Atom . s:Spec. x,y:Exp(boolean). (x & y) Exp(boolean)
DISP	ref_exp_df	( < x:exp:* > . < i:i:* > wrt < f:f:* > ; < s:spec:* > )== ( < x > . < i > ) ( < x:exp:* > . < i:i:* > )== ( < x > . < i > )
ABS	ref_exp	(x.i) == en.case x en of Exc(en',ex) - > ExpValueExc(en';ex) | Make(en',vx) - > ExpValueMake(en';(vx.i))
THM	ref_exp_wf	f:Atom . s:Spec. t:Type. x:Exp(t). i:JIdx(t). (x.i) Exp(Jfld(t.i))
DISP	var_exp_df	( < v:atom:* > : < t:jtype:* > )== ( < v > : < t > )
ABS	var_exp	(v:t) == en.ExpValueMake(en;en v t)
THM	var_exp_wf	f:Atom . s:Spec. t:Type. v:Atom. (v:t) Exp(t)

the other theories