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

• ⋯ = ⋯

def WeightedNetKAT.rSafety {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [DecidableEq N] {𝒮 : Type u_3} [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

inductive WeightedNetKAT.rSafety.Q'₀ : Type

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

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instDecidableEqQ'₀ : DecidableEq Q'₀

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instFintypeQ'₀ : Fintype Q'₀

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instListedQ'₀ : Listed Q'₀

Equations

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

@[reducible, inline]

abbrev WeightedNetKAT.rSafety.Q' (F : Type u_6) (N : Type u_7) (Q : Type u_8) [Listed F] : Type (max u_7 u_8)

Equations

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

def WeightedNetKAT.rSafety.I {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [DecidableEq Q] [Semiring 𝒮] : Matrix Unit (Q' F N Q) 𝒮

Equations

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

def WeightedNetKAT.rSafety.Δ {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [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

def WeightedNetKAT.rSafety.Λ {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [DecidableEq Q] [Semiring 𝒮] : Matrix (Q' F N Q) Unit 𝒮

Equations

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

def WeightedNetKAT.rSafety.Δ_star {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [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

def WeightedNetKAT.rSafety.M {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [Semiring 𝒮] (𝔄 : WNKA[F,N,𝒮,Q]) : Matrix (Q' F N Q) (Q' F N Q) 𝒮

Equations

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

noncomputable def WeightedNetKAT.rSafety.M_star {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [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 𝔄)

noncomputable def WeightedNetKAT.rSafety.sem' {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [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.Λ) () ()

def WeightedNetKAT.rSafety.EI {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [Listed Q] [Semiring 𝒮] : EMatrix Unit (Q' F N Q) 𝒮

Equations

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

def WeightedNetKAT.rSafety.EΔ {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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.

def WeightedNetKAT.rSafety.EΛ {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [Listed Q] [Semiring 𝒮] : EMatrix (Q' F N Q) Unit 𝒮

Equations

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

def WeightedNetKAT.rSafety.EΔ_star {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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

def WeightedNetKAT.rSafety.EΔ_star' {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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

def WeightedNetKAT.rSafety.Esem {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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Λ) () ()

def WeightedNetKAT.rSafety.EM {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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Δ 𝔈 α

def WeightedNetKAT.rSafety.EM_star {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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 𝔈)

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

Equations

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

@[simp]

theorem WeightedNetKAT.rSafety.EI_eq_I {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : EI = EMatrix.ofMatrix I

@[simp]

theorem WeightedNetKAT.rSafety.EΔ_eq_Δ {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [Listed Q] [DecidableEq Q] [Semiring 𝒮] (𝔈 : EWNKA[F,N,𝒮,Q]) [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {β : Li[Pk[F,N]]} : EΔ 𝔈 β = EMatrix.ofMatrix (Δ 𝔈.toWNKA (Listed.decodeFin β))

@[simp]

theorem WeightedNetKAT.rSafety.EΛ_eq_Λ {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : EΛ = EMatrix.ofMatrix Λ

@[simp]

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

def WeightedNetKAT.rSafety.ErSafety {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {𝒮 : Type u_5} [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)

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

Equations

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

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

Equations

• p.wnkaFast = p.ewnka.toWNKA

theorem WeightedNetKAT.rSafety.rSafety_iff {F : Type u_1} [Fintype F] [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {𝒮 : Type u_5} [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

theorem WeightedNetKAT.rSafety.rSafety_iff' {F : Type u_1} [Fintype F] [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {𝒮 : Type u_5} [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

@[implicit_reducible]

def WeightedNetKAT.rSafety.instFintypeVectorPk {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {n : ℕ} : Fintype (Vector Pk[F,N] n)

Equations

• WeightedNetKAT.rSafety.instFintypeVectorPk = Listed.fintype

theorem WeightedNetKAT.rSafety.ωSum_GS_eq_ωSum_nat {F : Type u_1} [Fintype F] [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {𝒮 : Type u_5} [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, β)

theorem WeightedNetKAT.rSafety.rSafety_iff'' {F : Type u_1} [Fintype F] [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {𝒮 : Type u_5} [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

theorem WeightedNetKAT.rSafety.rSafety_iff_ErSafety {F : Type u_1} [Fintype F] [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {𝒮 : Type u_5} [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

@[implicit_reducible]

instance WeightedNetKAT.rSafety.instDecidableErSafetyOfDecidableRelLe {F : Type u_1} [Listed F] [DecidableEq F] {N : Type u_2} [Listed N] [DecidableEq N] {𝒮 : Type u_5} [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

def WeightedNetKAT.rSafety.extraction_len {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] [DecidableEq N] {Q : Type u_4} {𝒮 : Type u_5} [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.

def WeightedNetKAT.rSafety.extraction_len' {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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.

def WeightedNetKAT.rSafety.extraction_len'' {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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.

def WeightedNetKAT.rSafety.extraction_len₀ {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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]])

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

def WeightedNetKAT.rSafety.extraction {F : Type u_1} [Listed F] {N : Type u_2} [Listed N] {Q : Type u_4} {𝒮 : Type u_5} [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