/-
  GENERATED from `Bigraph/Problems/ChIILean.lean` by `scripts/blank_exercises.py`;
  do not edit.  Replace each `sorry` by a proof.  The solutions are in
  `Bigraph/Problems/ChIILean.lean`, and the problems in `docs/problems-II.html`.
-/
import Bigraph.Problems.ChII

set_option autoImplicit false

namespace Bigraph.Problems.ChII

open Bigraph Bg Bigraph.CCSFull Bigraph.Dynamics
open Locus.CCSFull (Chan Act Proc Sum SC Red InSum co NamesIn)

/-- **Problem II.23(a) (Milner's Exercise 7.1, in Lean).** `G` is not active:
    its second site lies inside the passive `B`. -/
theorem G_not_active : ¬ G.Active := sorry

/-- **Problem II.23(b) ⋆.** `G ◦ F` is active. -/
theorem GF_active : (G ◦ F).Active := sorry

/-- **Problem II.24 (A rule in two active contexts).** A rule in the context
    `D`, then in `E`, reacts: Theorem II.1 for contexts that compose on the
    nose. -/
theorem react_two_contexts {Ctrl Name : Type} {S : Sig Ctrl} [DecidableEq Name]
    {R : Rules S Name} {ρ : GroundRule S Name} (h : R ρ) {K L : Iface Name}
    (D : Bg S ρ.J K) (E : Bg S K L) (hD : D.Active) (hE : E.Active) :
    React R ⟪E ◦ (D ◦ ρ.redex)⟫ ⟪E ◦ (D ◦ ρ.reactum)⟫ := sorry

/-- `(ā.0 | b̄.0) | a.0`: the partners are not side by side. -/
def pApart : Proc := .par (.par (pre0 (.snd a)) (pre0 (.snd b))) (pre0 (.rcv a))

/-- The reduct, `(0 | 0) | b̄.0`. -/
def qApart : Proc := .par (.par .nil .nil) (pre0 (.snd b))

/-- **Problem II.25(a) (A reduction that needs congruence).**
    `(ā.0 | b̄.0) | a.0` reduces to `(0 | 0) | b̄.0`. -/
theorem red_apart : Red pApart qApart := sorry

/-- **Problem II.25(b).** So its agent reacts. -/
theorem react_apart :
    React ccsRules (agent Xabc ρ0 pApart (by decide)) (agent Xabc ρ0 qApart (by decide)) := sorry

/-- `ȳ.0`, a send on the innermost binder, with no binder around it. -/
def pDangling : Proc := pre0 (.snd y)

/-- **Problem II.26 (Not closed).** A process whose channel is a dangling
    index is not closed (Definition II.9). -/
theorem dangling_not_closed : ¬ Bigraph.CCSFull.Closed pDangling := sorry

end Bigraph.Problems.ChII