test/Golden/Grammar/ViewGrammar/G14.expected.txt

   1 <*>
   2 + <*>
   3 | + pure (\u1 -> (\u2 -> u1))
   4 | ` <*>
   5 |   + <*>
   6 |   | + <*>
   7 |   | | + pure (\u1 -> (\u2 -> u1))
   8 |   | | ` pure (\u1 -> u1)
   9 |   | ` def <hidden>
  10 |   |   ` <*>
  11 |   |     + <*>
  12 |   |     | + <*>
  13 |   |     | | + pure (\u1 -> (\u2 -> u1))
  14 |   |     | | ` pure (\u1 -> u1)
  15 |   |     | ` <*>
  16 |   |     |   + <*>
  17 |   |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
  18 |   |     |   | ` def <hidden>
  19 |   |     |   |   ` pure Term
  20 |   |     |   ` def <hidden>
  21 |   |     |     ` <|>
  22 |   |     |       + <*>
  23 |   |     |       | + <*>
  24 |   |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
  25 |   |     |       | | ` <*>
  26 |   |     |       | |   + <*>
  27 |   |     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
  28 |   |     |       | |   | ` pure (\u1 -> (\u2 -> u1))
  29 |   |     |       | |   ` <|>
  30 |   |     |       | |     + <*>
  31 |   |     |       | |     | + <*>
  32 |   |     |       | |     | | + <*>
  33 |   |     |       | |     | | | + pure (\u1 -> (\u2 -> u1))
  34 |   |     |       | |     | | | ` pure (\u1 -> u1)
  35 |   |     |       | |     | | ` def <hidden>
  36 |   |     |       | |     | |   ` <*>
  37 |   |     |       | |     | |     + <*>
  38 |   |     |       | |     | |     | + <*>
  39 |   |     |       | |     | |     | | + pure (\u1 -> (\u2 -> u1))
  40 |   |     |       | |     | |     | | ` pure (\u1 -> u1)
  41 |   |     |       | |     | |     | ` satisfy
  42 |   |     |       | |     | |     ` ref <hidden>
  43 |   |     |       | |     | ` <*>
  44 |   |     |       | |     |   + <*>
  45 |   |     |       | |     |   | + <*>
  46 |   |     |       | |     |   | | + pure (\u1 -> (\u2 -> u1))
  47 |   |     |       | |     |   | | ` pure (\u1 -> u1)
  48 |   |     |       | |     |   | ` <*>
  49 |   |     |       | |     |   |   + <*>
  50 |   |     |       | |     |   |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
  51 |   |     |       | |     |   |   | ` pure Term
  52 |   |     |       | |     |   |   ` def <hidden>
  53 |   |     |       | |     |   |     ` <|>
  54 |   |     |       | |     |   |       + <*>
  55 |   |     |       | |     |   |       | + <*>
  56 |   |     |       | |     |   |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
  57 |   |     |       | |     |   |       | | ` <*>
  58 |   |     |       | |     |   |       | |   + <*>
  59 |   |     |       | |     |   |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
  60 |   |     |       | |     |   |       | |   | ` pure (\u1 -> (\u2 -> u1))
  61 |   |     |       | |     |   |       | |   ` ref <hidden>
  62 |   |     |       | |     |   |       | ` rec <hidden>
  63 |   |     |       | |     |   |       ` pure (\u1 -> u1)
  64 |   |     |       | |     |   ` pure Term
  65 |   |     |       | |     ` <*>
  66 |   |     |       | |       + <*>
  67 |   |     |       | |       | + <*>
  68 |   |     |       | |       | | + pure (\u1 -> (\u2 -> u1))
  69 |   |     |       | |       | | ` pure (\u1 -> u1)
  70 |   |     |       | |       | ` <*>
  71 |   |     |       | |       |   + <*>
  72 |   |     |       | |       |   | + <*>
  73 |   |     |       | |       |   | | + pure (\u1 -> (\u2 -> u1))
  74 |   |     |       | |       |   | | ` pure (\u1 -> u1)
  75 |   |     |       | |       |   | ` try
  76 |   |     |       | |       |   |   ` <*>
  77 |   |     |       | |       |   |     + <*>
  78 |   |     |       | |       |   |     | + pure cons
  79 |   |     |       | |       |   |     | ` <*>
  80 |   |     |       | |       |   |     |   + <*>
  81 |   |     |       | |       |   |     |   | + pure (\u1 -> (\u2 -> u1))
  82 |   |     |       | |       |   |     |   | ` pure '/'
  83 |   |     |       | |       |   |     |   ` satisfy
  84 |   |     |       | |       |   |     ` <*>
  85 |   |     |       | |       |   |       + <*>
  86 |   |     |       | |       |   |       | + pure cons
  87 |   |     |       | |       |   |       | ` <*>
  88 |   |     |       | |       |   |       |   + <*>
  89 |   |     |       | |       |   |       |   | + pure (\u1 -> (\u2 -> u1))
  90 |   |     |       | |       |   |       |   | ` pure '/'
  91 |   |     |       | |       |   |       |   ` satisfy
  92 |   |     |       | |       |   |       ` pure Term
  93 |   |     |       | |       |   ` <*>
  94 |   |     |       | |       |     + <*>
  95 |   |     |       | |       |     | + <*>
  96 |   |     |       | |       |     | | + pure (\u1 -> (\u2 -> u1))
  97 |   |     |       | |       |     | | ` pure (\u1 -> u1)
  98 |   |     |       | |       |     | ` <*>
  99 |   |     |       | |       |     |   + <*>
 100 |   |     |       | |       |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 101 |   |     |       | |       |     |   | ` ref <hidden>
 102 |   |     |       | |       |     |   ` def <hidden>
 103 |   |     |       | |       |     |     ` <|>
 104 |   |     |       | |       |     |       + <*>
 105 |   |     |       | |       |     |       | + <*>
 106 |   |     |       | |       |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 107 |   |     |       | |       |     |       | | ` <*>
 108 |   |     |       | |       |     |       | |   + <*>
 109 |   |     |       | |       |     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
 110 |   |     |       | |       |     |       | |   | ` pure (\u1 -> (\u2 -> u1))
 111 |   |     |       | |       |     |       | |   ` satisfy
 112 |   |     |       | |       |     |       | ` rec <hidden>
 113 |   |     |       | |       |     |       ` pure (\u1 -> u1)
 114 |   |     |       | |       |     ` ref <hidden>
 115 |   |     |       | |       ` ref <hidden>
 116 |   |     |       | ` rec <hidden>
 117 |   |     |       ` pure (\u1 -> u1)
 118 |   |     ` ref <hidden>
 119 |   ` <*>
 120 |     + <*>
 121 |     | + <*>
 122 |     | | + pure (\u1 -> (\u2 -> u1))
 123 |     | | ` pure (\u1 -> u1)
 124 |     | ` <*>
 125 |     |   + <*>
 126 |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 127 |     |   | ` ref <hidden>
 128 |     |   ` def <hidden>
 129 |     |     ` <|>
 130 |     |       + <*>
 131 |     |       | + <*>
 132 |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 133 |     |       | | ` <*>
 134 |     |       | |   + <*>
 135 |     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
 136 |     |       | |   | ` pure (\u1 -> (\u2 -> u1))
 137 |     |       | |   ` <*>
 138 |     |       | |     + <*>
 139 |     |       | |     | + <*>
 140 |     |       | |     | | + pure (\u1 -> (\u2 -> u1))
 141 |     |       | |     | | ` pure (\u1 -> u1)
 142 |     |       | |     | ` <*>
 143 |     |       | |     |   + <*>
 144 |     |       | |     |   | + <*>
 145 |     |       | |     |   | | + pure (\u1 -> (\u2 -> u1))
 146 |     |       | |     |   | | ` pure (\u1 -> u1)
 147 |     |       | |     |   | ` <*>
 148 |     |       | |     |   |   + <*>
 149 |     |       | |     |   |   | + <*>
 150 |     |       | |     |   |   | | + pure (\u1 -> (\u2 -> u1))
 151 |     |       | |     |   |   | | ` pure (\u1 -> u1)
 152 |     |       | |     |   |   | ` <*>
 153 |     |       | |     |   |   |   + <*>
 154 |     |       | |     |   |   |   | + <*>
 155 |     |       | |     |   |   |   | | + pure (\u1 -> (\u2 -> u1))
 156 |     |       | |     |   |   |   | | ` pure (\u1 -> u1)
 157 |     |       | |     |   |   |   | ` try
 158 |     |       | |     |   |   |   |   ` <*>
 159 |     |       | |     |   |   |   |     + <*>
 160 |     |       | |     |   |   |   |     | + <*>
 161 |     |       | |     |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
 162 |     |       | |     |   |   |   |     | | ` pure (\u1 -> u1)
 163 |     |       | |     |   |   |   |     | ` try
 164 |     |       | |     |   |   |   |     |   ` <*>
 165 |     |       | |     |   |   |   |     |     + <*>
 166 |     |       | |     |   |   |   |     |     | + pure cons
 167 |     |       | |     |   |   |   |     |     | ` <*>
 168 |     |       | |     |   |   |   |     |     |   + <*>
 169 |     |       | |     |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
 170 |     |       | |     |   |   |   |     |     |   | ` pure 'f'
 171 |     |       | |     |   |   |   |     |     |   ` satisfy
 172 |     |       | |     |   |   |   |     |     ` <*>
 173 |     |       | |     |   |   |   |     |       + <*>
 174 |     |       | |     |   |   |   |     |       | + pure cons
 175 |     |       | |     |   |   |   |     |       | ` <*>
 176 |     |       | |     |   |   |   |     |       |   + <*>
 177 |     |       | |     |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
 178 |     |       | |     |   |   |   |     |       |   | ` pure 'u'
 179 |     |       | |     |   |   |   |     |       |   ` satisfy
 180 |     |       | |     |   |   |   |     |       ` <*>
 181 |     |       | |     |   |   |   |     |         + <*>
 182 |     |       | |     |   |   |   |     |         | + pure cons
 183 |     |       | |     |   |   |   |     |         | ` <*>
 184 |     |       | |     |   |   |   |     |         |   + <*>
 185 |     |       | |     |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
 186 |     |       | |     |   |   |   |     |         |   | ` pure 'n'
 187 |     |       | |     |   |   |   |     |         |   ` satisfy
 188 |     |       | |     |   |   |   |     |         ` <*>
 189 |     |       | |     |   |   |   |     |           + <*>
 190 |     |       | |     |   |   |   |     |           | + pure cons
 191 |     |       | |     |   |   |   |     |           | ` <*>
 192 |     |       | |     |   |   |   |     |           |   + <*>
 193 |     |       | |     |   |   |   |     |           |   | + pure (\u1 -> (\u2 -> u1))
 194 |     |       | |     |   |   |   |     |           |   | ` pure 'c'
 195 |     |       | |     |   |   |   |     |           |   ` satisfy
 196 |     |       | |     |   |   |   |     |           ` <*>
 197 |     |       | |     |   |   |   |     |             + <*>
 198 |     |       | |     |   |   |   |     |             | + pure cons
 199 |     |       | |     |   |   |   |     |             | ` <*>
 200 |     |       | |     |   |   |   |     |             |   + <*>
 201 |     |       | |     |   |   |   |     |             |   | + pure (\u1 -> (\u2 -> u1))
 202 |     |       | |     |   |   |   |     |             |   | ` pure 't'
 203 |     |       | |     |   |   |   |     |             |   ` satisfy
 204 |     |       | |     |   |   |   |     |             ` <*>
 205 |     |       | |     |   |   |   |     |               + <*>
 206 |     |       | |     |   |   |   |     |               | + pure cons
 207 |     |       | |     |   |   |   |     |               | ` <*>
 208 |     |       | |     |   |   |   |     |               |   + <*>
 209 |     |       | |     |   |   |   |     |               |   | + pure (\u1 -> (\u2 -> u1))
 210 |     |       | |     |   |   |   |     |               |   | ` pure 'i'
 211 |     |       | |     |   |   |   |     |               |   ` satisfy
 212 |     |       | |     |   |   |   |     |               ` <*>
 213 |     |       | |     |   |   |   |     |                 + <*>
 214 |     |       | |     |   |   |   |     |                 | + pure cons
 215 |     |       | |     |   |   |   |     |                 | ` <*>
 216 |     |       | |     |   |   |   |     |                 |   + <*>
 217 |     |       | |     |   |   |   |     |                 |   | + pure (\u1 -> (\u2 -> u1))
 218 |     |       | |     |   |   |   |     |                 |   | ` pure 'o'
 219 |     |       | |     |   |   |   |     |                 |   ` satisfy
 220 |     |       | |     |   |   |   |     |                 ` <*>
 221 |     |       | |     |   |   |   |     |                   + <*>
 222 |     |       | |     |   |   |   |     |                   | + pure cons
 223 |     |       | |     |   |   |   |     |                   | ` <*>
 224 |     |       | |     |   |   |   |     |                   |   + <*>
 225 |     |       | |     |   |   |   |     |                   |   | + pure (\u1 -> (\u2 -> u1))
 226 |     |       | |     |   |   |   |     |                   |   | ` pure 'n'
 227 |     |       | |     |   |   |   |     |                   |   ` satisfy
 228 |     |       | |     |   |   |   |     |                   ` def <hidden>
 229 |     |       | |     |   |   |   |     |                     ` pure Term
 230 |     |       | |     |   |   |   |     ` def <hidden>
 231 |     |       | |     |   |   |   |       ` negLook
 232 |     |       | |     |   |   |   |         ` satisfy
 233 |     |       | |     |   |   |   ` ref <hidden>
 234 |     |       | |     |   |   ` def <hidden>
 235 |     |       | |     |   |     ` <*>
 236 |     |       | |     |   |       + <*>
 237 |     |       | |     |   |       | + <*>
 238 |     |       | |     |   |       | | + pure (\u1 -> (\u2 -> u1))
 239 |     |       | |     |   |       | | ` pure (\u1 -> u1)
 240 |     |       | |     |   |       | ` try
 241 |     |       | |     |   |       |   ` <*>
 242 |     |       | |     |   |       |     + <*>
 243 |     |       | |     |   |       |     | + <*>
 244 |     |       | |     |   |       |     | | + pure (\u1 -> (\u2 -> u1))
 245 |     |       | |     |   |       |     | | ` pure (\u1 -> u1)
 246 |     |       | |     |   |       |     | ` satisfy
 247 |     |       | |     |   |       |     ` <*>
 248 |     |       | |     |   |       |       + <*>
 249 |     |       | |     |   |       |       | + <*>
 250 |     |       | |     |   |       |       | | + pure (\u1 -> (\u2 -> u1))
 251 |     |       | |     |   |       |       | | ` pure (\u1 -> u1)
 252 |     |       | |     |   |       |       | ` <*>
 253 |     |       | |     |   |       |       |   + <*>
 254 |     |       | |     |   |       |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 255 |     |       | |     |   |       |       |   | ` ref <hidden>
 256 |     |       | |     |   |       |       |   ` def <hidden>
 257 |     |       | |     |   |       |       |     ` <|>
 258 |     |       | |     |   |       |       |       + <*>
 259 |     |       | |     |   |       |       |       | + <*>
 260 |     |       | |     |   |       |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 261 |     |       | |     |   |       |       |       | | ` <*>
 262 |     |       | |     |   |       |       |       | |   + <*>
 263 |     |       | |     |   |       |       |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
 264 |     |       | |     |   |       |       |       | |   | ` pure (\u1 -> (\u2 -> u1))
 265 |     |       | |     |   |       |       |       | |   ` satisfy
 266 |     |       | |     |   |       |       |       | ` rec <hidden>
 267 |     |       | |     |   |       |       |       ` pure (\u1 -> u1)
 268 |     |       | |     |   |       |       ` ref <hidden>
 269 |     |       | |     |   |       ` ref <hidden>
 270 |     |       | |     |   ` <*>
 271 |     |       | |     |     + <*>
 272 |     |       | |     |     | + pure (\u1 -> (\u2 -> u1))
 273 |     |       | |     |     | ` <*>
 274 |     |       | |     |     |   + <*>
 275 |     |       | |     |     |   | + <*>
 276 |     |       | |     |     |   | | + pure (\u1 -> (\u2 -> u1))
 277 |     |       | |     |     |   | | ` pure (\u1 -> u1)
 278 |     |       | |     |     |   | ` def <hidden>
 279 |     |       | |     |     |   |   ` <*>
 280 |     |       | |     |     |   |     + <*>
 281 |     |       | |     |     |   |     | + pure (\u1 -> (\u2 -> u1))
 282 |     |       | |     |     |   |     | ` <*>
 283 |     |       | |     |     |   |     |   + <*>
 284 |     |       | |     |     |   |     |   | + pure (\u1 -> (\u2 -> u1))
 285 |     |       | |     |     |   |     |   | ` pure '('
 286 |     |       | |     |     |   |     |   ` satisfy
 287 |     |       | |     |     |   |     ` ref <hidden>
 288 |     |       | |     |     |   ` <*>
 289 |     |       | |     |     |     + <*>
 290 |     |       | |     |     |     | + <*>
 291 |     |       | |     |     |     | | + pure (\u1 -> (\u2 -> u1))
 292 |     |       | |     |     |     | | ` pure (\u1 -> u1)
 293 |     |       | |     |     |     | ` def <hidden>
 294 |     |       | |     |     |     |   ` <|>
 295 |     |       | |     |     |     |     + <*>
 296 |     |       | |     |     |     |     | + <*>
 297 |     |       | |     |     |     |     | | + pure (\u1 -> (\u2 -> u1))
 298 |     |       | |     |     |     |     | | ` pure Term
 299 |     |       | |     |     |     |     | ` <*>
 300 |     |       | |     |     |     |     |   + <*>
 301 |     |       | |     |     |     |     |   | + <*>
 302 |     |       | |     |     |     |     |   | | + pure (\u1 -> (\u2 -> u1))
 303 |     |       | |     |     |     |     |   | | ` pure (\u1 -> u1)
 304 |     |       | |     |     |     |     |   | ` def <hidden>
 305 |     |       | |     |     |     |     |   |   ` <*>
 306 |     |       | |     |     |     |     |   |     + <*>
 307 |     |       | |     |     |     |     |   |     | + <*>
 308 |     |       | |     |     |     |     |   |     | | + pure (\u1 -> (\u2 -> u1))
 309 |     |       | |     |     |     |     |   |     | | ` pure (\u1 -> u1)
 310 |     |       | |     |     |     |     |   |     | ` ref <hidden>
 311 |     |       | |     |     |     |     |   |     ` <|>
 312 |     |       | |     |     |     |     |   |       + <*>
 313 |     |       | |     |     |     |     |   |       | + <*>
 314 |     |       | |     |     |     |     |   |       | | + pure (\u1 -> (\u2 -> u1))
 315 |     |       | |     |     |     |     |   |       | | ` pure Term
 316 |     |       | |     |     |     |     |   |       | ` def <hidden>
 317 |     |       | |     |     |     |     |   |       |   ` <*>
 318 |     |       | |     |     |     |     |   |       |     + <*>
 319 |     |       | |     |     |     |     |   |       |     | + pure (\u1 -> (\u2 -> u1))
 320 |     |       | |     |     |     |     |   |       |     | ` <*>
 321 |     |       | |     |     |     |     |   |       |     |   + <*>
 322 |     |       | |     |     |     |     |   |       |     |   | + <*>
 323 |     |       | |     |     |     |     |   |       |     |   | | + pure (\u1 -> (\u2 -> u1))
 324 |     |       | |     |     |     |     |   |       |     |   | | ` pure (\u1 -> u1)
 325 |     |       | |     |     |     |     |   |       |     |   | ` <*>
 326 |     |       | |     |     |     |     |   |       |     |   |   + <*>
 327 |     |       | |     |     |     |     |   |       |     |   |   | + pure (\u1 -> (\u2 -> u1))
 328 |     |       | |     |     |     |     |   |       |     |   |   | ` <*>
 329 |     |       | |     |     |     |     |   |       |     |   |   |   + <*>
 330 |     |       | |     |     |     |     |   |       |     |   |   |   | + pure (\u1 -> (\u2 -> u1))
 331 |     |       | |     |     |     |     |   |       |     |   |   |   | ` pure '['
 332 |     |       | |     |     |     |     |   |       |     |   |   |   ` satisfy
 333 |     |       | |     |     |     |     |   |       |     |   |   ` ref <hidden>
 334 |     |       | |     |     |     |     |   |       |     |   ` <*>
 335 |     |       | |     |     |     |     |   |       |     |     + <*>
 336 |     |       | |     |     |     |     |   |       |     |     | + <*>
 337 |     |       | |     |     |     |     |   |       |     |     | | + pure (\u1 -> (\u2 -> u1))
 338 |     |       | |     |     |     |     |   |       |     |     | | ` pure (\u1 -> u1)
 339 |     |       | |     |     |     |     |   |       |     |     | ` def <hidden>
 340 |     |       | |     |     |     |     |   |       |     |     |   ` satisfy
 341 |     |       | |     |     |     |     |   |       |     |     ` <*>
 342 |     |       | |     |     |     |     |   |       |     |       + <*>
 343 |     |       | |     |     |     |     |   |       |     |       | + <*>
 344 |     |       | |     |     |     |     |   |       |     |       | | + pure (\u1 -> (\u2 -> u1))
 345 |     |       | |     |     |     |     |   |       |     |       | | ` pure (\u1 -> u1)
 346 |     |       | |     |     |     |     |   |       |     |       | ` <*>
 347 |     |       | |     |     |     |     |   |       |     |       |   + <*>
 348 |     |       | |     |     |     |     |   |       |     |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 349 |     |       | |     |     |     |     |   |       |     |       |   | ` pure Term
 350 |     |       | |     |     |     |     |   |       |     |       |   ` def <hidden>
 351 |     |       | |     |     |     |     |   |       |     |       |     ` <|>
 352 |     |       | |     |     |     |     |   |       |     |       |       + <*>
 353 |     |       | |     |     |     |     |   |       |     |       |       | + <*>
 354 |     |       | |     |     |     |     |   |       |     |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 355 |     |       | |     |     |     |     |   |       |     |       |       | | ` <*>
 356 |     |       | |     |     |     |     |   |       |     |       |       | |   + <*>
 357 |     |       | |     |     |     |     |   |       |     |       |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
 358 |     |       | |     |     |     |     |   |       |     |       |       | |   | ` pure (\u1 -> (\u2 -> u1))
 359 |     |       | |     |     |     |     |   |       |     |       |       | |   ` ref <hidden>
 360 |     |       | |     |     |     |     |   |       |     |       |       | ` rec <hidden>
 361 |     |       | |     |     |     |     |   |       |     |       |       ` pure (\u1 -> u1)
 362 |     |       | |     |     |     |     |   |       |     |       ` pure Term
 363 |     |       | |     |     |     |     |   |       |     ` <*>
 364 |     |       | |     |     |     |     |   |       |       + <*>
 365 |     |       | |     |     |     |     |   |       |       | + pure (\u1 -> (\u2 -> u1))
 366 |     |       | |     |     |     |     |   |       |       | ` <*>
 367 |     |       | |     |     |     |     |   |       |       |   + <*>
 368 |     |       | |     |     |     |     |   |       |       |   | + pure (\u1 -> (\u2 -> u1))
 369 |     |       | |     |     |     |     |   |       |       |   | ` pure ']'
 370 |     |       | |     |     |     |     |   |       |       |   ` satisfy
 371 |     |       | |     |     |     |     |   |       |       ` ref <hidden>
 372 |     |       | |     |     |     |     |   |       ` ref <hidden>
 373 |     |       | |     |     |     |     |   ` <*>
 374 |     |       | |     |     |     |     |     + <*>
 375 |     |       | |     |     |     |     |     | + <*>
 376 |     |       | |     |     |     |     |     | | + pure (\u1 -> (\u2 -> u1))
 377 |     |       | |     |     |     |     |     | | ` pure (\u1 -> u1)
 378 |     |       | |     |     |     |     |     | ` <*>
 379 |     |       | |     |     |     |     |     |   + <*>
 380 |     |       | |     |     |     |     |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 381 |     |       | |     |     |     |     |     |   | ` ref <hidden>
 382 |     |       | |     |     |     |     |     |   ` def <hidden>
 383 |     |       | |     |     |     |     |     |     ` <|>
 384 |     |       | |     |     |     |     |     |       + <*>
 385 |     |       | |     |     |     |     |     |       | + <*>
 386 |     |       | |     |     |     |     |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 387 |     |       | |     |     |     |     |     |       | | ` <*>
 388 |     |       | |     |     |     |     |     |       | |   + def <hidden>
 389 |     |       | |     |     |     |     |     |       | |   | ` <*>
 390 |     |       | |     |     |     |     |     |       | |   |   + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
 391 |     |       | |     |     |     |     |     |       | |   |   ` pure (\u1 -> (\u2 -> u1))
 392 |     |       | |     |     |     |     |     |       | |   ` <*>
 393 |     |       | |     |     |     |     |     |       | |     + <*>
 394 |     |       | |     |     |     |     |     |       | |     | + <*>
 395 |     |       | |     |     |     |     |     |       | |     | | + pure (\u1 -> (\u2 -> u1))
 396 |     |       | |     |     |     |     |     |       | |     | | ` pure (\u1 -> u1)
 397 |     |       | |     |     |     |     |     |       | |     | ` def <hidden>
 398 |     |       | |     |     |     |     |     |       | |     |   ` <*>
 399 |     |       | |     |     |     |     |     |       | |     |     + <*>
 400 |     |       | |     |     |     |     |     |       | |     |     | + pure (\u1 -> (\u2 -> u1))
 401 |     |       | |     |     |     |     |     |       | |     |     | ` <*>
 402 |     |       | |     |     |     |     |     |       | |     |     |   + <*>
 403 |     |       | |     |     |     |     |     |       | |     |     |   | + pure (\u1 -> (\u2 -> u1))
 404 |     |       | |     |     |     |     |     |       | |     |     |   | ` pure ','
 405 |     |       | |     |     |     |     |     |       | |     |     |   ` satisfy
 406 |     |       | |     |     |     |     |     |       | |     |     ` ref <hidden>
 407 |     |       | |     |     |     |     |     |       | |     ` ref <hidden>
 408 |     |       | |     |     |     |     |     |       | ` rec <hidden>
 409 |     |       | |     |     |     |     |     |       ` pure (\u1 -> u1)
 410 |     |       | |     |     |     |     |     ` ref <hidden>
 411 |     |       | |     |     |     |     ` ref <hidden>
 412 |     |       | |     |     |     ` <|>
 413 |     |       | |     |     |       + <*>
 414 |     |       | |     |     |       | + <*>
 415 |     |       | |     |     |       | | + pure (\u1 -> (\u2 -> u1))
 416 |     |       | |     |     |       | | ` pure Term
 417 |     |       | |     |     |       | ` <*>
 418 |     |       | |     |     |       |   + <*>
 419 |     |       | |     |     |       |   | + <*>
 420 |     |       | |     |     |       |   | | + pure (\u1 -> (\u2 -> u1))
 421 |     |       | |     |     |       |   | | ` pure (\u1 -> u1)
 422 |     |       | |     |     |       |   | ` <*>
 423 |     |       | |     |     |       |   |   + <*>
 424 |     |       | |     |     |       |   |   | + pure (\u1 -> (\u2 -> u1))
 425 |     |       | |     |     |       |   |   | ` <*>
 426 |     |       | |     |     |       |   |   |   + <*>
 427 |     |       | |     |     |       |   |   |   | + pure (\u1 -> (\u2 -> u1))
 428 |     |       | |     |     |       |   |   |   | ` pure ':'
 429 |     |       | |     |     |       |   |   |   ` satisfy
 430 |     |       | |     |     |       |   |   ` ref <hidden>
 431 |     |       | |     |     |       |   ` ref <hidden>
 432 |     |       | |     |     |       ` ref <hidden>
 433 |     |       | |     |     ` def <hidden>
 434 |     |       | |     |       ` <*>
 435 |     |       | |     |         + <*>
 436 |     |       | |     |         | + pure (\u1 -> (\u2 -> u1))
 437 |     |       | |     |         | ` <*>
 438 |     |       | |     |         |   + <*>
 439 |     |       | |     |         |   | + pure (\u1 -> (\u2 -> u1))
 440 |     |       | |     |         |   | ` pure ')'
 441 |     |       | |     |         |   ` satisfy
 442 |     |       | |     |         ` ref <hidden>
 443 |     |       | |     ` def <hidden>
 444 |     |       | |       ` <*>
 445 |     |       | |         + <*>
 446 |     |       | |         | + pure (\u1 -> (\u2 -> u1))
 447 |     |       | |         | ` <*>
 448 |     |       | |         |   + <*>
 449 |     |       | |         |   | + <*>
 450 |     |       | |         |   | | + pure (\u1 -> (\u2 -> u1))
 451 |     |       | |         |   | | ` pure (\u1 -> u1)
 452 |     |       | |         |   | ` <*>
 453 |     |       | |         |   |   + <*>
 454 |     |       | |         |   |   | + pure (\u1 -> (\u2 -> u1))
 455 |     |       | |         |   |   | ` <*>
 456 |     |       | |         |   |   |   + <*>
 457 |     |       | |         |   |   |   | + pure (\u1 -> (\u2 -> u1))
 458 |     |       | |         |   |   |   | ` pure '{'
 459 |     |       | |         |   |   |   ` satisfy
 460 |     |       | |         |   |   ` ref <hidden>
 461 |     |       | |         |   ` <*>
 462 |     |       | |         |     + <*>
 463 |     |       | |         |     | + <*>
 464 |     |       | |         |     | | + pure (\u1 -> (\u2 -> u1))
 465 |     |       | |         |     | | ` pure (\u1 -> u1)
 466 |     |       | |         |     | ` <*>
 467 |     |       | |         |     |   + <*>
 468 |     |       | |         |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 469 |     |       | |         |     |   | ` ref <hidden>
 470 |     |       | |         |     |   ` def <hidden>
 471 |     |       | |         |     |     ` <|>
 472 |     |       | |         |     |       + <*>
 473 |     |       | |         |     |       | + <*>
 474 |     |       | |         |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 475 |     |       | |         |     |       | | ` <*>
 476 |     |       | |         |     |       | |   + <*>
 477 |     |       | |         |     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
 478 |     |       | |         |     |       | |   | ` pure (\u1 -> (\u2 -> u1))
 479 |     |       | |         |     |       | |   ` <|>
 480 |     |       | |         |     |       | |     + <|>
 481 |     |       | |         |     |       | |     | + <|>
 482 |     |       | |         |     |       | |     | | + <*>
 483 |     |       | |         |     |       | |     | | | + <*>
 484 |     |       | |         |     |       | |     | | | | + <*>
 485 |     |       | |         |     |       | |     | | | | | + pure (\u1 -> (\u2 -> u1))
 486 |     |       | |         |     |       | |     | | | | | ` pure (\u1 -> u1)
 487 |     |       | |         |     |       | |     | | | | ` <*>
 488 |     |       | |         |     |       | |     | | | |   + <*>
 489 |     |       | |         |     |       | |     | | | |   | + <*>
 490 |     |       | |         |     |       | |     | | | |   | | + pure (\u1 -> (\u2 -> u1))
 491 |     |       | |         |     |       | |     | | | |   | | ` pure (\u1 -> u1)
 492 |     |       | |         |     |       | |     | | | |   | ` <*>
 493 |     |       | |         |     |       | |     | | | |   |   + <*>
 494 |     |       | |         |     |       | |     | | | |   |   | + <*>
 495 |     |       | |         |     |       | |     | | | |   |   | | + pure (\u1 -> (\u2 -> u1))
 496 |     |       | |         |     |       | |     | | | |   |   | | ` pure (\u1 -> u1)
 497 |     |       | |         |     |       | |     | | | |   |   | ` <*>
 498 |     |       | |         |     |       | |     | | | |   |   |   + <*>
 499 |     |       | |         |     |       | |     | | | |   |   |   | + <*>
 500 |     |       | |         |     |       | |     | | | |   |   |   | | + pure (\u1 -> (\u2 -> u1))
 501 |     |       | |         |     |       | |     | | | |   |   |   | | ` pure (\u1 -> u1)
 502 |     |       | |         |     |       | |     | | | |   |   |   | ` try
 503 |     |       | |         |     |       | |     | | | |   |   |   |   ` <*>
 504 |     |       | |         |     |       | |     | | | |   |   |   |     + <*>
 505 |     |       | |         |     |       | |     | | | |   |   |   |     | + <*>
 506 |     |       | |         |     |       | |     | | | |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
 507 |     |       | |         |     |       | |     | | | |   |   |   |     | | ` pure (\u1 -> u1)
 508 |     |       | |         |     |       | |     | | | |   |   |   |     | ` try
 509 |     |       | |         |     |       | |     | | | |   |   |   |     |   ` <*>
 510 |     |       | |         |     |       | |     | | | |   |   |   |     |     + <*>
 511 |     |       | |         |     |       | |     | | | |   |   |   |     |     | + pure cons
 512 |     |       | |         |     |       | |     | | | |   |   |   |     |     | ` <*>
 513 |     |       | |         |     |       | |     | | | |   |   |   |     |     |   + <*>
 514 |     |       | |         |     |       | |     | | | |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
 515 |     |       | |         |     |       | |     | | | |   |   |   |     |     |   | ` pure 'i'
 516 |     |       | |         |     |       | |     | | | |   |   |   |     |     |   ` satisfy
 517 |     |       | |         |     |       | |     | | | |   |   |   |     |     ` <*>
 518 |     |       | |         |     |       | |     | | | |   |   |   |     |       + <*>
 519 |     |       | |         |     |       | |     | | | |   |   |   |     |       | + pure cons
 520 |     |       | |         |     |       | |     | | | |   |   |   |     |       | ` <*>
 521 |     |       | |         |     |       | |     | | | |   |   |   |     |       |   + <*>
 522 |     |       | |         |     |       | |     | | | |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
 523 |     |       | |         |     |       | |     | | | |   |   |   |     |       |   | ` pure 'f'
 524 |     |       | |         |     |       | |     | | | |   |   |   |     |       |   ` satisfy
 525 |     |       | |         |     |       | |     | | | |   |   |   |     |       ` ref <hidden>
 526 |     |       | |         |     |       | |     | | | |   |   |   |     ` ref <hidden>
 527 |     |       | |         |     |       | |     | | | |   |   |   ` ref <hidden>
 528 |     |       | |         |     |       | |     | | | |   |   ` def <hidden>
 529 |     |       | |         |     |       | |     | | | |   |     ` <*>
 530 |     |       | |         |     |       | |     | | | |   |       + <*>
 531 |     |       | |         |     |       | |     | | | |   |       | + <*>
 532 |     |       | |         |     |       | |     | | | |   |       | | + pure (\u1 -> (\u2 -> u1))
 533 |     |       | |         |     |       | |     | | | |   |       | | ` pure (\u1 -> u1)
 534 |     |       | |         |     |       | |     | | | |   |       | ` def <hidden>
 535 |     |       | |         |     |       | |     | | | |   |       |   ` <|>
 536 |     |       | |         |     |       | |     | | | |   |       |     + <|>
 537 |     |       | |         |     |       | |     | | | |   |       |     | + <*>
 538 |     |       | |         |     |       | |     | | | |   |       |     | | + <*>
 539 |     |       | |         |     |       | |     | | | |   |       |     | | | + <*>
 540 |     |       | |         |     |       | |     | | | |   |       |     | | | | + pure (\u1 -> (\u2 -> u1))
 541 |     |       | |         |     |       | |     | | | |   |       |     | | | | ` pure (\u1 -> u1)
 542 |     |       | |         |     |       | |     | | | |   |       |     | | | ` <|>
 543 |     |       | |         |     |       | |     | | | |   |       |     | | |   + <*>
 544 |     |       | |         |     |       | |     | | | |   |       |     | | |   | + <*>
 545 |     |       | |         |     |       | |     | | | |   |       |     | | |   | | + pure (\u1 -> (\u2 -> u1))
 546 |     |       | |         |     |       | |     | | | |   |       |     | | |   | | ` pure '0'
 547 |     |       | |         |     |       | |     | | | |   |       |     | | |   | ` satisfy
 548 |     |       | |         |     |       | |     | | | |   |       |     | | |   ` <*>
 549 |     |       | |         |     |       | |     | | | |   |       |     | | |     + <*>
 550 |     |       | |         |     |       | |     | | | |   |       |     | | |     | + pure (\u1 -> (\u2 -> u1))
 551 |     |       | |         |     |       | |     | | | |   |       |     | | |     | ` pure '1'
 552 |     |       | |         |     |       | |     | | | |   |       |     | | |     ` satisfy
 553 |     |       | |         |     |       | |     | | | |   |       |     | | ` ref <hidden>
 554 |     |       | |         |     |       | |     | | | |   |       |     | ` <*>
 555 |     |       | |         |     |       | |     | | | |   |       |     |   + <*>
 556 |     |       | |         |     |       | |     | | | |   |       |     |   | + pure (\u1 -> (\u2 -> u1))
 557 |     |       | |         |     |       | |     | | | |   |       |     |   | ` <*>
 558 |     |       | |         |     |       | |     | | | |   |       |     |   |   + <*>
 559 |     |       | |         |     |       | |     | | | |   |       |     |   |   | + <*>
 560 |     |       | |         |     |       | |     | | | |   |       |     |   |   | | + pure (\u1 -> (\u2 -> u1))
 561 |     |       | |         |     |       | |     | | | |   |       |     |   |   | | ` pure (\u1 -> u1)
 562 |     |       | |         |     |       | |     | | | |   |       |     |   |   | ` <*>
 563 |     |       | |         |     |       | |     | | | |   |       |     |   |   |   + <*>
 564 |     |       | |         |     |       | |     | | | |   |       |     |   |   |   | + pure (\u1 -> (\u2 -> u1))
 565 |     |       | |         |     |       | |     | | | |   |       |     |   |   |   | ` pure '\''
 566 |     |       | |         |     |       | |     | | | |   |       |     |   |   |   ` satisfy
 567 |     |       | |         |     |       | |     | | | |   |       |     |   |   ` <|>
 568 |     |       | |         |     |       | |     | | | |   |       |     |   |     + <*>
 569 |     |       | |         |     |       | |     | | | |   |       |     |   |     | + <*>
 570 |     |       | |         |     |       | |     | | | |   |       |     |   |     | | + <*>
 571 |     |       | |         |     |       | |     | | | |   |       |     |   |     | | | + pure (\u1 -> (\u2 -> u1))
 572 |     |       | |         |     |       | |     | | | |   |       |     |   |     | | | ` pure (\u1 -> u1)
 573 |     |       | |         |     |       | |     | | | |   |       |     |   |     | | ` satisfy
 574 |     |       | |         |     |       | |     | | | |   |       |     |   |     | ` ref <hidden>
 575 |     |       | |         |     |       | |     | | | |   |       |     |   |     ` <*>
 576 |     |       | |         |     |       | |     | | | |   |       |     |   |       + <*>
 577 |     |       | |         |     |       | |     | | | |   |       |     |   |       | + <*>
 578 |     |       | |         |     |       | |     | | | |   |       |     |   |       | | + pure (\u1 -> (\u2 -> u1))
 579 |     |       | |         |     |       | |     | | | |   |       |     |   |       | | ` pure (\u1 -> u1)
 580 |     |       | |         |     |       | |     | | | |   |       |     |   |       | ` <*>
 581 |     |       | |         |     |       | |     | | | |   |       |     |   |       |   + <*>
 582 |     |       | |         |     |       | |     | | | |   |       |     |   |       |   | + pure (\u1 -> (\u2 -> u1))
 583 |     |       | |         |     |       | |     | | | |   |       |     |   |       |   | ` pure '\\'
 584 |     |       | |         |     |       | |     | | | |   |       |     |   |       |   ` satisfy
 585 |     |       | |         |     |       | |     | | | |   |       |     |   |       ` <*>
 586 |     |       | |         |     |       | |     | | | |   |       |     |   |         + <*>
 587 |     |       | |         |     |       | |     | | | |   |       |     |   |         | + <*>
 588 |     |       | |         |     |       | |     | | | |   |       |     |   |         | | + pure (\u1 -> (\u2 -> u1))
 589 |     |       | |         |     |       | |     | | | |   |       |     |   |         | | ` pure (\u1 -> u1)
 590 |     |       | |         |     |       | |     | | | |   |       |     |   |         | ` satisfy
 591 |     |       | |         |     |       | |     | | | |   |       |     |   |         ` ref <hidden>
 592 |     |       | |         |     |       | |     | | | |   |       |     |   ` <*>
 593 |     |       | |         |     |       | |     | | | |   |       |     |     + <*>
 594 |     |       | |         |     |       | |     | | | |   |       |     |     | + pure (\u1 -> (\u2 -> u1))
 595 |     |       | |         |     |       | |     | | | |   |       |     |     | ` <*>
 596 |     |       | |         |     |       | |     | | | |   |       |     |     |   + <*>
 597 |     |       | |         |     |       | |     | | | |   |       |     |     |   | + pure (\u1 -> (\u2 -> u1))
 598 |     |       | |         |     |       | |     | | | |   |       |     |     |   | ` pure '\''
 599 |     |       | |         |     |       | |     | | | |   |       |     |     |   ` satisfy
 600 |     |       | |         |     |       | |     | | | |   |       |     |     ` ref <hidden>
 601 |     |       | |         |     |       | |     | | | |   |       |     ` <*>
 602 |     |       | |         |     |       | |     | | | |   |       |       + <*>
 603 |     |       | |         |     |       | |     | | | |   |       |       | + <*>
 604 |     |       | |         |     |       | |     | | | |   |       |       | | + pure (\u1 -> (\u2 -> u1))
 605 |     |       | |         |     |       | |     | | | |   |       |       | | ` pure (\u1 -> u1)
 606 |     |       | |         |     |       | |     | | | |   |       |       | ` ref <hidden>
 607 |     |       | |         |     |       | |     | | | |   |       |       ` <|>
 608 |     |       | |         |     |       | |     | | | |   |       |         + <*>
 609 |     |       | |         |     |       | |     | | | |   |       |         | + <*>
 610 |     |       | |         |     |       | |     | | | |   |       |         | | + pure (\u1 -> (\u2 -> u1))
 611 |     |       | |         |     |       | |     | | | |   |       |         | | ` pure Term
 612 |     |       | |         |     |       | |     | | | |   |       |         | ` <|>
 613 |     |       | |         |     |       | |     | | | |   |       |         |   + <*>
 614 |     |       | |         |     |       | |     | | | |   |       |         |   | + <*>
 615 |     |       | |         |     |       | |     | | | |   |       |         |   | | + pure (\u1 -> (\u2 -> u1))
 616 |     |       | |         |     |       | |     | | | |   |       |         |   | | ` <*>
 617 |     |       | |         |     |       | |     | | | |   |       |         |   | |   + <*>
 618 |     |       | |         |     |       | |     | | | |   |       |         |   | |   | + <*>
 619 |     |       | |         |     |       | |     | | | |   |       |         |   | |   | | + pure (\u1 -> (\u2 -> u1))
 620 |     |       | |         |     |       | |     | | | |   |       |         |   | |   | | ` pure (\u1 -> u1)
 621 |     |       | |         |     |       | |     | | | |   |       |         |   | |   | ` ref <hidden>
 622 |     |       | |         |     |       | |     | | | |   |       |         |   | |   ` <|>
 623 |     |       | |         |     |       | |     | | | |   |       |         |   | |     + <*>
 624 |     |       | |         |     |       | |     | | | |   |       |         |   | |     | + <*>
 625 |     |       | |         |     |       | |     | | | |   |       |         |   | |     | | + pure (\u1 -> (\u2 -> u1))
 626 |     |       | |         |     |       | |     | | | |   |       |         |   | |     | | ` pure Term
 627 |     |       | |         |     |       | |     | | | |   |       |         |   | |     | ` <*>
 628 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |   + <*>
 629 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | + <*>
 630 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | | + pure (\u1 -> (\u2 -> u1))
 631 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | | ` pure (\u1 -> u1)
 632 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | ` rec <hidden>
 633 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |   ` <*>
 634 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     + <*>
 635 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | + <*>
 636 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | | + pure (\u1 -> (\u2 -> u1))
 637 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | | ` pure (\u1 -> u1)
 638 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | ` <*>
 639 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   + <*>
 640 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 641 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   | ` ref <hidden>
 642 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   ` def <hidden>
 643 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |     ` <|>
 644 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       + <*>
 645 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | + <*>
 646 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 647 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | | ` <*>
 648 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |   + ref <hidden>
 649 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |   ` <*>
 650 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     + <*>
 651 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | + <*>
 652 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | | + pure (\u1 -> (\u2 -> u1))
 653 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | | ` pure (\u1 -> u1)
 654 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | ` ref <hidden>
 655 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     ` rec <hidden>
 656 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | ` rec <hidden>
 657 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       ` pure (\u1 -> u1)
 658 |     |       | |         |     |       | |     | | | |   |       |         |   | |     |     ` ref <hidden>
 659 |     |       | |         |     |       | |     | | | |   |       |         |   | |     ` ref <hidden>
 660 |     |       | |         |     |       | |     | | | |   |       |         |   | ` ref <hidden>
 661 |     |       | |         |     |       | |     | | | |   |       |         |   ` ref <hidden>
 662 |     |       | |         |     |       | |     | | | |   |       |         ` ref <hidden>
 663 |     |       | |         |     |       | |     | | | |   |       ` <*>
 664 |     |       | |         |     |       | |     | | | |   |         + <*>
 665 |     |       | |         |     |       | |     | | | |   |         | + <*>
 666 |     |       | |         |     |       | |     | | | |   |         | | + pure (\u1 -> (\u2 -> u1))
 667 |     |       | |         |     |       | |     | | | |   |         | | ` pure (\u1 -> u1)
 668 |     |       | |         |     |       | |     | | | |   |         | ` <*>
 669 |     |       | |         |     |       | |     | | | |   |         |   + <*>
 670 |     |       | |         |     |       | |     | | | |   |         |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 671 |     |       | |         |     |       | |     | | | |   |         |   | ` ref <hidden>
 672 |     |       | |         |     |       | |     | | | |   |         |   ` def <hidden>
 673 |     |       | |         |     |       | |     | | | |   |         |     ` <|>
 674 |     |       | |         |     |       | |     | | | |   |         |       + <*>
 675 |     |       | |         |     |       | |     | | | |   |         |       | + <*>
 676 |     |       | |         |     |       | |     | | | |   |         |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 677 |     |       | |         |     |       | |     | | | |   |         |       | | ` <*>
 678 |     |       | |         |     |       | |     | | | |   |         |       | |   + <*>
 679 |     |       | |         |     |       | |     | | | |   |         |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
 680 |     |       | |         |     |       | |     | | | |   |         |       | |   | ` pure (\u1 -> (\u2 -> u1))
 681 |     |       | |         |     |       | |     | | | |   |         |       | |   ` <*>
 682 |     |       | |         |     |       | |     | | | |   |         |       | |     + <*>
 683 |     |       | |         |     |       | |     | | | |   |         |       | |     | + <*>
 684 |     |       | |         |     |       | |     | | | |   |         |       | |     | | + pure (\u1 -> (\u2 -> u1))
 685 |     |       | |         |     |       | |     | | | |   |         |       | |     | | ` pure (\u1 -> u1)
 686 |     |       | |         |     |       | |     | | | |   |         |       | |     | ` <*>
 687 |     |       | |         |     |       | |     | | | |   |         |       | |     |   + <*>
 688 |     |       | |         |     |       | |     | | | |   |         |       | |     |   | + pure (\u1 -> (\u2 -> u1))
 689 |     |       | |         |     |       | |     | | | |   |         |       | |     |   | ` <*>
 690 |     |       | |         |     |       | |     | | | |   |         |       | |     |   |   + <*>
 691 |     |       | |         |     |       | |     | | | |   |         |       | |     |   |   | + pure (\u1 -> (\u2 -> u1))
 692 |     |       | |         |     |       | |     | | | |   |         |       | |     |   |   | ` pure '!'
 693 |     |       | |         |     |       | |     | | | |   |         |       | |     |   |   ` satisfy
 694 |     |       | |         |     |       | |     | | | |   |         |       | |     |   ` ref <hidden>
 695 |     |       | |         |     |       | |     | | | |   |         |       | |     ` ref <hidden>
 696 |     |       | |         |     |       | |     | | | |   |         |       | ` rec <hidden>
 697 |     |       | |         |     |       | |     | | | |   |         |       ` pure (\u1 -> u1)
 698 |     |       | |         |     |       | |     | | | |   |         ` ref <hidden>
 699 |     |       | |         |     |       | |     | | | |   ` rec <hidden>
 700 |     |       | |         |     |       | |     | | | ` <|>
 701 |     |       | |         |     |       | |     | | |   + <*>
 702 |     |       | |         |     |       | |     | | |   | + <*>
 703 |     |       | |         |     |       | |     | | |   | | + pure (\u1 -> (\u2 -> u1))
 704 |     |       | |         |     |       | |     | | |   | | ` pure Term
 705 |     |       | |         |     |       | |     | | |   | ` <*>
 706 |     |       | |         |     |       | |     | | |   |   + <*>
 707 |     |       | |         |     |       | |     | | |   |   | + <*>
 708 |     |       | |         |     |       | |     | | |   |   | | + pure (\u1 -> (\u2 -> u1))
 709 |     |       | |         |     |       | |     | | |   |   | | ` pure (\u1 -> u1)
 710 |     |       | |         |     |       | |     | | |   |   | ` <*>
 711 |     |       | |         |     |       | |     | | |   |   |   + <*>
 712 |     |       | |         |     |       | |     | | |   |   |   | + <*>
 713 |     |       | |         |     |       | |     | | |   |   |   | | + pure (\u1 -> (\u2 -> u1))
 714 |     |       | |         |     |       | |     | | |   |   |   | | ` pure (\u1 -> u1)
 715 |     |       | |         |     |       | |     | | |   |   |   | ` try
 716 |     |       | |         |     |       | |     | | |   |   |   |   ` <*>
 717 |     |       | |         |     |       | |     | | |   |   |   |     + <*>
 718 |     |       | |         |     |       | |     | | |   |   |   |     | + <*>
 719 |     |       | |         |     |       | |     | | |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
 720 |     |       | |         |     |       | |     | | |   |   |   |     | | ` pure (\u1 -> u1)
 721 |     |       | |         |     |       | |     | | |   |   |   |     | ` try
 722 |     |       | |         |     |       | |     | | |   |   |   |     |   ` <*>
 723 |     |       | |         |     |       | |     | | |   |   |   |     |     + <*>
 724 |     |       | |         |     |       | |     | | |   |   |   |     |     | + pure cons
 725 |     |       | |         |     |       | |     | | |   |   |   |     |     | ` <*>
 726 |     |       | |         |     |       | |     | | |   |   |   |     |     |   + <*>
 727 |     |       | |         |     |       | |     | | |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
 728 |     |       | |         |     |       | |     | | |   |   |   |     |     |   | ` pure 'e'
 729 |     |       | |         |     |       | |     | | |   |   |   |     |     |   ` satisfy
 730 |     |       | |         |     |       | |     | | |   |   |   |     |     ` <*>
 731 |     |       | |         |     |       | |     | | |   |   |   |     |       + <*>
 732 |     |       | |         |     |       | |     | | |   |   |   |     |       | + pure cons
 733 |     |       | |         |     |       | |     | | |   |   |   |     |       | ` <*>
 734 |     |       | |         |     |       | |     | | |   |   |   |     |       |   + <*>
 735 |     |       | |         |     |       | |     | | |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
 736 |     |       | |         |     |       | |     | | |   |   |   |     |       |   | ` pure 'l'
 737 |     |       | |         |     |       | |     | | |   |   |   |     |       |   ` satisfy
 738 |     |       | |         |     |       | |     | | |   |   |   |     |       ` <*>
 739 |     |       | |         |     |       | |     | | |   |   |   |     |         + <*>
 740 |     |       | |         |     |       | |     | | |   |   |   |     |         | + pure cons
 741 |     |       | |         |     |       | |     | | |   |   |   |     |         | ` <*>
 742 |     |       | |         |     |       | |     | | |   |   |   |     |         |   + <*>
 743 |     |       | |         |     |       | |     | | |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
 744 |     |       | |         |     |       | |     | | |   |   |   |     |         |   | ` pure 's'
 745 |     |       | |         |     |       | |     | | |   |   |   |     |         |   ` satisfy
 746 |     |       | |         |     |       | |     | | |   |   |   |     |         ` <*>
 747 |     |       | |         |     |       | |     | | |   |   |   |     |           + <*>
 748 |     |       | |         |     |       | |     | | |   |   |   |     |           | + pure cons
 749 |     |       | |         |     |       | |     | | |   |   |   |     |           | ` <*>
 750 |     |       | |         |     |       | |     | | |   |   |   |     |           |   + <*>
 751 |     |       | |         |     |       | |     | | |   |   |   |     |           |   | + pure (\u1 -> (\u2 -> u1))
 752 |     |       | |         |     |       | |     | | |   |   |   |     |           |   | ` pure 'e'
 753 |     |       | |         |     |       | |     | | |   |   |   |     |           |   ` satisfy
 754 |     |       | |         |     |       | |     | | |   |   |   |     |           ` ref <hidden>
 755 |     |       | |         |     |       | |     | | |   |   |   |     ` ref <hidden>
 756 |     |       | |         |     |       | |     | | |   |   |   ` ref <hidden>
 757 |     |       | |         |     |       | |     | | |   |   ` rec <hidden>
 758 |     |       | |         |     |       | |     | | |   ` ref <hidden>
 759 |     |       | |         |     |       | |     | | ` <*>
 760 |     |       | |         |     |       | |     | |   + <*>
 761 |     |       | |         |     |       | |     | |   | + <*>
 762 |     |       | |         |     |       | |     | |   | | + pure (\u1 -> (\u2 -> u1))
 763 |     |       | |         |     |       | |     | |   | | ` pure (\u1 -> u1)
 764 |     |       | |         |     |       | |     | |   | ` <*>
 765 |     |       | |         |     |       | |     | |   |   + <*>
 766 |     |       | |         |     |       | |     | |   |   | + <*>
 767 |     |       | |         |     |       | |     | |   |   | | + pure (\u1 -> (\u2 -> u1))
 768 |     |       | |         |     |       | |     | |   |   | | ` pure (\u1 -> u1)
 769 |     |       | |         |     |       | |     | |   |   | ` <*>
 770 |     |       | |         |     |       | |     | |   |   |   + <*>
 771 |     |       | |         |     |       | |     | |   |   |   | + <*>
 772 |     |       | |         |     |       | |     | |   |   |   | | + pure (\u1 -> (\u2 -> u1))
 773 |     |       | |         |     |       | |     | |   |   |   | | ` pure (\u1 -> u1)
 774 |     |       | |         |     |       | |     | |   |   |   | ` try
 775 |     |       | |         |     |       | |     | |   |   |   |   ` <*>
 776 |     |       | |         |     |       | |     | |   |   |   |     + <*>
 777 |     |       | |         |     |       | |     | |   |   |   |     | + <*>
 778 |     |       | |         |     |       | |     | |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
 779 |     |       | |         |     |       | |     | |   |   |   |     | | ` pure (\u1 -> u1)
 780 |     |       | |         |     |       | |     | |   |   |   |     | ` try
 781 |     |       | |         |     |       | |     | |   |   |   |     |   ` <*>
 782 |     |       | |         |     |       | |     | |   |   |   |     |     + <*>
 783 |     |       | |         |     |       | |     | |   |   |   |     |     | + pure cons
 784 |     |       | |         |     |       | |     | |   |   |   |     |     | ` <*>
 785 |     |       | |         |     |       | |     | |   |   |   |     |     |   + <*>
 786 |     |       | |         |     |       | |     | |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
 787 |     |       | |         |     |       | |     | |   |   |   |     |     |   | ` pure 'w'
 788 |     |       | |         |     |       | |     | |   |   |   |     |     |   ` satisfy
 789 |     |       | |         |     |       | |     | |   |   |   |     |     ` <*>
 790 |     |       | |         |     |       | |     | |   |   |   |     |       + <*>
 791 |     |       | |         |     |       | |     | |   |   |   |     |       | + pure cons
 792 |     |       | |         |     |       | |     | |   |   |   |     |       | ` <*>
 793 |     |       | |         |     |       | |     | |   |   |   |     |       |   + <*>
 794 |     |       | |         |     |       | |     | |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
 795 |     |       | |         |     |       | |     | |   |   |   |     |       |   | ` pure 'h'
 796 |     |       | |         |     |       | |     | |   |   |   |     |       |   ` satisfy
 797 |     |       | |         |     |       | |     | |   |   |   |     |       ` <*>
 798 |     |       | |         |     |       | |     | |   |   |   |     |         + <*>
 799 |     |       | |         |     |       | |     | |   |   |   |     |         | + pure cons
 800 |     |       | |         |     |       | |     | |   |   |   |     |         | ` <*>
 801 |     |       | |         |     |       | |     | |   |   |   |     |         |   + <*>
 802 |     |       | |         |     |       | |     | |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
 803 |     |       | |         |     |       | |     | |   |   |   |     |         |   | ` pure 'i'
 804 |     |       | |         |     |       | |     | |   |   |   |     |         |   ` satisfy
 805 |     |       | |         |     |       | |     | |   |   |   |     |         ` <*>
 806 |     |       | |         |     |       | |     | |   |   |   |     |           + <*>
 807 |     |       | |         |     |       | |     | |   |   |   |     |           | + pure cons
 808 |     |       | |         |     |       | |     | |   |   |   |     |           | ` <*>
 809 |     |       | |         |     |       | |     | |   |   |   |     |           |   + <*>
 810 |     |       | |         |     |       | |     | |   |   |   |     |           |   | + pure (\u1 -> (\u2 -> u1))
 811 |     |       | |         |     |       | |     | |   |   |   |     |           |   | ` pure 'l'
 812 |     |       | |         |     |       | |     | |   |   |   |     |           |   ` satisfy
 813 |     |       | |         |     |       | |     | |   |   |   |     |           ` <*>
 814 |     |       | |         |     |       | |     | |   |   |   |     |             + <*>
 815 |     |       | |         |     |       | |     | |   |   |   |     |             | + pure cons
 816 |     |       | |         |     |       | |     | |   |   |   |     |             | ` <*>
 817 |     |       | |         |     |       | |     | |   |   |   |     |             |   + <*>
 818 |     |       | |         |     |       | |     | |   |   |   |     |             |   | + pure (\u1 -> (\u2 -> u1))
 819 |     |       | |         |     |       | |     | |   |   |   |     |             |   | ` pure 'e'
 820 |     |       | |         |     |       | |     | |   |   |   |     |             |   ` satisfy
 821 |     |       | |         |     |       | |     | |   |   |   |     |             ` ref <hidden>
 822 |     |       | |         |     |       | |     | |   |   |   |     ` ref <hidden>
 823 |     |       | |         |     |       | |     | |   |   |   ` ref <hidden>
 824 |     |       | |         |     |       | |     | |   |   ` ref <hidden>
 825 |     |       | |         |     |       | |     | |   ` rec <hidden>
 826 |     |       | |         |     |       | |     | ` try
 827 |     |       | |         |     |       | |     |   ` <*>
 828 |     |       | |         |     |       | |     |     + <*>
 829 |     |       | |         |     |       | |     |     | + pure (\u1 -> (\u2 -> u1))
 830 |     |       | |         |     |       | |     |     | ` <*>
 831 |     |       | |         |     |       | |     |     |   + <*>
 832 |     |       | |         |     |       | |     |     |   | + <*>
 833 |     |       | |         |     |       | |     |     |   | | + pure (\u1 -> (\u2 -> u1))
 834 |     |       | |         |     |       | |     |     |   | | ` pure (\u1 -> u1)
 835 |     |       | |         |     |       | |     |     |   | ` <*>
 836 |     |       | |         |     |       | |     |     |   |   + <*>
 837 |     |       | |         |     |       | |     |     |   |   | + <*>
 838 |     |       | |         |     |       | |     |     |   |   | | + pure (\u1 -> (\u2 -> u1))
 839 |     |       | |         |     |       | |     |     |   |   | | ` pure (\u1 -> u1)
 840 |     |       | |         |     |       | |     |     |   |   | ` <*>
 841 |     |       | |         |     |       | |     |     |   |   |   + <*>
 842 |     |       | |         |     |       | |     |     |   |   |   | + <*>
 843 |     |       | |         |     |       | |     |     |   |   |   | | + pure (\u1 -> (\u2 -> u1))
 844 |     |       | |         |     |       | |     |     |   |   |   | | ` pure (\u1 -> u1)
 845 |     |       | |         |     |       | |     |     |   |   |   | ` <|>
 846 |     |       | |         |     |       | |     |     |   |   |   |   + <*>
 847 |     |       | |         |     |       | |     |     |   |   |   |   | + <*>
 848 |     |       | |         |     |       | |     |     |   |   |   |   | | + pure (\u1 -> (\u2 -> u1))
 849 |     |       | |         |     |       | |     |     |   |   |   |   | | ` pure Term
 850 |     |       | |         |     |       | |     |     |   |   |   |   | ` <*>
 851 |     |       | |         |     |       | |     |     |   |   |   |   |   + <*>
 852 |     |       | |         |     |       | |     |     |   |   |   |   |   | + <*>
 853 |     |       | |         |     |       | |     |     |   |   |   |   |   | | + pure (\u1 -> (\u2 -> u1))
 854 |     |       | |         |     |       | |     |     |   |   |   |   |   | | ` pure (\u1 -> u1)
 855 |     |       | |         |     |       | |     |     |   |   |   |   |   | ` try
 856 |     |       | |         |     |       | |     |     |   |   |   |   |   |   ` <*>
 857 |     |       | |         |     |       | |     |     |   |   |   |   |   |     + <*>
 858 |     |       | |         |     |       | |     |     |   |   |   |   |   |     | + <*>
 859 |     |       | |         |     |       | |     |     |   |   |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
 860 |     |       | |         |     |       | |     |     |   |   |   |   |   |     | | ` pure (\u1 -> u1)
 861 |     |       | |         |     |       | |     |     |   |   |   |   |   |     | ` try
 862 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |   ` <*>
 863 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     + <*>
 864 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     | + pure cons
 865 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     | ` <*>
 866 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   + <*>
 867 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
 868 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   | ` pure 'v'
 869 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   ` satisfy
 870 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |     ` <*>
 871 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       + <*>
 872 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       | + pure cons
 873 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       | ` <*>
 874 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   + <*>
 875 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
 876 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   | ` pure 'a'
 877 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   ` satisfy
 878 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |       ` <*>
 879 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         + <*>
 880 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         | + pure cons
 881 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         | ` <*>
 882 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   + <*>
 883 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
 884 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   | ` pure 'r'
 885 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   ` satisfy
 886 |     |       | |         |     |       | |     |     |   |   |   |   |   |     |         ` ref <hidden>
 887 |     |       | |         |     |       | |     |     |   |   |   |   |   |     ` ref <hidden>
 888 |     |       | |         |     |       | |     |     |   |   |   |   |   ` ref <hidden>
 889 |     |       | |         |     |       | |     |     |   |   |   |   ` ref <hidden>
 890 |     |       | |         |     |       | |     |     |   |   |   ` <*>
 891 |     |       | |         |     |       | |     |     |   |   |     + <*>
 892 |     |       | |         |     |       | |     |     |   |   |     | + <*>
 893 |     |       | |         |     |       | |     |     |   |   |     | | + pure (\u1 -> (\u2 -> u1))
 894 |     |       | |         |     |       | |     |     |   |   |     | | ` pure (\u1 -> u1)
 895 |     |       | |         |     |       | |     |     |   |   |     | ` ref <hidden>
 896 |     |       | |         |     |       | |     |     |   |   |     ` <*>
 897 |     |       | |         |     |       | |     |     |   |   |       + <*>
 898 |     |       | |         |     |       | |     |     |   |   |       | + <*>
 899 |     |       | |         |     |       | |     |     |   |   |       | | + pure (\u1 -> (\u2 -> u1))
 900 |     |       | |         |     |       | |     |     |   |   |       | | ` pure (\u1 -> u1)
 901 |     |       | |         |     |       | |     |     |   |   |       | ` <*>
 902 |     |       | |         |     |       | |     |     |   |   |       |   + <*>
 903 |     |       | |         |     |       | |     |     |   |   |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 904 |     |       | |         |     |       | |     |     |   |   |       |   | ` ref <hidden>
 905 |     |       | |         |     |       | |     |     |   |   |       |   ` def <hidden>
 906 |     |       | |         |     |       | |     |     |   |   |       |     ` <|>
 907 |     |       | |         |     |       | |     |     |   |   |       |       + <*>
 908 |     |       | |         |     |       | |     |     |   |   |       |       | + <*>
 909 |     |       | |         |     |       | |     |     |   |   |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 910 |     |       | |         |     |       | |     |     |   |   |       |       | | ` <*>
 911 |     |       | |         |     |       | |     |     |   |   |       |       | |   + ref <hidden>
 912 |     |       | |         |     |       | |     |     |   |   |       |       | |   ` <*>
 913 |     |       | |         |     |       | |     |     |   |   |       |       | |     + <*>
 914 |     |       | |         |     |       | |     |     |   |   |       |       | |     | + <*>
 915 |     |       | |         |     |       | |     |     |   |   |       |       | |     | | + pure (\u1 -> (\u2 -> u1))
 916 |     |       | |         |     |       | |     |     |   |   |       |       | |     | | ` pure (\u1 -> u1)
 917 |     |       | |         |     |       | |     |     |   |   |       |       | |     | ` ref <hidden>
 918 |     |       | |         |     |       | |     |     |   |   |       |       | |     ` ref <hidden>
 919 |     |       | |         |     |       | |     |     |   |   |       |       | ` rec <hidden>
 920 |     |       | |         |     |       | |     |     |   |   |       |       ` pure (\u1 -> u1)
 921 |     |       | |         |     |       | |     |     |   |   |       ` ref <hidden>
 922 |     |       | |         |     |       | |     |     |   |   ` <*>
 923 |     |       | |         |     |       | |     |     |   |     + <*>
 924 |     |       | |         |     |       | |     |     |   |     | + pure (\u1 -> (\u2 -> u1))
 925 |     |       | |         |     |       | |     |     |   |     | ` <*>
 926 |     |       | |         |     |       | |     |     |   |     |   + <*>
 927 |     |       | |         |     |       | |     |     |   |     |   | + pure (\u1 -> (\u2 -> u1))
 928 |     |       | |         |     |       | |     |     |   |     |   | ` pure '='
 929 |     |       | |         |     |       | |     |     |   |     |   ` satisfy
 930 |     |       | |         |     |       | |     |     |   |     ` ref <hidden>
 931 |     |       | |         |     |       | |     |     |   ` <*>
 932 |     |       | |         |     |       | |     |     |     + <*>
 933 |     |       | |         |     |       | |     |     |     | + <*>
 934 |     |       | |         |     |       | |     |     |     | | + pure (\u1 -> (\u2 -> u1))
 935 |     |       | |         |     |       | |     |     |     | | ` pure (\u1 -> u1)
 936 |     |       | |         |     |       | |     |     |     | ` ref <hidden>
 937 |     |       | |         |     |       | |     |     |     ` <*>
 938 |     |       | |         |     |       | |     |     |       + <*>
 939 |     |       | |         |     |       | |     |     |       | + <*>
 940 |     |       | |         |     |       | |     |     |       | | + pure (\u1 -> (\u2 -> u1))
 941 |     |       | |         |     |       | |     |     |       | | ` pure (\u1 -> u1)
 942 |     |       | |         |     |       | |     |     |       | ` <*>
 943 |     |       | |         |     |       | |     |     |       |   + <*>
 944 |     |       | |         |     |       | |     |     |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
 945 |     |       | |         |     |       | |     |     |       |   | ` ref <hidden>
 946 |     |       | |         |     |       | |     |     |       |   ` def <hidden>
 947 |     |       | |         |     |       | |     |     |       |     ` <|>
 948 |     |       | |         |     |       | |     |     |       |       + <*>
 949 |     |       | |         |     |       | |     |     |       |       | + <*>
 950 |     |       | |         |     |       | |     |     |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
 951 |     |       | |         |     |       | |     |     |       |       | | ` <*>
 952 |     |       | |         |     |       | |     |     |       |       | |   + ref <hidden>
 953 |     |       | |         |     |       | |     |     |       |       | |   ` <*>
 954 |     |       | |         |     |       | |     |     |       |       | |     + <*>
 955 |     |       | |         |     |       | |     |     |       |       | |     | + <*>
 956 |     |       | |         |     |       | |     |     |       |       | |     | | + pure (\u1 -> (\u2 -> u1))
 957 |     |       | |         |     |       | |     |     |       |       | |     | | ` pure (\u1 -> u1)
 958 |     |       | |         |     |       | |     |     |       |       | |     | ` ref <hidden>
 959 |     |       | |         |     |       | |     |     |       |       | |     ` ref <hidden>
 960 |     |       | |         |     |       | |     |     |       |       | ` rec <hidden>
 961 |     |       | |         |     |       | |     |     |       |       ` pure (\u1 -> u1)
 962 |     |       | |         |     |       | |     |     |       ` ref <hidden>
 963 |     |       | |         |     |       | |     |     ` def <hidden>
 964 |     |       | |         |     |       | |     |       ` <*>
 965 |     |       | |         |     |       | |     |         + <*>
 966 |     |       | |         |     |       | |     |         | + pure (\u1 -> (\u2 -> u1))
 967 |     |       | |         |     |       | |     |         | ` <*>
 968 |     |       | |         |     |       | |     |         |   + <*>
 969 |     |       | |         |     |       | |     |         |   | + pure (\u1 -> (\u2 -> u1))
 970 |     |       | |         |     |       | |     |         |   | ` pure ';'
 971 |     |       | |         |     |       | |     |         |   ` satisfy
 972 |     |       | |         |     |       | |     |         ` ref <hidden>
 973 |     |       | |         |     |       | |     ` <*>
 974 |     |       | |         |     |       | |       + <*>
 975 |     |       | |         |     |       | |       | + pure (\u1 -> (\u2 -> u1))
 976 |     |       | |         |     |       | |       | ` ref <hidden>
 977 |     |       | |         |     |       | |       ` ref <hidden>
 978 |     |       | |         |     |       | ` rec <hidden>
 979 |     |       | |         |     |       ` pure (\u1 -> u1)
 980 |     |       | |         |     ` ref <hidden>
 981 |     |       | |         ` <*>
 982 |     |       | |           + <*>
 983 |     |       | |           | + pure (\u1 -> (\u2 -> u1))
 984 |     |       | |           | ` <*>
 985 |     |       | |           |   + <*>
 986 |     |       | |           |   | + pure (\u1 -> (\u2 -> u1))
 987 |     |       | |           |   | ` pure '}'
 988 |     |       | |           |   ` satisfy
 989 |     |       | |           ` ref <hidden>
 990 |     |       | ` rec <hidden>
 991 |     |       ` pure (\u1 -> u1)
 992 |     ` ref <hidden>
 993 ` eof