Peer of an endpoint send head has an equivalent receive head to Swapping nested restrictions preserves conversion typing

TheoremPeer of an endpoint send head has an equivalent receive head#✓fully proved

Endpoint peer heads preserve literal advertised role/rank, independently equivalent payload and continuation branches, and payload orientation.

theorem endpoint_peer_head {c d : Capability} {r : Role} {k : Nat} {t s : Protocol}
    (he : d.Equivalent c.dual) (hh : c.protocol.unfold = .sendEndpoint r k t s) :
    ∃ v u, d.protocol.unfold = .recvEndpoint r k v u ∧ v.TreeEquiv t ∧ u.TreeEquiv s.dual

Uses 13 · Used by 4

Statement usesEndpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesFinite guarded regular protocol graph · Head and branch matching of protocols up to a child relation · Tree-equivalent protocols have matching heads · Protocol tree equivalence is symmetric · Unfolding commutes with protocol duality

Used byEndpoint delegation preserves conversion typing · Endpoint head communication preserves conversion ranked typing · Same-name conversion guards are opposite and communicate · Endpoint head communication preserves runtime typing

TheoremInput inversion for conversion typing#✓fully proved

Input inversion retains its actual advertised code and typed continuation.

theorem HasType.inp_inv {n : Nat} {Δ : Context} {a : Name} {p : Proc}
    (h : HasType n Δ (.inp a p)) :
    ∃ e c, e.name = a ∧ Δ.lookup e = some c ∧
      ((∃ s, c.protocol.unfold = .recvName s ∧
          HasType (n + 1) (Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)) p) ∨
       ∃ r k t s, c.protocol.unfold = .recvEndpoint r k t s ∧
          HasType (n + 1)
            ((Context.lift 0 (Δ.insert e ⟨c.rank, s⟩)).insert ⟨.var 0, r⟩ ⟨k, t⟩) p)

Uses 14 · Used by 2

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Lifting an ownership map past a binder · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesName scoped at a binder depth · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction

Used byEndpoint delegation preserves conversion typing · Passive head communication preserves conversion typing

TheoremPassive head communication preserves conversion typing#✓fully proved

GENERAL passive communicating-head preservation at a semantically compatible actual split, with literal receiver-tail and rank evidence.

theorem passive_head_preservation {n : Nat} {Γ Θ : Context} {e : Key} {c : Capability}
    {s : Protocol} {b : Name} {p q : Proc}
    (hd : Finmap.Disjoint Γ Θ) (hc : Γ.lookup e = some c)
    (hh : c.protocol.unfold = .sendName s)
    (hp : HasType n (Γ.insert e ⟨c.rank, s⟩) p) (hq : HasType n Θ (.inp e.name q))
    (hb : b.ClosedAt n) (hco : Compatible (Γ ∪ Θ)) :
    ∃ d u, Θ.lookup e.opposite = some d ∧ d.rank = c.rank ∧
      d.protocol.unfold = .recvName u ∧ u.TreeEquiv s.dual ∧
      HasType n (((Γ ∪ Θ).insert e ⟨c.rank, s⟩).insert e.opposite ⟨d.rank, u⟩)
        (.par p (PiCalculus.subst q b))

Uses 26 · 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 · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesEquivalence of endpoint capabilities · Dual of an endpoint capability · Updating an owned key preserves a disjoint split · Lifting an ownership map past a binder · Updating owned keys on both sides of a disjoint union · Input inversion for conversion typing · Passive name substitution preserves conversion typing · Communicating subjects have semantically dual capabilities · Peer of a passive send head has an equivalent receive head · Finite guarded regular protocol graph · Disjoint owned keys on one name have opposite roles

Used byHead communication preserves conversion typing

TheoremEndpoint delegation preserves conversion typing#✓fully proved

At an initially semantically compatible disjoint split, endpoint head communication transfers EXACT v, retaining the receiver's separately equivalent advertised payload/tail codes.

theorem endpoint_head_preservation {n k : Nat} {Γ Θ : Context} {e f : Key}
    {c v : Capability} {t s : Protocol} {p q : Proc}
    (hd : Finmap.Disjoint Γ Θ) (hc : Γ.lookup e = some c)
    (hh : c.protocol.unfold = .sendEndpoint f.role k t s)
    (hv : Γ.lookup f = some v) (hvt : v.Equivalent ⟨k, t⟩) (hne : e ≠ f)
    (hp : HasType n ((Γ.erase f).insert e ⟨c.rank, s⟩) p)
    (hq : HasType n Θ (.inp e.name q)) (hb : f.name.ClosedAt n)
    (hco : Compatible (Γ ∪ Θ)) :
    ∃ d t' u, Θ.lookup e.opposite = some d ∧ d.rank = c.rank ∧
      d.protocol.unfold = .recvEndpoint f.role k t' u ∧ t'.TreeEquiv t ∧ u.TreeEquiv s.dual ∧
      HasType n (((Γ ∪ Θ).insert e ⟨c.rank, s⟩).insert e.opposite ⟨d.rank, u⟩)
        (.par p (PiCalculus.subst q f.name))

Uses 28 · 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 · Semantic peer compatibility of an ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesTransitivity of capability equivalence · Dual of an endpoint capability · Capability transfer with carrier updates preserves disjointness · Lifting an ownership map past a binder · Combined context after delegation and two carrier updates · Input inversion for conversion typing · Endpoint substitution with freshness from a disjoint split · Communicating subjects have semantically dual capabilities · Peer of an endpoint send head has an equivalent receive head · Finite guarded regular protocol graph · Protocol tree equivalence is symmetric · Disjoint owned keys on one name have opposite roles

Used byHead communication preserves conversion typing

TheoremHead update leaves other lookups unchanged#✓fully proved

Exact two-insert head updates leave every other actual lookup unchanged, without requiring the receiver-tail code to equal the sender's dual.

theorem head_update_other (Δ : Context) (e x : Key) (c d : Capability)
    (hx : x ≠ e) (hp : x ≠ e.opposite) :
    ((Δ.insert e c).insert e.opposite d).lookup x = Δ.lookup x

Uses 6 · Used by 4

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Peer endpoint key · Endpoint role on a π name

Used byHead update leaves the transmitted payload slot unchanged · Semantic advancement preserves balance · Semantic advancement preserves compatibility · Semantic advancement preserves capability ranks

TheoremHead communication preserves conversion typing#✓fully proved

A typed opposite-head pair at an initially semantically compatible interface yields packed literal-head preservation. Both actual heads and payload/tail correspondence are conclusions, not fields in a protocol or admission predicate.

theorem HasType.head_preservation {n : Nat} {Δ : Context} {a b : Name} {p q : Proc}
    (h : HasType n Δ (.par (.out a b p) (.inp a q))) (hco : Compatible Δ) :
    ∃ e c d s u, e.name = a ∧ Δ.lookup e = some c ∧ Δ.lookup e.opposite = some d ∧
      d.rank = c.rank ∧ u.TreeEquiv s.dual ∧
      ((c.protocol.unfold = .sendName s ∧ d.protocol.unfold = .recvName u) ∨
       ∃ f v k t t', f.name = b ∧ Δ.lookup f = some v ∧ v.Equivalent ⟨k, t⟩ ∧
         c.protocol.unfold = .sendEndpoint f.role k t s ∧
         d.protocol.unfold = .recvEndpoint f.role k t' u ∧ t'.TreeEquiv t) ∧
      HasType n ((Δ.insert e ⟨c.rank, s⟩).insert e.opposite ⟨d.rank, u⟩)
        (.par p (PiCalculus.subst q b))

Uses 21 · Used by 1

Statement usesChannel name in the π-calculus · 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 · Semantic peer compatibility of an ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesName scoped at a binder depth · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Endpoint delegation preserves conversion typing · Passive head communication preserves conversion typing

Used byTyped head communication yields a semantic advancement

TheoremHead update leaves the transmitted payload slot unchanged#✓fully proved

A transmitted payload slot is literally unchanged in the combined map; its peer role may coexist, but it is neither carrier update key.

theorem endpoint_payload_after {Γ Θ : Context} {e f : Key} {c v : Capability}
    (hd : Finmap.Disjoint Γ Θ) (hv : Γ.lookup f = some v) (hp : Θ.lookup e.opposite = some c)
    (hne : e ≠ f) (x y : Capability) :
    (((Γ ∪ Θ).insert e x).insert e.opposite y).lookup f = some v

Uses 7

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized endpoint key · Peer endpoint key · Endpoint role on a π name

Proof usesHead update leaves other lookups unchanged

TheoremLowering a lifted process preserves conversion typing#✓fully proved

Canonical lowering removes only actual outer lifted keys, preserving all conversion typing without a closed-hole restriction.

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

Uses 14 · 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 · Conversion-enabled endpoint typing judgement · Polarized endpoint key

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 · Passive name substitution preserves conversion typing · Substitution cancels process lifting

Used byReverse scope extrusion preserves conversion typing

TheoremForward scope extrusion preserves conversion typing#✓fully proved

The forward canonical scope rule preserves the exact external context and ambient depth, with the dual pair derived from restriction typing.

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

Uses 15 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

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 · Lifting past a binder preserves conversion typing · Restriction inversion for conversion typing · Parallel inversion for conversion typing · Polarized endpoint key · Endpoint role on a π name

Used byScope extrusion preserves conversion typing in both directions

TheoremAdding a role unused by the partner preserves conversion typing#✓fully proved

A role missing from one component can be reattached only after actual absence in its typed partner derives completion of the advertised capability.

theorem HasType.insert_from_absent_partner {n : Nat} {Γ Ξ : 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 12 · 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 · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Absence of a physical name from a process · Endpoint role on a π name

Proof usesReinserting an owned capability changes nothing · Owned capabilities with absent names are completed · Weakening conversion typing by a completed capability

Used byRestoring the bound pair to the restricted component

TheoremRestoring the bound pair to the restricted component#✓fully proved

In the actual scope split, either freshly bound role can be moved back to the restricted component only when partner absence proves it completed.

theorem HasType.restore_scope_pair {n : Nat} {Δ Γ Ξ : 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 · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesName scoped at a binder depth · Negative role lookup after restriction binding · Positive role lookup after restriction binding · Adding a role unused by the partner preserves conversion typing · Absence of a physical name from a process · The inserted name is absent from a lifted process

Used byReverse scope extrusion preserves conversion typing

TheoremReverse scope extrusion preserves conversion typing#✓fully proved

Reverse scope transport recovers the exact external ownership split from the actual restriction/parallel typing, with no closed-hole premise.

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

Uses 27 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

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 · Erasing a role with an absent name preserves typing · Restriction inversion for conversion typing · Parallel inversion for conversion typing · Restoring the bound pair to the restricted component · Lowering a lifted process preserves conversion typing · Polarized endpoint key · Absence of a physical name from a process · Endpoint role on a π name · The inserted name is absent from a lifted process

Used byScope extrusion preserves conversion typing in both directions

TheoremScope extrusion preserves conversion typing in both directions#✓fully proved

Both directions of the canonical scope congruence preserve exact external polarized ownership and the unchanged ambient binder depth.

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

Uses 6 · Used by 1

Statement usesProcesses of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesForward scope extrusion preserves conversion typing · Reverse scope extrusion preserves conversion typing

Used byStructural congruence preserves conversion typing

TheoremParallel commutation preserves conversion typing#✓fully proved

Parallel commutation swaps a derived disjoint split, not its capabilities.

theorem HasType.par_comm {n : Nat} {Δ : Context} {p q : Proc}
    (h : HasType n Δ (.par p q)) : HasType n Δ (.par q p)

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Parallel inversion for conversion typing · Polarized endpoint key · Endpoint role on a π name

Used byStructural congruence preserves conversion typing

TheoremParallel reassociation preserves conversion typing#✓fully proved

Parallel reassociation preserves the actual three-way disjoint split.

theorem HasType.par_assoc {n : Nat} {Δ : Context} {p q r : Proc}
    (h : HasType n Δ (.par (.par p q) r)) :
    HasType n Δ (.par p (.par q r))

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Parallel inversion for conversion typing · Polarized endpoint key · Endpoint role on a π name

Used byStructural congruence preserves conversion typing

TheoremReverse parallel reassociation preserves conversion typing#✓fully proved

Reverse reassociation recovers both sub-splits from the supplied typing.

theorem HasType.par_assoc_reverse {n : Nat} {Δ : Context} {p q r : Proc}
    (h : HasType n Δ (.par p (.par q r))) :
    HasType n Δ (.par (.par p q) r)

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Parallel inversion for conversion typing · Polarized endpoint key · Endpoint role on a π name

Used byStructural congruence preserves conversion typing

TheoremAdding a parallel nil preserves conversion typing#✓fully proved

Adding a parallel nil allocates it no ownership; no active slot is dropped.

theorem HasType.par_nil_intro {n : Nat} {Δ : Context} {p : Proc}
    (h : HasType n Δ p) : HasType n Δ (.par p .nil)

Uses 11 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Completed ownership map · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byStructural congruence preserves conversion typing

TheoremRemoving a restriction around nil preserves conversion typing#✓fully proved

Restriction of nil has exactly the completed external ownership of nil.

theorem HasType.nu_nil_elim {n : Nat} {Δ : Context}
    (h : HasType n Δ (.nu .nil)) : HasType n Δ .nil

Uses 15 · Used by 2

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesChannel name in the π-calculus · Substitution for the innermost bound variable of a process · Endpoint capability with a dependency rank · Binding a fresh dual pair under restriction · Erasing the bound pair leaves the lifted context · Lifting an ownership map past a binder · Erasing a role with an absent name preserves typing · Restriction inversion for conversion typing · Passive name substitution preserves conversion typing · Polarized endpoint key · Absence of a physical name from a process · Endpoint role on a π name

Used byStructural congruence preserves conversion typing · Removing a restriction around nil preserves conversion ranked typing

TheoremAdding a restriction around nil preserves conversion typing#✓fully proved

A completed fresh pair may be introduced around nil while retaining all original external capabilities and scope.

theorem HasType.nu_nil_intro {n : Nat} {Δ : Context}
    (h : HasType n Δ .nil) : HasType n Δ (.nu .nil)

Uses 15 · Used by 2

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Endpoint capability with a dependency rank · Dual of an endpoint capability · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Lifting past a binder preserves conversion typing · Typed nil admits a completed scoped capability · Polarized endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byStructural congruence preserves conversion typing · Restricting nil preserves conversion ranked typing

TheoremSwapping nested restrictions preserves conversion typing#✓fully proved

Nested restriction commutation swaps their derived complete dual pairs.

theorem HasType.nu_swap {n : Nat} {Δ : Context} {p : Proc}
    (h : HasType n Δ (.nu (.nu p))) :
    HasType n Δ (.nu (.nu (swapProc 0 p)))

Uses 10 · Used by 2

Statement usesProcesses of the π-calculus · Swapping adjacent binders throughout a process · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement

Proof usesEndpoint capability with a dependency rank · Binding a fresh dual pair under restriction · Swapping two ambient binders in an ownership context · Swapping nested restrictions exchanges their bound pairs · Restriction inversion for conversion typing · Swapping adjacent binders preserves conversion typing

Used byStructural congruence preserves conversion typing · Reverse restriction swap preserves conversion typing

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.