Backport specification from my PhD thesis

This replaces the text of the specification and the rule list with the text in my PhD thesis.

Most importantly this adds an abstract proof checking procedure that specifies the semantic of an Altehe proof (modulo the proof rules).

Furthermore, it adapts the notation more to SMT-LIB: everything is in λ-application style ((f x) instead of f(x)) and we no longer have a distinct connective. Instead we use the equality predicate everywhere.

On the technical side this now requires lualatex for Unicode math.

spec/doc.tex

@@ -560,7 +560,7 @@ substitution for $x_n$:
 \]
 
 When $\Gamma$ ends in a mapping, the substitution is extended
-with this mapping:
+with this mapping\label{page:ctxdef}:
 \[
 \subst([c_1,\dots, c_{n-1}, x_n\mapsto t_n]) =
         \subst([c_1,\dots, c_{n-1}])\circ \{x_n\mapsto t_n\}.
@@ -799,8 +799,6 @@ a \index{rule!concluding}{\em concluding rule}
 After the \inlineAlethe{anchor} command, the proof uses \inlineAlethe{assume} commands to list
 the assumptions of the subproof.  Subsequently, the subproof is a list of
 \inlineAlethe{step} commands that can use prior steps in the subproofs as premises.
-% the assumptions of any parent subproof
-% as premises.
 
 In the abstract notation, every step is associated with a context.  The
 concrete syntax uses anchors to optimize this.
@@ -814,10 +812,16 @@ corresponding \inlineAlethe{step} commands pop from the context.
 To indicate these changes to the context, every anchor is associated with a list
 of fixed variables and mappings.
 This list can be empty.
-
-The \inlineAlethe{:step} annotation of the anchor command is used to indicate the \inlineAlethe{step}
-command that will end the subproof.  The clause of this \inlineAlethe{step}
-command is the conclusion of the subproof.   While it is possible to infer the
+Note that, when an \inlineAlethe{anchor} command extends a context $\Gamma$ with
+some mappings $x_1 \mapsto t_1, \dots,  x_n \mapsto t_n$,
+then the terms $t_i$ are normalized by applying
+the substitution $\subst(\Gamma)$ to $t_i$.  This is because the definition
+on page~\pageref{page:ctxdef} extends the context by composing the substitutions.
+
+The \inlineAlethe{:step} annotation of the anchor command is used to indicate
+the \inlineAlethe{step} command that will end the subproof.  The clause of
+this \inlineAlethe{step} command is the conclusion of the subproof.
+While it is possible to infer the
 step that concludes a subproof from the structure of the proof, the explicit
 annotation simplifies proof checking and makes the proof easier to read.
 If the subproof uses a
@@ -1574,13 +1578,12 @@ is a clause that has been derived from the premises by some binary
 resolution steps.
 
 \paragraph{Quantifier Instantiation}
-\label{reference=rule:forall_inst}
 To express quantifier instantiation, the rule \proofRule{forall_inst}
 is used. It produces a formula of the form $(\neg \forall \bar
 x_n.\,\varphi) \lor \varphi[\bar t_n]$, where $\varphi$ is
 a term containing the free variables $\bar x_n$, and for each $i$ the
 ground term $t_i$ is a new term with the same sort as $x_i$.\footnote{
-  For historical reasons, \proofRule{forall} has a unit clause with a disjunction
+  For historical reasons, \proofRule{forall_inst} has a unit clause with a disjunction
   as its conclusion and not the clause $(\neg \forall \bar x_n.\,\varphi), \varphi[\bar t_n]$.
 }