Skip to content
Permalink
Browse files

corrected axioms for vector spaces and timedurations

  • Loading branch information...
gruninger committed Dec 29, 2018
1 parent 65564cb commit ac90ffb8b3b44d0af0d23e0c8f1fe746f330f86f
@@ -1,30 +1,38 @@
(cl-text http://colore.oor.net/algebra/module.clif

(cl-imports http://colore.oor.net/ringoids/ring.clif)
(cl-module ring (cl-imports http://colore.oor.net/ringoids/ring.clif))

(cl-module ringoid (cl-imports http://colore.oor.net/ringoids/ring.clif))
(cl-module magma (cl-imports http://colore.oor.net/magma/abelian_group.clif))

(cl-module algebra (cl-imports http://colore.oor.net/magma/abelian_group.clif))
(forall (x)
(if (magma x)
(not (ring x))))

(forall (x r)
(if (and (ring r)
(magma x))
(magma (mult r x))))

(forall (r x y)
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult r (op x y)) (op (mult r x) (mult r y))))
(if (and (ring r)
(magma x)
(magma y))
(= (mult r (op x y)) (op (mult r x) (mult r y)))))

(forall (r s x)
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult (sum r s) x) (op (mult r x) (mult s x))))
(if (and (ring r)
(ring s)
(magma x))
(= (mult (sum r s) x) (op (mult r x) (mult s x)))))

(forall (r s x)
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult (prod r s) x) (mult r (mult s x))))
(if (and (ring r)
(ring s)
(magma x))
(= (mult (prod r s) x) (mult r (mult s x)))))

(forall (x)
(= x (mult one x)))
(if (magma x)
(= x (mult one x))))

)
@@ -1,19 +1,38 @@
(cl-text http://colore.oor.net/algebra/vector_semispace.clif

(cl-imports http://colore.oor.net/ringoids/field.clif)
(cl-module field (cl-imports http://colore.oor.net/ringoids/field.clif))

(cl-imports http://colore.oor.net/magma/commutative_monoid.clif)
(cl-module magma (cl-imports http://colore.oor.net/magma/commutative_monoid.clif))

(forall (x)
(if (magma x)
(not (field x))))

(forall (x r)
(if (and (field r)
(magma x))
(magma (mult r x))))

(forall (r x y)
(= (mult r (op x y)) (op (mult r x) (mult r y))))
(if (and (field r)
(magma x)
(magma y))
(= (mult r (op x y)) (op (mult r x) (mult r y)))))

(forall (r s x)
(= (mult (sum r s) x) (op (mult r x) (mult s x))))
(if (and (field r)
(field s)
(magma x))
(= (mult (sum r s) x) (op (mult r x) (mult s x)))))

(forall (r s x)
(= (mult (prod r s) x) (mult r (mult s x))))
(if (and (field r)
(field s)
(magma x))
(= (mult (prod r s) x) (mult r (mult s x)))))

(forall (x)
(= x (mult one x)))
(if (magma x)
(= x (mult one x))))

)
@@ -1,29 +1,38 @@
(cl-text http://colore.oor.net/algebra/vectorspace.clif

(cl-module ringoid (cl-imports http://colore.oor.net/ringoids/ringoid.clif))
(cl-module field (cl-imports http://colore.oor.net/ringoids/field.clif))

(cl-module algebra (cl-imports http://colore.oor.net/magma/abelian_group.clif))
(cl-module magma (cl-imports http://colore.oor.net/magma/abelian_group.clif))

(forall (x)
(if (magma x)
(not (field x))))

(forall (x r)
(if (and (field r)
(magma x))
(magma (mult r x))))

(forall (r x y)
(if (and (ringoid r)
(algebra x)
(algebra y))
(if (and (field r)
(magma x)
(magma y))
(= (mult r (op x y)) (op (mult r x) (mult r y)))))

(forall (r s x)
(if (and (ringoid r)
(algebra x)
(algebra y))
(if (and (field r)
(field s)
(magma x))
(= (mult (sum r s) x) (op (mult r x) (mult s x)))))

(forall (r s x)
(if (and (ringoid r)
(algebra x)
(algebra y))
(if (and (field r)
(field s)
(magma x))
(= (mult (prod r s) x) (mult r (mult s x)))))

(forall (x)
(if (algebra x)
(if (magma x)
(= x (mult one x))))

)
@@ -5,6 +5,10 @@

(cl-imports http://colore.oor.net/duration/timeduration.clif)

(forall (x)
(if (timepoint x)
(not (timeduration x))))

(forall (t1 t2)
(if (and (timepoint t1)
(timepoint t2))
@@ -3,74 +3,88 @@

(cl-module field (cl-imports http://colore.oor.net/ringoids/field.clif))

(timeduration zero)
(timeduration zero_duration)

(forall (d1 d2)
(if (and (timeduration d1)
(timeduration d2))
(timeduration (add d1 d2))))
(timeduration (add_duration d1 d2))))

(forall (d1 d2 d3)
(if (and (timeduration d1)
(timeduration d2)
(timeduration d3))
(= (add (add d1 d2) d3) (add d1 (add d2 d3)))))
(= (add_duration (add_duration d1 d2) d3) (add_duration d1 (add_duration d2 d3)))))

(forall (d)
(if (timeduration d)
(= (add d zero) d)))
(= (add_duration d zero_duration) d)))

(forall (d1)
(if (timeduration d1)
(exists (d2)
(and (timeduration d2)
(= (add d1 d2) zero)))))
(= (add_duration d1 d2) zero_duration)))))

(forall (d1 d2)
(if (and (timeduration d1)
(timeduration d2))
(= (add d1 d2) (add d2 d1))))
(= (add_duration d1 d2) (add_duration d2 d1))))

(forall (d r)
(if (and (timeduration d)
(field r))
(timeduration (mult r d))))
(timeduration (mult_duration r d))))

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

(forall (d r s)
(if (and (timeduration d)
(field r)
(field s))
(= (mult (sum r s) d) (add (mult r d) (mult s d)))))
(= (mult_duration (sum r s) d) (add_duration (mult_duration r d) (mult_duration s d)))))

(forall (d r s)
(if (and (timeduration d)
(field r)
(field s))
(= (mult (prod r s) d) (mult r (mult s d)))))
(= (mult_duration (prod r s) d) (mult_duration r (mult_duration s d)))))

(forall (d)
(if (timeduration d)
(= d (mult one d))))
(= d (mult_duration one d))))

(forall (d1 d2 d3)
(if (and (timeduration d1)
(timeduration d2)
(timeduration d3))
(iff (lesser d1 d2)
(lesser (add d1 d3) (add d2 d3)))))
(if (lesser d1 d2)
(lesser (add_duration d1 d3) (add_duration d2 d3)))))

(forall (d1 d2 d3)
(if (and (timeduration d1)
(timeduration d2)
(timeduration d3))
(iff (= d1 d2)
(= (add d1 d3) (add d2 d3)))))
(if (= d1 d2)
(= (add_duration d1 d3) (add_duration d2 d3)))))

(forall (d1 d2 r)
(if (and (timeduration d1)
(timeduration d2)
(field r))
(if (lesser d1 d2)
(lesser (mult r d1) (mult r d2)))))

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

)

@@ -3,13 +3,32 @@

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

(forall (x)
(not (lesser x x)))

(forall (x y)
(if (lesser x y)
(not (lesser y x))))

(forall (x y z)
(iff (lesser x y)
(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))))

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

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

(forall (x y r)
(if (= x y)
(= (mult r x) (mult r y))))

)

0 comments on commit ac90ffb

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.