← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/ivy/ivy-v2/ivy-sources/examples/group-x2

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/ivy/ivy-v2/ivy-sources/examples/group-x2
 
1
;; IVY operation: PROVE
 
2
;;
 
3
;; xx=e groups are commutative.
 
4
 
 
5
(imp (and (all x (= (f (e) x) x))
 
6
          (all x (= (f (g x) x) (e)))
 
7
          (all x (all y (all z (= (f (f x y) z) (f x (f y z))))))
 
8
          (all x (= (f x x) (e)))
 
9
          (all x (= x x)))
 
10
 
 
11
     (all x (all y (= (f x y) (f y x)))))