Next:Basic definitions and properties Up:User's manual of the Previous:Basic definitions Contents

Matching

We define

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm caseP}\hspace{0.2em} \... ...eVerb{Verb}caseP f g z r\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

and we prove the following:

Using the definite description, we define:

$\begin{definition}[ match function on sums ]~ \begin{center}% \afdmath{}\text{\r... ...SaveVerb{Verb}case f g z\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Then using the properties of the definite description, we prove the following propositions.

$\begin{fact}[ Characteristic properties of case ]\hspace{1cm} \begin{itemize} \i... ...ight}.\text{\rm Sum}\endafdmath{} added as equation \par \end{itemize}\end{fact}$

we add these facts as rewriting rules and we close the definition of case .

We also prove :

$\begin{fact}[% \afdmath{}\text{\rm case}.\text{\rm total}.\text{\rm Sum}\endafdm... ...em} \text{\it z}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

case.total.Sum added as introduction rule (abbrev: case , options: -t )

List Christophe Raffalli, Paul Roziere Equipe de Logique, Université Chambéry, Paris VII

Christophe Raffalli 2005-03-02