18537

1 


2 
(* $Id$ *)


3 


4 
theory logic imports base begin


5 

20470

6 
chapter {* Primitive logic \label{ch:logic} *}

18537

7 

20480

8 
text {*


9 
The logical foundations of Isabelle/Isar are that of the Pure logic,


10 
which has been introduced as a naturaldeduction framework in


11 
\cite{paulson700}. This is essentially the same logic as ``@{text

20493

12 
"\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)

20480

13 
\cite{BarendregtGeuvers:2001}, although there are some key

20491

14 
differences in the specific treatment of simple types in


15 
Isabelle/Pure.

20480

16 


17 
Following typetheoretic parlance, the Pure logic consists of three


18 
levels of @{text "\<lambda>"}calculus with corresponding arrows: @{text


19 
"\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text


20 
"\<And>"} for universal quantification (proofs depending on terms), and


21 
@{text "\<Longrightarrow>"} for implication (proofs depending on proofs).


22 


23 
Pure derivations are relative to a logical theory, which declares

20491

24 
type constructors, term constants, and axioms. Theory declarations


25 
support schematic polymorphism, which is strictly speaking outside


26 
the logic.\footnote{Incidently, this is the main logical reason, why


27 
the theory context @{text "\<Theta>"} is separate from the context @{text


28 
"\<Gamma>"} of the core calculus.}

20480

29 
*}


30 


31 

20451

32 
section {* Types \label{sec:types} *}

20437

33 


34 
text {*

20480

35 
The language of types is an uninterpreted ordersorted firstorder


36 
algebra; types are qualified by ordered type classes.


37 


38 
\medskip A \emph{type class} is an abstract syntactic entity


39 
declared in the theory context. The \emph{subclass relation} @{text


40 
"c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic

20491

41 
generating relation; the transitive closure is maintained


42 
internally. The resulting relation is an ordering: reflexive,


43 
transitive, and antisymmetric.

20451

44 

20480

45 
A \emph{sort} is a list of type classes written as @{text


46 
"{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic


47 
intersection. Notationally, the curly braces are omitted for


48 
singleton intersections, i.e.\ any class @{text "c"} may be read as


49 
a sort @{text "{c}"}. The ordering on type classes is extended to

20491

50 
sorts according to the meaning of intersections: @{text


51 
"{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff


52 
@{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection


53 
@{text "{}"} refers to the universal sort, which is the largest


54 
element wrt.\ the sort order. The intersections of all (finitely


55 
many) classes declared in the current theory are the minimal


56 
elements wrt.\ the sort order.

20480

57 

20491

58 
\medskip A \emph{fixed type variable} is a pair of a basic name

20493

59 
(starting with a @{text "'"} character) and a sort constraint. For

20480

60 
example, @{text "('a, s)"} which is usually printed as @{text


61 
"\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an


62 
indexname and a sort constraint. For example, @{text "(('a, 0),

20491

63 
s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.

20451

64 

20480

65 
Note that \emph{all} syntactic components contribute to the identity

20493

66 
of type variables, including the sort constraint. The core logic


67 
handles type variables with the same name but different sorts as


68 
different, although some outer layers of the system make it hard to


69 
produce anything like this.

20451

70 

20493

71 
A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}ary operator


72 
on types declared in the theory. Type constructor application is

20494

73 
usually written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.


74 
For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text


75 
"prop"} instead of @{text "()prop"}. For @{text "k = 1"} the


76 
parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text


77 
"(\<alpha>)list"}. Further notation is provided for specific constructors,


78 
notably the rightassociative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of


79 
@{text "(\<alpha>, \<beta>)fun"}.

20480

80 


81 
A \emph{type} is defined inductively over type variables and type

20491

82 
constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s  ?\<alpha>\<^isub>s 

20494

83 
(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.

20451

84 

20494

85 
A \emph{type abbreviation} is a syntactic abbreviation @{text


86 
"(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over


87 
variables @{text "\<^vec>\<alpha>"}. Type abbreviations looks like type


88 
constructors at the surface, but are fully expanded before entering


89 
the logical core.

20480

90 


91 
A \emph{type arity} declares the image behavior of a type

20494

92 
constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,


93 
s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is


94 
of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is


95 
of sort @{text "s\<^isub>i"}. Arity declarations are implicitly


96 
completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::

20491

97 
(\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.


98 


99 
\medskip The sort algebra is always maintained as \emph{coregular},


100 
which means that type arities are consistent with the subclass

20494

101 
relation: for each type constructor @{text "\<kappa>"} and classes @{text


102 
"c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::


103 
(\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>

20480

104 
:: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>

20494

105 
\<^vec>s\<^isub>2"} holds componentwise.

20451

106 

20491

107 
The key property of a coregular ordersorted algebra is that sort

20494

108 
constraints may be always solved in a most general fashion: for each


109 
type constructor @{text "\<kappa>"} and sort @{text "s"} there is a most


110 
general vector of argument sorts @{text "(s\<^isub>1, \<dots>,

20491

111 
s\<^isub>k)"} such that a type scheme @{text

20494

112 
"(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is

20491

113 
of sort @{text "s"}. Consequently, the unification problem on the


114 
algebra of types has most general solutions (modulo renaming and


115 
equivalence of sorts). Moreover, the usual typeinference algorithm


116 
will produce primary types as expected \cite{nipkowprehofer}.

20480

117 
*}

20451

118 

20480

119 
text %mlref {*


120 
\begin{mldecls}


121 
@{index_ML_type class} \\


122 
@{index_ML_type sort} \\

20494

123 
@{index_ML_type arity} \\

20480

124 
@{index_ML_type typ} \\

20494

125 
@{index_ML fold_atyps: "(typ > 'a > 'a) > typ > 'a > 'a"} \\

20480

126 
@{index_ML Sign.subsort: "theory > sort * sort > bool"} \\


127 
@{index_ML Sign.of_sort: "theory > typ * sort > bool"} \\


128 
@{index_ML Sign.add_types: "(bstring * int * mixfix) list > theory > theory"} \\


129 
@{index_ML Sign.add_tyabbrs_i: "


130 
(bstring * string list * typ * mixfix) list > theory > theory"} \\


131 
@{index_ML Sign.primitive_class: "string * class list > theory > theory"} \\


132 
@{index_ML Sign.primitive_classrel: "class * class > theory > theory"} \\


133 
@{index_ML Sign.primitive_arity: "arity > theory > theory"} \\


134 
\end{mldecls}


135 


136 
\begin{description}


137 


138 
\item @{ML_type class} represents type classes; this is an alias for


139 
@{ML_type string}.


140 


141 
\item @{ML_type sort} represents sorts; this is an alias for


142 
@{ML_type "class list"}.

20451

143 

20480

144 
\item @{ML_type arity} represents type arities; this is an alias for

20494

145 
triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::

20480

146 
(\<^vec>s)s"} described above.


147 


148 
\item @{ML_type typ} represents types; this is a datatype with


149 
constructors @{ML TFree}, @{ML TVar}, @{ML Type}.


150 

20494

151 
\item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}


152 
over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text


153 
"\<tau>"}; the type structure is traversed from left to right.


154 

20480

155 
\item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}


156 
tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.


157 


158 
\item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type

20491

159 
is of a given sort.

20480

160 

20494

161 
\item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new


162 
type constructors @{text "\<kappa>"} with @{text "k"} arguments and

20480

163 
optional mixfix syntax.

20451

164 

20494

165 
\item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}


166 
defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with

20491

167 
optional mixfix syntax.

20480

168 


169 
\item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,

20494

170 
c\<^isub>n])"} declares new class @{text "c"}, together with class


171 
relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.

20480

172 


173 
\item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,


174 
c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>


175 
c\<^isub>2"}.


176 

20494

177 
\item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares


178 
arity @{text "\<kappa> :: (\<^vec>s)s"}.

20480

179 


180 
\end{description}

20437

181 
*}


182 


183 

20480

184 

20451

185 
section {* Terms \label{sec:terms} *}

18537

186 


187 
text {*

20451

188 
\glossary{Term}{FIXME}

18537

189 

20491

190 
The language of terms is that of simplytyped @{text "\<lambda>"}calculus


191 
with deBruijn indices for bound variables, and named free


192 
variables, and constants. Terms with loose bound variables are


193 
usually considered malformed. The types of variables and constants


194 
is stored explicitly at each occurrence in the term (which is a


195 
known performance issue).


196 

20451

197 
FIXME deBruijn representation of lambda terms

20480

198 


199 
Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}


200 
and application @{text "t u"}, while types are usually implicit


201 
thanks to typeinference.


202 


203 
Terms of type @{text "prop"} are called


204 
propositions. Logical statements are composed via @{text "\<And>x ::


205 
\<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.

20498

206 


207 


208 
\[


209 
\infer{@{text "(\<lambda>x\<^sub>\<tau>. t): \<tau> \<Rightarrow> \<sigma>"}}{@{text "t: \<sigma>"}}


210 
\qquad


211 
\infer{@{text "(t u): \<sigma>"}}{@{text "t: \<tau> \<Rightarrow> \<sigma>"} & @{text "u: \<tau>"}}


212 
\]


213 

18537

214 
*}


215 


216 


217 
text {*


218 


219 
FIXME


220 


221 
\glossary{Schematic polymorphism}{FIXME}


222 


223 
\glossary{Type variable}{FIXME}


224 


225 
*}


226 


227 

20451

228 
section {* Theorems \label{sec:thms} *}

18537

229 


230 
text {*


231 

20480

232 
Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>


233 
\<phi>"}, with standard introduction and elimination rules for @{text


234 
"\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and


235 
hypotheses @{text "A"} from the context @{text "\<Gamma>"}. The


236 
corresponding proof terms are left implicit in the classic


237 
``LCFapproach'', although they could be exploited separately


238 
\cite{BerghoferNipkow:2000}.


239 


240 
The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>


241 
\<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}conversion rules. The internal


242 
conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of


243 
assumptions and conclusions emerging uniformly as simultaneous


244 
statements.


245 


246 


247 

18537

248 
FIXME


249 


250 
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}


251 
@{text "prop"}. Internally, there is nothing special about


252 
propositions apart from their type, but the concrete syntax enforces a


253 
clear distinction. Propositions are structured via implication @{text


254 
"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"}  anything


255 
else is considered atomic. The canonical form for propositions is


256 
that of a \seeglossary{Hereditary Harrop Formula}.}


257 


258 
\glossary{Theorem}{A proven proposition within a certain theory and


259 
proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are


260 
rarely spelled out explicitly. Theorems are usually normalized


261 
according to the \seeglossary{HHF} format.}


262 


263 
\glossary{Fact}{Sometimes used interchangably for


264 
\seeglossary{theorem}. Strictly speaking, a list of theorems,


265 
essentially an extralogical conjunction. Facts emerge either as


266 
local assumptions, or as results of local goal statements  both may


267 
be simultaneous, hence the list representation.}


268 


269 
\glossary{Schematic variable}{FIXME}


270 


271 
\glossary{Fixed variable}{A variable that is bound within a certain


272 
proof context; an arbitrarybutfixed entity within a portion of proof


273 
text.}


274 


275 
\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}


276 


277 
\glossary{Bound variable}{FIXME}


278 


279 
\glossary{Variable}{See \seeglossary{schematic variable},


280 
\seeglossary{fixed variable}, \seeglossary{bound variable}, or


281 
\seeglossary{type variable}. The distinguishing feature of different


282 
variables is their binding scope.}


283 

20498

284 


285 
\[


286 
\infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}


287 
\qquad


288 
\infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}


289 
\]


290 
\[


291 
\infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}}


292 
\qquad


293 
\infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}


294 
\]


295 
\[


296 
\infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma>  A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}


297 
\qquad


298 
\infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}


299 
\]

18537

300 

20491

301 

20498

302 
Admissible rules:


303 
\[


304 
\infer[@{text "(generalize_type)"}]{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}


305 
\qquad


306 
\infer[@{text "(generalize_term)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}


307 
\]


308 
\[


309 
\infer[@{text "(instantiate_type)"}]{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}


310 
\qquad


311 
\infer[@{text "(instantiate_term)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}


312 
\]

18537

313 

20498

314 
Note that @{text "instantiate_term"} could be derived using @{text


315 
"\<And>_intro/elim"}, but this is not how it is implemented. The type


316 
instantiation rule is a genuine admissible one, due to the lack of true


317 
polymorphism in the logic.


318 


319 


320 
Equality and logical equivalence:


321 


322 
\smallskip


323 
\begin{tabular}{ll}


324 
@{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\


325 
@{text "\<turnstile> x \<equiv> x"} & reflexivity law \\


326 
@{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\


327 
@{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\


328 
@{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\


329 
\end{tabular}


330 
\smallskip


331 


332 


333 

20491

334 
*}

18537

335 

20480

336 

20491

337 
section {* Rules \label{sec:rules} *}

18537

338 


339 
text {*


340 


341 
FIXME


342 

20491

343 
A \emph{rule} is any Pure theorem in HHF normal form; there is a


344 
separate calculus for rule composition, which is modeled after


345 
Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows


346 
rules to be nested arbitrarily, similar to \cite{extensions91}.


347 


348 
Normally, all theorems accessible to the user are proper rules.


349 
Lowlevel inferences are occasional required internally, but the


350 
result should be always presented in canonical form. The higher


351 
interfaces of Isabelle/Isar will always produce proper rules. It is


352 
important to maintain this invariant in addon applications!


353 


354 
There are two main principles of rule composition: @{text


355 
"resolution"} (i.e.\ backchaining of rules) and @{text


356 
"byassumption"} (i.e.\ closing a branch); both principles are


357 
combined in the variants of @{text "elimresosultion"} and @{text


358 
"destresolution"}. Raw @{text "composition"} is occasionally


359 
useful as well, also it is strictly speaking outside of the proper


360 
rule calculus.


361 


362 
Rules are treated modulo general higherorder unification, which is


363 
unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}conversion


364 
on @{text "\<lambda>"}terms. Moreover, propositions are understood modulo


365 
the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.


366 


367 
This means that any operations within the rule calculus may be


368 
subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}HHF conversions. It is common


369 
practice not to contract or expand unnecessarily. Some mechanisms


370 
prefer an one form, others the opposite, so there is a potential


371 
danger to produce some oscillation!


372 


373 
Only few operations really work \emph{modulo} HHF conversion, but


374 
expect a normal form: quantifiers @{text "\<And>"} before implications


375 
@{text "\<Longrightarrow>"} at each level of nesting.


376 

18537

377 
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF


378 
format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>


379 
A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.


380 
Any proposition may be put into HHF form by normalizing with the rule


381 
@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost


382 
quantifier prefix is represented via \seeglossary{schematic


383 
variables}, such that the toplevel structure is merely that of a


384 
\seeglossary{Horn Clause}}.


385 


386 
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}


387 

20498

388 


389 
\[


390 
\infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}


391 
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}


392 
\]


393 


394 


395 
\[


396 
\infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}


397 
{@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}


398 
\]


399 


400 


401 
\[


402 
\infer[@{text "(\<And>_lift)"}]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}}


403 
\]


404 
\[


405 
\infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}


406 
\]


407 


408 
The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},


409 
@{text "\<Longrightarrow>_lift"}, and @{text compose}.


410 


411 
\[


412 
\infer[@{text "(resolution)"}]


413 
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}


414 
{\begin{tabular}{l}


415 
@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\


416 
@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\


417 
@{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\


418 
\end{tabular}}


419 
\]


420 


421 


422 
FIXME @{text "elim_resolution"}, @{text "dest_resolution"}

18537

423 
*}


424 

20498

425 

18537

426 
end
