{"generator":"GNU social 2.0.2-beta0","title":"Conversation","totalItems":2,"items":[{"actor":{"id":"https:\/\/mastodon.tojo.tokyo\/users\/tojoqk","displayName":"\u304d\u3085\u30fc\u3051\u30fc","status_net":{"avatarLinks":[{"url":"https:\/\/social.senooken.jp\/avatar\/27709-original-tmp20200812042025.png","rel":"avatar","type":"image\/png","width":300,"height":300},{"url":"https:\/\/social.senooken.jp\/avatar\/27709-96-20200812042027.png","rel":"avatar","type":"image\/png","width":96,"height":96},{"url":"https:\/\/social.senooken.jp\/avatar\/27709-48-20200812042027.png","rel":"avatar","type":"image\/png","width":48,"height":48},{"url":"https:\/\/social.senooken.jp\/avatar\/27709-24-20200812042027.png","rel":"avatar","type":"image\/png","width":24,"height":24}],"profile_info":{"local_id":"27709"}},"image":{"url":"https:\/\/social.senooken.jp\/avatar\/27709-96-20200812042027.png","rel":"avatar","type":"image\/png","width":96,"height":96},"objectType":"person","summary":"GNU Guix \u30e6\u30fc\u30b6\u30fc\u306e Schemer \u3067\u3001\u81ea\u7531\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u3068\u884c\u52d5\u5206\u6790\u5b66\u304c\u597d\u304d\u3067\u3059\u3002Jami: e5fdfccb74c383420e6e647897dae018a4bd61fb","url":"https:\/\/mastodon.tojo.tokyo\/@tojoqk","portablecontacts_net":{"preferredUsername":"tojoqk","displayName":"\u304d\u3085\u30fc\u3051\u30fc","note":"GNU Guix \u30e6\u30fc\u30b6\u30fc\u306e Schemer \u3067\u3001\u81ea\u7531\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u3068\u884c\u52d5\u5206\u6790\u5b66\u304c\u597d\u304d\u3067\u3059\u3002Jami: e5fdfccb74c383420e6e647897dae018a4bd61fb"}},"content":"<p>ACL2 \u306e\u30ea\u30b9\u30c8\u306e\u9806\u5217\u306e\u6570\u304c\u968e\u4e57\u306b\u306a\u308b\u3084\u3064\u306e\u8a3c\u660e\u3092\u8d85\u30ea\u30d5\u30a1\u30af\u30bf\u30ea\u30f3\u30b0\u3057\u305f\u3002\u3084\u306f\u308a\u5168\u3066\u304c\u898b\u3048\u3066\u3044\u308b\u72b6\u614b\u3067\u304b\u304f\u3068\u9055\u3046\u3002\u7121\u99c4\u306a\u5b9a\u7406\u306e\u8a3c\u660e\u3092\u7701\u3044\u305f\u3053\u3068\u3067 300 \u884c\u3042\u3063\u305f\u306e\u304c 200 \u884c\u304f\u3089\u3044\u306b\u306a\u3063\u305f\u3057\u3001\u5168\u4f53\u7684\u306b\u7f8e\u3057\u304f\u306a\u3063\u305f\u3002\u6700\u9ad8\u3060\u3002<\/p><p>source: <a href=\"https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=7e2450d7f7ef454e8fa0a5c41ec6c305cc5a8c25\" rel=\"nofollow noreferrer\">https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=7e2450d7f7ef454e8fa0a5c41ec6c305cc5a8c25<\/a>CI: <a href=\"https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/235\" rel=\"nofollow noreferrer\">https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/235<\/a><\/p>","generator":{"id":"tag:social.senooken.jp,2026-08-09:notice-source:ActivityPub","objectType":"application","status_net":{"source_code":"ActivityPub"}},"id":"https:\/\/mastodon.tojo.tokyo\/users\/tojoqk\/statuses\/106746773011001817","object":{"id":"https:\/\/mastodon.tojo.tokyo\/users\/tojoqk\/statuses\/106746773011001817","objectType":"note","content":"<p>ACL2 \u306e\u30ea\u30b9\u30c8\u306e\u9806\u5217\u306e\u6570\u304c\u968e\u4e57\u306b\u306a\u308b\u3084\u3064\u306e\u8a3c\u660e\u3092\u8d85\u30ea\u30d5\u30a1\u30af\u30bf\u30ea\u30f3\u30b0\u3057\u305f\u3002\u3084\u306f\u308a\u5168\u3066\u304c\u898b\u3048\u3066\u3044\u308b\u72b6\u614b\u3067\u304b\u304f\u3068\u9055\u3046\u3002\u7121\u99c4\u306a\u5b9a\u7406\u306e\u8a3c\u660e\u3092\u7701\u3044\u305f\u3053\u3068\u3067 300 \u884c\u3042\u3063\u305f\u306e\u304c 200 \u884c\u304f\u3089\u3044\u306b\u306a\u3063\u305f\u3057\u3001\u5168\u4f53\u7684\u306b\u7f8e\u3057\u304f\u306a\u3063\u305f\u3002\u6700\u9ad8\u3060\u3002<\/p><p>source: <a href=\"https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=7e2450d7f7ef454e8fa0a5c41ec6c305cc5a8c25\" rel=\"nofollow noreferrer\">https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=7e2450d7f7ef454e8fa0a5c41ec6c305cc5a8c25<\/a>CI: <a href=\"https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/235\" rel=\"nofollow noreferrer\">https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/235<\/a><\/p>","url":"https:\/\/mastodon.tojo.tokyo\/@tojoqk\/106746773011001817","status_net":{"notice_id":null},"inReplyTo":{"objectType":"note","id":"https:\/\/mastodon.tojo.tokyo\/users\/tojoqk\/statuses\/106738161677829620","url":"https:\/\/mastodon.tojo.tokyo\/@tojoqk\/106738161677829620"}},"to":[{"objectType":"http:\/\/activitystrea.ms\/schema\/1.0\/collection","id":"http:\/\/activityschema.org\/collection\/public"}],"status_net":{"conversation":"tag:social.senooken.jp,2021-08-11:objectType=thread:nonce=6874c252f4809fb9","notice_info":{"local_id":"3865420","source":"ActivityPub"}},"published":"2021-08-13T03:48:15+00:00","provider":{"objectType":"service","displayName":"senooken JP Social","url":"https:\/\/social.senooken.jp\/"},"verb":"post","url":"https:\/\/mastodon.tojo.tokyo\/@tojoqk\/106746773011001817"},{"actor":{"id":"https:\/\/mastodon.tojo.tokyo\/users\/tojoqk","displayName":"\u304d\u3085\u30fc\u3051\u30fc","status_net":{"avatarLinks":[{"url":"https:\/\/social.senooken.jp\/avatar\/27709-original-tmp20200812042025.png","rel":"avatar","type":"image\/png","width":300,"height":300},{"url":"https:\/\/social.senooken.jp\/avatar\/27709-96-20200812042027.png","rel":"avatar","type":"image\/png","width":96,"height":96},{"url":"https:\/\/social.senooken.jp\/avatar\/27709-48-20200812042027.png","rel":"avatar","type":"image\/png","width":48,"height":48},{"url":"https:\/\/social.senooken.jp\/avatar\/27709-24-20200812042027.png","rel":"avatar","type":"image\/png","width":24,"height":24}],"profile_info":{"local_id":"27709"}},"image":{"url":"https:\/\/social.senooken.jp\/avatar\/27709-96-20200812042027.png","rel":"avatar","type":"image\/png","width":96,"height":96},"objectType":"person","summary":"GNU Guix \u30e6\u30fc\u30b6\u30fc\u306e Schemer \u3067\u3001\u81ea\u7531\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u3068\u884c\u52d5\u5206\u6790\u5b66\u304c\u597d\u304d\u3067\u3059\u3002Jami: e5fdfccb74c383420e6e647897dae018a4bd61fb","url":"https:\/\/mastodon.tojo.tokyo\/@tojoqk","portablecontacts_net":{"preferredUsername":"tojoqk","displayName":"\u304d\u3085\u30fc\u3051\u30fc","note":"GNU Guix \u30e6\u30fc\u30b6\u30fc\u306e Schemer \u3067\u3001\u81ea\u7531\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u3068\u884c\u52d5\u5206\u6790\u5b66\u304c\u597d\u304d\u3067\u3059\u3002Jami: e5fdfccb74c383420e6e647897dae018a4bd61fb"}},"content":"<p>ACL2 \u3067\u30ea\u30b9\u30c8\u306e\u5168\u3066\u306e\u9806\u5217\u3092\u6c42\u3081\u308b\u95a2\u6570\u3092\u66f8\u3044\u3066\u3001\u9806\u5217\u306e\u6570\u304c\u5143\u306e\u30ea\u30b9\u30c8\u306e\u9577\u3055\u306e\u968e\u4e57\u500b\u306b\u306a\u308b\u3053\u3068\u3092\u8a3c\u660e\u3067\u304d\u305f\u3002\u3053\u308c\u306f\u60f3\u50cf\u4ee5\u4e0a\u306b\u5927\u5909\u3060\u3063\u305f\u3002\u9806\u5217\u306e\u5b9f\u88c5\u306f20\u884c\u672a\u6e80\u306a\u306e\u306b\u88dc\u52a9\u95a2\u6570\u3084\u88dc\u52a9\u5b9a\u7406\u3067 300 \u884c\u304f\u3089\u3044\u66f8\u3044\u3066\u3044\u308b\u2026\u2026\u3002\u305f\u3076\u3093\u4f55\u304b\u56de\u308a\u9053\u3092\u3057\u3066\u3044\u308b\u6c17\u304c\u3059\u308b\u306e\u3067\u77ed\u7e2e\u306f\u53ef\u80fd\u3060\u3068\u601d\u3046\u3002<\/p><p>source: <a href=\"https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=c7cb466e2caf7bc500f66472d8781a14037eec1e\" rel=\"nofollow noreferrer\">https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=c7cb466e2caf7bc500f66472d8781a14037eec1e<\/a>CI: <a href=\"https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/221\" rel=\"nofollow noreferrer\">https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/221<\/a><\/p>","generator":{"id":"tag:social.senooken.jp,2026-08-09:notice-source:ActivityPub","objectType":"application","status_net":{"source_code":"ActivityPub"}},"id":"https:\/\/mastodon.tojo.tokyo\/users\/tojoqk\/statuses\/106738161677829620","object":{"id":"https:\/\/mastodon.tojo.tokyo\/users\/tojoqk\/statuses\/106738161677829620","objectType":"note","content":"<p>ACL2 \u3067\u30ea\u30b9\u30c8\u306e\u5168\u3066\u306e\u9806\u5217\u3092\u6c42\u3081\u308b\u95a2\u6570\u3092\u66f8\u3044\u3066\u3001\u9806\u5217\u306e\u6570\u304c\u5143\u306e\u30ea\u30b9\u30c8\u306e\u9577\u3055\u306e\u968e\u4e57\u500b\u306b\u306a\u308b\u3053\u3068\u3092\u8a3c\u660e\u3067\u304d\u305f\u3002\u3053\u308c\u306f\u60f3\u50cf\u4ee5\u4e0a\u306b\u5927\u5909\u3060\u3063\u305f\u3002\u9806\u5217\u306e\u5b9f\u88c5\u306f20\u884c\u672a\u6e80\u306a\u306e\u306b\u88dc\u52a9\u95a2\u6570\u3084\u88dc\u52a9\u5b9a\u7406\u3067 300 \u884c\u304f\u3089\u3044\u66f8\u3044\u3066\u3044\u308b\u2026\u2026\u3002\u305f\u3076\u3093\u4f55\u304b\u56de\u308a\u9053\u3092\u3057\u3066\u3044\u308b\u6c17\u304c\u3059\u308b\u306e\u3067\u77ed\u7e2e\u306f\u53ef\u80fd\u3060\u3068\u601d\u3046\u3002<\/p><p>source: <a href=\"https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=c7cb466e2caf7bc500f66472d8781a14037eec1e\" rel=\"nofollow noreferrer\">https:\/\/git.tojo.tokyo\/acl2-theorems.git\/tree\/permutations.lisp?id=c7cb466e2caf7bc500f66472d8781a14037eec1e<\/a>CI: <a href=\"https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/221\" rel=\"nofollow noreferrer\">https:\/\/ci.tojo.tokyo\/jobs\/acl2-verify\/221<\/a><\/p>","url":"https:\/\/mastodon.tojo.tokyo\/@tojoqk\/106738161677829620","status_net":{"notice_id":null}},"to":[{"objectType":"http:\/\/activitystrea.ms\/schema\/1.0\/collection","id":"http:\/\/activityschema.org\/collection\/public"}],"status_net":{"conversation":"tag:social.senooken.jp,2021-08-11:objectType=thread:nonce=6874c252f4809fb9","notice_info":{"local_id":"3862037","source":"ActivityPub"}},"published":"2021-08-11T15:18:16+00:00","provider":{"objectType":"service","displayName":"senooken JP Social","url":"https:\/\/social.senooken.jp\/"},"verb":"post","url":"https:\/\/mastodon.tojo.tokyo\/@tojoqk\/106738161677829620"}],"links":[{"url":"https:\/\/social.senooken.jp\/conversation\/2785896","rel":"alternate","type":"text\/html"}]}