Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
170 lines (118 sloc) 3.06 KB
/*******************************************************************************
* Copyright (c) University of Toronto and others. All rights reserved.
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 4.0 Unported license. The legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/4.0/legalcode.
*
* Contributors:
* Torsten Hahmann - initial implementation
*******************************************************************************/
(cl-text http://colore.oor.net/multidim_space_codi/codi_down.clif
(cl-imports http://colore.oor.net/multidim_space_codi/codi_basic.clif)
(cl-imports http://colore.oor.net/multidim_space_codi/definitions/ep.clif)
(cl-imports http://colore.oor.net/multidim_space_dim/definitions/dim_basic_defs.clif)
(cl-imports http://colore.oor.net/multidim_space_cont/definitions/c.clif)
(cl-comment 'Int-A1: disconnected entities have empty intersection')
(forall (x y)
(iff
(and
(S x)
(S y)
(not (C x y))
)
(ZEX (intersection x y))
)
)
(cl-comment 'Int-A2: the intersection is contained in the intersecting entities (also ensures the intersection is of no greater dimension than necessary)')
(forall (x y)
(if
(and
(S x)
(S y)
(not (ZEX (intersection x y)))
)
(Cont (intersection x y) x)
)
)
(cl-comment 'Int-A3: the intersection is of greatest possible dimension (determines the dimension of the intersection)')
(forall (x y z)
(if
(and
(Cont z x)
(Cont z y)
)
(<= z (intersection x y))
)
)
(cl-comment 'Int-A4: the intersection contains everything of the greatest possible dimension (and whatever those things contain)')
(forall (x y z)
(iff
(and
(Cont z x)
(Cont z y)
(EqDim z (intersection x y))
)
(P z (intersection x y))
)
)
(cl-comment 'Closure under differences')
(cl-comment 'Dif-A1: difference is of same dimension')
(forall (x y)
(if
(and
(S x)
(S y)
(not (ZEX (difference x y)))
)
(EqDim x (difference x y))
)
)
(cl-comment 'Dif-A2: difference with a entity of lower dimension')
(forall (x y)
(if
(< y x)
(= x (difference x y))
)
)
(cl-comment 'Dif-A3a: constitution of the difference with an entity of greater or equal dimension')
(forall (x y z)
(if
(and
(<= x y)
(Cont z x)
(< (intersection z y) z)
)
(Cont z (difference x y))
)
)
(cl-comment 'Dif-A3b: constitution of the difference with an entity of greater or equal dimension')
(forall (x y z)
(if
(and
(<= x y)
(Cont z (difference x y))
)
(Cont z x)
)
)
(cl-comment 'Dif-A3c: constitution of the difference with an entity of greater or equal dimension')
(forall (x y z)
(if
(and
(<= x y)
(P z (difference x y))
)
(< (intersection z y) z)
)
)
(cl-comment 'Dif-A4: zero difference only for contained entities or for zero entity')
(forall (x y)
(iff
(ZEX (difference x y))
(or
(ZEX x)
(Cont x y)
)
)
)
)
You can’t perform that action at this time.