DISP	sexpr_df	sExpr== sExpr
ABS	sexpr	sExpr == (Atom )
THM	sexpr_wf	sExpr
DISP	snum_df	<n:int:*>== <n>
ABS	snum	n == m.n
THM	snum_wf	n:. n sExpr
DISP	svar_df	<v:tok:*>== <v>
ABS	svar	v == m.m v
THM	svar_wf	v:Atom. v sExpr
DISP	sadd_df	<e1:e1:*> + <e2:e2:*>== <e1> + <e2>
ABS	sadd	e1 + e2 == m.e1 m + e2 m
THM	sadd_wf	e1,e2:sExpr. e1 + e2 sExpr
DISP	smul_df	<e1:e1:*> * <e2:e2:*>== <e1> * <e2>
ABS	smul	e1 * e2 == m.e1 m * e2 m
THM	smul_wf	e1,e2:sExpr. e1 * e2 sExpr
DISP	ssub_df	<e1:e1:*> - <e2:e2:*>== <e1> - <e2>
ABS	ssub	e1 - e2 == m.e1 m - e2 m
THM	ssub_wf	e1,e2:sExpr. e1 - e2 sExpr
DISP	sminus_df	-<e:e:*>== -<e>
ABS	sminus	-e == m.-(e m)
THM	sminus_wf	e:sExpr. -e sExpr
DISP	sbexpr_df	sBExpr== sBExpr
ABS	sbexpr	sBExpr == (Atom )
THM	sbexpr_wf	sBExpr
DISP	sbool_df	<b:bool:*>== <b>
ABS	sbool	b == m.b
THM	sbool_wf	b:. b sBExpr
DISP	sand_df	<b1:b1:*> and <b2:b2:*>== <b1> and <b2>
ABS	sand	b1 and b2 == m.b1 m b2 m
THM	sand_wf	b1,b2:sBExpr. b1 and b2 sBExpr
DISP	sor_df	<b1:b1:*> or <b2:b2:*>== <b1> or <b2>
ABS	sor	b1 or b2 == m.((b1 m) (b2 m))
THM	sor_wf	b1,b2:sBExpr. b1 or b2 sBExpr
DISP	snot_df	not <b:b:*>== not <b>
ABS	snot	not b == m.(b m)
THM	snot_wf	b:sBExpr. not b sBExpr
DISP	slt_df	<e1:e1:*> < <e2:e2:*>== <e1> < <e2>
ABS	slt	e1 < e2 == m.(e1 m) <z (e2 m)
THM	slt_wf	e1,e2:sExpr. e1 < e2 sBExpr
DISP	sequ_df	<e1:e1:*> == <e2:e2:*>== <e1> == <e2>
ABS	sequ	e1 == e2 == m.(e1 m = e2 m)
THM	sequ_wf	e1,e2:sExpr. e1 == e2 sBExpr
DISP	scom_df	sCom== sCom
ABS	scom	sCom == (Atom ) Atom
THM	scom_wf	sCom
DISP	sskip_df	skip== skip
ABS	sskip	skip == Id
THM	sskip_wf	skip sCom
DISP	sseq_df	<c1:com:*><c2:com:*>== <c1><c2>
ABS	sseq	c1;c2 == c2 o c1
THM	sseq_wf	c1,c2:sCom. c1;c2 sCom
DISP	sassig_df	<v:v:*> := <e:e:*>== <v> := <e>
ABS	sassig	v := e == m,i.if i=v then e m else (m i)
THM	sassig_wf	v:Atom. e:sExpr. v := e sCom
DISP	sif_df	if <b:b:*> then <c1:c1:*> else <c2:c2:*>== if <b> then <c1> else <c2>
ABS	sif	if b then c1 else c2 == m.if b m then c1 m else c2 m fi
THM	sif_wf	b:sBExpr. c1,c2:sCom. if b then c1 else c2 sCom
DISP	swhile_df	while <b:b:*> do <c:c:*>== while <b> do <c>
ML	swhile_ml	while b do c==r m.if b m then while b do c else m fi
THM	swhile_wf	[term]
DISP	sgcd_df	sGCD(<a:a:*><b:b:*>)== sGCD(<a><b>)
ABS	sgcd	sGCD(a;b) == while not a == b do if a < b then b := b - a else a := a - b
THM	sgcd_wf	[term]

the other theories