Index: doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c	(revision e72fc60c45c40f15ed2eb81b8f581c866cf011dc)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c	(revision 266732e2818527a06669f666f04fb32c296a3b9f)
@@ -10,49 +10,15 @@
 
 int main() {
+	float * x;			$\C{// x points at a floating-point number}$
+	void (*y)(void);	$\C{// y points at a function}$
+	@x = y;@			$\C{// wrong}$
+	@y = x;@			$\C{// wrong}$
 
-/*
-    These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
-*/
-    float * x;         // x points at a floating-point number
-    void (*y)(void);   // y points at a function
-                       ERR(
-    x = y;             // wrong
-    y = x;             // wrong
-                       )
+	float pi = 3.14;
+	void f( void (*g)(void) ) { g(); }
+	@f( &pi );@			$\C{// wrong}$
+}
 
-/*
-    The first gets
-        warning: assignment to `float *' from incompatible pointer type `void (*)(void)'
-    and the second gets the opposite.
-
-    Similarly,
-*/
-
-    float pi = 3.14;
-    void f( void (*g)(void) ) {
-        g();
-    }
-                       ERR(
-    f( & pi );         // wrong
-                       )
-/*
-    gets
-        warning: passing argument 1 of `f' from incompatible pointer type
-    with a segmentation fault at runtime.
-
-    That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@.
-    Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition.
-
-    A "tractable syntactic method for proving the absence of certain program behaviours
-    by classifying phrases according to the kinds of values they compute"*1
-    rejected the program.  The behaviour (whose absence is unprovable) is neither minor nor unlikely.
-    The rejection shows that the program is ill-typed.
-
-    Yet, the rejection presents as a GCC warning.
-
-    In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing.
-
-    *1  TAPL-pg1 definition of a type system
-*/
-
-}
+// Local Variables: //
+// compile-command: "sed -f sedcmd bkgd-c-tyerr.c > tmp.c; gcc tmp.c" //
+// End: //
Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c	(revision e72fc60c45c40f15ed2eb81b8f581c866cf011dc)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c	(revision 266732e2818527a06669f666f04fb32c296a3b9f)
@@ -24,172 +24,117 @@
 
 
-    // SHOW(sizeof( a   ), "%zd");
-    // SHOW(sizeof(&a   ), "%zd");
-    // SHOW(sizeof( a[0]), "%zd");
-    // SHOW(sizeof(&a[0]), "%zd");
+	// SHOW(sizeof( a   ), "%zd");
+	// SHOW(sizeof(&a   ), "%zd");
+	// SHOW(sizeof( a[0]), "%zd");
+	// SHOW(sizeof(&a[0]), "%zd");
 
 
 
 int main() {
+	float a[10];
+	static_assert(sizeof(float) == 4);		$\C{// floats (array elements) are 4 bytes}$
+	static_assert(sizeof(void*) == 8);		$\C{// pointers are 8 bytes}$
+	static_assert(sizeof(a) == 40);			$\C{// array}$
+	static_assert(sizeof(&a) == 8 );		$\C{// pointer to array}$
+	static_assert(sizeof(a[0]) == 4 );		$\C{// first element}$
+	static_assert(sizeof(&(a[0])) == 8 );	$\C{// pointer to first element}$
 
-/*
-When a programmer works with an array, C semantics provide access to a type that is different in every way from ``pointer to its first element.''
+	typeof(&a) x;							$\C{// x is pointer to array}$
+	typeof(&(a[0])) y;						$\C{// y is pointer to first element}$
+	@x = y;@								$\C{// ill-typed}$
+	@y = x;@								$\C{// ill-typed}$
+	static_assert(sizeof(typeof(a)) == 40);
+	static_assert(sizeof(typeof(&a)) == 8 );
+	static_assert(sizeof(typeof(a[0])) == 4 );
+	static_assert(sizeof(typeof(&(a[0]))) == 8 );
 
-Its qualities become apparent by inspecting the declaration
-*/
-    float a[10];
-/*
+	void f( float (*pa)[10] ) {
+	    static_assert(sizeof(   *pa     ) == 40); $\C{// array}$
+	    static_assert(sizeof(    pa     ) == 8 ); $\C{// pointer to array}$
+	    static_assert(sizeof(  (*pa)[0] ) == 4 ); $\C{// first element}$
+	    static_assert(sizeof(&((*pa)[0])) == 8 ); $\C{// pointer to first element}$
+	}
+	f( & a );
 
-The inspection begins by using @sizeof@ to provide definite program semantics for the intuition of an expression's type.
+	float fs[] = {3.14, 1.707};
+	char cs[] = "hello";
 
-Assuming a target platform keeps things concrete:
-*/
-    static_assert(sizeof(float)==4);    // floats (array elements) are 4 bytes
-    static_assert(sizeof(void*)==8);    // pointers are 8 bytes
-/*
-
-Consider the sizes of expressions derived from @a@, modified by adding ``pointer to'' and ``first element'' (and including unnecessary parentheses to avoid confusion about precedence).
-*/
-    static_assert(sizeof(  a    ) == 40); // array
-    static_assert(sizeof(& a    ) == 8 ); // pointer to array
-    static_assert(sizeof(  a[0] ) == 4 ); // first element
-    static_assert(sizeof(&(a[0])) == 8 ); // pointer to first element
-/*
-That @a@ takes up 40 bytes is common reasoning for C programmers.
-Set aside for a moment the claim that this first assertion is giving information about a type.
-For now, note that an array and a pointer to its first element are, sometimes, different things.
-
-The idea that there is such a thing as a pointer to an array may be surprising.
-It is not the same thing as a pointer to the first element:
-*/
-    typeof(& a    ) x;   // x is pointer to array
-    typeof(&(a[0])) y;   // y is pointer to first element
-                       ERR(
-    x = y;             // ill-typed
-    y = x;             // ill-typed
-                       )
-/*
-The first gets
-    warning: warning: assignment to `float (*)[10]' from incompatible pointer type `float *'
-and the second gets the opposite.
-*/
-
-/*
-We now refute a concern that @sizeof(a)@ is reporting on special knowledge from @a@ being an local variable,
-say that it is informing about an allocation, rather than simply a type.
-
-First, recognizing that @sizeof@ has two forms, one operating on an expression, the other on a type, we observe that the original answers are unaffected by using the type-parameterized form:
-*/
-    static_assert(sizeof(typeof(  a    )) == 40);
-    static_assert(sizeof(typeof(& a    )) == 8 );
-    static_assert(sizeof(typeof(  a[0] )) == 4 );
-    static_assert(sizeof(typeof(&(a[0]))) == 8 );
-
-/*
-Finally, the same sizing is reported when there is no allocation at all, and we launch the analysis instead from the pointer-to-array type.
-*/
-    void f( float (*pa)[10] ) {
-        static_assert(sizeof(   *pa     ) == 40); // array
-        static_assert(sizeof(    pa     ) == 8 ); // pointer to array
-        static_assert(sizeof(  (*pa)[0] ) == 4 ); // first element
-        static_assert(sizeof(&((*pa)[0])) == 8 ); // pointer to first element
-    }
-    f( & a );
-
-/*
-So, in spite of considerable programmer success enabled by an understanding that
-an array just a pointer to its first element (revisited TODO pointer decay),
-this understanding is simplistic.
-*/
-
-/*
-A shortened form for declaring local variables exists, provided that length information is given in the initializer:
-*/
-    float fs[] = {3.14, 1.707};
-    char cs[] = "hello";
-
-    static_assert( sizeof(fs) == 2 * sizeof(float) );
-    static_assert( sizeof(cs) == 6 * sizeof(char) );  // 5 letters + 1 null terminator
-
-/*
-In these declarations, the resulting types are both arrays, but their lengths are inferred.
-*/
-
+	static_assert( sizeof(fs) == 2 * sizeof(float) );
+	static_assert( sizeof(cs) == 6 * sizeof(char) );  $\C{// 5 letters + 1 null terminator}$
 }
 
+void syntaxReferenceCheck(void) {
+	// $\rightarrow$ & (base element)
+	//     & @float@ 
+	//     & @float x;@ 
+	//     & @[ float ]@
+	//     & @[ float ]@
+	float x0;
 
-void syntaxReferenceCheck(void) {
-    // $\rightarrow$ & (base element)
-    //     & @float@ 
-    //     & @float x;@ 
-    //     & @[ float ]@
-    //     & @[ float ]@
-    float x0;
+	// $\rightarrow$ & pointer
+	//     & @float *@ 
+	//     & @float * x;@ 
+	//     & @[ * float ]@
+	//     & @[ * float ]@
+	float * x1;
 
-    // $\rightarrow$ & pointer
-    //     & @float *@ 
-    //     & @float * x;@ 
-    //     & @[ * float ]@
-    //     & @[ * float ]@
-    float * x1;
+	// $\rightarrow$ & array 
+	//     & @float[10]@ 
+	//     & @float x[10];@ 
+	//     & @[ [10] float ]@
+	//     & @[ array(float, 10) ]@
+	float x2[10];
 
-    // $\rightarrow$ & array 
-    //     & @float[10]@ 
-    //     & @float x[10];@ 
-    //     & @[ [10] float ]@
-    //     & @[ array(float, 10) ]@
-    float x2[10];
+	typeof(float[10]) x2b;
 
-    typeof(float[10]) x2b;
-
-    // & array of pointers
-    //     & @(float*)[10]@
-    //     & @float *x[10];@
-    //     & @[ [10] * float ]@
-    //     & @[ array(*float, 10) ]@
-    float *x3[10];
+	// & array of pointers
+	//     & @(float*)[10]@
+	//     & @float *x[10];@
+	//     & @[ [10] * float ]@
+	//     & @[ array(*float, 10) ]@
+	float *x3[10];
 //    (float *)x3a[10];  NO
 
-    // $\rightarrow$ & pointer to array
-    //     & @float(*)[10]@
-    //     & @float (*x)[10];@
-    //     & @[ * [10] float ]@
-    //     & @[ * array(float, 10) ]@
-    float (*x4)[10];
+	// $\rightarrow$ & pointer to array
+	//     & @float(*)[10]@
+	//     & @float (*x)[10];@
+	//     & @[ * [10] float ]@
+	//     & @[ * array(float, 10) ]@
+	float (*x4)[10];
 
-    // & pointer to array
-    //     & @(float*)(*)[10]@
-    //     & @float *(*x)[10];@
-    //     & @[ * [10] * float ]@
-    //     & @[ * array(*float, 10) ]@
-    float *(*x5)[10];
-    x5 =     (float*(*)[10]) x4;
+	// & pointer to array
+	//     & @(float*)(*)[10]@
+	//     & @float *(*x)[10];@
+	//     & @[ * [10] * float ]@
+	//     & @[ * array(*float, 10) ]@
+	float *(*x5)[10];
+	x5 =     (float*(*)[10]) x4;
 //    x5 =     (float(*)[10]) x4;  // wrong target type; meta test suggesting above cast uses correct type
 
-    // [here]
-    // const
+	// [here]
+	// const
 
-    // [later]
-    // static
-    // star as dimension
-    // under pointer decay:                int p1[const 3]  being  int const *p1
+	// [later]
+	// static
+	// star as dimension
+	// under pointer decay:                int p1[const 3]  being  int const *p1
 
-    const float * y1;
-    float const * y2;
-    float * const y3;
+	const float * y1;
+	float const * y2;
+	float * const y3;
 
-    y1 = 0;
-    y2 = 0;
-    // y3 = 0; // bad
+	y1 = 0;
+	y2 = 0;
+	// y3 = 0; // bad
 
-    // *y1 = 3.14; // bad
-    // *y2 = 3.14; // bad
-    *y3 = 3.14;
+	// *y1 = 3.14; // bad
+	// *y2 = 3.14; // bad
+	*y3 = 3.14;
 
-    const float z1 = 1.414;
-    float const z2 = 1.414;
+	const float z1 = 1.414;
+	float const z2 = 1.414;
 
-    // z1 = 3.14; // bad
-    // z2 = 3.14; // bad
+	// z1 = 3.14; // bad
+	// z2 = 3.14; // bad
 
 
@@ -199,6 +144,10 @@
 void stx2() { const T x[10];
 //            x[5] = 3.14; // bad
-            }
+	        }
 void stx3() { T const x[10];
 //            x[5] = 3.14; // bad
-            }
+	        }
+
+// Local Variables: //
+// compile-command: "sed -f sedcmd bkgd-carray-arrty.c > tmp.c; gcc tmp.c" //
+// End: //
Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c	(revision e72fc60c45c40f15ed2eb81b8f581c866cf011dc)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c	(revision 266732e2818527a06669f666f04fb32c296a3b9f)
@@ -1,111 +1,47 @@
 #include <assert.h>
 int main() {
+	float a[10];				$\C{// array}$
+	float (*pa)[10] = &a;		$\C{// pointer to array}$
+	float a0 = a[0];			$\C{// element}$
+	float *pa0 = &(a[0]);		$\C{// pointer to element}$
 
-/*
-The last section established the difference between these four types:
-*/
+	float *pa0x = a;			$\C{// (ok)}$
+	assert( pa0 == pa0x );
+	assert( sizeof(pa0x) != sizeof(a) );
 
-    float    a  [10] ;          // array
-    float (*pa )[10] = & a    ; // pointer to array
-    float    a0      =   a[0] ; // element
-    float  *pa0      = &(a[0]); // pointer to element
+	void f( float x[10], float *y ) {
+		static_assert( sizeof(x) == sizeof(void*) );
+		static_assert( sizeof(y) == sizeof(void*) );
+	}
+	f(0,0);
 
-/*
-But the expression used for obtaining the pointer to the first element is pedantic.
-The root of all C programmer experience with arrays is the shortcut
-*/
-    float  *pa0x     =   a    ; // (ok)
-/*
-which reproduces @pa0@, in type and value:
-*/
-    assert( pa0 == pa0x );
-/*
-The validity of this initialization is unsettling, in the context of the facts established in the last section.
-Notably, it initializes name @pa0x@ from expression @a@, when they are not of the same type:
-*/
-    assert( sizeof(pa0x) != sizeof(a) );
+	// reusing local var `float a[10];`}
+	float v;
+	f(  a,  a ); $\C{// ok: two decays, one into an array spelling}$
+	f( &v, &v ); $\C{// ok: no decays; a non-array passes to an array spelling}$
 
+	char ca[] = "hello";    $\C{// array on stack, initialized from read-only data}$
+	char *cp = "hello";     $\C{// pointer to read-only data [decay here]}$
+	void edit(char c[]) {   $\C{// param is pointer}$
+		c[3] = 'p';
+	}
+	edit(ca);               $\C{// ok [decay here]}$
+	edit(cp);               $\C{// Segmentation fault}$
+	edit("hello");          $\C{// Segmentation fault [decay here]}$
 
+	void decay( float x[10] ) {
+		static_assert( sizeof(x) == sizeof(void*) );
+	}
+	static_assert( sizeof(a) == 10 * sizeof(float) );
+	decay(a);
 
+	void no_decay( float (*px)[10] ) {
+		static_assert( sizeof(*px) == 10 * sizeof(float) );
+	}
+	static_assert( sizeof(*pa) == 10 * sizeof(float) );
+	no_decay(pa);
+}
 
-
-
-
-
-
-
-
-
-
-    void f( float x[10], float *y ) {
-        static_assert( sizeof(x) == sizeof(void*) );
-        static_assert( sizeof(y) == sizeof(void*) );
-    }
-    f(0,0);
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-    // reusing local var `float a[10];`
-    float v;
-    f(  a,  a ); // ok: two decays, one into an array spelling
-    f( &v, &v ); // ok: no decays; a non-array passes to an array spelling
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-    char ca[] = "hello";    // array on stack, initialized from read-only data
-    char *cp = "hello";     // pointer to read-only data [decay here]
-    void edit(char c[]) {   // param is pointer
-        c[3] = 'p';
-    }
-    edit(ca);               // ok [decay here]
-    edit(cp);               // Segmentation fault
-    edit("hello");          // Segmentation fault [decay here]
-
-
-
-
-
-
-
-
-
-
-
-
-    void decay( float x[10] ) {
-        static_assert( sizeof(x) == sizeof(void*) );
-    }
-    static_assert( sizeof(a) == 10 * sizeof(float) );
-    decay(a);
-
-    void no_decay( float (*px)[10] ) {
-        static_assert( sizeof(*px) == 10 * sizeof(float) );
-    }
-    static_assert( sizeof(*pa) == 10 * sizeof(float) );
-    no_decay(pa);
-}
+// Local Variables: //
+// compile-command: "sed -f sedcmd bkgd-carray-decay.c > tmp.c; gcc tmp.c" //
+// End: //
Index: doc/theses/mike_brooks_MMath/programs/sedcmd
===================================================================
--- doc/theses/mike_brooks_MMath/programs/sedcmd	(revision 266732e2818527a06669f666f04fb32c296a3b9f)
+++ doc/theses/mike_brooks_MMath/programs/sedcmd	(revision 266732e2818527a06669f666f04fb32c296a3b9f)
@@ -0,0 +1,3 @@
+s/@//g
+s/\$\\C{//g
+s/}\$//g