/
output2.txt
365 lines (365 loc) · 15.8 KB
/
output2.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
! 0 = \f.\x.x
! SUCC = \n.\f.\x.n f (f x)
! ADD = \m.\n.m SUCC n
! MULT = \m.\n.m (ADD n) 0
> MULT (SUCC (SUCC 0)) (SUCC (SUCC (SUCC 0)))
: ||||
: |||||||||||||||||||
: (\m.\n.m (ADD n) 0) (SUCC (SUCC 0)) (SUCC (SUCC (SUCC 0)))
: |||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||
: (\n.SUCC (SUCC 0) (ADD n) 0) (SUCC (SUCC (SUCC 0)))
: |||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||
: SUCC (SUCC 0) (ADD (SUCC (SUCC (SUCC 0)))) 0
: ||||
: ||||||||||||||||||||
: (\n.\f.\x.n f (f x)) (SUCC 0) (ADD (SUCC (SUCC (SUCC 0)))) 0
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||||
: (\f.\x.SUCC 0 f (f x)) (ADD (SUCC (SUCC (SUCC 0)))) 0
: |||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: (\x.SUCC 0 (ADD (SUCC (SUCC (SUCC 0)))) (ADD (SUCC (SUCC (SUCC 0))) x)) 0
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: SUCC 0 (ADD (SUCC (SUCC (SUCC 0)))) (ADD (SUCC (SUCC (SUCC 0))) 0)
: ||||
: ||||||||||||||||||||
: (\n.\f.\x.n f (f x)) 0 (ADD (SUCC (SUCC (SUCC 0)))) (ADD (SUCC (SUCC (SUCC 0))) 0)
: ||||||||||||||||||||||
: |||||||||||||||||
: (\f.\x.0 f (f x)) (ADD (SUCC (SUCC (SUCC 0)))) (ADD (SUCC (SUCC (SUCC 0))) 0)
: ||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: (\x.0 (ADD (SUCC (SUCC (SUCC 0)))) (ADD (SUCC (SUCC (SUCC 0))) x)) (ADD (SUCC (SUCC (SUCC 0))) 0)
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: 0 (ADD (SUCC (SUCC (SUCC 0)))) (ADD (SUCC (SUCC (SUCC 0))) (ADD (SUCC (SUCC (SUCC 0))) 0))
: |
: |||||||||
: (\f.\x.x) (ADD (SUCC (SUCC (SUCC 0)))) (ADD (SUCC (SUCC (SUCC 0))) (ADD (SUCC (SUCC (SUCC 0))) 0))
: ||||||||||||||||||||||||||||||||||||||
: ||||||
: (\x.x) (ADD (SUCC (SUCC (SUCC 0))) (ADD (SUCC (SUCC (SUCC 0))) 0))
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ADD (SUCC (SUCC (SUCC 0))) (ADD (SUCC (SUCC (SUCC 0))) 0)
: |||
: ||||||||||||||||
: (\m.\n.m SUCC n) (SUCC (SUCC (SUCC 0))) (ADD (SUCC (SUCC (SUCC 0))) 0)
: |||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||
: (\n.SUCC (SUCC (SUCC 0)) SUCC n) (ADD (SUCC (SUCC (SUCC 0))) 0)
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: SUCC (SUCC (SUCC 0)) SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)
: ||||
: ||||||||||||||||||||
: (\n.\f.\x.n f (f x)) (SUCC (SUCC 0)) SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)
: ||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||
: (\f.\x.SUCC (SUCC 0) f (f x)) SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)
: ||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||
: (\x.SUCC (SUCC 0) SUCC (SUCC x)) (ADD (SUCC (SUCC (SUCC 0))) 0)
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: SUCC (SUCC 0) SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0))
: ||||
: ||||||||||||||||||||
: (\n.\f.\x.n f (f x)) (SUCC 0) SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0))
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||||
: (\f.\x.SUCC 0 f (f x)) SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0))
: |||||||||||||||||||||||||||
: |||||||||||||||||||||||||
: (\x.SUCC 0 SUCC (SUCC x)) (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0))
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: SUCC 0 SUCC (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)))
: ||||
: ||||||||||||||||||||
: (\n.\f.\x.n f (f x)) 0 SUCC (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)))
: ||||||||||||||||||||||
: |||||||||||||||||
: (\f.\x.0 f (f x)) SUCC (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)))
: ||||||||||||||||||||||
: ||||||||||||||||||||
: (\x.0 SUCC (SUCC x)) (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)))
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: 0 SUCC (SUCC (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0))))
: |
: |||||||||
: (\f.\x.x) SUCC (SUCC (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0))))
: ||||||||||||||
: ||||||
: (\x.x) (SUCC (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0))))
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||||
: SUCC (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)))
: ||||
: ||||||||||||||||||||
: (\n.\f.\x.n f (f x)) (SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)))
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: \f.\x.SUCC (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)) f (f x)
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) (SUCC (ADD (SUCC (SUCC (SUCC 0))) 0)) f (f x)
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||||||
: \f.\x.(\f.\x.SUCC (ADD (SUCC (SUCC (SUCC 0))) 0) f (f x)) f (f x)
: |||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||
: \f.\x.(\x.SUCC (ADD (SUCC (SUCC (SUCC 0))) 0) f (f x)) (f x)
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||
: \f.\x.SUCC (ADD (SUCC (SUCC (SUCC 0))) 0) f (f (f x))
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) (ADD (SUCC (SUCC (SUCC 0))) 0) f (f (f x))
: |||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||
: \f.\x.(\f.\x.ADD (SUCC (SUCC (SUCC 0))) 0 f (f x)) f (f (f x))
: ||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||
: \f.\x.(\x.ADD (SUCC (SUCC (SUCC 0))) 0 f (f x)) (f (f x))
: |||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||
: \f.\x.ADD (SUCC (SUCC (SUCC 0))) 0 f (f (f (f x)))
: |||
: ||||||||||||||||
: \f.\x.(\m.\n.m SUCC n) (SUCC (SUCC (SUCC 0))) 0 f (f (f (f x)))
: |||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||
: \f.\x.(\n.SUCC (SUCC (SUCC 0)) SUCC n) 0 f (f (f (f x)))
: ||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||
: \f.\x.SUCC (SUCC (SUCC 0)) SUCC 0 f (f (f (f x)))
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) (SUCC (SUCC 0)) SUCC 0 f (f (f (f x)))
: ||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||
: \f.\x.(\f.\x.SUCC (SUCC 0) f (f x)) SUCC 0 f (f (f (f x)))
: ||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||
: \f.\x.(\x.SUCC (SUCC 0) SUCC (SUCC x)) 0 f (f (f (f x)))
: ||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||
: \f.\x.SUCC (SUCC 0) SUCC (SUCC 0) f (f (f (f x)))
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) (SUCC 0) SUCC (SUCC 0) f (f (f (f x)))
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||||
: \f.\x.(\f.\x.SUCC 0 f (f x)) SUCC (SUCC 0) f (f (f (f x)))
: |||||||||||||||||||||||||||
: |||||||||||||||||||||||||
: \f.\x.(\x.SUCC 0 SUCC (SUCC x)) (SUCC 0) f (f (f (f x)))
: ||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||
: \f.\x.SUCC 0 SUCC (SUCC (SUCC 0)) f (f (f (f x)))
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) 0 SUCC (SUCC (SUCC 0)) f (f (f (f x)))
: ||||||||||||||||||||||
: |||||||||||||||||
: \f.\x.(\f.\x.0 f (f x)) SUCC (SUCC (SUCC 0)) f (f (f (f x)))
: ||||||||||||||||||||||
: ||||||||||||||||||||
: \f.\x.(\x.0 SUCC (SUCC x)) (SUCC (SUCC 0)) f (f (f (f x)))
: ||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||
: \f.\x.0 SUCC (SUCC (SUCC (SUCC 0))) f (f (f (f x)))
: |
: |||||||||
: \f.\x.(\f.\x.x) SUCC (SUCC (SUCC (SUCC 0))) f (f (f (f x)))
: ||||||||||||||
: ||||||
: \f.\x.(\x.x) (SUCC (SUCC (SUCC 0))) f (f (f (f x)))
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||
: \f.\x.SUCC (SUCC (SUCC 0)) f (f (f (f x)))
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) (SUCC (SUCC 0)) f (f (f (f x)))
: ||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||
: \f.\x.(\f.\x.SUCC (SUCC 0) f (f x)) f (f (f (f x)))
: |||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||
: \f.\x.(\x.SUCC (SUCC 0) f (f x)) (f (f (f x)))
: ||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||
: \f.\x.SUCC (SUCC 0) f (f (f (f (f x))))
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) (SUCC 0) f (f (f (f (f x))))
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||||
: \f.\x.(\f.\x.SUCC 0 f (f x)) f (f (f (f (f x))))
: ||||||||||||||||||||||||
: |||||||||||||||||||
: \f.\x.(\x.SUCC 0 f (f x)) (f (f (f (f x))))
: |||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||
: \f.\x.SUCC 0 f (f (f (f (f (f x)))))
: ||||
: ||||||||||||||||||||
: \f.\x.(\n.\f.\x.n f (f x)) 0 f (f (f (f (f (f x)))))
: ||||||||||||||||||||||
: |||||||||||||||||
: \f.\x.(\f.\x.0 f (f x)) f (f (f (f (f (f x)))))
: |||||||||||||||||||
: ||||||||||||||
: \f.\x.(\x.0 f (f x)) (f (f (f (f (f x)))))
: ||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||
: \f.\x.0 f (f (f (f (f (f (f x))))))
: |
: |||||||||
: \f.\x.(\f.\x.x) f (f (f (f (f (f (f x))))))
: |||||||||||
: ||||||
: \f.\x.(\x.x) (f (f (f (f (f (f x))))))
: ||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||
: \f.\x.f (f (f (f (f (f x)))))
: Done (75 reductions).
----------------------------------------
! MULTC = \m.\n.\x.m (n x)
> MULTC (SUCC (SUCC 0)) (SUCC (SUCC (SUCC 0)))
: |||||
: ||||||||||||||||||
: (\m.\n.\x.m (n x)) (SUCC (SUCC 0)) (SUCC (SUCC (SUCC 0)))
: ||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||
: (\n.\x.SUCC (SUCC 0) (n x)) (SUCC (SUCC (SUCC 0)))
: ||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||
: \x.SUCC (SUCC 0) (SUCC (SUCC (SUCC 0)) x)
: ||||
: ||||||||||||||||||||
: \x.(\n.\f.\x.n f (f x)) (SUCC 0) (SUCC (SUCC (SUCC 0)) x)
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||||
: \x.(\f.\x.SUCC 0 f (f x)) (SUCC (SUCC (SUCC 0)) x)
: |||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: \x.\x1.SUCC 0 (SUCC (SUCC (SUCC 0)) x) (SUCC (SUCC (SUCC 0)) x x1)
: ||||
: ||||||||||||||||||||
: \x.\x1.(\n.\f.\x.n f (f x)) 0 (SUCC (SUCC (SUCC 0)) x) (SUCC (SUCC (SUCC 0)) x x1)
: ||||||||||||||||||||||
: |||||||||||||||||
: \x.\x1.(\f.\x.0 f (f x)) (SUCC (SUCC (SUCC 0)) x) (SUCC (SUCC (SUCC 0)) x x1)
: ||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: \x.\x1.(\x2.0 (SUCC (SUCC (SUCC 0)) x) (SUCC (SUCC (SUCC 0)) x x2)) (SUCC (SUCC (SUCC 0)) x x1)
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: \x.\x1.0 (SUCC (SUCC (SUCC 0)) x) (SUCC (SUCC (SUCC 0)) x (SUCC (SUCC (SUCC 0)) x x1))
: |
: |||||||||
: \x.\x1.(\f.\x.x) (SUCC (SUCC (SUCC 0)) x) (SUCC (SUCC (SUCC 0)) x (SUCC (SUCC (SUCC 0)) x x1))
: ||||||||||||||||||||||||||||||||||
: ||||||
: \x.\x1.(\x.x) (SUCC (SUCC (SUCC 0)) x (SUCC (SUCC (SUCC 0)) x x1))
: |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||||||||
: \x.\x1.SUCC (SUCC (SUCC 0)) x (SUCC (SUCC (SUCC 0)) x x1)
: ||||
: ||||||||||||||||||||
: \x.\x1.(\n.\f.\x.n f (f x)) (SUCC (SUCC 0)) x (SUCC (SUCC (SUCC 0)) x x1)
: ||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||
: \x.\x1.(\f.\x.SUCC (SUCC 0) f (f x)) x (SUCC (SUCC (SUCC 0)) x x1)
: |||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||
: \x.\x1.(\x3.SUCC (SUCC 0) x (x x3)) (SUCC (SUCC (SUCC 0)) x x1)
: ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||||||
: \x.\x1.SUCC (SUCC 0) x (x (SUCC (SUCC (SUCC 0)) x x1))
: ||||
: ||||||||||||||||||||
: \x.\x1.(\n.\f.\x.n f (f x)) (SUCC 0) x (x (SUCC (SUCC (SUCC 0)) x x1))
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||||
: \x.\x1.(\f.\x.SUCC 0 f (f x)) x (x (SUCC (SUCC (SUCC 0)) x x1))
: ||||||||||||||||||||||||
: |||||||||||||||||||||
: \x.\x1.(\x4.SUCC 0 x (x x4)) (x (SUCC (SUCC (SUCC 0)) x x1))
: |||||||||||||||||||||||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||||||||||||||||||
: \x.\x1.SUCC 0 x (x (x (SUCC (SUCC (SUCC 0)) x x1)))
: ||||
: ||||||||||||||||||||
: \x.\x1.(\n.\f.\x.n f (f x)) 0 x (x (x (SUCC (SUCC (SUCC 0)) x x1)))
: ||||||||||||||||||||||
: |||||||||||||||||
: \x.\x1.(\f.\x.0 f (f x)) x (x (x (SUCC (SUCC (SUCC 0)) x x1)))
: |||||||||||||||||||
: ||||||||||||||||
: \x.\x1.(\x5.0 x (x x5)) (x (x (SUCC (SUCC (SUCC 0)) x x1)))
: ||||||||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||||||||
: \x.\x1.0 x (x (x (x (SUCC (SUCC (SUCC 0)) x x1))))
: |
: |||||||||
: \x.\x1.(\f.\x.x) x (x (x (x (SUCC (SUCC (SUCC 0)) x x1))))
: |||||||||||
: ||||||
: \x.\x1.(\x.x) (x (x (x (SUCC (SUCC (SUCC 0)) x x1))))
: ||||||||||||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||||||||||
: \x.\x1.x (x (x (SUCC (SUCC (SUCC 0)) x x1)))
: ||||
: ||||||||||||||||||||
: \x.\x1.x (x (x ((\n.\f.\x.n f (f x)) (SUCC (SUCC 0)) x x1)))
: ||||||||||||||||||||||||||||||||||||
: |||||||||||||||||||||||||||||
: \x.\x1.x (x (x ((\f.\x.SUCC (SUCC 0) f (f x)) x x1)))
: |||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||||||
: \x.\x1.x (x (x ((\x6.SUCC (SUCC 0) x (x x6)) x1)))
: |||||||||||||||||||||||||||||||||
: ||||||||||||||||||||||||
: \x.\x1.x (x (x (SUCC (SUCC 0) x (x x1))))
: ||||
: ||||||||||||||||||||
: \x.\x1.x (x (x ((\n.\f.\x.n f (f x)) (SUCC 0) x (x x1))))
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||||
: \x.\x1.x (x (x ((\f.\x.SUCC 0 f (f x)) x (x x1))))
: ||||||||||||||||||||||||
: |||||||||||||||||||||
: \x.\x1.x (x (x ((\x7.SUCC 0 x (x x7)) (x x1))))
: ||||||||||||||||||||||||||||||
: |||||||||||||||||||||
: \x.\x1.x (x (x (SUCC 0 x (x (x x1)))))
: ||||
: ||||||||||||||||||||
: \x.\x1.x (x (x ((\n.\f.\x.n f (f x)) 0 x (x (x x1)))))
: ||||||||||||||||||||||
: |||||||||||||||||
: \x.\x1.x (x (x ((\f.\x.0 f (f x)) x (x (x x1)))))
: |||||||||||||||||||
: ||||||||||||||||
: \x.\x1.x (x (x ((\x8.0 x (x x8)) (x (x x1)))))
: |||||||||||||||||||||||||||||
: ||||||||||||||||||||
: \x.\x1.x (x (x (0 x (x (x (x x1))))))
: |
: |||||||||
: \x.\x1.x (x (x ((\f.\x.x) x (x (x (x x1))))))
: |||||||||||
: ||||||
: \x.\x1.x (x (x ((\x.x) (x (x (x x1))))))
: |||||||||||||||||||||||
: ||||||||||||||
: \x.\x1.x (x (x (x (x (x x1)))))
: Done (43 reductions).
----------------------------------------