  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
  56  simp [firstPassSchedule] at h
  57  rcases h with h | h | h | h | h
  58  · subst h
  59    simp [isHighOrImmediate, empiricalPriority]
  60  · subst h
  61    simp [isHighOrImmediate, empiricalPriority]
  62  · subst h
  63    simp [isHighOrImmediate, empiricalPriority]
  64  · subst h
  65    simp [isHighOrImmediate, empiricalPriority]
  66  · subst h
  67    simp [isHighOrImmediate, empiricalPriority]
  68
  69/-- The first-pass schedule contains exactly the high-or-immediate tests. -/
  70theorem firstPassSchedule_mem_iff_high_or_immediate (c : CombinationID) :
  71    c ∈ firstPassSchedule ↔ isHighOrImmediate c := by
  72  cases c <;> simp [firstPassSchedule, isHighOrImmediate, empiricalPriority]
  73
  74theorem firstPassSchedule_mem_protocol
  75    {c : CombinationID} (_h : c ∈ firstPassSchedule) :

papers checked against this theorem

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