MM2 tutorial: Reachability P3
Reachability is the task of determining which elements can be reached from an initial set by repeatedly applying a given relation. In this tutorial, we will explore various types of reachability tasks and demonstrate how to encode them in MM2.
Each example covers the goal and desired result, introduces the data, builds code stepwise, and walks through an execution trace showing how each statement affects the space.
At the end of each part, you’ll also find a few exercises to try on your own.
If any part of the code is unclear, it can be helpful to start with the execution trace: seeing how the space evolves often makes the intention of the rules easier to understand.
So far, we have explored reachability through fixed relationships and through pattern matching. In this part, we extend these ideas by considering reachability under cost, where only a limited amount of resources is available.
An example of such a problem is the following: suppose we have a street map in which streets may be one-way or two-way. Which buildings are reachable from a hospital within 15 minutes?
In this tutorial, we slightly abstract this scenario by assigning each street a discrete length and by assuming that buildings are located at street crossings. This abstraction keeps the example simple, while remaining easy to extend to more realistic settings.
We model a mock street map in which streets of varying length connect buildings. We will later use this data to determine which buildings are reachable from a hospital under a fixed cost bound.
In our mm2 representation, a street is represented by a fact of the form street x y d, stating that there is a street from building x to building y with length d.
Streets are directed: a statement (street A B 1) allows travel from A to B, but not from B to A.
If a street can be used in both directions, we explicitly add two facts, one for each direction.
The concrete street map used in this example looks like this:
We encode it in MM2 as follows:
(street A B 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street D F 1)
(street F I 1)
(street D A 1)
(street A D 1)
(street E B 1)
(street E G 1)
(street C H 2)
(street H C 2)
(street J H 1)
(street H G 1)
(street D E 1)
(street F G 1)
(street G F 1)
(street I J 2)
We assume that H represents the hospital.
The question we want to answer is: starting from H, which other buildings can be reached within, e.g., four steps?
Here is a diagram showing all reachable buildings from H in maximum four steps:
We now build up the mm2 code step by step.
Since we are interested in buildings that are reachable from H, we can start by defining our starting point. This keeps the code easily adjustable if we ever want to change the starting point.
(startpoint H)
To start, we simplify the problem by ignoring street lengths. Our first goal is to compute which buildings are reachable from the start point.
This can be done iteratively. If there is a path from H to a building $q, and there is a street from $q to a building $r, then there is also a path from H to $r.
We can encode this using the following execution statement:
(exec 1 (, (path $p $q) (street $q $r $d))
(, (path $p $r)))
Conceptually, applying this rule n times yields all buildings that are reachable from H by going through n streets.
However, in the initial space, there are no path statements yet.
Therefore, we first need to add an initial path statement.
(exec 0 (, (startpoint $p))
(, (path $p $p)))
(exec 1 (, (path $p $q) (street $q $r $d))
(, (path $p $r)))
This setup allows us to find paths starting from H that consist of a single street.
To explore further, we want to apply exec 1 iteratively, which we will do in a later step.
For testing purposes, you can either copy-paste exec 1 a few times, or make the execution statement iterative by using Peano numbers to impose a maximum number of iterations, as shown in the Reachability Part 2 tutorial.
No worries if you do not know how to do this yet: we are merely testing this preliminary code here, and will expand on it in the rest of this tutorial.
We now extend the previous code to account for distances. For each path, we track its total length in our mm2 statements.
(exec 0 (, (startpoint $p))
(, (path $p $p 0)))
(exec 1 (, (path $p $q $d) (street $q $r $e))
(, (path $q $r ($d + $e))))
If there is a path from $p to $q with length $d, and a street from $q to $r with length $e,
then there is a path from $p to $r with total length $d + $e.
Note that MM2 does not automatically evaluate arithmetic expressions.
An expression such as (d + e) is added to the space syntactically, without being reduced.
Note that MM2 does not automatically evaluate arithmetic expressions.
An expression such as (d + e) is added to the space syntactically, without being reduced.
For example, if we execute exec 1 from above a few times (which I recommend doing), we obtain statements like
(path H D (((2 + 1) + 1) + 1))
which indicates a path from H to D of length 5, but none of the sums were evaluated. We will later see how we can evaluate these sums.
Again, I recommend running this code for a few iterations and observing what happens, either by copying and pasting exec 1 a few times or by writing an iterative execution statement with a maximum number of iterations, as in the previous tutorial.
Next, we want to restrict reachability to paths whose total length stays below a fixed maximum from our start point H.
We store this maximum in the space:
(maxlength 4)
What we want to do is restrict path extension to paths whose total length stays below a given maximum. To express this, we need a way to check inequalities within execution statements.
Suppose we could create statements of the form (a <= b), which represent that the inequality holds.
If we include such a statement in the patterns of an execution statement, that execution statement will only be applied when the inequality is true.
Under this assumption, our path-extension rule would look as follows:
(exec 0 (, (startpoint $p))
(, (path $p $p 0)))
(exec 1 (, (path $p $q $d) (street $q $r $e)
(maxlength $max) (($d + $e) <= $max))
(, (path $p $r ($d + $e))))
Here, exec 1 will only be applied if a statement of the form (($d + $e) <= $max) exists in the space.
We retrieve the maximum allowed length from the space and extend a path only when the newly computed length does not exceed it.
However, just like with addition, MM2 does not automatically evaluate inequalities.
Expressions such as ($d + $e) and (($d + $e) <= $max) are treated purely syntactically and are added to the space as such.
As a result, the code above does not yet produce the intended behaviour. In the next step, we will fix this by explicitly adding rules that generate addition and inequality statements.
Although arithmetic operations will soon be added to the grounded functions of MM2, we currently need to add addition and inequality statements to the space explicitly.
The idea is to include statements of the form (x + y = z) for all combinations of x, y, and z for which this equation holds.
Similarly, we add statements representing inequalities of the form (x <= y).
These statements could be written by hand, but in practice, it is more convenient to generate them automatically using a programming language.
To make it clear that these statements represent arithmetic information, and to easily distinguish them from the rest of the data, we prefix them with arith.
Below is the Python script I used to generate these arithmetic statements.
print('\n'.join([f"(arith ({x} + {y} = {x+y}))" for x in range(9) for y in range(9)]))
print('\n')
print('\n'.join([f"(arith ({x} <= {y}))" for x in range(17) for y in range(x, 17)]))The generated output can either be copied and pasted directly into our MM2 work file, or written to a separate file, e.g., arith.mm2, to keep things organised.
Before running MM2, the files can simply be concatenated.
The resulting arith.mm2 file will have the following structure:
(arith (0 + 0 = 0))
(arith (0 + 1 = 1))
(arith (0 + 2 = 2))
(arith (0 + 3 = 3))
...
(arith (1 + 0 = 1))
(arith (1 + 1 = 2))
(arith (1 + 2 = 3))
(arith (1 + 3 = 4))
...
(arith (0 <= 0))
(arith (0 <= 1))
(arith (0 <= 2))
(arith (0 <= 3))
...
(arith (1 <= 1))
(arith (1 <= 2))
(arith (1 <= 3))
...
(arith (2 <= 2))
(arith (2 <= 3))
...
I will show the full contents of the file arith.mm2 at the end of this document.
We now take our previous MM2 code and make slight adjustments to make it work with these arithmetic statements.
(exec 0 (, (startpoint $p))
(, (path $p $p 0)))
(exec 1 (, (path $p $q $d) (street $q $r $e)
(arith ($d + $e = $f)) ; <--- add arith label
(maxlength $max) (arith ($f <= $max))) ; <--- add arith label
(, (path $q $r $f)))
This code now works for a single iteration. The final step is to make it iterative, so that paths can be extended multiple times.
As we saw in the Reachability Part One and Two tutorials, iteration in MM2 can be achieved by having an execution statement add itself back to the space. Let’s try this out.
Before running this code, note that it will result in an infinite loop.
I therefore recommend setting the --steps flag when executing it.
(exec 0 (, (startpoint $p))
(, (path $p $p 0)))
(exec 1 (, (exec 1 $ps $ts) ; <--- matches on itself
(path $p $q $d) (street $q $r $e)
(arith ($d + $e = $f))
(maxlength $max) (arith ($f <= $max)))
(, (path $q $r $f))
(exec 1 $ps $ts)) ; <--- adds itself back to the space
One might ask why this loops infinitely. At some point, we can no longer find paths from H that are shorter than maxlength, right?
That is indeed correct. However, even though we cannot add any new paths anymore, our MM2 code never removes statements from the space. As a result, the execution pattern continues to match, causing it to be executed again and again, each time adding itself back to the space.
So even though the space no longer changes, the execution does not terminate. We therefore need to add a stopping criterion.
As we saw in Part 2 of the reachability tutorial, there are (at least) three different stopping criteria for iterative processes:
- a maximum number of iterations,
- stopping when the space no longer changes,
- stopping when a specific statement is reached (with a backup plan in case it can never be reached).
Any of these approaches could be used here. However, since our goal is to find all paths whose distance is less than a given maximum, we stop the iteration once no further paths can be extended without exceeding it. In other words, we stop when the space can no longer change, similarly to the Reachability Part 1 tutorial.
How can we detect that the space has stopped changing? To do this, we group all atoms added during a given iteration by assigning them an iteration index.
In each iteration, we only build on the paths produced in the previous iteration, since all earlier paths have already been handled. If, at some point, we can no longer extend the newest paths without exceeding the maximum distance, the iterative process terminates.
(exec (0 0) (, (startpoint $p))
(, (path 0 $p $p 0)))
(exec (1 0) (, (exec (1 $n) $ps $ts) (arith ($n + 1 = $m)) ; <--- add iteration index $n
(path $n $p $q $d) (street $q $r $e) ; <--- add iteration index $n
(arith ($d + $e = $f))
(maxlength $max) (arith ($f <= $max)))
(, (path $m $q $r $f)) ; <--- add next iteration index $m
(exec (1 $m) $ps $ts)) ; <--- add next iteration index $m
If this is still unclear, don’t worry; it will become clearer in the complete run-through.
As a final step, one can collect all results and drop the iteration indices. This step is optional.
(exec (3 0)
(, (path $n H $q $d))
(, (reachable H $q)))
We will go through the execution steps of our MM2 program step by step.
You can recreate these results by running mork with the --steps flag.
Note that the arithmetic facts are stored in a separate file (arith.mm2).
For clarity, we omit these arith statements from the spaces shown in this run-through.
Putting all the code together, the initial space of our program looks as follows:
(maxlength 4)
(startpoint H)
(street A B 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street D F 1)
(street F I 1)
(street D A 1)
(street A D 1)
(street E B 1)
(street E G 1)
(street C H 2)
(street H C 2)
(street J H 1)
(street H G 1)
(street D E 1)
(street F G 1)
(street G F 1)
(street I J 2)
(exec (0 0) (, (startpoint $p) (street $p $q $d))
(, (path 1 $p $q $d)))
(exec (1 1)
(,
(exec (1 $n) $ps $ts) (arith ($n + 1 = $m))
(path $n $p $q $d) (street $q $r $e)
(arith ($d + $e = $f))
(maxlength $max) (arith ($f <= $max))
)
(,
(path $m $p $r $f)
(exec (1 $m) $ps $ts)
)
)
(exec (2 0)
(, (path $n H $q $d))
(, (reachable H $q)))
We save this code in a file named, for example, reachabilitypt3.mm2.
To run the program, we also need the arithmetic information stored in arith.mm2 (the complete code for this file is at the end of this tutorial).
One way to do this is to create a combined file (for example, eval.mm2) that contains the contents of both files.
From the command line, this can be done as follows:
cat arith.mm2 reachabilitypt3.mm2 > eval.mm2.
We can then run the eval file.
You can find more information on keeping files separate in the MM2 structuring code tutorial.
In this run-through, we will omit the arith statements to keep a better overview of the code.
By executing the first execution statement, exec (0 0), we add the initial path of length zero from H to H.
When running the initial code with the --steps 0 flag, we obtain:
; insert all arith statements
(maxlength 4)
(startpoint H)
(exec (1 0) (, (exec (1 $a) $b $c) (arith ($a + 1 = $d)) (path $a $e $f $g) (street $f $h $i) (arith ($g + $i = $j)) (maxlength $x10) (arith ($j <= $x10))) (, (path $d $e $h $j) (exec (1 $d) $b $c)))
(exec (2 0) (, (path $a H $b $c)) (, (reachable H $b)))
(street A B 1)
(street A D 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street C H 2)
(street D A 1)
(street D E 1)
(street D F 1)
(street E B 1)
(street E G 1)
(street F G 1)
(street F I 1)
(street G F 1)
(street H C 2)
(street H G 1)
(street I J 2)
(street J H 1)
(path 0 H H 0) ; <--- added by exec (0 0)
Next, exec (1 0) is executed.
This execution statement adds path statements with iteration index 1, and re-adds the execution statement to the space with an increased iteration index, as exec (1 1).
(Run the initial code with the --steps 1 flag.)
; insert all arith statements
(maxlength 4)
(startpoint H)
; Added by exec (1 0)
(exec (1 1) (, (exec (1 $a) $b $c) (arith ($a + 1 = $d)) (path $a $e $f $g) (street $f $h $i) (arith ($g + $i = $j)) (maxlength $x10) (arith ($j <= $x10))) (, (path $d $e $h $j) (exec (1 $d) $b $c)))
(exec (2 0) (, (path $a H $b $c)) (, (reachable H $b)))
(street A B 1)
(street A D 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street C H 2)
(street D A 1)
(street D E 1)
(street D F 1)
(street E B 1)
(street E G 1)
(street F G 1)
(street F I 1)
(street G F 1)
(street H C 2)
(street H G 1)
(street I J 2)
(street J H 1)
(path 0 H H 0)
(path 1 H C 2) ; <--- Added by exec (1 0)
(path 1 H G 1) ; <--- Added by exec (1 0)
Next, exec (1 1) is executed.
This execution statement adds path statements with iteration index 2, and re-adds the execution statement to the space with an increased iteration index, as exec (1 2).
(Run with the --steps 2 flag.)
; insert all arith statements
(maxlength 4)
(startpoint H)
; Added by previous iteration, exec (1 1)
(exec (1 2) (, (exec (1 $a) $b $c) (arith ($a + 1 = $d)) (path $a $e $f $g) (street $f $h $i) (arith ($g + $i = $j)) (maxlength $x10) (arith ($j <= $x10))) (, (path $d $e $h $j) (exec (1 $d) $b $c)))
(exec (2 0) (, (path $a H $b $c)) (, (reachable H $b)))
(street A B 1)
(street A D 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street C H 2)
(street D A 1)
(street D E 1)
(street D F 1)
(street E B 1)
(street E G 1)
(street F G 1)
(street F I 1)
(street G F 1)
(street H C 2)
(street H G 1)
(street I J 2)
(street J H 1)
(path 0 H H 0)
(path 1 H C 2)
(path 1 H G 1)
(path 2 H B 3) ; <--- Added by exec (1 1)
(path 2 H F 2) ; <--- Added by exec (1 1)
(path 2 H H 4) ; <--- Added by exec (1 1)
We continue executing the iterative rule. In each step, the current execution statement is applied, producing path statements with the next iteration index and re-adding itself to the space with an increased index.
(Run with the --steps 4 flag.)
; insert all arith statements
(maxlength 4)
(startpoint H)
; Added by exec (1 3)
(exec (1 4) (, (exec (1 $a) $b $c) (arith ($a + 1 = $d)) (path $a $e $f $g) (street $f $h $i) (arith ($g + $i = $j)) (maxlength $x10) (arith ($j <= $x10))) (, (path $d $e $h $j) (exec (1 $d) $b $c)))
(exec (2 0) (, (path $a H $b $c)) (, (reachable H $b)))
(street A B 1)
(street A D 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street C H 2)
(street D A 1)
(street D E 1)
(street D F 1)
(street E B 1)
(street E G 1)
(street F G 1)
(street F I 1)
(street G F 1)
(street H C 2)
(street H G 1)
(street I J 2)
(street J H 1)
(path 0 H H 0)
(path 1 H C 2)
(path 1 H G 1)
(path 2 H B 3)
(path 2 H F 2)
(path 2 H H 4)
(path 3 H A 4) ; <--- Added by exec (1 2)
(path 3 H C 4) ; <--- Added by exec (1 2)
(path 3 H G 3) ; <--- Added by exec (1 2)
(path 3 H I 3) ; <--- Added by exec (1 2)
(path 4 H F 4) ; <--- Added by exec (1 3)
Next, exec (1 4) is executed.
It is still able to match with itself, and it finds a path from the previous iteration, namely (path 4 H F 4).
However, it does not find any street that can be added to this path so that the total distance from H remains less than 4.
In particular, it does not find a matching arithmetic statement of the form (arith ($j <= $x10)).
As a result, not all patterns of the execution statement are matched, and its templates are not written to the space.
The execution statement itself is therefore not added back to the space. This marks the end of the iterative process.
Running the initial program with --steps 5 gives us:
; -- insert all arith statements --
(maxlength 4)
(startpoint H)
; ---> No new exec statement added
(exec (2 0) (, (path $a H $b $c)) (, (reachable H $b)))
(street A B 1)
(street A D 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street C H 2)
(street D A 1)
(street D E 1)
(street D F 1)
(street E B 1)
(street E G 1)
(street F G 1)
(street F I 1)
(street G F 1)
(street H C 2)
(street H G 1)
(street I J 2)
(street J H 1)
(path 0 H H 0)
(path 1 H C 2)
(path 1 H G 1)
(path 2 H B 3)
(path 2 H F 2)
(path 2 H H 4)
(path 3 H A 4)
(path 3 H C 4)
(path 3 H G 3)
(path 3 H I 3)
(path 4 H F 4)
Lastly, we collect all statements indicating which buildings are reachable from H within four steps.
For --steps 6, or when running the program to completion, we obtain:
; insert all arith statements
(maxlength 4)
(startpoint H)
(reachable H A) ; <--- Added by exec (2 0)
(reachable H B) ; <--- Added by exec (2 0)
(reachable H C) ; <--- Added by exec (2 0)
(reachable H F) ; <--- Added by exec (2 0)
(reachable H G) ; <--- Added by exec (2 0)
(reachable H H) ; <--- Added by exec (2 0)
(reachable H I) ; <--- Added by exec (2 0)
(street A B 1)
(street A D 1)
(street B A 1)
(street B C 1)
(street C B 1)
(street C H 2)
(street D A 1)
(street D E 1)
(street D F 1)
(street E B 1)
(street E G 1)
(street F G 1)
(street F I 1)
(street G F 1)
(street H C 2)
(street H G 1)
(street I J 2)
(street J H 1)
(path 0 H H 0)
(path 1 H C 2)
(path 1 H G 1)
(path 2 H B 3)
(path 2 H F 2)
(path 2 H H 4)
(path 3 H A 4)
(path 3 H C 4)
(path 3 H G 3)
(path 3 H I 3)
(path 4 H F 4)
Coming soon
Coming soon
(arith (0 + 0 = 0))
(arith (0 + 1 = 1))
(arith (0 + 2 = 2))
(arith (0 + 3 = 3))
(arith (0 + 4 = 4))
(arith (0 + 5 = 5))
(arith (0 + 6 = 6))
(arith (0 + 7 = 7))
(arith (0 + 8 = 8))
(arith (1 + 0 = 1))
(arith (1 + 1 = 2))
(arith (1 + 2 = 3))
(arith (1 + 3 = 4))
(arith (1 + 4 = 5))
(arith (1 + 5 = 6))
(arith (1 + 6 = 7))
(arith (1 + 7 = 8))
(arith (1 + 8 = 9))
(arith (2 + 0 = 2))
(arith (2 + 1 = 3))
(arith (2 + 2 = 4))
(arith (2 + 3 = 5))
(arith (2 + 4 = 6))
(arith (2 + 5 = 7))
(arith (2 + 6 = 8))
(arith (2 + 7 = 9))
(arith (2 + 8 = 10))
(arith (3 + 0 = 3))
(arith (3 + 1 = 4))
(arith (3 + 2 = 5))
(arith (3 + 3 = 6))
(arith (3 + 4 = 7))
(arith (3 + 5 = 8))
(arith (3 + 6 = 9))
(arith (3 + 7 = 10))
(arith (3 + 8 = 11))
(arith (4 + 0 = 4))
(arith (4 + 1 = 5))
(arith (4 + 2 = 6))
(arith (4 + 3 = 7))
(arith (4 + 4 = 8))
(arith (4 + 5 = 9))
(arith (4 + 6 = 10))
(arith (4 + 7 = 11))
(arith (4 + 8 = 12))
(arith (5 + 0 = 5))
(arith (5 + 1 = 6))
(arith (5 + 2 = 7))
(arith (5 + 3 = 8))
(arith (5 + 4 = 9))
(arith (5 + 5 = 10))
(arith (5 + 6 = 11))
(arith (5 + 7 = 12))
(arith (5 + 8 = 13))
(arith (6 + 0 = 6))
(arith (6 + 1 = 7))
(arith (6 + 2 = 8))
(arith (6 + 3 = 9))
(arith (6 + 4 = 10))
(arith (6 + 5 = 11))
(arith (6 + 6 = 12))
(arith (6 + 7 = 13))
(arith (6 + 8 = 14))
(arith (7 + 0 = 7))
(arith (7 + 1 = 8))
(arith (7 + 2 = 9))
(arith (7 + 3 = 10))
(arith (7 + 4 = 11))
(arith (7 + 5 = 12))
(arith (7 + 6 = 13))
(arith (7 + 7 = 14))
(arith (7 + 8 = 15))
(arith (8 + 0 = 8))
(arith (8 + 1 = 9))
(arith (8 + 2 = 10))
(arith (8 + 3 = 11))
(arith (8 + 4 = 12))
(arith (8 + 5 = 13))
(arith (8 + 6 = 14))
(arith (8 + 7 = 15))
(arith (8 + 8 = 16))
(arith (0 <= 0))
(arith (0 <= 1))
(arith (0 <= 2))
(arith (0 <= 3))
(arith (0 <= 4))
(arith (0 <= 5))
(arith (0 <= 6))
(arith (0 <= 7))
(arith (0 <= 8))
(arith (0 <= 9))
(arith (0 <= 10))
(arith (0 <= 11))
(arith (0 <= 12))
(arith (0 <= 13))
(arith (0 <= 14))
(arith (0 <= 15))
(arith (0 <= 16))
(arith (1 <= 1))
(arith (1 <= 2))
(arith (1 <= 3))
(arith (1 <= 4))
(arith (1 <= 5))
(arith (1 <= 6))
(arith (1 <= 7))
(arith (1 <= 8))
(arith (1 <= 9))
(arith (1 <= 10))
(arith (1 <= 11))
(arith (1 <= 12))
(arith (1 <= 13))
(arith (1 <= 14))
(arith (1 <= 15))
(arith (1 <= 16))
(arith (2 <= 2))
(arith (2 <= 3))
(arith (2 <= 4))
(arith (2 <= 5))
(arith (2 <= 6))
(arith (2 <= 7))
(arith (2 <= 8))
(arith (2 <= 9))
(arith (2 <= 10))
(arith (2 <= 11))
(arith (2 <= 12))
(arith (2 <= 13))
(arith (2 <= 14))
(arith (2 <= 15))
(arith (2 <= 16))
(arith (3 <= 3))
(arith (3 <= 4))
(arith (3 <= 5))
(arith (3 <= 6))
(arith (3 <= 7))
(arith (3 <= 8))
(arith (3 <= 9))
(arith (3 <= 10))
(arith (3 <= 11))
(arith (3 <= 12))
(arith (3 <= 13))
(arith (3 <= 14))
(arith (3 <= 15))
(arith (3 <= 16))
(arith (4 <= 4))
(arith (4 <= 5))
(arith (4 <= 6))
(arith (4 <= 7))
(arith (4 <= 8))
(arith (4 <= 9))
(arith (4 <= 10))
(arith (4 <= 11))
(arith (4 <= 12))
(arith (4 <= 13))
(arith (4 <= 14))
(arith (4 <= 15))
(arith (4 <= 16))
(arith (5 <= 5))
(arith (5 <= 6))
(arith (5 <= 7))
(arith (5 <= 8))
(arith (5 <= 9))
(arith (5 <= 10))
(arith (5 <= 11))
(arith (5 <= 12))
(arith (5 <= 13))
(arith (5 <= 14))
(arith (5 <= 15))
(arith (5 <= 16))
(arith (6 <= 6))
(arith (6 <= 7))
(arith (6 <= 8))
(arith (6 <= 9))
(arith (6 <= 10))
(arith (6 <= 11))
(arith (6 <= 12))
(arith (6 <= 13))
(arith (6 <= 14))
(arith (6 <= 15))
(arith (6 <= 16))
(arith (7 <= 7))
(arith (7 <= 8))
(arith (7 <= 9))
(arith (7 <= 10))
(arith (7 <= 11))
(arith (7 <= 12))
(arith (7 <= 13))
(arith (7 <= 14))
(arith (7 <= 15))
(arith (7 <= 16))
(arith (8 <= 8))
(arith (8 <= 9))
(arith (8 <= 10))
(arith (8 <= 11))
(arith (8 <= 12))
(arith (8 <= 13))
(arith (8 <= 14))
(arith (8 <= 15))
(arith (8 <= 16))
(arith (9 <= 9))
(arith (9 <= 10))
(arith (9 <= 11))
(arith (9 <= 12))
(arith (9 <= 13))
(arith (9 <= 14))
(arith (9 <= 15))
(arith (9 <= 16))
(arith (10 <= 10))
(arith (10 <= 11))
(arith (10 <= 12))
(arith (10 <= 13))
(arith (10 <= 14))
(arith (10 <= 15))
(arith (10 <= 16))
(arith (11 <= 11))
(arith (11 <= 12))
(arith (11 <= 13))
(arith (11 <= 14))
(arith (11 <= 15))
(arith (11 <= 16))
(arith (12 <= 12))
(arith (12 <= 13))
(arith (12 <= 14))
(arith (12 <= 15))
(arith (12 <= 16))
(arith (13 <= 13))
(arith (13 <= 14))
(arith (13 <= 15))
(arith (13 <= 16))
(arith (14 <= 14))
(arith (14 <= 15))
(arith (14 <= 16))
(arith (15 <= 15))
(arith (15 <= 16))
(arith (16 <= 16))