#!/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"

You are viewing proxied material from sdf.org. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.