4
(include-book "Disjoint-lists")
6
; The following is commented out starting with v2-7 because a more general
7
; macro e/d is now part of ACL2.
8
; (defmacro e/d (enable disable)
9
; `(union-theories ',enable (disable ,@disable)))
11
(defun in-range (idx l)
17
(in-theory (enable in-range))
18
(in-theory (disable mod floor))
20
(defun mlambda-fn (args form)
21
(declare (xargs :guard (symbol-listp args)))
23
(cond ((member form args) form)
24
(t (list 'QUOTE form))))
25
(t (list 'CONS (mlambda-fn args (car form))
26
(mlambda-fn args (cdr form))))))
28
(defmacro mlambda (args form)
29
(declare (xargs :guard (symbol-listp args)))
30
(mlambda-fn args form))
33
(defmacro qr-guard (x y)
35
(and (force (rationalp x))
37
(force (not (equal 0 y))))))
39
(defun type-expected (vars)
41
( (and (true-listp vars)
44
( (and (true-listp vars)
45
(equal (len vars) (len *rns*)))
51
(defthm IN-RANGE-I-ON-M-IMPLIES-IN-RANGE-I-1-ON-CDR-M
52
(IMPLIES (AND (IN-RANGE IDX M)
55
(IN-RANGE (1- IDX) (CDR M))))
63
(defun positive-list (l)
66
(and (positivep (car l))
67
(positive-list (cdr l)))))
70
(defun boolean-to-int (bool)
73
(defun int-to-bool (int)
76
(defun make-n-list (el n)
80
(cons el (make-n-list el (1- n)))))
82
(defun eventually-make-list (l n)
84
(make-n-list (car l) n)
87
(defun double-induct (idx n)
88
(if (zp idx) (+ idx n)
89
(double-induct (1- idx) (1- n))))
91
(defthm el-of-makelist-is-el
95
(in-range idx (make-n-list el n)))
97
(nth idx (make-n-list el n))
99
:hints (("Goal" :induct (double-induct idx n))
100
("Subgoal *1/1" :use make-n-list)))
107
(in-theory (disable my-or-3 my-or-2))
113
(defun opcode (ins) (nth 0 ins))
114
(defun par1 (ins) (nth 1 ins))
115
(defun par2 (ins) (nth 2 ins))
116
(defun par3 (ins) (nth 3 ins))
117
(defun par4 (ins) (nth 4 ins))
120
(defun mem (s) (car s))
121
(defun pcc (s) (cadr s))
122
(defun code (s) (cddr s))
124
(defun make-state (mem pcc code)
125
(cons mem (cons pcc code)))
128
(defun initial-state (prog)
129
(make-state (car prog) 0 (cdr prog)))
136
(defun gem-instruction-p (instr mem)
141
(equal (opcode instr) 'gem-add)
142
(equal (len instr) 4)
143
(is-mem-cell-p (get-cell (par1 instr) mem))
144
(is-mem-cell-p (get-cell (par2 instr) mem))
145
(is-mem-cell-p (get-cell (par3 instr) mem))
146
(equal (var-type (get-cell (par1 instr) mem)) 'Int) )
148
(equal (opcode instr) 'gem-sub)
149
(equal (len instr) 4)
150
(is-mem-cell-p (get-cell (par1 instr) mem))
151
(is-mem-cell-p (get-cell (par2 instr) mem))
152
(is-mem-cell-p (get-cell (par3 instr) mem))
153
(equal (var-type (get-cell (par1 instr) mem)) 'Int)
154
(equal (var-type (get-cell (par2 instr) mem)) 'Int)
155
(equal (var-type (get-cell (par3 instr) mem)) 'Int) )
157
(equal (opcode instr) 'gem-equ)
158
(equal (len instr) 4)
159
(is-mem-cell-p (get-cell (par1 instr) mem))
160
(is-mem-cell-p (get-cell (par2 instr) mem))
161
(is-mem-cell-p (get-cell (par3 instr) mem))
162
(equal (var-type (get-cell (par1 instr) mem)) 'Bool) )
166
(defun gem-instruction-list-p (instlist mem)
171
(gem-instruction-p (car instlist) mem)
172
(gem-instruction-list-p (cdr instlist) mem))))
175
(defun gem-program-p (prog)
179
(is-typed-amem-p (car prog))
180
(bounded-amem-p (car prog))
181
(gem-instruction-list-p (cdr prog) (car prog))))
184
(defun gem-statep (x)
188
(is-typed-amem-p (mem x))
189
(bounded-amem-p (mem x)) ;;; new
190
(gem-instruction-list-p (code x) (mem x))))
193
(defthm nth-instruction-of-gem-list-is-gem-instruction
195
(gem-instruction-list-p gl mem)
198
(gem-instruction-p (nth idx gl) mem)))
199
:hints (("Goal" :in-theory (disable gem-instruction-p)))
202
(defthm an-instruction-of-gem-program-is-null-or-gem-instruction
206
(null (nth (pcc st) (code st)))
207
(gem-instruction-p (nth (pcc st) (code st)) (mem st))))
208
:hints (("Goal" :in-theory (disable code mem pcc gem-instruction-list-p gem-instruction-p)
209
:use (:instance nth-instruction-of-gem-list-is-gem-instruction
225
(defun rtm-instruction-p (instr mem)
230
(equal (opcode instr) 'rtm-add)
231
(equal (len instr) 4)
232
(is-mem-cell-p (get-cell (par1 instr) mem))
233
(is-mem-cell-p (get-cell (par2 instr) mem))
234
(is-mem-cell-p (get-cell (par3 instr) mem))
235
(equal (var-type (get-cell (par1 instr) mem)) 'Int)
236
(equal (var-type (get-cell (par2 instr) mem)) 'Int)
237
(equal (var-type (get-cell (par3 instr) mem)) 'Int)
238
(positivep (par4 instr)))
240
(equal (opcode instr) 'rtm-sub)
241
(equal (len instr) 4)
242
(is-mem-cell-p (get-cell (par1 instr) mem))
243
(is-mem-cell-p (get-cell (par2 instr) mem))
244
(is-mem-cell-p (get-cell (par3 instr) mem))
245
(equal (var-type (get-cell (par1 instr) mem)) 'Int)
246
(equal (var-type (get-cell (par2 instr) mem)) 'Int)
247
(equal (var-type (get-cell (par3 instr) mem)) 'Int)
248
(positivep (par4 instr)))
250
(equal (opcode instr) 'rtm-equ)
251
(equal (len instr) 4)
252
(is-mem-cell-p (get-cell (par1 instr) mem))
253
(is-mem-cell-p (get-cell (par2 instr) mem))
254
(is-mem-cell-p (get-cell (par3 instr) mem))
255
(equal (var-type (get-cell (par1 instr) mem)) 'Int)
256
(equal (var-type (get-cell (par2 instr) mem)) 'Int)
257
(equal (var-type (get-cell (par3 instr) mem)) 'Int))
259
(equal (opcode instr) 'rtm-or)
260
(equal (len instr) 4)
261
(is-mem-cell-p (get-cell (par1 instr) mem))
262
(is-mem-cell-p (get-cell (par2 instr) mem))
263
(is-mem-cell-p (get-cell (par3 instr) mem))
264
(equal (var-type (get-cell (par1 instr) mem)) 'Int)
265
(equal (var-type (get-cell (par2 instr) mem)) 'Int)
266
(equal (var-type (get-cell (par3 instr) mem)) 'Int))
268
(equal (opcode instr) 'rtm-and)
269
(equal (len instr) 4)
270
(is-mem-cell-p (get-cell (par1 instr) mem))
271
(is-mem-cell-p (get-cell (par2 instr) mem))
272
(is-mem-cell-p (get-cell (par3 instr) mem))
273
(equal (var-type (get-cell (par1 instr) mem)) 'Int)
274
(equal (var-type (get-cell (par2 instr) mem)) 'Int)
275
(equal (var-type (get-cell (par3 instr) mem)) 'Int)))))
277
(defun rtm-instruction-list-p (instlist mem)
282
(rtm-instruction-p (car instlist) mem)
283
(rtm-instruction-list-p (cdr instlist) mem))))
286
(defun rtm-program-p (prog)
290
(is-typed-amem-p (car prog))
291
(rtm-instruction-list-p (cdr prog) (car prog))))
296
(defun rtm-statep (x)
300
(is-typed-amem-p (mem x))
301
(rtm-instruction-list-p (code x) (mem x))))
309
(defthm nth-instruction-of-rtm-list-is-rtm-instruction
311
(rtm-instruction-list-p gl mem)
314
(rtm-instruction-p (nth idx gl) mem)))
315
:hints (("Goal" :in-theory (disable rtm-instruction-p)))
318
(defthm an-instruction-of-rtm-program-is-null-or-rtm-instruction
322
(null (nth (pcc st) (code st)))
323
(rtm-instruction-p (nth (pcc st) (code st)) (mem st))))
324
:hints (("Goal" :in-theory (disable code mem pcc rtm-instruction-list-p rtm-instruction-p)
325
:use (:instance nth-instruction-of-rtm-list-is-rtm-instruction
336
(defun sum-and-update (c1 c2 c3 prime mem)
340
(var-value (get-cell c2 mem))
341
(var-value (get-cell c3 mem)))
343
(var-attribute (get-cell c1 mem))
344
(var-type (get-cell c1 mem))))
347
(DEFUN SUM-AND-UPDATE-NOREST (C1 C2 C3 MEM)
349
(+ (VAR-VALUE (GET-CELL C2 MEM))
350
(VAR-VALUE (GET-CELL C3 MEM)))
352
(VAR-ATTRIBUTE (GET-CELL C1 MEM))
353
(VAR-TYPE (GET-CELL C1 MEM))))
355
(defun sub-and-update (c1 c2 c3 prime mem)
359
(var-value (get-cell c2 mem))
360
(var-value (get-cell c3 mem)))
362
(var-attribute (get-cell c1 mem))
363
(var-type (get-cell c1 mem))))
366
(DEFUN SUB-AND-UPDATE-NOREST (C1 C2 C3 MEM)
368
(- (VAR-VALUE (GET-CELL C2 MEM))
369
(VAR-VALUE (GET-CELL C3 MEM)))
371
(VAR-ATTRIBUTE (GET-CELL C1 MEM))
372
(VAR-TYPE (GET-CELL C1 MEM))))
376
(defun and-update (c1 c2 c3 mem)
380
(int-to-bool (var-value (get-cell c2 mem)))
381
(int-to-bool (var-value (get-cell c3 mem)))))
382
(var-attribute (get-cell c1 mem))
383
(var-type (get-cell c1 mem))))
385
(defun or-update (c1 c2 c3 mem)
389
(int-to-bool (var-value (get-cell c2 mem)))
390
(int-to-bool (var-value (get-cell c3 mem)))))
391
(var-attribute (get-cell c1 mem))
392
(var-type (get-cell c1 mem))))
394
(defun gen-eq-update (c1 c2 c3 mem)
398
(var-value (get-cell c2 mem))
399
(var-value (get-cell c3 mem))))
400
(var-attribute (get-cell c1 mem))
401
(var-type (get-cell c1 mem))))
407
(defthm sum-and-update-returns-a-mem-cell
410
(equal (var-type (get-cell c1 mem)) 'Int) ; This is added to account for booleans
411
(is-mem-cell-p (get-cell c1 mem))
412
(is-mem-cell-p (get-cell c2 mem))
413
(is-mem-cell-p (get-cell c3 mem))
415
(is-mem-cell-p (sum-and-update c1 c2 c3 prime mem)))
416
:hints (("Goal" :in-theory (enable mod make-cell var-type var-attribute var-value)))
417
:rule-classes :forward-chaining)
428
(G-C-D (- X Y) Y)))))
429
:hints (("Goal" :in-theory (enable g-c-d nonneg-int-gcd
430
(:executable-counterpart nonneg-int-gcd)
431
(:induction nonneg-int-gcd)))))
435
(defthm posp-all-unfold
440
(POSP-ALL (CDR L)))))
441
:hints (("Goal" :in-theory (enable posp-all))))
443
(defun integer>1-listp (l)
446
(and (integerp (car l))
448
(integer>1-listp (cdr l)))))
452
(equal (integer>1-listp l)
455
(AND (INTEGERP (CAR L))
457
(INTEGER>1-LISTP (CDR L))))))
460
(defthm fact-bout-rns
462
(integer-listp *rns*)
463
(rel-prime-moduli *rns*)
465
(integer>1-listp *rns*)
469
:hints (("Goal" :in-theory (enable prod posp rel-prime-moduli rel-prime-all rel-prime g-c-d (:executable-counterpart nonneg-int-gcd))))
474
posp-all-unfold int>1-unfold))
476
(defthm greater-one-means-greater-zero
477
(implies (integer>1-listp rns) (posp-all rns))
479
:in-theory (enable posp-all posp)))
483
(IMPLIES (AND (POSP M) (INTEGERP A))
487
'((:REWRITE INTEGERP-MOD-EXP)
491
((:INSTANCE MOD-TYPE-EXP (X A) (Y M))
492
(:INSTANCE MOD-=-0-EXP (X A) (Y M)))))
495
(defthm sum-and-update-norest-returns-a-mem-cell
498
(equal (var-type (get-cell c1 mem)) 'Int)
499
(is-mem-cell-p (get-cell c1 mem))
500
(is-mem-cell-p (get-cell c2 mem))
501
(is-mem-cell-p (get-cell c3 mem)))
503
(is-mem-cell-p (sum-and-update-norest c1 c2 c3 mem))
504
(bounded-value (sum-and-update-norest c1 c2 c3 mem))
505
(equal (var-type (sum-and-update-norest c1 c2 c3 mem)) 'Int)) )
509
(a (+ (var-value (get-cell c2 mem)) (var-value (get-cell c3 mem))))
511
(:instance mod-bounds-exp
512
(x (+ (var-value (get-cell c2 mem)) (var-value (get-cell c3 mem))))
514
:in-theory (enable posp make-cell var-type var-attribute var-value)))
515
:rule-classes :forward-chaining)
518
(defthm sub-and-update-returns-a-mem-cell
521
(equal (var-type (get-cell c1 mem)) 'Int)
522
(is-mem-cell-p (get-cell c1 mem))
523
(is-mem-cell-p (get-cell c2 mem))
524
(is-mem-cell-p (get-cell c3 mem))
526
(is-mem-cell-p (sub-and-update c1 c2 c3 prime mem)))
527
:hints (("Goal" :in-theory (enable mod make-cell var-type var-attribute var-value)))
528
:rule-classes :forward-chaining)
531
(defthm sub-and-update-norest-returns-a-mem-cell
534
(equal (var-type (get-cell c1 mem)) 'Int)
535
(is-mem-cell-p (get-cell c1 mem))
536
(is-mem-cell-p (get-cell c2 mem))
537
(is-mem-cell-p (get-cell c3 mem)))
539
(is-mem-cell-p (sub-and-update-norest c1 c2 c3 mem))
540
(bounded-value (sub-and-update-norest c1 c2 c3 mem))
541
(equal (var-type (sub-and-update-norest c1 c2 c3 mem)) 'Int)) )
545
(a (- (var-value (get-cell c2 mem)) (var-value (get-cell c3 mem))))
547
(:instance mod-bounds-exp
548
(x (- (var-value (get-cell c2 mem)) (var-value (get-cell c3 mem))))
550
:in-theory (enable posp make-cell var-type var-attribute var-value)))
551
:rule-classes :forward-chaining)
554
(defthm and-update-returns-a-mem-cell
557
(is-mem-cell-p (get-cell c1 mem))
558
(is-mem-cell-p (get-cell c2 mem))
559
(is-mem-cell-p (get-cell c3 mem)))
560
(is-mem-cell-p (and-update c1 c2 c3 mem)))
561
:hints (("Goal" :in-theory (enable my-or-2 make-cell var-type var-attribute var-value)))
562
:rule-classes :forward-chaining)
564
(defthm or-update-returns-a-mem-cell
567
(is-mem-cell-p (get-cell c1 mem))
568
(is-mem-cell-p (get-cell c2 mem))
569
(is-mem-cell-p (get-cell c3 mem)))
570
(is-mem-cell-p (or-update c1 c2 c3 mem)))
571
:hints (("Goal" :in-theory (enable my-or-2 make-cell var-type var-attribute var-value)))
572
:rule-classes :forward-chaining)
574
(defthm gen-eq-update-returns-a-mem-cell
577
(is-mem-cell-p (get-cell c1 mem))
578
(is-mem-cell-p (get-cell c2 mem))
579
(is-mem-cell-p (get-cell c3 mem)))
581
(bounded-value (gen-eq-update c1 c2 c3 mem))
582
(is-mem-cell-p (gen-eq-update c1 c2 c3 mem))))
586
(a (boolean-to-int (equal (var-value (get-cell c2 mem)) (var-value (get-cell c3 mem)))))
588
(:instance mod-bounds-exp
589
(x (boolean-to-int (equal (var-value (get-cell c2 mem)) (var-value (get-cell c3 mem)))))
591
:in-theory (enable posp my-or-2 make-cell var-type var-attribute var-value)))
592
:rule-classes :forward-chaining)
604
(defun gem-add (a b c s)
607
(sum-and-update-norest a b c (mem s))
612
(defun gem-sub (a b c s)
615
(sub-and-update-norest a b c (mem s))
620
(defun rtm-add (a b c d s)
623
(sum-and-update a b c d (mem s))
628
(defun rtm-sub (a b c d s)
631
(sub-and-update a b c d (mem s))
637
(defun rtm-and (a b c s)
640
(and-update a b c (mem s))
645
(defun rtm-or (a b c s)
648
(or-update a b c (mem s))
653
(defun generic-eql (a b c s)
656
(gen-eq-update a b c (mem s))
663
(defun execute-instruction (st)
665
((op (opcode (nth (pcc st) (code st))))
666
(ins (nth (pcc st) (code st))))
668
(gem-add (gem-add (par1 ins) (par2 ins) (par3 ins) st))
669
(gem-sub (gem-sub (par1 ins) (par2 ins) (par3 ins) st))
670
(gem-equ (generic-eql (par1 ins) (par2 ins) (par3 ins) st))
671
(rtm-add (rtm-add (par1 ins) (par2 ins) (par3 ins) (par4 ins) st))
672
(rtm-sub (rtm-sub (par1 ins) (par2 ins) (par3 ins) (par4 ins) st))
673
(rtm-and (rtm-and (par1 ins) (par2 ins) (par3 ins) st))
674
(rtm-or (rtm-or (par1 ins) (par2 ins) (par3 ins) st))
675
(rtm-equ (generic-eql (par1 ins) (par2 ins) (par3 ins) st))
679
(defun execute-n-instructions (st n)
683
(execute-n-instructions
684
(execute-instruction st)
689
(defthm instruction-incrementing-pvv
692
(>= (pcc (execute-instruction st)) 0)))
697
(defthm in-range-instruction-is-gem-instruction
701
(gem-instruction-list-p code mem))
702
(gem-instruction-p (nth pcc code) mem))
703
:hints (("Goal" :in-theory (disable gem-instruction-p)))
704
:rule-classes :forward-chaining)
708
(defthm in-range-instruction-is-rtmm-instruction
712
(rtm-instruction-list-p code mem))
713
(rtm-instruction-p (nth pcc code) mem))
714
:hints (("Goal" :in-theory (disable rtm-instruction-p)))
715
:rule-classes :forward-chaining)
721
(defthm null-not-in-range
726
(not (in-range idx l)))
728
:rule-classes :forward-chaining)
730
(defthm pcc-not-in-range-means-null-instruction
737
(not (in-range (pcc st) (code st))))
738
(null (nth (pcc st) (code st))))
739
:hints (("Goal" :cases ( (gem-statep st) (rtm-statep st))))
740
:rule-classes :forward-chaining)
742
(defthm null-opcode-implies-execution-does-not-touch-state
744
(null (nth (pcc st) (code st)))
745
(equal (execute-instruction st) st)))
747
(defthm execute-not-in-range-instruction-retrieves-same-state
754
(not (in-range (pcc st) (code st))))
755
(equal (execute-instruction st) st))
756
:hints (("Goal" :cases ( (gem-statep st) (rtm-statep st) ))
757
("Subgoal 2" :use ((:instance gem-statep (x st))
758
null-opcode-implies-execution-does-not-touch-state
759
pcc-not-in-range-means-null-instruction))
760
("Subgoal 1" :use ((:instance rtm-statep (x st))
761
null-opcode-implies-execution-does-not-touch-state
762
pcc-not-in-range-means-null-instruction))))
764
(in-theory (disable null-opcode-implies-execution-does-not-touch-state
765
execute-not-in-range-instruction-retrieves-same-state))
768
(defthm execute-instruction-does-not-touch-code (equal (code (execute-instruction st)) (code st)))
770
(defthm execute-n-instruction-does-not-touch-code (equal (code (execute-n-instructions st n)) (code st)))
772
(defthm execute-n-instruction-decomposition
780
(execute-n-instructions st (+ n1 n2))
781
(execute-n-instructions (execute-n-instructions st n1) n2)))
782
:hints (("Goal" :in-theory (disable execute-instruction member-equal))))
785
(defthm putting-a-new-cell-preserves-typed-amem
788
(is-typed-amem-p mem)
789
(is-mem-cell-p new-cell))
790
(is-typed-amem-p (put-cell c new-cell mem)))
791
:hints (("Goal" :in-theory (enable put-cell))))
793
(defthm no-influence-of-putting-mem-cells
797
(is-mem-cell-p (get-cell c1 mem)))
798
(is-mem-cell-p (get-cell c1 (put-cell pos cell mem))))
799
:hints ( ("Goal" :in-theory (enable put-cell get-cell) )))
802
(defthm putting-a-new-bounded-cell-preserves-boundedness
806
(bounded-value new-cell))
807
(bounded-amem-p (put-cell c new-cell mem)))
808
:hints (("Goal" :in-theory (enable put-cell))))
810
(defthm no-influence-of-putting-bounded-cells
814
(bounded-value (get-cell c1 mem)))
815
(bounded-value (get-cell c1 (put-cell pos cell mem))))
816
:hints ( ("Goal" :in-theory (enable put-cell get-cell) )))
820
(defthm putting-an-existing-cell-does-not-change-var-inclusion-right
822
(is-mem-cell-p (get-cell v mem))
823
(iff (vars-inclusion m mem) (vars-inclusion m (put-cell v anyvalue mem))))
824
:hints (("Goal" :in-theory (enable put-cell get-cell is-mem-cell-p))))
826
(defthm putting-an-existing-cell-does-not-change-var-inclusion-left
828
(is-mem-cell-p (get-cell v mem))
829
(iff (vars-inclusion mem m) (vars-inclusion (put-cell v anyvalue mem) m)))
830
:hints (("Goal" :in-theory (enable put-cell get-cell is-mem-cell-p))))
834
(defthm execute-instruction-is-type-and-attribute-invariant-on-any-var
836
(equal (var-attribute (get-cell cell (mem st)))
837
(var-attribute (get-cell cell (mem (execute-instruction st)))))
838
(equal (var-type (get-cell cell (mem st)))
839
(var-type (get-cell cell (mem (execute-instruction st))))))
840
:hints (("Goal" :in-theory (enable put-cell get-cell make-cell mem make-state var-attribute var-type))))
845
putting-an-existing-cell-does-not-change-var-inclusion-left
846
putting-an-existing-cell-does-not-change-var-inclusion-right
854
;;(ld "Properties-of-Execute-Gem-Instruction-New.lisp" :ld-error-action :error)
858
(defthm any-mem-cell-is-conserved-after-execute-instruction-on-gemstate
861
(is-mem-cell-p (get-cell anycell (mem st))))
862
(is-mem-cell-p (get-cell anycell (mem (execute-instruction st)))))
863
:hints (("Goal" :cases ( (null (nth (pcc st) (code st))) (gem-instruction-p (nth (pcc st) (code st)) (mem st))))
864
("Subgoal 3" :use an-instruction-of-gem-program-is-null-or-gem-instruction)
865
("Subgoal 1" :use (execute-instruction
866
(:instance sum-and-update-norest-returns-a-mem-cell
867
(c1 (par1 (nth (pcc st) (code st))))
868
(c2 (par2 (nth (pcc st) (code st))))
869
(c3 (par3 (nth (pcc st) (code st))))
871
(:instance sub-and-update-norest-returns-a-mem-cell
872
(c1 (par1 (nth (pcc st) (code st))))
873
(c2 (par2 (nth (pcc st) (code st))))
874
(c3 (par3 (nth (pcc st) (code st))))
876
(:instance gen-eq-update-returns-a-mem-cell
877
(c1 (par1 (nth (pcc st) (code st))))
878
(c2 (par2 (nth (pcc st) (code st))))
879
(c3 (par3 (nth (pcc st) (code st))))
881
:in-theory (disable bounded-value put-cell get-cell execute-instruction
882
sum-and-update-norest sub-and-update-norest gen-eq-update
883
par1 par2 par3 par4 member-equal nth rtm-add rtm-sub is-mem-cell-p))))
885
(defthm any-bounded-cell-is-bounded-after-execute-instruction-on-gemstate
888
(bounded-value (get-cell anycell (mem st))))
889
(bounded-value (get-cell anycell (mem (execute-instruction st)))))
890
:hints (("Goal" :cases ( (null (nth (pcc st) (code st))) (gem-instruction-p (nth (pcc st) (code st)) (mem st))))
891
("Subgoal 3" :use an-instruction-of-gem-program-is-null-or-gem-instruction)
892
("Subgoal 1" :use (execute-instruction
893
(:instance sum-and-update-norest-returns-a-mem-cell
894
(c1 (par1 (nth (pcc st) (code st))))
895
(c2 (par2 (nth (pcc st) (code st))))
896
(c3 (par3 (nth (pcc st) (code st))))
898
(:instance sub-and-update-norest-returns-a-mem-cell
899
(c1 (par1 (nth (pcc st) (code st))))
900
(c2 (par2 (nth (pcc st) (code st))))
901
(c3 (par3 (nth (pcc st) (code st))))
903
(:instance gen-eq-update-returns-a-mem-cell
904
(c1 (par1 (nth (pcc st) (code st))))
905
(c2 (par2 (nth (pcc st) (code st))))
906
(c3 (par3 (nth (pcc st) (code st))))
908
:in-theory (disable bounded-value put-cell get-cell execute-instruction bounded-value
909
sum-and-update-norest sub-and-update-norest gen-eq-update
910
par1 par2 par3 par4 member-equal nth rtm-add rtm-sub is-mem-cell-p))))
913
(defthm execute-instruction-is-type-and-attribute-invariant-on-any-var
915
(equal (var-attribute (get-cell cell (mem st)))
916
(var-attribute (get-cell cell (mem (execute-instruction st)))))
917
(equal (var-type (get-cell cell (mem st)))
918
(var-type (get-cell cell (mem (execute-instruction st))))))
919
:hints (("Goal" :in-theory (enable put-cell get-cell make-cell mem make-state var-attribute var-type))))
922
(defthm any-gem-instruction-is-conserved-by-execution
926
(gem-instruction-p instr (mem st)))
927
(gem-instruction-p instr (mem (execute-instruction st))))
929
:in-theory '((:definition gem-instruction-p))
932
(:instance any-mem-cell-is-conserved-after-execute-instruction-on-gemstate
933
(anycell (par1 instr)))
934
(:instance any-mem-cell-is-conserved-after-execute-instruction-on-gemstate
935
(anycell (par2 instr)))
936
(:instance any-mem-cell-is-conserved-after-execute-instruction-on-gemstate
937
(anycell (par3 instr)))
938
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
940
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
942
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
943
(cell (par3 instr)))))))
947
(defthm a-gem-instruction-list-is-such-after-execute-instruction
951
(gem-instruction-list-p instrlist (mem st)))
952
(gem-instruction-list-p instrlist (mem (execute-instruction st))))
954
:induct (gem-instruction-list-p instrlist (mem st)) ;(len instrlist)
955
:in-theory (disable execute-instruction))
956
("Subgoal *1/3" :use (:instance gem-instruction-list-p (instlist instrlist) (mem (mem st))))
958
:in-theory (union-theories (current-theory 'ground-zero) '((:definition gem-instruction-list-p)))
959
:use (:instance any-gem-instruction-is-conserved-by-execution (instr (car instrlist))))))
964
(defthm execute-gem-retrieves-a-memory
968
(gem-instruction-p (nth (pcc st) (code st)) (mem st)))
970
(bounded-amem-p (mem (execute-instruction st)))
971
(is-typed-amem-p (mem (execute-instruction st)))))
973
:in-theory (disable is-mem-cell-p sum-and-update-norest sub-and-update-norest gen-eq-update)
975
(:instance gen-eq-update-returns-a-mem-cell
976
(c1 (par1 (nth (pcc st) (code st))))
977
(c2 (par2 (nth (pcc st) (code st))))
978
(c3 (par3 (nth (pcc st) (code st))))
980
(:instance sum-and-update-norest-returns-a-mem-cell
981
(c1 (par1 (nth (pcc st) (code st))))
982
(c2 (par2 (nth (pcc st) (code st))))
983
(c3 (par3 (nth (pcc st) (code st))))
985
(:instance sub-and-update-norest-returns-a-mem-cell
986
(c1 (par1 (nth (pcc st) (code st))))
987
(c2 (par2 (nth (pcc st) (code st))))
988
(c3 (par3 (nth (pcc st) (code st))))
993
(defthm executing-gem-instruction-retrieves-a-gem-state-from-gem-state
996
(gem-statep (execute-instruction st)))
997
:hints (("Goal" :cases ( (null (nth (pcc st) (code st))) (gem-instruction-p (nth (pcc st) (code st)) (mem st))))
998
("Subgoal 3" :use an-instruction-of-gem-program-is-null-or-gem-instruction)
1001
(:instance a-gem-instruction-list-is-such-after-execute-instruction (instrlist (code st)))
1002
(:instance execute-gem-retrieves-a-memory))
1003
:in-theory (disable sum-and-update-norest sub-and-update-norest gen-eq-update gem-instruction-p
1004
par1 par2 par3 par4 member-equal nth))))
1010
(defthm executing-gem-instruction-preserves-correctness-wrt-arity
1014
(correct-wrt-arity m (mem st)))
1015
(correct-wrt-arity m (mem (execute-instruction st))))
1016
:hints (("Goal" :in-theory (disable correct-type gemvar-0 var-type gem-statep pcc nth execute-instruction type-0))
1017
("Subgoal *1/3" :use (:instance execute-instruction-is-type-and-attribute-invariant-on-any-var (cell (gemvar-0 m))))))
1023
(defthm executing-gem-instruction-keeps-vars-inclusion-right
1026
(iff (vars-inclusion m (mem st)) (vars-inclusion m (mem (execute-instruction st)))))
1027
:hints (("Goal" :cases ( (null (nth (pcc st) (code st))) (gem-instruction-p (nth (pcc st) (code st)) (mem st))))
1028
("Subgoal 3" :use an-instruction-of-gem-program-is-null-or-gem-instruction)
1029
("Subgoal 1" :in-theory (disable par1 par2 par3 par4 sum-and-update-norest opcode code pcc member-equal nth)
1030
:cases ( (equal (opcode (nth (pcc st) (code st))) 'gem-equ)
1031
(equal (opcode (nth (pcc st) (code st))) 'gem-add)
1032
(equal (opcode (nth (pcc st) (code st))) 'gem-sub)))
1033
("Subgoal 1.3" :in-theory '((:rewrite car-cons)
1034
(:definition make-state)
1036
(:definition generic-eql)
1037
(:definition execute-instruction)
1038
(:definition gem-instruction-p))
1039
:use (:instance putting-an-existing-cell-does-not-change-var-inclusion-right
1041
(v (par1 (nth (pcc st) (code st))))
1042
(anyvalue (gen-eq-update
1043
(par1 (nth (pcc st) (code st)))
1044
(par2 (nth (pcc st) (code st)))
1045
(par3 (nth (pcc st) (code st)))
1047
("Subgoal 1.2" :in-theory '((:rewrite car-cons)
1048
(:definition make-state)
1050
(:definition gem-add)
1051
(:definition execute-instruction)
1052
(:definition gem-instruction-p))
1053
:use (:instance putting-an-existing-cell-does-not-change-var-inclusion-right
1055
(v (par1 (nth (pcc st) (code st))))
1056
(anyvalue (sum-and-update-norest
1057
(par1 (nth (pcc st) (code st)))
1058
(par2 (nth (pcc st) (code st)))
1059
(par3 (nth (pcc st) (code st)))
1061
("Subgoal 1.1" :in-theory '((:rewrite car-cons)
1062
(:definition make-state)
1064
(:definition gem-sub)
1065
(:definition execute-instruction)
1066
(:definition gem-instruction-p))
1067
:use (:instance putting-an-existing-cell-does-not-change-var-inclusion-right
1069
(v (par1 (nth (pcc st) (code st))))
1070
(anyvalue (sub-and-update-norest
1071
(par1 (nth (pcc st) (code st)))
1072
(par2 (nth (pcc st) (code st)))
1073
(par3 (nth (pcc st) (code st)))
1076
(defthm executing-gem-instruction-keeps-vars-inclusion-left
1079
(iff (vars-inclusion (mem st) m) (vars-inclusion (mem (execute-instruction st)) m)))
1080
:hints (("Goal" :cases ( (null (nth (pcc st) (code st))) (gem-instruction-p (nth (pcc st) (code st)) (mem st))))
1081
("Subgoal 3" :use an-instruction-of-gem-program-is-null-or-gem-instruction)
1082
("Subgoal 1" :in-theory (disable par1 par2 par3 par4 sum-and-update-norest opcode code pcc member-equal nth)
1083
:cases ( (equal (opcode (nth (pcc st) (code st))) 'gem-equ)
1084
(equal (opcode (nth (pcc st) (code st))) 'gem-add)
1085
(equal (opcode (nth (pcc st) (code st))) 'gem-sub)))
1086
("Subgoal 1.3" :in-theory '((:rewrite car-cons)
1087
(:definition make-state)
1089
(:definition generic-eql)
1090
(:definition execute-instruction)
1091
(:definition gem-instruction-p))
1092
:use (:instance putting-an-existing-cell-does-not-change-var-inclusion-left
1094
(v (par1 (nth (pcc st) (code st))))
1095
(anyvalue (gen-eq-update
1096
(par1 (nth (pcc st) (code st)))
1097
(par2 (nth (pcc st) (code st)))
1098
(par3 (nth (pcc st) (code st)))
1100
("Subgoal 1.2" :in-theory '((:rewrite car-cons)
1101
(:definition make-state)
1103
(:definition gem-add)
1104
(:definition execute-instruction)
1105
(:definition gem-instruction-p))
1106
:use (:instance putting-an-existing-cell-does-not-change-var-inclusion-left
1108
(v (par1 (nth (pcc st) (code st))))
1109
(anyvalue (sum-and-update-norest
1110
(par1 (nth (pcc st) (code st)))
1111
(par2 (nth (pcc st) (code st)))
1112
(par3 (nth (pcc st) (code st)))
1114
("Subgoal 1.1" :in-theory '((:rewrite car-cons)
1115
(:definition make-state)
1117
(:definition gem-sub)
1118
(:definition execute-instruction)
1119
(:definition gem-instruction-p))
1120
:use (:instance putting-an-existing-cell-does-not-change-var-inclusion-left
1122
(v (par1 (nth (pcc st) (code st))))
1123
(anyvalue (sub-and-update-norest
1124
(par1 (nth (pcc st) (code st)))
1125
(par2 (nth (pcc st) (code st)))
1126
(par3 (nth (pcc st) (code st)))
1130
;;(ld "Properties-of-Execute-n-Rtm-Instructions-New.lisp" :ld-error-action :error)
1134
(defthm any-mem-cell-is-conserved-after-execute-instruction-on-rtmstate
1137
(is-mem-cell-p (get-cell anycell (mem st))))
1138
(is-mem-cell-p (get-cell anycell (mem (execute-instruction st)))))
1139
:hints (("Goal" :cases ( (null (nth (pcc st) (code st))) (rtm-instruction-p (nth (pcc st) (code st)) (mem st))))
1140
("Subgoal 3" :use an-instruction-of-rtm-program-is-null-or-rtm-instruction)
1141
("Subgoal 1" :use (execute-instruction
1142
(:instance gen-eq-update-returns-a-mem-cell
1143
(c1 (par1 (nth (pcc st) (code st))))
1144
(c2 (par2 (nth (pcc st) (code st))))
1145
(c3 (par3 (nth (pcc st) (code st))))
1147
(:instance and-update-returns-a-mem-cell
1148
(c1 (par1 (nth (pcc st) (code st))))
1149
(c2 (par2 (nth (pcc st) (code st))))
1150
(c3 (par3 (nth (pcc st) (code st))))
1152
(:instance or-update-returns-a-mem-cell
1153
(c1 (par1 (nth (pcc st) (code st))))
1154
(c2 (par2 (nth (pcc st) (code st))))
1155
(c3 (par3 (nth (pcc st) (code st))))
1157
(:instance sum-and-update-returns-a-mem-cell
1158
(c1 (par1 (nth (pcc st) (code st))))
1159
(c2 (par2 (nth (pcc st) (code st))))
1160
(c3 (par3 (nth (pcc st) (code st))))
1161
(prime (par4 (nth (pcc st) (code st))))
1163
(:instance sub-and-update-returns-a-mem-cell
1164
(c1 (par1 (nth (pcc st) (code st))))
1165
(c2 (par2 (nth (pcc st) (code st))))
1166
(c3 (par3 (nth (pcc st) (code st))))
1167
(prime (par4 (nth (pcc st) (code st))))
1169
:in-theory (disable put-cell get-cell execute-instruction
1170
sum-and-update sub-and-update and-update or-update gen-eq-update
1171
par1 par2 par3 par4 member-equal nth gem-add gem-sub is-mem-cell-p))))
1174
(defthm any-rtm-instruction-is-conserved-by-execution
1178
(rtm-instruction-p instr (mem st)))
1179
(rtm-instruction-p instr (mem (execute-instruction st))))
1181
:in-theory '((:definition rtm-instruction-p))
1184
(:instance any-mem-cell-is-conserved-after-execute-instruction-on-rtmstate
1185
(anycell (par1 instr)))
1186
(:instance any-mem-cell-is-conserved-after-execute-instruction-on-rtmstate
1187
(anycell (par2 instr)))
1188
(:instance any-mem-cell-is-conserved-after-execute-instruction-on-rtmstate
1189
(anycell (par3 instr)))
1190
(:instance any-mem-cell-is-conserved-after-execute-instruction-on-rtmstate
1191
(anycell (par4 instr)))
1192
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
1193
(cell (par1 instr)))
1194
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
1195
(cell (par2 instr)))
1196
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
1197
(cell (par3 instr)))
1198
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
1199
(cell (par4 instr)))))))
1203
(defthm a-rtm-instruction-list-is-such-after-execute-instruction
1207
(rtm-instruction-list-p instrlist (mem st)))
1208
(rtm-instruction-list-p instrlist (mem (execute-instruction st))))
1210
:induct (rtm-instruction-list-p instrlist (mem st))
1211
:in-theory (disable execute-instruction))
1212
("Subgoal *1/3" :use (:instance rtm-instruction-list-p (instlist instrlist) (mem (mem st))))
1214
:in-theory (union-theories (current-theory 'ground-zero) '((:definition rtm-instruction-list-p)))
1215
:use (:instance any-rtm-instruction-is-conserved-by-execution (instr (car instrlist))))))
1218
(defthm execute-rtm-retrieves-a-memory
1222
(rtm-instruction-p (nth (pcc st) (code st)) (mem st)))
1223
(is-typed-amem-p (mem (execute-instruction st))))
1225
:in-theory (disable is-mem-cell-p
1226
and-update or-update gen-eq-update sum-and-update sub-and-update )
1228
(:instance gen-eq-update-returns-a-mem-cell
1229
(c1 (par1 (nth (pcc st) (code st))))
1230
(c2 (par2 (nth (pcc st) (code st))))
1231
(c3 (par3 (nth (pcc st) (code st))))
1233
(:instance or-update-returns-a-mem-cell
1234
(c1 (par1 (nth (pcc st) (code st))))
1235
(c2 (par2 (nth (pcc st) (code st))))
1236
(c3 (par3 (nth (pcc st) (code st))))
1238
(:instance and-update-returns-a-mem-cell
1239
(c1 (par1 (nth (pcc st) (code st))))
1240
(c2 (par2 (nth (pcc st) (code st))))
1241
(c3 (par3 (nth (pcc st) (code st))))
1243
(:instance sum-and-update-returns-a-mem-cell
1244
(c1 (par1 (nth (pcc st) (code st))))
1245
(c2 (par2 (nth (pcc st) (code st))))
1246
(c3 (par3 (nth (pcc st) (code st))))
1247
(prime (par4 (nth (pcc st) (code st))))
1249
(:instance sub-and-update-returns-a-mem-cell
1250
(c1 (par1 (nth (pcc st) (code st))))
1251
(c2 (par2 (nth (pcc st) (code st))))
1252
(c3 (par3 (nth (pcc st) (code st))))
1253
(prime (par4 (nth (pcc st) (code st))))
1258
(defthm executing-rtm-instruction-retrieves-a-rtm-state-from-rtm-state
1261
(rtm-statep (execute-instruction st)))
1262
:hints (("Goal" :cases ( (null (nth (pcc st) (code st))) (rtm-instruction-p (nth (pcc st) (code st)) (mem st))))
1263
("Subgoal 3" :use an-instruction-of-rtm-program-is-null-or-rtm-instruction)
1266
(:instance a-rtm-instruction-list-is-such-after-execute-instruction (instrlist (code st)))
1267
(:instance execute-rtm-retrieves-a-memory))
1268
:in-theory (disable sum-and-update sub-and-update and-update or-update gen-eq-update
1270
par1 par2 par3 par4 member-equal nth))))
1276
(defthm executing-rtm-instruction-is-attributes-invariant
1280
(var-attributes vars (mem st))
1281
(var-attributes vars (mem (execute-instruction st)))))
1282
:hints (("Goal" :in-theory (disable par1 par2 par3 par4 member-equal nth))
1283
("Subgoal *1/2" :use (:instance execute-instruction-is-type-and-attribute-invariant-on-any-var
1284
(cell (car vars))))))
1288
(defthm executing-rtm-instruction-keeps-m-pointing-to-rtm-var-sets
1292
(m-entries-point-to-good-rtm-var-sets m (mem st)))
1293
(m-entries-point-to-good-rtm-var-sets m (mem (execute-instruction st))))
1294
:hints (("Goal" :in-theory (disable par1 par2 par3 par4 member-equal nth))
1295
("Subgoal *1/3" :use (:instance executing-rtm-instruction-is-attributes-invariant
1296
(vars (rtmintvars-0 m))))))
1314
(defun listpars1 (st n)
1317
(cons (par1 (nth (pcc st) (code st)))
1318
(listpars1 (execute-instruction st) (1- n)))))
1320
(defun listpars2 (st n)
1323
(cons (par2 (nth (pcc st) (code st)))
1324
(listpars2 (execute-instruction st) (1- n)))))
1326
(defun listpars3 (st n)
1329
(cons (par3 (nth (pcc st) (code st)))
1330
(listpars3 (execute-instruction st) (1- n)))))
1332
(defun listpars4 (st n)
1335
(cons (par4 (nth (pcc st) (code st)))
1336
(listpars4 (execute-instruction st) (1- n)))))
1341
(defthm lemma12-lp1r
1342
(equal (cdr (listpars1 st n)) (listpars1 (execute-instruction st) (1- n)))
1343
:hints (("Goal" :in-theory (disable execute-instruction))))
1346
(defthm lemma12-lp2r
1347
(equal (cdr (listpars2 st n)) (listpars2 (execute-instruction st) (1- n)))
1348
:hints (("Goal" :in-theory (disable execute-instruction))))
1351
(defthm lemma12-lp3r
1352
(equal (cdr (listpars3 st n)) (listpars3 (execute-instruction st) (1- n)))
1353
:hints (("Goal" :in-theory (disable execute-instruction))))
1356
(defthm lemma12-lp4r
1357
(equal (cdr (listpars4 st n)) (listpars4 (execute-instruction st) (1- n)))
1358
:hints (("Goal" :in-theory (disable execute-instruction))))
1360
(defthm length-of-listpars1-n-is-n
1365
(equal (len (listpars1 st n)) n))
1366
:hints (("Goal" :in-theory (disable execute-instruction nth par1 pcc code member-equal))))
1368
(defthm length-of-listpars2-n-is-n
1373
(equal (len (listpars2 st n)) n))
1374
:hints (("Goal" :in-theory (disable execute-instruction nth par2 pcc code member-equal))))
1376
(defthm length-of-listpars3-n-is-n
1381
(equal (len (listpars3 st n)) n))
1382
:hints (("Goal" :in-theory (disable execute-instruction))))
1384
(defthm length-of-listpars4-n-is-n
1389
(equal (len (listpars4 st n)) n))
1390
:hints (("Goal" :in-theory (disable execute-instruction))))
1405
(defthm only-par1-is-involved
1409
(null (nth (pcc gstate) (code gstate)))
1410
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
1411
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
1412
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub))
1413
(not (equal var (par1 (nth (pcc gstate) (code gstate))))) )
1414
(equal (get-cell var (mem gstate)) (get-cell var (mem (execute-instruction gstate)))))
1415
:hints (("Goal" :in-theory (disable sum-and-update sub-and-update gen-eq-update nth mod))))
1417
(defthm only-par1-is-involved-rtm
1421
(null (nth (pcc gstate) (code gstate)))
1422
(equal (opcode (nth (pcc gstate) (code gstate))) 'rtm-and)
1423
(equal (opcode (nth (pcc gstate) (code gstate))) 'rtm-or)
1424
(equal (opcode (nth (pcc gstate) (code gstate))) 'rtm-equ)
1425
(equal (opcode (nth (pcc gstate) (code gstate))) 'rtm-add)
1426
(equal (opcode (nth (pcc gstate) (code gstate))) 'rtm-sub))
1427
(not (equal var (par1 (nth (pcc gstate) (code gstate))))) )
1428
(equal (get-cell var (mem gstate)) (get-cell var (mem (execute-instruction gstate)))))
1429
:hints (("Goal" :in-theory (disable sum-and-update sub-and-update gen-eq-update nth mod))))
1450
(in-theory (enable build-values-by-rns))
1453
(in-theory (disable mod floor))
1459
(defun rtmintvars-i (gvar m) (cdr (assoc-equal gvar m)))
1461
(DEFUN TYPE-I (gvar M)
1462
(COND ((AND (TRUE-LISTP (RTMINTVARS-I gvar M))
1463
(EQUAL (LEN (RTMINTVARS-I gvar M)) 1))
1465
((AND (TRUE-LISTP (RTMINTVARS-I gvar M))
1466
(EQUAL (LEN (RTMINTVARS-I gvar M))
1471
(defthm type-i-is-vartyper
1474
(assoc-equal gvar1 m)
1476
(correct-wrt-arity m mem))
1477
(equal (type-i gvar1 m) (var-type (get-cell gvar1 mem))))
1478
:hints (("Goal" :in-theory (enable
1479
var-type gemvar-0 rtmintvars-0 var-type type-i type-0))))
1481
(defthm type-i-is-type-expected
1484
(assoc-equal gvar m)
1486
(correct-wrt-arity m mem))
1489
(type-expected (rtmintvars-i gvar m)))))
1491
(defun pos-equal-0 (el l)
1494
( (equal el (caar l)) 0 )
1495
(t (1+ (pos-equal-0 el (cdr l))))))
1497
(defthm assoc-means-pos-in-range
1498
(implies (assoc-equal el l) (in-range (pos-equal-0 el l) l))
1499
:rule-classes :forward-chaining)
1503
(defun retrieve-gemvars (m)
1507
(cons (gemvar-0 m) (retrieve-gemvars (cdr m)))))
1510
(defthm retrieve-gemvars-same-len
1513
(equal (len (retrieve-gemvars m)) (len m))))
1515
(defthm equal-nth-of-retrieve-car-of-nth
1516
(equal (nth idx (retrieve-gemvars m)) (car (nth idx m)))
1517
:hints (("Goal" :in-theory (enable gemvar-0))))
1520
(defthm no-duplicates-whose-caar-is-nth-idx-means-idx-is-0
1521
(IMPLIES (AND (NOT (ENDP L))
1522
(EQUAL (CAR (NTH IDX L)) (CAAR L))
1525
(NO-DUPLICATES-P (RETRIEVE-GEMVARS L)))
1528
:in-theory (union-theories (current-theory 'ground-zero)
1529
'((:definition in-range)
1531
(:rewrite equal-nth-of-retrieve-car-of-nth)))
1534
(:instance retrieve-gemvars-same-len (m l))
1535
(:instance no-dup-3 (l (retrieve-gemvars l)) (idx2 0)))))
1540
(IMPLIES (AND (NOT (ENDP L))
1541
(EQUAL (CAR (NTH IDX L)) (CAAR L))
1543
(< (POS-EQUAL-0 (CAR (NTH IDX L)) L)
1548
(NO-DUPLICATES-P (RETRIEVE-GEMVARS L)))
1549
(EQUAL (POS-EQUAL-0 (CAR (NTH IDX L)) L)
1552
:use no-duplicates-whose-caar-is-nth-idx-means-idx-is-0)))
1555
(defthm no-duplicates-has-pos-equal-right-in-that-place
1560
(no-duplicates-p (retrieve-gemvars l)))
1561
(equal (pos-equal-0 (car (nth idx l)) l) idx))
1562
:hints (("Goal" :in-theory (enable gemvar-0))
1563
("Subgoal *1/2" :use subgoal12)))
1569
(defthm rtmintvars-i-is-cdr-of-nth-entry
1570
(equal (rtmintvars-i gvar m)
1571
(cdr (nth (pos-equal-0 gvar m) m))))
1575
(defun type-i-idx (m idx)
1576
(COND ((AND (TRUE-LISTP (cdr (nth idx m)))
1577
(EQUAL (LEN (cdr (nth idx m))) 1))
1579
((AND (TRUE-LISTP (cdr (nth idx m)))
1580
(EQUAL (LEN (cdr (nth idx m)))
1585
(defun listinstr (st n)
1588
(cons (nth (pcc st) (code st))
1589
(listinstr (execute-instruction st) (1- n)))))
1591
(defthm inclusion-trans
1594
(vars-inclusion m1 m2)
1596
(assoc-equal v m2)))
1598
(defthm correct-wrt-arity-has-rtmintvars-i-tl
1600
(correct-wrt-arity m mem)
1601
(true-listp (rtmintvars-i gvar1 m)))
1602
:hints (("Goal" :in-theory (enable correct-wrt-arity type-0 gemvar-0 rtmintvars-0 correct-type))))
1604
(defun rtm-eq-and (v1 v2 tmp res)
1606
(list 'rtm-equ tmp v1 v2)
1607
(list 'rtm-and res tmp res)))
1609
(defun rtm-eq-or (v1 v2 tmp res)
1611
(list 'rtm-equ tmp v1 v2)
1612
(list 'rtm-or res tmp tmp)))
1614
(defun equality-trans2 (listvars1 listvars2 tmp res)
1615
(if (endp listvars1)
1618
(rtm-eq-and (car listvars1) (car listvars2) tmp res)
1619
(equality-trans2 (cdr listvars1) (cdr listvars2) tmp res))))
1621
(defun equality-trans3 (listvars1 listvars2 tmp res)
1623
(rtm-eq-or (car listvars1) (car listvars2) tmp res)
1624
(equality-trans2 (cdr listvars1) (cdr listvars2) tmp res)))
1626
(defun all-rtm-adds-for-n-steps (st n)
1627
(declare (xargs :measure (acl2-count n)))
1631
(equal (opcode (nth (pcc st) (code st))) 'rtm-add)
1632
(all-rtm-adds-for-n-steps (execute-instruction st) (1- n)))))
1634
(defun all-rtm-subs-for-n-steps (st n)
1635
(declare (xargs :measure (acl2-count n)))
1639
(equal (opcode (nth (pcc st) (code st))) 'rtm-sub)
1640
(all-rtm-subs-for-n-steps (execute-instruction st) (1- n)))))
1643
(defun good-translation-gem-rtm (gstate rstate m)
1644
(declare (xargs :measure (acl2-count (- (len (code gstate)) (pcc gstate)))))
1646
(or (not (integerp (pcc gstate)))
1648
(>= (pcc gstate) (len (code gstate))))
1649
(>= (pcc rstate) (len (code rstate)))
1650
(case (opcode (nth (pcc gstate) (code gstate)))
1653
(in-range (pcc rstate) (code rstate))
1654
(equal (listinstr rstate (* 2 (len *rns*)) )
1656
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*))
1657
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*))
1659
(car (rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m))))
1661
(par1 (nth (pcc gstate) (code gstate)))
1662
(par2 (nth (pcc gstate) (code gstate)))))
1664
(par1 (nth (pcc gstate) (code gstate)))
1665
(par3 (nth (pcc gstate) (code gstate)))))
1666
(good-translation-gem-rtm
1667
(execute-instruction gstate )
1668
(execute-n-instructions rstate (* 2 (len *rns*)) )
1672
(in-range (pcc rstate) (code rstate))
1673
(all-rtm-adds-for-n-steps rstate (len *rns*) )
1674
(equal (listpars1 rstate (len *rns*) )
1675
(rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m))
1676
(equal (listpars2 rstate (len *rns*) )
1677
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*))) ;new
1678
(equal (listpars3 rstate (len *rns*) )
1679
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*))) ;new
1680
(equal (listpars4 rstate (len *rns*) ) *rns*)
1681
(good-translation-gem-rtm
1682
(execute-instruction gstate )
1683
(execute-n-instructions rstate (len *rns*) )
1687
(in-range (pcc rstate) (code rstate))
1688
(all-rtm-subs-for-n-steps rstate (len *rns*) )
1689
(equal (listpars1 rstate (len *rns*) )
1690
(rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m))
1691
(equal (listpars2 rstate (len *rns*) )
1692
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*))) ;new
1693
(equal (listpars3 rstate (len *rns*) )
1694
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*))) ;new
1695
(equal (listpars4 rstate (len *rns*) ) *rns*)
1696
(good-translation-gem-rtm
1697
(execute-instruction gstate )
1698
(execute-n-instructions rstate (len *rns*) )
1706
(defun equal-get-cells (lcell mem1 mem2)
1710
(equal (get-cell (car lcell) mem1) (get-cell (car lcell) mem2))
1711
(equal-get-cells (cdr lcell) mem1 mem2))))
1713
(defthm equal-get-cells-implies-equal-parts-of-cells
1715
(equal-get-cells lcell mem1 mem2)
1718
(var-attributes lcell mem1)
1719
(var-attributes lcell mem2))
1721
(var-values lcell mem1)
1722
(var-values lcell mem2)))))
1725
(defthm equal-get-cells-implies-equal-values-and-attributes-still-works
1727
(equal-get-cells lcell mem1 mem2)
1729
(equal-values-and-attributes gemcell lcell mem1 type)
1730
(equal-values-and-attributes gemcell lcell mem2 type))))
1733
(defun idx-different-cell (l mem1 mem2)
1736
( (not (equal (get-cell (car l) mem1) (get-cell (car l) mem2))) 0 )
1737
(t (1+ (idx-different-cell (cdr l) mem1 mem2)))))
1741
(defthm if-bad-index-in-range-then-cells-must-be-different
1743
(in-range (idx-different-cell l mem1 mem2) l)
1745
(get-cell (nth (idx-different-cell l mem1 mem2) l) mem1)
1746
(get-cell (nth (idx-different-cell l mem1 mem2) l) mem2))))
1747
:rule-classes :forward-chaining)
1750
(defthm if-bad-index-not-in-range-then-every-equal
1751
(implies (and (true-listp l)
1752
(not (in-range (idx-different-cell l mem1 mem2) l)))
1753
(equal-get-cells l mem1 mem2)))
1760
(in-theory (enable gemvar-0 rtmintvars-0))
1762
(defthm m-correspondent-values-implies-equal-values-and-attribus
1766
(m-correspondent-values-p m memgstate memrstate)
1767
(assoc-equal gvar1 m))
1768
(equal-values-and-attributes
1769
(get-cell gvar1 memgstate)
1770
(rtmintvars-i gvar1 m)
1773
:hints (("Goal" :in-theory (disable equal-values-and-attributes))))
1775
(in-theory (disable gemvar-0 rtmintvars-0))
1778
(defun retrieve-rtmvars (m)
1782
(retrieve-rtmvars (cdr m)))))
1785
(defthm rtmintvars-i-is-pos-equal-0-of-retrieve-vars
1786
(equal (rtmintvars-i gvar m)
1787
(nth (pos-equal-0 gvar m) (retrieve-rtmvars m))))
1793
(equal (len m) (len (retrieve-rtmvars m))))
1799
(iff (in-range idx m) (in-range idx (retrieve-rtmvars m))))
1800
:hints (("Goal" :use lemma-help2))
1806
(assoc-equal gvar1 m)
1807
(not (equal gvar1 gvar2)))
1808
(not (equal (pos-equal-0 gvar1 m) (pos-equal-0 gvar2 m)))))
1810
(defthm lemma1-different-vars-do-not-belong
1814
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
1815
(assoc-equal gvar1 m)
1816
(assoc-equal gvar2 m)
1817
(not (equal gvar1 gvar2))
1818
(in-range idx1 (rtmintvars-i gvar1 m)))
1819
(not (member-equal-bool (nth idx1 (rtmintvars-i gvar1 m))
1820
(rtmintvars-i gvar2 m))))
1822
:in-theory '((:type-prescription retrieve-rtmvars)
1823
(:definition in-range)
1824
(:rewrite in-range-is-member-eq-bool))
1827
(:instance lemma-help3 (idx (pos-equal-0 gvar1 m)))
1828
(:instance lemma-help3 (idx (pos-equal-0 gvar2 m)))
1829
(:instance generalized-disjunctivity-unordered-2
1830
(el1 (nth idx1 (nth (pos-equal-0 gvar1 m) (retrieve-rtmvars m))))
1831
(ll (retrieve-rtmvars m))
1832
(idx1 (pos-equal-0 gvar1 m))
1833
(idx2 (pos-equal-0 gvar2 m)))
1834
(:instance assoc-means-pos-in-range (el gvar1) (l m))
1835
(:instance assoc-means-pos-in-range (el gvar2) (l m))
1836
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars (gvar gvar1))
1837
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars (gvar gvar2))))))
1840
(defthm teorema-main-con-pcc-in-range-su-variabile-non-interessata
1845
(in-range (pcc gstate) (code gstate))
1846
(in-range (pcc rstate) (code rstate))
1847
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate))))))
1849
(get-cell gvar1 (mem (execute-instruction gstate)))
1850
(get-cell gvar1 (mem gstate))))
1851
:hints (("Goal" :use (:instance only-par1-is-involved (var gvar1)))))
1854
(defun bad-idx-eqv-va (m gem-mem rtm-mem)
1858
( (not (equal-values-and-attributes
1859
(get-cell (gemvar-0 m) gem-mem)
1864
(t (1+ (bad-idx-eqv-va (cdr m) gem-mem rtm-mem)))))
1866
(defthm if-bad-index-in-range-thne-must-be-different-mc
1868
(in-range (bad-idx-eqv-va m gem-mem rtm-mem) m)
1869
(not (m-correspondent-values-p m gem-mem rtm-mem)))
1870
:hints (("Goal" :in-theory (enable gemvar-0))))
1872
(defthm if-bad-index-in-range-thne-must-be-different-vs
1874
(in-range (bad-idx-eqv-va m gem-mem rtm-mem) m)
1876
(equal-values-and-attributes
1877
(get-cell (car (nth (bad-idx-eqv-va m gem-mem rtm-mem) m)) gem-mem)
1878
(cdr (nth (bad-idx-eqv-va m gem-mem rtm-mem) m))
1880
(type-i-idx m (bad-idx-eqv-va m gem-mem rtm-mem)))))
1881
:hints (("Goal" :in-theory (e/d (type-0 gemvar-0 rtmintvars-0)
1882
(var-attribute var-attributes apply-direct-rns-to-value-according-to-type
1883
var-values-of-1-variable-is-one-element-list-of-var-value
1884
var-values equal-values
1888
(defthm if-bad-index-not-in-range-then-m-corr
1892
(not (in-range (bad-idx-eqv-va m gem-mem rtm-mem) m)))
1893
(m-correspondent-values-p m gem-mem rtm-mem))
1894
:hints (("Goal" :in-theory (e/d (gemvar-0)
1895
((:type-prescription retrieve-rtmvars)
1896
retrieve-rtmvars)))))
1898
(defthm execute-n-instructions-keeps-rtm-state-and-points-to-good
1902
(m-entries-point-to-good-rtm-var-sets m (mem st)))
1904
(rtm-statep (execute-n-instructions st n))
1905
(m-entries-point-to-good-rtm-var-sets m (mem (execute-n-instructions st n)))))
1906
:hints (("Goal" :induct (execute-n-instructions st n) )
1908
:in-theory '((:definition execute-n-instructions)
1909
(:rewrite executing-rtm-instruction-keeps-m-pointing-to-rtm-var-sets)
1910
(:rewrite executing-rtm-instruction-retrieves-a-rtm-state-from-rtm-state)))))
1913
;;(ld "Proof-Of-Plus.lisp" :ld-error-action :error)
1916
(:executable-counterpart build-values-by-rns)
1917
(:type-prescription build-values-by-rns)
1918
(:induction build-values-by-rns)
1919
(:definition build-values-by-rns)
1920
posp-all posp mod mod-+-exp mod-prod-makes-same-residues))
1922
(in-theory (disable mod floor))
1924
(defun sum-list (vl2 vl3 rns)
1927
(cons (mod (+ (car vl2) (car vl3)) (car rns))
1928
(sum-list (cdr vl2) (cdr vl3) (cdr rns)))))
1930
(defthm sum-correspondence-by-put-list
1936
(equal (build-values-by-rns (+ gval1 gval2) rns)
1938
(build-values-by-rns gval1 rns)
1939
(build-values-by-rns gval2 rns)
1941
:hints (("Goal" :induct t)))
1946
(defthm sum-correspondence-by-put-list-2-fin
1952
(equal (build-values-by-rns (mod (+ gval1 gval2) (prod rns)) rns)
1954
(build-values-by-rns gval1 rns)
1955
(build-values-by-rns gval2 rns)
1958
(in-theory (disable mod-prod-makes-same-residues))
1962
(in-theory (disable mod floor mod-+-exp mod-prod-makes-same-residues))
1970
(defthm sum-correspondence-by-put-list-h
1975
(integer>1-listp rns))
1976
(equal (build-values-by-rns (mod (+ gval1 gval2) (prod rns)) rns)
1978
(build-values-by-rns gval1 rns)
1979
(build-values-by-rns gval2 rns)
1981
:hints (("Goal" :use (sum-correspondence-by-put-list-2-fin greater-one-means-greater-zero))))
1985
(defthm a-boolean-has-same-rnss-than-list-of-itself
1989
(or (equal val 0) (equal val 1))
1990
(integer>1-listp rns))
1992
(build-values-by-rns val rns)
1993
(make-n-list val (len rns))))
1994
:hints (("Goal" :in-theory (enable mod-x-y-=-x-exp))))
1999
(defthm sum-correspondence-by-put-list-on-boolean
2004
(or (equal gval2 0) (equal gval2 1))
2005
(integer>1-listp rns))
2006
(equal (build-values-by-rns (mod (+ gval1 gval2) (prod rns)) rns)
2008
(build-values-by-rns gval1 rns)
2009
(make-n-list gval2 (len rns))
2011
:hints (("Goal" :in-theory nil
2012
:use (sum-correspondence-by-put-list-h
2013
(:instance a-boolean-has-same-rnss-than-list-of-itself (val gval2))))))
2017
(defun equal-sum-and-updates (reslist par1list par2list par3list primelist mem memafterputs)
2022
(get-cell (car reslist) memafterputs)
2029
(equal-sum-and-updates
2042
(defthm equal-sum-and-updates-have-same-attributes
2045
(true-listp rtmvars1)
2046
(true-listp rtmvarsres)
2047
(equal (len rtmvars1) (len rtmvarsres))
2048
(equal-sum-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns rtmmem rtmmemafter))
2049
(equal (var-attributes rtmvarsres rtmmemafter) (var-attributes rtmvars1 rtmmem))))
2051
(in-theory (enable sum-list))
2053
(defthm equal-sum-and-updates-have-values-that-are-sum-lists
2056
(equal (len rtmvars1) (len rtmvarsres))
2057
(equal (len rtmvars2) (len rtmvarsres))
2058
(equal (len rtmvars3) (len rtmvarsres))
2059
(equal-sum-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns rtmmem rtmmemafter))
2060
(equal (var-values rtmvarsres rtmmemafter)
2062
(var-values rtmvars2 rtmmem)
2063
(var-values rtmvars3 rtmmem)
2065
:hints ( ("Subgoal *1/2" :in-theory (enable var-value get-cell make-cell))))
2071
(defthm behaviour-of-sum-and-update-norest
2074
(var-attribute (sum-and-update-norest c1 c2 c3 mem))
2075
(var-attribute (get-cell c1 mem)))
2077
(var-value (sum-and-update-norest c1 c2 c3 mem))
2080
(var-value (get-cell c2 mem))
2081
(var-value (get-cell c3 mem)))
2084
(var-type (sum-and-update-norest c1 c2 c3 mem))
2085
(var-type (get-cell c1 mem))))
2086
:hints (("Goal" :in-theory (enable var-type var-value var-attribute make-cell))))
2091
(defthm defexpansion
2093
(not (null (var-value gcell)))
2095
(equal-values-and-attributes gcell rtmvars rtmmem 'Int)
2097
(equal-values (var-values rtmvars rtmmem)
2098
(build-values-by-rns (var-value gcell) *rns*))
2099
(equal-elements (var-attribute gcell)
2100
(var-attributes rtmvars rtmmem)))))
2101
:hints (("Goal" :in-theory '((:definition equal-values-and-attributes)
2102
(:definition apply-direct-rns-to-value-according-to-type))
2103
:use (:instance build-values-by-rns-extended-behaves-standardly-on-non-nils
2104
(gem-value (var-value gcell))
2108
(defthm if-gem-is-sum-and-update-inf-every-rtm-var-is-sum-and-update-then-equal-values-is-kept
2111
(true-listp rtmvars1)
2112
(true-listp rtmvarsres)
2113
(equal (len rtmvars1) (len rtmvarsres))
2114
(equal (len rtmvars2) (len rtmvarsres))
2115
(equal (len rtmvars3) (len rtmvarsres))
2116
(not (null (var-value (get-cell gvar1 gemmem))))
2117
(integerp (var-value (get-cell gvar2 gemmem)))
2118
(integerp (var-value (get-cell gvar3 gemmem)))
2119
(equal-sum-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 *rns* rtmmem rtmmemafter)
2120
(equal-values-and-attributes (get-cell gvar1 gemmem) rtmvars1 rtmmem 'Int)
2121
(equal-values-and-attributes (get-cell gvar2 gemmem) rtmvars2 rtmmem 'Int)
2122
(equal-values-and-attributes (get-cell gvar3 gemmem) rtmvars3 rtmmem 'Int))
2123
(equal-values-and-attributes
2124
(sum-and-update-norest gvar1 gvar2 gvar3 gemmem)
2129
:in-theory (union-theories (current-theory 'ground-zero)
2131
(:definition integer>1-listp)
2132
(:definition equal-values)
2133
(:rewrite defexpansion)))
2135
(:instance greater-one-means-greater-zero (rns *rns*))
2136
(:instance equal-sum-and-updates-have-values-that-are-sum-lists (rns *rns*))
2137
(:instance equal-sum-and-updates-have-same-attributes (rns *rns*))
2138
(:instance sum-correspondence-by-put-list-h
2139
(gval1 (var-value (get-cell gvar2 gemmem)))
2140
(gval2 (var-value (get-cell gvar3 gemmem)))
2142
(:instance behaviour-of-sum-and-update-norest
2155
(defthm if-a-var-value-is-same-then-var-values-are-list-of
2157
(equal (var-value (get-cell (car rtmvars) rtmmem)) (var-value gcell))
2158
(equal-values (var-values (make-n-list (car rtmvars) (len rns)) rtmmem)
2159
(make-n-list (var-value gcell) (len rns)))))
2161
(defthm if-a-var-attribute-is-same-then-var-attributes-are-list-of
2163
(equal (var-attribute (get-cell (car rtmvars) rtmmem)) (var-attribute gcell))
2165
(var-attribute gcell)
2166
(var-attributes (make-n-list (car rtmvars) (len rns)) rtmmem))))
2170
(defthm defexpansion-bool-values
2172
(or (equal (var-value gcell) 0)
2173
(equal (var-value gcell) 1))
2175
(equal-values-and-attributes gcell rtmvars rtmmem 'Bool)
2176
(equal-values (var-values (make-n-list (car rtmvars) (len *rns*)) rtmmem)
2177
(build-values-by-rns (var-value gcell) *rns*))))
2178
:hints (("Goal" :use ( (:instance if-a-var-value-is-same-then-var-values-are-list-of
2184
(defthm equal-values-on-list-entails-equality-on-first-els
2189
(equal-values (var-values (make-n-list el n) mem)
2190
(make-n-list val n)))
2191
(equal-values (var-values (list el) mem)
2193
:hints (("Subgoal *1/3'" :use ( (:instance make-n-list (el el) (n 1))
2194
(:instance make-n-list (el val) (n 1)) ))))
2199
(is-mem-cell-p gcell)
2201
(equal (var-type gcell) 'Bool)
2202
(equal (var-type gcell) 'Int)))
2203
:hints (("Goal" :in-theory (enable my-or-2)))
2209
(is-mem-cell-p gcell)
2210
(equal (var-type gcell) 'Bool))
2212
(integerp (var-value gcell))
2213
(or (equal (var-value gcell) 0)
2214
(equal (var-value gcell) 1))))
2220
(is-mem-cell-p gcell)
2221
(equal (var-type gcell) 'Int))
2222
(integerp (var-value gcell)))
2226
(defthm defexpansion-bool-values-inv
2229
(is-mem-cell-p gcell)
2230
(equal (var-type gcell) 'Bool)
2231
(equal (type-expected rtmvars) (var-type gcell)))
2233
(equal-values (var-values (eventually-make-list rtmvars (len *rns*)) rtmmem)
2234
(build-values-by-rns (var-value gcell) *rns*))
2236
(var-values rtmvars rtmmem)
2237
(apply-direct-rns-to-value-according-to-type gcell (var-type gcell)))))
2238
:hints (("Goal" :use (bool-cell
2239
(:instance equal-values-on-list-entails-equality-on-first-els
2243
(val (var-value gcell)))
2244
(:instance a-boolean-has-same-rnss-than-list-of-itself
2245
(val (var-value gcell)) (rns *rns*))))))
2250
(defthm defexpansion-bool-attrs-1
2252
(equal-values-and-attributes gcell rtmvars rtmmem 'Bool)
2253
(equal (var-attribute (get-cell (car rtmvars) rtmmem)) (var-attribute gcell))))
2256
(defthm defexpansion-bool-attrs
2258
(equal-values-and-attributes gcell rtmvars rtmmem 'Bool)
2260
(var-attribute gcell)
2261
(var-attributes (make-n-list (car rtmvars) (len *rns*)) rtmmem)))
2262
:hints (("Goal" :use ( defexpansion-bool-attrs-1
2263
(:instance if-a-var-attribute-is-same-then-var-attributes-are-list-of
2267
(defthm defexpansion-bool-attrs-inv-1
2269
(equal (type-expected rtmvars) 'Bool)
2271
(var-attributes rtmvars rtmmem)
2272
(list (var-attribute (get-cell (car rtmvars) rtmmem)))))
2273
:hints (("Subgoal 1'" :use (:theorem (implies
2274
(and (true-listp rtmvars2)
2275
(equal (+ 1 (len rtmvars2)) 1))
2279
(defthm defexpansion-bool-attrs-inv-2
2282
(equal (type-expected rtmvars) 'Bool)
2283
(equal val (var-attribute (get-cell (car rtmvars) rtmmem))))
2284
(equal-elements val (var-attributes rtmvars rtmmem))))
2287
(defthm defexpansion-bool-attrs-inv-3
2295
(var-attributes (make-n-list car-rtmvars n) rtmmem))
2298
(var-attribute (get-cell car-rtmvars rtmmem)))))
2299
:hints (("Subgoal *1/3'" :use (:instance make-n-list (el car-rtmvars) (n 1))))
2303
(defthm defexpansion-bool-attrs-inv
2306
(equal (var-type gcell) 'Bool)
2307
(equal (type-expected rtmvars) (var-type gcell)))
2310
(var-attribute gcell)
2311
(var-attributes (make-n-list (car rtmvars) (len *rns*)) rtmmem))
2313
(var-attribute gcell)
2314
(var-attributes rtmvars rtmmem))))
2315
:hints (("Goal" :use
2316
( defexpansion-bool-attrs-inv-1
2317
defexpansion-bool-attrs-inv-2
2318
(:instance defexpansion-bool-attrs-inv-3
2320
(car-rtmvars (car rtmvars))
2321
(val (var-attribute gcell)))))))
2323
(defthm defexpansion-bool
2326
(is-mem-cell-p gcell)
2327
(equal (var-type gcell) 'Bool)
2328
(equal (type-expected rtmvars) (var-type gcell)))
2330
(equal-values-and-attributes gcell rtmvars rtmmem 'Bool)
2332
(equal-values (var-values (make-n-list (car rtmvars) (len *rns*)) rtmmem)
2333
(build-values-by-rns (var-value gcell) *rns*))
2335
(var-attribute gcell)
2336
(var-attributes (make-n-list (car rtmvars) (len *rns*)) rtmmem)))))
2337
:hints (("Goal" :use
2339
defexpansion-bool-attrs
2340
defexpansion-bool-values
2341
defexpansion-bool-attrs-inv
2342
defexpansion-bool-values-inv))))
2348
(defthm defexpansion-generic-bool
2351
(is-mem-cell-p gcell)
2352
(equal (var-type gcell) 'Bool)
2353
(equal (type-expected rtmvars) (var-type gcell)))
2355
(equal-values-and-attributes gcell rtmvars rtmmem (var-type gcell))
2357
(equal-values (var-values (eventually-make-list rtmvars (len *rns*)) rtmmem)
2358
(build-values-by-rns (var-value gcell) *rns*))
2359
(equal-elements (var-attribute gcell)
2360
(var-attributes (eventually-make-list rtmvars (len *rns*)) rtmmem)))))
2361
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero)
2362
'((:definition type-expected)
2363
(:definition eventually-make-list)))
2364
:use (defexpansion-bool bool-cell))))
2366
(defthm defexpansion-generic-int
2369
(is-mem-cell-p gcell)
2370
(equal (var-type gcell) 'Int)
2371
(equal (type-expected rtmvars) (var-type gcell)))
2373
(equal-values-and-attributes gcell rtmvars rtmmem (var-type gcell))
2375
(equal-values (var-values (eventually-make-list rtmvars (len *rns*)) rtmmem)
2376
(build-values-by-rns (var-value gcell) *rns*))
2377
(equal-elements (var-attribute gcell)
2378
(var-attributes (eventually-make-list rtmvars (len *rns*)) rtmmem)))))
2379
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero)
2380
'((:definition type-expected)
2381
(:definition eventually-make-list)))
2382
:use (defexpansion int-cell))))
2387
(defthm defexpansion-generic
2390
(is-mem-cell-p gcell)
2391
(equal (type-expected rtmvars) (var-type gcell)))
2393
(equal-values-and-attributes gcell rtmvars rtmmem (var-type gcell))
2395
(equal-values (var-values (eventually-make-list rtmvars (len *rns*)) rtmmem)
2396
(build-values-by-rns (var-value gcell) *rns*))
2397
(equal-elements (var-attribute gcell)
2398
(var-attributes (eventually-make-list rtmvars (len *rns*)) rtmmem)))))
2400
:cases ( (equal (var-type gcell) 'Bool)
2401
(equal (var-type gcell) 'Int) ))
2402
("Subgoal 3" :use cell-types)
2403
("Subgoal 2" :use defexpansion-generic-bool)
2404
("Subgoal 1" :use defexpansion-generic-int)))
2411
(defthm if-gem-is-sum-and-update-inf-every-rtm-var-is-sum-and-update-then-equal-values-is-kept-g
2414
(true-listp rtmvars1)
2415
(true-listp rtmvarsres)
2416
(equal (len rtmvars1) (len rtmvarsres))
2417
(equal (len (eventually-make-list rtmvars2 (len *rns*))) (len rtmvarsres))
2418
(equal (len (eventually-make-list rtmvars3 (len *rns*))) (len rtmvarsres))
2419
(equal (var-type (get-cell gvar2 gemmem)) (type-expected rtmvars2))
2420
(equal (var-type (get-cell gvar3 gemmem)) (type-expected rtmvars3))
2421
(is-mem-cell-p (get-cell gvar1 gemmem))
2422
(equal (var-type (get-cell gvar1 gemmem)) 'Int)
2423
(is-mem-cell-p (get-cell gvar2 gemmem))
2424
(is-mem-cell-p (get-cell gvar3 gemmem))
2425
(equal-sum-and-updates
2428
(eventually-make-list rtmvars2 (len *rns*))
2429
(eventually-make-list rtmvars3 (len *rns*))
2430
*rns* rtmmem rtmmemafter)
2431
(equal-values-and-attributes (get-cell gvar1 gemmem) rtmvars1 rtmmem 'Int)
2432
(equal-values-and-attributes (get-cell gvar2 gemmem) rtmvars2 rtmmem (var-type (get-cell gvar2 gemmem)))
2433
(equal-values-and-attributes (get-cell gvar3 gemmem) rtmvars3 rtmmem (var-type (get-cell gvar3 gemmem))))
2434
(equal-values-and-attributes
2435
(sum-and-update-norest gvar1 gvar2 gvar3 gemmem)
2440
:in-theory (union-theories (current-theory 'ground-zero)
2441
'((:definition integer>1-listp)
2442
(:definition equal-values)
2443
(:definition is-mem-cell-p)
2444
(:rewrite defexpansion)))
2446
(:instance defexpansion-generic
2447
(gcell (get-cell gvar2 gemmem))
2449
(:instance defexpansion-generic
2450
(gcell (get-cell gvar3 gemmem))
2452
(:instance equal-sum-and-updates-have-values-that-are-sum-lists
2453
(rtmvars2 (eventually-make-list rtmvars2 (len *rns*)))
2454
(rtmvars3 (eventually-make-list rtmvars3 (len *rns*)))
2456
(:instance equal-sum-and-updates-have-same-attributes
2457
(rtmvars2 (eventually-make-list rtmvars2 (len *rns*)))
2458
(rtmvars3 (eventually-make-list rtmvars3 (len *rns*)))
2460
(:instance sum-correspondence-by-put-list-h
2461
(gval1 (var-value (get-cell gvar2 gemmem)))
2462
(gval2 (var-value (get-cell gvar3 gemmem)))
2464
(:instance behaviour-of-sum-and-update-norest
2474
(in-theory (disable sum-list sum-correspondence-by-put-list
2475
equal-sum-and-updates-have-same-attributes
2476
equal-sum-and-updates-have-values-that-are-sum-lists
2477
behaviour-of-sum-and-update-norest
2479
if-a-var-value-is-same-then-var-values-are-list-of
2480
if-a-var-attribute-is-same-then-var-attributes-are-list-of
2481
defexpansion-generic-bool
2482
defexpansion-generic-int
2483
defexpansion-generic
2484
defexpansion-bool-values-inv
2485
defexpansion-bool-values
2486
defexpansion-bool-attrs-inv
2487
defexpansion-bool-attrs-inv-1
2488
defexpansion-bool-attrs-inv-2
2489
defexpansion-bool-attrs
2490
defexpansion-bool-attrs-1
2491
equal-values-on-list-entails-equality-on-first-els
2498
(defun execute-n-rtm-adds (st n)
2504
(par1 (nth (pcc st) (code st)))
2505
(par2 (nth (pcc st) (code st)))
2506
(par3 (nth (pcc st) (code st)))
2507
(par4 (nth (pcc st) (code st)))
2512
(defthm all-rtm-adds-means-only-adds-are-executed
2514
(all-rtm-adds-for-n-steps st n)
2516
(execute-n-rtm-adds st n)
2517
(execute-n-instructions st n)))
2518
:hints (("Goal" :in-theory (disable rtm-add member-equal nth par1 par2 par3))))
2521
(defun adds-list-n (l1 l2 l3 l4 mem n)
2524
(adds-list-n (cdr l1) (cdr l2) (cdr l3) (cdr l4)
2542
(in-theory (disable member-equal))
2545
(in-theory (enable make-cell))
2549
(defthm execute-n-rtm-adds-tantamount-to-add-list-n
2552
(all-rtm-adds-for-n-steps st n)
2556
(mem (execute-n-rtm-adds st n))
2565
(("Goal" :induct t )
2566
("Subgoal *1/2.2" :in-theory '((:definition all-rtm-adds-for-n-steps)
2567
(:definition execute-instruction)
2568
(:definition rtm-add)
2569
(:definition make-state)
2573
:use ( execute-n-rtm-adds
2574
(:instance adds-list-n
2575
(l1 (listpars1 st n))
2576
(l2 (listpars2 st n))
2577
(l3 (listpars3 st n))
2578
(l4 (listpars4 st n))
2580
lemma12-lp1r lemma12-lp2r lemma12-lp3r lemma12-lp4r
2582
(IMPLIES (AND (ALL-RTM-ADDS-FOR-N-STEPS ST N)
2585
(equal (mem (execute-instruction st))
2586
(PUT-CELL (CAR (LISTPARS1 ST N))
2587
(SUM-AND-UPDATE (CAR (LISTPARS1 ST N))
2588
(CAR (LISTPARS2 ST N))
2589
(CAR (LISTPARS3 ST N))
2590
(CAR (LISTPARS4 ST N))
2593
executing-rtm-instruction-retrieves-a-rtm-state-from-rtm-state
2594
instruction-incrementing-pvv))))
2597
(in-theory (disable lemma12-lp1r lemma12-lp2r lemma12-lp3r lemma12-lp4r ))
2608
(defun adds-list-e (c1 c2 c3 c4 mem)
2617
(put-cell (car c1) (sum-and-update (car c1) (car c2) (car c3) (car c4) mem) mem))))
2621
(defthm adds-list-e-is-adds-list-n
2622
(equal (adds-list-e c1 c2 c3 c4 mem) (adds-list-n c1 c2 c3 c4 mem (len c1)))
2627
(defthm execute-n-instructions-tantamount-to-add-list-e
2632
(all-rtm-adds-for-n-steps st n)
2636
(mem (execute-n-instructions st n))
2643
:hints (("Goal" :in-theory nil
2644
:use ((:instance adds-list-e-is-adds-list-n
2645
(c1 (listpars1 st n))
2646
(c2 (listpars2 st n))
2647
(c3 (listpars3 st n))
2648
(c4 (listpars4 st n))
2650
execute-n-rtm-adds-tantamount-to-add-list-n
2651
all-rtm-adds-means-only-adds-are-executed
2652
length-of-listpars1-n-is-n))))
2663
(defthm not-in-list-untouched-by-adds-list-e
2665
(not (member-equal-bool v l1))
2666
(equal (get-cell v (adds-list-e l1 l2 l3 l4 mem)) (get-cell v mem)))
2667
:hints (("Goal" :in-theory (disable sum-and-update))))
2669
(defthm not-in-list-untouched-by-adds-list-e-1
2671
(not (member-equal-bool (car l1) (cdr l1)))
2672
(equal (get-cell (car l1) (adds-list-e (cdr l1) (cdr l2) (cdr l3) (cdr l4) mem))
2673
(get-cell (car l1) mem))))
2676
(defthm sum-and-update-independent-from-firstbn
2679
(not (member-equal-bool (nth idx l1) (firstn idx l1)))
2680
(not (member-equal-bool (nth idx l2) (firstn idx l1)))
2681
(not (member-equal-bool (nth idx l3) (firstn idx l1))))
2682
(equal (sum-and-update
2687
(adds-list-e (firstn idx l1) (firstn idx l2) (firstn idx l3) (firstn idx l4) mem))
2697
(defthm adds-list-decomp
2705
(adds-list-e l1 l2 l3 l4 mem)
2706
(adds-list-e (nthcdr idx l1) (nthcdr idx l2) (nthcdr idx l3) (nthcdr idx l4)
2707
(adds-list-e (firstn idx l1) (firstn idx l2) (firstn idx l3) (firstn idx l4) mem))))
2708
:hints (("Goal" :in-theory (disable sum-and-update))))
2711
(defthm if-el-does-not-appear-after-its-position-then-adds-list-e-produces-its-sum
2714
(not (member-equal-bool (nth idx l1) (cdr (nthcdr idx l1))))
2720
(get-cell (nth idx l1) (adds-list-e l1 l2 l3 l4 mem))
2726
(adds-list-e (firstn idx l1) (firstn idx l2) (firstn idx l3) (firstn idx l4) mem))))
2727
:hints (("Goal" :in-theory (disable sum-and-update))))
2732
(defthm rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables
2737
(no-duplicates-p (append-lists ll))
2741
(in-range idx (nth gem1 ll))
2742
(in-range idx (nth gem2 ll))
2743
(in-range idx (nth gem3 ll))
2746
(get-cell (nth idx (nth gem1 ll)) (adds-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem))
2747
(sum-and-update (nth idx (nth gem1 ll)) (nth idx (nth gem2 ll)) (nth idx (nth gem3 ll)) (nth idx rns) mem)))
2748
:hints (("Goal" :in-theory (disable sum-and-update)
2750
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
2751
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
2752
if-el-does-not-appear-after-its-position-then-adds-list-e-produces-its-sum
2753
(:instance adds-list-decomp
2754
(l1 (nth gem1 ll)) (l2 (nth gem2 ll)) (l3 (nth gem3 ll)))
2755
(:instance sum-and-update-independent-from-firstbn
2756
(l1 (nth gem1 ll)) (l2 (nth gem2 ll)) (l3 (nth gem3 ll)))))))
2760
(defun index-different-sum-and-updates (rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-add)
2764
( (not (equal (get-cell (car rtmvarsres) mem-after-add)
2765
(sum-and-update (car rtmvars1) (car rtmvars2) (car rtmvars3) (car rns) mem)))
2768
(1+ (index-different-sum-and-updates
2777
(defthm if-bad-index-in-range-thne-must-be-nonsumandupdate
2778
(let ((bad-idx (index-different-sum-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-add)))
2780
(in-range bad-idx rtmvarsres)
2782
(get-cell (nth bad-idx rtmvarsres) mem-after-add)
2784
(nth bad-idx rtmvars1)
2785
(nth bad-idx rtmvars2)
2786
(nth bad-idx rtmvars3)
2789
:hints (("Goal" :in-theory (disable get-cell sum-and-update))))
2792
(defthm if-bad-index-not-in-range-then-every-equalsumandupdate
2793
(let ((bad-idx (index-different-sum-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-add)))
2794
(implies (and (true-listp rtmvarsres)
2795
(not (in-range bad-idx rtmvarsres)))
2796
(equal-sum-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-add))))
2799
(defthm rtm-variable-of-adds-list-e-is-sum-and-updates
2804
(no-duplicates-p (append-lists ll))
2805
(equal (len (nth gem1 ll)) (len (nth gem2 ll)))
2806
(equal (len (nth gem1 ll)) (len (nth gem3 ll)))
2807
(equal (len (nth gem1 ll)) (len rns))
2811
(true-listp (nth gem1 ll)))
2812
(equal-sum-and-updates (nth gem1 ll) (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem
2813
(adds-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem)))
2814
:hints (("Goal" :use (:instance rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables
2815
(idx (index-different-sum-and-updates
2822
(adds-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem)))))
2823
("Goal'" :cases ( (in-range (index-different-sum-and-updates
2830
(adds-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem))
2832
("Subgoal 1" :in-theory '((:definition in-range)
2833
(:rewrite if-bad-index-in-range-thne-must-be-nonsumandupdate)))
2834
("Subgoal 2" :in-theory '((:rewrite if-bad-index-not-in-range-then-every-equalsumandupdate)))))
2839
(defthm any-element-of-make-list-does-not-appear-into-other-lists
2844
(no-duplicates-p (append-lists ll))
2847
(not (equal gem1 gem2))
2848
(equal (len (nth gem1 ll)) 1)
2849
(in-range idx (make-n-list (car (nth gem1 ll)) n)))
2850
(not (member-equal-bool
2851
(nth idx (make-n-list (car (nth gem1 ll)) n))
2853
:hints (("Goal" :use
2856
el-of-makelist-is-el
2857
(el (car (nth gem1 ll))))
2858
(:instance generalized-disjunctivity-unordered-2
2859
(idx1 gem1) (idx2 gem2) (el1 (car (nth gem1 ll)))))))
2862
(defthm firstns-do-not-cotain-el-of-make-n-list-if-diff
2867
(no-duplicates-p (append-lists ll))
2870
(not (equal gem1 gem2))
2871
(equal (len (nth gem1 ll)) 1)
2872
(in-range idx (make-n-list (car (nth gem1 ll)) n)))
2873
(not (member-equal-bool
2874
(nth idx (make-n-list (car (nth gem1 ll)) n))
2875
(firstn idx (nth gem2 ll)))))
2876
:hints (("Goal" :use
2878
(:instance no-member-holds-on-firstn
2879
(el (nth idx (make-n-list (car (nth gem1 ll)) n)))
2881
any-element-of-make-list-does-not-appear-into-other-lists))))
2885
(defthm rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-when-var-3-is-boolean
2891
(no-duplicates-p (append-lists ll))
2895
(not (equal gem1 gem3))
2896
(equal (len (nth gem3 ll)) 1)
2897
(in-range idx (nth gem1 ll))
2898
(in-range idx (nth gem2 ll))
2899
(in-range idx (make-n-list (car (nth gem3 ll)) n))
2902
(get-cell (nth idx (nth gem1 ll))
2906
(make-n-list (car (nth gem3 ll)) n)
2909
(nth idx (nth gem1 ll))
2910
(nth idx (nth gem2 ll))
2911
(nth idx (make-n-list (car (nth gem3 ll)) n))
2912
(nth idx rns) mem)))
2913
:hints (("Goal" :in-theory (disable sum-and-update)
2915
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem3) (gem2 gem1))
2916
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
2917
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
2918
(:instance adds-list-decomp
2921
(l3 (make-n-list (car (nth gem3 ll)) n))
2923
(:instance sum-and-update-independent-from-firstbn
2926
(l3 (make-n-list (car (nth gem3 ll)) n))
2929
(defthm rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-when-var-2-is-boolean
2935
(no-duplicates-p (append-lists ll))
2939
(not (equal gem1 gem2))
2940
(equal (len (nth gem2 ll)) 1)
2941
(in-range idx (nth gem1 ll))
2942
(in-range idx (nth gem3 ll))
2943
(in-range idx (make-n-list (car (nth gem2 ll)) n))
2946
(get-cell (nth idx (nth gem1 ll))
2949
(make-n-list (car (nth gem2 ll)) n)
2953
(nth idx (nth gem1 ll))
2954
(nth idx (make-n-list (car (nth gem2 ll)) n))
2955
(nth idx (nth gem3 ll))
2956
(nth idx rns) mem)))
2957
:hints (("Goal" :in-theory (disable sum-and-update)
2959
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem2) (gem2 gem1))
2960
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
2961
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
2962
(:instance adds-list-decomp
2964
(l2 (make-n-list (car (nth gem2 ll)) n))
2967
(:instance sum-and-update-independent-from-firstbn
2969
(l2 (make-n-list (car (nth gem2 ll)) n))
2973
(defthm rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-when-var-2and3-are-boolean
2979
(no-duplicates-p (append-lists ll))
2983
(not (equal gem1 gem2))
2984
(not (equal gem1 gem3))
2985
(equal (len (nth gem2 ll)) 1)
2986
(equal (len (nth gem3 ll)) 1)
2987
(in-range idx (nth gem1 ll))
2988
(in-range idx (make-n-list (car (nth gem2 ll)) n))
2989
(in-range idx (make-n-list (car (nth gem3 ll)) n))
2992
(get-cell (nth idx (nth gem1 ll))
2995
(make-n-list (car (nth gem2 ll)) n)
2996
(make-n-list (car (nth gem3 ll)) n)
2999
(nth idx (nth gem1 ll))
3000
(nth idx (make-n-list (car (nth gem2 ll)) n))
3001
(nth idx (make-n-list (car (nth gem3 ll)) n))
3002
(nth idx rns) mem)))
3003
:hints (("Goal" :in-theory (disable sum-and-update)
3005
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem2) (gem2 gem1))
3006
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem3) (gem2 gem1))
3007
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
3008
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
3009
(:instance adds-list-decomp
3011
(l2 (make-n-list (car (nth gem2 ll)) n))
3012
(l3 (make-n-list (car (nth gem3 ll)) n))
3014
(:instance sum-and-update-independent-from-firstbn
3016
(l2 (make-n-list (car (nth gem2 ll)) n))
3017
(l3 (make-n-list (car (nth gem3 ll)) n))
3023
(defthm rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-with-all-vars-types
3029
(no-duplicates-p (append-lists ll))
3033
(not (equal (len (nth gem1 ll)) 1))
3034
(in-range idx (nth gem1 ll))
3035
(in-range idx (eventually-make-list (nth gem2 ll) n))
3036
(in-range idx (eventually-make-list (nth gem3 ll) n))
3039
(get-cell (nth idx (nth gem1 ll))
3042
(eventually-make-list (nth gem2 ll) n)
3043
(eventually-make-list (nth gem3 ll) n)
3046
(nth idx (nth gem1 ll))
3047
(nth idx (eventually-make-list (nth gem2 ll) n))
3048
(nth idx (eventually-make-list (nth gem3 ll) n))
3049
(nth idx rns) mem)))
3050
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero)
3051
'((:definition eventually-make-list)))
3053
( (and (not (equal (len (nth gem3 ll)) 1)) (equal (len (nth gem2 ll)) 1))
3054
(and (equal (len (nth gem3 ll)) 1) (not (equal (len (nth gem2 ll)) 1)))
3055
(and (not (equal (len (nth gem3 ll)) 1)) (not (equal (len (nth gem2 ll)) 1)))
3056
(and (equal (len (nth gem3 ll)) 1) (equal (len (nth gem2 ll)) 1))))
3058
:use rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-when-var-2-is-boolean)
3060
:use rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-when-var-3-is-boolean)
3062
:use rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables)
3064
:use rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-when-var-2and3-are-boolean)))
3068
(defthm sum-and-updates-holding-for-every-variable-type
3072
(not (equal (len (nth gem1 ll)) 1))
3075
(no-duplicates-p (append-lists ll))
3076
(equal (len (nth gem1 ll)) (len (eventually-make-list (nth gem2 ll) n)))
3077
(equal (len (nth gem1 ll)) (len (eventually-make-list (nth gem3 ll) n)))
3078
(equal (len (nth gem1 ll)) (len rns))
3082
(true-listp (nth gem1 ll)))
3083
(equal-sum-and-updates
3086
(eventually-make-list (nth gem2 ll) n)
3087
(eventually-make-list (nth gem3 ll) n)
3091
(eventually-make-list (nth gem2 ll) n)
3092
(eventually-make-list (nth gem3 ll) n)
3094
:hints (("Goal" :use (:instance rtm-variable-of-adds-list-e-is-sum-of-correspondent-variables-with-all-vars-types
3095
(idx (index-different-sum-and-updates
3098
(eventually-make-list (nth gem2 ll) n)
3099
(eventually-make-list (nth gem3 ll) n)
3104
(eventually-make-list (nth gem2 ll) n)
3105
(eventually-make-list (nth gem3 ll) n)
3107
("Goal'" :cases ( (in-range (index-different-sum-and-updates
3110
(eventually-make-list (nth gem2 ll) n)
3111
(eventually-make-list (nth gem3 ll) n)
3116
(eventually-make-list (nth gem2 ll) n)
3117
(eventually-make-list (nth gem3 ll) n)
3120
("Subgoal 1" :in-theory '((:definition in-range)
3121
(:rewrite if-bad-index-in-range-thne-must-be-nonsumandupdate)))
3122
("Subgoal 2" :in-theory '((:rewrite if-bad-index-not-in-range-then-every-equalsumandupdate)))))
3126
(defthm lemma2-only-adds-in-rtm-add
3131
(in-range (pcc gstate) (code gstate))
3132
(in-range (pcc rstate) (code rstate))
3133
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3134
(good-translation-gem-rtm gstate rstate m))
3135
(all-rtm-adds-for-n-steps rstate (len *rns*)))
3136
:hints (("Goal" :expand
3137
( (good-translation-gem-rtm gstate rstate m)
3140
(in-range (pcc gstate) (code gstate))
3141
(in-range (pcc rstate) (code rstate)))
3146
(defthm cells-untouched-by-execute-on-other-cell-add
3151
(all-rtm-adds-for-n-steps st n)
3154
(not (member-equal-bool v (listpars1 st n))))
3155
(equal (get-cell v (mem st))
3156
(get-cell v (mem (execute-n-instructions st n)))))
3158
:use (execute-n-instructions-tantamount-to-add-list-e
3159
(:instance not-in-list-untouched-by-adds-list-e
3161
(l1 (listpars1 st n))
3162
(l2 (listpars2 st n))
3163
(l3 (listpars3 st n))
3164
(l4 (listpars4 st n))
3168
(defthm rtm-variable-of-other-cell-untouched-add
3171
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3174
(good-translation-gem-rtm gstate rstate m)
3175
(in-range (pcc gstate) (code gstate))
3176
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m)
3178
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3179
(assoc-equal gvar1 m)
3180
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
3181
(in-range idx1 (rtmintvars-i gvar1 m)))
3182
(equal (get-cell (nth idx1 (rtmintvars-i gvar1 m)) (mem rstate))
3183
(get-cell (nth idx1 (rtmintvars-i gvar1 m)) (mem (execute-n-instructions rstate (len *rns*))))))
3184
:hints (("Goal" :in-theory (current-theory 'ground-zero)
3185
:expand ( (in-range (pcc gstate) (code gstate))
3186
(good-translation-gem-rtm gstate rstate m) )
3188
(:instance lemma1-different-vars-do-not-belong (gvar2 (par1 (nth (pcc gstate) (code gstate)))))
3189
(:instance cells-untouched-by-execute-on-other-cell-add (st rstate) (n (len *rns*))
3190
(v (nth idx1 (rtmintvars-i gvar1 m))))))))
3192
(defthm rtm-variables-of-other-cell-untouched-add
3195
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3198
(good-translation-gem-rtm gstate rstate m)
3199
(in-range (pcc gstate) (code gstate))
3200
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m)
3202
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3203
(assoc-equal gvar1 m)
3204
(true-listp (rtmintvars-i gvar1 m))
3205
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate))))))
3207
(rtmintvars-i gvar1 m) (mem rstate) (mem (execute-n-instructions rstate (len *rns*)))))
3208
:hints (("Goal" :in-theory nil
3209
:use ( (:instance rtm-variable-of-other-cell-untouched-add
3210
(idx1 (idx-different-cell
3211
(rtmintvars-i gvar1 m)
3213
(mem (execute-n-instructions rstate (len *rns*)))))) ))
3214
("Goal'" :cases ( (in-range
3216
(rtmintvars-i gvar1 m)
3218
(mem (execute-n-instructions rstate (len *rns*))))
3219
(rtmintvars-i gvar1 m))))
3220
("Subgoal 2" :in-theory '((:rewrite if-bad-index-not-in-range-then-every-equal)))
3221
("Subgoal 1" :in-theory '((:forward-chaining if-bad-index-in-range-then-cells-must-be-different)))))
3226
(defthm properies-of-type-and-existence-of-current-args-add
3230
(in-range (pcc gstate) (code gstate))
3231
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add))
3233
(equal (var-type (get-cell (par1 (nth (pcc gstate) (code gstate))) (mem gstate))) 'Int)
3234
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) (mem gstate))
3235
(assoc-equal (par2 (nth (pcc gstate) (code gstate))) (mem gstate))
3236
(assoc-equal (par3 (nth (pcc gstate) (code gstate))) (mem gstate))))
3237
:hints (("Goal" :in-theory (enable get-cell)
3238
:use (:instance in-range-instruction-is-gem-instruction
3240
(code (code gstate))
3241
(mem (mem gstate)))))
3245
(defthm par1-of-current-instruction-is-into-mapping-add
3248
(vars-inclusion (mem gstate) m)
3250
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3251
(in-range (pcc gstate) (code gstate)))
3252
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m))
3253
:hints (("Goal" :in-theory (enable get-cell)
3254
:use (properies-of-type-and-existence-of-current-args-add
3255
(:instance inclusion-trans
3256
(v (par1 (nth (pcc gstate) (code gstate))))
3259
(:instance in-range-instruction-is-gem-instruction
3261
(code (code gstate))
3262
(mem (mem gstate)))))))
3266
(defthm teorema-main-con-pcc-in-range-su-variabile-non-interessata-final-add
3269
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3270
(good-translation-gem-rtm gstate rstate m)
3271
(vars-inclusion (mem gstate) m)
3273
(assoc-equal gvar1 m)
3276
(in-range (pcc gstate) (code gstate))
3277
(in-range (pcc rstate) (code rstate))
3278
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
3279
(m-correspondent-values-p m (mem gstate) (mem rstate))
3280
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3281
(correct-wrt-arity m (mem gstate)))
3282
(equal-values-and-attributes
3283
(get-cell gvar1 (mem (execute-instruction gstate)))
3284
(rtmintvars-i gvar1 m)
3285
(mem (execute-n-instructions rstate (len *rns*)))
3288
:in-theory '((:definition good-translation-gem-rtm))
3290
par1-of-current-instruction-is-into-mapping-add
3291
(:instance correct-wrt-arity-has-rtmintvars-i-tl (mem (mem gstate)))
3292
(:instance m-correspondent-values-implies-equal-values-and-attribus
3293
(memgstate (mem gstate)) (memrstate (mem rstate)))
3294
(:instance in-range (idx (pcc gstate)) (l (code gstate)))
3295
(:instance in-range (idx (pcc rstate)) (l (code rstate)))
3296
rtm-variables-of-other-cell-untouched-add
3297
teorema-main-con-pcc-in-range-su-variabile-non-interessata
3298
(:instance equal-get-cells-implies-equal-values-and-attributes-still-works
3299
(gemcell (get-cell gvar1 (mem gstate)))
3300
(lcell (rtmintvars-i gvar1 m))
3302
(mem2 (mem (execute-n-instructions rstate (len *rns*))))
3303
(type (type-i gvar1 m)))))))
3306
(defthm teorema-main-con-pcc-in-range-su-variabile-interessata-add
3311
(in-range (pcc gstate) (code gstate))
3312
(in-range (pcc rstate) (code rstate))
3313
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3314
(good-translation-gem-rtm gstate rstate m))
3316
(mem (execute-n-instructions rstate (len *rns*)))
3318
(rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)
3319
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
3320
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
3324
:in-theory (union-theories (current-theory 'ground-zero) '((:definition in-range)))
3325
:use (good-translation-gem-rtm
3326
lemma2-only-adds-in-rtm-add
3327
(:instance execute-n-instructions-tantamount-to-add-list-e
3338
(vars-inclusion (mem gstate) m)
3340
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3341
(in-range (pcc gstate) (code gstate)))
3343
(in-range (pos-equal-0 (par1 (nth (pcc gstate) (code gstate))) m) m)
3344
(in-range (pos-equal-0 (par2 (nth (pcc gstate) (code gstate))) m) m)
3345
(in-range (pos-equal-0 (par3 (nth (pcc gstate) (code gstate))) m) m)))
3347
:use (properies-of-type-and-existence-of-current-args-add
3348
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3349
(v (par1 (nth (pcc gstate) (code gstate)))))
3350
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3351
(v (par2 (nth (pcc gstate) (code gstate)))))
3352
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3353
(v (par3 (nth (pcc gstate) (code gstate)))))
3354
(:instance assoc-means-pos-in-range
3355
(el (par1 (nth (pcc gstate) (code gstate))))
3357
(:instance assoc-means-pos-in-range
3358
(el (par2 (nth (pcc gstate) (code gstate))))
3360
(:instance assoc-means-pos-in-range
3361
(el (par3 (nth (pcc gstate) (code gstate))))
3370
(in-range (pcc gstate) (code gstate))
3371
(in-range (pcc rstate) (code rstate))
3372
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3373
(good-translation-gem-rtm gstate rstate m))
3375
(equal (len (rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)) (len *rns*))
3376
(equal (len (eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*))) (len *rns*))
3377
(equal (len (eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*))) (len *rns*))))
3379
:in-theory (union-theories (current-theory 'ground-zero) '((:definition in-range)))
3382
good-translation-gem-rtm
3383
(:instance length-of-listpars1-n-is-n (st rstate) (n (len *rns*)))
3384
(:instance length-of-listpars2-n-is-n (st rstate) (n (len *rns*)))
3385
(:instance length-of-listpars3-n-is-n (st rstate) (n (len *rns*))))))
3389
(defthm equal-sum-and-updates-after-n-instr
3393
(correct-wrt-arity m (mem gstate))
3396
(vars-inclusion (mem gstate) m)
3397
(in-range (pcc gstate) (code gstate))
3398
(in-range (pcc rstate) (code rstate))
3399
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3400
(good-translation-gem-rtm gstate rstate m)
3401
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3402
(assoc-equal gvar1 m)
3403
(equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
3404
(equal-sum-and-updates
3405
(rtmintvars-i gvar1 m)
3406
(rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)
3407
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
3408
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
3411
(mem (execute-n-instructions rstate (len *rns*)))))
3413
:in-theory (union-theories (current-theory 'ground-zero)
3414
'((:type-prescription retrieve-rtmvars)
3415
(:definition positive-list)
3416
(:definition positivep)
3417
(:definition in-range)))
3420
(:instance correct-wrt-arity-has-rtmintvars-i-tl (mem (mem gstate)))
3421
(:instance sum-and-updates-holding-for-every-variable-type
3423
(ll (retrieve-rtmvars m))
3425
(gem1 (pos-equal-0 (par1 (nth (pcc gstate) (code gstate))) m))
3426
(gem2 (pos-equal-0 (par2 (nth (pcc gstate) (code gstate))) m))
3427
(gem3 (pos-equal-0 (par3 (nth (pcc gstate) (code gstate))) m))
3432
teorema-main-con-pcc-in-range-su-variabile-interessata-add
3433
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
3434
(gvar (par1 (nth (pcc gstate) (code gstate)))))
3435
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
3436
(gvar (par2 (nth (pcc gstate) (code gstate)))))
3437
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
3438
(gvar (par3 (nth (pcc gstate) (code gstate)))))
3439
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
3440
(gvar (par4 (nth (pcc gstate) (code gstate)))))))))
3443
(defthm equal-sum-and-update-norest-afetr-one-instr
3447
(in-range (pcc gstate) (code gstate))
3448
(good-translation-gem-rtm gstate rstate m)
3449
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3450
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
3451
(equal gvar2 (par2 (nth (pcc gstate) (code gstate))))
3452
(equal gvar3 (par3 (nth (pcc gstate) (code gstate)))))
3453
(equal (get-cell gvar1 (mem (execute-instruction gstate)))
3454
(sum-and-update-norest gvar1 gvar2 gvar3 (mem gstate))))
3455
:hints (("Goal" :in-theory (e/d (put-cell get-cell)
3456
(par1 par2 par3 par4 opcode pcc code nth gem-instruction-list-p
3457
gen-eq-update sum-and-update sub-and-update sub-and-update-norest sum-and-update-norest))))
3461
(DEFTHM mem-cellity-of-current-gem-args-add
3463
(AND (GEM-STATEP GSTATE)
3464
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3465
(IN-RANGE (PCC GSTATE) (CODE GSTATE)))
3466
(AND (is-mem-cell-p (get-cell (PAR1 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))
3467
(is-mem-cell-p (get-cell (PAR2 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))
3468
(is-mem-cell-p (get-cell (PAR3 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))))
3472
(:INSTANCE IN-RANGE-INSTRUCTION-IS-GEM-INSTRUCTION
3474
(CODE (CODE GSTATE))
3475
(MEM (MEM GSTATE))))))
3479
(defthm type-is-for-pars-add
3483
(vars-inclusion (mem gstate) m)
3485
(correct-wrt-arity m (mem gstate))
3486
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3487
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
3488
(equal gvar2 (par2 (nth (pcc gstate) (code gstate))))
3489
(equal gvar3 (par3 (nth (pcc gstate) (code gstate))))
3490
(in-range (pcc gstate) (code gstate)))
3491
(equal (type-i gvar1 m) 'int))
3493
:in-theory (disable type-i-is-type-expected rtmintvars-i-is-pos-equal-0-of-retrieve-vars)
3494
:use ( properies-of-type-and-existence-of-current-args-add
3495
(:instance type-i-is-vartyper (gvar1 gvar1))
3496
(:instance type-i-is-vartyper (gvar1 gvar2))
3497
(:instance type-i-is-vartyper (gvar1 gvar3))
3498
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3499
(v (par1 (nth (pcc gstate) (code gstate)))))
3500
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3501
(v (par2 (nth (pcc gstate) (code gstate)))))
3502
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3503
(v (par3 (nth (pcc gstate) (code gstate))))))))
3507
(defthm m-correspondence-kept-on-same-gvar-add
3510
(good-translation-gem-rtm gstate rstate m)
3511
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3512
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
3514
(correct-wrt-arity m (mem gstate))
3517
(vars-inclusion (mem gstate) m)
3518
(in-range (pcc gstate) (code gstate))
3519
(in-range (pcc rstate) (code rstate))
3520
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3521
(assoc-equal gvar1 m)
3522
(m-correspondent-values-p m (mem gstate) (mem rstate)))
3523
(equal-values-and-attributes
3524
(get-cell gvar1 (mem (execute-instruction gstate)))
3525
(rtmintvars-i gvar1 m)
3526
(mem (execute-n-instructions rstate (len *rns*)))
3528
:hints (("Goal" :in-theory nil
3530
properies-of-type-and-existence-of-current-args-add
3531
mem-cellity-of-current-gem-args-add
3532
good-translation-gem-rtm
3533
(:instance type-i-is-vartyper (gvar1 gvar1) (mem (mem gstate)))
3534
(:instance type-i-is-vartyper (gvar1 (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
3535
(:instance type-i-is-vartyper (gvar1 (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
3536
(:instance type-i-is-type-expected (gvar gvar1) (mem (mem gstate)))
3537
(:instance type-i-is-type-expected (gvar (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
3538
(:instance type-i-is-type-expected (gvar (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
3539
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3540
(v (par1 (nth (pcc gstate) (code gstate)))))
3541
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3542
(v (par2 (nth (pcc gstate) (code gstate)))))
3543
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
3544
(v (par3 (nth (pcc gstate) (code gstate)))))
3546
equal-sum-and-update-norest-afetr-one-instr
3547
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
3548
(gvar3 (par3 (nth (pcc gstate) (code gstate))))
3551
(:instance correct-wrt-arity-has-rtmintvars-i-tl (mem (mem gstate)))
3552
(:instance type-is-for-pars-add
3553
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
3554
(gvar3 (par3 (nth (pcc gstate) (code gstate)))))
3555
(:instance m-correspondent-values-implies-equal-values-and-attribus
3556
(memgstate (mem gstate)) (memrstate (mem rstate))
3558
(:instance m-correspondent-values-implies-equal-values-and-attribus
3559
(memgstate (mem gstate)) (memrstate (mem rstate))
3560
(gvar1 (par2 (nth (pcc gstate) (code gstate)))))
3561
(:instance m-correspondent-values-implies-equal-values-and-attribus
3562
(memgstate (mem gstate)) (memrstate (mem rstate))
3563
(gvar1 (par3 (nth (pcc gstate) (code gstate)))))
3564
equal-sum-and-updates-after-n-instr
3566
if-gem-is-sum-and-update-inf-every-rtm-var-is-sum-and-update-then-equal-values-is-kept-g
3567
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
3568
(gvar3 (par3 (nth (pcc gstate) (code gstate))))
3569
(rtmvars1 (rtmintvars-i gvar1 m))
3570
(rtmvars2 (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m))
3571
(rtmvars3 (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m))
3572
(rtmvarsres (rtmintvars-i gvar1 m))
3573
(gemmem (mem gstate))
3574
(rtmmem (mem rstate))
3575
(rtmmemafter (mem (execute-n-instructions rstate (len *rns*)))))))))
3578
(defthm equal-values-correspondence-kept-by-any-execution-add
3581
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3582
(good-translation-gem-rtm gstate rstate m)
3584
(correct-wrt-arity m (mem gstate))
3587
(vars-inclusion (mem gstate) m)
3588
(in-range (pcc gstate) (code gstate))
3589
(in-range (pcc rstate) (code rstate))
3590
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3591
(assoc-equal gvar1 m)
3592
(m-correspondent-values-p m (mem gstate) (mem rstate)))
3593
(equal-values-and-attributes
3594
(get-cell gvar1 (mem (execute-instruction gstate)))
3595
(rtmintvars-i gvar1 m)
3596
(mem (execute-n-instructions rstate (len *rns*)))
3598
:hints (("Goal" :use (m-correspondence-kept-on-same-gvar-add
3599
teorema-main-con-pcc-in-range-su-variabile-non-interessata-final-add))))
3603
(defthm equal-values-correspondence-kept-by-any-execution-idxed-add
3606
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3607
(no-duplicates-p (retrieve-gemvars m))
3608
(good-translation-gem-rtm gstate rstate m)
3610
(correct-wrt-arity m (mem gstate))
3613
(vars-inclusion (mem gstate) m)
3614
(in-range (pcc gstate) (code gstate))
3615
(in-range (pcc rstate) (code rstate))
3616
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3618
(m-correspondent-values-p m (mem gstate) (mem rstate)))
3619
(equal-values-and-attributes
3620
(get-cell (car (nth idx m)) (mem (execute-instruction gstate)))
3622
(mem (execute-n-instructions rstate (len *rns*)))
3623
(type-i-idx m idx)))
3624
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero) '((:definition in-range)))
3632
(assoc-equal (car (nth idx m)) m))))
3634
(:instance type-i (gvar (car (nth idx m))))
3635
(:instance rtmintvars-i-is-cdr-of-nth-entry (gvar (car (nth idx m))))
3636
(:instance equal-values-correspondence-kept-by-any-execution-add (gvar1 (car (nth idx m))))
3637
(:instance no-duplicates-has-pos-equal-right-in-that-place (l m)))))
3640
(defthm m-correspondence-kept-by-any-execution-idxed-add
3643
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3644
(no-duplicates-p (retrieve-gemvars m))
3645
(good-translation-gem-rtm gstate rstate m)
3647
(correct-wrt-arity m (mem gstate))
3650
(vars-inclusion (mem gstate) m)
3651
(in-range (pcc gstate) (code gstate))
3652
(in-range (pcc rstate) (code rstate))
3653
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3654
(m-correspondent-values-p m (mem gstate) (mem rstate)))
3655
(m-correspondent-values-p
3657
(mem (execute-instruction gstate))
3658
(mem (execute-n-instructions rstate (len *rns*)))))
3659
:hints (("Goal" :use (:instance equal-values-correspondence-kept-by-any-execution-idxed-add
3660
(idx (bad-idx-eqv-va m
3661
(mem (execute-instruction gstate))
3662
(mem (execute-n-instructions rstate (len *rns*)))))))
3663
("Goal'" :cases ( (in-range (bad-idx-eqv-va m (mem (execute-instruction gstate))
3664
(mem (execute-n-instructions rstate (len *rns*)))) m)))
3665
("Subgoal 2" :in-theory '((:forward-chaining alistp-forward-to-true-listp)
3666
(:rewrite if-bad-index-not-in-range-then-m-corr)))
3667
("Subgoal 1" :in-theory '((:rewrite if-bad-index-in-range-thne-must-be-different-vs)))))
3672
(defthm m-correspondence-and-other-conditions-kept-by-any-execution-add
3676
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-add)
3677
(no-duplicates-p (retrieve-gemvars m))
3678
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
3679
(good-translation-gem-rtm gstate rstate m)
3680
(correct-wrt-arity m (mem gstate))
3683
(vars-inclusion (mem gstate) m)
3684
(vars-inclusion m (mem gstate))
3685
(in-range (pcc gstate) (code gstate))
3686
(in-range (pcc rstate) (code rstate))
3687
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
3688
(m-correspondent-values-p m (mem gstate) (mem rstate)))
3690
(good-translation-gem-rtm (execute-instruction gstate) (execute-n-instructions rstate (len *rns*)) m)
3691
(rtm-statep (execute-n-instructions rstate (len *rns*)))
3692
(m-entries-point-to-good-rtm-var-sets m (mem (execute-n-instructions rstate (len *rns*))))
3693
(gem-statep (execute-instruction gstate))
3694
(correct-wrt-arity m (mem (execute-instruction gstate)))
3695
(vars-inclusion (mem (execute-instruction gstate)) m)
3696
(vars-inclusion m (mem (execute-instruction gstate)))
3697
(m-correspondent-values-p
3699
(mem (execute-instruction gstate))
3700
(mem (execute-n-instructions rstate (len *rns*))))))
3703
rtm-statep gem-statep
3705
execute-instruction rtmintvars-i par1 par2 par3 nth len member-equal)
3707
(m-correspondence-kept-by-any-execution-idxed-add
3708
good-translation-gem-rtm
3709
(:instance execute-n-instructions-keeps-rtm-state-and-points-to-good
3710
(st rstate) (n (len *rns*)))
3711
(:instance executing-gem-instruction-retrieves-a-gem-state-from-gem-state (st gstate))
3712
(:instance executing-gem-instruction-preserves-correctness-wrt-arity (st gstate))
3713
(:instance executing-gem-instruction-keeps-vars-inclusion-right (st gstate))
3714
(:instance executing-gem-instruction-keeps-vars-inclusion-left (st gstate))))))
3726
;;(ld "Proof-Of-Minus.lisp" :ld-error-action :error)
3730
(:executable-counterpart build-values-by-rns)
3731
(:type-prescription build-values-by-rns)
3732
(:induction build-values-by-rns)
3733
(:definition build-values-by-rns)
3734
posp-all posp mod mod-- mod-prod-makes-same-residues))
3736
(in-theory (disable mod floor))
3738
(defun sub-list (vl2 vl3 rns)
3741
(cons (mod (- (car vl2) (car vl3)) (car rns))
3742
(sub-list (cdr vl2) (cdr vl3) (cdr rns)))))
3745
(defthm sub-correspondence-by-put-list
3751
(equal (build-values-by-rns (- gval1 gval2) rns)
3753
(build-values-by-rns gval1 rns)
3754
(build-values-by-rns gval2 rns)
3756
:hints (("Goal" :induct t)))
3761
(in-theory (disable mod floor))
3763
(defthm sub-correspondence-by-put-list-2-fin
3769
(equal (build-values-by-rns (mod (- gval1 gval2) (prod rns)) rns)
3771
(build-values-by-rns gval1 rns)
3772
(build-values-by-rns gval2 rns)
3774
:hints (("Goal" :in-theory (disable sum-correspondence-by-put-list-2-fin sum-correspondence-by-put-list)
3775
:use (sub-correspondence-by-put-list
3776
(:instance mod-prod-makes-same-residues (x (- gval1 gval2)))))))
3780
(in-theory (disable mod floor mod-- mod-prod-makes-same-residues))
3783
(defthm sub-correspondence-by-put-list-h
3788
(integer>1-listp rns))
3789
(equal (build-values-by-rns (mod (- gval1 gval2) (prod rns)) rns)
3791
(build-values-by-rns gval1 rns)
3792
(build-values-by-rns gval2 rns)
3794
:hints (("Goal" :use (sub-correspondence-by-put-list-2-fin greater-one-means-greater-zero))))
3799
(defthm a-boolean-has-same-rnss-than-list-of-itself
3803
(or (equal val 0) (equal val 1))
3804
(integer>1-listp rns))
3806
(build-values-by-rns val rns)
3807
(make-n-list val (len rns)))))
3811
(defthm sub-correspondence-by-put-list-on-boolean
3816
(or (equal gval2 0) (equal gval2 1))
3817
(integer>1-listp rns))
3818
(equal (build-values-by-rns (mod (- gval1 gval2) (prod rns)) rns)
3820
(build-values-by-rns gval1 rns)
3821
(make-n-list gval2 (len rns))
3823
:hints (("Goal" :in-theory nil
3824
:use (sub-correspondence-by-put-list-h
3825
(:instance a-boolean-has-same-rnss-than-list-of-itself (val gval2))))))
3827
(in-theory (disable mod--))
3830
(defun equal-sub-and-updates (reslist par1list par2list par3list primelist mem memafterputs)
3835
(get-cell (car reslist) memafterputs)
3842
(equal-sub-and-updates
3855
(defthm equal-sub-and-updates-have-same-attributes
3858
(true-listp rtmvars1)
3859
(true-listp rtmvarsres)
3860
(equal (len rtmvars1) (len rtmvarsres))
3861
(equal-sub-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns rtmmem rtmmemafter))
3862
(equal (var-attributes rtmvarsres rtmmemafter) (var-attributes rtmvars1 rtmmem)))
3863
:hints (("Goal" :in-theory (enable var-attribute make-cell))))
3865
;(in-theory (enable sub-list))
3867
(defthm equal-sub-and-updates-have-values-that-are-sub-lists
3870
(equal (len rtmvars1) (len rtmvarsres))
3871
(equal (len rtmvars2) (len rtmvarsres))
3872
(equal (len rtmvars3) (len rtmvarsres))
3873
(equal-sub-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns rtmmem rtmmemafter))
3874
(equal (var-values rtmvarsres rtmmemafter)
3876
(var-values rtmvars2 rtmmem)
3877
(var-values rtmvars3 rtmmem)
3879
:hints ( ("Subgoal *1/2" :in-theory (enable var-value get-cell make-cell))))
3885
(defthm behaviour-of-sub-and-update-norest
3888
(var-attribute (sub-and-update-norest c1 c2 c3 mem))
3889
(var-attribute (get-cell c1 mem)))
3891
(var-value (sub-and-update-norest c1 c2 c3 mem))
3894
(var-value (get-cell c2 mem))
3895
(var-value (get-cell c3 mem)))
3898
(var-type (sub-and-update-norest c1 c2 c3 mem))
3899
(var-type (get-cell c1 mem))))
3900
:hints (("Goal" :in-theory (enable var-type var-value var-attribute make-cell))))
3905
(defthm defexpansion-sub
3907
(not (null (var-value gcell)))
3909
(equal-values-and-attributes gcell rtmvars rtmmem 'Int)
3911
(equal-values (var-values rtmvars rtmmem)
3912
(build-values-by-rns (var-value gcell) *rns*))
3913
(equal-elements (var-attribute gcell)
3914
(var-attributes rtmvars rtmmem)))))
3915
:hints (("Goal" :in-theory '((:definition equal-values-and-attributes)
3916
(:definition apply-direct-rns-to-value-according-to-type))
3917
:use (:instance build-values-by-rns-extended-behaves-standardly-on-non-nils
3918
(gem-value (var-value gcell))
3925
(defthm if-gem-is-sub-and-update-inf-every-rtm-var-is-sub-and-update-then-equal-values-is-kept
3928
(true-listp rtmvars1)
3929
(true-listp rtmvarsres)
3930
(equal (len rtmvars1) (len rtmvarsres))
3931
(equal (len rtmvars2) (len rtmvarsres))
3932
(equal (len rtmvars3) (len rtmvarsres))
3933
(not (null (var-value (get-cell gvar1 gemmem))))
3934
(integerp (var-value (get-cell gvar2 gemmem)))
3935
(integerp (var-value (get-cell gvar3 gemmem)))
3936
(equal-sub-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 *rns* rtmmem rtmmemafter)
3937
(equal-values-and-attributes (get-cell gvar1 gemmem) rtmvars1 rtmmem 'Int)
3938
(equal-values-and-attributes (get-cell gvar2 gemmem) rtmvars2 rtmmem 'Int)
3939
(equal-values-and-attributes (get-cell gvar3 gemmem) rtmvars3 rtmmem 'Int))
3940
(equal-values-and-attributes
3941
(sub-and-update-norest gvar1 gvar2 gvar3 gemmem)
3946
:in-theory (union-theories (current-theory 'ground-zero)
3948
(:definition integer>1-listp)
3949
(:definition equal-values)
3950
(:rewrite defexpansion-sub)))
3952
(:instance greater-one-means-greater-zero (rns *rns*))
3953
(:instance equal-sub-and-updates-have-values-that-are-sub-lists (rns *rns*))
3954
(:instance equal-sub-and-updates-have-same-attributes (rns *rns*))
3955
(:instance sub-correspondence-by-put-list-h
3956
(gval1 (var-value (get-cell gvar2 gemmem)))
3957
(gval2 (var-value (get-cell gvar3 gemmem)))
3959
(:instance behaviour-of-sub-and-update-norest
3977
(defthm if-gem-is-sub-and-update-inf-every-rtm-var-is-sub-and-update-then-equal-values-is-kept-g
3980
(true-listp rtmvars1)
3981
(true-listp rtmvarsres)
3982
(equal (len rtmvars1) (len rtmvarsres))
3983
(equal (len (eventually-make-list rtmvars2 (len *rns*))) (len rtmvarsres))
3984
(equal (len (eventually-make-list rtmvars3 (len *rns*))) (len rtmvarsres))
3985
(equal (var-type (get-cell gvar2 gemmem)) (type-expected rtmvars2))
3986
(equal (var-type (get-cell gvar3 gemmem)) (type-expected rtmvars3))
3987
(is-mem-cell-p (get-cell gvar1 gemmem))
3988
(equal (var-type (get-cell gvar1 gemmem)) 'Int)
3989
(is-mem-cell-p (get-cell gvar2 gemmem))
3990
(is-mem-cell-p (get-cell gvar3 gemmem))
3991
(equal-sub-and-updates
3994
(eventually-make-list rtmvars2 (len *rns*))
3995
(eventually-make-list rtmvars3 (len *rns*))
3996
*rns* rtmmem rtmmemafter)
3997
(equal-values-and-attributes (get-cell gvar1 gemmem) rtmvars1 rtmmem 'Int)
3998
(equal-values-and-attributes (get-cell gvar2 gemmem) rtmvars2 rtmmem (var-type (get-cell gvar2 gemmem)))
3999
(equal-values-and-attributes (get-cell gvar3 gemmem) rtmvars3 rtmmem (var-type (get-cell gvar3 gemmem))))
4000
(equal-values-and-attributes
4001
(sub-and-update-norest gvar1 gvar2 gvar3 gemmem)
4006
:in-theory (union-theories (current-theory 'ground-zero)
4007
'((:definition integer>1-listp)
4008
(:definition equal-values)
4009
(:definition is-mem-cell-p)
4010
(:rewrite defexpansion-sub)))
4012
(:instance defexpansion-generic
4013
(gcell (get-cell gvar2 gemmem))
4015
(:instance defexpansion-generic
4016
(gcell (get-cell gvar3 gemmem))
4018
(:instance equal-sub-and-updates-have-values-that-are-sub-lists
4019
(rtmvars2 (eventually-make-list rtmvars2 (len *rns*)))
4020
(rtmvars3 (eventually-make-list rtmvars3 (len *rns*)))
4022
(:instance equal-sub-and-updates-have-same-attributes
4023
(rtmvars2 (eventually-make-list rtmvars2 (len *rns*)))
4024
(rtmvars3 (eventually-make-list rtmvars3 (len *rns*)))
4026
(:instance sub-correspondence-by-put-list-h
4027
(gval1 (var-value (get-cell gvar2 gemmem)))
4028
(gval2 (var-value (get-cell gvar3 gemmem)))
4030
(:instance behaviour-of-sub-and-update-norest
4040
(in-theory (disable sub-list sub-correspondence-by-put-list
4041
sub-correspondence-by-put-list-h
4042
sub-correspondence-by-put-list-2-fin
4043
equal-sub-and-updates-have-same-attributes
4044
equal-sub-and-updates-have-values-that-are-sub-lists
4045
behaviour-of-sub-and-update-norest
4047
if-a-var-value-is-same-then-var-values-are-list-of
4048
if-a-var-attribute-is-same-then-var-attributes-are-list-of
4049
defexpansion-generic-bool
4050
defexpansion-generic-int
4051
defexpansion-generic
4052
defexpansion-bool-values-inv
4053
defexpansion-bool-values
4054
defexpansion-bool-attrs-inv
4055
defexpansion-bool-attrs-inv-1
4056
defexpansion-bool-attrs-inv-2
4057
defexpansion-bool-attrs
4058
defexpansion-bool-attrs-1
4059
equal-values-on-list-entails-equality-on-first-els
4066
(defun execute-n-rtm-subs (st n)
4072
(par1 (nth (pcc st) (code st)))
4073
(par2 (nth (pcc st) (code st)))
4074
(par3 (nth (pcc st) (code st)))
4075
(par4 (nth (pcc st) (code st)))
4080
(defthm all-rtm-subs-means-only-subs-are-executed
4082
(all-rtm-subs-for-n-steps st n)
4084
(execute-n-rtm-subs st n)
4085
(execute-n-instructions st n)))
4086
:hints (("Goal" :in-theory (disable rtm-sub member-equal nth par1 par2 par3))))
4089
(defun subs-list-n (l1 l2 l3 l4 mem n)
4092
(subs-list-n (cdr l1) (cdr l2) (cdr l3) (cdr l4)
4110
(in-theory (disable member-equal))
4113
(in-theory (enable make-cell))
4117
(defthm execute-n-rtm-subs-tantamount-to-sub-list-n
4120
(all-rtm-subs-for-n-steps st n)
4124
(mem (execute-n-rtm-subs st n))
4133
(("Goal" :induct t )
4134
("Subgoal *1/2.2" :in-theory '((:definition all-rtm-subs-for-n-steps)
4135
(:definition execute-instruction)
4136
(:definition rtm-sub)
4137
(:definition make-state)
4141
:use ( execute-n-rtm-subs
4142
(:instance subs-list-n
4143
(l1 (listpars1 st n))
4144
(l2 (listpars2 st n))
4145
(l3 (listpars3 st n))
4146
(l4 (listpars4 st n))
4148
lemma12-lp1r lemma12-lp2r lemma12-lp3r lemma12-lp4r
4150
(IMPLIES (AND (ALL-RTM-SUBS-FOR-N-STEPS ST N)
4153
(equal (mem (execute-instruction st))
4154
(PUT-CELL (CAR (LISTPARS1 ST N))
4155
(SUB-AND-UPDATE (CAR (LISTPARS1 ST N))
4156
(CAR (LISTPARS2 ST N))
4157
(CAR (LISTPARS3 ST N))
4158
(CAR (LISTPARS4 ST N))
4161
executing-rtm-instruction-retrieves-a-rtm-state-from-rtm-state
4162
instruction-incrementing-pvv))))
4165
(in-theory (disable lemma12-lp1r lemma12-lp2r lemma12-lp3r lemma12-lp4r ))
4176
(defun subs-list-e (c1 c2 c3 c4 mem)
4185
(put-cell (car c1) (sub-and-update (car c1) (car c2) (car c3) (car c4) mem) mem))))
4189
(defthm subs-list-e-is-subs-list-n
4190
(equal (subs-list-e c1 c2 c3 c4 mem) (subs-list-n c1 c2 c3 c4 mem (len c1)))
4195
(defthm execute-n-instructions-tantamount-to-sub-list-e
4200
(all-rtm-subs-for-n-steps st n)
4204
(mem (execute-n-instructions st n))
4211
:hints (("Goal" :in-theory nil
4212
:use ((:instance subs-list-e-is-subs-list-n
4213
(c1 (listpars1 st n))
4214
(c2 (listpars2 st n))
4215
(c3 (listpars3 st n))
4216
(c4 (listpars4 st n))
4218
execute-n-rtm-subs-tantamount-to-sub-list-n
4219
all-rtm-subs-means-only-subs-are-executed
4220
length-of-listpars1-n-is-n))))
4231
(defthm not-in-list-untouched-by-subs-list-e
4233
(not (member-equal-bool v l1))
4234
(equal (get-cell v (subs-list-e l1 l2 l3 l4 mem)) (get-cell v mem)))
4235
:hints (("Goal" :in-theory (disable sub-and-update))))
4237
(defthm not-in-list-untouched-by-subs-list-e-1
4239
(not (member-equal-bool (car l1) (cdr l1)))
4240
(equal (get-cell (car l1) (subs-list-e (cdr l1) (cdr l2) (cdr l3) (cdr l4) mem))
4241
(get-cell (car l1) mem))))
4244
(defthm sub-and-update-independent-from-firstbn
4247
(not (member-equal-bool (nth idx l1) (firstn idx l1)))
4248
(not (member-equal-bool (nth idx l2) (firstn idx l1)))
4249
(not (member-equal-bool (nth idx l3) (firstn idx l1))))
4250
(equal (sub-and-update
4255
(subs-list-e (firstn idx l1) (firstn idx l2) (firstn idx l3) (firstn idx l4) mem))
4265
(defthm subs-list-decomp
4273
(subs-list-e l1 l2 l3 l4 mem)
4274
(subs-list-e (nthcdr idx l1) (nthcdr idx l2) (nthcdr idx l3) (nthcdr idx l4)
4275
(subs-list-e (firstn idx l1) (firstn idx l2) (firstn idx l3) (firstn idx l4) mem))))
4276
:hints (("Goal" :in-theory (disable sub-and-update))))
4279
(defthm if-el-does-not-appear-after-its-position-then-subs-list-e-produces-its-sub
4282
(not (member-equal-bool (nth idx l1) (cdr (nthcdr idx l1))))
4288
(get-cell (nth idx l1) (subs-list-e l1 l2 l3 l4 mem))
4294
(subs-list-e (firstn idx l1) (firstn idx l2) (firstn idx l3) (firstn idx l4) mem))))
4295
:hints (("Goal" :in-theory (disable sub-and-update))))
4300
(defthm rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables
4305
(no-duplicates-p (append-lists ll))
4309
(in-range idx (nth gem1 ll))
4310
(in-range idx (nth gem2 ll))
4311
(in-range idx (nth gem3 ll))
4314
(get-cell (nth idx (nth gem1 ll)) (subs-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem))
4315
(sub-and-update (nth idx (nth gem1 ll)) (nth idx (nth gem2 ll)) (nth idx (nth gem3 ll)) (nth idx rns) mem)))
4316
:hints (("Goal" :in-theory (disable sub-and-update)
4318
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
4319
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
4320
if-el-does-not-appear-after-its-position-then-subs-list-e-produces-its-sub
4321
(:instance subs-list-decomp
4322
(l1 (nth gem1 ll)) (l2 (nth gem2 ll)) (l3 (nth gem3 ll)))
4323
(:instance sub-and-update-independent-from-firstbn
4324
(l1 (nth gem1 ll)) (l2 (nth gem2 ll)) (l3 (nth gem3 ll)))))))
4328
(defun index-different-sub-and-updates (rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-sub)
4332
( (not (equal (get-cell (car rtmvarsres) mem-after-sub)
4333
(sub-and-update (car rtmvars1) (car rtmvars2) (car rtmvars3) (car rns) mem)))
4336
(1+ (index-different-sub-and-updates
4345
(defthm if-bad-index-in-range-thne-must-be-nonsubandupdate
4346
(let ((bad-idx (index-different-sub-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-sub)))
4348
(in-range bad-idx rtmvarsres)
4350
(get-cell (nth bad-idx rtmvarsres) mem-after-sub)
4352
(nth bad-idx rtmvars1)
4353
(nth bad-idx rtmvars2)
4354
(nth bad-idx rtmvars3)
4357
:hints (("Goal" :in-theory (disable get-cell sub-and-update))))
4360
(defthm if-bad-index-not-in-range-then-every-equalsubandupdate
4361
(let ((bad-idx (index-different-sub-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-sub)))
4362
(implies (and (true-listp rtmvarsres)
4363
(not (in-range bad-idx rtmvarsres)))
4364
(equal-sub-and-updates rtmvarsres rtmvars1 rtmvars2 rtmvars3 rns mem mem-after-sub))))
4367
(defthm rtm-variable-of-subs-list-e-is-sub-and-updates
4372
(no-duplicates-p (append-lists ll))
4373
(equal (len (nth gem1 ll)) (len (nth gem2 ll)))
4374
(equal (len (nth gem1 ll)) (len (nth gem3 ll)))
4375
(equal (len (nth gem1 ll)) (len rns))
4379
(true-listp (nth gem1 ll)))
4380
(equal-sub-and-updates (nth gem1 ll) (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem
4381
(subs-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem)))
4382
:hints (("Goal" :use (:instance rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables
4383
(idx (index-different-sub-and-updates
4390
(subs-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem)))))
4391
("Goal'" :cases ( (in-range (index-different-sub-and-updates
4398
(subs-list-e (nth gem1 ll) (nth gem2 ll) (nth gem3 ll) rns mem))
4400
("Subgoal 1" :in-theory '((:definition in-range)
4401
(:rewrite if-bad-index-in-range-thne-must-be-nonsubandupdate)))
4402
("Subgoal 2" :in-theory '((:rewrite if-bad-index-not-in-range-then-every-equalsubandupdate)))))
4407
(defthm any-element-of-make-list-does-not-appear-into-other-lists
4412
(no-duplicates-p (append-lists ll))
4415
(not (equal gem1 gem2))
4416
(equal (len (nth gem1 ll)) 1)
4417
(in-range idx (make-n-list (car (nth gem1 ll)) n)))
4418
(not (member-equal-bool
4419
(nth idx (make-n-list (car (nth gem1 ll)) n))
4421
:hints (("Goal" :use
4424
el-of-makelist-is-el
4425
(el (car (nth gem1 ll))))
4426
(:instance generalized-disjunctivity-unordered-2
4427
(idx1 gem1) (idx2 gem2) (el1 (car (nth gem1 ll)))))))
4430
(defthm firstns-do-not-cotain-el-of-make-n-list-if-diff
4435
(no-duplicates-p (append-lists ll))
4438
(not (equal gem1 gem2))
4439
(equal (len (nth gem1 ll)) 1)
4440
(in-range idx (make-n-list (car (nth gem1 ll)) n)))
4441
(not (member-equal-bool
4442
(nth idx (make-n-list (car (nth gem1 ll)) n))
4443
(firstn idx (nth gem2 ll)))))
4444
:hints (("Goal" :use
4446
(:instance no-member-holds-on-firstn
4447
(el (nth idx (make-n-list (car (nth gem1 ll)) n)))
4449
any-element-of-make-list-does-not-appear-into-other-lists))))
4453
(defthm rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-when-var-3-is-boolean
4459
(no-duplicates-p (append-lists ll))
4463
(not (equal gem1 gem3))
4464
(equal (len (nth gem3 ll)) 1)
4465
(in-range idx (nth gem1 ll))
4466
(in-range idx (nth gem2 ll))
4467
(in-range idx (make-n-list (car (nth gem3 ll)) n))
4470
(get-cell (nth idx (nth gem1 ll))
4474
(make-n-list (car (nth gem3 ll)) n)
4477
(nth idx (nth gem1 ll))
4478
(nth idx (nth gem2 ll))
4479
(nth idx (make-n-list (car (nth gem3 ll)) n))
4480
(nth idx rns) mem)))
4481
:hints (("Goal" :in-theory (disable sub-and-update)
4483
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem3) (gem2 gem1))
4484
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
4485
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
4486
(:instance subs-list-decomp
4489
(l3 (make-n-list (car (nth gem3 ll)) n))
4491
(:instance sub-and-update-independent-from-firstbn
4494
(l3 (make-n-list (car (nth gem3 ll)) n))
4497
(defthm rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-when-var-2-is-boolean
4503
(no-duplicates-p (append-lists ll))
4507
(not (equal gem1 gem2))
4508
(equal (len (nth gem2 ll)) 1)
4509
(in-range idx (nth gem1 ll))
4510
(in-range idx (nth gem3 ll))
4511
(in-range idx (make-n-list (car (nth gem2 ll)) n))
4514
(get-cell (nth idx (nth gem1 ll))
4517
(make-n-list (car (nth gem2 ll)) n)
4521
(nth idx (nth gem1 ll))
4522
(nth idx (make-n-list (car (nth gem2 ll)) n))
4523
(nth idx (nth gem3 ll))
4524
(nth idx rns) mem)))
4525
:hints (("Goal" :in-theory (disable sub-and-update)
4527
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem2) (gem2 gem1))
4528
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
4529
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
4530
(:instance subs-list-decomp
4532
(l2 (make-n-list (car (nth gem2 ll)) n))
4535
(:instance sub-and-update-independent-from-firstbn
4537
(l2 (make-n-list (car (nth gem2 ll)) n))
4541
(defthm rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-when-var-2and3-are-boolean
4547
(no-duplicates-p (append-lists ll))
4551
(not (equal gem1 gem2))
4552
(not (equal gem1 gem3))
4553
(equal (len (nth gem2 ll)) 1)
4554
(equal (len (nth gem3 ll)) 1)
4555
(in-range idx (nth gem1 ll))
4556
(in-range idx (make-n-list (car (nth gem2 ll)) n))
4557
(in-range idx (make-n-list (car (nth gem3 ll)) n))
4560
(get-cell (nth idx (nth gem1 ll))
4563
(make-n-list (car (nth gem2 ll)) n)
4564
(make-n-list (car (nth gem3 ll)) n)
4567
(nth idx (nth gem1 ll))
4568
(nth idx (make-n-list (car (nth gem2 ll)) n))
4569
(nth idx (make-n-list (car (nth gem3 ll)) n))
4570
(nth idx rns) mem)))
4571
:hints (("Goal" :in-theory (disable sub-and-update)
4573
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem2) (gem2 gem1))
4574
(:instance firstns-do-not-cotain-el-of-make-n-list-if-diff (gem1 gem3) (gem2 gem1))
4575
(:instance no-duplicates-all-implies-no-duplicates-one (idx1 gem1))
4576
(:instance no-duplicates-means-an-element-does-not-appear-after-its-position (l (nth gem1 ll)))
4577
(:instance subs-list-decomp
4579
(l2 (make-n-list (car (nth gem2 ll)) n))
4580
(l3 (make-n-list (car (nth gem3 ll)) n))
4582
(:instance sub-and-update-independent-from-firstbn
4584
(l2 (make-n-list (car (nth gem2 ll)) n))
4585
(l3 (make-n-list (car (nth gem3 ll)) n))
4591
(defthm rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-with-all-vars-types
4597
(no-duplicates-p (append-lists ll))
4601
(not (equal (len (nth gem1 ll)) 1))
4602
(in-range idx (nth gem1 ll))
4603
(in-range idx (eventually-make-list (nth gem2 ll) n))
4604
(in-range idx (eventually-make-list (nth gem3 ll) n))
4607
(get-cell (nth idx (nth gem1 ll))
4610
(eventually-make-list (nth gem2 ll) n)
4611
(eventually-make-list (nth gem3 ll) n)
4614
(nth idx (nth gem1 ll))
4615
(nth idx (eventually-make-list (nth gem2 ll) n))
4616
(nth idx (eventually-make-list (nth gem3 ll) n))
4617
(nth idx rns) mem)))
4618
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero)
4619
'((:definition eventually-make-list)))
4621
( (and (not (equal (len (nth gem3 ll)) 1)) (equal (len (nth gem2 ll)) 1))
4622
(and (equal (len (nth gem3 ll)) 1) (not (equal (len (nth gem2 ll)) 1)))
4623
(and (not (equal (len (nth gem3 ll)) 1)) (not (equal (len (nth gem2 ll)) 1)))
4624
(and (equal (len (nth gem3 ll)) 1) (equal (len (nth gem2 ll)) 1))))
4626
:use rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-when-var-2-is-boolean)
4628
:use rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-when-var-3-is-boolean)
4630
:use rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables)
4632
:use rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-when-var-2and3-are-boolean)))
4636
(defthm sub-and-updates-holding-for-every-variable-type
4640
(not (equal (len (nth gem1 ll)) 1))
4643
(no-duplicates-p (append-lists ll))
4644
(equal (len (nth gem1 ll)) (len (eventually-make-list (nth gem2 ll) n)))
4645
(equal (len (nth gem1 ll)) (len (eventually-make-list (nth gem3 ll) n)))
4646
(equal (len (nth gem1 ll)) (len rns))
4650
(true-listp (nth gem1 ll)))
4651
(equal-sub-and-updates
4654
(eventually-make-list (nth gem2 ll) n)
4655
(eventually-make-list (nth gem3 ll) n)
4659
(eventually-make-list (nth gem2 ll) n)
4660
(eventually-make-list (nth gem3 ll) n)
4662
:hints (("Goal" :use (:instance rtm-variable-of-subs-list-e-is-sub-of-correspondent-variables-with-all-vars-types
4663
(idx (index-different-sub-and-updates
4666
(eventually-make-list (nth gem2 ll) n)
4667
(eventually-make-list (nth gem3 ll) n)
4672
(eventually-make-list (nth gem2 ll) n)
4673
(eventually-make-list (nth gem3 ll) n)
4675
("Goal'" :cases ( (in-range (index-different-sub-and-updates
4678
(eventually-make-list (nth gem2 ll) n)
4679
(eventually-make-list (nth gem3 ll) n)
4684
(eventually-make-list (nth gem2 ll) n)
4685
(eventually-make-list (nth gem3 ll) n)
4688
("Subgoal 1" :in-theory '((:definition in-range)
4689
(:rewrite if-bad-index-in-range-thne-must-be-nonsubandupdate)))
4690
("Subgoal 2" :in-theory '((:rewrite if-bad-index-not-in-range-then-every-equalsubandupdate)))))
4694
(defthm lemma2-only-subs-in-rtm-sub
4699
(in-range (pcc gstate) (code gstate))
4700
(in-range (pcc rstate) (code rstate))
4701
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4702
(good-translation-gem-rtm gstate rstate m))
4703
(all-rtm-subs-for-n-steps rstate (len *rns*)))
4704
:hints (("Goal" :expand
4705
( (good-translation-gem-rtm gstate rstate m)
4708
(in-range (pcc gstate) (code gstate))
4709
(in-range (pcc rstate) (code rstate)))
4714
(defthm cells-untouched-by-execute-on-other-cell-sub
4719
(all-rtm-subs-for-n-steps st n)
4722
(not (member-equal-bool v (listpars1 st n))))
4723
(equal (get-cell v (mem st))
4724
(get-cell v (mem (execute-n-instructions st n)))))
4726
:use (execute-n-instructions-tantamount-to-sub-list-e
4727
(:instance not-in-list-untouched-by-subs-list-e
4729
(l1 (listpars1 st n))
4730
(l2 (listpars2 st n))
4731
(l3 (listpars3 st n))
4732
(l4 (listpars4 st n))
4736
(defthm rtm-variable-of-other-cell-untouched-sub
4739
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4742
(good-translation-gem-rtm gstate rstate m)
4743
(in-range (pcc gstate) (code gstate))
4744
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m)
4746
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
4747
(assoc-equal gvar1 m)
4748
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
4749
(in-range idx1 (rtmintvars-i gvar1 m)))
4750
(equal (get-cell (nth idx1 (rtmintvars-i gvar1 m)) (mem rstate))
4751
(get-cell (nth idx1 (rtmintvars-i gvar1 m)) (mem (execute-n-instructions rstate (len *rns*))))))
4752
:hints (("Goal" :in-theory (current-theory 'ground-zero)
4753
:expand ( (in-range (pcc gstate) (code gstate))
4754
(good-translation-gem-rtm gstate rstate m) )
4756
(:instance lemma1-different-vars-do-not-belong (gvar2 (par1 (nth (pcc gstate) (code gstate)))))
4757
(:instance cells-untouched-by-execute-on-other-cell-sub (st rstate) (n (len *rns*))
4758
(v (nth idx1 (rtmintvars-i gvar1 m))))))))
4760
(defthm rtm-variables-of-other-cell-untouched-sub
4763
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4766
(good-translation-gem-rtm gstate rstate m)
4767
(in-range (pcc gstate) (code gstate))
4768
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m)
4770
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
4771
(assoc-equal gvar1 m)
4772
(true-listp (rtmintvars-i gvar1 m))
4773
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate))))))
4775
(rtmintvars-i gvar1 m) (mem rstate) (mem (execute-n-instructions rstate (len *rns*)))))
4776
:hints (("Goal" :in-theory nil
4777
:use ( (:instance rtm-variable-of-other-cell-untouched-sub
4778
(idx1 (idx-different-cell
4779
(rtmintvars-i gvar1 m)
4781
(mem (execute-n-instructions rstate (len *rns*)))))) ))
4782
("Goal'" :cases ( (in-range
4784
(rtmintvars-i gvar1 m)
4786
(mem (execute-n-instructions rstate (len *rns*))))
4787
(rtmintvars-i gvar1 m))))
4788
("Subgoal 2" :in-theory '((:rewrite if-bad-index-not-in-range-then-every-equal)))
4789
("Subgoal 1" :in-theory '((:forward-chaining if-bad-index-in-range-then-cells-must-be-different)))))
4794
(defthm properies-of-type-and-existence-of-current-args-sub
4798
(in-range (pcc gstate) (code gstate))
4799
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub))
4801
(equal (var-type (get-cell (par1 (nth (pcc gstate) (code gstate))) (mem gstate))) 'Int)
4802
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) (mem gstate))
4803
(assoc-equal (par2 (nth (pcc gstate) (code gstate))) (mem gstate))
4804
(assoc-equal (par3 (nth (pcc gstate) (code gstate))) (mem gstate))))
4805
:hints (("Goal" :in-theory (enable get-cell)
4806
:use (:instance in-range-instruction-is-gem-instruction
4808
(code (code gstate))
4809
(mem (mem gstate)))))
4813
(defthm par1-of-current-instruction-is-into-mapping-sub
4816
(vars-inclusion (mem gstate) m)
4818
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4819
(in-range (pcc gstate) (code gstate)))
4820
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m))
4821
:hints (("Goal" :in-theory (enable get-cell)
4822
:use (properies-of-type-and-existence-of-current-args-sub
4823
(:instance inclusion-trans
4824
(v (par1 (nth (pcc gstate) (code gstate))))
4827
(:instance in-range-instruction-is-gem-instruction
4829
(code (code gstate))
4830
(mem (mem gstate)))))))
4834
(defthm teorema-main-con-pcc-in-range-su-variabile-non-interessata-final-sub
4837
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4838
(good-translation-gem-rtm gstate rstate m)
4839
(vars-inclusion (mem gstate) m)
4841
(assoc-equal gvar1 m)
4844
(in-range (pcc gstate) (code gstate))
4845
(in-range (pcc rstate) (code rstate))
4846
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
4847
(m-correspondent-values-p m (mem gstate) (mem rstate))
4848
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
4849
(correct-wrt-arity m (mem gstate)))
4850
(equal-values-and-attributes
4851
(get-cell gvar1 (mem (execute-instruction gstate)))
4852
(rtmintvars-i gvar1 m)
4853
(mem (execute-n-instructions rstate (len *rns*)))
4856
:in-theory '((:definition good-translation-gem-rtm))
4858
par1-of-current-instruction-is-into-mapping-sub
4859
(:instance correct-wrt-arity-has-rtmintvars-i-tl (mem (mem gstate)))
4860
(:instance m-correspondent-values-implies-equal-values-and-attribus
4861
(memgstate (mem gstate)) (memrstate (mem rstate)))
4862
(:instance in-range (idx (pcc gstate)) (l (code gstate)))
4863
(:instance in-range (idx (pcc rstate)) (l (code rstate)))
4864
rtm-variables-of-other-cell-untouched-sub
4865
teorema-main-con-pcc-in-range-su-variabile-non-interessata
4866
(:instance equal-get-cells-implies-equal-values-and-attributes-still-works
4867
(gemcell (get-cell gvar1 (mem gstate)))
4868
(lcell (rtmintvars-i gvar1 m))
4870
(mem2 (mem (execute-n-instructions rstate (len *rns*))))
4871
(type (type-i gvar1 m)))))))
4874
(defthm teorema-main-con-pcc-in-range-su-variabile-interessata-sub
4879
(in-range (pcc gstate) (code gstate))
4880
(in-range (pcc rstate) (code rstate))
4881
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4882
(good-translation-gem-rtm gstate rstate m))
4884
(mem (execute-n-instructions rstate (len *rns*)))
4886
(rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)
4887
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
4888
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
4892
:in-theory (union-theories (current-theory 'ground-zero) '((:definition in-range)))
4893
:use (good-translation-gem-rtm
4894
lemma2-only-subs-in-rtm-sub
4895
(:instance execute-n-instructions-tantamount-to-sub-list-e
4906
(vars-inclusion (mem gstate) m)
4908
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4909
(in-range (pcc gstate) (code gstate)))
4911
(in-range (pos-equal-0 (par1 (nth (pcc gstate) (code gstate))) m) m)
4912
(in-range (pos-equal-0 (par2 (nth (pcc gstate) (code gstate))) m) m)
4913
(in-range (pos-equal-0 (par3 (nth (pcc gstate) (code gstate))) m) m)))
4915
:use (properies-of-type-and-existence-of-current-args-sub
4916
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
4917
(v (par1 (nth (pcc gstate) (code gstate)))))
4918
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
4919
(v (par2 (nth (pcc gstate) (code gstate)))))
4920
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
4921
(v (par3 (nth (pcc gstate) (code gstate)))))
4922
(:instance assoc-means-pos-in-range
4923
(el (par1 (nth (pcc gstate) (code gstate))))
4925
(:instance assoc-means-pos-in-range
4926
(el (par2 (nth (pcc gstate) (code gstate))))
4928
(:instance assoc-means-pos-in-range
4929
(el (par3 (nth (pcc gstate) (code gstate))))
4938
(in-range (pcc gstate) (code gstate))
4939
(in-range (pcc rstate) (code rstate))
4940
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4941
(good-translation-gem-rtm gstate rstate m))
4943
(equal (len (rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)) (len *rns*))
4944
(equal (len (eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*))) (len *rns*))
4945
(equal (len (eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*))) (len *rns*))))
4947
:in-theory (union-theories (current-theory 'ground-zero) '((:definition in-range)))
4950
good-translation-gem-rtm
4951
(:instance length-of-listpars1-n-is-n (st rstate) (n (len *rns*)))
4952
(:instance length-of-listpars2-n-is-n (st rstate) (n (len *rns*)))
4953
(:instance length-of-listpars3-n-is-n (st rstate) (n (len *rns*))))))
4957
(defthm equal-sub-and-updates-after-n-instr
4961
(correct-wrt-arity m (mem gstate))
4964
(vars-inclusion (mem gstate) m)
4965
(in-range (pcc gstate) (code gstate))
4966
(in-range (pcc rstate) (code rstate))
4967
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
4968
(good-translation-gem-rtm gstate rstate m)
4969
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
4970
(assoc-equal gvar1 m)
4971
(equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
4972
(equal-sub-and-updates
4973
(rtmintvars-i gvar1 m)
4974
(rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)
4975
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
4976
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*)) ;new
4979
(mem (execute-n-instructions rstate (len *rns*)))))
4981
:in-theory (union-theories (current-theory 'ground-zero)
4982
'((:type-prescription retrieve-rtmvars)
4983
(:definition positive-list)
4984
(:definition positivep)
4985
(:definition in-range)))
4988
(:instance correct-wrt-arity-has-rtmintvars-i-tl (mem (mem gstate)))
4989
(:instance sub-and-updates-holding-for-every-variable-type
4991
(ll (retrieve-rtmvars m))
4993
(gem1 (pos-equal-0 (par1 (nth (pcc gstate) (code gstate))) m))
4994
(gem2 (pos-equal-0 (par2 (nth (pcc gstate) (code gstate))) m))
4995
(gem3 (pos-equal-0 (par3 (nth (pcc gstate) (code gstate))) m))
5000
teorema-main-con-pcc-in-range-su-variabile-interessata-sub
5001
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
5002
(gvar (par1 (nth (pcc gstate) (code gstate)))))
5003
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
5004
(gvar (par2 (nth (pcc gstate) (code gstate)))))
5005
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
5006
(gvar (par3 (nth (pcc gstate) (code gstate)))))
5007
(:instance rtmintvars-i-is-pos-equal-0-of-retrieve-vars
5008
(gvar (par4 (nth (pcc gstate) (code gstate)))))))))
5011
(defthm equal-sub-and-update-norest-afetr-one-instr
5015
(in-range (pcc gstate) (code gstate))
5016
(good-translation-gem-rtm gstate rstate m)
5017
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5018
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
5019
(equal gvar2 (par2 (nth (pcc gstate) (code gstate))))
5020
(equal gvar3 (par3 (nth (pcc gstate) (code gstate)))))
5021
(equal (get-cell gvar1 (mem (execute-instruction gstate)))
5022
(sub-and-update-norest gvar1 gvar2 gvar3 (mem gstate))))
5023
:hints (("Goal" :in-theory (e/d (put-cell get-cell)
5024
(par1 par2 par3 par4 opcode pcc code nth gem-instruction-list-p
5025
gen-eq-update sub-and-update sub-and-update sub-and-update-norest sub-and-update-norest))))
5029
(DEFTHM mem-cellity-of-current-gem-args-sub
5031
(AND (GEM-STATEP GSTATE)
5032
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5033
(IN-RANGE (PCC GSTATE) (CODE GSTATE)))
5034
(AND (is-mem-cell-p (get-cell (PAR1 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))
5035
(is-mem-cell-p (get-cell (PAR2 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))
5036
(is-mem-cell-p (get-cell (PAR3 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))))
5040
(:INSTANCE IN-RANGE-INSTRUCTION-IS-GEM-INSTRUCTION
5042
(CODE (CODE GSTATE))
5043
(MEM (MEM GSTATE))))))
5047
(defthm type-is-for-pars-sub
5051
(vars-inclusion (mem gstate) m)
5053
(correct-wrt-arity m (mem gstate))
5054
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5055
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
5056
(equal gvar2 (par2 (nth (pcc gstate) (code gstate))))
5057
(equal gvar3 (par3 (nth (pcc gstate) (code gstate))))
5058
(in-range (pcc gstate) (code gstate)))
5059
(equal (type-i gvar1 m) 'int))
5061
:in-theory (disable type-i-is-type-expected rtmintvars-i-is-pos-equal-0-of-retrieve-vars)
5062
:use ( properies-of-type-and-existence-of-current-args-sub
5063
(:instance type-i-is-vartyper (gvar1 gvar1))
5064
(:instance type-i-is-vartyper (gvar1 gvar2))
5065
(:instance type-i-is-vartyper (gvar1 gvar3))
5066
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
5067
(v (par1 (nth (pcc gstate) (code gstate)))))
5068
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
5069
(v (par2 (nth (pcc gstate) (code gstate)))))
5070
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
5071
(v (par3 (nth (pcc gstate) (code gstate))))))))
5075
(defthm m-correspondence-kept-on-same-gvar-sub
5078
(good-translation-gem-rtm gstate rstate m)
5079
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5080
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
5082
(correct-wrt-arity m (mem gstate))
5085
(vars-inclusion (mem gstate) m)
5086
(in-range (pcc gstate) (code gstate))
5087
(in-range (pcc rstate) (code rstate))
5088
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
5089
(assoc-equal gvar1 m)
5090
(m-correspondent-values-p m (mem gstate) (mem rstate)))
5091
(equal-values-and-attributes
5092
(get-cell gvar1 (mem (execute-instruction gstate)))
5093
(rtmintvars-i gvar1 m)
5094
(mem (execute-n-instructions rstate (len *rns*)))
5096
:hints (("Goal" :in-theory nil
5098
properies-of-type-and-existence-of-current-args-sub
5099
mem-cellity-of-current-gem-args-sub
5100
good-translation-gem-rtm
5101
(:instance type-i-is-vartyper (gvar1 gvar1) (mem (mem gstate)))
5102
(:instance type-i-is-vartyper (gvar1 (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
5103
(:instance type-i-is-vartyper (gvar1 (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
5104
(:instance type-i-is-type-expected (gvar gvar1) (mem (mem gstate)))
5105
(:instance type-i-is-type-expected (gvar (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
5106
(:instance type-i-is-type-expected (gvar (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
5107
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
5108
(v (par1 (nth (pcc gstate) (code gstate)))))
5109
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
5110
(v (par2 (nth (pcc gstate) (code gstate)))))
5111
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
5112
(v (par3 (nth (pcc gstate) (code gstate)))))
5114
equal-sub-and-update-norest-afetr-one-instr
5115
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
5116
(gvar3 (par3 (nth (pcc gstate) (code gstate))))
5119
(:instance correct-wrt-arity-has-rtmintvars-i-tl (mem (mem gstate)))
5120
(:instance type-is-for-pars-sub
5121
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
5122
(gvar3 (par3 (nth (pcc gstate) (code gstate)))))
5123
(:instance m-correspondent-values-implies-equal-values-and-attribus
5124
(memgstate (mem gstate)) (memrstate (mem rstate))
5126
(:instance m-correspondent-values-implies-equal-values-and-attribus
5127
(memgstate (mem gstate)) (memrstate (mem rstate))
5128
(gvar1 (par2 (nth (pcc gstate) (code gstate)))))
5129
(:instance m-correspondent-values-implies-equal-values-and-attribus
5130
(memgstate (mem gstate)) (memrstate (mem rstate))
5131
(gvar1 (par3 (nth (pcc gstate) (code gstate)))))
5132
equal-sub-and-updates-after-n-instr
5134
if-gem-is-sub-and-update-inf-every-rtm-var-is-sub-and-update-then-equal-values-is-kept-g
5135
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
5136
(gvar3 (par3 (nth (pcc gstate) (code gstate))))
5137
(rtmvars1 (rtmintvars-i gvar1 m))
5138
(rtmvars2 (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m))
5139
(rtmvars3 (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m))
5140
(rtmvarsres (rtmintvars-i gvar1 m))
5141
(gemmem (mem gstate))
5142
(rtmmem (mem rstate))
5143
(rtmmemafter (mem (execute-n-instructions rstate (len *rns*)))))))))
5146
(defthm equal-values-correspondence-kept-by-any-execution-sub
5149
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5150
(good-translation-gem-rtm gstate rstate m)
5152
(correct-wrt-arity m (mem gstate))
5155
(vars-inclusion (mem gstate) m)
5156
(in-range (pcc gstate) (code gstate))
5157
(in-range (pcc rstate) (code rstate))
5158
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
5159
(assoc-equal gvar1 m)
5160
(m-correspondent-values-p m (mem gstate) (mem rstate)))
5161
(equal-values-and-attributes
5162
(get-cell gvar1 (mem (execute-instruction gstate)))
5163
(rtmintvars-i gvar1 m)
5164
(mem (execute-n-instructions rstate (len *rns*)))
5166
:hints (("Goal" :use (m-correspondence-kept-on-same-gvar-sub
5167
teorema-main-con-pcc-in-range-su-variabile-non-interessata-final-sub))))
5171
(defthm equal-values-correspondence-kept-by-any-execution-idxed-sub
5174
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5175
(no-duplicates-p (retrieve-gemvars m))
5176
(good-translation-gem-rtm gstate rstate m)
5178
(correct-wrt-arity m (mem gstate))
5181
(vars-inclusion (mem gstate) m)
5182
(in-range (pcc gstate) (code gstate))
5183
(in-range (pcc rstate) (code rstate))
5184
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
5186
(m-correspondent-values-p m (mem gstate) (mem rstate)))
5187
(equal-values-and-attributes
5188
(get-cell (car (nth idx m)) (mem (execute-instruction gstate)))
5190
(mem (execute-n-instructions rstate (len *rns*)))
5191
(type-i-idx m idx)))
5192
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero) '((:definition in-range)))
5200
(assoc-equal (car (nth idx m)) m))))
5202
(:instance type-i (gvar (car (nth idx m))))
5203
(:instance rtmintvars-i-is-cdr-of-nth-entry (gvar (car (nth idx m))))
5204
(:instance equal-values-correspondence-kept-by-any-execution-sub (gvar1 (car (nth idx m))))
5205
(:instance no-duplicates-has-pos-equal-right-in-that-place (l m)))))
5208
(defthm m-correspondence-kept-by-any-execution-idxed-sub
5211
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5212
(no-duplicates-p (retrieve-gemvars m))
5213
(good-translation-gem-rtm gstate rstate m)
5215
(correct-wrt-arity m (mem gstate))
5218
(vars-inclusion (mem gstate) m)
5219
(in-range (pcc gstate) (code gstate))
5220
(in-range (pcc rstate) (code rstate))
5221
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
5222
(m-correspondent-values-p m (mem gstate) (mem rstate)))
5223
(m-correspondent-values-p
5225
(mem (execute-instruction gstate))
5226
(mem (execute-n-instructions rstate (len *rns*)))))
5227
:hints (("Goal" :use (:instance equal-values-correspondence-kept-by-any-execution-idxed-sub
5228
(idx (bad-idx-eqv-va m
5229
(mem (execute-instruction gstate))
5230
(mem (execute-n-instructions rstate (len *rns*)))))))
5231
("Goal'" :cases ( (in-range (bad-idx-eqv-va m (mem (execute-instruction gstate))
5232
(mem (execute-n-instructions rstate (len *rns*)))) m)))
5233
("Subgoal 2" :in-theory '((:forward-chaining alistp-forward-to-true-listp)
5234
(:rewrite if-bad-index-not-in-range-then-m-corr)))
5235
("Subgoal 1" :in-theory '((:rewrite if-bad-index-in-range-thne-must-be-different-vs)))))
5240
(defthm m-correspondence-and-other-conditions-kept-by-any-execution-sub
5244
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-sub)
5245
(no-duplicates-p (retrieve-gemvars m))
5246
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
5247
(good-translation-gem-rtm gstate rstate m)
5248
(correct-wrt-arity m (mem gstate))
5251
(vars-inclusion (mem gstate) m)
5252
(vars-inclusion m (mem gstate))
5253
(in-range (pcc gstate) (code gstate))
5254
(in-range (pcc rstate) (code rstate))
5255
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
5256
(m-correspondent-values-p m (mem gstate) (mem rstate)))
5258
(good-translation-gem-rtm (execute-instruction gstate) (execute-n-instructions rstate (len *rns*)) m)
5259
(rtm-statep (execute-n-instructions rstate (len *rns*)))
5260
(m-entries-point-to-good-rtm-var-sets m (mem (execute-n-instructions rstate (len *rns*))))
5261
(gem-statep (execute-instruction gstate))
5262
(correct-wrt-arity m (mem (execute-instruction gstate)))
5263
(vars-inclusion (mem (execute-instruction gstate)) m)
5264
(vars-inclusion m (mem (execute-instruction gstate)))
5265
(m-correspondent-values-p
5267
(mem (execute-instruction gstate))
5268
(mem (execute-n-instructions rstate (len *rns*))))))
5271
rtm-statep gem-statep
5273
execute-instruction rtmintvars-i par1 par2 par3 nth len member-equal)
5275
(m-correspondence-kept-by-any-execution-idxed-sub
5276
good-translation-gem-rtm
5277
(:instance execute-n-instructions-keeps-rtm-state-and-points-to-good
5278
(st rstate) (n (len *rns*)))
5279
(:instance executing-gem-instruction-retrieves-a-gem-state-from-gem-state (st gstate))
5280
(:instance executing-gem-instruction-preserves-correctness-wrt-arity (st gstate))
5281
(:instance executing-gem-instruction-keeps-vars-inclusion-right (st gstate))
5282
(:instance executing-gem-instruction-keeps-vars-inclusion-left (st gstate))))))
5290
;;(ld "Proof-Of-Comparison.lisp" :ld-error-action :error)
5294
(defthm listinstr-of-2-unfolding-f
5298
(nth (pcc st) (code st))
5299
(nth (pcc (execute-instruction st)) (code (execute-instruction st)))))
5301
:in-theory (current-theory 'ground-zero)
5302
:use ( (:instance listinstr (n 2))
5303
(:instance listinstr (st (execute-instruction st)) (n 1))
5304
(:instance listinstr (st (execute-instruction (execute-instruction st))) (n 0))))))
5308
(defthm listinstr-of-2-has-the-two-instructions
5310
(equal (listinstr st 2)
5311
(rtm-eq-and v1 v2 tmp res))
5313
(equal (nth (pcc st) (code st))
5314
(list 'rtm-equ tmp v1 v2))
5315
(equal (nth (pcc (execute-instruction st)) (code (execute-instruction st)))
5316
(list 'rtm-and res tmp res))))
5317
:hints (("Goal" :in-theory (current-theory 'ground-zero)
5319
listinstr-of-2-unfolding-f ))))
5321
(defthm listinstr-of-2-has-the-two-opcodes
5323
(equal (listinstr st 2)
5324
(rtm-eq-and v1 v2 tmp res))
5326
(equal (opcode (nth (pcc st) (code st))) 'rtm-equ)
5327
(equal (par1 (nth (pcc st) (code st))) tmp)
5328
(equal (par2 (nth (pcc st) (code st))) v1)
5329
(equal (par3 (nth (pcc st) (code st))) v2)
5330
(equal (opcode (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) 'rtm-and)
5331
(equal (par1 (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) res)
5332
(equal (par2 (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) tmp)
5333
(equal (par3 (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) res)))
5334
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero)
5335
'((:definition par1)
5338
(:definition opcode)))
5339
:use (listinstr-of-2-has-the-two-instructions
5342
(equal (nth 0 (list a b c d)) a)
5343
(equal (nth 1 (list a b c d)) b)
5344
(equal (nth 2 (list a b c d)) c)
5345
(equal (nth 3 (list a b c d)) d)))
5352
(equal (nth 0 (list a b c d)) a)
5353
(equal (nth 1 (list a b c d)) b)
5354
(equal (nth 2 (list a b c d)) c)
5355
(equal (nth 3 (list a b c d)) d)))
5363
(defthm listinstr-of-2-or-the-two-instructions
5365
(equal (listinstr st 2)
5366
(rtm-eq-or v1 v2 tmp res))
5368
(equal (nth (pcc st) (code st))
5369
(list 'rtm-equ tmp v1 v2))
5370
(equal (nth (pcc (execute-instruction st)) (code (execute-instruction st)))
5371
(list 'rtm-or res tmp tmp))))
5372
:hints (("Goal" :in-theory (current-theory 'ground-zero)
5374
listinstr-of-2-unfolding-f ))))
5376
(defthm listinstr-of-2-or-has-the-two-opcodes
5378
(equal (listinstr st 2)
5379
(rtm-eq-or v1 v2 tmp res))
5381
(equal (opcode (nth (pcc st) (code st))) 'rtm-equ)
5382
(equal (par1 (nth (pcc st) (code st))) tmp)
5383
(equal (par2 (nth (pcc st) (code st))) v1)
5384
(equal (par3 (nth (pcc st) (code st))) v2)
5385
(equal (opcode (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) 'rtm-or)
5386
(equal (par1 (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) res)
5387
(equal (par2 (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) tmp)
5388
(equal (par3 (nth (pcc (execute-instruction st)) (code (execute-instruction st)))) tmp)))
5389
:hints (("Goal" :in-theory (union-theories (current-theory 'ground-zero)
5390
'((:definition par1)
5393
(:definition opcode)))
5394
:use (listinstr-of-2-or-the-two-instructions
5397
(equal (nth 0 (list a b c d)) a)
5398
(equal (nth 1 (list a b c d)) b)
5399
(equal (nth 2 (list a b c d)) c)
5400
(equal (nth 3 (list a b c d)) d)))
5407
(equal (nth 0 (list a b c d)) a)
5408
(equal (nth 1 (list a b c d)) b)
5409
(equal (nth 2 (list a b c d)) c)
5410
(equal (nth 3 (list a b c d)) d)))
5420
(defthm one-steps-of-execution
5422
(equal (listinstr st 2)
5423
(rtm-eq-and v1 v2 tmp res))
5424
(equal (execute-instruction st)
5425
(generic-eql tmp v1 v2 st)))
5427
:in-theory '((:definition execute-instruction))
5428
:use (listinstr-of-2-has-the-two-opcodes))))
5430
(defthm two-steps-of-execution
5432
(equal (listinstr st 2)
5433
(rtm-eq-and v1 v2 tmp res))
5434
(equal (execute-instruction (execute-instruction st))
5435
(rtm-and res tmp res (generic-eql tmp v1 v2 st))))
5437
:in-theory '((:definition execute-instruction))
5438
:use (listinstr-of-2-has-the-two-opcodes))))
5441
; Note: Below I have disabled a couple of names. This was not in the
5442
; original script. In the conversion from Version 2.5 to 2.6, we
5443
; added the case-split-limitations and choked it down from (nil nil)
5444
; -- the old default -- to something smaller. The first proof to
5445
; break was two-steps-inertia, below. In analyzing why it broke, I
5446
; realized that two-steps-of-execution was being :USEd but not
5447
; DISABLEd. So it could be rewritten away. Disabling it, however,
5448
; had no good effect. Then I realized that it could be rewritten away
5449
; by proving it again, which meant using the definition of
5450
; execute-instruction. So I disabled that too. And voila, the proof
5451
; happens very quickly, without significant case analysis -- certainly
5452
; without approaching the case-split-limitations. You will see a
5453
; similar pair of disables once more below.
5455
(defthm two-steps-inertia
5458
(equal (listinstr st 2)
5459
(rtm-eq-and v1 v2 tmp res))
5460
(not (equal tmp vx1))
5461
(not (equal res vx1)))
5462
(equal (get-cell vx1 (mem (execute-instruction (execute-instruction st))))
5463
(get-cell vx1 (mem st))))
5464
:hints (("Goal" :in-theory (disable execute-instruction ; (See note above.)
5465
two-steps-of-execution ; (See note above.)
5466
opcode one-steps-of-execution;par1 par2 par3 pcc code
5467
gem-add gem-sub rtm-add rtm-sub and-update gen-eq-update)
5468
:use (two-steps-of-execution))))
5472
(defthm two-steps-inertia-on-sequence-of-vars
5475
(equal (listinstr st 2) (rtm-eq-and v1 v2 tmp res))
5476
(not (member-equal-bool tmp listvars1))
5477
(not (member-equal-bool res listvars1)))
5479
(var-values listvars1 (mem st))
5480
(var-values listvars1 (mem (execute-instruction (execute-instruction st))))))
5482
:induct (var-values listvars1 (mem st))
5483
:in-theory (disable listinstr-of-2-unfolding-f
5484
two-steps-of-execution execute-instruction one-steps-of-execution))
5485
("Subgoal *1/2" :use (:instance two-steps-inertia (vx1 (car listvars1))))))
5488
(defthm two-steps-res
5491
(equal (listinstr st 2)
5492
(rtm-eq-and v1 v2 tmp res))
5493
(not (equal tmp v1))
5494
(not (equal tmp v2))
5495
(not (equal res v1))
5496
(not (equal res v2))
5497
(not (equal tmp res)))
5498
(equal (var-value (get-cell res (mem (rtm-and res tmp res (generic-eql tmp v1 v2 st)))))
5502
(boolean-to-int (equal (var-value (get-cell v1 (mem st)))
5503
(var-value (get-cell v2 (mem st))))))
5504
(int-to-bool (var-value (get-cell res (mem st))))))))
5507
(make-cell put-cell get-cell var-value)
5508
(opcode one-steps-of-execution execute-instruction
5509
int-to-bool boolean-to-int
5510
gem-add gem-sub rtm-add rtm-sub )))))
5513
(defthm one-steps-of-execution-or
5515
(equal (listinstr st 2)
5516
(rtm-eq-or v1 v2 tmp res))
5517
(equal (execute-instruction st)
5518
(generic-eql tmp v1 v2 st)))
5520
:in-theory '((:definition execute-instruction))
5521
:use (listinstr-of-2-or-has-the-two-opcodes))))
5523
(defthm two-steps-of-execution-or
5525
(equal (listinstr st 2)
5526
(rtm-eq-or v1 v2 tmp res))
5527
(equal (execute-instruction (execute-instruction st))
5528
(rtm-or res tmp tmp (generic-eql tmp v1 v2 st))))
5530
:in-theory '((:definition execute-instruction))
5531
:use (listinstr-of-2-or-has-the-two-opcodes))))
5534
(defthm two-steps-inertia-or
5537
(equal (listinstr st 2)
5538
(rtm-eq-or v1 v2 tmp res))
5539
(not (equal tmp vx1))
5540
(not (equal res vx1)))
5541
(equal (get-cell vx1 (mem (execute-instruction (execute-instruction st))))
5542
(get-cell vx1 (mem st))))
5543
:hints (("Goal" :in-theory (disable execute-instruction ; (See note above.)
5544
two-steps-of-execution-or ; (See note above.)
5545
opcode one-steps-of-execution-or ;par1 par2 par3 pcc code
5546
gem-add gem-sub rtm-add rtm-sub and-update gen-eq-update or-update)
5547
:use (two-steps-of-execution-or))))
5551
(defthm two-steps-inertia-on-sequence-of-vars-or
5554
(equal (listinstr st 2) (rtm-eq-or v1 v2 tmp res))
5555
(not (member-equal-bool tmp listvars1))
5556
(not (member-equal-bool res listvars1)))
5558
(var-values listvars1 (mem st))
5559
(var-values listvars1 (mem (execute-instruction (execute-instruction st))))))
5561
:induct (var-values listvars1 (mem st))
5562
:in-theory (disable listinstr-of-2-unfolding-f
5563
two-steps-of-execution-or execute-instruction one-steps-of-execution-or))
5564
("Subgoal *1/2" :use (:instance two-steps-inertia-or (vx1 (car listvars1))))))
5567
(defthm two-steps-res-or
5570
(equal (listinstr st 2)
5571
(rtm-eq-or v1 v2 tmp res))
5572
(not (equal tmp v1))
5573
(not (equal tmp v2))
5574
(not (equal res v1))
5575
(not (equal res v2))
5576
(not (equal tmp res)))
5577
(equal (var-value (get-cell res (mem (rtm-or res tmp tmp (generic-eql tmp v1 v2 st)))))
5579
(equal (var-value (get-cell v1 (mem st)))
5580
(var-value (get-cell v2 (mem st)))))))
5586
(boolean-to-int (equal (var-value (get-cell v1 (mem st)))
5587
(var-value (get-cell v2 (mem st))))))
5589
(boolean-to-int (equal (var-value (get-cell v1 (mem st)))
5590
(var-value (get-cell v2 (mem st)))))))
5591
(equal (var-value (get-cell v1 (mem st)))
5592
(var-value (get-cell v2 (mem st))))))
5594
(make-cell put-cell get-cell var-value)
5595
(opcode one-steps-of-execution-or execute-instruction
5596
int-to-bool boolean-to-int
5597
gem-add gem-sub rtm-add rtm-sub )))))
5601
(defthm execute-instruction-2-unfolding
5603
(execute-n-instructions st 2)
5604
(execute-instruction (execute-instruction st)))
5606
:in-theory (current-theory 'ground-zero)
5608
((:instance execute-n-instructions (n 2))
5609
(:instance execute-n-instructions (st (execute-instruction st)) (n 1))
5610
(:instance execute-n-instructions (st (execute-instruction (execute-instruction st))) (n 0))))))
5614
(defthm two-steps-res-2
5617
(equal (listinstr st 2)
5618
(rtm-eq-and v1 v2 tmp res))
5619
(not (equal tmp v1))
5620
(not (equal tmp v2))
5621
(not (equal res v1))
5622
(not (equal res v2))
5623
(not (equal tmp res)))
5624
(equal (var-value (get-cell res (mem (execute-n-instructions st 2))))
5627
(equal (var-value (get-cell v1 (mem st)))
5628
(var-value (get-cell v2 (mem st))))
5629
(int-to-bool (var-value (get-cell res (mem st))))))))
5630
:hints (("Goal" :in-theory '((:definition int-to-bool)
5631
(:definition boolean-to-int))
5632
:use (two-steps-res two-steps-of-execution execute-instruction-2-unfolding))))
5635
(defthm two-steps-res-or-2
5638
(equal (listinstr st 2)
5639
(rtm-eq-or v1 v2 tmp res))
5640
(not (equal tmp v1))
5641
(not (equal tmp v2))
5642
(not (equal res v1))
5643
(not (equal res v2))
5644
(not (equal tmp res)))
5645
(equal (var-value (get-cell res (mem (execute-n-instructions st 2))))
5647
(equal (var-value (get-cell v1 (mem st)))
5648
(var-value (get-cell v2 (mem st)))))))
5649
:hints (("Goal" :in-theory '((:definition int-to-bool)
5650
(:definition boolean-to-int))
5651
:use (two-steps-res-or two-steps-of-execution-or execute-instruction-2-unfolding))))
5654
(defthm int-bool-int-cancellation
5655
(equal (int-to-bool (boolean-to-int (equal v1 v2))) (equal v1 v2)))
5657
(defthm bool-int-bool-cancellation
5659
(or (equal res 0) (equal res 1))
5660
(equal (boolean-to-int (int-to-bool res)) res)))
5662
(defun eq-values (listvars1 listvars2 res mem n)
5670
(equal (var-value (get-cell (car listvars1) mem))
5671
(var-value (get-cell (car listvars2) mem)))
5677
(defun equal-lv (listvars1 listvars2 mem n)
5678
(declare (xargs :measure (acl2-count n)))
5683
(var-value (get-cell (car listvars1) mem))
5684
(var-value (get-cell (car listvars2) mem)))
5685
(equal-lv (cdr listvars1) (cdr listvars2) mem (1- n)))))
5689
(equal (eq-values listvars1 listvars2 0 mem n) 0))
5692
(equal (eq-values listvars1 listvars2 1 mem n) (boolean-to-int (equal-lv listvars1 listvars2 mem n))))
5694
(defthm eq-values-is-equal-lv
5697
(or (equal res 0) (equal res 1))
5698
(equal n (len listvars2))
5699
(equal n (len listvars1)))
5701
(eq-values listvars1 listvars2 res mem n)
5704
(equal-lv listvars1 listvars2 mem n)
5705
(int-to-bool res)))))
5706
:hints (("Goal" :in-theory (disable int-to-bool boolean-to-int))))
5709
(defthm equal-lv-is-equal-values
5712
(equal n (len listvars1))
5713
(equal n (len listvars2)))
5715
(equal-lv listvars1 listvars2 mem n)
5717
(var-values listvars1 mem)
5718
(var-values listvars2 mem)))))
5721
(defthm eq-values-is-equal-values
5724
(or (equal res 0) (equal res 1))
5725
(equal n (len listvars2))
5726
(equal n (len listvars1)))
5728
(eq-values listvars1 listvars2 res mem n)
5732
(var-values listvars1 mem)
5733
(var-values listvars2 mem))
5734
(int-to-bool res))))))
5737
(defun induct-support (listvars1 listvars2 tmp res st)
5741
(cons (list (car listvars1) (car listvars2) tmp res (pcc st))
5747
(execute-n-instructions st 2)))))
5752
(not (endp listvars1))
5753
(not (member-equal-bool tmp listvars1))
5754
(not (member-equal-bool tmp listvars2))
5755
(not (member-equal-bool res listvars1))
5756
(not (member-equal-bool res listvars2)))
5758
(not (member-equal-bool tmp (cdr listvars1)))
5759
(not (member-equal-bool tmp (cdr listvars2)))
5760
(not (member-equal-bool res (cdr listvars1)))
5761
(not (member-equal-bool res (cdr listvars2))))))
5763
(defthm listinstr-is-decomposed
5769
(listinstr (execute-n-instructions st n) m)
5770
(nthcdr n (listinstr st (+ n m)))))
5772
:induct (execute-n-instructions st n)
5773
:in-theory (disable execute-instruction))))
5775
(defthm nthcdr-2-unfolding
5776
(equal (nthcdr 2 l) (cddr l)))
5778
(defthm nthcdr2ofeqtrans2
5780
(not (endp listvars1))
5782
(equality-trans2 (cdr listvars1) (cdr listvars2) tmp res)
5783
(nthcdr 2 (equality-trans2 listvars1 listvars2 tmp res))))
5784
:hints (("Goal" :use
5785
( (:instance nthcdr-2-unfolding
5786
(l (equality-trans2 listvars1 listvars2 tmp res)))
5788
:in-theory (union-theories (current-theory 'ground-zero) '((:definition rtm-eq-and))))))
5790
(in-theory (disable nthcdr-2-unfolding nthcdr2ofeqtrans2 listinstr-is-decomposed))
5794
(not (endp listvars1))
5795
(equal (listinstr (execute-n-instructions st 2) (* 2 (len (cdr listvars1))))
5796
(nthcdr 2 (listinstr st (* 2 (len listvars1))))))
5799
(:instance listinstr-is-decomposed
5801
(m (* 2 (len (cdr listvars1))))))
5802
:in-theory (disable execute-instruction execute-instruction-2-unfolding is-mem-cell-p))))
5807
(not (endp listvars1))
5808
(equal (listinstr st (* 2 (len listvars1)))
5809
(equality-trans2 listvars1 listvars2 tmp res)))
5810
(equal (listinstr (execute-n-instructions st 2) (* 2 (len (cdr listvars1))))
5811
(equality-trans2 (cdr listvars1) (cdr listvars2) tmp res)))
5814
:use (nthcdr2ofeqtrans2 support-2a))))
5818
(defthm listinstr-append
5826
(listinstr st (+ m n))
5827
(append (listinstr st m)
5828
(listinstr (execute-n-instructions st m) n))))
5830
:in-theory (disable execute-instruction))))
5835
(equal l (append l1 l2))
5838
(equal (car l1) (car l))
5839
(equal (cadr l1) (cadr l)))))
5841
(defthm length-of-listintr
5846
(equal (len (listinstr st n)) n)))
5848
(defthm first-2-instr-are-same-if-many
5854
(equal (car (listinstr st 2)) (car (listinstr st le)))
5855
(equal (cadr (listinstr st 2)) (cadr (listinstr st le)))))
5856
:hints (("Goal" :in-theory (current-theory 'ground-zero)
5859
(:theorem (implies (integerp le) (equal (+ 2 -2 le) le)))
5861
(l1 (listinstr st 2))
5862
(l2 (listinstr (execute-n-instructions st 2) (- le 2)))
5863
(l (listinstr st le)))
5864
(:instance length-of-listintr (n 2))
5865
(:instance listinstr-append
5870
(defthm first-2-instr-are-same-if-many-inst
5872
(not (endp listvars1))
5874
(equal (car (listinstr st 2)) (car (listinstr st (* 2 (len listvars1)))))
5875
(equal (cadr (listinstr st 2)) (cadr (listinstr st (* 2 (len listvars1)))))))
5877
:in-theory (current-theory 'ground-zero)
5878
:use (:instance first-2-instr-are-same-if-many (le (* 2 (len listvars1))))))
5883
(defthm first-two-instructions-are-eq-and
5886
(not (endp listvars1))
5887
(equal (listinstr st (* 2 (len listvars1)))
5888
(equality-trans2 listvars1 listvars2 tmp res)))
5889
(equal (listinstr st 2) (rtm-eq-and (car listvars1) (car listvars2) tmp res)))
5891
:in-theory (disable execute-instruction)
5892
:use first-2-instr-are-same-if-many-inst)))
5899
(equal (listinstr st (* 2 (len listvars1)))
5900
(equality-trans2 listvars1 listvars2 tmp res))
5901
(not (endp listvars1))
5902
(not (endp listvars2))
5903
(not (member-equal-bool tmp listvars1))
5904
(not (member-equal-bool tmp listvars2))
5905
(not (member-equal-bool res listvars1))
5906
(not (member-equal-bool res listvars2))
5907
(not (equal tmp res)))
5912
(var-value (get-cell res (mem st)))
5918
(var-value (get-cell res (mem (execute-n-instructions st 2))))
5920
(len (cdr listvars1)))))
5922
:in-theory (disable listinstr-append listinstr-of-2-unfolding-f
5923
execute-instruction one-steps-of-execution execute-instruction-2-unfolding)
5925
(first-two-instructions-are-eq-and
5926
(:instance two-steps-res-2 (v1 (car listvars1)) (v2 (car listvars2)))))))
5935
(equal (listinstr st (* 2 (len listvars1)))
5936
(equality-trans2 listvars1 listvars2 tmp res))
5937
(not (endp listvars1))
5938
(not (endp listvars2))
5939
(equal (len listvars1) (len listvars2))
5940
(not (member-equal-bool tmp listvars1))
5941
(not (member-equal-bool tmp listvars2))
5942
(not (member-equal-bool res listvars1))
5943
(not (member-equal-bool res listvars2))
5944
(not (equal tmp res)))
5949
(var-value (get-cell res (mem st)))
5955
(var-value (get-cell res (mem (execute-n-instructions st 2))))
5956
(mem (execute-instruction (execute-instruction st)))
5957
(len (cdr listvars1)))))
5959
:in-theory (disable listinstr-append listinstr-of-2-unfolding-f
5960
execute-instruction one-steps-of-execution execute-instruction-2-unfolding)
5962
(first-two-instructions-are-eq-and
5963
(:instance two-steps-inertia-on-sequence-of-vars
5964
(v1 (car listvars1))
5965
(v2 (car listvars2))
5966
(listvars1 (cdr listvars1)))
5967
(:instance two-steps-inertia-on-sequence-of-vars
5968
(v1 (car listvars1))
5969
(v2 (car listvars2))
5970
(listvars1 (cdr listvars2)))
5971
(:instance two-steps-res-2 (v1 (car listvars1)) (v2 (car listvars2)))))))
5980
(defthm value-of-result-after-executing-2n-instr
5983
(not (member-equal-bool tmp listvars1))
5984
(not (member-equal-bool tmp listvars2))
5985
(not (member-equal-bool res listvars1))
5986
(not (member-equal-bool res listvars2))
5987
(equal (len listvars1) (len listvars2))
5988
(not (equal tmp res))
5989
(equal (listinstr st (* 2 (len listvars1)))
5990
(equality-trans2 listvars1 listvars2 tmp res)))
5995
(mem (execute-n-instructions st (* 2 (len listvars1))))))
5999
(var-value (get-cell res (mem st)))
6003
:in-theory (disable execute-instruction is-mem-cell-p)
6004
:induct (induct-support listvars1 listvars2 tmp res st))
6005
("Subgoal *1/2" :use (support-1 support-2 support-3))))
6008
(defthm value-of-result-after-executing-2n-instr-fin
6011
(not (member-equal-bool tmp listvars1))
6012
(not (member-equal-bool tmp listvars2))
6013
(not (member-equal-bool res listvars1))
6014
(not (member-equal-bool res listvars2))
6015
(equal (len listvars1) (len listvars2))
6017
(equal (var-value (get-cell res (mem st))) 0)
6018
(equal (var-value (get-cell res (mem st))) 1))
6019
(not (equal tmp res))
6020
(equal (listinstr st (* 2 (len listvars1)))
6021
(equality-trans2 listvars1 listvars2 tmp res)))
6026
(mem (execute-n-instructions st (* 2 (len listvars1))))))
6030
(var-values listvars1 (mem st))
6031
(var-values listvars2 (mem st)))
6032
(int-to-bool (var-value (get-cell res (mem st))))))))
6034
:in-theory (disable execute-instruction is-mem-cell-p)
6035
:use (value-of-result-after-executing-2n-instr))))
6036
(defthm nthcdr2ofeqtrans3
6038
(equality-trans2 (cdr listvars1) (cdr listvars2) tmp res)
6039
(nthcdr 2 (equality-trans3 listvars1 listvars2 tmp res)))
6040
:hints (("Goal" :use
6041
( (:instance nthcdr-2-unfolding
6042
(l (equality-trans3 listvars1 listvars2 tmp res)))
6044
:in-theory (union-theories (current-theory 'ground-zero) '((:definition rtm-eq-or))))))
6046
(in-theory (disable nthcdr-2-unfolding nthcdr2ofeqtrans3 listinstr-is-decomposed))
6052
(not (endp listvars1))
6053
(equal (listinstr st (* 2 (len listvars1)))
6054
(equality-trans3 listvars1 listvars2 tmp res)))
6055
(equal (listinstr (execute-n-instructions st 2) (* 2 (len (cdr listvars1))))
6056
(equality-trans2 (cdr listvars1) (cdr listvars2) tmp res)))
6059
:use (nthcdr2ofeqtrans3 support-2a))))
6063
(defthm first-two-instructions-are-eq-or
6066
(not (endp listvars1))
6067
(equal (listinstr st (* 2 (len listvars1)))
6068
(equality-trans3 listvars1 listvars2 tmp res)))
6069
(equal (listinstr st 2) (rtm-eq-or (car listvars1) (car listvars2) tmp res)))
6071
:in-theory (disable nthcdr nthcdr2ofeqtrans3 execute-instruction
6074
:use first-2-instr-are-same-if-many-inst)))
6081
(not (endp listvars1))
6083
(EXECUTE-N-INSTRUCTIONS (EXECUTE-N-INSTRUCTIONS ST 2) (* 2 (LEN (CDR LISTVARS1))))
6084
(EXECUTE-N-INSTRUCTIONS ST (* 2 (LEN LISTVARS1)))))
6086
:in-theory (current-theory 'ground-zero)
6088
(:instance execute-n-instruction-decomposition
6090
(n2 (* 2 (1- (len listvars1))))))
6092
:use ((:theorem (equal (+ -2 2 (* 2 (LEN (CDR LISTVARS1))))
6093
(* 2 (LEN (CDR LISTVARS1)))))
6094
(:theorem (equal (+ 2 (* 2 (LEN (CDR LISTVARS1))))
6095
(+ 2 -2 2 (* 2 (LEN (CDR LISTVARS1))))))))))
6098
(defthm value-of-result-after-executing-2n-+2instr-fin
6101
(not (member-equal-bool tmp listvars1))
6102
(not (member-equal-bool tmp listvars2))
6103
(not (member-equal-bool res listvars1))
6104
(not (member-equal-bool res listvars2))
6105
(equal (len listvars1) (len listvars2))
6106
(not (endp listvars1))
6107
(not (equal tmp res))
6108
(equal (listinstr st (* 2 (len listvars1)))
6109
(equality-trans3 listvars1 listvars2 tmp res)))
6114
(mem (execute-n-instructions st (* 2 (len listvars1))))))
6118
(var-values (cdr listvars1) (mem (execute-n-instructions st 2)))
6119
(var-values (cdr listvars2) (mem (execute-n-instructions st 2))))
6122
(equal (var-value (get-cell (car listvars1) (mem st)))
6123
(var-value (get-cell (car listvars2) (mem st))))))))))
6125
:in-theory (union-theories (current-theory 'ground-zero)
6126
'((:definition member-equal-bool)
6127
(:definition boolean-to-int)))
6132
first-two-instructions-are-eq-or
6133
(:instance value-of-result-after-executing-2n-instr-fin
6134
(st (execute-n-instructions st 2))
6135
(listvars1 (cdr listvars1))
6136
(listvars2 (cdr listvars2)))
6137
(:instance two-steps-res-or-2
6138
(v1 (car listvars1))
6139
(v2 (car listvars2)))))))
6142
(defthm at-the-end-equality-on-all
6145
(not (endp listvars1))
6146
(equal (len listvars1) (len listvars2)))
6150
(var-values listvars1 (mem st ))
6151
(var-values listvars2 (mem st ))))
6155
(var-values (cdr listvars1) (mem st ))
6156
(var-values (cdr listvars2) (mem st )))
6159
(equal (var-value (get-cell (car listvars1) (mem st)))
6160
(var-value (get-cell (car listvars2) (mem st)))))))))))
6168
(defthm value-of-result-after-executing-2n-+2instr-finale
6171
(not (member-equal-bool tmp listvars1))
6172
(not (member-equal-bool tmp listvars2))
6173
(not (member-equal-bool res listvars1))
6174
(not (member-equal-bool res listvars2))
6175
(equal (len listvars1) (len listvars2))
6176
(not (endp listvars1))
6177
(not (equal tmp res))
6178
(equal (listinstr st (* 2 (len listvars1)))
6179
(equality-trans3 listvars1 listvars2 tmp res)))
6184
(mem (execute-n-instructions st (* 2 (len listvars1))))))
6187
(var-values listvars1 (mem st ))
6188
(var-values listvars2 (mem st ))))))
6191
(union-theories (current-theory 'ground-zero)
6192
'((:rewrite execute-instruction-2-unfolding)
6193
(:definition member-equal-bool)))
6195
(:instance two-steps-inertia-on-sequence-of-vars-or
6196
(v1 (car listvars1))
6197
(v2 (car listvars2))
6198
(listvars1 (cdr listvars1)))
6199
(:instance two-steps-inertia-on-sequence-of-vars-or
6200
(v1 (car listvars1))
6201
(v2 (car listvars2))
6202
(listvars1 (cdr listvars2)))
6203
first-two-instructions-are-eq-or
6204
value-of-result-after-executing-2n-+2instr-fin
6205
at-the-end-equality-on-all))))
6209
listinstr-of-2-unfolding-f listinstr-of-2-has-the-two-instructions listinstr-of-2-has-the-two-opcodes
6210
listinstr-of-2-or-the-two-instructions listinstr-of-2-or-has-the-two-opcodes
6211
one-steps-of-execution two-steps-of-execution two-steps-inertia
6212
two-steps-inertia-on-sequence-of-vars two-steps-res
6213
one-steps-of-execution-or two-steps-of-execution-or two-steps-inertia-or
6214
two-steps-inertia-on-sequence-of-vars-or two-steps-res-or
6215
execute-instruction-2-unfolding two-steps-res-2 two-steps-res-or-2
6216
int-bool-int-cancellation bool-int-bool-cancellation case-zero case-one
6217
equal-lv-is-equal-values eq-values-is-equal-values
6218
support-1 listinstr-is-decomposed nthcdr-2-unfolding support-2a support-2
6219
listinstr-append silly-00 length-of-listintr
6220
first-2-instr-are-same-if-many first-2-instr-are-same-if-many-inst
6221
first-two-instructions-are-eq-and support-3a support-3
6222
value-of-result-after-executing-2n-instr value-of-result-after-executing-2n-instr-fin
6223
equality-trans3 nthcdr2ofeqtrans3 support-2b
6224
first-two-instructions-are-eq-or support4
6225
value-of-result-after-executing-2n-+2instr-fin
6226
at-the-end-equality-on-all value-of-result-after-executing-2n-+2instr-finale))
6228
(defun pars1-instructions (listinstr)
6229
(if (endp listinstr)
6231
(cons (par1 (car listinstr))
6232
(pars1-instructions (cdr listinstr)))))
6234
(defthm pars1-instruction-is-listpars1
6236
(pars1-instructions (listinstr st n))
6241
(defun eqtr2 (l1 tmp res)
6245
(append (list tmp res) (eqtr2 (cdr l1) tmp res))))
6247
(defun eqtr3 (l1 tmp res)
6248
(append (list tmp res) (eqtr2 (cdr l1) tmp res)))
6250
(defthm cgr1 (equal (pars1-instructions (equality-trans2 l1 l2 tmp res)) (eqtr2 l1 tmp res)))
6252
(defthm pars1iappend
6253
(equal (pars1-instructions (append l1 l2))
6254
(append (pars1-instructions l1) (pars1-instructions l2))))
6256
(defthm parsi-instructions-of-eq3-are-eqtr3
6257
(equal (pars1-instructions (equality-trans3 l1 l2 tmp res)) (eqtr3 l1 tmp res))
6258
:hints (("Subgoal 2" :in-theory nil)
6260
(:instance pars1iappend
6261
(l1 (rtm-eq-or (car l1) (car l2 ) tmp res))
6262
(l2 (equality-trans2 (cdr l1) (cdr l2) tmp res)))
6263
(:instance cgr1 (l1 (cdr l1)) (l2 (cdr l2)))
6264
(:theorem (equal (pars1-instructions (rtm-eq-or (car l1) (car l2) tmp res)) (list tmp res)))
6265
(:instance equality-trans3 (listvars1 l1) (listvars2 l2))))))
6268
(defthm only-tmp-res-into-eqtr3
6272
(not (equal v res)))
6273
(not (member-equal-bool v (eqtr3 l1 tmp res))))
6280
(defthm equality-trans3-has-par1-made-of-tmp-res
6287
(equality-trans3 l1 l2 tmp res)))
6288
(not (member-equal-bool v (listpars1 st n))))
6289
:hints (("Goal" :in-theory nil
6290
:use (pars1-instruction-is-listpars1
6291
parsi-instructions-of-eq3-are-eqtr3
6292
only-tmp-res-into-eqtr3))))
6301
(DEFUN LISTOPCODES (ST N)
6304
(CONS (OPCODE (NTH (PCC ST) (CODE ST)))
6305
(LISTOPCODES (EXECUTE-INSTRUCTION ST)
6307
(defun all-par1ops (opcodes)
6312
(equal (car opcodes) 'rtm-and)
6313
(equal (car opcodes) 'rtm-or)
6314
(equal (car opcodes) 'rtm-equ)
6315
(equal (car opcodes) 'rtm-add)
6316
(equal (car opcodes) 'rtm-sub))
6317
(all-par1ops (cdr opcodes)))))
6319
(defun all-par1opso (st n)
6320
(declare (xargs :measure (acl2-count n)))
6325
(null (NTH (PCC ST) (CODE ST)))
6326
(equal (OPCODE (NTH (PCC ST) (CODE ST))) 'rtm-and)
6327
(equal (OPCODE (NTH (PCC ST) (CODE ST))) 'rtm-or)
6328
(equal (OPCODE (NTH (PCC ST) (CODE ST))) 'rtm-equ)
6329
(equal (OPCODE (NTH (PCC ST) (CODE ST))) 'rtm-add)
6330
(equal (OPCODE (NTH (PCC ST) (CODE ST))) 'rtm-sub))
6331
(all-par1opso (execute-instruction st) (1- n)))))
6335
(defthm if-only-par1-involving-ops-are-there-then-other-vars-are-untouched
6339
(not (member-equal-bool v (listpars1 st n))))
6340
(equal (get-cell v (mem st)) (get-cell v (mem (execute-n-instructions st n)))))
6341
:hints (("Goal" :in-theory (disable execute-instruction))
6342
("Subgoal *1/2" :use (:instance only-par1-is-involved-rtm
6349
(defun pars1-opcodes (listinstr)
6350
(if (endp listinstr)
6352
(cons (opcode (car listinstr))
6353
(pars1-opcodes (cdr listinstr)))))
6355
(defthm pars1-opcodes-is-listopcodes
6357
(pars1-opcodes (listinstr st n))
6358
(listopcodes st n)))
6364
(append (list 'rtm-equ 'rtm-and) (eqtr2o (cdr l1)))))
6367
(append (list 'rtm-equ 'rtm-or) (eqtr2o (cdr l1))))
6369
(defthm cgr2 (equal (pars1-opcodes (equality-trans2 l1 l2 tmp res)) (eqtr2o l1)))
6371
(defthm pars1oappend
6372
(equal (pars1-opcodes (append l1 l2))
6373
(append (pars1-opcodes l1) (pars1-opcodes l2))))
6375
(defthm parsi-opcodes-of-eq3-are-eqtr3o
6376
(equal (pars1-opcodes (equality-trans3 l1 l2 tmp res)) (eqtr3o l1))
6377
:hints (("Subgoal 2" :in-theory nil)
6378
("Goal" :use (eqtr3o
6379
(:instance pars1oappend
6380
(l1 (rtm-eq-or (car l1) (car l2 ) tmp res))
6381
(l2 (equality-trans2 (cdr l1) (cdr l2) tmp res)))
6382
(:instance cgr2 (l1 (cdr l1)) (l2 (cdr l2)))
6383
(:theorem (equal (pars1-opcodes (rtm-eq-or (car l1) (car l2) tmp res)) (list 'rtm-equ 'rtm-or)))
6384
(:instance equality-trans3 (listvars1 l1) (listvars2 l2))))))
6387
(defthm eqtr3o-makes-par1-instrs
6388
(all-par1ops (eqtr3o l))
6393
(defthm opcodes-on-par1-imply-instructions-on-par1
6395
(all-par1ops (pars1-opcodes (listinstr st n)))
6396
(all-par1opso st n)))
6398
(defthm if-instructions-are-trans3-and-v-non-in-par1-v-untouched
6401
(equal (listinstr st n)
6402
(equality-trans3 l1 l2 tmp res))
6403
(not (member-equal-bool v (listpars1 st n))))
6405
(get-cell v (mem st))
6406
(get-cell v (mem (execute-n-instructions st n)))))
6410
(opcodes-on-par1-imply-instructions-on-par1
6411
pars1-opcodes-is-listopcodes
6412
parsi-opcodes-of-eq3-are-eqtr3o
6413
(:instance eqtr3o-makes-par1-instrs (l l1))
6414
if-only-par1-involving-ops-are-there-then-other-vars-are-untouched))))
6417
(defthm equality-trans3-means-touching-just-tmp-res
6424
(equality-trans3 l1 l2 tmp res)))
6426
(get-cell v (mem st))
6427
(get-cell v (mem (execute-n-instructions st n)))))
6430
(if-instructions-are-trans3-and-v-non-in-par1-v-untouched
6431
equality-trans3-has-par1-made-of-tmp-res))))
6438
pars1-instructions pars1-instruction-is-listpars1
6439
eqtr2 eqtr3 cgr1 pars1iappend parsi-instructions-of-eq3-are-eqtr3
6440
only-tmp-res-into-eqtr3 equality-trans3-has-par1-made-of-tmp-res
6441
all-par1ops all-par1opso
6442
if-only-par1-involving-ops-are-there-then-other-vars-are-untouched
6443
pars1-opcodes pars1-opcodes-is-listopcodes
6444
eqtr2o eqtr3o cgr2 pars1oappend parsi-opcodes-of-eq3-are-eqtr3o
6445
eqtr3o-makes-par1-instrs opcodes-on-par1-imply-instructions-on-par1
6446
if-instructions-are-trans3-and-v-non-in-par1-v-untouched))
6450
(defthm lemma2-only-adds-in-rtm-equ
6455
(in-range (pcc gstate) (code gstate))
6456
(in-range (pcc rstate) (code rstate))
6457
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6458
(good-translation-gem-rtm gstate rstate m))
6460
(equal (listinstr rstate (* 2 (len *rns*)) )
6462
(eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*))
6463
(eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*))
6465
(car (rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m))))
6467
(par1 (nth (pcc gstate) (code gstate)))
6468
(par2 (nth (pcc gstate) (code gstate)))))
6470
(par1 (nth (pcc gstate) (code gstate)))
6471
(par3 (nth (pcc gstate) (code gstate)))))))
6472
:hints (("Goal" :expand
6473
( (good-translation-gem-rtm gstate rstate m)
6476
(in-range (pcc gstate) (code gstate))
6477
(in-range (pcc rstate) (code rstate)))
6483
(defthm lemma1-different-vars-do-not-belong-ref
6487
(not (endp (rtmintvars-i gvar2 m)))
6488
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
6489
(assoc-equal gvar1 m)
6490
(assoc-equal gvar2 m)
6491
(not (equal gvar1 gvar2))
6492
(in-range idx1 (rtmintvars-i gvar1 m)))
6493
(not (equal (nth idx1 (rtmintvars-i gvar1 m))
6494
(car (rtmintvars-i gvar2 m)))))
6495
:hints (("Goal" :in-theory nil
6496
:use (lemma1-different-vars-do-not-belong
6497
(:instance member-equal-bool
6498
(el (nth idx1 (rtmintvars-i gvar1 m)))
6499
(l (rtmintvars-i gvar2 m)))))))
6501
(defun no-tmp-into-mapping (m)
6505
(not (member-equal-bool 'tmp (rtmintvars-0 m)))
6506
(no-tmp-into-mapping (cdr m)))))
6508
(defthm a-variable-is-never-tmp
6511
(no-tmp-into-mapping m)
6512
(assoc-equal gvar1 m)
6513
(in-range idx1 (rtmintvars-i gvar1 m)))
6514
(not (equal (nth idx1 (rtmintvars-i gvar1 m)) 'tmp)))
6515
:hints (("Goal" :in-theory (enable rtmintvars-0))))
6518
(defthm an-m-entry-is-never-nil
6522
(m-entries-point-to-good-rtm-var-sets m rtm-mem)
6523
(assoc-equal var m))
6524
(not (endp (rtmintvars-i var m))))
6525
:hints (("Goal" :in-theory (enable rtmintvars-0))))
6528
(defthm rtm-variable-of-other-cell-untouched-equ
6531
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6534
(no-tmp-into-mapping m)
6535
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
6536
(good-translation-gem-rtm gstate rstate m)
6537
(in-range (pcc gstate) (code gstate))
6538
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m)
6540
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
6541
(assoc-equal gvar1 m)
6542
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
6543
(in-range idx1 (rtmintvars-i gvar1 m)))
6544
(equal (get-cell (nth idx1 (rtmintvars-i gvar1 m)) (mem rstate))
6545
(get-cell (nth idx1 (rtmintvars-i gvar1 m)) (mem (execute-n-instructions rstate (* 2 (len *rns*)))))))
6546
:hints (("Goal" :in-theory (current-theory 'ground-zero)
6547
:expand ( (in-range (pcc gstate) (code gstate))
6548
(good-translation-gem-rtm gstate rstate m) )
6550
(:instance a-variable-is-never-tmp (gvar1 gvar1))
6551
(:instance an-m-entry-is-never-nil
6552
(rtm-mem (mem rstate))
6553
(var (par1 (nth (pcc gstate) (code gstate)))))
6554
(:instance equality-trans3-means-touching-just-tmp-res
6555
(v (nth idx1 (rtmintvars-i gvar1 m)))
6556
(l1 (eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*)))
6557
(l2 (eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*)))
6560
(res (car (rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)))
6561
(n (* 2 (len *rns*))))
6562
(:instance lemma1-different-vars-do-not-belong-ref (gvar2 (par1 (nth (pcc gstate) (code gstate)))))))))
6566
(defthm rtm-variables-of-other-cell-untouched-equ
6569
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6570
(no-tmp-into-mapping m)
6571
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
6574
(good-translation-gem-rtm gstate rstate m)
6575
(in-range (pcc gstate) (code gstate))
6576
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m)
6578
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
6579
(assoc-equal gvar1 m)
6580
(true-listp (rtmintvars-i gvar1 m))
6581
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate))))))
6583
(rtmintvars-i gvar1 m) (mem rstate) (mem (execute-n-instructions rstate (* 2 (len *rns*))))))
6584
:hints (("Goal" :in-theory nil
6585
:use ( (:instance rtm-variable-of-other-cell-untouched-equ
6586
(idx1 (idx-different-cell
6587
(rtmintvars-i gvar1 m)
6589
(mem (execute-n-instructions rstate (* 2 (len *rns*)))))) )))
6590
("Goal'" :cases ( (in-range
6592
(rtmintvars-i gvar1 m)
6594
(mem (execute-n-instructions rstate (* 2 (len *rns*)))))
6595
(rtmintvars-i gvar1 m))))
6596
("Subgoal 2" :in-theory '((:rewrite if-bad-index-not-in-range-then-every-equal)))
6597
("Subgoal 1" :in-theory '((:forward-chaining if-bad-index-in-range-then-cells-must-be-different)))))
6601
(defthm properies-of-type-and-existence-of-current-args-equ
6605
(in-range (pcc gstate) (code gstate))
6606
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ))
6608
(equal (var-type (get-cell (par1 (nth (pcc gstate) (code gstate))) (mem gstate))) 'Bool)
6609
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) (mem gstate))
6610
(assoc-equal (par2 (nth (pcc gstate) (code gstate))) (mem gstate))
6611
(assoc-equal (par3 (nth (pcc gstate) (code gstate))) (mem gstate))))
6612
:hints (("Goal" :in-theory (enable get-cell)
6613
:use (:instance in-range-instruction-is-gem-instruction
6615
(code (code gstate))
6616
(mem (mem gstate)))))
6620
(defthm par1-of-current-instruction-is-into-mapping-equ
6623
(vars-inclusion (mem gstate) m)
6625
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6626
(in-range (pcc gstate) (code gstate)))
6627
(assoc-equal (par1 (nth (pcc gstate) (code gstate))) m))
6628
:hints (("Goal" :in-theory (enable get-cell)
6629
:use (properies-of-type-and-existence-of-current-args-equ
6630
(:instance inclusion-trans
6631
(v (par1 (nth (pcc gstate) (code gstate))))
6634
(:instance in-range-instruction-is-gem-instruction
6636
(code (code gstate))
6637
(mem (mem gstate)))))))
6642
(defthm teorema-main-con-pcc-in-range-su-variabile-non-interessata-final-equ
6645
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6646
(no-tmp-into-mapping m)
6647
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
6648
(good-translation-gem-rtm gstate rstate m)
6649
(vars-inclusion (mem gstate) m)
6651
(assoc-equal gvar1 m)
6654
(in-range (pcc gstate) (code gstate))
6655
(in-range (pcc rstate) (code rstate))
6656
(not (equal gvar1 (par1 (nth (pcc gstate) (code gstate)))))
6657
(m-correspondent-values-p m (mem gstate) (mem rstate))
6658
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
6659
(correct-wrt-arity m (mem gstate)))
6660
(equal-values-and-attributes
6661
(get-cell gvar1 (mem (execute-instruction gstate)))
6662
(rtmintvars-i gvar1 m)
6663
(mem (execute-n-instructions rstate (* 2 (len *rns*))))
6666
:in-theory '((:definition good-translation-gem-rtm))
6668
par1-of-current-instruction-is-into-mapping-equ
6669
(:instance correct-wrt-arity-has-rtmintvars-i-tl (mem (mem gstate)))
6670
(:instance m-correspondent-values-implies-equal-values-and-attribus
6671
(memgstate (mem gstate)) (memrstate (mem rstate)))
6672
(:instance in-range (idx (pcc gstate)) (l (code gstate)))
6673
(:instance in-range (idx (pcc rstate)) (l (code rstate)))
6674
rtm-variables-of-other-cell-untouched-equ
6675
teorema-main-con-pcc-in-range-su-variabile-non-interessata
6676
(:instance equal-get-cells-implies-equal-values-and-attributes-still-works
6677
(gemcell (get-cell gvar1 (mem gstate)))
6678
(lcell (rtmintvars-i gvar1 m))
6680
(mem2 (mem (execute-n-instructions rstate (* 2 (len *rns*)))))
6681
(type (type-i gvar1 m)))))))
6687
(vars-inclusion (mem gstate) m)
6689
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6690
(in-range (pcc gstate) (code gstate)))
6692
(in-range (pos-equal-0 (par1 (nth (pcc gstate) (code gstate))) m) m)
6693
(in-range (pos-equal-0 (par2 (nth (pcc gstate) (code gstate))) m) m)
6694
(in-range (pos-equal-0 (par3 (nth (pcc gstate) (code gstate))) m) m)))
6695
:hints (("Goal" :use (properies-of-type-and-existence-of-current-args-equ
6696
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
6697
(v (par1 (nth (pcc gstate) (code gstate)))))
6698
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
6699
(v (par2 (nth (pcc gstate) (code gstate)))))
6700
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
6701
(v (par3 (nth (pcc gstate) (code gstate)))))
6702
(:instance assoc-means-pos-in-range
6703
(el (par1 (nth (pcc gstate) (code gstate))))
6705
(:instance assoc-means-pos-in-range
6706
(el (par2 (nth (pcc gstate) (code gstate))))
6708
(:instance assoc-means-pos-in-range
6709
(el (par3 (nth (pcc gstate) (code gstate))))
6714
(defthm equal-eq-update-norest-afetr-one-instr
6718
(in-range (pcc gstate) (code gstate))
6719
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6720
(good-translation-gem-rtm gstate rstate m)
6721
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
6722
(equal gvar2 (par2 (nth (pcc gstate) (code gstate))))
6723
(equal gvar3 (par3 (nth (pcc gstate) (code gstate)))))
6724
(equal (get-cell gvar1 (mem (execute-instruction gstate)))
6725
(gen-eq-update gvar1 gvar2 gvar3 (mem gstate))))
6726
:hints (("Goal" :in-theory (e/d (put-cell get-cell)
6727
(par1 par2 par3 par4 opcode pcc code nth gem-instruction-list-p
6728
gen-eq-update sum-and-update sub-and-update sub-and-update-norest sum-and-update-norest))))
6731
(DEFTHM mem-cellity-of-current-gem-args-equ
6733
(AND (GEM-STATEP GSTATE)
6734
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6735
(IN-RANGE (PCC GSTATE) (CODE GSTATE)))
6736
(AND (is-mem-cell-p (get-cell (PAR1 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))
6737
(is-mem-cell-p (get-cell (PAR2 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))
6738
(is-mem-cell-p (get-cell (PAR3 (NTH (PCC GSTATE) (CODE GSTATE))) (mem gstate)))))
6742
(:INSTANCE IN-RANGE-INSTRUCTION-IS-GEM-INSTRUCTION
6744
(CODE (CODE GSTATE))
6745
(MEM (MEM GSTATE))))))
6751
VAR-ATTRIBUTES-OF-1-VARIABLE-IS-ONE-ELEMENT-LIST-OF-VAR-ATTRIBUTE
6752
(IMPLIES (AND (TRUE-LISTP VARS)
6753
(EQUAL (LEN VARS) 1))
6754
(EQUAL (VAR-ATTRIBUTES VARS MEM)
6755
(LIST (VAR-ATTRIBUTE (GET-CELL (CAR VARS) MEM)))))
6759
(:THEOREM (IMPLIES (AND (TRUE-LISTP VARS)
6760
(EQUAL (LEN VARS) 1))
6761
(AND (EQUAL (LEN (CDR VARS)) 0)
6762
(TRUE-LISTP (CDR VARS))))))))
6765
(defthm equal-values-and-attributes-in-boolean-case
6767
(equal (type-expected rtmvars) 'Bool)
6769
(equal-values-and-attributes gcell rtmvars rtmmem 'Bool)
6772
(var-value (get-cell (car rtmvars) rtmmem))
6775
(var-attribute gcell)
6776
(var-attribute (get-cell (car rtmvars) rtmmem)))))))
6782
(defthm type-is-for-pars-equ
6786
(vars-inclusion (mem gstate) m)
6788
(correct-wrt-arity m (mem gstate))
6789
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
6790
(equal gvar2 (par2 (nth (pcc gstate) (code gstate))))
6791
(equal gvar3 (par3 (nth (pcc gstate) (code gstate))))
6792
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
6793
(in-range (pcc gstate) (code gstate)))
6794
(equal (type-i gvar1 m) 'bool))
6796
:in-theory nil ;(current-theory 'ground-zero)
6797
:use ( properies-of-type-and-existence-of-current-args-equ
6798
(:instance type-i-is-vartyper (gvar1 gvar1) (mem (mem gstate)))
6799
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
6800
(v (par1 (nth (pcc gstate) (code gstate))))))))
6809
(INTEGERP VAR-VALUE-GCELL2)
6810
(EQUAL (BUILD-VALUES-BY-RNS-EXTENDED-FOR-NIL VAR-VALUE-GCELL2
6812
(LIST (MOD VAR-VALUE-GCELL2 11)
6813
(MOD VAR-VALUE-GCELL2 13)
6814
(MOD VAR-VALUE-GCELL2 15)
6815
(MOD VAR-VALUE-GCELL2 17)
6816
(MOD VAR-VALUE-GCELL2 19))))
6817
:hints (("Goal" :use (
6818
(:instance build-values-by-rns-extended-for-nil
6819
(gem-value VAR-VALUE-GCELL2)
6820
(rns '(11 13 15 17 19)))
6821
(:instance build-values-by-rns-extended-for-nil
6822
(gem-value VAR-VALUE-GCELL2)
6823
(rns '(13 15 17 19)))
6824
(:instance build-values-by-rns-extended-for-nil
6825
(gem-value VAR-VALUE-GCELL2)
6827
(:instance build-values-by-rns-extended-for-nil
6828
(gem-value VAR-VALUE-GCELL2)
6830
(:instance build-values-by-rns-extended-for-nil
6831
(gem-value VAR-VALUE-GCELL2)
6833
(:instance build-values-by-rns-extended-for-nil
6834
(gem-value VAR-VALUE-GCELL2)
6838
(defthm var-values-of-n-list
6840
(var-values (make-n-list gvar n) mem)
6841
(make-n-list (var-value (get-cell gvar mem)) n))
6844
(defthm make-n-list-expansion-5
6847
(list el el el el el))
6848
:hints (("Goal" :use
6849
( (:instance make-n-list (n 5))
6850
(:instance make-n-list (n 4))
6851
(:instance make-n-list (n 3))
6852
(:instance make-n-list (n 2))
6853
(:instance make-n-list (n 1))
6854
(:instance make-n-list (n 0)) ) ))
6861
(EQUAL (VAR-VALUE (GET-CELL RTMINTVARS-I-GVAR3 RTMMEM))
6863
(EQUAL (VAR-VALUES (MAKE-N-LIST RTMINTVARS-I-GVAR3 5)
6866
:hints (("Goal" :use ( (:instance make-n-list-expansion-5 (el (VAR-VALUE (GET-CELL RTMINTVARS-I-GVAR3 RTMMEM))))
6867
(:instance var-values-of-n-list
6868
(gvar RTMINTVARS-I-GVAR3)
6875
(EQUAL (VAR-VALUE (GET-CELL RTMINTVARS-I-GVAR3 RTMMEM))
6877
(EQUAL (VAR-VALUES (MAKE-N-LIST RTMINTVARS-I-GVAR3 5)
6880
:hints (("Goal" :use ( (:instance make-n-list-expansion-5 (el (VAR-VALUE (GET-CELL RTMINTVARS-I-GVAR3 RTMMEM))))
6881
(:instance var-values-of-n-list
6882
(gvar RTMINTVARS-I-GVAR3)
6889
(defthm var-values-of-evmakelist-is-rns-anyway
6892
(is-mem-cell-p gcell2)
6893
(equal (type-expected rtmintvars-i-gvar2) (var-type gcell2))
6894
(equal-values-and-attributes gcell2 rtmintvars-i-gvar2 rtmmem (var-type gcell2)))
6896
(var-values (eventually-make-list rtmintvars-i-gvar2 (len *rns*)) rtmmem)
6897
(build-values-by-rns (var-value gcell2) *rns*)))
6898
:hints (("Goal" :in-theory (enable my-or-2))
6899
("Subgoal 5'''" :use (:instance goal15 (var-value-gcell2 (var-value gcell2))))
6900
; fcd/Satriani v3.7 Moore - used to Subgoal 4.1
6901
("Subgoal 1.1" :use subgoal41)
6902
; fcd/Satriani v3.7 Moore - used to Subgoal 2.1
6903
("Subgoal 3.1" :use subgoal21)))
6907
(defthm ax-on-rns-values
6911
(< gval1 (prod *rns*))
6913
(< gval2 (prod *rns*))
6914
(not (equal gval1 gval2)))
6915
(not (equal (build-values-by-rns gval1 *rns*) (build-values-by-rns gval2 *rns*))))
6916
:hints (("Goal" :use ( fact-bout-rns
6917
(:instance crt-inversion (val gval1) (rns *rns*))
6918
(:instance crt-inversion (val gval2) (rns *rns*))))))
6923
(is-mem-cell-p cell)
6924
(bounded-value cell))
6926
(natp (var-value cell))
6927
(< (var-value cell) (prod *rns*))))
6930
(defthm equal-equality-of-var-values-euqlity-of-evlists
6933
(is-mem-cell-p gcell2)
6934
(is-mem-cell-p gcell3)
6935
(bounded-value gcell2)
6936
(bounded-value gcell3)
6937
(equal (type-expected rtmintvars-i-gvar2) (var-type gcell2))
6938
(equal (type-expected rtmintvars-i-gvar3) (var-type gcell3))
6939
(equal-values-and-attributes gcell2 rtmintvars-i-gvar2 rtmmem (var-type gcell2))
6940
(equal-values-and-attributes gcell3 rtmintvars-i-gvar3 rtmmem (var-type gcell3)))
6944
(var-value gcell3) )
6946
(var-values (eventually-make-list rtmintvars-i-gvar2 (len *rns*)) rtmmem)
6947
(var-values (eventually-make-list rtmintvars-i-gvar3 (len *rns*)) rtmmem))))
6951
( (:instance hlp1 (cell gcell2))
6952
(:instance hlp1 (cell gcell3))
6953
(:instance ax-on-rns-values
6954
(gval1 (var-value gcell2))
6955
(gval2 (var-value gcell3)))
6956
(:instance var-values-of-evmakelist-is-rns-anyway
6958
(rtmintvars-i-gvar2 rtmintvars-i-gvar2))
6959
(:instance var-values-of-evmakelist-is-rns-anyway
6961
(rtmintvars-i-gvar2 rtmintvars-i-gvar3))))))
6963
(in-theory (disable ax-on-rns-values))
6969
(defthm length-of-makelist-n
6974
(equal (len (make-n-list l n)) n)))
6976
(defthm if-type-exepcted-is-ok-eventually-always-has-len-of-rns
6979
(equal (type-expected l) 'Bool)
6980
(equal (type-expected l) 'Int))
6981
(equal (len (eventually-make-list l (len *rns*))) (len *rns*))))
6983
(defthm tmp-never-appears
6986
(no-tmp-into-mapping m)
6987
(assoc-equal gvar1 m))
6988
(not (member-equal-bool 'tmp (eventually-make-list (rtmintvars-i gvar1 m) n))))
6989
:hints (("Goal" :in-theory (enable rtmintvars-0))))
6991
(defthm tmp-never-appears-simple
6994
(no-tmp-into-mapping m)
6995
(assoc-equal gvar1 m))
6996
(not (member-equal-bool 'tmp (rtmintvars-i gvar1 m) )))
6997
:hints (("Goal" :in-theory (enable rtmintvars-0))))
6999
(defthm type-of-a-mem-cell
7001
(is-mem-cell-p cell)
7003
(equal (var-type cell) 'Bool)
7004
(equal (var-type cell) 'Int)))
7005
:hints (("Goal" :in-theory (enable my-or-2)))
7010
(equal (make-n-list l1 1) (list l1))
7011
:hints (("Goal" :use (:instance make-n-list (el l1) (n 1))))
7014
; Added by Matt K. for v3-5. Heuristic changes to linear arithmetic were
7015
; preventing the next lemma, not-member-equal-bool-holds-on-ev, from going
7016
; through. But the original proof involved generalization and three levels of
7017
; induction, so rather than investigate further, we'll just prove the following
7018
; lemma. With it, the proof of not-member-equal-bool-holds-on-ev goes through
7021
(defthm helper-from-matt-k
7022
(implies (not (equal el l1))
7023
(not (member-equal-bool el (make-n-list l1 n))))))
7025
(defthm not-member-equal-bool-holds-on-ev
7030
(not (member-equal-bool el l)))
7031
(not (member-equal-bool el (eventually-make-list l n))))
7032
:hints (("Subgoal *1.1/4''" :use sillllly) ; Modified for v2-6 by Matt K.
7033
("Subgoal *1.1/4.1" :use sillllly))
7040
(equal (len (rtmintvars-i gvar1 m)) 1)
7041
(assoc-equal gvar1 m)
7042
(assoc-equal gvar2 m)
7043
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7044
(not (equal gvar1 gvar2)))
7045
(not (member-equal-bool
7046
(car (rtmintvars-i gvar1 m))
7047
(rtmintvars-i gvar2 m))))
7049
:use ( (:instance lemma1-different-vars-do-not-belong (idx1 0)))))
7056
(equal (len (rtmintvars-i gvar1 m)) 1)
7057
(assoc-equal gvar1 m)
7058
(assoc-equal gvar2 m)
7059
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7060
(not (equal gvar1 gvar2)))
7061
(not (member-equal-bool
7062
(car (rtmintvars-i gvar1 m))
7063
(eventually-make-list (rtmintvars-i gvar2 m) (len *rns*)))))
7066
(:instance not-member-equal-bool-holds-on-ev
7067
(el (car (rtmintvars-i gvar1 m)))
7068
(l (rtmintvars-i gvar2 m))
7073
(defthm eq-and-update-behaviour
7076
(var-value (gen-eq-update c1 c2 c3 mem))
7077
(boolean-to-int (equal
7078
(var-value (get-cell c2 mem))
7079
(var-value (get-cell c3 mem)))))
7081
(var-attribute (gen-eq-update c1 c2 c3 mem))
7082
(var-attribute (get-cell c1 mem))))
7083
:hints (("Goal" :in-theory (enable var-value var-attribute))))
7086
(defthm var-attribute-of-a-var-is-same-after-n-steps
7089
(equal (var-attribute (get-cell anyvar (mem st)))
7090
(var-attribute (get-cell anyvar (mem (execute-n-instructions st n))))))
7092
:induct (execute-n-instructions st n)
7093
:in-theory (disable rtm-statep execute-instruction))
7097
(:instance execute-instruction-is-type-and-attribute-invariant-on-any-var (cell anyvar))
7098
executing-rtm-instruction-retrieves-a-rtm-state-from-rtm-state))))
7101
(defthm bool-to-int-strip
7103
(equal (boolean-to-int (equal a b)) (boolean-to-int (equal-values c d)))
7104
(equal (equal a b) (equal c d))))
7107
(defthm equal-equality-of-var-values-euqlity-of-evlists-2
7110
(is-mem-cell-p gcell2)
7111
(is-mem-cell-p gcell3)
7112
(bounded-value gcell2)
7113
(bounded-value gcell3)
7114
(equal (type-expected rtmintvars-i-gvar2) (var-type gcell2))
7115
(equal (type-expected rtmintvars-i-gvar3) (var-type gcell3))
7116
(equal-values-and-attributes gcell2 rtmintvars-i-gvar2 rtmmem (var-type gcell2))
7117
(equal-values-and-attributes gcell3 rtmintvars-i-gvar3 rtmmem (var-type gcell3)))
7122
(var-value gcell3) ))
7125
(var-values (eventually-make-list rtmintvars-i-gvar2 (len *rns*)) rtmmem)
7126
(var-values (eventually-make-list rtmintvars-i-gvar3 (len *rns*)) rtmmem)))))
7130
((:instance bool-to-int-strip
7131
(a (var-value gcell2))
7132
(b (var-value gcell3))
7133
(c (var-values (eventually-make-list rtmintvars-i-gvar2 (len *rns*)) rtmmem))
7134
(d (var-values (eventually-make-list rtmintvars-i-gvar3 (len *rns*)) rtmmem)))
7135
equal-equality-of-var-values-euqlity-of-evlists))))
7139
(defthm sil-support-2
7145
(equal (type-expected l) 'Bool)
7146
(equal (type-expected l) 'Int)))
7147
(not (endp (eventually-make-list l n))))
7148
:hints (("Subgoal *1.1/3'" :use sillllly))
7151
(defthm sil-support-3
7154
(equal (type-expected l) 'Bool)
7155
(equal (type-expected l) 'Int))
7156
(not (endp (eventually-make-list l (len *rns*)))))
7157
:hints (("Goal" :use (:instance sil-support-2 (n (len *rns*))))))
7160
(defthm not-in-car-if-no-memb
7164
(not (member-equal-bool 'tmp l)))
7165
(not (equal 'tmp (car l)))))
7167
(defthm sil-support-1
7169
(equal (type-i gvar1 m) 'bool)
7170
(equal (LEN (RTMINTVARS-I gvar1 m)) 1)))
7173
(defthm bounded-are-bounded
7176
(bounded-amem-p mem)
7177
(assoc-equal cell mem))
7178
(bounded-value (get-cell cell mem)))
7179
:hints (("Goal" :in-theory (enable get-cell)))
7185
(defthm m-correspondence-kept-on-same-gvar-equ
7188
(NOT (ENDP (EVENTUALLY-MAKE-LIST
7189
(RTMINTVARS-I (PAR2 (NTH (PCC GSTATE) (CODE GSTATE)))
7191
(LEN '(11 13 15 17 19)))))
7193
(CAR (RTMINTVARS-I (PAR1 (NTH (PCC GSTATE) (CODE GSTATE)))
7195
(EQUAL (LEN (RTMINTVARS-I (PAR1 (NTH (PCC GSTATE) (CODE GSTATE))) M)) 1)
7196
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
7197
(no-tmp-into-mapping m)
7198
(good-translation-gem-rtm gstate rstate m)
7199
(vars-inclusion (mem gstate) m)
7201
(assoc-equal gvar1 m)
7204
(in-range (pcc gstate) (code gstate))
7205
(in-range (pcc rstate) (code rstate))
7206
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
7207
(m-correspondent-values-p m (mem gstate) (mem rstate))
7208
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7209
(correct-wrt-arity m (mem gstate)))
7210
(equal-values-and-attributes
7211
(get-cell gvar1 (mem (execute-instruction gstate)))
7212
(rtmintvars-i gvar1 m)
7213
(mem (execute-n-instructions rstate (* 2 (len *rns*))))
7215
:hints (("Goal" :in-theory nil
7217
(:instance gem-statep (x gstate))
7218
(:instance bounded-are-bounded (cell (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7219
(:instance bounded-are-bounded (cell (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7220
(:instance eq-and-update-behaviour
7222
(c2 (par2 (nth (pcc gstate) (code gstate))))
7223
(c3 (par3 (nth (pcc gstate) (code gstate))))
7225
(:instance var-attribute-of-a-var-is-same-after-n-steps
7227
(anyvar (car (rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)))
7228
(n (* 2 (len *rns*))))
7229
(:instance in-range (idx (pcc gstate)) (l (code gstate)))
7230
(:instance not-memb-2
7231
(gvar1 (par1 (nth (pcc gstate) (code gstate))))
7232
(gvar2 (par2 (nth (pcc gstate) (code gstate)))))
7233
(:instance not-memb-2
7234
(gvar1 (par1 (nth (pcc gstate) (code gstate))))
7235
(gvar2 (par3 (nth (pcc gstate) (code gstate)))))
7236
(:instance type-of-a-mem-cell (cell (get-cell (par2 (nth (pcc gstate) (code gstate))) (mem gstate))))
7237
(:instance type-of-a-mem-cell (cell (get-cell (par3 (nth (pcc gstate) (code gstate))) (mem gstate))))
7238
properies-of-type-and-existence-of-current-args-equ
7239
mem-cellity-of-current-gem-args-equ
7240
good-translation-gem-rtm
7241
(:instance tmp-never-appears (n (len *rns*)) (gvar1 (par2 (nth (pcc gstate) (code gstate)))))
7242
(:instance tmp-never-appears (n (len *rns*)) (gvar1 (par3 (nth (pcc gstate) (code gstate)))))
7243
(:instance if-type-exepcted-is-ok-eventually-always-has-len-of-rns
7244
(l (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m)))
7245
(:instance if-type-exepcted-is-ok-eventually-always-has-len-of-rns
7246
(l (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m)))
7247
(:instance type-i-is-vartyper (gvar1 gvar1) (mem (mem gstate)))
7248
(:instance type-i-is-vartyper (gvar1 (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7249
(:instance type-i-is-vartyper (gvar1 (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7250
(:instance type-i-is-type-expected (gvar gvar1) (mem (mem gstate)))
7251
(:instance type-i-is-type-expected (gvar (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7252
(:instance type-i-is-type-expected (gvar (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7253
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7254
(v (par1 (nth (pcc gstate) (code gstate)))))
7255
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7256
(v (par2 (nth (pcc gstate) (code gstate)))))
7257
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7258
(v (par3 (nth (pcc gstate) (code gstate)))))
7260
equal-eq-update-norest-afetr-one-instr
7261
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
7262
(gvar3 (par3 (nth (pcc gstate) (code gstate))))
7264
(:instance type-is-for-pars-equ
7265
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
7266
(gvar3 (par3 (nth (pcc gstate) (code gstate)))))
7267
(:instance equal-values-and-attributes-in-boolean-case
7268
(rtmvars (rtmintvars-i gvar1 m))
7269
(gcell (get-cell gvar1 (mem gstate)))
7270
(rtmmem (mem rstate)))
7271
(:instance equal-values-and-attributes-in-boolean-case
7272
(rtmvars (rtmintvars-i gvar1 m))
7273
(gcell (get-cell gvar1 (mem (execute-instruction gstate))))
7274
(rtmmem (mem (execute-n-instructions rstate (* 2 (len *rns*))))))
7275
(:instance m-correspondent-values-implies-equal-values-and-attribus
7276
(memgstate (mem gstate)) (memrstate (mem rstate))
7277
(gvar1 (par1 (nth (pcc gstate) (code gstate)))))
7278
(:instance m-correspondent-values-implies-equal-values-and-attribus
7279
(memgstate (mem gstate)) (memrstate (mem rstate))
7280
(gvar1 (par2 (nth (pcc gstate) (code gstate)))))
7281
(:instance m-correspondent-values-implies-equal-values-and-attribus
7282
(memgstate (mem gstate)) (memrstate (mem rstate))
7283
(gvar1 (par3 (nth (pcc gstate) (code gstate)))))
7284
(:instance value-of-result-after-executing-2n-+2instr-finale
7286
(res (car (rtmintvars-i (par1 (nth (pcc gstate) (code gstate))) m)))
7287
(listvars1 (eventually-make-list (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m) (len *rns*)))
7288
(listvars2 (eventually-make-list (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m) (len *rns*)))
7290
(:instance equal-equality-of-var-values-euqlity-of-evlists-2
7291
(gcell2 (get-cell (par2 (nth (pcc gstate) (code gstate))) (mem gstate)))
7292
(gcell3 (get-cell (par3 (nth (pcc gstate) (code gstate))) (mem gstate)))
7293
(rtmintvars-i-gvar2 (rtmintvars-i (par2 (nth (pcc gstate) (code gstate))) m))
7294
(rtmintvars-i-gvar3 (rtmintvars-i (par3 (nth (pcc gstate) (code gstate))) m))
7295
(rtmmem (mem rstate)))))))
7298
(defthm m-correspondence-kept-on-same-gvar-equ-supp
7301
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
7302
(no-tmp-into-mapping m)
7303
(equal gvar1 (par1 (nth (pcc gstate) (code gstate))))
7304
(assoc-equal gvar1 m)
7305
(vars-inclusion (mem gstate) m)
7309
(in-range (pcc gstate) (code gstate))
7310
(in-range (pcc rstate) (code rstate))
7311
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7312
(correct-wrt-arity m (mem gstate)))
7314
(NOT (ENDP (EVENTUALLY-MAKE-LIST
7315
(RTMINTVARS-I (PAR2 (NTH (PCC GSTATE) (CODE GSTATE)))
7317
(LEN '(11 13 15 17 19)))))
7319
(CAR (RTMINTVARS-I (PAR1 (NTH (PCC GSTATE) (CODE GSTATE)))
7321
(EQUAL (LEN (RTMINTVARS-I (PAR1 (NTH (PCC GSTATE) (CODE GSTATE))) M)) 1)))
7322
:hints (("Goal" :in-theory nil
7324
(:instance sil-support-3 (l (RTMINTVARS-I (PAR2 (NTH (PCC GSTATE) (CODE GSTATE))) M) ))
7325
(:instance not-in-car-if-no-memb (l (RTMINTVARS-I (PAR1 (NTH (PCC GSTATE) (CODE GSTATE))) m)))
7326
(:instance sil-support-1 (gvar1 (PAR1 (NTH (PCC GSTATE) (CODE GSTATE)))))
7327
(:instance in-range (idx (pcc gstate)) (l (code gstate)))
7328
(:instance type-of-a-mem-cell (cell (get-cell (par2 (nth (pcc gstate) (code gstate))) (mem gstate))))
7329
(:instance type-of-a-mem-cell (cell (get-cell (par3 (nth (pcc gstate) (code gstate))) (mem gstate))))
7330
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7331
(v (par1 (nth (pcc gstate) (code gstate)))))
7332
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7333
(v (par2 (nth (pcc gstate) (code gstate)))))
7334
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7335
(v (par3 (nth (pcc gstate) (code gstate)))))
7336
properies-of-type-and-existence-of-current-args-equ
7337
mem-cellity-of-current-gem-args-equ
7338
(:instance tmp-never-appears-simple (gvar1 (par1 (nth (pcc gstate) (code gstate)))))
7339
(:instance type-i-is-vartyper (gvar1 gvar1) (mem (mem gstate)))
7340
(:instance type-i-is-vartyper (gvar1 (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7341
(:instance type-i-is-vartyper (gvar1 (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7342
(:instance type-i-is-type-expected (gvar gvar1) (mem (mem gstate)))
7343
(:instance type-i-is-type-expected (gvar (par2 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7344
(:instance type-i-is-type-expected (gvar (par3 (nth (pcc gstate) (code gstate)))) (mem (mem gstate)))
7345
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7346
(v (par1 (nth (pcc gstate) (code gstate)))))
7347
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7348
(v (par2 (nth (pcc gstate) (code gstate)))))
7349
(:instance inclusion-trans (m1 (mem gstate)) (m2 m)
7350
(v (par3 (nth (pcc gstate) (code gstate)))))
7351
(:instance type-is-for-pars-equ
7352
(gvar2 (par2 (nth (pcc gstate) (code gstate))))
7353
(gvar3 (par3 (nth (pcc gstate) (code gstate)))))))))
7357
(defthm equal-values-correspondence-kept-by-any-execution-equ
7360
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
7361
(no-tmp-into-mapping m)
7362
(good-translation-gem-rtm gstate rstate m)
7363
(vars-inclusion (mem gstate) m)
7365
(assoc-equal gvar1 m)
7368
(in-range (pcc gstate) (code gstate))
7369
(in-range (pcc rstate) (code rstate))
7370
(m-correspondent-values-p m (mem gstate) (mem rstate))
7371
(M-ENTRIES-POINT-TO-GOOD-RTM-VAR-SETS M (MEM RSTATE))
7372
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7373
(correct-wrt-arity m (mem gstate)))
7374
(equal-values-and-attributes
7375
(get-cell gvar1 (mem (execute-instruction gstate)))
7376
(rtmintvars-i gvar1 m)
7377
(mem (execute-n-instructions rstate (* 2 (len *rns*))))
7379
:hints (("Goal" :in-theory nil
7380
:use (m-correspondence-kept-on-same-gvar-equ
7381
m-correspondence-kept-on-same-gvar-equ-supp
7382
teorema-main-con-pcc-in-range-su-variabile-non-interessata-final-equ))))
7385
(defthm rtmintvars-i-iscdrnth
7390
(no-duplicates-p (retrieve-gemvars m)))
7391
(equal (rtmintvars-i (car (nth idx m)) m)
7396
(:instance no-duplicates-has-pos-equal-right-in-that-place (l m))
7397
(:instance rtmintvars-i-is-cdr-of-nth-entry (gvar (car (nth idx m))))))))
7399
(defthm type-i-is-typeidx
7404
(no-duplicates-p (retrieve-gemvars m)))
7405
(equal (type-i (car (nth idx m)) m)
7406
(type-i-idx m idx))))
7410
(defthm equal-values-correspondence-kept-by-any-execution-idxed-equ
7413
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
7414
(no-tmp-into-mapping m)
7415
(good-translation-gem-rtm gstate rstate m)
7416
(vars-inclusion (mem gstate) m)
7421
(in-range (pcc gstate) (code gstate))
7422
(in-range (pcc rstate) (code rstate))
7423
(m-correspondent-values-p m (mem gstate) (mem rstate))
7424
(M-ENTRIES-POINT-TO-GOOD-RTM-VAR-SETS M (MEM RSTATE))
7425
(no-duplicates-p (retrieve-gemvars m))
7426
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7427
(correct-wrt-arity m (mem gstate)))
7428
(equal-values-and-attributes
7429
(get-cell (car (nth idx m)) (mem (execute-instruction gstate)))
7431
(mem (execute-n-instructions rstate (* 2 (len *rns*))))
7432
(type-i-idx m idx)))
7433
:hints (("Subgoal 2" :in-theory nil)
7434
("Goal" :in-theory (union-theories (current-theory 'ground-zero)
7435
'((:definition in-range)))
7443
(assoc-equal (car (nth idx m)) m))))
7445
rtmintvars-i-iscdrnth
7447
(:instance equal-values-correspondence-kept-by-any-execution-equ (gvar1 (car (nth idx m)))))))
7453
(defthm m-correspondence-kept-by-any-execution-idxed-equ
7456
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
7457
(no-tmp-into-mapping m)
7458
(good-translation-gem-rtm gstate rstate m)
7459
(vars-inclusion (mem gstate) m)
7463
(in-range (pcc gstate) (code gstate))
7464
(in-range (pcc rstate) (code rstate))
7465
(m-correspondent-values-p m (mem gstate) (mem rstate))
7466
(M-ENTRIES-POINT-TO-GOOD-RTM-VAR-SETS M (MEM RSTATE))
7467
(no-duplicates-p (retrieve-gemvars m))
7468
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7469
(correct-wrt-arity m (mem gstate)))
7470
(m-correspondent-values-p
7472
(mem (execute-instruction gstate))
7473
(mem (execute-n-instructions rstate (* 2 (len *rns*))))))
7474
:hints (("Goal" :use (:instance equal-values-correspondence-kept-by-any-execution-idxed-equ
7475
(idx (bad-idx-eqv-va m
7476
(mem (execute-instruction gstate))
7477
(mem (execute-n-instructions rstate (* 2 (len *rns*))))))))
7478
("Goal'" :cases ( (in-range (bad-idx-eqv-va m (mem (execute-instruction gstate))
7479
(mem (execute-n-instructions rstate (* 2 (len *rns*))))) m)))
7480
("Subgoal 2" :in-theory '((:forward-chaining alistp-forward-to-true-listp)
7481
(:rewrite if-bad-index-not-in-range-then-m-corr)))
7482
("Subgoal 1" :in-theory '((:rewrite if-bad-index-in-range-thne-must-be-different-vs)))))
7486
(defthm m-correspondence-and-other-conditions-kept-by-any-execution-idxed-equ
7489
(equal (opcode (nth (pcc gstate) (code gstate))) 'gem-equ)
7490
(no-tmp-into-mapping m)
7491
(good-translation-gem-rtm gstate rstate m)
7492
(vars-inclusion (mem gstate) m)
7493
(vars-inclusion m (mem gstate))
7497
(in-range (pcc gstate) (code gstate))
7498
(in-range (pcc rstate) (code rstate))
7499
(m-correspondent-values-p m (mem gstate) (mem rstate))
7500
(M-ENTRIES-POINT-TO-GOOD-RTM-VAR-SETS M (MEM RSTATE))
7501
(no-duplicates-p (retrieve-gemvars m))
7502
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7503
(correct-wrt-arity m (mem gstate)))
7505
(good-translation-gem-rtm (execute-instruction gstate) (execute-n-instructions rstate (* 2 (len *rns*))) m)
7506
(rtm-statep (execute-n-instructions rstate (* 2 (len *rns*))))
7507
(m-entries-point-to-good-rtm-var-sets m (mem (execute-n-instructions rstate (* 2 (len *rns*)))))
7508
(gem-statep (execute-instruction gstate))
7509
(correct-wrt-arity m (mem (execute-instruction gstate)))
7510
(vars-inclusion (mem (execute-instruction gstate)) m)
7511
(vars-inclusion m (mem (execute-instruction gstate)))
7512
(m-correspondent-values-p
7514
(mem (execute-instruction gstate))
7515
(mem (execute-n-instructions rstate (* 2 (len *rns*)))))))
7519
rtm-statep gem-statep
7521
execute-instruction rtmintvars-i par1 par2 par3 nth len member-equal)
7523
(m-correspondence-kept-by-any-execution-idxed-equ
7524
good-translation-gem-rtm
7525
(:instance execute-n-instructions-keeps-rtm-state-and-points-to-good
7526
(st rstate) (n (* 2 (len *rns*))))
7527
(:instance executing-gem-instruction-retrieves-a-gem-state-from-gem-state (st gstate))
7528
(:instance executing-gem-instruction-preserves-correctness-wrt-arity (st gstate))
7529
(:instance executing-gem-instruction-keeps-vars-inclusion-right (st gstate))
7530
(:instance executing-gem-instruction-keeps-vars-inclusion-left (st gstate))))))
7536
;;; Modified 12/24/2014 to avoid the nu-rewriter, which is being eliminated.
7537
; (set-nu-rewriter-mode nil) ; to avoid skip-proofs below
7538
(defthm after-n-instructions-out-of-range-rtmstate-untouched
7542
(>= (pcc rstate) (len (code rstate))))
7543
(equal (execute-n-instructions rstate n) rstate))
7544
:hints (("Goal" :in-theory (enable execute-not-in-range-instruction-retrieves-same-state)))))
7548
(defun correspondent-steps-to-current-gem-instruction (gstate)
7549
(case (opcode (nth (pcc gstate) (code gstate)))
7550
(gem-add (len *rns*))
7551
(gem-sub (len *rns*))
7552
(gem-equ (* 2 (len *rns*)))
7557
(defun correspondent-steps (n gstate)
7560
(+ (correspondent-steps-to-current-gem-instruction gstate)
7561
(correspondent-steps (1- n) (execute-instruction gstate)))))
7567
(defthm m-correspondence-and-other-conditions-kept-by-out-of-range-execution-2
7571
(no-duplicates-p (retrieve-gemvars m))
7572
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7573
(good-translation-gem-rtm gstate rstate m)
7574
(correct-wrt-arity m (mem gstate))
7577
(vars-inclusion (mem gstate) m)
7578
(vars-inclusion m (mem gstate))
7579
(not (in-range (pcc gstate) (code gstate)))
7581
(>= (pcc rstate) (len (code rstate)))
7582
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
7583
(m-correspondent-values-p m (mem gstate) (mem rstate)))
7585
(good-translation-gem-rtm
7586
(execute-instruction gstate)
7587
(execute-n-instructions rstate
7588
(correspondent-steps-to-current-gem-instruction gstate)) m)
7589
(rtm-statep (execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate)))
7590
(m-entries-point-to-good-rtm-var-sets
7592
(mem (execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate))))
7593
(gem-statep (execute-instruction gstate))
7594
(correct-wrt-arity m (mem (execute-instruction gstate)))
7595
(vars-inclusion (mem (execute-instruction gstate)) m)
7596
(vars-inclusion m (mem (execute-instruction gstate)))
7597
(m-correspondent-values-p
7599
(mem (execute-instruction gstate))
7600
(mem (execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate))))))
7602
:in-theory '((in-range))
7605
(:instance after-n-instructions-out-of-range-rtmstate-untouched
7606
(n (correspondent-steps-to-current-gem-instruction gstate)))
7607
(:instance execute-not-in-range-instruction-retrieves-same-state (st gstate))))))
7613
(defthm m-correspondence-and-other-conditions-kept-execution-2
7617
(no-tmp-into-mapping m)
7618
(no-duplicates-p (retrieve-gemvars m))
7619
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7620
(good-translation-gem-rtm gstate rstate m)
7621
(correct-wrt-arity m (mem gstate))
7624
(vars-inclusion (mem gstate) m)
7625
(vars-inclusion m (mem gstate))
7627
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
7628
(m-correspondent-values-p m (mem gstate) (mem rstate)))
7630
(>= (pcc (execute-instruction gstate)) 0)
7631
(good-translation-gem-rtm
7632
(execute-instruction gstate)
7633
(execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate)) m)
7634
(rtm-statep (execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate)))
7635
(m-entries-point-to-good-rtm-var-sets
7637
(mem (execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate))))
7638
(gem-statep (execute-instruction gstate))
7639
(correct-wrt-arity m (mem (execute-instruction gstate)))
7640
(vars-inclusion (mem (execute-instruction gstate)) m)
7641
(vars-inclusion m (mem (execute-instruction gstate)))
7642
(m-correspondent-values-p
7644
(mem (execute-instruction gstate))
7645
(mem (execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate))))))
7646
:hints (("Goal" :in-theory '((:definition in-range))
7647
:use ((:instance instruction-incrementing-pvv (st gstate))
7648
correspondent-steps-to-current-gem-instruction
7649
good-translation-gem-rtm
7650
m-correspondence-and-other-conditions-kept-by-out-of-range-execution-2
7651
m-correspondence-and-other-conditions-kept-by-any-execution-add
7652
m-correspondence-and-other-conditions-kept-by-any-execution-sub
7653
m-correspondence-and-other-conditions-kept-by-any-execution-idxed-equ))))
7668
(defun parallel-exec (gstate rstate n)
7670
(list gstate rstate)
7672
(execute-instruction gstate)
7673
(execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate))
7687
(defthm m-correspondence-and-other-conditions-kept-execution-on-n
7693
(no-duplicates-p (retrieve-gemvars m))
7694
(no-duplicates-p (append-lists (retrieve-rtmvars m)))
7695
(no-tmp-into-mapping m)
7696
(good-translation-gem-rtm gstate rstate m)
7697
(correct-wrt-arity m (mem gstate))
7700
(vars-inclusion (mem gstate) m)
7701
(vars-inclusion m (mem gstate))
7703
(m-entries-point-to-good-rtm-var-sets m (mem rstate))
7704
(m-correspondent-values-p m (mem gstate) (mem rstate)))
7706
(>= (pcc (execute-n-instructions gstate n)) 0)
7707
(good-translation-gem-rtm
7708
(execute-n-instructions gstate n)
7709
(execute-n-instructions rstate (correspondent-steps n gstate)) m)
7710
(rtm-statep (execute-n-instructions rstate (correspondent-steps n gstate)))
7711
(m-entries-point-to-good-rtm-var-sets
7713
(mem (execute-n-instructions rstate (correspondent-steps n gstate))))
7714
(gem-statep (execute-n-instructions gstate n))
7715
(correct-wrt-arity m (mem (execute-n-instructions gstate n)))
7716
(vars-inclusion (mem (execute-n-instructions gstate n)) m)
7717
(vars-inclusion m (mem (execute-n-instructions gstate n)))
7718
(m-correspondent-values-p
7720
(mem (execute-n-instructions gstate n))
7721
(mem (execute-n-instructions rstate (correspondent-steps n gstate))))))
7722
:hints (("Goal" :in-theory
7723
;(current-theory 'ground-zero)
7724
(disable executing-gem-instruction-preserves-correctness-wrt-arity
7725
execute-instruction-is-type-and-attribute-invariant-on-any-var
7726
;executing-gem-instruction-is-type-attribute-invariant
7727
executing-gem-instruction-keeps-vars-inclusion-left
7728
executing-gem-instruction-keeps-vars-inclusion-right
7729
execute-n-instructions-keeps-rtm-state-and-points-to-good
7730
correspondent-steps-to-current-gem-instruction
7731
execute-n-instructions-tantamount-to-add-list-e
7732
m-correspondence-and-other-conditions-kept-by-any-execution-add
7733
m-correspondence-and-other-conditions-kept-by-any-execution-sub
7734
m-correspondence-and-other-conditions-kept-by-any-execution-idxed-equ
7735
m-correspondence-and-other-conditions-kept-by-out-of-range-execution-2
7736
executing-gem-instruction-retrieves-a-gem-state-from-gem-state
7737
executing-rtm-instruction-retrieves-a-rtm-state-from-rtm-state
7738
instruction-incrementing-pvv
7739
good-translation-gem-rtm
7740
all-rtm-adds-for-n-steps
7741
null-opcode-implies-execution-does-not-touch-state
7743
mem pcc code opcode retrieve-rtmvars gem-statep rtm-statep execute-instruction)
7744
:induct (parallel-exec gstate rstate n))
7745
("Subgoal *1/2" :use
7747
(:instance execute-n-instruction-decomposition
7748
(n1 (correspondent-steps (1- n) gstate))
7749
(n2 (correspondent-steps-to-current-gem-instruction gstate))
7751
(:instance m-correspondence-and-other-conditions-kept-execution-2
7752
(gstate (execute-instruction gstate))
7753
(rstate (execute-n-instructions rstate (correspondent-steps-to-current-gem-instruction gstate))))))))
7758
(defthm simple-fact-about-initial-gemstate
7760
(gem-program-p gemprog)
7762
(>= (pcc (initial-state gemprog)) 0)
7763
(gem-statep (initial-state gemprog)))))
7765
(defthm simple-fact-about-initial-rtmstate
7767
(rtm-program-p rtmprog)
7769
(>= (pcc (initial-state rtmprog)) 0)
7770
(rtm-statep (initial-state rtmprog)))))
7773
(defun good-mapping (m)
7776
(no-tmp-into-mapping m)
7777
(no-duplicates-p (retrieve-gemvars m))
7778
(no-duplicates-p (append-lists (retrieve-rtmvars m)))))
7780
(defun good-mapping-wrt-memories (m mem-gstate mem-rstate)
7782
(correct-wrt-arity m mem-gstate)
7783
(vars-inclusion mem-gstate m)
7784
(vars-inclusion m mem-gstate)
7785
(m-entries-point-to-good-rtm-var-sets m mem-rstate)
7786
(m-correspondent-values-p m mem-gstate mem-rstate)))
7791
(defun correct-translation (gemprog rtmprog m)
7792
(good-translation-gem-rtm (initial-state gemprog) (initial-state rtmprog) m))
7795
(defthm execution-of-correctly-translated-gem-and-rtm-yields-same-output
7797
((gstate (initial-state gemprog))
7798
(rstate (initial-state rtmprog))
7799
(n (len (code gstate))))
7802
(gem-program-p gemprog)
7803
(rtm-program-p rtmprog)
7805
(good-mapping-wrt-memories m (mem gstate) (mem rstate))
7806
(correct-translation gemprog rtmprog m))
7808
(decode m (projectio (mem (execute-n-instructions rstate (correspondent-steps n gstate))) attr))
7809
(projectio (mem (execute-n-instructions gstate n)) attr))))
7811
:in-theory (union-theories (current-theory 'ground-zero)
7812
'((:rewrite equalities-on-io)
7813
(:definition correct-translation)
7814
(:definition good-mapping-wrt-memories)
7815
(:definition gem-statep)
7816
(:definition rtm-statep)
7817
(:definition good-mapping)))
7821
simple-fact-about-initial-rtmstate
7822
simple-fact-about-initial-gemstate
7823
(:instance m-correspondence-and-other-conditions-kept-execution-on-n
7824
(gstate (initial-state gemprog))
7825
(rstate (initial-state rtmprog))
7826
(n (len (code gstate))))))))
added
removed
books/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Correctness-OneCycle.lisp
