Restoring the bound pair preserves conversion ranked typing to Global progress of conversion-ranked processes at balanced interfaces

TheoremRestoring the bound pair preserves conversion ranked typing#✓fully proved

Restoring the bound pair adds only absent completed partner roles; all original active ownership and inequalities of the restricted component remain.

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

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 · Dual of an endpoint capability · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Priority-ranked conversion typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesNegative role lookup after restriction binding · Positive role lookup after restriction binding · Adding a role unused by the partner preserves conversion ranked typing · Absence of a physical name from a process · The inserted name is absent from a lifted process

Used byReverse scope extrusion preserves conversion ranked typing

TheoremReverse scope extrusion preserves conversion ranked typing#✓fully proved

Reverse extrusion derives the entire outer ownership split from typing, removes only genuinely absent partner roles and retains all guard inequalities.

theorem RankedType.scope_reverse {n : Nat} {Δ : Context} {p q : Proc}
    (h : RankedType n Δ (.nu (.par p (liftProc 0 q)))) :
    RankedType 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 · Priority-ranked conversion 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 key whose name is absent preserves conversion ranked typing · Restriction inversion for conversion ranked typing · Parallel inversion for conversion ranked typing · Restoring the bound pair preserves conversion ranked typing · Conversion ranked typing descends from a lifted process · 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 byConversion ranked typing is invariant under scope extrusion

TheoremConversion ranked typing is invariant under scope extrusion#✓fully proved

Exact bidirectional canonical scope transport for the same refinement.

theorem RankedType.scope_iff {n : Nat} {Δ : Context} {p q : Proc} :
    RankedType n Δ (.par (.nu p) q) ↔ RankedType 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 · Priority-ranked conversion typing judgement

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

Used byStructural congruence preserves conversion ranked typing

TheoremParallel commutation preserves conversion ranked typing#✓fully proved

Commutation retains the actual disjoint split and both ranked subterms.

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

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement

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

Used byStructural congruence preserves conversion ranked typing

TheoremParallel reassociation preserves conversion ranked typing#✓fully proved

Reassociation derives all pairwise disjointness from actual typing.

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

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement

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

Used byStructural congruence preserves conversion ranked typing

TheoremReverse parallel reassociation preserves conversion ranked typing#✓fully proved

Reverse reassociation retains exact contexts and guard checks.

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

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement

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

Used byStructural congruence preserves conversion ranked typing

TheoremRemoving a parallel nil preserves conversion ranked typing#✓fully proved

Nil's actual completed ownership can be reattached without new dependencies.

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

Uses 13 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Completed ownership map · Nil inversion for conversion typing · Forgetting priorities yields conversion typing · Parallel inversion for conversion ranked typing · Weakening conversion ranked typing by a disjoint completed context · Polarized endpoint key · Endpoint role on a π name

Used byStructural congruence preserves conversion ranked typing

TheoremAdding a parallel nil preserves conversion ranked typing#✓fully proved

Nil introduction allocates an empty ownership context, not an active frame.

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

Uses 11 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion 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 ranked typing

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

Restricting nil is equivalent to its original completed/scoped interface.

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

Uses 6 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement

Proof usesRemoving a restriction around nil preserves conversion typing · Forgetting priorities yields conversion typing · Nil typing lifts to conversion ranked typing

Used byStructural congruence preserves conversion ranked typing

TheoremRestricting nil preserves conversion ranked typing#✓fully proved

A completed fresh pair can be introduced around nil without changing guards.

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

Uses 10 · Used by 1

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement

Proof usesEndpoint capability with a dependency rank · Binding a fresh dual pair under restriction · Conversion-enabled endpoint typing judgement · Restriction inversion for conversion typing · Adding a restriction around nil preserves conversion typing · Forgetting priorities yields conversion typing · Nil typing lifts to conversion ranked typing

Used byStructural congruence preserves conversion ranked typing

TheoremSwapping two restrictions preserves conversion ranked typing#✓fully proved

Swapping the two restrictions preserves all guard constraints by the GENERAL capture-safe rename theorem and the exact four-role context equation.

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

Uses 21 · Used by 2

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

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 · Binding a fresh dual pair under restriction · Collision-free rekeying of an ownership map · Swapping two ambient binders in an ownership context · Swapping nested restrictions exchanges their bound pairs · Restriction inversion for conversion ranked typing · Collision-free renaming preserves conversion ranked typing · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · 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 conversion ranked typing · Reverse restriction swap preserves conversion ranked typing

TheoremReverse restriction swap preserves conversion ranked typing#✓fully proved

Reverse restriction swap uses the canonical process involution.

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

Uses 6 · Used by 1

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

Proof usesSwapping two restrictions preserves conversion ranked typing · Process swap is an involution

Used byStructural congruence preserves conversion ranked typing

TheoremStructural congruence preserves conversion ranked typing#✓fully proved

Every canonical Cong constructor preserves the whole priority refinement at exactly the same context and ambient depth. Unsupported sum/replication constructors are impossible by the invariant DERIVED from refinement typing.

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

Uses 33 · Used by 2

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement

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 · Lifting an ownership map past a binder · Conversion-typed processes have no sum or replication · Forgetting priorities yields conversion typing · Restriction inversion for conversion ranked typing · Removing a restriction around nil preserves conversion ranked typing · Restricting nil preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Reverse restriction swap preserves conversion ranked typing · Parallel reassociation preserves conversion ranked typing · Reverse parallel reassociation preserves conversion ranked typing · Parallel commutation preserves conversion ranked typing · Parallel inversion for conversion ranked typing · Removing a parallel nil preserves conversion ranked typing · Adding a parallel nil preserves conversion ranked typing · Conversion ranked typing is invariant under scope extrusion · Finite linear π fragment without choice or replication · 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

Used byConversion-ranked processes have a typed frontier normal form · Conversion ranked subject reduction at compatible interfaces

TheoremConversion ranked subject reduction at compatible interfaces#✓fully proved

From a typed source at an initially compatible interface, all five canonical reduction constructors preserve typing and compatibility, with one matched external subject-pair advancement or an unchanged interface when communication is private. No fragment or enabled-edge premise is required.

theorem RankedType.subject_reduction {n : Nat} {Δ : Context} {p q : Proc}
    (h : RankedType n Δ p) (hco : Compatible Δ) (hs : PiCalculus.Step p q) :
    ∃ Ξ, RankedType n Ξ q ∧ Compatible Ξ ∧ (Ξ = Δ ∨ SemanticAdvance Δ Ξ)

Uses 30 · Used by 3

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Priority-ranked conversion typing judgement · Semantic advancement of a communicating endpoint pair

Proof usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Guarded-choice resolution 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 · Binding a dual private pair preserves compatibility · Compatibility restricts to the left part of a union · Compatibility restricts to the right part of a disjoint union · Conversion-typed processes have no sum or replication · Structural congruence preserves conversion ranked typing · Forgetting priorities yields conversion typing · Conversion head communication yields a semantic advance · Restriction inversion for conversion ranked typing · Parallel inversion for conversion ranked typing · Semantic advancement preserves compatibility · Semantic advancement preserves disjointness from a frame · Semantic advancement extends from the left part to the whole union · Semantic advancement extends from the right part to a disjoint union · Semantic advance under a private binding is private or outer · Finite linear π fragment without choice or replication · Polarized endpoint key · Endpoint role on a π name · Selection is trivial on the choice-free fragment

Used byFinite runs keep conversion ranked typing at compatible interfaces · Conversion ranked subject reduction at balanced interfaces · Conversion ranked subject reduction at the empty interface

TheoremConversion ranked subject reduction at balanced interfaces#✓fully proved

A typed source with a balanced initial interface retains typing and balance after any canonical step. Balance supplies the required compatibility; the exact zero-or-one external advancement evidence is retained.

theorem RankedType.subject_reduction_balanced {n : Nat} {Δ : Context} {p q : Proc}
    (h : RankedType n Δ p) (hb : Balanced Δ) (hs : PiCalculus.Step p q) :
    ∃ Ξ, RankedType n Ξ q ∧ Balanced Ξ ∧ (Ξ = Δ ∨ SemanticAdvance Δ Ξ)

Uses 10

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Priority-ranked conversion typing judgement · Semantic advancement of a communicating endpoint pair

Proof usesSemantic balance implies semantic compatibility · Semantic peer compatibility of an ownership map · Conversion ranked subject reduction at compatible interfaces · Semantic advancement preserves balance

TheoremConversion ranked subject reduction at the empty interface#✓fully proved

An empty-interface typed network retains empty-interface typing through any canonical step. The empty context is balanced, hence compatible, including communication behind restrictions and pre/post congruence.

theorem RankedType.subject_reduction_empty {n : Nat} {p q : Proc}
    (h : RankedType n ∅ p) (hs : PiCalculus.Step p q) : RankedType n ∅ q

Uses 20 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key

Proof usesChannel name in the π-calculus · Equivalence of endpoint capabilities · Dual of an endpoint capability · Semantic balance implies semantic compatibility · Matching send and receive heads of two capabilities · Semantic peer compatibility of an ownership map · Conversion ranked subject reduction at compatible interfaces · Semantic advancement of a communicating endpoint pair · The empty context is semantically balanced · Peer endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Dual of an endpoint protocol · Endpoint role on a π name

Used byReachable closed conversion-ranked states keep the empty interface

TheoremFinite runs keep conversion ranked typing at compatible interfaces#✓fully proved

A ranked-typed source at an initially semantically compatible interface retains typing and compatibility through finite actual execution, with a finite trace of faithful advances. This is safety, not progress or termination.

theorem RankedType.reachable {n : Nat} {Δ : Context} {p q : Proc} (h : RankedType n Δ p)
    (hc : Compatible Δ) (hr : Relation.ReflTransGen PiCalculus.Step p q) :
    ∃ Ξ, RankedType n Ξ q ∧ Compatible Ξ ∧ Relation.ReflTransGen SemanticAdvance Δ Ξ

Uses 7

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Priority-ranked conversion typing judgement · Semantic advancement of a communicating endpoint pair

Proof usesConversion ranked subject reduction at compatible interfaces

TheoremReachable closed conversion-ranked states keep the empty interface#✓fully proved

Every finite reachable closed state retains the exact empty interface.

theorem RankedType.reachable_empty {n : Nat} {p q : Proc} (h : RankedType n ∅ p)
    (hr : Relation.ReflTransGen PiCalculus.Step p q) : RankedType n ∅ q

Uses 7 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Polarized endpoint key

Proof usesConversion ranked subject reduction at the empty interface

Used byProgress at reachable states of closed conversion-ranked networks

TheoremConversion-ranked processes have a typed frontier normal form#✓fully proved

Normalization is derived from finite syntax, then NEW ranked Cong keeps ownership.

theorem RankedType.frontier_normal {n : Nat} {Δ : Context} {p : Proc}
    (h : RankedType n Δ p) : ∃ q, Cong p q ∧ RankedType n Δ q ∧ FrontierNormal q

Uses 9 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Finite endpoint ownership map · Priority-ranked conversion typing judgement · Frontier normal form of finite networks

Proof usesConversion-typed processes have no sum or replication · Structural congruence preserves conversion ranked typing · Forgetting priorities yields conversion typing · Every finite linear π term has a frontier normal form

Used byGlobal progress of conversion-ranked processes at balanced interfaces

TheoremGlobal progress of conversion-ranked processes at balanced interfaces#✓fully proved

For a ranked-typed process at ANY balanced interface, global progress holds, including disconnected networks. All private channels are tracked through the derived restriction tower. Completion means process congruence to nil, not completion of the interface.

theorem RankedType.progress_balanced {n : Nat} {Δ : Context} {p : Proc}
    (h : RankedType n Δ p) (hb : Balanced Δ) :
    Cong p .nil ∨ ∃ q, PiCalculus.Step p q

Uses 14 · Used by 1

Statement usesStructural congruence of π-calculus processes · Processes of the π-calculus · Reduction relation of the π-calculus · Finite endpoint ownership map · Semantic balance of a linear context · Priority-ranked conversion typing judgement

Proof usesEndpoint capability with a dependency rank · Binding a fresh dual pair under restriction · Binding a dual private pair preserves balance · Progress for semantically balanced conversion frontiers · Conversion-ranked processes have a typed frontier normal form · Restriction inversion for conversion ranked typing · Frontier normal form of finite networks · Parallel guard frontier

Used byClosed conversion-ranked networks are completed or can step

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.