Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c	(revision 7972603ba78a3b2d7041e7208a3c3be2479d2b37)
+++ 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: //
