diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 09:59:59 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 17:56:10 -0300 |
| commit | e92c8e00290bab8db328058c437b471c0f1671a4 (patch) | |
| tree | f4ff85923298f70b7e66c3ec8e9e780bab784d7b /docs/vm.org | |
| parent | c3b4c7aee1f0d4beb078938d330e982e752927a1 (diff) | |
| download | SOL-e92c8e00290bab8db328058c437b471c0f1671a4.tar.gz SOL-e92c8e00290bab8db328058c437b471c0f1671a4.zip | |
algebraic identities of plus and times discharge symbolically
Diffstat (limited to '')
| -rw-r--r-- | docs/vm.org | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/docs/vm.org b/docs/vm.org index a51b85a..d678acd 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -106,8 +106,11 @@ engine decides entailment algebraically. Every natural is at least zero: proven. Not every integer is: refuted, and the refutation is backed by a concrete counterexample. Every integer is a rational: proven, which is decision 12's subtype inclusion decided -symbolically. A universal outside that fragment is a non total plan, -rejected, as decision 10 requires. +symbolically. The unit identities of the numeric relations discharge +too: =[Plus left: X right: 0 result: X]= holds over all integers by +the algebra of =Plus=, in the flat membership form of decision 14, +and fails over strings, which do not add. A universal outside that +fragment is a non total plan, rejected, as decision 10 requires. * Membership criteria as domains |