Multi-letter identifiers have been changed to look better than they do with vanilla L^{A}TEX: instead of specifications, you get specifications. The letters haven’t been spread apart, and the ligature fi has been used.

This is in typewriter font

BirthdayBook known : ℙ NAME birthday : NAME \underrightarrow{}DATE

known = dom birthday

limit : ℕ

limit ≤ 65536

Shape colour : Colour

perim : ℝ

perim > 0

ini : State × Occ × T → Bool

∀ S : State, i : Occ, t : T • ini(S, i, t) ⇔

θ(S→, 1, 0) ∧

∃ t_{1} : T • θ(→S, i, t_{1}) ∧ t_{1} ≤ t ∧ ∀ t_{2} : T • t_{2} < t ⇒ ¬θ(S→, i + 1, t_{2})

∨ θ(→S, 1, 0) ∧

∃ t_{1} : T • θ(→S, i, t_{1}) ∧ t_{1} ≤ t ∧ ∀ t_{2} : T • t_{2} < t ⇒ ¬θ(S→, i, t_{2})

Let us see if zbreak works:

MakePlan

c? : Company  [The company that is making the plan]
t? : Month  [Time period]

ΞNFMM ΞAttrOfMarkets

[OpenMarkets]

ΞCost ΞAttrOfEconomy

[Buying and selling price of quota ]

ΞAttrOfQuota ΞAttrOfProduction ΞFishingLimitations Plans! : Company → Plan

[The output is the plan for the company]

∀ v : Vessel; f : Fishery; s : QuotaStock; p : Product; l : Landing; t : Month; i : Input • ∃ plan : Plan; Months : ℙ Month; vs : ℙ Vessel; fs : ℙ Fishery; qs : ℙ QuotaStock; ls : ℙ Landing; ps : ℙ Product; catch : Vessel × Fishery × QuotaStock \underrightarrow{}Tons; MAXnet profit : Kronur; fishing cost : Kronur;

production earnings : Kronur;

production cost : Kronur; quota trading profit : Kronur; fishing days : Vessel × Fishery × Month \underrightarrow{}ℕ; value landing : Vessel → Kronur; export : Vessel × Landing × Month \underrightarrow{}Tons;

trade in, trade out : Landing × Month \underrightarrow{}Tons;

prod : Product × Month → Tons; quota rent in, quota rent out, quota next to,

quota next from, quota exch to, quota exch from,

quota trans from, quota trans to : Vessel × QuotaStock \underrightarrow{}Tons; ExchangeCharge : ℤ;

[charge for changing one species into another]

quota used : Vessel × QuotaStock \underrightarrow{}Tons • Plans! = Plans! ⊕ {c? ↦ plan} ∧

Months = t? . . 12 ∧

i ∈ Inputs ∧

vs = Vessels c? ∧ v ∈ vs ∧ fs = {f : Fishery | f ∈

(⋃{v : Vessel | v ∈ vs • Fisheries(v)}) • f } ∧ f ∈ fs ∧ qs = {s : QuotaStock; f : Fishery |

f ∈ fs ∧ s ∈ QuotaStocks(f ) • s} ∧ s ∈ qs ∧ ls = {s : QuotaStock; f : Fishery | f ∈ fs ∧ s ∈ qs •

Landings (f , s)} ∧ l ∈ ls ∧ ps = {p : Product |

p ∈ ⋃{fa : Factory | fa ∈ Factories c? • Products(fa)} • p} ∧

p ∈ ps ∧

[The overall goal is to maximize net profits]

MAXnet profit = −fishing cost + production earnings+ −production cost + quota trading profit ∧

[A.1]

catch (v, f , s) = ExpCatch (v, f , s)∗

[A.4]

∑_{t:Month|t∈Months} fishing days (v, f , t) ∧

[One of the prices LandingPrice or ExportPrice is always zero for any l]

(∀ l | l ∈ ls • LandingPrice(l) = 0 ∨ ExportPrice(l) = 0 ∧

LandingPrice(l) ≠ ExportPrice(l)) ∧ value landing =

[A.3]

{v : Vessel | v ∈ vs • v ↦ ∑_{l:Landing|l∈ls} LandingPrice(l) ∗ ExportPriceConst(l)∗ ∑_{f :Fishery|f ∈fs} ∑_{s:QuotaStock|s∈qs}(SpeciesToLandings (s, f , l) ∗ (catch (v, f , s))} ∧

fishing cost = ∑_{v:Vessel|v∈vs} Share(v) ∗ value landing(v)+

[A.2]

∑_{f :Fishery|f ∈fs} CostFishDay (v, f )∗ ∑_{t:Month|t∈Months} fishing days (v, f , t) ∧ production earnings =

[A.5]

∑l:Landing|l∈ls ∑t:Month|t∈Months

(ExportPrice (l, t)) ∗ (1 − 0.002) ∗ t)∗ ∑_{v:Vessel|v∈vs} export (v, l, t)

−WetfishBuyingPrice(l) ∗ (1 − 0.002) ∗ t) ∗ trade in (l, t) +WetfishSellingPrice(l) ∗ (1 − 0.002) ∗ t) ∗ trade out (l, t) + ∑_{p:Product|p∈ps} ProductPrice (p, t) ∗ (1 − 0.002) ∗ t)∗ ∑_{t:Month|t∈Months} prod (p, t) ∧

production cost = ∑_{i:Input|i∈Inputs} InputCost(i)∗

[A.6]

∑_{p:Product|p∈ps} InputForProduct(p, i)∗ ∑_{t:Month|t∈Months} prod(p, t) ∧

ExchangeCharge = 0.005 ∗ NextPrice(s) ∧ quota trading profit = −(∑_{s:QuotaStock|s∈qs} QuotaRentInPrice(s)∗

∑_{v:Vessel|v∈vs} quota rent in (v, s))

[A.7]

+ ∑_{s:QuotaStock|s∈qs} QuotaRentOutPrice(s)∗ ∑_{v:Vessel|v∈vs} quota rent out (v, s) + ∑_{s:QuotaStock|s∈qs} NextCharge ∗ NextPrice(s) ∗ (1 − InterestRate)∗ ∑_{v:Vessel|v∈vs} quota next to (v, s) + ∑_{s:QuotaStock|s∈qs} NextPrice(s) ∗ (1 − InterestRate)∗ ∑_{v:Vessel|v∈vs} quota next from (v, s) −ExchangeCharge ∗ ∑_{v:Vessel|v∈vs} ∑_{s:QuotaStock|s∈qs} quota exch to(v, s) −TransferCharge ∗ ∑_{v:Vessel|v∈vs} ∑_{s:QuotaStock|s∈qs} quota trans to (v, s) ∧

∑_{f :Fishery|f ∈fs} fishing days (v, f , t) ≤ MaxTotFishingDays (v, t) ∧

[A.9]

[A.6.1 Constraints on fishing time ]

l ∈ ExportLandings ⇒

∑f :Fishery|f ∈fs ∑s:QuotaStock|s∈qs

[A.10]

SpeciesToLandings (s, f , l) ∗ ExpCatch(v, f , s) ∗ fishing days(v, f , t) =

export (v, l, t) ∧

[A.6.2 Processing and selling the catch ]

l ∉ ExportLandings ⇒

∑v:Vessel|v∈vs ∑f :Fishery|f ∈fs ∑s:QuotaStock|s∈qs

SpeciesToLandings (s, f , l) ∗ ExpCatch (v, f , s) ∗ fishing days (v, f , t) = (1/LandingsToProducts (p, l)) ∗ prod (p, t) − trade in (l, t) + trade out(l, t) ∧

[A.11] ∑_{t:Month|t∈Months} ∑_{p:Product|p∈ps} InputForProduct(p, i) ∗ prod(p, t)

≤ ∑_{i:Input|i∈Inputs} MaxInput (i, t) ∧

[A.13]

∑_{t:Month|t∈Months} ∑_{p:Product|p∈ps} InputForProduct(p, i) ∗ prod (p, t)

≥ ∑_{i:Input|i∈Inputs} MinInput (i, t) ∧

[A.14]

∑_{t:Month|t∈Months} export (v, l, t) ≤ MaxExport (v, l) ∧

[A.15]

[A.6.3 Constraints because of quota restrictions ]

quota used =  [A.17]

{v : Vessel; s : QuotaStock | v ∈ vs ∧ s ∈ qs • (v, s) ↦ ∑_{f :Fishery|f ∈fs}(1 + QuotaSurcharge (s, f ))∗ catch (v, f , s)} ∧

∑_{v:Vessel|v∈vs} quota trans to(v, s) − quota trans from(v, s) = 0 ∧

[A.18]

quota used(v, s) − quota rent in(v, s) + quota rent out(v, s)−

[A.16]

quota exch to(v, s) + quota exch from(v, s)− quota trans to(v, s) + quota trans from(v, s)− quota next to (v, s) + quota next from (v, s) ≤ QuotaLeft (v, s) ∧

s = Cod ⇒ MaxQuotaInto(v, s) = 0 ∧

[A.19]

s ≠ Cod ⇒ MaxQuotaInto(v, s) = 0.05 ∗ QuotaAllocated(v, s) ∧

QuotaValueInto(s) ∗ quota exch to(v, s) ≤

∑_{s:QuotaStock|s∈qs} MaxQuotaInto (v, s) ∧

∑_{s:QuotaStock|s∈qs} QuotaValueInto(s) ∗ quota exch to (v, s)−

[A.20]

∑_{s:QuotaStock|s∈qs} QuotaValueFrom(s) ∗ quota exch from (v, s) = 0 ∧ quota next from(v, s) ≤ (QuotaOver(v, s)/100) ∗ QuotaAllocated(v, s) ∧

[A.21]

quota next to (v, s) ≤ (QuotaUnder(v, s)/100) ∗ QuotaAllocated(v, s) ∧

[A.22] [Bounds]

fishing days (v, f , t) ≤ MaxFishingDays (f , t) ∧

[A.23]

QuotaAllocated (v, s) = 0 ⇒ (quota exch to (v, s) = 0 ∧

[A.24]

quota rent in (v, s) = 0 ∧

[A.25]

quota trans to (v, s) = 0) ∧

[A.26]

QuotaValueInto s = 0 ⇒ quota exch to (v, s) = 0 ∧

[A.27]

QuotaValueFrom s = 0 ⇒ quota exch from (v, s) = 0 [A.28] plan.c = c? plan.fishing days = fishing days ∧ plan.quota rent out = quota rent out ∧ plan.quota rent in = quota rent in ∧ plan.quota trans from = quota trans from ∧ plan.quota trans to = quota trans to ∧ plan.quota next from = quota next from ∧ plan.quota next to = quota next to ∧ plan.quota exch from = quota exch from ∧ plan.quota exch to = quota exch to ∧ plan.trade out = trade out ∧ plan.trade in = trade in ∧ plan.prod = prod ∧ plan.export = export