Conversion-typed processes have no sum or replication to Peer of a passive send head has an equivalent receive head

TheoremConversion-typed processes have no sum or replication#✓fully proved

Typing excludes sum and repl by syntax, not by a caller fragment premise.

theorem HasType.finiteLinear {n : Nat} {Δ : Context} {p : Proc} (h : HasType n Δ p) :
    FiniteLinear p

Uses 15 · Used by 5

Statement usesProcesses of the π-calculus · Finite endpoint ownership map · Conversion-enabled endpoint typing judgement · Finite linear π fragment without choice or replication

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · 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 · 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 · Subject reduction at a compatible conversion interface · Structural congruence preserves conversion ranked typing · Conversion-ranked processes have a typed frontier normal form · Conversion ranked subject reduction at compatible interfaces

TheoremParallel inversion for conversion typing#✓fully proved

Parallel inversion derives its actual disjoint map split.

theorem HasType.par_inv {n : Nat} {Δ : Context} {p q : Proc} (h : HasType n Δ (.par p q)) :
    ∃ Γ Θ, Δ = Γ ∪ Θ ∧ Finmap.Disjoint Γ Θ ∧ HasType n Γ p ∧ HasType n Θ q

Uses 14 · Used by 8

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

Used byRemoving a parallel nil preserves conversion typing · Parallel reassociation preserves conversion typing · Reverse parallel reassociation preserves conversion typing · Parallel commutation preserves conversion typing · Forward scope extrusion preserves conversion typing · Reverse scope extrusion preserves conversion typing · Structural congruence preserves conversion typing · Subject reduction at a compatible conversion interface

TheoremRestriction inversion for conversion typing#✓fully proved

The private pair comes from the actual restriction derivation.

theorem HasType.nu_inv {n : Nat} {Δ : Context} {p : Proc} (h : HasType n Δ (.nu p)) :
    ∃ c, HasType (n + 1) (Context.bind c Δ) p

Uses 14 · Used by 7

Statement usesProcesses of the π-calculus · Endpoint capability with a dependency rank · Finite endpoint ownership map · Binding a fresh dual pair under restriction · Conversion-enabled endpoint typing judgement

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

Used byRemoving a restriction around nil preserves conversion typing · Swapping nested restrictions preserves conversion typing · Forward scope extrusion preserves conversion typing · Reverse scope extrusion preserves conversion typing · Structural congruence preserves conversion typing · Subject reduction at a compatible conversion interface · Restricting nil preserves conversion ranked typing

TheoremNil inversion for conversion typing#✓fully proved

Nil exposes actual completed ownership and key scope.

theorem HasType.nil_inv {n : Nat} {Δ : Context} (h : HasType n Δ .nil) :
    Δ.Completed ∧ (∀ e ∈ Δ, e.name.ClosedAt n)

Uses 14 · Used by 5

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 · Completed ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key

Proof usesEquivalence of endpoint capabilities · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Used byTyped nil admits a completed scoped capability · Removing a parallel nil preserves conversion typing · Minimum active role is the subject of a conversion frontier leaf · Nil typing lifts to conversion ranked typing · Removing a parallel nil preserves conversion ranked typing

TheoremTyped nil admits a completed scoped capability#✓fully proved

Only a scoped actually completed capability can be added at nil.

theorem HasType.nil_insert {n : Nat} {Δ : Context} {e : Key} {c : Capability}
    (h : HasType n Δ .nil) (hc : c.protocol.unfold = .done) (he : e.name.ClosedAt n) :
    HasType n (Δ.insert e c) .nil

Uses 13 · Used by 2

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 · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesCompleted ownership map · Inserting a completed capability preserves completion · Nil inversion for conversion typing

Used byWeakening conversion typing by a completed capability · Adding a restriction around nil preserves conversion typing

TheoremWeakening conversion typing by a completed capability#✓fully proved

An unused completed endpoint may be added through every current typing constructor. Scope and freshness are explicit; active weakening is not admitted.

theorem HasType.weaken_completed {n : Nat} {Δ : Context} {p : Proc}
    (h : HasType n Δ p) {z : Key} {u : Capability} (hz : z ∉ Δ)
    (hu : u.protocol.unfold = .done) (hscope : z.name.ClosedAt n) :
    HasType n (Δ.insert z u) p

Uses 26 · Used by 2

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 · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesLifting free de Bruijn indices of a π-calculus name · Equivalence of endpoint capabilities · Completed ownership map · Binding a fresh dual pair under restriction · Restriction binding commutes with inserting an outer key · Inserting a key absent from the other side preserves disjointness · Erasing a different key commutes with insertion · Restriction binding preserves absence of an outer key · Updating an owned key keeps absent keys absent · Lifting preserves absence of a key · Lifting an ownership map past a binder · Context lifting commutes with insertion · Typed nil admits a completed scoped capability · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · Lifting preserves and reflects name scoping

Used byWeakening conversion typing by a disjoint completed context · Adding a role unused by the partner preserves conversion typing

TheoremWeakening conversion typing by a disjoint completed context#✓fully proved

A disjoint completed context can be reattached to any typed process, with the exact finite-map union required by parallel-nil congruence.

theorem HasType.weaken_completed_union {n : Nat} {Δ Θ : Context} {p : Proc}
    (h : HasType n Δ p) (hd : Finmap.Disjoint Δ Θ) (hc : Θ.Completed)
    (hs : ∀ e ∈ Θ, e.name.ClosedAt n) : HasType n (Δ ∪ Θ) p

Uses 13 · 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 · Completed ownership map · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesErasing a key preserves completion · Inserting a left-absent key into a union updates the right part · Moving a capability across a union preserves the union · Weakening conversion typing by a completed capability

Used byRemoving a parallel nil preserves conversion typing

TheoremRemoving a parallel nil preserves conversion typing#✓fully proved

Removing a parallel nil reattaches exactly its completed ownership; no active capability is silently dropped.

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

Uses 12 · 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 · Nil inversion for conversion typing · Parallel inversion for conversion typing · Weakening conversion typing by a disjoint completed context · Polarized endpoint key · Endpoint role on a π name

Used byStructural congruence preserves conversion typing

TheoremErasing a role with an absent name preserves typing#✓fully proved

A role can be erased when its physical name is absent from every subject, payload and binder-adjusted continuation position of the typed term.

theorem HasType.erase_nameAbsent {n : Nat} {Δ : Context} {p : Proc}
    (h : HasType n Δ p) {z : Key} (hab : NameAbsent z.name p) :
    HasType n (Δ.erase z) p

Uses 24 · Used by 2

Statement usesChannel name in the π-calculus · 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 usesName scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus name · Equivalence of endpoint capabilities · Completed ownership map · Erasing a key preserves completion · Binding a fresh dual pair under restriction · Restriction binding commutes with erasing an owned outer key · Erasing a different key commutes with insertion · Erasing an absent key changes nothing · Erasure distributes over union · Lifting an ownership map past a binder · Context lifting commutes with erasing an owned key · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol

Used byRemoving a restriction around nil preserves conversion typing · Reverse scope extrusion preserves conversion typing

TheoremOwned capabilities with absent names are completed#✓fully proved

An owned capability with no physical-name occurrence must already be completed. This is derived from typing, including endpoint payload positions.

theorem HasType.absent_lookup_completed {n : Nat} {Δ : Context} {p : Proc}
    (h : HasType n Δ p) {z : Key} {t : Capability}
    (hz : Δ.lookup z = some t) (hab : NameAbsent z.name p) :
    t.protocol.unfold = .done

Uses 20 · Used by 2

Statement usesChannel name in the π-calculus · 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 protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name

Proof usesName scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus name · Equivalence of endpoint capabilities · Dual of an endpoint capability · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Lookups in a lifted ownership map · A lifted key is never a freshly bound key · Renaming the physical name of an endpoint key

Used byAdding a role unused by the partner preserves conversion typing · Adding a role unused by the partner preserves conversion ranked typing

TheoremRetyping along ownership-map equivalence#✓fully proved

GENERAL arbitrary-depth, arbitrary-context retyping, by all seven typing constructors. Target ownership, ranks and every unfolded branch are derived.

theorem HasType.retype {n : Nat} {Δ Ξ : Context} {p : Proc}
    (h : HasType n Δ p) (he : ContextEquivalent Δ Ξ) : HasType n Ξ p

Uses 30 · Used by 2

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

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Reflexivity of capability equivalence · Symmetry of capability equivalence · Transitivity of capability equivalence · Completed ownership map · Binding a fresh dual pair under restriction · Lifting an ownership map past a binder · Binding equivalent fresh pairs preserves ownership-map equivalence · Ownership-map equivalence preserves completion · Erasure preserves ownership-map equivalence · Equivalent insertions preserve ownership-map equivalence · Lifting preserves ownership-map equivalence · Lookups transfer along ownership-map equivalence · Ownership-map equivalence preserves key scoping · Equivalence of a disjoint union splits into equivalent parts · Finite guarded regular protocol graph · Head and branch matching of protocols up to a child relation · Polarized endpoint key · Endpoint protocol with guarded regular recursion · Regular-tree equivalence of protocols as bisimilarity · Tree-equivalent protocols have matching heads · One-step unfolding of a protocol · Endpoint role on a π name

Used byOwnership-map equivalence preserves typing in both directions · Endpoint substitution preserves conversion typing

TheoremOwnership-map equivalence preserves typing in both directions#✓fully proved

Equivalence transports typing in BOTH directions at the same process/depth.

theorem HasType.retype_iff {n : Nat} {Δ Ξ : Context} {p : Proc}
    (he : ContextEquivalent Δ Ξ) : HasType n Δ p ↔ HasType n Ξ p

Uses 6

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

Proof usesSymmetry of ownership-map equivalence · Retyping along ownership-map equivalence

TheoremCollision-free renaming preserves conversion typing#✓fully proved

GENERAL name transport with collision freedom on actual owned keys and canonical ambient name scope; protocol codes, roles and ranks stay exact.

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

Uses 33 · 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 · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Renaming the physical name of an endpoint key · 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 · Endpoint protocol with guarded regular recursion · One-step unfolding of a protocol · Endpoint role on a π name · Extension of a name map under a binder · Extending a scoped name map under a binder keeps it scoped

Used byLifting past a binder preserves conversion typing · Endpoint substitution preserves conversion typing · Passive name substitution preserves conversion typing · Swapping adjacent binders preserves conversion typing

TheoremLifting past a binder preserves conversion typing#✓fully proved

Lift uses the canonical cutoff-aware name and process operations.

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

Uses 18 · Used by 2

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 · Conversion-enabled endpoint typing judgement

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 · Collision-free renaming preserves conversion typing · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Injectivity of name lifting · Capture-safe renaming of processes · Process renaming by a lift is process lifting

Used byAdding a restriction around nil preserves conversion typing · Forward scope extrusion preserves conversion typing

TheoremSwapping adjacent binders preserves conversion typing#✓fully proved

Swap retains roles, protocols and ranks while permuting two ambient binders.

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

Uses 18 · 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 · Conversion-enabled endpoint 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 · Collision-free rekeying of an ownership map · Collision-free renaming preserves conversion 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 bySwapping nested restrictions preserves conversion typing

TheoremEndpoint substitution preserves conversion typing#✓fully proved

GENERAL endpoint substitution: retain the ACTUAL transmitted capability's code and rank at the sent polarized key, allowing its opposite-role alias. Collision freedom is needed only for that exact key and canonical substitution.

theorem HasType.subst_endpoint {n : Nat} {Δ : 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) ∉ Δ) :
    HasType n (Δ.insert ⟨b, r⟩ v) (PiCalculus.subst p b)

Uses 25 · 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 · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Endpoint role on a π name

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 · Collision-free renaming preserves conversion typing · Retyping along ownership-map equivalence · Renaming the physical name of an endpoint key · Capture-safe renaming of processes · Process renaming by a substitution is process substitution

Used byEndpoint substitution with freshness from a disjoint split

TheoremEndpoint substitution with freshness from a disjoint split#✓fully proved

GENERAL split-derived freshness: actual payload ownership and the receiver's already-owned carrier derive non-aliasing even after advancement.

theorem HasType.subst_endpoint_from_split {n : Nat} {Γ Θ : Context} {b : Name} {r : Role}
    {c v old next : Capability} {e : Key} {p : Proc}
    (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 14 · 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 · Conversion-enabled endpoint typing judgement · Polarized endpoint key · Endpoint role on a π name

Proof usesUpdating an owned key keeps absent keys absent · Owned keys are absent from the other side of a disjoint split · Endpoint substitution preserves conversion typing

Used byEndpoint delegation preserves conversion typing

TheoremPassive name substitution preserves conversion typing#✓fully proved

GENERAL passive substitution transports all scoped positions but adds NO capability. The input context contains only lifted outer ownership.

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

Uses 19 · Used by 3

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 · Conversion-enabled endpoint typing judgement

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 · Collision-free renaming preserves conversion typing · Polarized endpoint key · Renaming the physical name of an endpoint key · Capture-safe renaming of processes · Process renaming by a substitution is process substitution

Used byRemoving a restriction around nil preserves conversion typing · Passive head communication preserves conversion typing · Lowering a lifted process preserves conversion typing

TheoremCommunicating subjects have semantically dual capabilities#✓fully proved

At a semantically compatible combined interface, actual disjoint same-name ownership derives opposite roles, literal cap-rank agreement and semantic duality, not raw capability equality.

theorem communicating_equivalent {Γ Θ : Context} {e f : Key} {c d : Capability}
    (hd : Finmap.Disjoint Γ Θ) (hc : Γ.lookup e = some c) (hp : Θ.lookup f = some d)
    (hn : e.name = f.name) (hco : Compatible (Γ ∪ Θ)) : d.Equivalent c.dual

Uses 10 · Used by 8

Statement usesChannel name in the π-calculus · Endpoint capability with a dependency rank · Equivalence of endpoint capabilities · Dual of an endpoint capability · Finite endpoint ownership map · Semantic peer compatibility of an ownership map · Polarized endpoint key · Endpoint role on a π name

Proof usesPeer endpoint key · Disjoint owned keys on one name have opposite roles

Used byEndpoint delegation preserves conversion typing · Passive head communication preserves conversion typing · Endpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Same-name conversion guards are opposite and communicate · Endpoint head communication preserves runtime typing · Passive head communication preserves runtime typing · Same-name linear guards at a compatible interface communicate

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

Semantic duality forces an actual receive-name head and equivalent tail, while keeping the receiver's literal continuation code.

theorem passive_peer_head {c d : Capability} {s : Protocol}
    (he : d.Equivalent c.dual) (hh : c.protocol.unfold = .sendName s) :
    ∃ u, d.protocol.unfold = .recvName u ∧ 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

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 · Endpoint role on a π name

Used byPassive head communication preserves conversion typing · Passive head communication preserves conversion ranked typing · Same-name conversion guards are opposite and communicate · Passive head communication preserves runtime typing

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.