diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 00:35:33 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 00:35:33 -0300 |
| commit | 7aacf596d73cc74eb9af381a72723b50b4069e30 (patch) | |
| tree | 6970478e0866167285dc15820812b464407b75cb /docs/virtual-machine-specification.org | |
| parent | 6520b876af064d57bccf944a6fef9807a8c79de5 (diff) | |
| download | SOL-7aacf596d73cc74eb9af381a72723b50b4069e30.tar.gz SOL-7aacf596d73cc74eb9af381a72723b50b4069e30.zip | |
symbolic discharge: universals over infinite domains decided by intervals
Diffstat (limited to '')
| -rw-r--r-- | docs/virtual-machine-specification.org | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org index 828bc3c..f84bc84 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -135,9 +135,10 @@ without changing admitted semantics: one-sided comparisons; difference constraints between variables, arithmetic relations, and propagation through record structure are the next strengths; -- symbolic discharge: algebraic evidence for universals over - infinite domains, and arithmetic decrease measures for recursion - that structural containment cannot see; +- symbolic discharge beyond the interval fragment: algebraic + identities of relations (universals mentioning =Plus= and kin), + and arithmetic decrease measures for recursion that structural + containment cannot see; - Rocq certificates as admission evidence, and extraction of the lexicographic search itself (the containment core is already extracted); |