theorem List.max?_getD_lt {α : Type} [LinearOrder α] [Inhabited α] {xs : List α} {f e : α} (hf : xs ≠ [] ∨ f < e) (h : ∀ x ∈ xs, x < e) : xs.max?.getD f < e

@[reducible, inline]

abbrev WeightedNetKAT.rReachability.Run {F : Type} [Listed F] {N Q : Type} : Type

Equations

• WeightedNetKAT.rReachability.Run = (List (Q × (Pk[F,N] × Pk[F,N]) × Q) × (Pk[F,N] × Pk[F,N]) × Q)

def WeightedNetKAT.rReachability.«termRun[_,_,_]» : Lean.ParserDescr

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.rReachability.instDecidableEqProdListPk {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] {Q : Type} [DecidableEq Q] : DecidableEq (List (Q × (Pk[F,N] × Pk[F,N]) × Q) × (Pk[F,N] × Pk[F,N]) × Q)

Equations

• WeightedNetKAT.rReachability.instDecidableEqProdListPk = inferInstance

@[implicit_reducible]

instance WeightedNetKAT.rReachability.instReprProdListPk {F : Type} [Listed F] {N Q : Type} [Repr F] [Repr N] [Repr Q] : Repr (List (Q × (Pk[F,N] × Pk[F,N]) × Q) × (Pk[F,N] × Pk[F,N]) × Q)

Equations

• WeightedNetKAT.rReachability.instReprProdListPk = inferInstance

@[irreducible]

def WeightedNetKAT.rReachability.runsOf {F : Type} [Listed F] {N Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [DecidableEq 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) (q q' : Q) (gs : GS F N) : Array Run

Equations

• One or more equations did not get rendered due to their size.
• WeightedNetKAT.rReachability.runsOf 𝒜 q q' (α, [], β) = if q = q' then #[([], (α, β), q)] else #[]

def WeightedNetKAT.rReachability.Run.isCycleFree {F : Type} [Listed F] {N Q : Type} [DecidableEq Q] (run : Run) : Bool

Equations

• run.isCycleFree = decide (run.2.2 :: List.map (fun (x : Q × (Pk[F,N] × Pk[F,N]) × Q) => match x with | (q, fst, snd) => q) run.1).Nodup

def WeightedNetKAT.rReachability.Run.length {F : Type} [Listed F] {N Q : Type} (run : Run) : ℕ

Equations

• run.length = ‖run.1‖

def WeightedNetKAT.rReachability.Run.countQ {F : Type} [Listed F] {N Q : Type} [DecidableEq Q] (run : Run) : ℕ

Equations

• run.countQ = ‖(run.2.2 :: List.map (fun (x : Q × (Pk[F,N] × Pk[F,N]) × Q) => match x with | (q, fst, snd) => q) run.1).dedup‖

def WeightedNetKAT.rReachability.extendCycleFree' {F : Type} [Listed F] {N : Type} [Listed N] {Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [DecidableEq 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) (cur : Run) (h : cur.isCycleFree = true) : Array Run

Equations

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

@[simp]

theorem WeightedNetKAT.rReachability.extendCycleFree'_isCycleFree {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [DecidableEq 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) {ρ : Run} {h : ρ.isCycleFree = true} (ρ' : Run) : ρ' ∈ extendCycleFree' 𝒜 ρ h → ρ'.isCycleFree = true

@[irreducible]

def WeightedNetKAT.rReachability.extendCycleFree {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [DecidableEq 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) (cur : Array Run) (h : ∀ ρ ∈ cur, ρ.isCycleFree = true) : Array Run

Equations

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

def WeightedNetKAT.rReachability.cycleFreeRunsOf {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [Fintype Q] [DecidableEq Q] [Semiring 𝒮] [DecidableEq 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) (q : Q) : Array Run

Equations

• WeightedNetKAT.rReachability.cycleFreeRunsOf 𝒜 q = WeightedNetKAT.rReachability.extendCycleFree 𝒜 (Array.map (fun (x : Pk[F,N] × Pk[F,N]) => ([], x, q)) Listed.array) ⋯

@[irreducible]

def WeightedNetKAT.rReachability.Run.weight {F : Type} [Listed F] {N Q 𝒮 : Type} [Semiring 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) : Run → 𝒮

Equations

• WeightedNetKAT.rReachability.Run.weight 𝒜 ([], (fst, snd), snd_1) = 1
• WeightedNetKAT.rReachability.Run.weight 𝒜 ((q, (α, β), q') :: ρ, ρ') = 𝒜.δ α β q q' * WeightedNetKAT.rReachability.Run.weight 𝒜 (ρ, ρ')

def WeightedNetKAT.rReachability.δ_star {F : Type} [Listed F] {N Q 𝒮 : Type} [Listed Q] [DecidableEq Q] [Semiring 𝒮] [DecidableEq 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) (q q' : Q) (gs : GS F N) : 𝒮

Equations

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

def WeightedNetKAT.rReachability.all {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {Q 𝒮 : Type} [Listed Q] [Fintype Q] [DecidableEq Q] [Semiring 𝒮] [DecidableEq 𝒮] (𝒜 : WNKA[F,N,𝒮,Q]) : Array (Run × 𝒮)

Equations

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

def WeightedNetKAT.rReachability.potential {F : Type} [Listed F] {N Q 𝒮 : Type} : Array (Q × Q × Run × 𝒮)

Equations

• WeightedNetKAT.rReachability.potential = sorry