← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/arithmetic-3/bind-free/normalize.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/arithmetic-3/bind-free/normalize.lisp
383
383
                    (+ (bubble-down x match) y))))
384
384
 
385
385
(theory-invariant 
386
 
 (or (not (member-equal '(:rewrite normalize-addends)
387
 
                        theory))
388
 
     (and (member-equal '(:rewrite bubble-down-+-bubble-down)
389
 
                        theory)
390
 
          (member-equal '(:rewrite bubble-down-+-match-1)
391
 
                        theory)
392
 
          (member-equal '(:rewrite bubble-down-+-match-2)
393
 
                        theory)
394
 
          (not (member-equal '(:rewrite bubble-down)
395
 
                         theory))
396
 
          (not (member-equal '(:executable-counterpart bubble-down)
397
 
                             theory))))
 
386
 (or (not (active-runep '(:rewrite normalize-addends)))
 
387
     (and (active-runep '(:rewrite bubble-down-+-bubble-down))
 
388
          (active-runep '(:rewrite bubble-down-+-match-1))
 
389
          (active-runep '(:rewrite bubble-down-+-match-2))
 
390
          (not (active-runep '(:rewrite bubble-down)))
 
391
          (not (active-runep '(:executable-counterpart bubble-down)))))
398
392
 :error nil)
399
393
 
400
394
(local
428
422
                    (* (bubble-down x match) y))))
429
423
 
430
424
(theory-invariant 
431
 
 (or (not (member-equal '(:rewrite normalize-factors-gather-exponents)
432
 
                        theory))
433
 
     (and (member-equal '(:rewrite bubble-down-*-bubble-down)
434
 
                        theory)
435
 
          (member-equal '(:rewrite bubble-down-*-match-1)
436
 
                        theory)
437
 
          (member-equal '(:rewrite bubble-down-*-match-2)
438
 
                        theory)
439
 
          (not (member-equal '(:rewrite bubble-down)
440
 
                         theory))
441
 
          (not (member-equal '(:executable-counterpart bubble-down)
442
 
                             theory))))
 
425
 (or (not (active-runep '(:rewrite normalize-factors-gather-exponents)))
 
426
     (and (active-runep '(:rewrite bubble-down-*-bubble-down))
 
427
          (active-runep '(:rewrite bubble-down-*-match-1))
 
428
          (active-runep '(:rewrite bubble-down-*-match-2))
 
429
          (not (active-runep '(:rewrite bubble-down)))
 
430
          (not (active-runep '(:executable-counterpart bubble-down)))))
443
431
 :error nil)
444
432
 
445
433
(local
473
461
                    (* (bubble-down x match) y))))
474
462
 
475
463
(theory-invariant 
476
 
 (or (not (member-equal '(:rewrite normalize-scatter-exponents)
477
 
                        theory))
478
 
     (and (member-equal '(:rewrite bubble-down-*-bubble-down)
479
 
                        theory)
480
 
          (member-equal '(:rewrite bubble-down-*-match-1)
481
 
                        theory)
482
 
          (member-equal '(:rewrite bubble-down-*-match-2)
483
 
                        theory)
484
 
          (not (member-equal '(:rewrite bubble-down)
485
 
                         theory))
486
 
          (not (member-equal '(:executable-counterpart bubble-down)
487
 
                             theory))))
 
464
 (or (not (active-runep '(:rewrite normalize-scatter-exponents)))
 
465
     (and (active-runep '(:rewrite bubble-down-*-bubble-down))
 
466
          (active-runep '(:rewrite bubble-down-*-match-1))
 
467
          (active-runep '(:rewrite bubble-down-*-match-2))
 
468
          (not (active-runep '(:rewrite bubble-down)))
 
469
          (not (active-runep '(:executable-counterpart bubble-down)))))
488
470
 :error nil)
489
471
 
490
472
(local
493
475
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
494
476
 
495
477
(theory-invariant 
496
 
 (not (and (member-equal '(:rewrite normalize-factors-gather-exponents)
497
 
                         theory)
498
 
           (member-equal '(:rewrite normalize-factors-scatter-exponents)
499
 
                         theory)))
 
478
 (not (and (active-runep '(:rewrite normalize-factors-gather-exponents))
 
479
           (active-runep '(:rewrite normalize-factors-scatter-exponents))))
500
480
 :error nil)
501
481
 
502
482
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;