{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":568310372,"defaultBranch":"master","name":"matching-logic-mm0","ownerLogin":"Formal-Systems-Laboratory","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2022-11-20T05:26:48.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/12419182?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1725238642.0","currentOid":""},"activityList":{"items":[{"before":"b6019045130ef288e77fbb8b5bc27039f99109fc","after":"cf142e6355c1382973e0c805673138d807225742","ref":"refs/heads/theory_separation","pushedAt":"2024-09-13T02:59:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished proof","shortMessageHtmlLink":"finished proof"}},{"before":"e3a167db850423f6ea468c1d1c1e50e2be2798fa","after":"b6019045130ef288e77fbb8b5bc27039f99109fc","ref":"refs/heads/theory_separation","pushedAt":"2024-09-13T02:50:49.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished proof","shortMessageHtmlLink":"finished proof"}},{"before":"8caaee30112210a3aa78c09187609a78d159e389","after":"e3a167db850423f6ea468c1d1c1e50e2be2798fa","ref":"refs/heads/theory_separation","pushedAt":"2024-09-10T00:25:34.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished proof","shortMessageHtmlLink":"finished proof"}},{"before":"f16b91e7d6266ef533a3389d4998797af985cc64","after":"8caaee30112210a3aa78c09187609a78d159e389","ref":"refs/heads/theory_separation","pushedAt":"2024-09-10T00:25:00.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished proof","shortMessageHtmlLink":"finished proof"}},{"before":"08adb392f936abc0589eb6eded2abf04a280c243","after":"f16b91e7d6266ef533a3389d4998797af985cc64","ref":"refs/heads/theory_separation","pushedAt":"2024-09-10T00:19:32.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished proof","shortMessageHtmlLink":"finished proof"}},{"before":"e6f73b87fae61c2b20fc6f924b1a1412f9960c3c","after":"08adb392f936abc0589eb6eded2abf04a280c243","ref":"refs/heads/theory_separation","pushedAt":"2024-09-09T23:20:56.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished proof","shortMessageHtmlLink":"finished proof"}},{"before":"42babb6e4752f2f360bb5fdafd77f407717fe962","after":"e6f73b87fae61c2b20fc6f924b1a1412f9960c3c","ref":"refs/heads/theory_separation","pushedAt":"2024-09-07T00:23:05.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"5ebf6d30f229e52d903f69e2d5757a944087e386","after":"42babb6e4752f2f360bb5fdafd77f407717fe962","ref":"refs/heads/theory_separation","pushedAt":"2024-09-04T23:42:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"03447cab901437ac257cff8dab78200da15b04a7","after":null,"ref":"refs/heads/deleteme_debugging","pushedAt":"2024-09-02T00:57:22.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"}},{"before":"4a0fa90dbd8ddf7f11bf8119f532888ade7e029a","after":"5ebf6d30f229e52d903f69e2d5757a944087e386","ref":"refs/heads/theory_separation","pushedAt":"2024-09-02T00:57:01.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished reproving the vars case","shortMessageHtmlLink":"finished reproving the vars case"}},{"before":"b386a6715cde6942f433009d4d28d56d3153d8f1","after":"4a0fa90dbd8ddf7f11bf8119f532888ade7e029a","ref":"refs/heads/theory_separation","pushedAt":"2024-09-02T00:45:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished reproving the vars case","shortMessageHtmlLink":"finished reproving the vars case"}},{"before":"1f0a304f25c92de3710e633b574540da7a0e4311","after":"b386a6715cde6942f433009d4d28d56d3153d8f1","ref":"refs/heads/theory_separation","pushedAt":"2024-08-12T08:00:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished EV proof","shortMessageHtmlLink":"finished EV proof"}},{"before":null,"after":"03447cab901437ac257cff8dab78200da15b04a7","ref":"refs/heads/deleteme_debugging","pushedAt":"2024-08-09T19:55:05.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"baa8142271ec1a4299a69cef4548172ff365e056","after":"1f0a304f25c92de3710e633b574540da7a0e4311","ref":"refs/heads/theory_separation","pushedAt":"2024-08-06T17:33:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished bulk of ev proof","shortMessageHtmlLink":"finished bulk of ev proof"}},{"before":"b0ea5c7ae8dd17be24a32862ba21cd9c97c49b8b","after":"baa8142271ec1a4299a69cef4548172ff365e056","ref":"refs/heads/theory_separation","pushedAt":"2024-07-19T04:38:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"simplified all induction principle lemmas","shortMessageHtmlLink":"simplified all induction principle lemmas"}},{"before":"2921270b74624b6b6990009f4dd6764b1cd7029d","after":"b0ea5c7ae8dd17be24a32862ba21cd9c97c49b8b","ref":"refs/heads/theory_separation","pushedAt":"2024-07-16T16:39:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"almost finished proof","shortMessageHtmlLink":"almost finished proof"}},{"before":"6555d60e99aff90d00624887a2cadebeb8e4ce0a","after":"2921270b74624b6b6990009f4dd6764b1cd7029d","ref":"refs/heads/theory_separation","pushedAt":"2024-07-16T02:59:13.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"finished main proof but with some gaps","shortMessageHtmlLink":"finished main proof but with some gaps"}},{"before":"0876c3f2692047e08e337d981ad3e182c8992a80","after":"6555d60e99aff90d00624887a2cadebeb8e4ce0a","ref":"refs/heads/theory_separation","pushedAt":"2024-07-15T20:35:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"002de001c916475b353245a608255ed4a5770ebe","after":"0876c3f2692047e08e337d981ad3e182c8992a80","ref":"refs/heads/theory_separation","pushedAt":"2024-07-15T00:24:12.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"proved the first chunk of subst_induction","shortMessageHtmlLink":"proved the first chunk of subst_induction"}},{"before":"2b4c74b465dec39475b73dc8616184615b4e6141","after":"002de001c916475b353245a608255ed4a5770ebe","ref":"refs/heads/theory_separation","pushedAt":"2024-07-14T02:26:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"proved first chunk of subst induction","shortMessageHtmlLink":"proved first chunk of subst induction"}},{"before":"c7fabcc9881ab0612206d82adc44308e4fd5522a","after":"2b4c74b465dec39475b73dc8616184615b4e6141","ref":"refs/heads/theory_separation","pushedAt":"2024-07-13T17:38:48.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"138a5d3b871178e9f403882e981aba556ec59567","after":"c7fabcc9881ab0612206d82adc44308e4fd5522a","ref":"refs/heads/theory_separation","pushedAt":"2024-07-07T11:30:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"75b7721a660c49b178579be002d2f95b12a7535e","after":"138a5d3b871178e9f403882e981aba556ec59567","ref":"refs/heads/theory_separation","pushedAt":"2024-06-26T17:17:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"add statement for subst induction and use support instead of freshness","shortMessageHtmlLink":"add statement for subst induction and use support instead of freshness"}},{"before":"09799213022c1d54c018ad1aa093062780d4f7a2","after":"75b7721a660c49b178579be002d2f95b12a7535e","ref":"refs/heads/theory_separation","pushedAt":"2024-06-24T19:29:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"fixed nl core axioms","shortMessageHtmlLink":"fixed nl core axioms"}},{"before":"22a72a64b44924ddd18a78cc2eeaf720c3347bbc","after":"09799213022c1d54c018ad1aa093062780d4f7a2","ref":"refs/heads/theory_separation","pushedAt":"2024-06-12T22:29:00.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"definition of subst","shortMessageHtmlLink":"definition of subst"}},{"before":"e5cd00592844d30577a3399b9f9d670a88383253","after":"22a72a64b44924ddd18a78cc2eeaf720c3347bbc","ref":"refs/heads/theory_separation","pushedAt":"2024-04-01T19:20:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"rename induction principle","shortMessageHtmlLink":"rename induction principle"}},{"before":"6e073b7349f4e8e2b325188bcf336e60f4928a64","after":"e5cd00592844d30577a3399b9f9d670a88383253","ref":"refs/heads/theory_separation","pushedAt":"2024-04-01T19:06:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"fully proved induction principle","shortMessageHtmlLink":"fully proved induction principle"}},{"before":"11188bb858063039cad8903ee21e2c4ebb4fdd6b","after":"6e073b7349f4e8e2b325188bcf336e60f4928a64","ref":"refs/heads/theory_separation","pushedAt":"2024-03-22T15:24:35.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"rewitre inference rules added","shortMessageHtmlLink":"rewitre inference rules added"}},{"before":"e5085580e29dda7d1596f5d71d0b096c2d69756e","after":"11188bb858063039cad8903ee21e2c4ebb4fdd6b","ref":"refs/heads/theory_separation","pushedAt":"2024-03-22T13:24:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"one lemma left","shortMessageHtmlLink":"one lemma left"}},{"before":"1b3782b5b243b0d8141723343970309bad182348","after":"e5085580e29dda7d1596f5d71d0b096c2d69756e","ref":"refs/heads/theory_separation","pushedAt":"2024-03-06T11:15:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MirceaS","name":"Octavian Mircea Sebe","path":"/MirceaS","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5909705?s=80&v=4"},"commit":{"message":"cleanup","shortMessageHtmlLink":"cleanup"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xM1QwMjo1OTo1Mi4wMDAwMDBazwAAAAS1CNqR","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xM1QwMjo1OTo1Mi4wMDAwMDBazwAAAAS1CNqR","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMy0wNlQxMToxNTozMC4wMDAwMDBazwAAAAQN1_FP"}},"title":"Activity · Formal-Systems-Laboratory/matching-logic-mm0"}