diff --git a/oMiser/obaptheory.txt b/oMiser/obaptheory.txt
index 40075d4..a2e6f18 100644
--- a/oMiser/obaptheory.txt
+++ b/oMiser/obaptheory.txt
@@ -1,4 +1,4 @@
-obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
+obaptheory.txt 0.1.3                UTF-8                       dh:2023-07-13
 ----|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
 
                           MISER THEORETICAL CONCEPTION
@@ -92,7 +92,7 @@ obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
           The last five constitute special forms in the evaluation of obs as
           expressions of scripts.
 
-          For simplicity of expression, the CFob notation for fixed
+          For simplicity of expression, the CFob notation for primitive
           individuals uses the name with only the prefix ".".  For example,
           .NIL, .A, and .SELF.
 
@@ -114,7 +114,9 @@ obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
           IMPLEMENTATION NOTE: In computer representations, the alphanumeric
           characters permitted in lindies are Unicode glyphs, encoded in
           UTF-8, in the form of XML Names without any "." and ":" characters
-          [XML10:2.3 Common Syntactic Constructs, Names and Tokens].
+          [XML10:2.3 Common Syntactic Constructs, Names and Tokens].  It is
+          also permissible for "s" to begin with a numeral and to be entirely
+          numerical.  The only feature of lindies is their differentiation.
 
           Ʃ's' = Ʃ't' ⇔ s Ʃ= t
              where s Ʃ= t signifies identity of the string texts
@@ -126,7 +128,7 @@ obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
           Plain lindies are distinct conveniently-named individuals that have
           no intrinsic significance.  They are available to applications of
           obs for any purpose as distinct literals, written in Ot forms
-          Ʃ'alpha', Ʃ'ABCs', Ʃ'letterQ', Ʃ'foo', etc.
+          Ʃ'alpha', Ʃ'ABCs', Ʃ'letterQ', Ʃ'foo', Ʃ'4', Ʃ'005', etc.
 
           obap.is-lindy(x) => is-pure-lindy-trace(x)                 (b)
 
@@ -135,6 +137,9 @@ obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
 
           ¬ is-pure-lindy-trace(ob.e(x))                             (d)
 
+          is-pure-lindy-trace(x :: ob.NIL)                           (e)
+             ⇔ is-pure-lindy-trace(x)
+
           Applications of lindies to operands in scripts cannot proceed
           further; there is no intrinsic interpretation for application.
           Instead, application is defined to yield a trace form, an
@@ -177,6 +182,8 @@ obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
                 ⇒ obap.ap(p,x) = p :: ob.e(x)
           Pure lindy forms are resolved to trace forms in this manner to
           be more informative on inspection when the occurence is unintended.
+          There is also an intended usage of pure lindy traces as a form of
+          text expression.
 
         ¬ is-pure-lindy-trace(p)                                     (d)
                 => ob.is-pair(p) ⇒ obap.ap(p,x) = ev(p,x,p)
@@ -255,7 +262,7 @@ obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
 
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
 
-                  Copyright 2017-2022 Dennis E. Hamilton
+                  Copyright 2017-2023 Dennis E. Hamilton
 
     Licensed under the Apache License, Version 2.0 (the "License");
     you may not use this file except in compliance with the License.
@@ -274,7 +281,7 @@ obaptheory.txt 0.1.2                UTF-8                       dh:2022-08-11
  ATTRIBUTION
 
    Hamilton, Dennis E. ‹ob› Universal Applicative Functions.  Miser Theory
-   Conception text file obaptheory.txt version 0.1.2 dated 2022-08-11,
+   Conception text file obaptheory.txt version 0.1.3 dated 2023-07-13,
    available on the Internet as a version of
    <https://github.com/orcmid/miser/blob/master/oMiser/obaptheory.txt>
 
@@ -312,15 +319,19 @@ TODO
  * The determination of trace forms is the oMiser approach to handling of
    undefined situations.  There is no exception mechanism at the oMiser level
    and it is common for an operation to simply return an unmodified object
-   as a trace instead of any further result evaluation.
+   as a trace instead of any further result evaluation.  A consequence is that
+   there is use as a hack for symbolic execution and for interpretation of
+   pure lindy traces as text structures that can be treated as strings.
 
- * In Obap4(c) determine whether such a result should be viewed as a pure-
-   lindy in any chain and whether there is any benefit of chaining/stacking
-   or whatever the use of space-separated lindies will be called.  This has
-   to be worked out in CFob.txt also.
+ * It is desirable for output containing pure trace forms be presentable in
+   applicative rather than pairing ('::') form.  This should be either an
+   option or simply the way of doing this sort of thing.  Then presenting
+   list [x,y, ...] forms also needs to be considered.  Oh my.
 
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
 
+ 0.1.3  2023-07-13T19:41Z Tidy up around pure lindy trace forms to enable
+        output variation and interpretation as text structures.
  0.1.2  2022-08-11T20:27Z Touch-ups and review of pure-lindy case
  0.1.1  2022-08-01T20:49Z Refer now to oFrugal/ob-exp.txt
  0.1.0  2022-01-04T01:10Z Introduce the conditional lindies to satisfy the