While this submission is a draft, it cannot be used by other submissions.

The standard reading of scheduling instances and schedules

Lax434175.StandardReading · concepts/Lax434175/StandardReading.lean · lax-434175

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The words in which the literature writes scheduling instances, schedules and online information, for the operations family, the batching family and the two standalone problems. All numbers are written in binary, as entries of the word.

    Blocks. A finite set of tuples of numbers is written canonically: the number of tuples, then every tuple, preceded by its length, in increasing lexicographic order and without repetition.

    Instances of the operations family. A field is written by its view, the meaning its constraints use, and not by its internal representation, so that two representations of the same constraints have the same word. The word consists of

    • a flag, 00 for the standard encoding and 11 for high multiplicity, the number of jobs and the number of machines;
    • for every job a record, preceded by its length: its number of operations, the processing time of every operation on every machine, its deadline (00 for none, or 11 followed by the deadline), and three blocks: the sets of machines each operation may occupy, the setup time of each operation at the server, and the transport delays between its operations; and its batch for batch setups;
    • a block of the facts on pairs of jobs: (0,i,j)(0, i, j) when ii precedes jj, (1,i,j,s,l)(1, i, j, s, l) for the lag ±l±l of such a pair (s=1s = 1 for a negative lag), and (2,i,j,c)(2, i, j, c) when the pair has communication delay cc;
    • a block of the global facts: (0,t)(0, t) for every forbidden time, (1,a,b,s)(1, a, b, s) for the setup time ss from batch aa to batch bb, for the batches of jobs, and, when the problem has a transport robot, (2,i,i′,t)(2, i, i', t) for the empty moving time tt of the robot from machine ii to machine i′i', for all machines (all 00 when the robot has no empty moves);
    • for every job its release date, weight and due date (11 and 00 when the objective has none), three numbers each, in the order of the jobs.

    The release dates, weights and due dates come last so that changing the objective — which the threshold steps between objectives do — rewrites only the end of the word. With high multiplicity the jobs are written as a block of their distinct records, each followed by the job's release date, weight and due date and preceded by the number of jobs that have both, and there are no facts on pairs.

    Instances of batching: the number of jobs, the setup time and the capacity, then for every job its processing time, release date, weight, due date, deadline and size, then the block of precedence pairs, each with its lag. Rejection: the number of jobs and the budget, then the processing time and rejection cost of every job. Machine covering: the numbers of jobs and machines and the processing times.

    Schedules. A schedule of the operations family is the list of its pieces, each written as its job, operation, start and length (a rational as numerator and reduced denominator) and the sorted machines it occupies. With high multiplicity a schedule is written compactly, by machine patterns: a list of groups, each a number cc of machines followed by the pieces every one of them runs, a piece written as the type of its job (the position of the job's tuple in the block of distinct records), its operation, start and length. The groups use consecutive machines, cc for a group, and the kk-th piece of a type and an operation goes to the kk-th job of that type, in the order of the jobs; every operation is one piece. A batch schedule writes for every job its batch and the start and processing time of that batch; a rejection schedule for every job whether it is accepted and its start; a covering the machine of every job.

    Online. For problems whose jobs arrive online, the scheduler sees at time tt the records of the jobs released by tt (with their numbers), the facts on pairs of them, and the global facts; two schedules made the same decisions up to tt if they have the same pieces starting before tt. Other problems are revealed at once.

    Concept map
    59 concepts
    100%
    Conjunctive normal formAssembling problems from fieldsOne family for serial and parallel batchingBatching problems in three-field notationBatch scheduling on a single machineCommunication delaysBounds on the number of machines and jobsDeadlinesForbidden times and input encodingsInterruption as a field of parallel-machineschedulingScheduling kernelsMaximizing the minimum machine loadMachine sets and multiprocessor tasksConstraint modules and objectivesNon-preemptive scheduling on parallelmachinesCompletion-time objectivesOnline scheduling as a gameScheduling with operationsOne family for parallel machines and shopsOne family for parallel machines with andwithout preemptionParallel machinesProblems on parallel machines in three-fieldnotationParameters along embeddingsPrecedence constraints and time lagsPreemptive scheduling on parallel machinesPreemptive shop problems in three-fieldnotationPreemptive shop schedulingOptimization problems and embeddingsSingle-machine scheduling with rejectionRelease datesPreemption with restarts on parallelmachinesParameters of the zoo's resultsThe kinds of results on scheduling problemsA single server with setup timesNo-idle shops and batch setup timesOne family for shops with and withoutpreemptionShop problems in three-field notationShop schedulingThe standard reading of scheduling instancesand schedulesThreshold reductions between objectivesTransportation delays and a transport robotScheduling problems as parameterizedproblems on wordsParameters of scheduling problemsBinary encoding of an input and a certificateThe complexity class NPThe complexity class PFixed-Parameter Time on the Word RAMFPT-Reductions, FPT, Hardness andCompletenessFinite Relational StructuresFirst-Order Formulas and the Classes Σ_tand Π_tModel Checking and Weighted FaginDefinabilityThe W-Hierarchy and the A-HierarchyNP-Hardness of a Problem on Words ofNumbersBinary encoding of finite wordsPolynomial-time computation by a wordRAMPolynomial-time computation by a TuringmachineThe word RAMComputing a function within a time boundParameterized Problems andFPT-Reductions on a Word RAM
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax434175.Results
    2import Lax434175.ResultParameters
    3
    4/-!
    5---
    6title: The standard reading of scheduling instances and schedules
    7type: definition
    8---
    9The words in which the literature writes scheduling instances, schedules and
    10online information, for the operations family, the batching family and the two
    11standalone problems. All numbers are written in binary, as entries of the word.
    12
    13**Blocks.** A finite set of tuples of numbers is written canonically: the
    14number of tuples, then every tuple, preceded by its length, in increasing
    15lexicographic order and without repetition.
    16
    17**Instances of the operations family.** A field is written by its *view*, the
    18meaning its constraints use, and not by its internal representation, so that
    19two representations of the same constraints have the same word. The word
    20consists of
    21
    22- a flag, `0` for the standard encoding and `1` for high multiplicity, the number
    23 of jobs and the number of machines;
    24- for every job a record, preceded by its length: its number of operations, the
    25 processing time of every operation on every machine, its deadline (`0` for
    26 none, or `1` followed by the deadline), and three blocks: the sets of machines
    27 each operation may occupy, the setup time of each operation at the server, and
    28 the transport delays between its operations; and its batch for batch setups;
    29- a block of the facts on pairs of jobs: `(0, i, j)` when `i` precedes `j`,
    30 `(1, i, j, s, l)` for the lag `±l` of such a pair (`s = 1` for a negative lag),
    31 and `(2, i, j, c)` when the pair has communication delay `c`;
    32- a block of the global facts: `(0, t)` for every forbidden time,
    33 `(1, a, b, s)` for the setup time `s` from batch `a` to batch `b`, for the
    34 batches of jobs, and, when the problem has a transport robot, `(2, i, i', t)`
    35 for the empty moving time `t` of the robot from machine `i` to machine `i'`,
    36 for all machines (all `0` when the robot has no empty moves);
    37- for every job its release date, weight and due date (`1` and `0` when the
    38 objective has none), three numbers each, in the order of the jobs.
    39
    40The release dates, weights and due dates come last so that changing the
    41objective — which the threshold steps between objectives do — rewrites only the
    42end of the word. With high multiplicity the jobs are written as a block of their
    43distinct records, each followed by the job's release date, weight and due date and
    44preceded by the number of jobs that have both, and there are no facts on pairs.
    45
    46**Instances of batching**: the number of jobs, the setup time and the capacity,
    47then for every job its processing time, release date, weight, due date, deadline
    48and size, then the block of precedence pairs, each with its lag. **Rejection**: the number of jobs
    49and the budget, then the processing time and rejection cost of every job.
    50**Machine covering**: the numbers of jobs and machines and the processing times.
    51
    52**Schedules.** A schedule of the operations family is the list of its pieces,
    53each written as its job, operation, start and length (a rational as numerator
    54and reduced denominator) and the sorted machines it occupies. With high
    55multiplicity a schedule is written compactly, by *machine patterns*: a list of
    56groups, each a number cc of machines followed by the pieces every one of them
    57runs, a piece written as the type of its job (the position of the job's tuple in
    58the block of distinct records), its operation, start and length. The groups use
    59consecutive machines, cc for a group, and the kk-th piece of a type and an
    60operation goes to the kk-th job of that type, in the order of the jobs; every
    61operation is one piece. A batch schedule
    62writes for every job its batch and the start and processing time of that batch;
    63a rejection schedule for every job whether it is accepted and its start; a
    64covering the machine of every job.
    65
    66**Online.** For problems whose jobs arrive online, the scheduler sees at time tt
    67the records of the jobs released by tt (with their numbers), the facts on pairs
    68of them, and the global facts; two schedules made the same decisions up to tt if
    69they have the same pieces starting before tt. Other problems are revealed at
    70once.
    71-/
    72
    73namespace Lax434175.StandardReading
    74open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Results
    75open Lax434175.ResultParameters
    76
    77-- Blocks
    78
    79/-- The list writes the set: increasing, without repetition, and with the same
    80elements. -/
    81def Lists (S : Set (List ℕ)) (L : List (List ℕ)) : Prop :=
    82 L.Pairwise (· < ·) ∧ ∀ t, t ∈ L ↔ t ∈ S
    83
    84/-- A list of tuples, each preceded by its length, after their number. -/
    85def flat (L : List (List ℕ)) : List ℕ := L.length :: L.flatMap fun t => t.length :: t
    86
    87/-- The word is the canonical block of the set. -/
    88def Block (S : Set (List ℕ)) (b : List ℕ) : Prop := ∃ L, Lists S L ∧ b = flat L
    89
    90/-- An integer as sign and absolute value. -/
    91def int (z : ℤ) : List ℕ := [if z < 0 then 1 else 0, z.natAbs]
    92
    93/-- A deadline: `0` for none, `1` and the value otherwise. -/
    94def enat (e : ℕ∞) : List ℕ := if e = ⊤ then [0] else [1, e.toNat]
    95
    96/-- A rational as numerator and denominator. -/
    97def rat (q : NNRat) : List ℕ := [q.num, q.den]
    98
    99/-- A set of machines, sorted. -/
    100def machinesWord {m : ℕ} (S : Finset (Fin m)) : List ℕ :=
    101 (S.image Fin.val).sort (· ≤ ·)
    102
    103-- The operations family
    104
    105section Ops
    106
    107variable {s : Spec OperationsFamily.family} (x : Inst OperationsFamily.family s)
    108
    109/-- The fixed part of the record of a job. -/
    110def jobHead (j : Fin x.base.jobs) : List ℕ :=
    111 [x.base.ops j] ++
    112 (List.ofFn fun k : Fin (x.base.ops j) => List.ofFn fun i => x.base.p j k i).flatten ++
    113 enat (Deadlines.view (K := Operations.kernel) (s.module .deadlines) (x.data .deadlines) j)
    114
    115/-- The release date, weight and due date of a job. -/
    116def objOf (j : Fin x.base.jobs) : List ℕ := [x.base.r j, Ops.weight s x j, Ops.due s x j]
    117
    118/-- The release dates, weights and due dates of all jobs, three numbers each. -/
    119def objWord : List ℕ := (List.ofFn (objOf x)).flatten
    120
    121/-- The machines an operation of the job may occupy. -/
    122def machineTuples (j : Fin x.base.jobs) : Set (List ℕ) :=
    123 {t | ∃ (k : Fin (x.base.ops j)) (S : Finset (Fin x.base.machines)),
    124 Operations.Machines.view (s.module .machineSets)
    125 (x.data .machineSets : Operations.Machines.Data _ x.base) ⟨j, k⟩ S ∧
    126 t = k.val :: machinesWord S}
    127
    128/-- The setup times of the operations of the job at the server. -/
    129def serverTuples (j : Fin x.base.jobs) : Set (List ℕ) :=
    130 {t | ∃ (k : Fin (x.base.ops j)) (f : Operations.Op x.base → ℕ),
    131 Servers.view (s.module .server) (x.data .server : Servers.Data (Operations.Op x.base) _) =
    132 some f ∧ t = [k.val, f ⟨j, k⟩]}
    133
    134/-- The transport delays between the operations of the job. -/
    135def transportTuples (j : Fin x.base.jobs) : Set (List ℕ) :=
    136 {t | ∃ k k' : Fin (x.base.ops j),
    137 t = [k.val, k'.val, (x.data .transportation : Transportation.Data x.base.toShop).1 j k k']}
    138
    139/-- The batch of the job for batch setups. -/
    140def batchOf (j : Fin x.base.jobs) : ℕ :=
    141 ShopExtras.BatchSetups.batch (x := x.base.toShop) (s.module .batchSetups)
    142 (x.data .batchSetups) j
    143
    144/-- The word is the record of the job. -/
    145def Record (j : Fin x.base.jobs) (b : List ℕ) : Prop :=
    146 ∃ b₁ b₂ b₃, Block (machineTuples x j) b₁ ∧ Block (serverTuples x j) b₂ ∧
    147 Block (transportTuples x j) b₃ ∧ b = jobHead x j ++ b₁ ++ b₂ ++ b₃ ++ [batchOf x j]
    148
    149/-- The facts on pairs of jobs. -/
    150def pairTuples : Set (List ℕ) :=
    151 {t | ∃ i j : Fin x.base.jobs, Ops.prec s x i j ∧ t = [0, i.val, j.val]} ∪
    152 {t | ∃ i j : Fin x.base.jobs, Ops.prec s x i j ∧
    153 t = [1, i.val, j.val] ++ int ((s.module .precedence).lags.view (x.data .precedence).2 i j)} ∪
    154 {t | ∃ (i j : Fin x.base.jobs) (c : ℕ), CommunicationDelays.view (s.module .communicationDelays)
    155 (x.data .communicationDelays : CommunicationDelays.Data _ x.base.toPar) i j c ∧
    156 t = [2, i.val, j.val, c]}
    157
    158/-- The global facts. -/
    159def globalTuples : Set (List ℕ) :=
    160 {t | ∃ τ ∈ ForbiddenTimes.view (s.module .forbiddenTimes) (x.data .forbiddenTimes), t = [0, τ]} ∪
    161 {t | ∃ i j : Fin x.base.jobs, t = [1, batchOf x i, batchOf x j,
    162 ShopExtras.BatchSetups.setup (x := x.base.toShop) (s.module .batchSetups)
    163 (x.data .batchSetups) (batchOf x i) (batchOf x j)]} ∪
    164 {t | (s.module .transportation).robot = true ∧ ∃ i i' : Fin x.base.machines,
    165 t = [2, i.val, i'.val, (x.data .transportation : Transportation.Data x.base.toShop).2 i i']}
    166
    167/-- The records of all jobs, in order, each preceded by its length. -/
    168def Records (b : List ℕ) : Prop :=
    169 ∃ R : Fin x.base.jobs → List ℕ, (∀ j, Record x j (R j)) ∧
    170 b = (List.ofFn fun j => (R j).length :: R j).flatten
    171
    172/-- The distinct records, each with the number of jobs that have it. -/
    173noncomputable def typeTuples : Set (List ℕ) :=
    174 {t | ∃ b j, Record x j b ∧
    175 t = Nat.card {j' // Record x j' b ∧ objOf x j' = objOf x j} :: (b ++ objOf x j)}
    176
    177/-- The word of an instance of the operations family. -/
    178def EncodesOps (w : List ℕ) : Prop :=
    179 ∃ b₂ b₃, Block (pairTuples x) b₂ ∧ Block (globalTuples x) b₃ ∧
    180 ((s.module .encoding = .standard ∧ ∃ b₁, Records x b₁ ∧
    181 w = [0, x.base.jobs, x.base.machines] ++ b₁ ++ b₂ ++ b₃ ++ objWord x) ∨
    182 (s.module .encoding = .highMultiplicity ∧ pairTuples x = ∅ ∧ ∃ b₁, Block (typeTuples x) b₁ ∧
    183 w = [1, x.base.jobs, x.base.machines] ++ b₁ ++ b₂ ++ b₃))
    184
    185/-- The word of a piece of a schedule. -/
    186def pieceWord (q : Operations.Piece x.base) : List ℕ :=
    187 [q.op.1.val, q.op.2.val] ++ rat q.start ++ rat q.length ++ machinesWord q.machines
    188
    189/-- The word of a schedule: its pieces in order. -/
    190def schedWord (σ : Operations.Sched x.base) : List ℕ := flat (σ.pieces.map (pieceWord x))
    191
    192/-- The type of a job in a high-multiplicity word: the position of its tuple in
    193the canonical list of the distinct records. -/
    194def TypeIndex (j : Fin x.base.jobs) (t : ℕ) : Prop :=
    195 ∃ L b, Lists (typeTuples x) L ∧ Record x j b ∧
    196 L[t]? = some (Nat.card {j' // Record x j' b ∧ objOf x j' = objOf x j} :: (b ++ objOf x j))
    197
    198end Ops
    199
    200/-- A piece of a machine pattern: the type of its job, its operation, start and
    201length. -/
    202structure Slot where
    203 type : ℕ
    204 op : ℕ
    205 start : NNRat
    206 length : NNRat
    207
    208/-- A group of a compact schedule: a number of machines and the pieces each of
    209them runs. -/
    210abbrev Group := ℕ × List Slot
    211
    212/-- The word of a group. -/
    213def groupWord (g : Group) : List ℕ :=
    214 g.1 :: flat (g.2.map fun q => [q.type, q.op] ++ rat q.start ++ rat q.length)
    215
    216/-- The word of a compact schedule. -/
    217def compactWord (G : List Group) : List ℕ := flat (G.map groupWord)
    218
    219/-- The pieces of a compact schedule with their machines, the groups using
    220consecutive machines from `base` on. -/
    221def expand : List Group → ℕ → List (ℕ × Slot)
    222 | [], _ => []
    223 | (c, P) :: G, base =>
    224 (List.range c).flatMap (fun k => P.map fun q => (base + k, q)) ++ expand G (base + c)
    225
    226section Ops
    227
    228variable {s : Spec OperationsFamily.family} (x : Inst OperationsFamily.family s)
    229
    230/-- The schedule is the one the compact schedule writes: piece by piece the same
    231machine, operation, start and length, a job of the slot's type, and the `k`-th
    232slot of a type and an operation for the `k`-th job of that type. -/
    233def ExpandsTo (G : List Group) (σ : Operations.Sched x.base) : Prop :=
    234 σ.pieces.length = (expand G 0).length ∧
    235 ∀ (n : ℕ) (hσ : n < σ.pieces.length) (hG : n < (expand G 0).length),
    236 (σ.pieces[n].machines.image Fin.val = {((expand G 0)[n]).1}) ∧
    237 σ.pieces[n].op.2.val = ((expand G 0)[n]).2.op ∧
    238 σ.pieces[n].start = ((expand G 0)[n]).2.start ∧
    239 σ.pieces[n].length = ((expand G 0)[n]).2.length ∧
    240 TypeIndex x σ.pieces[n].op.1 ((expand G 0)[n]).2.type ∧
    241 Nat.card {j : Fin x.base.jobs // j < σ.pieces[n].op.1 ∧ TypeIndex x j ((expand G 0)[n]).2.type} =
    242 ((expand G 0).take n).countP fun b =>
    243 b.2.type == ((expand G 0)[n]).2.type && b.2.op == ((expand G 0)[n]).2.op
    244
    245/-- What is revealed at time `t`: the records of the jobs released by `t` with
    246their numbers, the facts on pairs of them, and the global facts. -/
    247def RevealedOps (t : NNRat) (w : List ℕ) : Prop :=
    248 ∃ (R : Fin x.base.jobs → List ℕ) (b₂ b₃ : List ℕ), (∀ j, Record x j (R j)) ∧
    249 Block {u ∈ pairTuples x | ∀ v ∈ u.drop 1 |>.take 2,
    250 ∃ j : Fin x.base.jobs, j.val = v ∧ (x.base.r j : NNRat) ≤ t} b₂ ∧
    251 Block (globalTuples x) b₃ ∧
    252 w = [x.base.machines] ++ ((List.ofFn fun j => (j, R j)).filter fun p =>
    253 decide ((x.base.r p.1 : NNRat) ≤ t)).flatMap
    254 (fun p => p.1.val :: p.2.length :: (p.2 ++ objOf x p.1)) ++
    255 b₂ ++ b₃
    256
    257end Ops
    258
    259open Classical in
    260/-- The standard reading of the operations family. -/
    261noncomputable def ops : Reading OperationsFamily.family where
    262 Encodes _ w x := EncodesOps x w
    263 Decodes s x w σ := if s.module .encoding = .highMultiplicity then
    264 ∃ G, w = compactWord G ∧ ExpandsTo x G σ else w = schedWord x σ
    265 reveal s :=
    266 { same := fun x y t =>
    267 if s.module .releaseDates = .online then ∀ w, RevealedOps x t w ↔ RevealedOps y t w
    268 else ∀ w, EncodesOps x w ↔ EncodesOps y w
    269 agree := fun x y σ τ t =>
    270 flat ((σ.pieces.filter fun q => decide (q.start < t)).map (pieceWord x)) =
    271 flat ((τ.pieces.filter fun q => decide (q.start < t)).map (pieceWord y)) }
    272
    273-- The batching family
    274
    275section Batch
    276
    277variable {s : Spec BatchFamily.family} (x : Inst BatchFamily.family s)
    278
    279/-- The record of a job. -/
    280def batchRecord (j : Fin x.base.jobs) : List ℕ :=
    281 [x.base.p j, x.base.r j, Batch.weight s x j,
    282 Objectives.dueDate (K := BatchFamily.kernel) s.objective x.objectiveData j] ++
    283 enat (Deadlines.view (K := BatchFamily.kernel) (s.module (.field .deadlines))
    284 (x.data (.field .deadlines)) j) ++
    285 [Batching.Capacity.size (x := x.base) (s.module (.field .capacity)) (x.data (.field .capacity)) j]
    286
    287/-- The precedence pairs, each with its lag. -/
    288def batchPairs : Set (List ℕ) :=
    289 {t | ∃ i j : Fin x.base.jobs,
    290 (s.module (.field .precedence)).order.view (x.data (.field .precedence)).1 i j ∧
    291 t = [i.val, j.val] ++ int ((s.module (.field .precedence)).lags.view (x.data (.field .precedence)).2 i j)}
    292
    293/-- The word of a batching instance. -/
    294def EncodesBatch (w : List ℕ) : Prop :=
    295 ∃ b, Block (batchPairs x) b ∧
    296 w = [x.base.jobs, x.base.setup,
    297 Batching.Capacity.bound (x := x.base) (s.module (.field .capacity)) (x.data (.field .capacity))] ++
    298 (List.ofFn fun j => batchRecord x j).flatten ++ b
    299
    300/-- The word of a batch schedule: for every job its batch and that batch's start
    301and processing time. -/
    302def batchSchedWord (σ : BatchFamily.Sched x.base) : List ℕ :=
    303 (List.ofFn fun j => [σ.batch j, σ.start (σ.batch j), σ.length (σ.batch j)]).flatten
    304
    305end Batch
    306
    307/-- The standard reading of the batching family. -/
    308noncomputable def batch : Reading BatchFamily.family where
    309 Encodes _ w x := EncodesBatch x w
    310 Decodes _ x w σ := w = batchSchedWord x σ
    311 reveal _ :=
    312 { same := fun x y _ => ∀ w, EncodesBatch x w ↔ EncodesBatch y w
    313 agree := fun x y σ τ _ => batchSchedWord x σ = batchSchedWord y τ }
    314
    315-- The standalone problems
    316
    317/-- The standard reading of single-machine scheduling with rejection. -/
    318noncomputable def rejection : PReading Rejection.problem where
    319 Encodes w x := w = [x.jobs, x.budget] ++ (List.ofFn fun j => [x.p j, x.e j]).flatten
    320 Decodes _ w σ := w = (List.ofFn fun j =>
    321 [if j ∈ σ.accepted then 1 else 0, σ.start j]).flatten
    322 reveal :=
    323 { same := fun x y _ => x = y
    324 agree := fun _ _ _ _ _ => True }
    325
    326/-- The standard reading of machine covering. -/
    327def covering : PReading MachineCovering.problem where
    328 Encodes w x := w = [x.jobs, x.machines] ++ List.ofFn x.p
    329 Decodes _ w σ := w = List.ofFn fun j => (σ j).val
    330 reveal :=
    331 { same := fun x y _ => x = y
    332 agree := fun _ _ _ _ _ => True }
    333
    334end Lax434175.StandardReading
    335

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…