Skip to content
Permalink
Browse files

Changed the ordered_algebra theories to import theories from Ordering…

…s Hierarchy
  • Loading branch information...
gruninger committed Jan 14, 2019
1 parent a16769a commit 7c1de020782ebb52f22c7f501513748d41a94770
@@ -62,8 +62,8 @@
(if (and (timeduration d1)
(timeduration d2)
(timeduration d3))
(if (lesser d1 d2)
(lesser (add_duration d1 d3) (add_duration d2 d3)))))
(if (lesser_duration d1 d2)
(lesser_duration (add_duration d1 d3) (add_duration d2 d3)))))

(forall (d1 d2 d3)
(if (and (timeduration d1)
@@ -76,15 +76,15 @@
(if (and (timeduration d1)
(timeduration d2)
(field r))
(if (lesser d1 d2)
(lesser (mult r d1) (mult r d2)))))
(if (lesser_duration d1 d2)
(lesser_duration (mult_duration r d1) (mult_duration r d2)))))

(forall (d1 d2 r)
(if (and (timeduration d1)
(timeduration d2)
(field r))
(if (= d1 d2)
(= (mult r d1) (mult r d2)))))
(= (mult_duration r d1) (mult_duration r d2)))))

)

@@ -63,18 +63,39 @@
(if (and (amount d1)
(amount d2)
(amount d3))
(iff (lesser_mass d1 d2)
(if (lesser_mass d1 d2)
(lesser_mass (add_mass d1 d3) (add_mass d2 d3)))))

(forall (d1 d2 d3)
(if (and (amount d1)
(amount d2)
(amount d3))
(iff (= d1 d2)
(if (= d1 d2)
(= (add_mass d1 d3) (add_mass d2 d3)))))

(forall (d1 d2 r)
(if (and (amount d1)
(amount d2)
(field r))
(if (lesser_amount d1 d2)
(lesser_amount (mult_mass r d1) (mult_mass r d2)))))

(forall (d1 d2 r)
(if (and (amount d1)
(amount d2)
(field r))
(if (= d1 d2)
(= (mult_mass r d1) (mult_mass r d2)))))

(forall (x)
(if (amount x)
(not (lesser_mass x zero_mass))))

)
(forall (x y)
(if (and (amount x)
(amount y))
(or (lesser_mass x y)
(lesser_mass y x)
(= x y))))

)
@@ -21,10 +21,9 @@
(= (mass x) (add_mass (mass y) (mass z)))))

(forall (x y)
(if (proper_chunk y x)
(if (lesser_mass (mass x) (mass y))
(exists (z)
(and (proper_chunk z x)
(not (= y z))
(and (proper_chunk z y)
(= (mass y) (mass z))))))

)
)
@@ -0,0 +1,8 @@

(cl-text http://colore.oor.net/ordered_algebra/linear_ordered_vectorspace.clif

(cl-imports http://colore.oor.net/ordered_algebra/ordered_vectorspace.clif)

(cl-imports http://colore.oor.net/orderings/linear_ordering.clif)

)
@@ -3,29 +3,21 @@

(cl-imports http://colore.oor.net/algebra/vectorspace.clif)

(forall (x)
(not (lesser x x)))
(cl-imports http://colore.oor.net/orderings/partial_ordering.clif)

(forall (x y)
(if (lesser x y)
(not (lesser y x))))
(cl-imports http://colore.oor.net/orderings/definitions/lt.clif)

(forall (x y z)
(if (and (lesser x y)
(lesser y z))
(lesser x z)))

(forall (x y z)
(if (lesser x y)
(lesser (op x z) (op y z))))
(if (lt x y)
(lt (op x z) (op y z))))

(forall (x y z)
(if (= x y)
(= (op x z) (op y z))))

(forall (x y r)
(if (lesser y x)
(lesser (mult r y) (mult r x))))
(if (lt y x)
(lt (mult r y) (mult r x))))

(forall (x y r)
(if (= x y)
@@ -0,0 +1,8 @@

(cl-text http://colore.oor.net/ordered_algebra/riesz_space.clif

(cl-imports http://colore.oor.net/ordered_algebra/ordered_vectorspace.clif)

(cl-imports http://colore.oor.net/orderings/lattice_ordering.clif)

)

0 comments on commit 7c1de02

Please sign in to comment.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.