diff --git "a/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md"
index b45ea7d3..2fcf9b46 100644
--- "a/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md"
+++ "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md"
@@ -383,7 +383,7 @@ end
 
 我们还有一个线上的演算场，可以用来方便地分享代码。
 
-[去 Nat 与 `(add)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gVHlwZSBlbmQKCm5vZGUgemVybwogIC0tLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQxCiAgTmF0IDpwcmV2CiAgLS0tLS0tLS0tLS0tCiAgTmF0IDp2YWx1ZSEKZW5kCgpub2RlIGFkZAogIE5hdCA6dGFyZ2V0IQogIE5hdCA6YWRkZW5kCiAgLS0tLS0tLS0tLS0tCiAgTmF0IDpyZXR1cm4KZW5kCgpydWxlIHplcm8gYWRkCiAgKGFkZCktYWRkZW5kCiAgcmV0dXJuLShhZGQpCmVuZAoKcnVsZSBhZGQxIGFkZAogIChhZGQpLWFkZGVuZAogIChhZGQxKS1wcmV2IGFkZAogIGFkZDEgcmV0dXJuLShhZGQpCmVuZAoKY2xhaW0gb25lIC0tIE5hdCBlbmQKCmRlZmluZSBvbmUKICB6ZXJvIGFkZDEKZW5kCgpjbGFpbSB0d28gLS0gTmF0IGVuZAoKZGVmaW5lIHR3bwogIG9uZSBvbmUgYWRkCmVuZAoKY2xhaW0gYWRkX3R3byBOYXQgLS0gTmF0IGVuZAoKZGVmaW5lIGFkZF90d28KICB0d28gYWRkCmVuZAoKb25lIGFkZF90d28Kb25lIGFkZF90d28KYWRk)
+[去 Nat 与 `(add)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gVHlwZSBlbmQKCm5vZGUgemVybwogIC0tLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQxCiAgTmF0IDpwcmV2CiAgLS0tLS0tLS0tLS0tCiAgTmF0IDp2YWx1ZSEKZW5kCgpub2RlIGFkZAogIE5hdCA6dGFyZ2V0IQogIE5hdCA6YWRkZW5kCiAgLS0tLS0tLS0tLS0tCiAgTmF0IDpyZXR1cm4KZW5kCgpydWxlIHplcm8gYWRkCiAgKGFkZCktYWRkZW5kCiAgcmV0dXJuLShhZGQpCmVuZAoKcnVsZSBhZGQxIGFkZAogIChhZGQpLWFkZGVuZAogIChhZGQxKS1wcmV2IGFkZAogIGFkZDEgcmV0dXJuLShhZGQpCmVuZAoKY2xhaW0gb25lIC0tIE5hdCBlbmQKCmRlZmluZSBvbmUKICB6ZXJvIGFkZDEKZW5kCgpjbGFpbSB0d28gLS0gTmF0IGVuZAoKZGVmaW5lIHR3bwogIG9uZSBhZGQxCmVuZAoKY2xhaW0gYWRkX3R3byBOYXQgLS0gTmF0IGVuZAoKZGVmaW5lIGFkZF90d28KICB0d28gYWRkCmVuZAoKb25lIGFkZF90d28Kb25lIGFkZF90d28KYWRk)
 
 ```
 type Nat -- Type end
@@ -426,7 +426,7 @@ end
 claim two -- Nat end
 
 define two
-  one one add
+  one add1
 end
 
 claim add_two Nat -- Nat end
@@ -641,7 +641,7 @@ rule add1 max_aux
 end
 ```
 
-[去 Nat 与 `(max)` 的演算场](https://inet.run/playground/)
+[去 Nat 与 `(max)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gVHlwZSBlbmQKCm5vZGUgemVybwogIC0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQxCiAgTmF0IDpwcmV2CiAgLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKLy8gVG8gZGVmaW5lIGBtYXhgLCB3ZSBuZWVkIGBtYXhfYXV4YC4KCm5vZGUgbWF4X2F1eAogIE5hdCA6Zmlyc3QKICBOYXQgOnNlY29uZCEKICAtLS0tLS0tLQogIE5hdCA6cmV0dXJuCmVuZAoKbm9kZSBtYXgKICBOYXQgOmZpcnN0IQogIE5hdCA6c2Vjb25kCiAgLS0tLS0tLS0tLQogIE5hdCA6cmV0dXJuCmVuZAoKcnVsZSB6ZXJvIG1heAogIChtYXgpLXNlY29uZCByZXR1cm4tKG1heCkKZW5kCgpydWxlIGFkZDEgbWF4CiAgKG1heCktc2Vjb25kIChhZGQxKS1wcmV2IG1heF9hdXgKICByZXR1cm4tKG1heCkKZW5kCgpydWxlIHplcm8gbWF4X2F1eAogIChtYXhfYXV4KS1maXJzdCBhZGQxCiAgcmV0dXJuLShtYXhfYXV4KQplbmQKCnJ1bGUgYWRkMSBtYXhfYXV4CiAgKGFkZDEpLXByZXYgKG1heF9hdXgpLWZpcnN0IG1heAogIGFkZDEgcmV0dXJuLShtYXhfYXV4KQplbmQKCmNsYWltIG9uZSAtLSBOYXQgZW5kCmRlZmluZSBvbmUgemVybyBhZGQxIGVuZAoKY2xhaW0gdHdvIC0tIE5hdCBlbmQKZGVmaW5lIHR3byBvbmUgYWRkMSBlbmQKCmNsYWltIHRocmVlIC0tIE5hdCBlbmQKZGVmaW5lIHRocmVlIHR3byBhZGQxIGVuZAoKY2xhaW0gZm91ciAtLSBOYXQgZW5kCmRlZmluZSBmb3VyIHRocmVlIGFkZDEgZW5kCgp0aHJlZSB0d28gbWF4Cgp6ZXJvIHR3byBtYXg)
 
 ```
 type Nat -- Type end