Applicative game media now instantiated.  I started with three goals in mind
for  media:   Must be able to play sound,  must be convenient  to  structure
complex  autostereogram  illusions, and must be convenient for plain text as
well.  To this end I have selected  common lisp (duh) format control strings
and arguments  as my universal media control.  It is a complete  programming
language built around pretty printing. Because it can do anything, sound and
complex  lispy post-processing  are easy. A simple convention  and say, SDL2
will also let me drive pixel mapped  graphics  via format control strings in
the future too. ACL2 is not suitable itself for media side effects. Its role
is constrained  to proving the applicative  logic of the game's state to the
media representation  namely the format controls and their arguments.  Let's
look at my tictacto,  though  it could  also be baduk which would  be cooler
actually.    The game will be expressed  as a proven  (in some senses)  acl2
applicative  function on a list stored in a single threaded object, followed
by a normal lisp - sbcl - evaluating  acl2's media output.

ACL2 !> (new-game game-state)
<game-state>
ACL2 !> (fmt-game game-state)
(FORMAT T "~{~a~a~a~%~a~a~a~%~a~a~a~%~}"
        '(#\. #\. #\. #\. #\. #\. #\. #\. #\.))
;;Over in sbcl's *
* (FORMAT T "~{~a~a~a~%~a~a~a~%~a~a~a~%~}"
         '(#\. #\. #\. #\. #\. #\. #\. #\. #\.))
...
...
...
NIL
ACL2 !>(play-x game-state 1 1)
<game-state>
ACL2 !>(play-o game-state 0 2)
<game-state>
ACL2 !>(fmt-game game-state)
(FORMAT T "~{~a~a~a~%~a~a~a~%~a~a~a~%~}"
        '(#\. #\. #\. #\. #\x #\. #\o #\. #\.))
* (FORMAT T "~{~a~a~a~%~a~a~a~%~a~a~a~%~}"
         '(#\. #\. #\. #\. #\x #\. #\o #\. #\.))

...
.x.
o..
NIL

Clearly I can maintain state in the game-state single threaded object, and I
allege  deterministically   produce a common lisp format  expression   media
depiction  of the game state  evaluable to some literal media which  in this
case is a three  by three  game board that gets hugged and kissed.   Text is
convenient  here and always,  but all sorts of media control is possible and
fairly convenient. 
On  the  topic  of  ACL2 particularly,  you might  notice  that  my  measure
conjectures  are always trivial, and the way I have expressed myself has not
required any lemmas or particular  rewrite rules from me. I think it is good
that my robot  team mate needs  relatively  little  input  from me.  I  will
revisit  this towards the end of this post.  For now, let me present my ACL2
logic. 
;;Same everything as before; I am noting game-state here since it is used.
(defstobj game-state
   (sparse-objects :type t :initially nil)
   (subject-cursor :type integer :initially 0)
   (object-cursor :type integer :initially 0)
   (chars-in :type t :initially nil))

;;The test world of tictacto/a very unfair baduk totally explicitly
(defun new-tictacto-board ()
 '(((row . 0) (col . 0) (fmt-ctl . "~a") (fmt-args . (#\.)))
   ((row . 1) (col . 0) (fmt-ctl . "~a") (fmt-args . (#\.)))
   ((row . 2) (col . 0) (fmt-ctl . "~a~%") (fmt-args . (#\.)))
   ((row . 0) (col . 1) (fmt-ctl . "~a") (fmt-args . (#\.)))
   ((row . 1) (col . 1) (fmt-ctl . "~a") (fmt-args . (#\.)))
   ((row . 2) (col . 1) (fmt-ctl . "~a~%") (fmt-args . (#\.)))
   ((row . 0) (col . 2) (fmt-ctl . "~a") (fmt-args . (#\.)))
   ((row . 1) (col . 2) (fmt-ctl . "~a") (fmt-args . (#\.)))
   ((row . 2) (col . 2) (fmt-ctl . "~a~%") (fmt-args . (#\.)))))

;;Transform the game sparse objects (actually dense here) into a lisp format 
(defun get-lisp-format (input fmt-ctls fmt-args)
 (if (= 0 (length input)) `(format t ,(concatenate 'string "~{" fmt-ctls "~}") ',fmt-args)
  (get-lisp-format (cdr input)
   (concatenate 'string fmt-ctls (cdr (assoc 'fmt-ctl (car input))))
   (append fmt-args (cdr (assoc 'fmt-args (car input)))))))

;;Change the character displayed without changing the control string,
;;By prepending a new fmt-args since lisp/acl2's assoc only finds 
;;first matches. Yes this function is terribly named.
(defun row-col2char (row col char input output)
 (if (= 0 (length input)) output
  (let ((pushp (if (subsetp-equal `((row . ,row) (col . ,col)) (car input))
                `((fmt-args . (,char)))
                nil)))
   (row-col2char row col char (cdr input)
    (append output (list (append pushp (car input))))))))
;;That was everything functional, onto

;;;game-state
;;I'm not trying to prove I have handled every side-effect error scenario with my stobj
;;Hence I am declaring verify-guards to nil for stateful functions here.
(defun new-game (game-state)
 (declare (xargs :stobjs (game-state) :verify-guards nil))
 (update-sparse-objects (new-tictacto-board) game-state))

(defun fmt-game (game-state)
 (declare (xargs :stobjs (game-state) :verify-guards nil))
 (get-lisp-format (sparse-objects game-state) "" nil))

(defun play-x (game-state row col)
 (declare (xargs :stobjs (game-state) :verify-guards nil))
 (let* ((board (sparse-objects game-state))
        (new-board (row-col2char row col #\x board nil)))
  (update-sparse-objects new-board game-state)))

(defun play-o (game-state row col)
 (declare (xargs :stobjs (game-state) :verify-guards nil))
 (let* ((board (sparse-objects game-state))
        (new-board (row-col2char row col #\o board nil)))
  (update-sparse-objects new-board game-state)))

Easy easy easy.  The trouble  I mentioned yesterday  is not visible anywhere
because I decided to just use a simple element by element O(n) filtering  of
an input list into an output list for everything. What I had been working on
was pulling out subsequences relying on some well-ordering I will look at in
a moment complicated  by col-min and col-max not necessarily being the edges
of a row. Anyway, everything is pretty great now without even trying.
I keep saying common lisp format can and is appropriate  for arbitrary media
because   it furnishes  arbitrary  functionality  like this (on top  of  its
iteration,  gotos, logic and so on):
(in-package cl-user)
(defun beep-if-true (stream bool-arg &rest flags)
 (declare (ignore flags))
 (format stream "~@[~1@*~]" bool-arg #\Bel))

(format t "~/cl-user::beep-if-true/" t)
(format t "~/cl-user::beep-if-true/" nil)

					;I assume my hacky scripting and 
					;typos achieved the following

which is normally used to craft a response to put into the stream at the

function  call position, but does not necessarily  have to.  For example  it
could enqueue  post processing  of the output,  or drive Simple  Directmedia
Layer 2 through ecl's sffi. 
Something I did not end up using explicitly in this example is that I

modified  my insertion  sort from before  to sort lists  having  row and col
conses in row-major order. The only change was this:

(defun leq-pushp (a b)
 (let ((row-a (cdr (assoc 'row a)))
       (row-b (cdr (assoc 'row (car b))))
       (col-a (cdr (assoc 'col a)))
       (col-b (cdr (assoc 'col (car b)))))
  (cond
   ((< row-a row-b) (append (list a) b))
   ((and (= row-a row-b)
         (<= col-a col-b)) (append (list a) b))
   (t nil))))

which, accepted trivially, did not change the logic of my acl2

'insert-sorted    or  'insertion-sort.    By  always  being  sorted  through
'insert-sorted 

(defun insert-sorted (a b result)
 (if (= 0 (length b)) (append result (list a))
  (let ((final-tail (leq-pushp a b)))
   (if final-tail (append result final-tail)
    (insert-sorted a (cdr b) (append result (list (car b))))))))

I trivially avoid lots of pathological cases. The reason that I have not had

any lemmas or fiddly rewrite  rules so far is that I am not proving any very
strong theorems. Regarding insertion  sort

(defun insertion-sort (input result)
 (if (= 0 (length input)) result
  (insertion-sort (cdr input)
   (insert-sorted (car input) result nil))))

I checked weak theorems like

(thm (implies (< (cdr (assoc 'row a)) (cdr (assoc 'row b)))
      (= (search (list a) (insertion-sort (list a b) nil))
       0)))

or in English, if I 'insertion-sort (list a b) and a's row is less than b's,
a is in position  0.  The usual stronger theories of a sorting function  are
that  the output is in fact sorted,  and that the output is some permutation
of the input.  I think a weak theory like- in this kind of scenario,  a will
be in position  0 is often  useful on its own. These  weak theories  are not
usually worth lodging as rewrite rules. When I was thumbing  through an ACL2
book, I found the book's insertion sort example, which required proving some
supporting  lemmas  in order to admit the function.  My form didn't need any
though. 
The next two things I want for a game, being a notion of a clock and network
multiplayer are mostly about side effects. I de finitely need some healthier
networking. I will develop a clock and some networking on other topics, then
introduce them to my theory of games afterwards.
---
Post script
Ultimately I expect to do: acl2 -> ecl -> sdl2 executable preserving the 
logic of acl2.