Next: Projections Up: User's manual of the Previous: Basic definitions. Contents

Subsections

Properties of basic operations and predicates on the product.

Basic definitions

To define the product of two predicates, we extend the language with one binary function symbol [ x, y ] . Then the product of two unary predicates is defined by the following predicate A × B

$\begin{definition}[ Product ]\hspace{1cm} \begin{itemize} \item product['a,'b] \... ...erb{Verb}¶Product A B p¶\marginpar{\UseVerb{Verb}} \end{itemize}\end{definition}$

The introduction rule for ×

$\begin{fact}[% \afdmath{}\text{\rm intro}.\text{\rm Product}\endafdmath{}]Produc... ...;\; \text{\it y}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

intro.Product added as introduction rule (abbrev: i , options: -i -c )

The elimination rules for ×

$\begin{fact}[% \afdmath{}\text{\rm elim}.\text{\rm Product}\endafdmath{}]Product... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

elim.Product added as elimination rule (abbrev: r , options: -i )

$\begin{axiom}[% \afdmath{}\text{\rm injective}.\text{\rm Product}\endafdmath{}]P... ...'\endprettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{axiom}$

$\begin{fact}[% \afdmath{}\text{\rm injective}\_\text{\rm left}.\text{\rm Product... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

injective_left.Product added as elimination rule (abbrev: Product , options: -i -n )

Christophe Raffalli 2005-03-02