DISP	stmt_value_df	StmtValue== StmtValue( < f > ; < s > ) StmtValue( < f:f:* > ; < s:s:* > )== StmtValue( < f > ; < s > )
ABS	stmt_value	StmtValue(f;s) == Env ?J(Exception)
THM	stmt_value_wf	f:Atom . s:Spec. StmtValue(f;s)
THM	stmt_value_total	f:Atom . s:Spec. StmtValue(f;s) total
ML	stmt_value_hd	let StmtValueHD i = MoveDepHypsToConcl i THEN Unfold `stmt_value` i TH EN D i THEN D (i+1) THEN RenameVarUsingArg `en` `en' i THENL [RenameVa rUsingArg `ex` `ex' (i+1) THEN Fold `stmt_value_exc` 0; D (i+1) THEN T hin (i+1) THEN Fold `it` 0 THEN Fold `stmt_value_norm` 0];;
DISP	stmt_value_exc_df	StmtValueExc( < en:env:* > ; < ex:exc:* > )== StmtValueExc( < en > ; < ex > )
ABS	stmt_value_exc	StmtValueExc(en;ex) == < en, inl ex >
THM	stmt_value_exc_wf	f:Atom . s:Spec. en:Env. ex:J(Exception). StmtValueExc(en;ex) StmtValue(f;s)
DISP	stmt_value_norm_df	StmtValueNorm( < en:en:* > )== StmtValueNorm( < en > )
ABS	stmt_value_norm	StmtValueNorm(en) == < en, inr >
THM	stmt_value_norm_wf	f:Atom . s:Spec. en:Env. StmtValueNorm(en) StmtValue(f;s)
DISP	stmt_value_cases_df	{- > 0}{[SOFT}case < stv:stv:* > {\\}of StmtValueExc( < en:var > , < ex:var > ) - > < E:E:* > {\\} | StmtValueNorm( < en:var > ) - > < N:N:* > {\\}{]}{ < -} == case < stv > of StmtValueExc( < en > , < ex > ) - > < E > | StmtValueNorm( < en > ) - > < N >
ABS	stmt_value_cases	case stv of StmtValueExc(en,ex) - > E[en; ex] | StmtValueNorm(en) - > N[en] == let < en,r > = stv in case r of inl(ex) = > E[en; ex] | inr(i) = > N[en]
THM	stmt_value_cases_wf	f:Atom . s:Spec. stv:StmtValue(f;s). T:. E:Env J(Exception) T. N:Env T. case stv of StmtValueExc(en,ex) - > E[en;ex] | StmtValueNorm(en) - > N[en] T
THM	stmt_value_cases_wf_bar	f:Atom . s:Spec. stv:bar(StmtValue(f;s)). E:Env J(Exception) bar(StmtValue(f;s)). N:Env bar(StmtValue(f;s)). case stv of StmtValueExc(en,ex) - > E[en;ex] | StmtValueNorm(en) - > N[en] bar(StmtValue(f;s))
THM	comb_for_stmt_value_cases_wf	(f,s,stv,T,E,N,z. case stv of StmtValueExc(en,ex) - > E[en;ex] | StmtValueNorm(en) - > N[en] ) f:(Atom ) s:Spec stv:StmtValue(f;s) T: E:(Env J(Exception) T) N:(Env T) True T
ML	stmt_value_cases_eval	let stmt_value_cases_normC = SimpleMacroC `stmt_value_cases_norm` case StmtValueNorm(en) of StmtValueExc(en',ex) - > E[en'; ex] | StmtValueNorm(en') - > N[en'] N[en]``stmt_value_cases stmt_value_norm``;; let stmt_value_cases_excC = SimpleMacroC `stmt_value_cases_exc` case StmtValueExc(en;x) of StmtValueExc(en',ex) - > E[en'; ex] | StmtValueNorm(en') - > N[en'] E[en; x]``stmt_value_cases stmt_value_exc``;; let stmt_value_casesC = FirstC [stmt_value_cases_normC; stmt_value_cases_excC;] ;; add_AbReduce_conv `stmt_value_cases` stmt_value_casesC ;;
THM	stmt_value_cases_norm	f:Atom . s:Spec. stv:StmtValue(f;s). T:. E:Env J(Exception) T. N:Env T. IsNorm(stv) case stv of StmtValueExc(en,ex) - > E[en;ex] | StmtValueNorm(en) - > N[en] = N[env(stv)]
THM	stmt_value_cases_exc	f:Atom . s:Spec. stv:StmtValue(f;s). T:. E,N:Env T. IsNorm(stv) case stv of StmtValueExc(en,ex) - > E[en] | StmtValueNorm(en) - > N[en] = E[env(stv)]
DISP	stmt_value_env_df	env( < v:stmt_value:* > )== env( < v > )
ABS	stmt_value_env	env(v) == case v of StmtValueExc(en,ex) - > en | StmtValueNorm(en) - > en
THM	stmt_value_env_wf	f:Atom . s:Spec. v:StmtValue(f;s). env(v) Env
ML	stmt_value_env_eval	let stmt_value_env_normC = SimpleMacroC `stmt_value_env_normC` env(StmtValueNorm(p)) p ``stmt_value_env stmt_value_norm stmt_value_cases`` ;; let stmt_value_env_excC = SimpleMacroC `stmt_value_env_excC` env(StmtValueExc(en;ex)) en ``stmt_value_env stmt_value_exc stmt_value_cases`` ;; let stmt_value_envC = FirstC [stmt_value_env_normC; stmt_value_env_excC] ;; add_AbReduce_conv `stmt_value_env` stmt_value_envC ;;
DISP	stmt_value_is_norm_df	IsNorm( < v:stmt_value:* > )== IsNorm( < v > )
ABS	stmt_value_is_norm	IsNorm(v) == case v of StmtValueExc(en,ex) - > ff | StmtValueNorm(en) - > tt
THM	stmt_value_is_norm_wf	f:Atom . s:Spec. v:StmtValue(f;s). IsNorm(v)
THM	stmt_value_is_norm_wf_bar	f:Atom . s:Spec. v:bar(StmtValue(f;s)). IsNorm(v) bar()
THM	stmt_value_is_norm_wf_bar2	f:Atom . s:Spec. v:bar(StmtValue(f;s)). v in! StmtValue(f;s) IsNorm(v)
ML	stmt_value_is_norm_eval	let stmt_value_norm_normC = SimpleMacroC `stmt_value_norm_norm` IsNorm(StmtValueNorm(en)) tt ``stmt_value_is_norm stmt_value_norm stmt_value_cases``;; let stmt_value_norm_excC = SimpleMacroC `stmt_value_norm_exc` IsNorm(StmtValueExc(en;ex)) ff ``stmt_value_is_norm stmt_value_exc stmt_value_cases``;; let stmt_value_is_normC = FirstC [stmt_value_norm_excC; stmt_value_norm_normC] ;; add_AbReduce_conv `stmt_value_is_norm` stmt_value_is_normC ;;
DISP	stmt_df	Stmt( < f:f:* > ; < s:s:* > )== Stmt Stmt== Stmt
ABS	stmt	Stmt == Env bar(StmtValue(f;s))
ML	stmt_soft	add_soft_abs ``stmt``;;
DISP	skip_df	skip== skip
ABS	skip	skip == en.StmtValueNorm(en)
THM	skip_wf	f:Atom . s:Spec. skip Stmt
DISP	seq_df	{[SOFT} < st1:st1:* > ; {\\} < st2:st2:* > {]}== < st1 > ; < st2 >
ABS	seq	st1; st2 == en.case st1 en of StmtValueExc(en',ex) - > st1 en | StmtValueNorm(en') - > st2 en'
THM	seq_wf	f:Atom . s:Spec. st1,st2:Stmt. st1; st2 Stmt
DISP	throw_df	throw( < e:e:* > )== throw( < e > )
ABS	throw	throw(e) == en.case e en of Exc(en',ex) - > StmtValueExc(en';ex) | Make(en',v) - > StmtValueExc(en';v)
THM	throw_wf	f:Atom . s:Spec. e:Exp(Exception). throw(e) Stmt
DISP	if_df	if( < b:b:* > ; < c:c:* > ; < d:d:* > ; < f:f:* > ; < s:s:* > )== if( < b > ; < c > ; < d > ; < f > ; < s > )
ABS	if	if(b;c;d;f;s) == en.case b en of Exc(en',ex) - > StmtValueExc(en';ex) | Make(en',bv) - > case get_j_cor(bv;f;s) of Jc - > StmtValueExc(en';JConst( " NilPointerE xception " ;Exception)) | Jac(bav) - > if bav then c en' else d en' fi
THM	if_wf	f:Atom . s:Spec. b:Exp(boolean). c,d:Stmt. if(b;c;d;f;s) Stmt
DISP	var_assig_df	( < v:atom:* > : < t:jtype:* > ) := < e:exp:* > == ( < v > : < t > ) := < e >
ABS	var_assig	(v:t) := e == en.case e en of Exc(en',exc) - > StmtValueExc(en';exc) | Make(en',o) - > StmtValueNorm(en'{(v:t) - > o})
THM	var_assig_wf	f:Atom . s:Spec. v:Atom. t:Type. e:Exp(t). (v:t) := e Stmt

the other theories