Runtime typing under renamings that fix and avoid shared names to Request-freeness is invariant under binder swapping

TheoremRuntime typing under renamings that fix and avoid shared names#✓fully proved

ALL10 runtime derivation rules transport actual names with Γ unchanged. Shared nonalias is required only on OWNED images, not unrestricted passive names.

theorem HasType.rename {n m : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc} {f : Name → Name}
    (h : HasType n Γ Δ p) (hscope : ∀ a, a.ClosedAt n → (f a).ClosedAt m)
    (hfix : FixesShared Γ f) (hn : NonAliases Γ Δ f)
    (hf : Set.InjOn (Key.mapName f) {e | e ∈ Δ}) :
    HasType m Γ (Context.rekey (Key.mapName f) Δ hf) (mapProc f p)

Uses 56 · Used by 4

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Collision-free rekeying of an ownership map · Polarized endpoint key · Renaming the physical name of an endpoint key · Name map fixing every declared shared constant · Runtime typing with guarded shared replication · Nonaliasing of owned-name images with shared constants · Shared service environment · Capture-safe renaming of processes

Proof usesEquivalence of endpoint capabilities · Completed ownership map · Rekeying preserves completion · Binding a fresh dual pair under restriction · Injective rekeying preserves disjoint ownership · Injectivity of rekeying survives erasing a key · Injectivity of rekeying survives updating an owned key · Injectivity of rekeying under a restriction binding · Injectivity of rekeying passes under a binder · Injectivity of rekeying after receiving a fresh role · Lifting an ownership map past a binder · Lookups in a rekeyed ownership map · Keys of a rekeyed ownership map · Rekeying commutes with binding a private pair · Collision-free rekeying commutes with erasing an owned key · Collision-free rekeying commutes with insertion · Rekeying under a binder is the lift of the outer rekeying · Collision-free rekeying commutes with a disjoint union · Guard priority condition on active endpoints · Injective rekeying preserves the guard condition · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Binder extension preserves fixing of shared constants · Priority of a shared invocation over active owned keys · Rekeying preserves shared invocation priority · Erasing an owned key preserves nonaliasing · Updating an already-owned key preserves nonaliasing · Rekeying along a nonaliasing name map yields separation · Nonaliasing survives binding a private session pair · Binder extension preserves nonaliasing of lifted contexts · Nonaliasing survives adding a received parameter under a binder · Nonaliasing restricts to the left part of a union · Nonaliasing restricts to the right part of a union · Separation of owned linear names from shared names · Shared service signature · Structural shared-service template · Service templates are preserved by renamings fixing shared names · Every name map is nonaliasing on empty ownership · Rekeying the empty context gives the empty context · Rekeying a singleton moves its key and keeps its capability · Extension of a name map under a binder · Extending a scoped name map under a binder keeps it scoped

Used byBinder lifting preserves runtime typing · Runtime typing under substitution of a transmitted endpoint · Runtime typing under passive name substitution · Binder swapping preserves runtime typing

TheoremBinder lifting preserves runtime typing#✓fully proved

Canonical binder lift retains the entire runtime derivation and Γ literally.

theorem HasType.lift {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) (k : Nat) : HasType (n + 1) Γ (Context.lift k Δ) (liftProc k p)

Uses 22 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Lifting an ownership map past a binder · Runtime typing with guarded shared replication · Shared service environment

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting preserves name scoping · Lifting free de Bruijn indices of a π-calculus name · Endpoint capability with a dependency rank · Collision-free rekeying of an ownership map · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Runtime typing under renamings that fix and avoid shared names · Runtime typing separates owned names from shared services · Separation gives nonaliasing for binder lifting · Shared service signature · Injectivity of name lifting · Capture-safe renaming of processes · Process renaming by a lift is process lifting

Used byRuntime typing is preserved by forward scope extrusion

TheoremBinder swapping preserves runtime typing#✓fully proved

Canonical swap permutes actual owned binders without changing Γ or cap metadata.

theorem HasType.swap {n k : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc}
    (h : HasType n Γ Δ p) (hk : k + 1 < n) : HasType n Γ (Context.swap k Δ) (swapProc k p)

Uses 22 · Used by 1

Statement usesProcesses of the π-calculus · Swapping adjacent binders throughout a process · Finite endpoint ownership map · Swapping two ambient binders in an ownership context · Runtime typing with guarded shared replication · Shared service environment

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Swapping adjacent de Bruijn indices in a name · Endpoint capability with a dependency rank · Collision-free rekeying of an ownership map · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Runtime typing under renamings that fix and avoid shared names · Runtime typing separates owned names from shared services · Separation gives nonaliasing for binder swapping · Shared service signature · Swapping binders in scope preserves name scoping · Capture-safe renaming of processes · Process renaming by a swap is the restriction swap · Injectivity of name swapping

Used byStructural congruence preserves runtime typing

TheoremNonshared endpoint substitution keeps owned names nonshared#✓fully proved

An actual nonshared endpoint replacement keeps every owned substituted image nonshared.

theorem Separated.nonaliases_subst {Γ : ServiceEnv} {Δ : Context} (h : Separated Γ Δ)
    {b : Name} (hb : ∀ s sig, Γ.lookup s = some sig → b ≠ .const s) :
    NonAliases Γ Δ (substName b 0)

Uses 10 · Used by 1

Statement usesChannel name in the π-calculus · Substitution of a name into a π-calculus name · Finite endpoint ownership map · Nonaliasing of owned-name images with shared constants · Separation of owned linear names from shared names · Shared service environment · Shared service signature

Proof usesEndpoint capability with a dependency rank · Polarized endpoint key · Endpoint role on a π name

Used byRuntime typing under substitution of a transmitted endpoint

TheoremPassive substitution creates no owned shared-name alias#✓fully proved

Passive var0 is NOT owned: even a shared-constant replacement preserves all actual lifted owned names and creates no linear shared-name alias.

theorem Separated.nonaliases_passive {Γ : ServiceEnv} {Δ : Context}
    (h : Separated Γ (Context.lift 0 Δ)) (b : Name) :
    NonAliases Γ (Context.lift 0 Δ) (substName b 0)

Uses 12 · Used by 1

Statement usesChannel name in the π-calculus · Substitution of a name into a π-calculus name · Finite endpoint ownership map · Lifting an ownership map past a binder · Nonaliasing of owned-name images with shared constants · Separation of owned linear names from shared names · Shared service environment

Proof usesEndpoint capability with a dependency rank · Both roles of the new name are fresh for a lifted map · Polarized endpoint key · Endpoint role on a π name · Shared service signature

Used byRuntime typing under passive name substitution

TheoremRuntime typing under substitution of a transmitted endpoint#✓fully proved

Actual transmitted endpoint substitution preserves literal role/rank and raw code. Shared nonalias of b is a static consequence of ACTUAL sender ownership/separation.

theorem HasType.subst_endpoint {n : Nat} {Γ : ServiceEnv} {Δ : Context} {b : Name} {r : Role}
    {c v : Capability} {p : Proc}
    (h : HasType (n + 1) Γ ((Context.lift 0 Δ).insert ⟨.var 0, r⟩ c) p)
    (he : v.Equivalent c) (hb : b.ClosedAt n) (hfresh : (⟨b, r⟩ : Key) ∉ Δ)
    (hshared : ∀ s sig, Γ.lookup s = some sig → b ≠ .const s) :
    HasType n Γ (Δ.insert ⟨b, r⟩ v) (PiCalculus.subst p b)

Uses 29 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Shared service environment · Shared service signature

Proof usesName substitution preserves scoping · Substitution of a name into a π-calculus name · Substitution of a name into a π-calculus process at a cutoff · Symmetry of capability equivalence · Received-endpoint substitution is injective when the role is fresh · Collision-free rekeying of an ownership map · Received-endpoint substitution moves the bound role to the sent key · Equivalent insertions preserve ownership-map equivalence · Reflexivity of ownership-map equivalence · Renaming the physical name of an endpoint key · Runtime typing under renamings that fix and avoid shared names · Runtime typing transfers to an equivalent linear context · Runtime typing separates owned names from shared services · Nonshared endpoint substitution keeps owned names nonshared · Capture-safe renaming of processes · Process renaming by a substitution is process substitution

Used byEndpoint substitution with side conditions derived from a split · Shared invocation and input worker preserve the combined interface

TheoremRuntime typing under passive name substitution#✓fully proved

Passive substitution has NO owned var0 and adds NO capability. A scoped shared constant can be received as data without becoming a linear/service subject.

theorem HasType.subst_passive {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p : Proc} {b : Name}
    (h : HasType (n + 1) Γ (Context.lift 0 Δ) p) (hb : b.ClosedAt n) :
    HasType n Γ Δ (PiCalculus.subst p b)

Uses 23 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Finite endpoint ownership map · Lifting an ownership map past a binder · Runtime typing with guarded shared replication · Shared service environment

Proof usesName substitution preserves scoping · Substitution of a name into a π-calculus name · Substitution of a name into a π-calculus process at a cutoff · Endpoint capability with a dependency rank · Passive substitution is injective on lifted outer keys · Collision-free rekeying of an ownership map · Passive substitution leaves the linear context unchanged · Polarized endpoint key · Renaming the physical name of an endpoint key · Runtime typing under renamings that fix and avoid shared names · Runtime typing separates owned names from shared services · Passive substitution creates no owned shared-name alias · Shared service signature · Capture-safe renaming of processes · Process renaming by a substitution is process substitution

Used byRuntime typing reflects through binder lifting · Passive head communication preserves runtime typing

TheoremEndpoint substitution with side conditions derived from a split#✓fully proved

Real sender ownership and a disjoint receiver carrier derive exact-role freshness and shared nonalias of the actual transmitted endpoint.

theorem HasType.subst_endpoint_from_split {n : Nat} {Γ : ServiceEnv} {Λ Θ : Context}
    {b : Name} {r : Role} {c v old next : Capability} {e : Key} {p : Proc}
    (hsep : Separated Γ Λ) (hd : Finmap.Disjoint Λ Θ) (hv : Λ.lookup ⟨b, r⟩ = some v)
    (hc : Θ.lookup e = some old)
    (h : HasType (n + 1) Γ ((Context.lift 0 (Θ.insert e next)).insert ⟨.var 0, r⟩ c) p)
    (he : v.Equivalent c) (hb : b.ClosedAt n) :
    HasType n Γ ((Θ.insert e next).insert ⟨b, r⟩ v) (PiCalculus.subst p b)

Uses 16 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Finite endpoint ownership map · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Separation of owned linear names from shared names · Shared service environment

Proof usesUpdating an owned key keeps absent keys absent · Owned keys are absent from the other side of a disjoint split · Runtime typing under substitution of a transmitted endpoint

Used byEndpoint head communication preserves runtime typing

TheoremRuntime typing reflects through binder lifting#✓fully proved

Reflection of a canonical lifted term retains exact owned capabilities and Γ.

theorem HasType.unlift {n : Nat} {Γ : ServiceEnv} {Δ : Context} {q : Proc}
    (h : HasType (n + 1) Γ Δ (liftProc 0 q)) (hΔ : ∀ e ∈ Δ, e.name ≠ .var 0) :
    HasType n Γ (Context.lower Δ hΔ) q

Uses 15 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Endpoint capability with a dependency rank · Finite endpoint ownership map · Lowering of an outer context past a fresh binder · Polarized endpoint key · Runtime typing with guarded shared replication · Shared service environment

Proof usesSubstitution for the innermost bound variable of a process · Substitution of a name into a π-calculus process at a cutoff · Lifting an ownership map past a binder · Lifting a lowered context recovers it · Runtime typing under passive name substitution · Substitution cancels process lifting

Used byRuntime typing is preserved by reverse scope extrusion

TheoremRuntime typing is preserved by forward scope extrusion#✓fully proved

Forward extrusion uses the actual disjoint split and literal bound pair.

theorem HasType.scope_forward {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p q : Proc}
    (h : HasType n Γ Δ (.par (.nu p) q)) :
    HasType n Γ Δ (.nu (.par p (liftProc 0 q)))

Uses 18 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Runtime typing with guarded shared replication · Shared service environment

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Binding a fresh dual pair under restriction · Restriction binding of a disjoint union · Binding a fresh pair keeps disjointness from a lifted context · Lifting an ownership map past a binder · Polarized endpoint key · Endpoint role on a π name · Binder lifting preserves runtime typing · Inversion of runtime typing for restriction · Inversion of runtime typing for parallel composition · Runtime typing separates owned names from shared services · Separation of owned linear names from shared names

Used byRuntime typing is invariant under scope extrusion

TheoremRuntime typing absorbs a role absent from its parallel partner#✓fully proved

Partner ownership may be restored only when actual absence DERIVES completion. Shared nonalias is obtained from the typed owner, not a new unchecked assumption.

theorem HasType.insert_from_absent_partner {n : Nat} {Γ : ServiceEnv} {Δ Ξ : Context}
    {p q : Proc} {e : Key} {c : Capability} (hp : HasType n Γ Δ p) (hq : HasType n Γ Ξ q)
    (hc : (Δ ∪ Ξ).lookup e = some c) (hab : NameAbsent e.name q) (he : e.name.ClosedAt n) :
    HasType n Γ (Δ.insert e c) p

Uses 14 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Absence of a physical name from a process · Endpoint role on a π name · Runtime typing with guarded shared replication · Shared service environment

Proof usesReinserting an owned capability changes nothing · Owned names absent from a runtime process are completed · Runtime typing separates owned names from shared services · Weakening runtime typing by one fresh completed entry

Used byRuntime typing restores both bound roles to the restricted side

TheoremRuntime typing restores both bound roles to the restricted side#✓fully proved

Restoring a private pair adds only actually absent completed partner roles.

theorem HasType.restore_scope_pair {n : Nat} {Γ : ServiceEnv} {Δ Λ Ξ : Context} {p q : Proc}
    {c : Capability} (hp : HasType (n + 1) Γ Λ p)
    (hq : HasType (n + 1) Γ Ξ (liftProc 0 q)) (hs : Context.bind c Δ = Λ ∪ Ξ) :
    HasType (n + 1) Γ ((Λ.insert (⟨.var 0, .positive⟩ : Key) c).insert
      (⟨.var 0, .negative⟩ : Key) c.dual) p

Uses 16 · Used by 1

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Endpoint capability with a dependency rank · Dual of an endpoint capability · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Polarized endpoint key · Endpoint role on a π name · Runtime typing with guarded shared replication · Shared service environment

Proof usesNegative role lookup after restriction binding · Positive role lookup after restriction binding · Absence of a physical name from a process · Runtime typing absorbs a role absent from its parallel partner · The inserted name is absent from a lifted process

Used byRuntime typing is preserved by reverse scope extrusion

TheoremRuntime typing is preserved by reverse scope extrusion#✓fully proved

Reverse extrusion derives the exact external split from actual typing and removes only genuinely absent partner roles. No closed-hole or ready premise.

theorem HasType.scope_reverse {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p q : Proc}
    (h : HasType n Γ Δ (.nu (.par p (liftProc 0 q)))) :
    HasType n Γ Δ (.par (.nu p) q)

Uses 31 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Runtime typing with guarded shared replication · Shared service environment

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Dual of an endpoint capability · Binding a fresh dual pair under restriction · Lowering preserves disjointness of outer contexts · Erasing the bound pair leaves the lifted context · Erasure distributes over union · Erasing both roles of the fresh name leaves outer keys · Lifting an ownership map past a binder · Lifting a lowered context recovers it · Context lifting preserves a disjoint union · Context lifting is injective · Lowering of an outer context past a fresh binder · Reinstalling the bound pair after erasing its slots · Polarized endpoint key · Absence of a physical name from a process · Endpoint role on a π name · Erasing a key whose name is absent preserves runtime typing · Inversion of runtime typing for restriction · Inversion of runtime typing for parallel composition · Runtime typing restores both bound roles to the restricted side · Runtime typing separates owned names from shared services · Runtime typing reflects through binder lifting · Separation of owned linear names from shared names · Separation restricts to the left part of a union · The inserted name is absent from a lifted process

Used byRuntime typing is invariant under scope extrusion

TheoremRuntime typing is invariant under scope extrusion#✓fully proved

Exact canonical scope transport preserves SAME Γ, n and Δ in both directions.

theorem HasType.scope_iff {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p q : Proc} :
    HasType n Γ Δ (.par (.nu p) q) ↔ HasType n Γ Δ (.nu (.par p (liftProc 0 q)))

Uses 7 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Runtime typing with guarded shared replication · Shared service environment

Proof usesRuntime typing is preserved by forward scope extrusion · Runtime typing is preserved by reverse scope extrusion

Used byStructural congruence preserves runtime typing

TheoremStructural congruence preserves runtime typing#✓fully proved

ALL16 canonical Cong rules preserve the whole runtime derivation at exactly SAME Γ/n/Δ, including guarded replicated templates, completed ambient annotations, and actual runtime delegation continuations. No typing-up-to-Cong constructor.

theorem HasType.cong_iff {n : Nat} {Γ : ServiceEnv} {Δ : Context} {p q : Proc} (hc : Cong p q) :
    HasType n Γ Δ p ↔ HasType n Γ Δ q

Uses 45 · Used by 2

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Finite endpoint ownership map · Runtime typing with guarded shared replication · Shared service environment

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent binders throughout a process · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction · The empty ownership map is completed · Lifting an ownership map past a binder · Swapping two ambient binders in an ownership context · Swapping nested restrictions exchanges their bound pairs · Guard priority condition on active endpoints · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Whole owned context of a runtime typing is scoped at ambient depth · Inversion of runtime typing for the nil process · Inversion of runtime typing for restriction · Removing a restriction around nil preserves runtime typing · Adding a restriction around nil preserves runtime typing · Inversion of runtime typing for parallel composition · Typed replication has a body with empty ownership · Inversion of runtime typing for replication · Runtime typing is invariant under scope extrusion · Runtime typing separates owned names from shared services · Binder swapping preserves runtime typing · Typed service templates own only completed entries · Typed service templates retype at empty ownership · Typed service templates retype at any well-formed completed context · Weakening runtime typing by a disjoint completed context · Priority of a shared invocation over active owned keys · Separation of owned linear names from shared names · Binding a private pair preserves separation · Shared service signature · Structural shared-service template · Service templates are invariant under structural congruence · Empty ownership is separated from shared names · Process swap is an involution

Used byGuarded normal form of a typed process keeps its typing · Subject reduction for runtime typing at compatible interfaces

InductiveGuarded frontier of guards and idle service templates#✓fully proved

Unguarded frontier atoms are actual guards or existing guarded idle templates.

inductive GuardedFrontier (Γ : ServiceEnv) : Proc → Prop where
  | template {p : Proc} : ServiceTemplate Γ p → GuardedFrontier Γ p
  | out (a b : Name) (p : Proc) : GuardedFrontier Γ (.out a b p)
  | inp (a : Name) (p : Proc) : GuardedFrontier Γ (.inp a p)
  | par {p q : Proc} : GuardedFrontier Γ p → GuardedFrontier Γ q → GuardedFrontier Γ (.par p q)

Uses 4 · Used by 11

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Shared service environment · Structural shared-service template

Used byGuarded normal form: restrictions over a guarded frontier · Request-free completed runtime frontiers are service templates · Minimum active key is the subject of a runtime frontier leaf · Non-request-free frontier exposes a shared output up to congruence · Lifting preserves guarded frontiers · Lifting preserves guarded normal forms · Parallel composition preserves guarded normal forms up to congruence · Exposed shared requests step when declared services are available · Runtime-typed processes are congruent to a guarded normal form · Balanced runtime frontiers are idle or step given availability · Global runtime progress at balanced interfaces given availability

InductiveGuarded normal form: restrictions over a guarded frontier#✓fully proved

Actual private restriction towers around a guarded runtime frontier.

inductive GuardedNormal (Γ : ServiceEnv) : Proc → Prop where
  | frontier {p : Proc} : GuardedFrontier Γ p → GuardedNormal Γ p
  | nu {p : Proc} : GuardedNormal Γ p → GuardedNormal Γ (.nu p)

Uses 3 · Used by 5

Statement usesProcesses of the π-calculus · Guarded frontier of guards and idle service templates · Shared service environment

Used byGuarded normal form of a typed process keeps its typing · Lifting preserves guarded normal forms · Parallel composition preserves guarded normal forms up to congruence · Runtime-typed processes are congruent to a guarded normal form · Global runtime progress at balanced interfaces given availability

DefinitionProcess with no exposed output on a declared shared name#✓fully proved

No exposed output is addressed to an actually declared shared constant. Prefix bodies are not inspected. This is syntax only, not a GLOBAL premise.

def RequestFree (Γ : ServiceEnv) : Proc → Prop
  | .nil | .inp .. => True
  | .out a _ _ => ∀ s sig, Γ.lookup s = some sig → a ≠ .const s
  | .par p q | .sum p q => RequestFree Γ p ∧ RequestFree Γ q
  | .nu p | .repl p => RequestFree Γ p

Uses 4 · Used by 11

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Shared service environment · Shared service signature

Used byRequest-freeness is invariant under lifting · Request-freeness is invariant under binder swapping · Request-free completed runtime frontiers are service templates · Request-freeness is invariant under structural congruence · Minimum active key is the subject of a runtime frontier leaf · Non-request-free frontier exposes a shared output up to congruence · Request-free runtime outputs have an active linear subject · Runtime minimum guard leaf cannot own an equivalent dual peer · Service templates are request-free · Exposed shared requests step when declared services are available · Balanced runtime frontiers are idle or step given availability

TheoremRequest-freeness is invariant under lifting#✓fully proved

Literal shared constants are unaffected by canonical lifting.

theorem RequestFree.lift_iff (Γ : ServiceEnv) (k : Nat) (p : Proc) :
    RequestFree Γ (liftProc k p) ↔ RequestFree Γ p

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Process with no exposed output on a declared shared name · Shared service environment

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Shared service signature · Injectivity of name lifting

Used byRequest-freeness is invariant under structural congruence

TheoremRequest-freeness is invariant under binder swapping#✓fully proved

Canonical binder swap does not turn a nonshared output into a shared one.

theorem RequestFree.swap_iff (Γ : ServiceEnv) (k : Nat) (p : Proc) :
    RequestFree Γ (swapProc k p) ↔ RequestFree Γ p

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Swapping adjacent binders throughout a process · Process with no exposed output on a declared shared name · Shared service environment

Proof usesChannel name in the π-calculus · Swapping adjacent de Bruijn indices in a name · Shared service signature · Injectivity of name swapping

Used byRequest-freeness is invariant under structural congruence

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.