  22open OptionAEmpiricalQueue
  23
  24/-- First-pass empirical test order. -/
  25def firstPassSchedule : List CombinationID :=
  26  [ .c3OncologyTensor
  27  , .c8MillerSpan
  28  , .c5AttentionTensor
  29  , .c9RegulatoryCeiling
  30  , .c2PlanetStrata
  31  ]
  32
  33theorem firstPassSchedule_length :
  34    firstPassSchedule.length = 5 := by
  35  decide
  36
  37theorem firstPassSchedule_head :
  38    firstPassSchedule.head? = some .c3OncologyTensor := by
  39  decide
  40
  41theorem firstPassSchedule_second :
  42    firstPassSchedule[1]? = some .c8MillerSpan := by
  43  decide
  44
  45theorem firstPassSchedule_third :
  46    firstPassSchedule[2]? = some .c5AttentionTensor := by
  47  decide
  48
  49theorem firstPassSchedule_nodup :
  50    firstPassSchedule.Nodup := by
  51  decide
  52
  53theorem firstPassSchedule_mem_high_or_immediate
  54    {c : CombinationID} (h : c ∈ firstPassSchedule) :
  55    isHighOrImmediate c := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.