Moser Set Operations

def Moser.WorkingSet.bigSetRemoval (s : WorkingSet) : WorkingSet

Operation 1: Remove polygons with area exceeding the threshold

Equations

• s.bigSetRemoval = { polygons := List.filter (fun (p : ConvexPolygon) => decide (p.area ≤ Moser.areaThreshold)) s.polygons }

def Moser.WorkingSet.supersetRemoval (s : WorkingSet) : WorkingSet

Operation 2: Remove polygons which are supersets of others

Equations

• One or more equations did not get rendered due to their size.

def Moser.WorkingSet.wormAdding (wormHull : ConvexPolygon) (epsilon : ℚ) (eps_pos : 0 < epsilon) (s : WorkingSet) : WorkingSet

Operation 4: Add a worm to the working set

Equations

• One or more equations did not get rendered due to their size.

def Moser.WorkingSet.cleanup (s : WorkingSet) : WorkingSet

Apply all cleanup operations: bigSetRemoval

Equations

• s.cleanup = s.bigSetRemoval.supersetRemoval

def Moser.WorkingSet.addWormAndCleanup (wormHull : ConvexPolygon) (epsilon : ℚ) (eps_pos : 0 < epsilon) (s : WorkingSet) : WorkingSet

Add worm and cleanup

Equations

• Moser.WorkingSet.addWormAndCleanup wormHull epsilon eps_pos s = (Moser.WorkingSet.wormAdding wormHull epsilon eps_pos s).cleanup

def Moser.WorkingSet.InitialWorkingSet : WorkingSet

The initial working set: a single polygon, the InitialWorm.

Equations

• Moser.WorkingSet.InitialWorkingSet = { polygons := [Moser.InitialWorm] }