((k:{k:
| 0 = k 
}
k
)+(k:{k:| 
0 = k }k)) ~ ((k:{k:| 0 = k }k)+(k:{k:| 0 = k }k)) ~ | By: |
ml_RWH_ooc_chain((k:{k: | 0 = k }k | k:1k | 0 | 1))
THEN ml_RWH_ooc_chain{:s, 0:s, true:s} ml_RWH_ooc_chain((k:{k: | 0 = k }k | k: k | )) |
| 1 |
(k:{k:| 0 = k }k) ~ (k:1k) | 1 step |
| 2 |
(k:1k) ~ (0) | 1 step |
| 3 |
(0) ~ 1 | 1 step |
| 4 |
(k:{k:| 0 = k }k) ~ (k:k) | 2 steps |
| 5 |
(k:k) ~ | 1 step |
| 6 |
(1+) ~ | 1 step |
About:
 |  |  |  |  |  |