firstPassSchedule_second

formal source

  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
  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