locus: Blueprint

4.2. Bisimilarity is a congruence🔗

Definition4.2.1
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 4.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsfrom source

A wide reactive system is a precategory with supports, a width for each interface, and a set of ground rules (r, r') closed under translation; agents are the arrows from the origin. A transition a \xrightarrow{L}_{\lambda} a' is an idem pushout \mathrm{IPO}(a, r; L, D) for a rule (r, r') and an active D, with a' \bumpeq D \circ r' and \lambda the set of roots in the image of the width map of D. Bisimilarity a \sim b is the largest symmetric relation in which every a \xrightarrow{L}_{\lambda} a' with L \circ b defined is matched by some b \xrightarrow{L}_{\lambda} b'. The system has RPOs when every span with a bound has an RPO relative to it.

Lean code for Definition4.2.1●4 definitions
  • structure(extends 2, 31 fields)defined in Bigraph/Concrete/Wide.lean
    complete
    structure WRS.{u, v} : Type (max (u + 1) (v + 1))
    structure WRS.{u, v} : Type (max (u + 1) (v + 1))
    **A wide reactive system** (TR-580 Defs 4.1, 4.3), given by its ground
rules.

    Extends

    • SPreCat

    Fields

    Obj : Type u
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    Hom : self.Obj → self.Obj → Type v
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    id : (a : self.Obj) → self.Hom a a
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    Comp : {a b c : self.Obj} → self.Hom b c → self.Hom a b → self.Hom a c → Prop
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    comp_fun : ∀ {a b c : self.Obj} {g : self.Hom b c} {f : self.Hom a b} {h h' : self.Hom a c}, g ◦ f ≃ h → g ◦ f ≃ h' → h = h'
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    id_left : ∀ {a b : self.Obj} (f : self.Hom a b), self.id b ◦ f ≃ f
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    id_right : ∀ {a b : self.Obj} (f : self.Hom a b), f ◦ self.id a ≃ f
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    assoc : ∀ {a b c d : self.Obj} (f : self.Hom a b) (g : self.Hom b c) (h : self.Hom c d) (x : self.Hom a d),
  (∃ gf, g ◦ f ≃ gf ∧ h ◦ gf ≃ x) ↔ ∃ hg, h ◦ g ≃ hg ∧ hg ◦ f ≃ x
    Inherited from
    1. Bigraph.Concrete.SPreCat
    2. Bigraph.Concrete.PreCat
    supp : {a b : self.Obj} → self.Hom a b → Nat → Bool
    Inherited from
    1. Bigraph.Concrete.SPreCat
    supp_bound : ∀ {a b : self.Obj} (f : self.Hom a b), ∃ N, ∀ (v : Nat), self.supp f v = true → v < N
    Inherited from
    1. Bigraph.Concrete.SPreCat
    defined_iff : ∀ {a b c : self.Obj} (g : self.Hom b c) (f : self.Hom a b),
  (∃ h, g ◦ f ≃ h) ↔ ∀ (v : Nat), ¬(self.supp g v = true ∧ self.supp f v = true)
    Inherited from
    1. Bigraph.Concrete.SPreCat
    supp_comp : ∀ {a b c : self.Obj} {g : self.Hom b c} {f : self.Hom a b} {h : self.Hom a c},
  g ◦ f ≃ h → ∀ (v : Nat), self.supp h v = true ↔ self.supp g v = true ∨ self.supp f v = true
    Inherited from
    1. Bigraph.Concrete.SPreCat
    supp_id : ∀ (a : self.Obj) (v : Nat), self.supp (self.id a) v = false
    Inherited from
    1. Bigraph.Concrete.SPreCat
    tr : {a b : self.Obj} → Perm → self.Hom a b → self.Hom a b
    Inherited from
    1. Bigraph.Concrete.SPreCat
    tr_comp : ∀ {a b c : self.Obj} (π : Perm) {g : self.Hom b c} {f : self.Hom a b} {h : self.Hom a c},
  g ◦ f ≃ h → self.tr π g ◦ self.tr π f ≃ self.tr π h
    Inherited from
    1. Bigraph.Concrete.SPreCat
    tr_fix : ∀ {a b : self.Obj} (π : Perm) (f : self.Hom a b), (∀ (v : Nat), self.supp f v = true → π.f v = v) → self.tr π f = f
    Inherited from
    1. Bigraph.Concrete.SPreCat
    tr_mul : ∀ {a b : self.Obj} (π σ : Perm) (f : self.Hom a b), self.tr π (self.tr σ f) = self.tr (π.mul σ) f
    Inherited from
    1. Bigraph.Concrete.SPreCat
    supp_tr : ∀ {a b : self.Obj} (π : Perm) (f : self.Hom a b) (v : Nat), self.supp (self.tr π f) v = self.supp f (π.g v)
    Inherited from
    1. Bigraph.Concrete.SPreCat
    width : self.Obj → Nat
    The width of an interface. 
    wid : {a b : self.Obj} → self.Hom a b → Fin (self.width a) → Fin (self.width b)
    The width of an arrow: the root each site lies in. 
    wid_id : ∀ (a : self.Obj) (i : Fin (self.width a)), self.wid (self.id a) i = i
    wid_comp : ∀ {a b c : self.Obj} {g : self.Hom b c} {f : self.Hom a b} {h : self.Hom a c},
  g ◦ f ≃ h → ∀ (i : Fin (self.width a)), self.wid h i = self.wid g (self.wid f i)
    wid_tr : ∀ {a b : self.Obj} (π : Perm) (f : self.Hom a b) (i : Fin (self.width a)), self.wid (self.tr π f) i = self.wid f i
    act : {a b : self.Obj} → self.Hom a b → Fin (self.width a) → Prop
    The activity map: the sites at which an arrow is active. 
    act_id : ∀ (a : self.Obj) (i : Fin (self.width a)), self.act (self.id a) i
    Def 4.3 (1). 
    act_comp : ∀ {a b c : self.Obj} {g : self.Hom b c} {f : self.Hom a b} {h : self.Hom a c},
  g ◦ f ≃ h → ∀ (i : Fin (self.width a)), self.act h i ↔ self.act f i ∧ self.act g (self.wid f i)
    Def 4.3 (2): `act(D ∘ C) = act(C) ∩ width(C)⁻¹(act(D))`. 
    act_tr : ∀ {a b : self.Obj} (π : Perm) (f : self.Hom a b) (i : Fin (self.width a)), self.act (self.tr π f) i ↔ self.act f i
    origin : self.Obj
    The origin `ε`; agents are its arrows. 
    origin_width : self.width self.origin = 0
    Rule : {J : self.Obj} → self.Hom self.origin J → self.Hom self.origin J → Prop
    The ground reaction rules, closed under support translation. 
    rule_tr : ∀ {J : self.Obj} {r r' : self.Hom self.origin J} (π σ : Perm), self.Rule r r' → self.Rule (self.tr π r) (self.tr σ r')
  • defdefined in Bigraph/Concrete/Wide.lean
    complete
    def Trans.{u, v} (W : WRS) {I J : W.Obj} (a : W.Hom W.origin I)
  (L : W.Hom I J) (loc : Fin (W.width J) → Prop)
  (a' : W.Hom W.origin J) : Prop
    def Trans.{u, v} (W : WRS) {I J : W.Obj}
  (a : W.Hom W.origin I) (L : W.Hom I J)
  (loc : Fin (W.width J) → Prop)
  (a' : W.Hom W.origin J) : Prop
    **A standard transition** `a —L▷_λ a'` (TR-580 Def 5.1, minimal): an
IPO `L ∘ a = D ∘ r` for a ground rule `(r, r')` and an active `D`, at the
location `λ = width(D)(m)`, with `a' ≏ D ∘ r'`.
  • defdefined in Bigraph/Concrete/Wide.lean
    complete
    def Bisim.{u, v} (W : WRS) {I : W.Obj} (a b : W.Hom W.origin I) : Prop
    def Bisim.{u, v} (W : WRS) {I : W.Obj}
  (a b : W.Hom W.origin I) : Prop
    **Wide bisimilarity** `∼`.
  • defdefined in Bigraph/Concrete/Wide.lean
    complete
    def HasRPOs.{u, v} (W : WRS) : Prop
    def HasRPOs.{u, v} (W : WRS) : Prop
    **Enough RPOs**: every pair with a bound has an RPO relative to it.
Theorem4.2.2
Statement uses 2
Statement dependency previews
Preview
Theorem 4.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 4.2.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

In a wide reactive system with RPOs, bisimilarity is a congruence (TR-580 Thm 5.5): for every context C with C \circ a_0 and C \circ a_1 defined,

a_0 \sim a_1 \;\Longrightarrow\; C \circ a_0 \sim C \circ a_1 .

Lean code for Theorem4.2.2●1 theorem
  • theoremdefined in Bigraph/Concrete/Wide.lean
    complete
    theorem bisim_congr.{u, v} {W : WRS} (hR : W.HasRPOs) {I J : W.Obj}
  {a₀ a₁ : W.Hom W.origin I} (C : W.Hom I J) {x₀ x₁ : W.Hom W.origin J}
  (h : a₀ ∼ a₁) (h₀ : C ◦ a₀ ≃ x₀) (h₁ : C ◦ a₁ ≃ x₁) : x₀ ∼ x₁
    theorem bisim_congr.{u, v} {W : WRS}
  (hR : W.HasRPOs) {I J : W.Obj}
  {a₀ a₁ : W.Hom W.origin I}
  (C : W.Hom I J)
  {x₀ x₁ : W.Hom W.origin J} (h : a₀ ∼ a₁)
  (h₀ : C ◦ a₀ ≃ x₀) (h₁ : C ◦ a₁ ≃ x₁) :
  x₀ ∼ x₁
    **TR-580 Theorem 5.5 (congruence of wide bisimilarity)**: in a wide
reactive system with RPOs, if `a₀ ∼ a₁` then `C ∘ a₀ ∼ C ∘ a₁`.
Theorem4.2.3
Statement uses 2
Statement dependency previews
Preview
Theorem 4.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Concrete bigraphs with any set of ground rules closed under translation form a wide reactive system with RPOs, so (TR-580 Cor 12.4), for C \circ a_0 and C \circ a_1 defined,

a_0 \sim a_1 \;\Longrightarrow\; C \circ a_0 \sim C \circ a_1 .

The same holds for concrete binding bigraphs: bigraphs over binding interfaces that obey the scope rule and link every binding port to an edge.

Rests on NEW: BBig, Perm; not audited: BBig.tr, BIGW, Big.

Lean code for Theorem4.2.3●3 theorems
  • theoremdefined in Bigraph/Concrete/BigCongr.lean
    complete
    theorem bigw_hasRPOs {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm),
      R r r' → R (Big.tr π r) (Big.tr σ r')) :
  (BIGW S (fun {J} => R) ⋯).HasRPOs
    theorem bigw_hasRPOs {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  (R :
    {J : Face} →
      Big S Face.origin J →
        Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face}
      {r r' : Big S Face.origin J}
      (π σ : Perm),
      R r r' →
        R (Big.tr π r) (Big.tr σ r')) :
  (BIGW S (fun {J} => R) ⋯).HasRPOs
    **Bigraphs have RPOs**, in the form Theorem 5.5 asks for.
  • theoremdefined in Bigraph/Concrete/BigCongr.lean
    complete
    theorem big_bisim_congr {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm),
      R r r' → R (Big.tr π r) (Big.tr σ r'))
  {I J : Face} {a₀ a₁ : Big S Face.origin I} (C : Big S I J)
  {x₀ x₁ : Big S Face.origin J} (h : a₀ ∼ a₁) (h₀ : C ◦ a₀ ≃ x₀)
  (h₁ : C ◦ a₁ ≃ x₁) : x₀ ∼ x₁
    theorem big_bisim_congr {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  (R :
    {J : Face} →
      Big S Face.origin J →
        Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face}
      {r r' : Big S Face.origin J}
      (π σ : Perm),
      R r r' →
        R (Big.tr π r) (Big.tr σ r'))
  {I J : Face}
  {a₀ a₁ : Big S Face.origin I}
  (C : Big S I J)
  {x₀ x₁ : Big S Face.origin J}
  (h : a₀ ∼ a₁) (h₀ : C ◦ a₀ ≃ x₀)
  (h₁ : C ◦ a₁ ≃ x₁) : x₀ ∼ x₁
    **TR-580 Corollary 12.4 (congruence of wide bisimilarity)**, for pure
bigraphs: in any concrete BRS, wide bisimilarity of agents is a
congruence.
  • theoremdefined in Bigraph/Concrete/BindingRPO.lean
    complete
    theorem bbg_bisim_congr {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {B : Bigraph.Bg.BindSig S}
  (R :
    {J : BFace} → BBig B BFace.origin J → BBig B BFace.origin J → Prop)
  (hR :
    ∀ {J : BFace} {r r' : BBig B BFace.origin J} (π σ : Perm),
      R r r' → R (BBig.tr π r) (BBig.tr σ r'))
  {I J : BFace} {a₀ a₁ : BBig B BFace.origin I} (C : BBig B I J)
  {x₀ x₁ : BBig B BFace.origin J} (h : a₀ ∼ a₁) (h₀ : C ◦ a₀ ≃ x₀)
  (h₁ : C ◦ a₁ ≃ x₁) : x₀ ∼ x₁
    theorem bbg_bisim_congr {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {B : Bigraph.Bg.BindSig S}
  (R :
    {J : BFace} →
      BBig B BFace.origin J →
        BBig B BFace.origin J → Prop)
  (hR :
    ∀ {J : BFace}
      {r r' : BBig B BFace.origin J}
      (π σ : Perm),
      R r r' →
        R (BBig.tr π r) (BBig.tr σ r'))
  {I J : BFace}
  {a₀ a₁ : BBig B BFace.origin I}
  (C : BBig B I J)
  {x₀ x₁ : BBig B BFace.origin J}
  (h : a₀ ∼ a₁) (h₀ : C ◦ a₀ ≃ x₀)
  (h₁ : C ◦ a₁ ≃ x₁) : x₀ ∼ x₁
    **TR-580 Corollary 12.4 (congruence of wide bisimilarity) for binding
bigraphs**: in any concrete binding BRS, wide bisimilarity of agents is
a congruence.
Theorem4.2.4
uses 1used by 1✓L∃∀N

The congruence transfers to abstract bigraphs, the classes [G] under \Bumpeq (TR-580 Cor 12.6). If every redex is lean (has no idle edge) and has no idle names, then for concrete agents a, b of one interface, and for abstract bigraphs p, q, G over natural-number names with G \circ p and G \circ q defined,

a \sim b \iff [a] \sim [b], \qquad p \sim q \;\Longrightarrow\; G \circ p \sim G \circ q ,

where the transitions of abstract bigraphs are the images of the concrete ones. The second statement holds in the quotient by \Bumpeq and in the abstract bigraphs of the Bigraphs chapter.

Rests on NEW: Big.LeanEquiv, Perm, WRS.RBisim, WRS.Rep; not audited: BIGW, Big, absRep, leanCong.

Lean code for Theorem4.2.4●3 theorems
  • theoremdefined in Bigraph/Concrete/BigCongr.lean
    complete
    theorem lean_congr {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm),
      R r r' → R (Big.tr π r) (Big.tr σ r'))
  (hRl :
    ∀ {J : Face} {r r' : Big S Face.origin J},
      R r r' → r.IsLean ∧ r.NoIdleNames)
  {I J : Face}
  {p q :
    (BIGW S (fun {J} => R) ⋯).Q (leanCong (fun {J} => R) ⋯) Face.origin
      I}
  (G : (BIGW S (fun {J} => R) ⋯).Q (leanCong (fun {J} => R) ⋯) I J)
  {x y :
    (BIGW S (fun {J} => R) ⋯).Q (leanCong (fun {J} => R) ⋯) Face.origin
      J}
  (h : (BIGW S (fun {J} => R) ⋯).QBisim (leanCong (fun {J} => R) ⋯) p q)
  (hx :
    (BIGW S (fun {J} => R) ⋯).QComp (leanCong (fun {J} => R) ⋯) G p x)
  (hy :
    (BIGW S (fun {J} => R) ⋯).QComp (leanCong (fun {J} => R) ⋯) G q y) :
  (BIGW S (fun {J} => R) ⋯).QBisim (leanCong (fun {J} => R) ⋯) x y
    theorem lean_congr {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  (R :
    {J : Face} →
      Big S Face.origin J →
        Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face}
      {r r' : Big S Face.origin J}
      (π σ : Perm),
      R r r' →
        R (Big.tr π r) (Big.tr σ r'))
  (hRl :
    ∀ {J : Face}
      {r r' : Big S Face.origin J},
      R r r' → r.IsLean ∧ r.NoIdleNames)
  {I J : Face}
  {p q :
    (BIGW S (fun {J} => R) ⋯).Q
      (leanCong (fun {J} => R) ⋯)
      Face.origin I}
  (G :
    (BIGW S (fun {J} => R) ⋯).Q
      (leanCong (fun {J} => R) ⋯) I J)
  {x y :
    (BIGW S (fun {J} => R) ⋯).Q
      (leanCong (fun {J} => R) ⋯)
      Face.origin J}
  (h :
    (BIGW S (fun {J} => R) ⋯).QBisim
      (leanCong (fun {J} => R) ⋯) p q)
  (hx :
    (BIGW S (fun {J} => R) ⋯).QComp
      (leanCong (fun {J} => R) ⋯) G p x)
  (hy :
    (BIGW S (fun {J} => R) ⋯).QComp
      (leanCong (fun {J} => R) ⋯) G q y) :
  (BIGW S (fun {J} => R) ⋯).QBisim
    (leanCong (fun {J} => R) ⋯) x y
    **TR-580 Corollary 12.6 (2)** in the quotient by `≎`, with Milner's
condition on redexes: bisimilarity of lean-support classes is a
congruence.  (Part (1) is `lean_transfer`.)
  • theoremdefined in Bigraph/Concrete/Cor126.lean
    complete
    theorem cor_12_6 {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm),
      R r r' → R (Big.tr π r) (Big.tr σ r'))
  (hRl :
    ∀ {J : Face} {r r' : Big S Face.origin J},
      R r r' → r.IsLean ∧ r.NoIdleNames)
  {I : Face} (a b : Big S Face.origin I) :
  a ∼ b ↔ WRS.RBisim (absRep (fun {J} => R) ⋯) a.abs b.abs
    theorem cor_12_6 {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  (R :
    {J : Face} →
      Big S Face.origin J →
        Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face}
      {r r' : Big S Face.origin J}
      (π σ : Perm),
      R r r' →
        R (Big.tr π r) (Big.tr σ r'))
  (hRl :
    ∀ {J : Face}
      {r r' : Big S Face.origin J},
      R r r' → r.IsLean ∧ r.NoIdleNames)
  {I : Face} (a b : Big S Face.origin I) :
  a ∼ b ↔
    WRS.RBisim (absRep (fun {J} => R) ⋯)
      a.abs b.abs
    **TR-580 Corollary 12.6 (1)**, in the library's `Abstract`: with every
redex lean and without idle names, two agents are bisimilar iff their
abstract classes are.
  • theoremdefined in Bigraph/Concrete/Cor126.lean
    complete
    theorem cor_12_6_congr {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm),
      R r r' → R (Big.tr π r) (Big.tr σ r'))
  (hRl :
    ∀ {J : Face} {r r' : Big S Face.origin J},
      R r r' → r.IsLean ∧ r.NoIdleNames)
  {p q G x y : Bigraph.Bg.Abstract S Nat}
  (h : WRS.RBisim (absRep (fun {J} => R) ⋯) p q)
  (hx : G.comp p = some x) (hy : G.comp q = some y) :
  WRS.RBisim (absRep (fun {J} => R) ⋯) x y
    theorem cor_12_6_congr {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  (R :
    {J : Face} →
      Big S Face.origin J →
        Big S Face.origin J → Prop)
  (hR :
    ∀ {J : Face}
      {r r' : Big S Face.origin J}
      (π σ : Perm),
      R r r' →
        R (Big.tr π r) (Big.tr σ r'))
  (hRl :
    ∀ {J : Face}
      {r r' : Big S Face.origin J},
      R r r' → r.IsLean ∧ r.NoIdleNames)
  {p q G x y : Bigraph.Bg.Abstract S Nat}
  (h :
    WRS.RBisim (absRep (fun {J} => R) ⋯) p
      q)
  (hx : G.comp p = some x)
  (hy : G.comp q = some y) :
  WRS.RBisim (absRep (fun {J} => R) ⋯) x y
    **TR-580 Corollary 12.6 (2)**, in the library's `Abstract`: bisimilarity
of abstract bigraphs is a congruence.
Theorem4.2.5
uses 1used by 0✓L∃∀N

REFUTED: the transfer for lean redexes that may have idle names, as TR-580 Prop 12.5 and Cor 12.6 state it. With the rule taking a K-atom to an L-atom under the face \langle 1, \{x\} \rangle, nothing being linked to x, all redexes are lean and have the idle name x, and for b a K-atom of face \langle 1, \emptyset \rangle and a the same with one idle edge,

a \Bumpeq b \;\text{ but }\; a \not\sim b .

Rests on NEW: Big.LeanEquiv, Perm; not audited: Big, IdleNameCounter.Ctl, IdleNameCounter.J1, IdleNameCounter.N0, IdleNameCounter.R, IdleNameCounter.W, IdleNameCounter.a, IdleNameCounter.b and 1 more.

Lean code for Theorem4.2.5●3 theorems
  • theoremdefined in Bigraph/Concrete/IdleNameCounter.lean
    complete
    theorem leanEquiv_not_bisim :
  IdleNameCounter.a ≎ IdleNameCounter.b ∧
    ¬IdleNameCounter.a ∼ IdleNameCounter.b
    theorem leanEquiv_not_bisim :
  IdleNameCounter.a ≎ IdleNameCounter.b ∧
    ¬IdleNameCounter.a ∼ IdleNameCounter.b
    **The counterexample**: `a ≎ b` but `a ≁ b`, so lean-support equivalent
agents need not be bisimilar when a lean redex has an idle name; TR-580
Cor 12.6(1) needs Milner's further condition.
  • theoremdefined in Bigraph/Concrete/IdleNameCounter.lean
    complete
    theorem redex_lean {J : Face} {r r' : Big IdleNameCounter.sig Face.origin J} :
  IdleNameCounter.R r r' → r.IsLean
    theorem redex_lean {J : Face}
  {r r' :
    Big IdleNameCounter.sig Face.origin
      J} :
  IdleNameCounter.R r r' → r.IsLean
    **Every redex is lean**: it has no edges at all.
  • theoremdefined in Bigraph/Concrete/IdleNameCounter.lean
    complete
    theorem redex_idle_name : ∃ r r', IdleNameCounter.R r r' ∧ ¬r.NoIdleNames
    theorem redex_idle_name :
  ∃ r r',
    IdleNameCounter.R r r' ∧
      ¬r.NoIdleNames
    **A redex has an idle name**: nothing in `r₀` is linked to the name `0`.