author | paulson |

Mon Jan 11 10:22:04 1999 +0100 (1999-01-11) | |

changeset 6076 | 560396301672 |

parent 6075 | c148037f53c6 |

child 6077 | 60d97d521453 |

tidying, e.g. from \\tt to \\texttt

1.1 --- a/doc-src/Logics/HOL.tex Sat Jan 09 17:55:54 1999 +0100 1.2 +++ b/doc-src/Logics/HOL.tex Mon Jan 11 10:22:04 1999 +0100 1.3 @@ -203,7 +203,7 @@ 1.4 denote something, a description is always meaningful, but we do not 1.5 know its value unless $P$ defines it uniquely. We may write 1.6 descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax 1.7 -\hbox{\tt \at $x$. $P[x]$}. 1.8 +\hbox{\tt \at $x$.\ $P[x]$}. 1.9 1.10 Existential quantification is defined by 1.11 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] 1.12 @@ -222,7 +222,7 @@ 1.13 available. Both notations are accepted for input. The {\ML} reference 1.14 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt 1.15 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set 1.16 -to \texttt{false}, then~{\tt ALL} and~{\tt EX} are displayed. 1.17 +to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed. 1.18 1.19 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a 1.20 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined 1.21 @@ -253,7 +253,7 @@ 1.22 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} 1.23 and \sdx{of} are reserved words. Initially, this is mere syntax and has no 1.24 logical meaning. By declaring translations, you can cause instances of the 1.25 -{\tt case} construct to denote applications of particular case operators. 1.26 +\texttt{case} construct to denote applications of particular case operators. 1.27 This is what happens automatically for each \texttt{datatype} definition 1.28 (see~\S\ref{sec:HOL:datatype}). 1.29 1.30 @@ -590,13 +590,13 @@ 1.31 $\neg(a\in b)$. 1.32 1.33 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in 1.34 -the obvious manner using~{\tt insert} and~$\{\}$: 1.35 +the obvious manner using~\texttt{insert} and~$\{\}$: 1.36 \begin{eqnarray*} 1.37 \{a, b, c\} & \equiv & 1.38 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) 1.39 \end{eqnarray*} 1.40 1.41 -The set \hbox{\tt{\ttlbrace}$x$. $P[x]${\ttrbrace}} consists of all $x$ (of suitable type) 1.42 +The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type) 1.43 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free 1.44 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda 1.45 x. P[x])$. It defines sets by absolute comprehension, which is impossible 1.46 @@ -612,19 +612,19 @@ 1.47 write\index{*"! symbol}\index{*"? symbol} 1.48 \index{*ALL symbol}\index{*EX symbol} 1.49 % 1.50 -\hbox{\tt !~$x$:$A$. $P[x]$} and \hbox{\tt ?~$x$:$A$. $P[x]$}. Isabelle's 1.51 +\hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's 1.52 usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted 1.53 for input. As with the primitive quantifiers, the {\ML} reference 1.54 \ttindex{HOL_quantifiers} specifies which notation to use for output. 1.55 1.56 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and 1.57 $\bigcap@{x\in A}B[x]$, are written 1.58 -\sdx{UN}~\hbox{\tt$x$:$A$. $B[x]$} and 1.59 -\sdx{INT}~\hbox{\tt$x$:$A$. $B[x]$}. 1.60 +\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and 1.61 +\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}. 1.62 1.63 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x 1.64 -B[x]$, are written \sdx{UN}~\hbox{\tt$x$. $B[x]$} and 1.65 -\sdx{INT}~\hbox{\tt$x$. $B[x]$}. They are equivalent to the previous 1.66 +B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and 1.67 +\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous 1.68 union and intersection operators when $A$ is the universal set. 1.69 1.70 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are 1.71 @@ -905,9 +905,8 @@ 1.72 1.73 \subsection{Simplification and substitution} 1.74 1.75 -Simplification tactics tactics such as {\tt 1.76 - Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset 1.77 -({\tt simpset()}), which works for most purposes. A quite minimal 1.78 +Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset 1.79 +(\texttt{simpset()}), which works for most purposes. A quite minimal 1.80 simplification set for higher-order logic is~\ttindexbold{HOL_ss}; 1.81 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which 1.82 also expresses logical equivalence, may be used for rewriting. See 1.83 @@ -946,7 +945,7 @@ 1.84 \label{subsec:HOL:case:splitting} 1.85 1.86 \HOL{} also provides convenient means for case splitting during 1.87 -rewriting. Goals containing a subterm of the form {\tt if}~$b$~{\tt 1.88 +rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt 1.89 then\dots else\dots} often require a case distinction on $b$. This is 1.90 expressed by the theorem \tdx{split_if}: 1.91 $$ 1.92 @@ -1006,7 +1005,7 @@ 1.93 rule; recall Fig.\ts\ref{hol-lemmas2} above. 1.94 1.95 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt 1.96 -Best_tac} refer to the default claset ({\tt claset()}), which works for most 1.97 +Best_tac} refer to the default claset (\texttt{claset()}), which works for most 1.98 purposes. Named clasets include \ttindexbold{prop_cs}, which includes the 1.99 propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier 1.100 rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules, 1.101 @@ -1076,12 +1075,12 @@ 1.102 In addition, it is possible to use tuples 1.103 as patterns in abstractions: 1.104 \begin{center} 1.105 -{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$. $t$)} 1.106 +{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} 1.107 \end{center} 1.108 Nested patterns are also supported. They are translated stepwise: 1.109 {\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$ 1.110 {\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$ 1.111 - $z$. $t$))}. The reverse translation is performed upon printing. 1.112 + $z$.\ $t$))}. The reverse translation is performed upon printing. 1.113 \begin{warn} 1.114 The translation between patterns and \texttt{split} is performed automatically 1.115 by the parser and printer. Thus the internal and external form of a term 1.116 @@ -1273,8 +1272,8 @@ 1.117 Reasoning about arithmetic inequalities can be tedious. A minimal amount of 1.118 automation is provided by the tactic \ttindex{trans_tac} of type \texttt{int -> 1.119 tactic} that deals with simple inequalities. Note that it only knows about 1.120 -{\tt 0}, \texttt{Suc}, {\tt<} and {\tt<=}. The following goals are all solved by 1.121 -{\tt trans_tac 1}: 1.122 +\texttt{0}, \texttt{Suc}, {\tt<} and {\tt<=}. The following goals are all solved by 1.123 +\texttt{trans_tac 1}: 1.124 \begin{ttbox} 1.125 {\out 1. \dots ==> m <= Suc(Suc m)} 1.126 {\out 1. [| \dots i <= j \dots Suc j <= k \dots |] ==> i < k} 1.127 @@ -1425,7 +1424,7 @@ 1.128 which can be fed to \ttindex{addsplits} just like 1.129 \texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}). 1.130 1.131 -{\tt List} provides a basic library of list processing functions defined by 1.132 +\texttt{List} provides a basic library of list processing functions defined by 1.133 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations 1.134 are shown in Fig.\ts\ref{fig:HOL:list-simps}. 1.135 1.136 @@ -1784,7 +1783,7 @@ 1.137 \label{sec:HOL:datatype} 1.138 \index{*datatype|(} 1.139 1.140 -Inductive datatypes, similar to those of \ML, frequently appear in actual 1.141 +Inductive datatypes, similar to those of \ML, frequently appear in 1.142 applications of Isabelle/HOL. In principle, such types could be defined by 1.143 hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too 1.144 tedious. The \ttindex{datatype} definition package of \HOL\ automates such 1.145 @@ -1832,12 +1831,12 @@ 1.146 (\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t' 1.147 \] 1.148 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple 1.149 -example of a datatype is the type {\tt list}, which can be defined by 1.150 +example of a datatype is the type \texttt{list}, which can be defined by 1.151 \begin{ttbox} 1.152 datatype 'a list = Nil 1.153 | Cons 'a ('a list) 1.154 \end{ttbox} 1.155 -Arithmetic expressions {\tt aexp} and boolean expressions {\tt bexp} can be modelled 1.156 +Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled 1.157 by the mutually recursive datatype definition 1.158 \begin{ttbox} 1.159 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp) 1.160 @@ -1849,7 +1848,7 @@ 1.161 | And ('a bexp) ('a bexp) 1.162 | Or ('a bexp) ('a bexp) 1.163 \end{ttbox} 1.164 -The datatype {\tt term}, which is defined by 1.165 +The datatype \texttt{term}, which is defined by 1.166 \begin{ttbox} 1.167 datatype ('a, 'b) term = Var 'a 1.168 | App 'b ((('a, 'b) term) list) 1.169 @@ -1869,7 +1868,7 @@ 1.170 must have a constructor $C^j@i$ without recursive arguments, a \emph{base 1.171 case}, to ensure that the new types are non-empty. If there are nested 1.172 occurrences, a datatype can even be non-empty without having a base case 1.173 -itself. Since {\tt list} is a non-empty datatype, {\tt datatype t = C (t 1.174 +itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t 1.175 list)} is non-empty as well. 1.176 1.177 The datatype constructors are automatically defined as functions of their 1.178 @@ -1935,7 +1934,7 @@ 1.179 \] 1.180 i.e.\ the properties $P@j$ can be assumed for all recursive arguments. 1.181 1.182 -For datatypes with nested recursion, such as the {\tt term} example from 1.183 +For datatypes with nested recursion, such as the \texttt{term} example from 1.184 above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds 1.185 a definition like 1.186 \begin{ttbox} 1.187 @@ -1949,11 +1948,11 @@ 1.188 and ('a, 'b) term_list = Nil' 1.189 | Cons' (('a,'b) term) (('a,'b) term_list) 1.190 \end{ttbox} 1.191 -Note however, that the type {\tt ('a,'b) term_list} and the constructors {\tt 1.192 - Nil'} and {\tt Cons'} are not really introduced. One can directly work with 1.193 -the original (isomorphic) type {\tt (('a, 'b) term) list} and its existing 1.194 -constructors {\tt Nil} and {\tt Cons}. Thus, the structural induction rule for 1.195 -{\tt term} gets the form 1.196 +Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt 1.197 + Nil'} and \texttt{Cons'} are not really introduced. One can directly work with 1.198 +the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing 1.199 +constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for 1.200 +\texttt{term} gets the form 1.201 \[ 1.202 \infer{P@1~x@1 \wedge P@2~x@2} 1.203 {\begin{array}{l} 1.204 @@ -1963,11 +1962,11 @@ 1.205 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2) 1.206 \end{array}} 1.207 \] 1.208 -Note that there are two predicates $P@1$ and $P@2$, one for the type {\tt ('a,'b) term} 1.209 -and one for the type {\tt (('a, 'b) term) list}. 1.210 +Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term} 1.211 +and one for the type \texttt{(('a, 'b) term) list}. 1.212 1.213 \medskip In principle, inductive types are already fully determined by 1.214 -freeness and structural induction. For convenience in actual applications, 1.215 +freeness and structural induction. For convenience in applications, 1.216 the following derived constructions are automatically provided for any 1.217 datatype. 1.218 1.219 @@ -2065,8 +2064,8 @@ 1.220 {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous 1.221 structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This 1.222 is the canonical way to prove properties of mutually recursive datatypes 1.223 - such as {\tt aexp} and {\tt bexp}, or datatypes with nested recursion such as 1.224 - {\tt term}. 1.225 + such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as 1.226 + \texttt{term}. 1.227 \end{ttdescription} 1.228 In some cases, induction is overkill and a case distinction over all 1.229 constructors of the datatype suffices. 1.230 @@ -2101,22 +2100,22 @@ 1.231 val size : thm list 1.232 val simps : thm list 1.233 \end{ttbox} 1.234 -{\tt distinct}, \texttt{inject}, \texttt{induct}, {\tt size} 1.235 -and {\tt split} contain the theorems 1.236 +\texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size} 1.237 +and \texttt{split} contain the theorems 1.238 described above. For user convenience, \texttt{distinct} contains 1.239 inequalities in both directions. The reduction rules of the {\tt 1.240 case}-construct are in \texttt{cases}. All theorems from {\tt 1.241 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. 1.242 -In case of mutually recursive datatypes, {\tt recs}, {\tt size}, {\tt induct} 1.243 -and {\tt simps} are contained in a separate structure named $t@1_\ldots_t@n$. 1.244 +In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct} 1.245 +and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. 1.246 1.247 1.248 \subsection{Representing existing types as datatypes} 1.249 1.250 -For foundational reasons, some basic types such as {\tt nat}, {\tt *}, {\tt 1.251 - +}, {\tt bool} and {\tt unit} are not defined in a {\tt datatype} section, 1.252 +For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt 1.253 + +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section, 1.254 but by more primitive means using \texttt{typedef}. To be able to use the 1.255 -tactics {\tt induct_tac} and {\tt exhaust_tac} and to define functions by 1.256 +tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by 1.257 primitive recursion on these types, such types may be represented as actual 1.258 datatypes. This is done by specifying an induction rule, as well as theorems 1.259 stating the distinctness and injectivity of constructors in a {\tt 1.260 @@ -2338,8 +2337,8 @@ 1.261 \end{ttbox} 1.262 1.263 \subsubsection{Example: Evaluation of expressions} 1.264 -Using mutual primitive recursion, we can define evaluation functions {\tt eval_aexp} 1.265 -and {\tt eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in 1.266 +Using mutual primitive recursion, we can define evaluation functions \texttt{eval_aexp} 1.267 +and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in 1.268 \S\ref{subsec:datatype:basics}: 1.269 \begin{ttbox} 1.270 consts 1.271 @@ -2359,13 +2358,13 @@ 1.272 "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)" 1.273 \end{ttbox} 1.274 Since the value of an expression depends on the value of its variables, 1.275 -the functions {\tt eval_aexp} and {\tt eval_bexp} take an additional 1.276 -parameter, an {\em environment} of type {\tt 'a => nat}, which maps 1.277 +the functions \texttt{eval_aexp} and \texttt{eval_bexp} take an additional 1.278 +parameter, an {\em environment} of type \texttt{'a => nat}, which maps 1.279 variables to their values. 1.280 1.281 -Similarly, we may define substitution functions {\tt subst_aexp} 1.282 -and {\tt subst_bexp} for expressions: The mapping {\tt f} of type 1.283 -{\tt 'a => 'a aexp} given as a parameter is lifted canonically 1.284 +Similarly, we may define substitution functions \texttt{subst_aexp} 1.285 +and \texttt{subst_bexp} for expressions: The mapping \texttt{f} of type 1.286 +\texttt{'a => 'a aexp} given as a parameter is lifted canonically 1.287 on the types {'a aexp} and {'a bexp}: 1.288 \begin{ttbox} 1.289 consts 1.290 @@ -2400,10 +2399,10 @@ 1.291 1.292 \subsubsection{Example: A substitution function for terms} 1.293 Functions on datatypes with nested recursion, such as the type 1.294 -{\tt term} mentioned in \S\ref{subsec:datatype:basics}, are 1.295 +\texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are 1.296 also defined by mutual primitive recursion. A substitution 1.297 -function {\tt subst_term} on type {\tt term}, similar to the functions 1.298 -{\tt subst_aexp} and {\tt subst_bexp} described above, can 1.299 +function \texttt{subst_term} on type \texttt{term}, similar to the functions 1.300 +\texttt{subst_aexp} and \texttt{subst_bexp} described above, can 1.301 be defined as follows: 1.302 \begin{ttbox} 1.303 consts 1.304 @@ -2420,7 +2419,7 @@ 1.305 subst_term f t # subst_term_list f ts" 1.306 \end{ttbox} 1.307 The recursion scheme follows the structure of the unfolded definition of type 1.308 -{\tt term} shown in \S\ref{subsec:datatype:basics}. To prove properties of 1.309 +\texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of 1.310 this substitution function, mutual induction is needed: 1.311 \begin{ttbox} 1.312 Goal 1.313 @@ -2653,7 +2652,7 @@ 1.314 1.315 \item[\tt elims] is the list of elimination rule. 1.316 1.317 -\item[\tt elim] is the head of the list {\tt elims}. 1.318 +\item[\tt elim] is the head of the list \texttt{elims}. 1.319 1.320 \item[\tt mk_cases] is a function to create simplified instances of {\tt 1.321 elim}, using freeness reasoning on some underlying datatype. 1.322 @@ -2695,7 +2694,7 @@ 1.323 con_defs {\it constructor definitions} 1.324 \end{ttbox} 1.325 A coinductive definition is identical, except that it starts with the keyword 1.326 -{\tt coinductive}. 1.327 +\texttt{coinductive}. 1.328 1.329 The \texttt{monos} and \texttt{con_defs} sections are optional. If present, 1.330 each is specified by a list of identifiers. 1.331 @@ -2719,7 +2718,7 @@ 1.332 1.333 \subsection{Example of an inductive definition} 1.334 Two declarations, included in a theory file, define the finite powerset 1.335 -operator. First we declare the constant~{\tt Fin}. Then we declare it 1.336 +operator. First we declare the constant~\texttt{Fin}. Then we declare it 1.337 inductively, with two introduction rules: 1.338 \begin{ttbox} 1.339 consts Fin :: 'a set => 'a set set 1.340 @@ -2728,13 +2727,13 @@ 1.341 emptyI "{\ttlbrace}{\ttrbrace} : Fin A" 1.342 insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A" 1.343 \end{ttbox} 1.344 -The resulting theory structure contains a substructure, called~{\tt Fin}. 1.345 +The resulting theory structure contains a substructure, called~\texttt{Fin}. 1.346 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs}, 1.347 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction 1.348 rule is \texttt{Fin.induct}. 1.349 1.350 For another example, here is a theory file defining the accessible 1.351 -part of a relation. The main thing to note is the use of~{\tt Pow} in 1.352 +part of a relation. The main thing to note is the use of~\texttt{Pow} in 1.353 the sole introduction rule, and the corresponding mention of the rule 1.354 \verb|Pow_mono| in the \texttt{monos} list. The paper 1.355 \cite{paulson-CADE} discusses a \ZF\ version of this example in more 1.356 @@ -2753,7 +2752,7 @@ 1.357 The Isabelle distribution contains many other inductive definitions. Simple 1.358 examples are collected on subdirectory \texttt{HOL/Induct}. The theory 1.359 \texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples 1.360 -may be found on other subdirectories of \texttt{HOL}, such as {\tt IMP}, 1.361 +may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP}, 1.362 \texttt{Lambda} and \texttt{Auth}. 1.363 1.364 \index{*coinductive|)} \index{*inductive|)} 1.365 @@ -2802,7 +2801,7 @@ 1.366 set of theorems defined inductively. A similar proof in \ZF{} is 1.367 described elsewhere~\cite{paulson-set-II}. 1.368 1.369 -\item Theory \texttt{Term} defines the datatype {\tt term}. 1.370 +\item Theory \texttt{Term} defines the datatype \texttt{term}. 1.371 1.372 \item Theory \texttt{ABexp} defines arithmetic and boolean expressions 1.373 as mutually recursive datatypes. 1.374 @@ -2951,7 +2950,7 @@ 1.375 {\out No subgoals!} 1.376 \end{ttbox} 1.377 How much creativity is required? As it happens, Isabelle can prove this 1.378 -theorem automatically. The default classical set {\tt claset()} contains rules 1.379 +theorem automatically. The default classical set \texttt{claset()} contains rules 1.380 for most of the constructs of \HOL's set theory. We must augment it with 1.381 \tdx{equalityCE} to break up set equalities, and then apply best-first 1.382 search. Depth-first search would diverge, but best-first search