style: fix bad indents (#418)

Theorem statements and their binders should always be indented four
spaces or more

Author: eric-wieser

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

@@ -198,8 +198,8 @@ theorem mergeSort_time_le (xs : List α) :
 
 /-- Time complexity of mergeSort -/
 theorem mergeSort_time (xs : List α) :
-  let n := xs.length
-  (mergeSort xs).time ≤ n * clog 2 n := by
+    let n := xs.length
+    (mergeSort xs).time ≤ n * clog 2 n := by
   grind [mergeSort_time_le, timeMergeSortRec_le]
 
 end TimeComplexity

Cslib/Computability/Automata/NA/Hist.lean

@@ -45,7 +45,7 @@ theorem hist_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State × Hist)}
 /-- Given a run of the original automaton, `makeHist` builds a run of the history state. -/
 @[scoped grind =]
 def makeHist (start' : State → Hist) (tr' : State × Hist → Symbol → State → Hist)
-  (xs : ωSequence Symbol) (ss : ωSequence State) : ℕ → Hist
+    (xs : ωSequence Symbol) (ss : ωSequence State) : ℕ → Hist
   | 0 => start' (ss 0)
   | n + 1 => tr' (ss n, makeHist start' tr' xs ss n) (xs n) (ss (n + 1))
 

Cslib/Foundations/Control/Monad/Free/Fold.lean

@@ -48,26 +48,26 @@ namespace FreeM
 variable {F : Type u → Type v} {ι : Type u} {α : Type w} {β : Type w'}
 
 /-- Fold function for the `FreeM` monad -/
-def foldFreeM {F : Type u → Type v} {α β : Type w}
-  (onValue : α → β)
-  (onEffect : {ι : Type u} → F ι → (ι → β) → β)
-  : FreeM F α → β
+def foldFreeM
+    (onValue : α → β)
+    (onEffect : {ι : Type u} → F ι → (ι → β) → β) :
+    FreeM F α → β
   | .pure a => onValue a
   | .liftBind op k => onEffect op (fun x => foldFreeM onValue onEffect (k x))
 
 @[simp]
-theorem foldFreeM_pure {F : Type u → Type v} {α β : Type w}
-  (onValue : α → β)
-  (onEffect : {ι : Type u} → F ι → (ι → β) → β)
-  (a : α) : foldFreeM onValue onEffect (.pure a) = onValue a := rfl
+theorem foldFreeM_pure
+    (onValue : α → β)
+    (onEffect : {ι : Type u} → F ι → (ι → β) → β)
+    (a : α) : foldFreeM onValue onEffect (.pure a) = onValue a := rfl
 
 @[simp]
-theorem foldFreeM_liftBind {F : Type u → Type v} {α β : Type w}
-  (onValue : α → β)
-  (onEffect : {ι : Type u} → F ι → (ι → β) → β)
-  (op : F ι) (k : ι → FreeM F α) :
+theorem foldFreeM_liftBind
+    (onValue : α → β)
+    (onEffect : {ι : Type u} → F ι → (ι → β) → β)
+    (op : F ι) (k : ι → FreeM F α) :
     foldFreeM onValue onEffect (.liftBind op k)
-    = onEffect op (fun x => foldFreeM onValue onEffect (k x)) := rfl
+      = onEffect op (fun x => foldFreeM onValue onEffect (k x)) := rfl
 
 /--
 **Universal Property**: If `h : FreeM F α → β` satisfies:
@@ -77,15 +77,13 @@ theorem foldFreeM_liftBind {F : Type u → Type v} {α β : Type w}
 then `h` is equal to `foldFreeM onValue onEffect`.
 -/
 theorem foldFreeM_unique
-  {F : Type u → Type v} {α : Type w} {β : Type w}
-  (onValue : α → β)
-  (onEffect : {ι : Type u} → F ι → (ι → β) → β)
-  (h : FreeM F α → β)
-  (h_pure : ∀ a, h (.pure a) = onValue a)
-  (h_liftBind : ∀ {ι} (op : F ι) (k : ι → FreeM F α),
-    h (.liftBind op k) = onEffect op (fun x => h (k x))) :
-  h = foldFreeM onValue onEffect :=
-by
+    (onValue : α → β)
+    (onEffect : {ι : Type u} → F ι → (ι → β) → β)
+    (h : FreeM F α → β)
+    (h_pure : ∀ a, h (.pure a) = onValue a)
+    (h_liftBind : ∀ {ι} (op : F ι) (k : ι → FreeM F α),
+      h (.liftBind op k) = onEffect op (fun x => h (k x))) :
+    h = foldFreeM onValue onEffect := by
   funext x
   induction x with
   | pure a =>

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -659,7 +659,7 @@ theorem LTS.deterministic_tr_image_singleton [lts.Deterministic] :
 /-- In a deterministic LTS, any image is either a singleton or the empty set. -/
 @[scoped grind .]
 theorem LTS.deterministic_image_char [lts.Deterministic] (s : State) (μ : Label) :
-  (∃ s', lts.image s μ = { s' }) ∨ (lts.image s μ = ∅) := by grind
+    (∃ s', lts.image s μ = { s' }) ∨ (lts.image s μ = ∅) := by grind
 
 /-- In a deterministic LTS, the image of any state-label combination is finite. -/
 instance [lts.Deterministic] (s : State) (μ : Label) : Finite (lts.image s μ) := by
@@ -777,9 +777,9 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
 @[scoped grind →]
 theorem LTS.STrN.trans_τ
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
-  lts.STrN (n + m) s1 HasTau.τ s3 := by
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
+    lts.STrN (n + m) s1 HasTau.τ s3 := by
   cases h1
   case refl => grind
   case tr n1 sb sb' n2 hstr1 htr hstr2 =>
@@ -790,9 +790,9 @@ theorem LTS.STrN.trans_τ
 /-- Saturated transitions labelled by τ can be composed. -/
 @[scoped grind →]
 theorem LTS.STr.trans_τ
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
-  lts.STr s1 HasTau.τ s3 := by
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
+    lts.STr s1 HasTau.τ s3 := by
   obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
   obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
   have concN := LTS.STrN.trans_τ lts h1N h2N
@@ -801,10 +801,10 @@ theorem LTS.STr.trans_τ
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[scoped grind <=]
 theorem LTS.STrN.append
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n1 s1 μ s2)
-  (h2 : lts.STrN n2 s2 HasTau.τ s3) :
-  lts.STrN (n1 + n2) s1 μ s3 := by
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STrN n1 s1 μ s2)
+    (h2 : lts.STrN n2 s2 HasTau.τ s3) :
+    lts.STrN (n1 + n2) s1 μ s3 := by
   cases h1
   case refl => grind
   case tr n11 sb sb' n12 hstr1 htr hstr2 =>
@@ -816,11 +816,11 @@ theorem LTS.STrN.append
 /-- Saturated transitions can be composed (weighted version). -/
 @[scoped grind <=]
 theorem LTS.STrN.comp
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n1 s1 HasTau.τ s2)
-  (h2 : lts.STrN n2 s2 μ s3)
-  (h3 : lts.STrN n3 s3 HasTau.τ s4) :
-  lts.STrN (n1 + n2 + n3) s1 μ s4 := by
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STrN n1 s1 HasTau.τ s2)
+    (h2 : lts.STrN n2 s2 μ s3)
+    (h3 : lts.STrN n3 s3 HasTau.τ s4) :
+    lts.STrN (n1 + n2 + n3) s1 μ s4 := by
   cases h2
   case refl =>
     apply LTS.STrN.trans_τ lts h1 h3
@@ -833,11 +833,11 @@ theorem LTS.STrN.comp
 /-- Saturated transitions can be composed. -/
 @[scoped grind <=]
 theorem LTS.STr.comp
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STr s1 HasTau.τ s2)
-  (h2 : lts.STr s2 μ s3)
-  (h3 : lts.STr s3 HasTau.τ s4) :
-  lts.STr s1 μ s4 := by
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STr s1 HasTau.τ s2)
+    (h2 : lts.STr s2 μ s3)
+    (h3 : lts.STr s3 HasTau.τ s4) :
+    lts.STr s1 μ s4 := by
   obtain ⟨n1, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
   obtain ⟨n2, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
   obtain ⟨n3, h3N⟩ := (LTS.sTr_sTrN lts).1 h3
@@ -848,7 +848,7 @@ open scoped LTS.STr in
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 @[scoped grind _=_]
 theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
-  (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
+    (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
   ext s'
   apply Iff.intro <;> intro h
   case mp =>
@@ -894,9 +894,9 @@ def LTS.Divergent [HasTau Label] (lts : LTS State Label) (s : State) : Prop :=
 /-- If a trace is divergent, then any 'suffix' is also divergent. -/
 @[scoped grind ⇒]
 theorem LTS.divergentTrace_drop
-  [HasTau Label] {μs : ωSequence Label}
-  (h : DivergentTrace μs) (n : ℕ) :
-  DivergentTrace (μs.drop n) := by
+    [HasTau Label] {μs : ωSequence Label}
+    (h : DivergentTrace μs) (n : ℕ) :
+    DivergentTrace (μs.drop n) := by
   intro m
   simp only [DivergentTrace] at h
   simp only [ωSequence.get_fun, ωSequence.drop]

Cslib/Foundations/Semantics/LTS/Bisimulation.lean

@@ -86,14 +86,14 @@ def LTS.IsBisimulation (lts : LTS State Label) (r : State → State → Prop) :
 
 /-- Helper for following a transition by the first state in a pair of a `Bisimulation`. -/
 theorem LTS.IsBisimulation.follow_fst
-  (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s1 μ s1') :
-  ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' :=
+    (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s1 μ s1') :
+    ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' :=
   (hb hr μ).1 _ htr
 
 /-- Helper for following a transition by the second state in a pair of a `Bisimulation`. -/
 theorem LTS.IsBisimulation.follow_snd
-  (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s2 μ s2') :
-  ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2' :=
+    (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s2 μ s2') :
+    ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2' :=
   (hb hr μ).2 _ htr
 
 /-- Two states are bisimilar if they are related by some bisimulation. -/
@@ -130,14 +130,14 @@ theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1 := b
 /-- The composition of two bisimulations is a bisimulation. -/
 @[scoped grind .]
 theorem LTS.IsBisimulation.comp
-  (h1 : lts.IsBisimulation r1) (h2 : lts.IsBisimulation r2) :
+    (h1 : lts.IsBisimulation r1) (h2 : lts.IsBisimulation r2) :
   lts.IsBisimulation (Relation.Comp r1 r2) := by grind [Relation.Comp]
 
 open LTS in
 /-- Bisimilarity is transitive. -/
 @[scoped grind →]
 theorem Bisimilarity.trans
-  (h1 : s1 ~[lts] s2) (h2 : s2 ~[lts] s3) :
+    (h1 : s1 ~[lts] s2) (h2 : s2 ~[lts] s3) :
   s1 ~[lts] s3 := by
   obtain ⟨r1, _, _⟩ := h1
   obtain ⟨r2, _, _⟩ := h2
@@ -215,7 +215,7 @@ theorem Bisimilarity.largest_bisimulation (h : lts.IsBisimulation r) :
 /-- The union of bisimilarity with any bisimulation is bisimilarity. -/
 @[scoped grind =, simp]
 theorem Bisimilarity.gfp (r : State → State → Prop) (h : lts.IsBisimulation r) :
-  (Bisimilarity lts) ⊔ r = Bisimilarity lts := by
+    (Bisimilarity lts) ⊔ r = Bisimilarity lts := by
   funext s1 s2
   simp only [max, SemilatticeSup.sup, eq_iff_iff, or_iff_left_iff_imp]
   apply Bisimilarity.largest_bisimulation h
@@ -349,8 +349,8 @@ theorem LTS.IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) :
 /-- If two states are related by a bisimulation, they can mimic each other's multi-step
 transitions. -/
 theorem Bisimulation.bisim_trace
-  (hb : lts.IsBisimulation r) (hr : r s1 s2) :
-  ∀ μs s1', lts.MTr s1 μs s1' → ∃ s2', lts.MTr s2 μs s2' ∧ r s1' s2' := by
+    (hb : lts.IsBisimulation r) (hr : r s1 s2) :
+    ∀ μs s1', lts.MTr s1 μs s1' → ∃ s2', lts.MTr s2 μs s2' ∧ r s1' s2' := by
   intro μs
   induction μs generalizing s1 s2
   case nil =>
@@ -383,8 +383,8 @@ theorem Bisimulation.bisim_trace
 /-- Any bisimulation implies trace equivalence. -/
 @[scoped grind =>]
 theorem LTS.IsBisimulation.traceEq
-  (hb : lts.IsBisimulation r) (hr : r s1 s2) :
-  s1 ~tr[lts] s2 := by
+    (hb : lts.IsBisimulation r) (hr : r s1 s2) :
+    s1 ~tr[lts] s2 := by
   funext μs
   simp only [eq_iff_iff]
   constructor
@@ -424,7 +424,8 @@ private inductive BisimMotTr : ℕ → Char → ℕ → Prop where
 /-- In general, trace equivalence is not a bisimulation (extra conditions are needed, see for
 example `Bisimulation.deterministic_trace_eq_is_bisim`). -/
 theorem Bisimulation.traceEq_not_bisim :
-  ∃ (State : Type) (Label : Type) (lts : LTS State Label), ¬(lts.IsBisimulation (TraceEq lts)) := by
+    ∃ (State : Type) (Label : Type) (lts : LTS State Label),
+      ¬(lts.IsBisimulation (TraceEq lts)) := by
   exists ℕ
   exists Char
   let lts := LTS.mk BisimMotTr
@@ -810,9 +811,9 @@ def LTS.IsSWBisimulation [HasTau Label] (lts : LTS State Label) (r : State → S
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (first component, weighted version). -/
 theorem SWBisimulation.follow_internal_fst_n
-  [HasTau Label] {lts : LTS State Label}
-  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s1 HasTau.τ s1') :
-  ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
+    [HasTau Label] {lts : LTS State Label}
+    (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s1 HasTau.τ s1') :
+    ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
   cases n
   case zero =>
     cases hstrN
@@ -837,9 +838,9 @@ theorem SWBisimulation.follow_internal_fst_n
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (second component, weighted version). -/
 theorem SWBisimulation.follow_internal_snd_n
-  [HasTau Label] {lts : LTS State Label}
-  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s2 HasTau.τ s2') :
-  ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
+    [HasTau Label] {lts : LTS State Label}
+    (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s2 HasTau.τ s2') :
+    ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
   cases n
   case zero =>
     cases hstrN
@@ -864,26 +865,26 @@ theorem SWBisimulation.follow_internal_snd_n
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (first component). -/
 theorem SWBisimulation.follow_internal_fst
-  [HasTau Label] {lts : LTS State Label}
-  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s1 HasTau.τ s1') :
-  ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
+    [HasTau Label] {lts : LTS State Label}
+    (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s1 HasTau.τ s1') :
+    ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
   obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr
   apply SWBisimulation.follow_internal_fst_n hswb hr hstrN
 
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (second component). -/
 theorem SWBisimulation.follow_internal_snd
-  [HasTau Label] {lts : LTS State Label}
-  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s2 HasTau.τ s2') :
-  ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
+    [HasTau Label] {lts : LTS State Label}
+    (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s2 HasTau.τ s2') :
+    ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
   obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr
   apply SWBisimulation.follow_internal_snd_n hswb hr hstrN
 
 /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`.
 This formalises lemma 4.2.10 in [Sangiorgi2011]. -/
 theorem LTS.isWeakBisimulation_iff_isSWBisimulation
-  [HasTau Label] {lts : LTS State Label} :
-  lts.IsWeakBisimulation r ↔ lts.IsSWBisimulation r := by
+    [HasTau Label] {lts : LTS State Label} :
+    lts.IsWeakBisimulation r ↔ lts.IsSWBisimulation r := by
   apply Iff.intro
   case mp =>
     intro h s1 s2 hr μ
@@ -959,8 +960,8 @@ theorem WeakBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State)
 
 /-- The inverse of a weak bisimulation is a weak bisimulation. -/
 theorem WeakBisimulation.inv [HasTau Label] (lts : LTS State Label)
-  (r : State → State → Prop) (h : lts.IsWeakBisimulation r) :
-  lts.IsWeakBisimulation (flip r) := by
+    (r : State → State → Prop) (h : lts.IsWeakBisimulation r) :
+    lts.IsWeakBisimulation (flip r) := by
   grind [WeakBisimulation.toSwBisimulation, LTS.IsSWBisimulation,
     flip, SWBisimulation.toWeakBisimulation]
 
@@ -973,19 +974,20 @@ theorem WeakBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈
 
 /-- The composition of two weak bisimulations is a weak bisimulation. -/
 theorem WeakBisimulation.comp
-  [HasTau Label]
-  (lts : LTS State Label)
-  (r1 r2 : State → State → Prop) (h1 : lts.IsWeakBisimulation r1) (h2 : lts.IsWeakBisimulation r2) :
-  lts.IsWeakBisimulation (Relation.Comp r1 r2) := by
+    [HasTau Label]
+    (lts : LTS State Label)
+    (r1 r2 : State → State → Prop)
+    (h1 : lts.IsWeakBisimulation r1) (h2 : lts.IsWeakBisimulation r2) :
+    lts.IsWeakBisimulation (Relation.Comp r1 r2) := by
   simp_all only [LTS.IsWeakBisimulation]
   exact h1.comp h2
 
 /-- The composition of two sw-bisimulations is an sw-bisimulation. -/
 theorem SWBisimulation.comp
-  [HasTau Label]
-  (lts : LTS State Label)
-  (r1 r2 : State → State → Prop) (h1 : lts.IsSWBisimulation r1) (h2 : lts.IsSWBisimulation r2) :
-  lts.IsSWBisimulation (Relation.Comp r1 r2) := by
+    [HasTau Label]
+    (lts : LTS State Label)
+    (r1 r2 : State → State → Prop) (h1 : lts.IsSWBisimulation r1) (h2 : lts.IsSWBisimulation r2) :
+    lts.IsSWBisimulation (Relation.Comp r1 r2) := by
   simp_all only [LTS.isWeakBisimulation_iff_isSWBisimulation.symm]
   apply WeakBisimulation.comp lts r1 r2 h1 h2
 
@@ -1003,11 +1005,10 @@ theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State}
 
 /-- Weak bisimilarity is an equivalence relation. -/
 theorem WeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} :
-  Equivalence (WeakBisimilarity lts) := {
-    refl := WeakBisimilarity.refl lts
-    symm := WeakBisimilarity.symm lts
-    trans := WeakBisimilarity.trans lts
-  }
+    Equivalence (WeakBisimilarity lts) where
+  refl := WeakBisimilarity.refl lts
+  symm := WeakBisimilarity.symm lts
+  trans := WeakBisimilarity.trans lts
 
 end WeakBisimulation
 

Cslib/Foundations/Semantics/LTS/Simulation.lean

@@ -74,8 +74,8 @@ theorem Similarity.refl (s : State) : s ≤[lts] s := by
 
 /-- The composition of two simulations is a simulation. -/
 theorem Simulation.comp
-  (r1 r2 : State → State → Prop) (h1 : Simulation lts r1) (h2 : Simulation lts r2) :
-  Simulation lts (Relation.Comp r1 r2) := by
+    (r1 r2 : State → State → Prop) (h1 : Simulation lts r1) (h2 : Simulation lts r2) :
+    Simulation lts (Relation.Comp r1 r2) := by
   simp_all only [Simulation]
   intro s1 s2 hrc μ s1' htr
   rcases hrc with ⟨sb, hr1, hr2⟩