locus: Blueprint

7.5. Tracked logic🔗

Theorem7.5.1
Statement uses 2
Statement dependency previews
Preview
Definition 7.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 7.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The tracked logic adds quantifiers over the nodes and links present; a valuation \sigma of the variables is carried along each reaction by the map recording which nodes and edges survive it (after Gadducci, Laretto and Trotta, Specification and verification of a linear-time temporal logic for graph transformation, 2023; Distefano, Rensink and Katoen, Model checking birth and death, 2002). For a passing tracked certificate c and a listed state s_i, a true verdict is sound,

\mathrm{check}(c, \varphi, i, \sigma) = \mathrm{true} \;\Longrightarrow\; \llbracket s_i \rrbracket \models_\sigma \varphi ,

for every \varphi without box modalities under no hypothesis on the rules, and for every \varphi when the rules satisfy G1 and no redex has an idle edge. Completeness of the tracked checker is OPEN.

Rests on NEW: BigraphSim.BD.outFace, BigraphSim.Par, PAtom, PForm, PSat, RuleG.g1, TrRule.rules, noIdleB; not audited: PForm.Ex.

Lean code for Theorem7.5.1●4 declarations
  • inductive(15 constructors, 2 parameters)defined in Logic/TrackLogic.lean
    complete
    inductive PForm (α Ctrl : Type) : Type
    inductive PForm (α Ctrl : Type) : Type
    **Tracked formulas** (positive normal form; named first-order variables,
de Bruijn fixpoint variables).

    Constructors

    atom {α Ctrl : Type} (p : PAtom Ctrl) : PForm α Ctrl
    natom {α Ctrl : Type} (p : PAtom Ctrl) : PForm α Ctrl
    and {α Ctrl : Type} (φ ψ : PForm α Ctrl) : PForm α Ctrl
    or {α Ctrl : Type} (φ ψ : PForm α Ctrl) : PForm α Ctrl
    exN {α Ctrl : Type} (x : Nat) (φ : PForm α Ctrl) :
  PForm α Ctrl
    allN {α Ctrl : Type} (x : Nat) (φ : PForm α Ctrl) :
  PForm α Ctrl
    exL {α Ctrl : Type} (x : Nat) (φ : PForm α Ctrl) :
  PForm α Ctrl
    allL {α Ctrl : Type} (x : Nat) (φ : PForm α Ctrl) :
  PForm α Ctrl
    dia {α Ctrl : Type} (t : Option α) (φ : PForm α Ctrl) :
  PForm α Ctrl
    box {α Ctrl : Type} (t : Option α) (φ : PForm α Ctrl) :
  PForm α Ctrl
    diaA {α Ctrl : Type} (φ : PForm α Ctrl) : PForm α Ctrl
    boxA {α Ctrl : Type} (φ : PForm α Ctrl) : PForm α Ctrl
    var {α Ctrl : Type} (k : Nat) : PForm α Ctrl
    mu {α Ctrl : Type} (φ : PForm α Ctrl) : PForm α Ctrl
    nu {α Ctrl : Type} (φ : PForm α Ctrl) : PForm α Ctrl
  • defdefined in Logic/TrackLogic.lean
    complete
    def PSat {α : Type} [DecidableEq α] {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) (trs : List (TrRule α Ctrl)) {J : Face} :
  (Nat → BigH S Face.origin J → PVal → Prop) →
    BigH S Face.origin J → PVal → PForm α Ctrl → Prop
    def PSat {α : Type} [DecidableEq α]
  {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl)
  (trs : List (TrRule α Ctrl))
  {J : Face} :
  (Nat →
      BigH S Face.origin J →
        PVal → Prop) →
    BigH S Face.origin J →
      PVal → PForm α Ctrl → Prop
    **The library meaning** of a tracked formula, over tracked library
reactions `TrReact`. Fixpoint variables denote predicates on (agent,
valuation).
  • theoremdefined in Logic/TrackEvalSound.lean
    complete
    theorem trackSound {Ctrl : Type} [DecidableEq Ctrl] (S : Bigraph.Sig Ctrl)
  (α : Type) [DecidableEq α] : TrackSoundStatement S α
    theorem trackSound {Ctrl : Type}
  [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) (α : Type)
  [DecidableEq α] :
  TrackSoundStatement S α
    **Soundness of the tracked checker on the existential fragment, PROVED.**
  • theoremdefined in Logic/TrackFullSound.lean
    complete
    theorem trackSoundAll {Ctrl : Type} [DecidableEq Ctrl] (S : Bigraph.Sig Ctrl)
  (α : Type) [DecidableEq α] : TrackSoundAllStatement S α
    theorem trackSoundAll {Ctrl : Type}
  [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) (α : Type)
  [DecidableEq α] :
  TrackSoundAllStatement S α
    **P3 (soundness for every formula), PROVED.**
Definition7.5.2
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 7.5.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbridgednot audited

On the simulator's data, a checked occurrence o \checkmark_F a gives a rule R \to R' with instantiation \eta, a context D, a parameter d and a renumbering \rho with a = \rho \bullet W, where W = D \circ ((R \otimes \mathrm{id}) \circ d); its result is a' = D \circ ((R' \otimes \mathrm{id}) \circ \bar\eta(d)). Writing n_D, n_R, n_{R'} for the numbers of items, W lists the context at [0, n_D), then the redex, then the parameter, and a' lists the context at [0, n_D), then the reactum, then the kept copies (j, p) of parameter items, at \kappa(j, p) = n_D + n_{R'} + \mathrm{idx}(j, p): every item of a' is in exactly one of the context [0, n_D), the reactum [n_D, n_D + n_{R'}), and the kept copies, the k-th of which is the copy of the k-th kept pair. For a list \tau sending redex items to reactum items, the tracking map \mathrm{tr}_\tau from the items of a to those of a' sends \rho(v) to v for a context item, \rho(n_D + u) to n_D + \tau(u) for a redex item, and a parameter item to its kept copy; it is undefined where \tau is, and on a parameter item whose region the rule discards.

Class: occTrack BRIDGED; OccPreserve.result_n, OccPreserve.result_part not audited.

Lean code for Definition7.5.2●3 declarations
  • defdefined in Logic/Track.lean
    complete
    def occTrack {Ctrl : Type} (τ : List (Nat × Nat)) (o : BigraphSim.Occ Ctrl)
  (v : Nat) : Option Nat
    def occTrack {Ctrl : Type}
  (τ : List (Nat × Nat))
  (o : BigraphSim.Occ Ctrl) (v : Nat) :
  Option Nat
    **The tracking map of a matcher occurrence**, from the agent
`o.whole.perm o.ren` to `o.result`: the context keeps its numbers, a
redex item goes by `τ`, a parameter node to its kept copy (region
discarded: undefined).
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem result_n {Ctrl : Type} {o : BigraphSim.Occ Ctrl} :
  o.result.n =
    o.ctx.n + (o.rule.reactum.n + (o.param.kept o.rule.eta).length)
    theorem result_n {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} :
  o.result.n =
    o.ctx.n +
      (o.rule.reactum.n +
        (o.param.kept o.rule.eta).length)
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem result_part {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {v : Nat}
  (hv : v < o.result.n) :
  v < o.ctx.n ∨
    (∃ u, u < o.rule.reactum.n ∧ v = o.ctx.n + u) ∨
      ∃ k,
        k < (o.param.kept o.rule.eta).length ∧
          v = o.ctx.n + o.rule.reactum.n + k
    theorem result_part {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {v : Nat}
  (hv : v < o.result.n) :
  v < o.ctx.n ∨
    (∃ u,
        u < o.rule.reactum.n ∧
          v = o.ctx.n + u) ∨
      ∃ k,
        k <
            (o.param.kept
                o.rule.eta).length ∧
          v =
            o.ctx.n + o.rule.reactum.n + k
    **The partition of the result**: context, reactum, kept copies.
Theorem7.5.3
uses 1used by 0✓L∃∀N

A checked reaction leaves the context as it was. Let o \checkmark_F a. Every item of a is, through \rho, in one of the context, the redex and the parameter. For context items v, w < n_D, ports i, j and any \tau,

\mathrm{tr}_\tau(\rho(v)) = v, \qquad \mathrm{ctrl}_a(\rho(v)) = \mathrm{ctrl}_D(v) = \mathrm{ctrl}_{a'}(v), \qquad \mathrm{prnt}_a(\rho(v)) = \rho(\mathrm{prnt}_D(v)), \quad \mathrm{prnt}_{a'}(v) = \mathrm{prnt}_D(v) ,

\mathrm{link}_a(\rho(v), i) = \rho(\mathrm{link}_D(v, i)), \quad \mathrm{link}_{a'}(v, i) = \mathrm{link}_D(v, i), \qquad \mathrm{link}_a(\rho(v), i) = \mathrm{link}_a(\rho(w), j) \iff \mathrm{link}_{a'}(v, i) = \mathrm{link}_{a'}(w, j) .

The children of a context node are not claimed to be preserved.

Rests on NEW: BigraphSim.Item, BigraphSim.Occ, BigraphSim.Par; not audited: BigraphSim.BD.ctrl, BigraphSim.BD.link, BigraphSim.BD.n, BigraphSim.BD.parOf, BigraphSim.BD.renLk, BigraphSim.BD.renPar, BigraphSim.Occ.Ok, BigraphSim.Ren.bn and 1 more.

Lean code for Theorem7.5.3●6 theorems
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem part {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o) {w : Nat}
  (hw : w < a.n) :
  o.ren.bn w < o.ctx.n ∨
    o.ctx.n ≤ o.ren.bn w ∧ o.ren.bn w < o.ctx.n + o.rule.redex.n ∨
      o.ctx.n + o.rule.redex.n ≤ o.ren.bn w ∧
        o.ren.bn w < o.ctx.n + o.rule.redex.n + o.param.n
    theorem part {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  {w : Nat} (hw : w < a.n) :
  o.ren.bn w < o.ctx.n ∨
    o.ctx.n ≤ o.ren.bn w ∧
        o.ren.bn w <
          o.ctx.n + o.rule.redex.n ∨
      o.ctx.n + o.rule.redex.n ≤
          o.ren.bn w ∧
        o.ren.bn w <
          o.ctx.n + o.rule.redex.n +
            o.param.n
    **The partition.** Every item of the agent is, through `ρ`, in exactly
one of the context, the redex, the parameter.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem occTrack_ctx {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o)
  (τ : List (Nat × Nat)) {v : Nat} (hv : v < o.ctx.n) :
  occTrack τ o (o.ren.fn v) = some v
    theorem occTrack_ctx {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  (τ : List (Nat × Nat)) {v : Nat}
  (hv : v < o.ctx.n) :
  occTrack τ o (o.ren.fn v) = some v
    A context item is tracked to itself (`occTrack`, any tracking list).
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem ctx_ctrl {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o) {v : Nat}
  (hv : v < o.ctx.n) :
  a.ctrl (o.ren.fn v) = o.ctx.ctrl v ∧ o.result.ctrl v = o.ctx.ctrl v
    theorem ctx_ctrl {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  {v : Nat} (hv : v < o.ctx.n) :
  a.ctrl (o.ren.fn v) = o.ctx.ctrl v ∧
    o.result.ctrl v = o.ctx.ctrl v
    **Q3.** A context node has the same control in the agent and the result.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem ctx_parOf {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o) {v : Nat}
  (hv : v < o.ctx.n) :
  a.parOf (o.ren.fn v) =
      Option.map (BigraphSim.BD.renPar o.ren) (o.ctx.parOf v) ∧
    o.result.parOf v = o.ctx.parOf v
    theorem ctx_parOf {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  {v : Nat} (hv : v < o.ctx.n) :
  a.parOf (o.ren.fn v) =
      Option.map
        (BigraphSim.BD.renPar o.ren)
        (o.ctx.parOf v) ∧
    o.result.parOf v = o.ctx.parOf v
    **Q3.** A context node has the same parent, up to `ρ`.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem ctx_link {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o) {v : Nat}
  (hv : v < o.ctx.n) (i : Nat) :
  a.link (Pt.port (o.ren.fn v) i) =
      Option.map (BigraphSim.BD.renLk o.ren)
        (o.ctx.link (Pt.port v i)) ∧
    o.result.link (Pt.port v i) = o.ctx.link (Pt.port v i)
    theorem ctx_link {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  {v : Nat} (hv : v < o.ctx.n) (i : Nat) :
  a.link (Pt.port (o.ren.fn v) i) =
      Option.map
        (BigraphSim.BD.renLk o.ren)
        (o.ctx.link (Pt.port v i)) ∧
    o.result.link (Pt.port v i) =
      o.ctx.link (Pt.port v i)
    **Q4.** A context port lies on the same context link on both sides.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem ctx_share {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o)
  {v w : Nat} (hv : v < o.ctx.n) (hw : w < o.ctx.n) (i j : Nat) :
  a.link (Pt.port (o.ren.fn v) i) = a.link (Pt.port (o.ren.fn w) j) ↔
    o.result.link (Pt.port v i) = o.result.link (Pt.port w j)
    theorem ctx_share {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  {v w : Nat} (hv : v < o.ctx.n)
  (hw : w < o.ctx.n) (i j : Nat) :
  a.link (Pt.port (o.ren.fn v) i) =
      a.link (Pt.port (o.ren.fn w) j) ↔
    o.result.link (Pt.port v i) =
      o.result.link (Pt.port w j)
    **Q4.** Two context ports share a link in the agent iff in the result.
Theorem7.5.4
uses 1used by 0✓L∃∀N

A kept parameter node keeps its control, its links and a parent inside the parameter. Let o \checkmark_F a, let the parameter node p lie under root s of d, and let \eta(j) = s. Then, with q = n_D + n_R + p its position in W, for every port i and any \tau,

\mathrm{tr}_\tau(\rho(q)) = \kappa(j, p), \qquad \mathrm{ctrl}_{a'}(\kappa(j, p)) = \mathrm{ctrl}_W(q), \qquad \mathrm{link}_{a'}(\kappa(j, p), i) = \mathrm{link}_W(q, i) ,

\mathrm{prnt}_d(p) = u \text{ a node} \;\Longrightarrow\; \mathrm{prnt}_{a'}(\kappa(j, p)) = \kappa(j, u) .

The parent of a node at the top of its region is not kept: it is where site s of the redex sits in W, and where site j of the reactum sits in a'. The same holds by position: the copy at position k among the kept copies has the control of its parameter node, and its parent is given by the same three cases.

Rests on NEW: BigraphSim.Item, BigraphSim.Occ, BigraphSim.Par; not audited: BigraphSim.BD.ctrl, BigraphSim.BD.kept, BigraphSim.BD.link, BigraphSim.BD.n, BigraphSim.BD.parOf, BigraphSim.BD.rootUp, BigraphSim.BD.shiftItem, BigraphSim.BD.shiftPar and 4 more.

Lean code for Theorem7.5.4●9 theorems
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem occTrack_param {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o)
  (τ : List (Nat × Nat)) {p s j : Nat}
  (hr : o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s) :
  occTrack τ o (o.ren.fn (o.ctx.n + o.rule.redex.n + p)) =
    some
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p) (o.param.kept o.rule.eta))
    theorem occTrack_param {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  (τ : List (Nat × Nat)) {p s j : Nat}
  (hr :
    o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s) :
  occTrack τ o
      (o.ren.fn
        (o.ctx.n + o.rule.redex.n + p)) =
    some
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p)
          (o.param.kept o.rule.eta))
    **Q5.** `occTrack` sends a kept parameter node to the copy above.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem kept_ctrl {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {p s j : Nat}
  (hr : o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s) :
  o.result.ctrl
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p) (o.param.kept o.rule.eta)) =
    o.whole.ctrl (o.ctx.n + o.rule.redex.n + p)
    theorem kept_ctrl {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {p s j : Nat}
  (hr :
    o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s) :
  o.result.ctrl
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p)
          (o.param.kept o.rule.eta)) =
    o.whole.ctrl
      (o.ctx.n + o.rule.redex.n + p)
    **Q5.** A kept parameter node keeps its control.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem kept_link {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool} {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl} (ok : BigraphSim.Occ.Ok S fam a o)
  {p s j : Nat} (hr : o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s) (i : Nat) :
  o.result.link
      (Pt.port
        (o.ctx.n + o.rule.reactum.n +
          List.idxOf (j, p) (o.param.kept o.rule.eta))
        i) =
    o.whole.link (Pt.port (o.ctx.n + o.rule.redex.n + p) i)
    theorem kept_link {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {fam : BigraphSim.RuleD Ctrl → Bool}
  {a : BigraphSim.BD Ctrl}
  {o : BigraphSim.Occ Ctrl}
  (ok : BigraphSim.Occ.Ok S fam a o)
  {p s j : Nat}
  (hr :
    o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s)
  (i : Nat) :
  o.result.link
      (Pt.port
        (o.ctx.n + o.rule.reactum.n +
          List.idxOf (j, p)
            (o.param.kept o.rule.eta))
        i) =
    o.whole.link
      (Pt.port
        (o.ctx.n + o.rule.redex.n + p) i)
    **Q5.** A kept parameter node keeps the link of every port.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem kept_parOf_node {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {p s j u : Nat}
  (hr : o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s)
  (hp : o.param.parOf p = some (BigraphSim.Par.node u)) :
  o.result.parOf
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p) (o.param.kept o.rule.eta)) =
    some
      (BigraphSim.Par.node
        (o.ctx.n + o.rule.reactum.n +
          List.idxOf (j, u) (o.param.kept o.rule.eta)))
    theorem kept_parOf_node {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl}
  {p s j u : Nat}
  (hr :
    o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s)
  (hp :
    o.param.parOf p =
      some (BigraphSim.Par.node u)) :
  o.result.parOf
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p)
          (o.param.kept o.rule.eta)) =
    some
      (BigraphSim.Par.node
        (o.ctx.n + o.rule.reactum.n +
          List.idxOf (j, u)
            (o.param.kept o.rule.eta)))
    **Q5.** A parent that is a parameter node: its copy, in the result.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem param_parOf_root {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {p s : Nat}
  (hp : o.param.parOf p = some (BigraphSim.Par.root s)) :
  o.whole.parOf (o.ctx.n + o.rule.redex.n + p) =
    some
      (o.ctx.shiftPar o.ctx.n
        (o.rule.redex.sites[s]?.getD (BigraphSim.Par.root s)))
    theorem param_parOf_root {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {p s : Nat}
  (hp :
    o.param.parOf p =
      some (BigraphSim.Par.root s)) :
  o.whole.parOf
      (o.ctx.n + o.rule.redex.n + p) =
    some
      (o.ctx.shiftPar o.ctx.n
        (o.rule.redex.sites[s]?.getD
          (BigraphSim.Par.root s)))
    **Q5.** A node at the top of its region: its parent in the matched agent
is where the REDEX's site `s` sits.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem kept_parOf_root {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {p s j s' : Nat}
  (hr : o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s)
  (hp : o.param.parOf p = some (BigraphSim.Par.root s')) :
  o.result.parOf
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p) (o.param.kept o.rule.eta)) =
    some
      (o.ctx.shiftPar o.ctx.n
        (o.rule.reactum.sites[j]?.getD (BigraphSim.Par.root j)))
    theorem kept_parOf_root {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl}
  {p s j s' : Nat}
  (hr :
    o.param.rootUp o.param.n p = some s)
  (hj : o.rule.eta[j]? = some s)
  (hp :
    o.param.parOf p =
      some (BigraphSim.Par.root s')) :
  o.result.parOf
      (o.ctx.n + o.rule.reactum.n +
        List.idxOf (j, p)
          (o.param.kept o.rule.eta)) =
    some
      (o.ctx.shiftPar o.ctx.n
        (o.rule.reactum.sites[j]?.getD
          (BigraphSim.Par.root j)))
    **Q5.** A node at the top of its region: the parent of its copy is where
the REACTUM's site `j` sits.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem result_kept_at {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {k : Nat}
  (hk : k < (o.param.kept o.rule.eta).length) :
  o.result.items[o.ctx.n + o.rule.reactum.n + k]? =
    Option.map (o.ctx.shiftItem o.ctx.n)
      (Option.map (o.reactumX.shiftItem o.reactumX.n)
        (some
          (o.param.instItem o.rule.eta (o.param.kept o.rule.eta)[k])))
    theorem result_kept_at {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {k : Nat}
  (hk :
    k <
      (o.param.kept o.rule.eta).length) :
  o.result.items[o.ctx.n +
          o.rule.reactum.n +
        k]? =
    Option.map (o.ctx.shiftItem o.ctx.n)
      (Option.map
        (o.reactumX.shiftItem
          o.reactumX.n)
        (some
          (o.param.instItem o.rule.eta
            (o.param.kept
                o.rule.eta)[k])))
    The kept copy at position `k`.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem kept_at_ctrl {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {k : Nat}
  (hk : k < (o.param.kept o.rule.eta).length) :
  o.result.ctrl (o.ctx.n + o.rule.reactum.n + k) =
    o.param.ctrl (o.param.kept o.rule.eta)[k].snd
    theorem kept_at_ctrl {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {k : Nat}
  (hk :
    k <
      (o.param.kept o.rule.eta).length) :
  o.result.ctrl
      (o.ctx.n + o.rule.reactum.n + k) =
    o.param.ctrl
      (o.param.kept o.rule.eta)[k].snd
    The copy at position `k` has the control of its parameter node.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem kept_at_parOf {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {k : Nat}
  (hk : k < (o.param.kept o.rule.eta).length) :
  o.result.parOf (o.ctx.n + o.rule.reactum.n + k) =
    Option.map (o.ctx.shiftPar o.ctx.n)
      (Option.map (o.reactumX.shiftPar o.reactumX.n)
        (Option.map
          (o.param.instPar o.rule.eta (o.param.kept o.rule.eta)[k].fst)
          (o.param.parOf (o.param.kept o.rule.eta)[k].snd)))
    theorem kept_at_parOf {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {k : Nat}
  (hk :
    k <
      (o.param.kept o.rule.eta).length) :
  o.result.parOf
      (o.ctx.n + o.rule.reactum.n + k) =
    Option.map (o.ctx.shiftPar o.ctx.n)
      (Option.map
        (o.reactumX.shiftPar o.reactumX.n)
        (Option.map
          (o.param.instPar o.rule.eta
            (o.param.kept
                  o.rule.eta)[k].fst)
          (o.param.parOf
            (o.param.kept
                  o.rule.eta)[k].snd)))
    The parent of the copy at position `k`.
Theorem7.5.5
uses 1used by 0✓L∃∀N

The reactum appears in the result as the rule gives it, read through the context: an edge of the reactum is renumbered, and an outer name of the reactum becomes the context's link of that name (\mathrm{sh}_D below). For reactum items u, u' < n_{R'} and ports i, i',

\mathrm{ctrl}_{a'}(n_D + u) = \mathrm{ctrl}_{R'}(u), \qquad \mathrm{link}_{a'}(n_D + u, i) = \mathrm{sh}_D(\mathrm{link}_{R'}(u, i)) ,

\mathrm{link}_{R'}(u, i) = \mathrm{link}_{R'}(u', i') \;\Longrightarrow\; \mathrm{link}_{a'}(n_D + u, i) = \mathrm{link}_{a'}(n_D + u', i') .

Rests on NEW: BigraphSim.Item, BigraphSim.Occ, BigraphSim.Par; not audited: BigraphSim.BD.ctrl, BigraphSim.BD.link, BigraphSim.BD.n, BigraphSim.BD.shiftItem, BigraphSim.BD.shiftLk.

Lean code for Theorem7.5.5●4 theorems
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem result_reactum {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {u : Nat}
  (hu : u < o.rule.reactum.n) :
  o.result.items[o.ctx.n + u]? =
    Option.map (o.ctx.shiftItem o.ctx.n) o.rule.reactum.items[u]?
    theorem result_reactum {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {u : Nat}
  (hu : u < o.rule.reactum.n) :
  o.result.items[o.ctx.n + u]? =
    Option.map (o.ctx.shiftItem o.ctx.n)
      o.rule.reactum.items[u]?
    **Q6.** A reactum item, read through the context.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem reactum_ctrl {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {u : Nat}
  (hu : u < o.rule.reactum.n) :
  o.result.ctrl (o.ctx.n + u) = o.rule.reactum.ctrl u
    theorem reactum_ctrl {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {u : Nat}
  (hu : u < o.rule.reactum.n) :
  o.result.ctrl (o.ctx.n + u) =
    o.rule.reactum.ctrl u
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem reactum_link {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {u : Nat}
  (hu : u < o.rule.reactum.n) (i : Nat) :
  o.result.link (Pt.port (o.ctx.n + u) i) =
    Option.map (o.ctx.shiftLk o.ctx.n)
      (o.rule.reactum.link (Pt.port u i))
    theorem reactum_link {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {u : Nat}
  (hu : u < o.rule.reactum.n) (i : Nat) :
  o.result.link
      (Pt.port (o.ctx.n + u) i) =
    Option.map (o.ctx.shiftLk o.ctx.n)
      (o.rule.reactum.link (Pt.port u i))
    **Q6.** The link of a reactum port: an edge of the reactum shifted, an
outer name read as the context's link of that name.
  • theoremdefined in Logic/OccPreserve.lean
    complete
    theorem reactum_share {Ctrl : Type} {o : BigraphSim.Occ Ctrl} {u u' : Nat}
  (hu : u < o.rule.reactum.n) (hu' : u' < o.rule.reactum.n) (i i' : Nat)
  (h :
    o.rule.reactum.link (Pt.port u i) =
      o.rule.reactum.link (Pt.port u' i')) :
  o.result.link (Pt.port (o.ctx.n + u) i) =
    o.result.link (Pt.port (o.ctx.n + u') i')
    theorem reactum_share {Ctrl : Type}
  {o : BigraphSim.Occ Ctrl} {u u' : Nat}
  (hu : u < o.rule.reactum.n)
  (hu' : u' < o.rule.reactum.n)
  (i i' : Nat)
  (h :
    o.rule.reactum.link (Pt.port u i) =
      o.rule.reactum.link
        (Pt.port u' i')) :
  o.result.link
      (Pt.port (o.ctx.n + u) i) =
    o.result.link
      (Pt.port (o.ctx.n + u') i')
    **Q6.** Ports sharing a link in the reactum share one in the result.