SOL/test/test_vm.ml, branch masteralgebraic identities of plus and times discharge symbolically2026-07-12T20:56:10+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-12T12:59:59+00:00e92c8e00290bab8db328058c437b471c0f1671a4
symbolic discharge: universals over infinite domains decided by intervals2026-07-12T03:35:33+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-12T03:35:33+00:007aacf596d73cc74eb9af381a72723b50b4069e30
mutual recursion admitted under lexicographic measures2026-07-12T02:39:40+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-12T02:39:40+00:00726f3dfb116ec9265041e642000612831633fe3c
world relation as the universe for scoped negation2026-07-12T01:13:33+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-12T01:13:33+00:005d967951eb0b08c36ee59f70d7f4cca37b0ca72b
residuation: open membership returns residual constraints2026-07-12T01:12:53+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-12T01:12:53+00:000886f3c71cf8551e4f8b3726654003a4f29645f0
admission runs the containment checker extracted from rocq2026-07-12T01:03:21+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-12T01:03:21+00:00f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507
embedding surface, host world test, deep recursion, line tracking2026-07-11T06:17:10+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-11T06:17:10+00:00eb81c07047979f3fe53383ff2a42393f0b29bd28
negation, quantifiers and membership criteria as schema domains2026-07-11T06:15:25+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-11T06:15:25+00:0040376c3ea009eab4db9ba27837e61d8bec310b8f
working vm: parser, admission with totality checks, solver and repl2026-07-11T06:07:56+00:00Marcos Maguetamaguetamarcos@gmail.com2026-07-11T06:07:56+00:00c530682030e80ee2de2c263471e5eda7a3392e84