1
#|-*-Lisp-*-=================================================================|#
3
#| coi: Computational Object Inference |#
5
#|===========================================================================|#
1
; Computational Object Inference
2
; Copyright (C) 2005-2014 Kookamara LLC
7
; 11410 Windermere Meadows
8
; Austin, TX 78759, USA
9
; http://www.kookamara.com/
11
; License: (An MIT/X11-style license)
13
; Permission is hereby granted, free of charge, to any person obtaining a
14
; copy of this software and associated documentation files (the "Software"),
15
; to deal in the Software without restriction, including without limitation
16
; the rights to use, copy, modify, merge, publish, distribute, sublicense,
17
; and/or sell copies of the Software, and to permit persons to whom the
18
; Software is furnished to do so, subject to the following conditions:
20
; The above copyright notice and this permission notice shall be included in
21
; all copies or substantial portions of the Software.
23
; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
24
; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
25
; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
26
; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
27
; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
28
; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
29
; DEALINGS IN THE SOFTWARE.
6
31
;; update-nth-array.lisp
7
32
;; Rules about update-nth-array.
72
97
(implies (and (integerp n)
74
99
(equal (len l1) (len l2)))
75
(equal (equal (update-nth-array n i v1 l1)
100
(equal (equal (update-nth-array n i v1 l1)
76
101
(update-nth-array n i v2 l2))
78
(equal (update-nth i v1 (nth n l1))
103
(equal (update-nth i v1 (nth n l1))
79
104
(update-nth i v2 (nth n l2)))
82
(equal (nthcdr (1+ n) l1)
107
(equal (nthcdr (1+ n) l1)
83
108
(nthcdr (1+ n) l2)))))
84
109
:hints (("Goal" :in-theory (enable equal-update-nth-casesplit
85
110
update-nth-array))))
129
154
(equal (update-nth-array i j1 v1 (update-nth-array i j1 v2 l))
130
155
(update-nth-array i j1 v1 l)))
131
156
:rule-classes ((:rewrite :loop-stopper ((j1 j2))))
132
:hints (("Goal" :in-theory (enable update-nth-array))))
157
:hints (("Goal" :in-theory (enable update-nth-array))))
b'\\ No newline at end of file'