Rings

Definition Ring.D1:

Let R1 and R2 be two externally connected, thickly connected regions, whose outsides meet in two disconnected surface patches. Then R1 union R2 is a ring , also called a thick ring If the common boundary of the two contains a surface patch and a disconnected point set, then R1 union R2 is a thin ring. ("Thin ring" is a more general category than "ring".)

Declaration:
make_thin_ring(R1,R2,R : region; S1 : surface; S2 : pointset) -- Predicate
ring(R : region) --- Predicate.
thin_ring(R: region) --- Predicate.
ring_slice(RS, R : region) --- Predicate.

Formalism:
make_thin_ring(R1,R2,R : region; S1 : surface; S2 : pointset) < = >
rcc_EC(R1,R2) ^ R = R1 union R2 ^ thickly_connected(R1) ^ thickly_connected(R2) ^
R1 intersect R2 = S1 union S2 ^ connected(S1) ^ connected(S2) ^ PP(S1,outside(R1)) ^ PP(S2,outside(R2)) ^ DC(S1,S2).

ring(R) < = >
exists(R1,R2 : region; S1, S2 : surface) make_thin_ring(R1,R2,R,S1,S2).

thin_ring(R) < = >
exists(R1,R2 : region; S1 : surface; S2 : pointset) make_thin_ring(R1,R2,R,S1,S2).

ring_slice(RS,R) < = >
exists(R2) make_thin_ring(RS,R2,R).

Formalism:
thin_ring(R) < = >
exists(R1,R2 : region; S1,S2 : point_set) rcc_EC(R1,R2) ^ connected_component(S1,R1 cup R2) ^ connected_component(S2,R1 cup R2) ^ disjoint(S1,S2).

Definition Ring.D2:

RH is a ring hole through ring R if RH is a hole through R relative to some filling-in RF and all of the outlets of RH meet the outside of RF.

Formalism
ring_hole(RH,R : region) --- Predicate.

Definition: ring_hole(RH,R) < = >
exists(RF : region; RHS : set[region]) holes(RHS,R,RF) ^ RH in RHS ^
[forall((S : surface) in outlets(RH,R)) subset(S,outside(RF))]

Fact Ring.F1:

R is a thin ring if and only if there is a hole through R.

Characteristics : Topology.

Formalism:
thin_ring(R) < = > exists(RH : region) ring_hole(RH,R)

Fact Ring.F2:

If R1 and R2 combine to make a ring, then either R1 or R2 is not convex.

Characteristics : Geometry.

Formalism:
make_thin_ring(R1,R2,R,S1,S2) => ~convex(R1) V ~convex(R2).

Fact Ring.F3:

A ring is not a blob.

Characteristics : Topology

Formalism:
ring(R) => ~blob(R).

Definition Ring.D3:

Let R1 and R2 be disjoint thin rings. R1 interlocks with R2 iff every blob that contains R1 overlaps R2.

Declaration:
interlock(R1,R2 : region) --- Predicate.

Formalism:
interlock(R1,R2) < = >
thin_ring(R1) ^ thin_ring(R2) ^ DS(R1,R2) ^
forall(RS : region) [blob(RS) ^ PP(R1,RS)] => rcc_O(RS,R2).

Fact Ring.F4

If R1 interlocks R2 then R2 interlocks R1

Characteristics : Topology.

Formalism:
interlocks(R1,R2) < = > interlocks(R2,R1)

Fact Ring.F5

Let R1 be a ring and R2 be a region outside R1. Then there exists a blob handle RH such that R2 union RH interlocks with R1, but RH by itself does not interlock with R1.

Characteristics : Geometry.

Formalism:
thin_ring(R1) ^ PP(R2,outside(R1)) =>
exists(RH : region) rcc_EC(R2,RH) ^ blob(RH) ^ interlocks(R1,R2 union RH). ^ ~interlocks(R1,RH).

Fact Ring.F6

Let R1 and R2 be interlocking rings. Let R1A be a connected superset of R1 and let R2A be a connected superset of R2. If R1A and R2A are disjoint, then they are interlocking rings.

Characteristics : Geometry.

Formalism
interlocks(R1,R2) ^ PP(R1,R1A) ^ PP(R2,R2A) ^ rcc_DS(R1A,R2A) ^ connected(R1A) ^ connected(R2A) =>
interlocks(R1A,R2A).

Fact Ring.F7

If R1 is a ring, R2 is a connected subset of R1, and R2 is not a ring, then R1-R2 contains a slice through R.

Characteristics : Topology.

Formalism:
thin_ring(R1) ^ PP(R2,R1) ^ subset(R2,R1) ^ ~thin_ring(R2) =>
exists(R3 : region) ring_slice(R3,R1).

Fact Ring.F8

If R is a ring and R1 is a connected subset of R and not a ring, then R-R1 contains a slice of R.

Characteristics : Topology.

Formalism:
ring(R) ^ PP(R1,R) ^ ~ring(R1) => exists(R2) P(R2,R--R1) ^ ring_slice(R2,R).

Definition Ring.D4

A ring R is simple if it is composed of two slices that are not, themselves, rings.

Declaration: simple_ring(R : region)

Formalism:
simple_ring(R) < = >
exists(R1,R2,S1,S2) ~ring(R1) ^ ~ring(R2) ^ make_ring(R1,R2,R,S1,S2)

Fact Ring.F9

If R is a simple ring, and RS is a slice of R and not a ring, then R-RS is not a ring.

Characteristics : Topology.

Formalism:
simple_ring(R) ^ slice(R1,R) ^ ~ring(R1) => ~ring(R--R1).

Fact Ring.F10

If R is a simple ring and RS1 and RS2 are disconnected slices of R then R--RS1--RS2 is not connected.

Characteristics : Topology.

Formalism:
thin_ring(R1) ^ slice(RS1,R) ^ slice(RS2,R) ^ DC(RS1,RS2) => ~connected(R--R1--R2).

Fact Ring.F11

A ring can be divided into two rings.

Characteristics : Topology.

Formalism:
ring(R) => exists(R1,R2) ring(R1) ^ ring(R2) ^ rcc_EC(R1,R2) ^ R = R1 intersect R.

Fact Ring.F12

If R1 and R2 are interlocking solid rings, then there is no plane that separates R1 and R2.

Characteristics: Geometry

Formalism:
interlock(R1,R2) => ~[exists(SP) plane(SP) ^ plane_separates(SP,R1,R2)].

Kinematics

Fact Ring.F13

If O1 is a ring, O2 is a [thin] ring, and O1 and O2 are interlocking, then they have always been interlocking and will always be interlocking.

Characteristics: Kinematics

Formalism:
ring(O1 : object) ^ thin_ring(O2 : object) ^ holds(S1,interlock(O1,O2)) ^ S1 in H ^ S2 in H ^ kinematic(H) =>
holds(S2,interlock(O1,O2))