Permalink
Browse files

changed plus to sum in arithmetic theories

  • Loading branch information...
michael.gruninger
michael.gruninger committed Jan 29, 2015
1 parent f67e2ac commit 609e4b952dbbd2372c7e7f08488395d7e0dcd4c9
@@ -13,15 +13,15 @@
(= y (S x)))))
(forall (x)
(= x (plus x zero)))
(= x (sum x zero)))
(forall (x y)
(= (plus x (S y)) (S (plus x y))))
(= (sum x (S y)) (S (sum x y))))
(forall (x)
(= zero (times x zero)))
(forall (x y)
(= (times x (S y)) (plus (times x y) x)))
(= (times x (S y)) (sum (times x y) x)))
)
@@ -3,19 +3,19 @@
(cl-imports http://colore.oor.net/sum_arithmetic/sum_def.clif)
(forall (x y)
(= (plus x y) (plus y x)))
(= (sum x y) (sum y x)))
(forall (x y z)
(= (plus (plus x y) z) (plus x (plus y z))))
(= (sum (sum x y) z) (sum x (sum y z))))
(forall (x)
(= x (plus x zero)))
(= x (sum x zero)))
(forall (x)
(not (= (x (plus x one)))))
(not (= (x (sum x one)))))
(forall (x y)
(if (= one (plus x y))
(if (= one (sum x y))
(or (= x zero)
(= x one))))
@@ -1,23 +1,23 @@
(cl-text http://colore.oor.net/sum_arithmetic/presburger.clif
(forall (x)
(not (= zero (plus x one))))
(not (= zero (sum x one))))
(forall (x y)
(if (= (plus x one) (plus y one))
(if (= (sum x one) (sum y one))
(= x y)))
(forall (x)
(= x (plus x zero)))
(= x (sum x zero)))
(forall (x y)
(= (plus (plus x y) one) (plus x (plus y one))))
(= (sum (sum x y) one) (sum x (sum y one))))
(forall (p)
(if (and (p zero)
(forall (x)
(if (p x)
(p (plus x one)))))
(p (sum x one)))))
(forall (y)
(p y))))
@@ -1,10 +1,10 @@
(cl-text http://colore.oor.net/sum_arithmetic/sum_root.clif
(forall (x y)
(= (plus x y) (plus y x)))
(= (sum x y) (sum y x)))
(forall (x y z)
(= (plus (plus x y) z) (plus x (plus y z))))
(= (sum (sum x y) z) (sum x (sum y z))))
(forall (x y)
(exists (z)

0 comments on commit 609e4b9

Please sign in to comment.