#!/bin/sh

acl2 <<"EOG"
(include-book "car-game")
(in-package "ACL2-USER")

(defstobj game-state (gamealist :type t :initially nil))
(update-gamealist (fill-grid (reset nil) 2 3) game-state)

(defthm one-finite-row-length
 (implies (and (equal n 3) (equal start-alist (reset nil))
               (equal game-alist (fill-grid start-alist n 1))
               (equal nodes (cdr (assoc 'nodes game-alist))))
  (equal (length nodes) n)))
"EOG"