Permalink
Browse files

modified theories in successor ad ordered arithmetic

  • Loading branch information...
michael.gruninger
michael.gruninger committed Jan 27, 2015
1 parent 5d019c3 commit 2b1de352a1694a8c26489253be73ac67f2bb6582
@@ -3,9 +3,7 @@
(cl-imports http://colore.oor.net/cyclic_ordering/megiddo_cyclic.clif)
(cl-imports http://colore.oor.net/successor/no_min_succ.clif)
(cl-imports http://colore.oor.net/successor/no_max_succ.clif)
(cl-imports http://colore.oor.net/successor/c_arithmetic.clif)
(forall (x y z w)
(if (and (C x y z)
@@ -22,14 +22,4 @@
(iff (lt x z)
(leq x y))))
(forall (x)
(iff (minimal x)
(not (exists (y)
(lt y x)))))
(forall (x)
(iff (maximal x)
(not (exists (y)
(lt x y)))))
)
@@ -22,14 +22,4 @@
(iff (lt x z)
(leq x y))))
(forall (x)
(iff (minimal x)
(not (exists (y)
(lt y x)))))
(forall (x)
(iff (maximal x)
(not (exists (y)
(lt x y)))))
)
@@ -0,0 +1,7 @@
(cl-text http://colore.oor.net/successor/c_arithmetic.clif
(cl-imports http://colore.oor.net/successor/no_min_succ.clif)
(cl-imports http://colore.oor.net/successor/no_max_succ.clif)
)
@@ -2,6 +2,8 @@
(cl-imports http://colore.oor.net/successor/unique_min_succ.clif)
(cl-imports http://colore.oor.net/successor/no_max_succ.clif)
(cl-imports http://colore.oor.net/successor/path_succ.clif)
)
@@ -1,6 +1,8 @@
(cl-text http://colore.oor.net/successor/successor.clif
(cl-imports http://colore.oor.net/successor/definitions/successor_def.clif)
(forall (x y z)
(if (and (S x y)
(S x z))
@@ -11,4 +13,9 @@
(S z y))
(= x z)))
(forall (y)
(if (not (zero y))
(exists (x)
(S x y))))
)

0 comments on commit 2b1de35

Please sign in to comment.