Commit 2a3bc980 authored by Michael Kohlhase's avatar Michael Kohlhase

changing_the_optional_value_of_\defi_and_friends_from_the_name_to_a_keyval_argument

parent efa1421c
\begin{mhmodnl}[creators=miko]{abstract-reduction-system}{en}
\begin{definition}
An \defiii{abstract}{reduction}{system} (or
\defiii[abstract-reduction-system]{abstract}{rewriting}{system}, or
\defi[abstract-reduction-system]{ARS}) $\mvstructure{A,R}$ consists of a set $A$
\defiii[name=abstract-reduction-system]{abstract}{rewriting}{system}, or
\defi[name=abstract-reduction-system]{ARS}) $\mvstructure{A,R}$ consists of a set $A$
together with a relation $\sseteq{R}{\twodim{A}}$. The relation $R$ is written as
$\arsRconvOp{R}$ or simply as $\arsconvOp$.
......
\begin{mhmodnl}[creators=miko]{alpharenaming}{de}
\begin{definition}
Wir nennen eine Formel $\bA$ eine \defii[alphabetic-variant]{alphabetische}{Variante}
von $\bB$ (oder \adefii[alphabetic-variant]{$\alphaeqFN$-gleich}{alpha}{gleich};
Wir nennen eine Formel $\bA$ eine \defii[name=alphabetic-variant]{alphabetische}{Variante}
von $\bB$ (oder \adefii[name=alphabetic-variant]{$\alphaeqFN$-gleich}{alpha}{gleich};
schreibe $\alphaeq{\bA,\bB}$), wenn $\bB$ aus $\bA$ hervorgeht durch systematische
Umbenennung gebundener Variablen.
\end{definition}
......
\begin{mhmodnl}[creators=jusche]{alpharenaming}{en}
\begin{definition}
We call a formula $\bA$ an \defii{alphabetic}{variant} of $\bB$ (or
\adefii[alphabetic-variant]{$\alphaeqFN$-equal}{alpha}{equal}; write
\adefii[name=alphabetic-variant]{$\alphaeqFN$-equal}{alpha}{equal}; write
$\alphaeq{\bA,\bB}$), iff $\bB$ can be obtained from $\bA$ by systematically renaming
bound variables.
\end{definition}
......
......@@ -4,7 +4,7 @@
$\mvstructure{A,R}$
\begin{itemize}
\item has the \defii{diamond}{property} (or is
\defii[diamond-property]{strongly}{confluent}), iff for every $\minset{a,b,c}A$ with
\defii[name=diamond-property]{strongly}{confluent}), iff for every $\minset{a,b,c}A$ with
$\arsRconv{R}ab$ and $\arsRconv{R}ac$ there is a $\inset{d}A$ with $\arsRconv{R}bd$
and $\arsRconv{R}cd$.
\item is \defi{confluent}, iff for every $\minset{a,b,c}A$ with $\arsRconvtr{R}ab$
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment