WeightedNetKAT.rSafety

source

def Listed.Li.getSum {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] :

Fin (size (α ⊕ β)) ≃ Fin (size α) ⊕ Fin (size β)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Listed.Li.getProd {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] :

Fin (size (α × β)) ≃ Fin (size α) × Fin (size β)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Listed.decodeFin_getSum {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : Fin (size (α ⊕ β))) :

decodeFin i = Sum.map decodeFin decodeFin (Li.getSum i)

source

theorem Listed.decodeFin_getProd {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : Fin (size (α × β))) :

decodeFin i = Prod.map decodeFin decodeFin (Li.getProd i)

source

@[simp]

theorem Listed.Li.getSum_encodeFin {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : α ⊕ β) :

getSum (encodeFin i) = Sum.map encodeFin encodeFin i

source

@[simp]

theorem Listed.Li.getProd_encodeFin {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : α × β) :

getProd (encodeFin i) = Prod.map encodeFin encodeFin i

source

def EMatrix.ofFn_eq_ofFnSlow {m : Type u_1} {n : Type u_2} {α : Type u_3} [Listed m] [Listed n] (f : Li[m] → Li[n] → α) :

ofFn f = ofFnSlow fun (a : m) (b : n) => f (Listed.encodeFin a) (Listed.encodeFin b)

Equations

⋯ = ⋯

Instances For

source

def WeightedNetKAT.rSafety {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (p : Pol[F,N,𝒮]) (r : 𝒮) :

Prop

Equations

WeightedNetKAT.rSafety p r = ∀ (π : Pk[F,N]) (h : Pk[F,N] × List Pk[F,N]), (p.sem (π, [])) h ≤ r

Instances For

source

inductive WeightedNetKAT.rSafety.Q'₀ :

Type

qι : Q'₀
q𝒪 : Q'₀

Instances For

source

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instDecidableEqQ'₀ :

DecidableEq Q'₀

Equations

WeightedNetKAT.rSafety.instDecidableEqQ'₀ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instFintypeQ'₀ :

Fintype Q'₀

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instListedQ'₀ :

Listed Q'₀

Equations

One or more equations did not get rendered due to their size.

source

@[reducible, inline]

abbrev WeightedNetKAT.rSafety.Q' (F N Q : Type) [Listed F] :

Type

Equations

WeightedNetKAT.rSafety.Q' F N Q = (Q × Pk[F,N] ⊕ WeightedNetKAT.rSafety.Q'₀)

Instances For

source

def WeightedNetKAT.rSafety.I {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] {Q 𝒮 : Type} [DecidableEq Q] [Semiring 𝒮] :

Matrix Unit (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.I = WeightedNetKAT.η₂ () (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι)

Instances For

source

def WeightedNetKAT.rSafety.Δ {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] {Q 𝒮 : Type} [Semiring 𝒮] (𝔄 : WNKA[F,N,𝒮,Q]) (β : Pk[F,N]) :

Matrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inl (q, α)) (Sum.inl (q', β')) = if β = β' then 𝔄.δ α β q q' else 0
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι) (Sum.inl (q, β')) = if β = β' then 𝔄.ι () q else 0
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inl (q, α)) (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) = 𝔄.𝒪 α β q ()
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) = 0
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι) = 0
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) (Sum.inl val) = 0
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι) (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) = 0
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι) (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι) = 0
WeightedNetKAT.rSafety.Δ 𝔄 β (Sum.inl val) (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι) = 0

Instances For

source

def WeightedNetKAT.rSafety.Λ {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] {Q 𝒮 : Type} [DecidableEq Q] [Semiring 𝒮] :

Matrix (Q' F N Q) Unit 𝒮

Equations

WeightedNetKAT.rSafety.Λ = WeightedNetKAT.η₂ (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) ()

Instances For

source

def WeightedNetKAT.rSafety.Δ_star {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Fintype Q] [DecidableEq Q] [Semiring 𝒮] (𝔄 : WNKA[F,N,𝒮,Q]) :

List Pk[F,N] → Matrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.Δ_star 𝔄 [] = 1
WeightedNetKAT.rSafety.Δ_star 𝔄 (α :: x_1) = WeightedNetKAT.rSafety.Δ 𝔄 α * WeightedNetKAT.rSafety.Δ_star 𝔄 x_1

Instances For

source

def WeightedNetKAT.rSafety.M {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Semiring 𝒮] (𝔄 : WNKA[F,N,𝒮,Q]) :

Matrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.M 𝔄 = ∑ α : Pk[F,N], WeightedNetKAT.rSafety.Δ 𝔄 α

Instances For

source

noncomputable def WeightedNetKAT.rSafety.M_star {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Fintype Q] [DecidableEq Q] [Semiring 𝒮] (𝔄 : WNKA[F,N,𝒮,Q]) [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] :

Matrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.M_star 𝔄 = KStar.kstar (WeightedNetKAT.rSafety.M 𝔄)

Instances For

source

noncomputable def WeightedNetKAT.rSafety.sem' {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Fintype Q] [DecidableEq Q] [Semiring 𝒮] (𝔄 : WNKA[F,N,𝒮,Q]) [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed Q] [KStar 𝒮] :

𝒮

Equations

WeightedNetKAT.rSafety.sem' 𝔄 = (WeightedNetKAT.rSafety.I * WeightedNetKAT.rSafety.M_star 𝔄 * WeightedNetKAT.rSafety.Λ) () ()

Instances For

source

def WeightedNetKAT.rSafety.EI {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] :

EMatrix Unit (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.EI = WeightedNetKAT.Eη₂ () (Sum.inr WeightedNetKAT.rSafety.Q'₀.qι)

Instances For

source

def WeightedNetKAT.rSafety.EΔ {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) (β : Li[Pk[F,N]]) :

EMatrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def WeightedNetKAT.rSafety.EΛ {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] :

EMatrix (Q' F N Q) Unit 𝒮

Equations

WeightedNetKAT.rSafety.EΛ = WeightedNetKAT.Eη₂ (Sum.inr WeightedNetKAT.rSafety.Q'₀.q𝒪) ()

Instances For

source

def WeightedNetKAT.rSafety.EΔ_star {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) :

List Li[Pk[F,N]] → EMatrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.EΔ_star 𝔈 [] = 1
WeightedNetKAT.rSafety.EΔ_star 𝔈 (α :: xs) = WeightedNetKAT.rSafety.EΔ 𝔈 α * WeightedNetKAT.rSafety.EΔ_star 𝔈 xs

Instances For

source

def WeightedNetKAT.rSafety.EΔ_star' {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) (acc : EMatrix Unit (Q' F N Q) 𝒮) :

List Li[Pk[F,N]] → EMatrix Unit (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.EΔ_star' 𝔈 acc [] = acc
WeightedNetKAT.rSafety.EΔ_star' 𝔈 acc (α :: xs) = WeightedNetKAT.rSafety.EΔ_star' 𝔈 (acc * WeightedNetKAT.rSafety.EΔ 𝔈 α) xs

Instances For

source

def WeightedNetKAT.rSafety.Esem {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) :

List Li[Pk[F,N]] → 𝒮

Equations

WeightedNetKAT.rSafety.Esem 𝔈 x = (WeightedNetKAT.rSafety.EΔ_star' 𝔈 WeightedNetKAT.rSafety.EI x * WeightedNetKAT.rSafety.EΛ) () ()

Instances For

source

def WeightedNetKAT.rSafety.EM {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) :

EMatrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.EM 𝔈 = ∑ α : Li[Pk[F,N]], WeightedNetKAT.rSafety.EΔ 𝔈 α

Instances For

source

def WeightedNetKAT.rSafety.EM_star {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [KStar 𝒮] :

EMatrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

WeightedNetKAT.rSafety.EM_star 𝔈 = KStar.kstar (WeightedNetKAT.rSafety.EM 𝔈)

Instances For

source

def WeightedNetKAT.rSafety.Esem' {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [KStar 𝒮] :

𝒮

Equations

WeightedNetKAT.rSafety.Esem' 𝔈 = (WeightedNetKAT.rSafety.EI * WeightedNetKAT.rSafety.EM_star 𝔈 * WeightedNetKAT.rSafety.EΛ) () ()

Instances For

source

@[simp]

theorem WeightedNetKAT.rSafety.EI_eq_I {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] :

EI = EMatrix.ofMatrix I

source

@[simp]

theorem WeightedNetKAT.rSafety.EΔ_eq_Δ {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {β : Li[Pk[F,N]]} :

EΔ 𝔈 β = EMatrix.ofMatrix (Δ 𝔈.toWNKA (Listed.decodeFin β))

source

@[simp]

theorem WeightedNetKAT.rSafety.EΛ_eq_Λ {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] :

EΛ = EMatrix.ofMatrix Λ

source

@[simp]

theorem WeightedNetKAT.rSafety.Esem'_eq_sem' {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [Fintype Q] [DecidableEq Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [KStar 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] :

Esem' 𝔈 = sem' 𝔈.toWNKA

source

def WeightedNetKAT.rSafety.ErSafety {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [LawfulKStar 𝒮] (p : Pol[F,N,𝒮]) (r : 𝒮) :

Prop

Equations

WeightedNetKAT.rSafety.ErSafety p r = (WeightedNetKAT.rSafety.Esem' p.toRPol.ewnka ≤ r)

Instances For

source

def WeightedNetKAT.rSafety.sem'_fast {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Fintype Q] [DecidableEq Q] [Semiring 𝒮] (𝔄 : WNKA[F,N,𝒮,Q]) [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed Q] [KStar 𝒮] :

𝒮

Equations

WeightedNetKAT.rSafety.sem'_fast 𝔄 = WeightedNetKAT.rSafety.Esem' 𝔄.toEWNKA

Instances For

source

def WeightedNetKAT.RPol.wnkaFast {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] (p : RPol 𝒮) :

WNKA[F,N,𝒮,S p]

Equations

p.wnkaFast = p.ewnka.toWNKA

Instances For

source

theorem WeightedNetKAT.rSafety.rSafety_iff {F : Type} [Fintype F] [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] [Inhabited Pk[F,N]] {p : Pol[F,N,𝒮]} {r : 𝒮} :

rSafety p r ↔ ∀ (x : GS F N), RPol.𝒜 ⟦~p.toRPol⟧ x ≤ r

source

theorem WeightedNetKAT.rSafety.rSafety_iff' {F : Type} [Fintype F] [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] [Inhabited Pk[F,N]] {p : Pol[F,N,𝒮]} {r : 𝒮} :

rSafety p r ↔ ω∑ (x : GS F N), RPol.𝒜 ⟦~p.toRPol⟧ x ≤ r

source

@[implicit_reducible]

def WeightedNetKAT.rSafety.instFintypeVectorPk {F : Type} [Listed F] {N : Type} [Listed N] {n : ℕ} :

Fintype (Vector Pk[F,N] n)

Equations

WeightedNetKAT.rSafety.instFintypeVectorPk = Listed.fintype

Instances For

source

theorem WeightedNetKAT.rSafety.ωSum_GS_eq_ωSum_nat {F : Type} [Fintype F] [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f : GS F N → 𝒮} :

ω∑ (x : GS F N), f x = ω∑ (n : ℕ), ∑ x ∈ Finset.univ ×ˢ Finset.univ ×ˢ Finset.univ, match x with | (α, xs, β) => f (α, xs.toList, β)

source

theorem WeightedNetKAT.rSafety.rSafety_iff'' {F : Type} [Fintype F] [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] [Inhabited Pk[F,N]] {p : Pol[F,N,𝒮]} {r : 𝒮} :

rSafety p r ↔ sem' p.toRPol.wnka ≤ r

source

theorem WeightedNetKAT.rSafety.rSafety_iff_ErSafety {F : Type} [Fintype F] [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] [Inhabited Pk[F,N]] {p : Pol[F,N,𝒮]} {r : 𝒮} :

rSafety p r ↔ ErSafety p r

source

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instDecidableErSafetyOfDecidableRelLe {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [DecidableRel fun (x1 x2 : 𝒮) => x1 ≤ x2] {p : Pol[F,N,𝒮]} {r : 𝒮} :

Decidable (ErSafety p r)

Equations

WeightedNetKAT.rSafety.instDecidableErSafetyOfDecidableRelLe = ⋯.mpr inferInstance

source

def WeightedNetKAT.rSafety.extraction_len {F : Type} [Listed F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [DecidableEq 𝒮] (n : ℕ) (r : 𝒮) :

Option (GS F N)

Enumerate all GS and check their weight

Example execution time: N/A

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def WeightedNetKAT.rSafety.extraction_len' {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [DecidableEq 𝒮] (n : ℕ) (r : 𝒮) :

Option (GS F N)

Enumerate all GS and check their weight, reusing computation up to the exit weight

Example execution time: 113.988409s

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def WeightedNetKAT.rSafety.extraction_len'' {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [DecidableEq 𝒮] (acc : EMatrix Unit Q 𝒮) (n : ℕ) (γ : Li[Pk[F,N]]) (r : 𝒮) :

Option (GS F N)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def WeightedNetKAT.rSafety.extraction_len₀ {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [DecidableEq 𝒮] (n : ℕ) (r : 𝒮) :

Option (GS F N)

Enumerate all GS and check their weight, reusing computation up for every prefix

Example execution time: 30.157497s

Equations

WeightedNetKAT.rSafety.extraction_len₀ 𝔈 n r = Array.findSome? (fun (x : Li[Pk[F,N]]) => WeightedNetKAT.rSafety.extraction_len'' 𝔈 𝔈.ι n x r) (Listed.arrayOf Li[Pk[F,N]])

Instances For

source

partial def WeightedNetKAT.rSafety.extraction_go {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [DecidableEq 𝒮] [Inhabited F] [Inhabited N] (n : ℕ) (r : 𝒮) :

GS F N

source

def WeightedNetKAT.rSafety.extraction {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [DecidableEq 𝒮] [Inhabited F] [Inhabited N] (r : 𝒮) :

GS F N

Equations

WeightedNetKAT.rSafety.extraction 𝔈 r = WeightedNetKAT.rSafety.extraction_go 𝔈 0 r

Instances For