up

docs/articles/反应网编程.md

@@ -383,7 +383,7 @@ end
 
 我们还有一个线上的演算场，可以用来方便地分享代码。
 
-[去关于 Nat 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gVHlwZSBlbmQKCm5vZGUgemVybwogIC0tLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQxCiAgTmF0IDpwcmV2CiAgLS0tLS0tLS0tLS0tCiAgTmF0IDp2YWx1ZSEKZW5kCgpub2RlIGFkZAogIE5hdCA6dGFyZ2V0IQogIE5hdCA6YWRkZW5kCiAgLS0tLS0tLS0tLS0tCiAgTmF0IDpyZXR1cm4KZW5kCgpydWxlIHplcm8gYWRkCiAgKGFkZCktYWRkZW5kCiAgcmV0dXJuLShhZGQpCmVuZAoKcnVsZSBhZGQxIGFkZAogIChhZGQpLWFkZGVuZAogIChhZGQxKS1wcmV2IGFkZAogIGFkZDEgcmV0dXJuLShhZGQpCmVuZAoKY2xhaW0gb25lIC0tIE5hdCBlbmQKCmRlZmluZSBvbmUKICB6ZXJvIGFkZDEKZW5kCgpjbGFpbSB0d28gLS0gTmF0IGVuZAoKZGVmaW5lIHR3bwogIG9uZSBvbmUgYWRkCmVuZAoKY2xhaW0gYWRkX3R3byBOYXQgLS0gTmF0IGVuZAoKZGVmaW5lIGFkZF90d28KICB0d28gYWRkCmVuZAoKb25lIGFkZF90d28Kb25lIGFkZF90d28KYWRk)
+[去 Nat 与 `(add)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gVHlwZSBlbmQKCm5vZGUgemVybwogIC0tLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQxCiAgTmF0IDpwcmV2CiAgLS0tLS0tLS0tLS0tCiAgTmF0IDp2YWx1ZSEKZW5kCgpub2RlIGFkZAogIE5hdCA6dGFyZ2V0IQogIE5hdCA6YWRkZW5kCiAgLS0tLS0tLS0tLS0tCiAgTmF0IDpyZXR1cm4KZW5kCgpydWxlIHplcm8gYWRkCiAgKGFkZCktYWRkZW5kCiAgcmV0dXJuLShhZGQpCmVuZAoKcnVsZSBhZGQxIGFkZAogIChhZGQpLWFkZGVuZAogIChhZGQxKS1wcmV2IGFkZAogIGFkZDEgcmV0dXJuLShhZGQpCmVuZAoKY2xhaW0gb25lIC0tIE5hdCBlbmQKCmRlZmluZSBvbmUKICB6ZXJvIGFkZDEKZW5kCgpjbGFpbSB0d28gLS0gTmF0IGVuZAoKZGVmaW5lIHR3bwogIG9uZSBvbmUgYWRkCmVuZAoKY2xhaW0gYWRkX3R3byBOYXQgLS0gTmF0IGVuZAoKZGVmaW5lIGFkZF90d28KICB0d28gYWRkCmVuZAoKb25lIGFkZF90d28Kb25lIGFkZF90d28KYWRk)
 
 ```
 type Nat -- Type end
@@ -641,6 +641,74 @@ rule add1 max_aux
 end
 ```
 
+[去 Nat 与 `(max)` 的演算场](https://inet.run/playground/)
+
+```
+type Nat -- Type end
+
+node zero
+  ------
+  Nat :value!
+end
+
+node add1
+  Nat :prev
+  ----------
+  Nat :value!
+end
+
+// To define `max`, we need `max_aux`.
+
+node max_aux
+  Nat :first
+  Nat :second!
+  --------
+  Nat :return
+end
+
+node max
+  Nat :first!
+  Nat :second
+  ----------
+  Nat :return
+end
+
+rule zero max
+  (max)-second return-(max)
+end
+
+rule add1 max
+  (max)-second (add1)-prev max_aux
+  return-(max)
+end
+
+rule zero max_aux
+  (max_aux)-first add1
+  return-(max_aux)
+end
+
+rule add1 max_aux
+  (add1)-prev (max_aux)-first max
+  add1 return-(max_aux)
+end
+
+claim one -- Nat end
+define one zero add1 end
+
+claim two -- Nat end
+define two one add1 end
+
+claim three -- Nat end
+define three two add1 end
+
+claim four -- Nat end
+define four three add1 end
+
+three two max
+
+zero two max
+```
+
 # TODO
 
 `nat_erase`, `nat_dup` -- 零返回值和多返回值。