Commit deec408b authored by Michael Kohlhase's avatar Michael Kohlhase


parent 71a260c2
Wir nennen eine Formel $\bA$ eine \defii[alphabetic-variant]{alphabetische}{Variante}
von $\bB$ (oder \adefii[alphabetic-variant]{$\alphaeqRel$-gleich}{alpha}{gleich};
von $\bB$ (oder \adefii[alphabetic-variant]{$\alphaeqFN$-gleich}{alpha}{gleich};
schreibe $\alphaeq\bA\bB$), wenn $\bB$ aus $\bA$ hervorgeht durch systematische
Umbenennung gebundener Variablen.
We call a formula $\bA$ an \defii{alphabetic}{variant} of $\bB$ (or
\adefii[alphabetic-variant]{$\alphaeqRel$-equal}{alpha}{equal}; write
\adefii[alphabetic-variant]{$\alphaeqFN$-equal}{alpha}{equal}; write
$\alphaeq\bA\bB$), iff $\bB$ can be obtained from $\bA$ by systematically renaming
bound variables.
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