#|
ACL2     !>(let*      ((foo     '(1     2     3     .      bar))
(alist  (list (cons 'bar foo))))
 (%cdrs 7 foo alist))
(2 3 . BAR)
ACL2 !>
Seven   steps   forwards    gets   us  to  one   step   forward,
semi-circularly. 

Glorious return to ACL2 game programming  (do you remember  last
time?) 

ldbeth  asked  after  seeing  my #1=(1  2 3 .  #1#) wzard   game
structure whether I could represent circular lists without sharp
quote syntax. Well
(let   ((foo   '(1  2  3)))  (setf  (cdr   (last   foo))   foo))
but one of the As in ACL2 is Applicative,  so we don't have SETF
neither 

so I have used an alist and not-true-listps  so when cdr returns
a     symbol     it     means     cdr-assoc      the      alist.
Since ACL2 enforces  single-threadedness,  I don't think there's
ever  a problem  except  for informality.   So  let's  add  some
formality. |#
(defun %cdrs (measure list alist)
(if (or (zp measure) (not (natp measure)))  list
(let ((next-measure  (- measure 1))
(next-list  (cdr (if (symbolp (cdr list))
 (assoc (cdr list) alist)
 list))))
 (%cdrs next-measure next-list alist))))

;;;We  don't  have  to  worry  about  SETFability   since  we're
applicative. 

;;;I'm figuring...  If it's a true list, %cdrs 1 is trivial  and
%cdrs n is (%cdrs (1- n) (%cdrs 1 list alist) alist) to get some
recursion going.

(defthm stepwise-nil-alist-%cdrs
(implies  (and (listp list) (equal alist nil) (equal n (length
list)))  (equal  (%cdrs  n list alist)  (%cdrs  1 (%cdrs  (1- n)
list alist) alist)))) 

;;;Since   we can reach  the end of a list  one step  at a  time
;;;can   we get from  what  I seem to have  called  (cons  b  e)
;;;to (cons e d) in the continuation alist?

(defthm last-cdr-symbol
(implies (and (symbolp  e) (equal list (append a (cons b e)))
(equal  alist (list (cons e d))))
 (equal (%cdrs 1 (last list) alist) d)))

;;;So  we can mostly get through one im/proper  list, but can we
get to the next? 

(defthm composite-%cdrs
(implies (and (listp a) (listp b) (not (null b)) (symbolp  foo)
(not (null foo)) (equal  list (append  a (cons whatever   foo)))
(equal alist (list (cons foo b))) (equal n (length  list)))
 (equal (%cdrs n list alist) b)))

;;;There's    (always)   more  to  do  but  it  seems  like  our
faux-circularity is working. ;;;Oh that's actually equivalent to
the last one I guess.   Actually  all of them ;;;were   trivial.
#|
It took  me a while  to be able  to write  anything  at all acl2
would  accept  from me. Then I got back into the zone  of mostly
saying    trivial   things.    The   automated    prover    took
111      steps     for     the     admission      of      %cdrs,
2620 steps for STEPWISE-NIL-ALIST-%CDRS
1093 steps for LAST-CDR-SYMBOL
and
1778 for composite-%cdrs

I feel very efficient when my machine does thousands  of  things
for me.
|#