decision 14: no application in term position, spec example rewritten flat

1 files changed, 11 insertions, 3 deletions

diff --git a/docs/language-specification.org b/docs/language-specification.org
index 9158130..639e8d6 100644
--- a/docs/language-specification.org
+++ b/docs/language-specification.org
@@ -1152,12 +1152,20 @@ For example:
 #+BEGIN_SRC sol
 [ForAll variable: X
         quantifier: [Integer value: X]
-        body:
-          [Equal left: [Plus left: X right: 0] right: X]]
+        body: [Plus left: X right: 0 result: X]]
 #+END_SRC
 
+This says that the tuple ={left: X, right: 0, result: X}= belongs to
+=Plus= for every integer =X=: the identity law stated as membership.
+Note what it is not written as: =[Equal left: [Plus left: X right: 0]
+right: X]=, with an application nested in term position. That form is
+rejected. A block is a proposition, never a value; treating it as a
+value would require privileging one attribute as "the" result, and a
+relation has no distinguished output. The flat membership form is
+both the honest one and the shorter one.
+
 This should be proved symbolically, by the algebraic properties of
-=Plus= and =Equal=, not by checking every integer.
+=Plus=, not by checking every integer.
 
 If Sol cannot prove such a universal symbolically, it must reject the
 program, keep it as an unproven obligation, or require an explicit