def WeightedNetKAT.«term𝟙» : Lean.ParserDescr

Equations

• WeightedNetKAT.«term𝟙» = Lean.ParserDescr.node `WeightedNetKAT.«term𝟙» 1024 (Lean.ParserDescr.symbol "𝟙")

structure WeightedNetKAT.WNKA (F N 𝒮 Q : Type) [Semiring 𝒮] [Listed F] : Type

Weighted NetKAT Automaton.

• Q is a set of states.
• ι is the initial weightings.
• δ is a family of transition functions B[α,β] : Q → 𝒞 𝒮 Q indexed by packet pairs.
• 𝒪 is a family of output weightings R[α,β] : 𝒞 𝒮 Q indexed by packet pairs. Note that we use 𝒪 instead of λ, since λ is the function symbol in Lean.

• ι : Matrix Unit Q 𝒮

  ι is the initial weightings.

• δ (α β : Pk[F,N]) : Matrix Q Q 𝒮

  δ is a family of transition functions B[α,β] : Q → 𝒞 𝒮 Q indexed by packet pairs.

• 𝒪 (α β : Pk[F,N]) : Matrix Q Unit 𝒮

  𝒪 is a family of output weightings R[α,β] : 𝒞 𝒮 Q indexed by packet pairs. Note that we use 𝒪 instead of λ, since λ is the function symbol in Lean.

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

Equations

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

def WeightedNetKAT.WNKA.sem {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] {Q : Type} [Fintype Q] [DecidableEq N] [DecidableEq F] (𝒜 : WNKA[F,N,𝒮,Q]) : GS F N →c 𝒮

Equations

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

def WeightedNetKAT.WNKA.xδ {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] {Q : Type} [Fintype Q] [DecidableEq Q] (d : Pk[F,N] → Pk[F,N] → Matrix Q Q 𝒮) (xs : List Pk[F,N]) : Matrix Q Q 𝒮

Equations

• WeightedNetKAT.WNKA.xδ d [] = 1
• WeightedNetKAT.WNKA.xδ d [head] = 1
• WeightedNetKAT.WNKA.xδ d (α :: α' :: xs_2) = d α α' * WeightedNetKAT.WNKA.xδ d (α' :: xs_2)

theorem WeightedNetKAT.WNKA.xδ_right {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] {Q : Type} [Fintype Q] [DecidableEq Q] (f : Pk[F,N] → Pk[F,N] → Matrix Q Q 𝒮) (A : List Pk[F,N]) {α₁ α₀ : Pk[F,N]} : xδ f (A ++ [α₁, α₀]) = xδ f (A ++ [α₁]) * f α₁ α₀

theorem WeightedNetKAT.WNKA.xδ_δ'_as_sum_unfolded {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] {Q : Type} [Fintype Q] [DecidableEq Q] [Inhabited Pk[F,N]] {xₙ : List Pk[F,N]} {l r : Matrix Pk[F,N] Pk[F,N] (Matrix Q Q 𝒮)} : xδ (l + r) xₙ = xδ l xₙ + ∑ n ∈ Finset.range (‖xₙ‖ - 1), xδ l (xₙ[..n + 1]) * r xₙ[n]! xₙ[n + 1]! * xδ (l + r) (xₙ[n + 1..])

def WeightedNetKAT.«term♡» : Lean.ParserDescr

Equations

• WeightedNetKAT.«term♡» = Lean.ParserDescr.node `WeightedNetKAT.«term♡» 1024 (Lean.ParserDescr.symbol "♡")

def WeightedNetKAT.«term♣» : Lean.ParserDescr

Equations

• WeightedNetKAT.«term♣» = Lean.ParserDescr.node `WeightedNetKAT.«term♣» 1024 (Lean.ParserDescr.symbol "♣")

@[reducible, inline]

abbrev WeightedNetKAT.S {F : Type} [Listed F] {N 𝒮 : Type} : RPol 𝒮 → Type

Equations

• WeightedNetKAT.S WeightedNetKAT.RPol.Drop = Unit
• WeightedNetKAT.S wnk_rpol {skip} = Unit
• WeightedNetKAT.S wnk_rpol {@test ~pk} = Unit
• WeightedNetKAT.S wnk_rpol {@mod ~pk} = Unit
• WeightedNetKAT.S wnk_rpol {dup} = (Unit ⊕ Unit)
• WeightedNetKAT.S wnk_rpol {~w ⨀ ~p₁} = WeightedNetKAT.S p₁
• WeightedNetKAT.S wnk_rpol {~p₁ ⨁ ~p₂} = (WeightedNetKAT.S p₁ ⊕ WeightedNetKAT.S p₂)
• WeightedNetKAT.S wnk_rpol {~p₁; ~p₂} = (WeightedNetKAT.S p₁ ⊕ WeightedNetKAT.S p₂)
• WeightedNetKAT.S wnk_rpol {~p₁*} = (WeightedNetKAT.S p₁ ⊕ Unit)

@[reducible, inline]

abbrev WeightedNetKAT.S.decidableEq {F : Type} [Listed F] {N 𝒮 : Type} (p : RPol 𝒮) : DecidableEq (S p)

Equations

• WeightedNetKAT.S.decidableEq WeightedNetKAT.RPol.Drop = fun (a b : PUnit.{1}) => isTrue ⋯
• WeightedNetKAT.S.decidableEq wnk_rpol {skip} = fun (a b : PUnit.{1}) => isTrue ⋯
• WeightedNetKAT.S.decidableEq wnk_rpol {@test ~pk} = fun (a b : PUnit.{1}) => isTrue ⋯
• WeightedNetKAT.S.decidableEq wnk_rpol {@mod ~pk} = fun (a b : PUnit.{1}) => isTrue ⋯
• WeightedNetKAT.S.decidableEq wnk_rpol {dup} = fun (a b : Unit ⊕ Unit) => instDecidableEqSum a b
• WeightedNetKAT.S.decidableEq wnk_rpol {~w ⨀ ~p₁} = WeightedNetKAT.S.decidableEq p₁
• WeightedNetKAT.S.decidableEq wnk_rpol {~p₁ ⨁ ~p₂} = instDecidableEqSum
• WeightedNetKAT.S.decidableEq wnk_rpol {~p₁; ~p₂} = instDecidableEqSum
• WeightedNetKAT.S.decidableEq wnk_rpol {~p₁*} = instDecidableEqSum

@[implicit_reducible]

instance WeightedNetKAT.instUniqueFinSizeUnit : Unique (Fin (Listed.size Unit))

Equations

• WeightedNetKAT.instUniqueFinSizeUnit = { toInhabited := Fin.instInhabited, uniq := WeightedNetKAT.instUniqueFinSizeUnit._proof_5 }

@[implicit_reducible]

instance WeightedNetKAT.S.instDecidableEq {F : Type} [Listed F] {N 𝒮 : Type} (p : RPol 𝒮) : DecidableEq (S p)

Equations

• WeightedNetKAT.S.instDecidableEq p = WeightedNetKAT.S.decidableEq p

@[reducible]

instance WeightedNetKAT.S.fintype {F : Type} [Listed F] {N 𝒮 : Type} (p : RPol 𝒮) : Fintype (S p)

Equations

• WeightedNetKAT.S.fintype WeightedNetKAT.RPol.Drop = { elems := {PUnit.unit}, complete := ⋯ }
• WeightedNetKAT.S.fintype wnk_rpol {skip} = { elems := {PUnit.unit}, complete := ⋯ }
• WeightedNetKAT.S.fintype wnk_rpol {@test ~pk} = { elems := {PUnit.unit}, complete := ⋯ }
• WeightedNetKAT.S.fintype wnk_rpol {@mod ~pk} = { elems := {PUnit.unit}, complete := ⋯ }
• WeightedNetKAT.S.fintype wnk_rpol {dup} = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }
• WeightedNetKAT.S.fintype wnk_rpol {~w ⨀ ~p₁} = WeightedNetKAT.S.fintype p₁
• WeightedNetKAT.S.fintype wnk_rpol {~p₁ ⨁ ~p₂} = instFintypeSum (WeightedNetKAT.S p₁) (WeightedNetKAT.S p₂)
• WeightedNetKAT.S.fintype wnk_rpol {~p₁; ~p₂} = instFintypeSum (WeightedNetKAT.S p₁) (WeightedNetKAT.S p₂)
• WeightedNetKAT.S.fintype wnk_rpol {~p₁*} = instFintypeSum (WeightedNetKAT.S p₁) Unit

instance WeightedNetKAT.S.Finite {F : Type} [Listed F] {N 𝒮 : Type} {p : RPol 𝒮} : _root_.Finite (S p)

@[implicit_reducible]

instance WeightedNetKAT.S.listed {F : Type} [Listed F] {N 𝒮 : Type} (p : RPol 𝒮) : Listed (S p)

Equations

• One or more equations did not get rendered due to their size.
• WeightedNetKAT.S.listed wnk_rpol {~w ⨀ ~p₁} = WeightedNetKAT.S.listed p₁
• WeightedNetKAT.S.listed wnk_rpol {~p₁ ⨁ ~p₂} = Listed.instSum
• WeightedNetKAT.S.listed wnk_rpol {~p₁; ~p₂} = Listed.instSum
• WeightedNetKAT.S.listed wnk_rpol {~p₁*} = Listed.instSum

@[reducible, inline]

abbrev WeightedNetKAT.η₁ {𝒮 : Type} [Semiring 𝒮] {X : Type} [DecidableEq X] (i : X) : X → 𝒮

Equations

• WeightedNetKAT.η₁ i i' = if i = i' then 1 else 0

@[reducible, inline]

abbrev WeightedNetKAT.η₂ {𝒮 : Type} [Semiring 𝒮] {X Y : Type} [DecidableEq X] [DecidableEq Y] (i : X) (j : Y) : Matrix X Y 𝒮

Equations

• WeightedNetKAT.η₂ i j i' j' = if i = i' ∧ j = j' then 1 else 0

Homebrew matrix operators

For the automata construction we define some custom matrix operators that are variants of nested multiplication or nested scalar multiplication.

def WeightedNetKAT.box {N : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype B] {Q : Type u_5} [AddCommMonoid Q] [Mul Q] [Unique A] (l : Matrix A B Q) (r : Matrix N N (Matrix B A Q)) : Matrix N N Q

Equations

• (l ⊠ r) α β = (l * r α β).down

def WeightedNetKAT.«term_⊠_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊠_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊠_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊠ ") (Lean.ParserDescr.cat `term 71))

def WeightedNetKAT.fox {N : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Fintype B] {Q : Type u_5} [AddCommMonoid Q] [Mul Q] (l : Matrix A B Q) (r : Matrix N N (Matrix B C Q)) : Matrix N N (Matrix A C Q)

Equations

• (l ⊡ r) α β = l * r α β

def WeightedNetKAT.«term_⊡_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊡_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊡_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊡ ") (Lean.ParserDescr.cat `term 71))

def WeightedNetKAT.sox {N : Type u_1} [Fintype N] {A : Type u_2} {B : Type u_3} {Q : Type u_5} [AddCommMonoid Q] [Mul Q] (l : Matrix N N Q) (r : Matrix N N (Matrix A B Q)) : Matrix N N (Matrix A B Q)

Equations

• (l ⊟> r) α β = ∑ m : N, l α m • r m β

def WeightedNetKAT.«term_⊟>_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊟>_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊟>_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊟> ") (Lean.ParserDescr.cat `term 71))

def WeightedNetKAT.sox' {N : Type u_1} [Fintype N] {A : Type u_2} {B : Type u_3} {Q : Type u_5} [AddCommMonoid Q] [Mul Q] (l : Matrix N N (Matrix A B Q)) (r : Matrix N N Q) : Matrix N N (Matrix A B Q)

Equations

• (l <⊟ r) α β = ∑ m : N, MulOpposite.op (r m β) • l α m

def WeightedNetKAT.«term_<⊟_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_<⊟_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_<⊟_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <⊟ ") (Lean.ParserDescr.cat `term 71))

def WeightedNetKAT.crox {N : Type u_1} [Fintype N] {A : Type u_2} {B : Type u_3} {C : Type u_4} [Fintype B] {Q : Type u_5} [AddCommMonoid Q] [Mul Q] (l : Matrix N N (Matrix A B Q)) (r : Matrix N N (Matrix B C Q)) : Matrix N N (Matrix A C Q)

Equations

• (l ⊞ r) α β = ∑ m : N, l α m * r m β

def WeightedNetKAT.«term_⊞_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊞_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊞_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊞ ") (Lean.ParserDescr.cat `term 71))

theorem WeightedNetKAT.add_sox {N : Type u_1} [Fintype N] {A : Type u_2} {B : Type u_3} {Q : Type u_5} [AddCommMonoid Q] [Mul Q] [RightDistribClass Q] (l l' : Matrix N N Q) (r : Matrix N N (Matrix A B Q)) : (l + l') ⊟> r = l ⊟> r + l' ⊟> r

theorem WeightedNetKAT.mul_sox {N : Type u_1} [Fintype N] {A : Type u_2} {B : Type u_3} {Q : Type u_6} [NonUnitalSemiring Q] (l l' : Matrix N N Q) (r : Matrix N N (Matrix A B Q)) : l * l' ⊟> r = l ⊟> (l' ⊟> r)

@[simp]

theorem WeightedNetKAT.one_sox {N : Type u_1} [Fintype N] {A : Type u_2} {B : Type u_3} [DecidableEq N] {Q : Type u_6} [Semiring Q] (r : Matrix N N (Matrix A B Q)) : 1 ⊟> r = r

def WeightedNetKAT.RPol.ι {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] (p : RPol 𝒮) : Matrix Unit (S p) 𝒮

Equations

• WeightedNetKAT.RPol.Drop.ι = WeightedNetKAT.η₂ () ()
• wnk_rpol {skip}.ι = WeightedNetKAT.η₂ () ()
• wnk_rpol {@test ~pk}.ι = WeightedNetKAT.η₂ () ()
• wnk_rpol {@mod ~pk}.ι = WeightedNetKAT.η₂ () ()
• wnk_rpol {dup}.ι = WeightedNetKAT.η₂ () (Sum.inl ())
• wnk_rpol {~w ⨀ ~p₁}.ι = w • p₁.ι
• wnk_rpol {~p₁ ⨁ ~p₂}.ι = p₁.ι.fromCols p₂.ι
• wnk_rpol {~p₁; ~p₂}.ι = p₁.ι.fromCols 0
• wnk_rpol {~p₁*}.ι = Matrix.fromCols 0 1

@[irreducible]

def WeightedNetKAT.RPol.𝒪_heart {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p₁ : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] 𝒮

Equations

• p₁.𝒪_heart = KStar.kstar (p₁.ι ⊠ p₁.𝒪)

@[irreducible]

def WeightedNetKAT.RPol.𝒪 {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p) Unit 𝒮)

Equations

• WeightedNetKAT.RPol.Drop.𝒪 α β = 0
• wnk_rpol {skip}.𝒪 α β = if α = β then fun (x : WeightedNetKAT.S wnk_rpol {skip}) => 1 else 0
• wnk_rpol {@test ~pk}.𝒪 α β = if α = β ∧ β = pk then fun (x : WeightedNetKAT.S wnk_rpol {@test ~pk}) => 1 else 0
• wnk_rpol {@mod ~pk}.𝒪 α β = if β = pk then fun (x : WeightedNetKAT.S wnk_rpol {@mod ~pk}) => 1 else 0
• wnk_rpol {dup}.𝒪 α β = if α = β then WeightedNetKAT.η₂ (Sum.inr ()) () else 0
• wnk_rpol {~w ⨀ ~p₁}.𝒪 α β = p₁.𝒪 α β
• wnk_rpol {~p₁ ⨁ ~p₂}.𝒪 α β = (p₁.𝒪 α β).fromRows (p₂.𝒪 α β)
• wnk_rpol {~p₁; ~p₂}.𝒪 α β = (∑ γ : Pk[F,N], p₁.𝒪 α γ * p₂.ι * p₂.𝒪 γ β).fromRows (p₂.𝒪 α β)
• wnk_rpol {~p₁*}.𝒪 α β = ((p₁.𝒪 <⊟ p₁.𝒪_heart) α β).fromRows ↑(p₁.𝒪_heart α β)

@[irreducible]

def WeightedNetKAT.RPol.δ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p) (S p) 𝒮)

Equations

• WeightedNetKAT.RPol.Drop.δ α β = 0
• wnk_rpol {skip}.δ α β = 0
• wnk_rpol {@test ~pk}.δ α β = 0
• wnk_rpol {@mod ~pk}.δ α β = 0
• wnk_rpol {dup}.δ α β = fun (s : WeightedNetKAT.S wnk_rpol {dup}) => if s = Sum.inl () ∧ α = β then WeightedNetKAT.η₁ (Sum.inr ()) else 0
• wnk_rpol {~w ⨀ ~p₁}.δ α β = p₁.δ α β
• wnk_rpol {~p₁ ⨁ ~p₂}.δ α β = Matrix.fromBlocks (p₁.δ α β) 0 0 (p₂.δ α β)
• wnk_rpol {~p₁; ~p₂}.δ α β = Matrix.fromBlocks (p₁.δ α β) (∑ γ : Pk[F,N], p₁.𝒪 α γ * p₂.ι * p₂.δ γ β) 0 (p₂.δ α β)
• wnk_rpol {~p₁*}.δ α β = Matrix.fromBlocks (WeightedNetKAT.RPol.δ.δ' p₁ α β) 0 ((p₁.𝒪_heart ⊟> (p₁.ι ⊡ p₁.δ)) α β) 0

@[irreducible]

def WeightedNetKAT.RPol.δ.δ' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p₁ : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p₁) (S p₁) 𝒮)

Equations

• WeightedNetKAT.RPol.δ.δ' p₁ = p₁.δ + p₁.𝒪 ⊞ (p₁.𝒪_heart ⊟> (p₁.ι ⊡ p₁.δ))

noncomputable def WeightedNetKAT.RPol.𝒪ₐ_heart {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p₁ : RPol 𝒮) (n : ℕ) : Matrix Pk[F,N] Pk[F,N] 𝒮

Equations

• p₁.𝒪ₐ_heart n = ∑ i ∈ Finset.range n, (p₁.ι ⊠ p₁.𝒪) ^ i

def WeightedNetKAT.RPol.ιₐ {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] (p : RPol 𝒮) : Matrix Unit (S p ⊕ Unit) 𝒮

Equations

• p.ιₐ = Matrix.fromCols 0 fun (x : Unit) => 1

noncomputable def WeightedNetKAT.RPol.𝒪ₐ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) (n : ℕ) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p ⊕ Unit) Unit 𝒮)

Equations

• p.𝒪ₐ n α β = ((p.𝒪 <⊟ p.𝒪ₐ_heart n) α β).fromRows ↑(p.𝒪ₐ_heart n α β)

noncomputable def WeightedNetKAT.RPol.δₐ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) (n : ℕ) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p ⊕ Unit) (S p ⊕ Unit) 𝒮)

Equations

• p.δₐ n α β = Matrix.fromBlocks (WeightedNetKAT.RPol.δₐ.δ' p n α β) 0 ((p.𝒪ₐ_heart n ⊟> (p.ι ⊡ p.δ)) α β) 0

noncomputable def WeightedNetKAT.RPol.δₐ.δ' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) (n : ℕ) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p) (S p) 𝒮)

Equations

• WeightedNetKAT.RPol.δₐ.δ' p n = p.δ + p.𝒪 ⊞ (p.𝒪ₐ_heart n ⊟> (p.ι ⊡ p.δ))

theorem WeightedNetKAT.RPol.xδ_δ_iter {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] {p₁ : RPol 𝒮} {α : Pk[F,N]} {xₙ : List Pk[F,N]} : WNKA.xδ wnk_rpol {~p₁*}.δ (α :: xₙ) = Matrix.fromBlocks (WNKA.xδ (δ.δ' p₁) (α :: xₙ)) 0 (if xₙ = [] then 0 else (p₁.𝒪_heart ⊟> (p₁.ι ⊡ p₁.δ)) α (xₙ.head?.getD α) * WNKA.xδ (δ.δ' p₁) xₙ) (if xₙ = [] then 1 else 0)

theorem WeightedNetKAT.RPol.xδ_δₐ_iter {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] {p₁ : RPol 𝒮} {α : Pk[F,N]} {xₙ : List Pk[F,N]} {n : ℕ} : WNKA.xδ (p₁.δₐ n) (α :: xₙ) = Matrix.fromBlocks (WNKA.xδ (δₐ.δ' p₁ n) (α :: xₙ)) 0 (if xₙ = [] then 0 else (p₁.𝒪ₐ_heart n ⊟> (p₁.ι ⊡ p₁.δ)) α (xₙ.head?.getD α) * WNKA.xδ (δₐ.δ' p₁ n) xₙ) (if xₙ = [] then 1 else 0)

theorem WeightedNetKAT.RPol.xδ_seq_eq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] {p₁ p₂ : RPol 𝒮} [Inhabited Pk[F,N]] {A : List Pk[F,N]} : WNKA.xδ wnk_rpol {~p₁; ~p₂}.δ A = Matrix.fromBlocks (WNKA.xδ p₁.δ A) (∑ γ : Pk[F,N], ∑ i ∈ Finset.range (‖A‖ - 1), WNKA.xδ p₁.δ (A[..i + 1]) * p₁.𝒪 A[i]! γ * p₂.ι * WNKA.xδ p₂.δ (γ :: A[i + 1..])) 0 (WNKA.xδ p₂.δ A)

def WeightedNetKAT.RPol.unexpand : Lean.TSyntax `term → Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `cwnk_rpol)

Equations

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

class WeightedNetKAT.RPol.Semantics (F N : Type) [Listed F] (𝒮 : Type) {α : Type u_1} (sem : RPol 𝒮 → α) : Type

Notation class for X⟦~p⟧

@[reducible, inline]

abbrev WeightedNetKAT.RPol.Semantics.sem {F N : Type} [Listed F] {𝒮 : Type} {α : Type u_1} (sem : RPol 𝒮 → α) : RPol 𝒮 → α

Equations

• WeightedNetKAT.RPol.Semantics.sem sem = sem

def WeightedNetKAT.RPol.«term_⟦_⟧» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.RPol.Semantics.sem.unexpander : Lean.PrettyPrinter.Unexpander

Equations

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

noncomputable def WeightedNetKAT.RPol.wnka {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]

The WNKA of policy p

Equations

• p.wnka = { ι := p.ι, δ := p.δ, 𝒪 := p.𝒪 }

@[simp]

theorem WeightedNetKAT.RPol.wnka_ι {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] : p.wnka.ι = p.ι

@[simp]

theorem WeightedNetKAT.RPol.wnka_δ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] : p.wnka.δ = p.δ

@[simp]

theorem WeightedNetKAT.RPol.wnka_𝒪 {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] : p.wnka.𝒪 = p.𝒪

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

𝒜⟦·⟧ is the automata semantics of p

Equations

• p.𝒜 = p.wnka.sem

@[implicit_reducible]

instance WeightedNetKAT.RPol.instSemanticsCountsuppGS𝒜 {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] : Semantics F N 𝒮 𝒜

Equations

• WeightedNetKAT.RPol.instSemanticsCountsuppGS𝒜 = { }

noncomputable def WeightedNetKAT.RPol.Q {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] (p : RPol 𝒮) (xᵢ : List Pk[F,N]) : Matrix Pk[F,N] Pk[F,N] 𝒮

Q⟦·⟧ is the automata semantics of p expressed as a matrix

Equations

• p.Q xᵢ α β = WeightedNetKAT.RPol.𝒜⟦~p⟧ (α, xᵢ, β)

@[implicit_reducible]

instance WeightedNetKAT.RPol.instSemanticsForallListPkMatrixQ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] : Semantics F N 𝒮 Q

Equations

• WeightedNetKAT.RPol.instSemanticsForallListPkMatrixQ = { }

noncomputable def WeightedNetKAT.RPol.𝒜ₐ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) (n : ℕ) : GS F N → 𝒮

𝒜ₐ⟦·⟧ is the approximate automata semantics of p

Equations

• p.𝒜ₐ n (α, xs, β) = (p.ιₐ * WeightedNetKAT.WNKA.xδ (p.δₐ n) (α :: xs) * p.𝒪ₐ n (xs.getLast?.getD α) β).down

@[implicit_reducible]

instance WeightedNetKAT.RPol.instSemanticsForallNatForallGS𝒜ₐ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] : Semantics F N 𝒮 𝒜ₐ

Equations

• WeightedNetKAT.RPol.instSemanticsForallNatForallGS𝒜ₐ = { }

noncomputable def WeightedNetKAT.RPol.M {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) (xᵢ : List Pk[F,N]) : Matrix Pk[F,N] Pk[F,N] 𝒮

M⟦·⟧ is the language semantics of p expressed as a matrix

Equations

• p.M xᵢ α β = G⟦~p⟧ (α, xᵢ, β)

@[implicit_reducible]

instance WeightedNetKAT.RPol.instSemanticsForallListPkMatrixM {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] : Semantics F N 𝒮 M

Equations

• WeightedNetKAT.RPol.instSemanticsForallListPkMatrixM = { }

noncomputable def WeightedNetKAT.RPol.Qₐ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) (n : ℕ) (xs : List Pk[F,N]) : Matrix Pk[F,N] Pk[F,N] 𝒮

Qₐ⟦·⟧ is the n-bounded automata semantics of p expressed as a matrix

Equations

• p.Qₐ n xs a b = WeightedNetKAT.RPol.𝒜ₐ⟦~p⟧ n (a, xs, b)

@[implicit_reducible]

instance WeightedNetKAT.RPol.instSemanticsForallNatForallListPkMatrixQₐ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] : Semantics F N 𝒮 Qₐ

Equations

• WeightedNetKAT.RPol.instSemanticsForallNatForallListPkMatrixQₐ = { }

noncomputable def WeightedNetKAT.RPol.M' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) (n : ℕ) : Matrix Pk[F,N] Pk[F,N] 𝒮

M'⟦·⟧ is the n-repeated language semantics of p expressed as a matrix

Equations

• p.M' n = ∑ i ∈ Finset.range n, WeightedNetKAT.RPol.M⟦~p⟧ [] ^ i

@[implicit_reducible]

instance WeightedNetKAT.RPol.instSemanticsForallNatMatrixPkM' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] : Semantics F N 𝒮 M'

Equations

• WeightedNetKAT.RPol.instSemanticsForallNatMatrixPkM' = { }

@[simp]

theorem WeightedNetKAT.RPol.𝒜ₐ_iter_empty {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {α β : Pk[F,N]} {n : ℕ} : 𝒜ₐ⟦~p⟧ n (α, [], β) = p.𝒪ₐ_heart n α β

theorem WeightedNetKAT.RPol.𝒜_def {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {p : RPol 𝒮} {gs : GS F N} : 𝒜⟦~p⟧ gs = (List.foldl (fun (acc : Matrix Unit (S p) 𝒮) (x : Pk[F,N] × Pk[F,N]) => match x with | (γ, κ) => acc * p.δ γ κ) p.ι ((gs.1 :: gs.2.1).zip gs.2.1) * p.𝒪 (gs.2.1.getLast?.getD gs.1) gs.2.2) () ()

theorem WeightedNetKAT.RPol.𝒜_def' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {p : RPol 𝒮} {gs : GS F N} : 𝒜⟦~p⟧ gs = if gs.2.1 = [] then (p.ι * p.𝒪 gs.1 gs.2.2) () () else (p.ι * (List.map (fun (x : Pk[F,N] × Pk[F,N]) => match x with | (γ, κ) => p.δ γ κ) ((gs.1 :: gs.2.1).zip gs.2.1)).prod * p.𝒪 (gs.2.1.getLast?.getD gs.1) gs.2.2) () ()

theorem WeightedNetKAT.RPol.𝒜_def'' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {p : RPol 𝒮} {gs : GS F N} : 𝒜⟦~p⟧ gs = if gs.2.1 = [] then (p.ι * p.𝒪 gs.1 gs.2.2) () () else (p.ι * WNKA.xδ p.δ (gs.1 :: gs.2.1) * p.𝒪 (gs.2.1.getLast?.getD gs.1) gs.2.2) () ()

def WeightedNetKAT.RPol.term𝒜_proof_ : Lean.ParserDescr

A proof that 𝒜⟦p⟧ = G⟦p⟧

Equations

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

theorem WeightedNetKAT.RPol.𝒜_drop {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] : 𝒜⟦~Drop⟧ = G⟦~Drop⟧

theorem WeightedNetKAT.RPol.𝒜_single {α : Type u_1} {motive : α → List α → α → Prop} (nil : ∀ (a b : α), motive a [] b) (single : ∀ (a x b : α), motive a [x] b) (ind : ∀ (a b c d : α) (xs : List α), motive c xs d → motive b (c :: xs) d → motive a (b :: c :: xs) d) (a : α) (xs : List α) (b : α) : motive a xs b

@[simp]

theorem WeightedNetKAT.RPol.𝒜_skip {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] : 𝒜⟦skip⟧ = G⟦skip⟧

theorem WeightedNetKAT.RPol.𝒜_test {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {t : Pk[F,N]} : 𝒜⟦@test ~t⟧ = G⟦@test ~t⟧

theorem WeightedNetKAT.RPol.𝒜_mod {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {π : Pk[F,N]} : 𝒜⟦@mod ~π⟧ = G⟦@mod ~π⟧

theorem WeightedNetKAT.RPol.𝒜_dup {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] : 𝒜⟦dup⟧ = G⟦dup⟧

@[simp]

theorem WeightedNetKAT.RPol.𝒜_add_eq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {p₁ p₂ : RPol 𝒮} : 𝒜⟦~p₁ ⨁ ~p₂⟧ = 𝒜⟦~p₁⟧ + 𝒜⟦~p₂⟧

theorem WeightedNetKAT.RPol.𝒜_add {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {p₁ p₂ : RPol 𝒮} (ih₁ : 𝒜⟦~p₁⟧ = G⟦~p₁⟧) (ih₂ : 𝒜⟦~p₂⟧ = G⟦~p₂⟧) : 𝒜⟦~p₁ ⨁ ~p₂⟧ = G⟦~p₁ ⨁ ~p₂⟧

@[simp]

theorem WeightedNetKAT.RPol.𝒜_weight_eq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {w : 𝒮} {p : RPol 𝒮} : 𝒜⟦~w ⨀ ~p⟧ = w * 𝒜⟦~p⟧

theorem WeightedNetKAT.RPol.𝒜_weight {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {w : 𝒮} {p : RPol 𝒮} (ih : 𝒜⟦~p⟧ = G⟦~p⟧) : 𝒜⟦~w ⨀ ~p⟧ = G⟦~w ⨀ ~p⟧

@[simp]

theorem WeightedNetKAT.RPol.𝒜_seq_eq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {p₁ p₂ : RPol 𝒮} : 𝒜⟦~p₁; ~p₂⟧ = 𝒜⟦~p₁⟧ ♢ 𝒜⟦~p₂⟧

theorem WeightedNetKAT.RPol.𝒜_seq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] {p₁ p₂ : RPol 𝒮} (ih₁ : 𝒜⟦~p₁⟧ = G⟦~p₁⟧) (ih₂ : 𝒜⟦~p₂⟧ = G⟦~p₂⟧) : 𝒜⟦~p₁; ~p₂⟧ = G⟦~p₁; ~p₂⟧

theorem WeightedNetKAT.RPol.Q_eq_𝒜 {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] (p : RPol 𝒮) {xs : List Pk[F,N]} : Q⟦~p⟧ xs = fun (x z : Pk[F,N]) => 𝒜⟦~p⟧ (x, xs, z)

theorem WeightedNetKAT.RPol.𝒜_eq_M {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] {a : Pk[F,N]} {xs : List Pk[F,N]} {b : Pk[F,N]} (ihp : G⟦~p⟧ = 𝒜⟦~p⟧) : 𝒜⟦~p⟧ (a, xs, b) = M⟦~p⟧ xs a b

theorem WeightedNetKAT.RPol.𝒪ₐ_heart_eq_M {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] {n : ℕ} (ihp : G⟦~p⟧ = 𝒜⟦~p⟧) : p.𝒪ₐ_heart n = ∑ x ∈ Finset.range n, M⟦~p⟧ [] ^ x

@[simp]

theorem WeightedNetKAT.RPol.Q_nil_iter_eq_𝒜 {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] {i : ℕ} {α γ : Pk[F,N]} : (Q⟦~p⟧ [] ^ i) α γ = (𝒜⟦~p⟧ ^ i) (α, [], γ)

@[simp]

theorem WeightedNetKAT.RPol.𝒜_iter_nil {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] {α β : Pk[F,N]} : 𝒜⟦~p*⟧ (α, [], β) = p.𝒪_heart α β

theorem WeightedNetKAT.RPol.𝒜_pow_empty {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] {i : ℕ} {α β : Pk[F,N]} : (𝒜⟦~p⟧ ^ i) (α, [], β) = ((p.ι ⊠ p.𝒪) ^ i) α β

@[simp]

theorem WeightedNetKAT.RPol.Qₐ_iter_nil {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] {n : ℕ} (ihp : G⟦~p⟧ = 𝒜⟦~p⟧) : Qₐ⟦~p⟧ n [] = M'⟦~p⟧ n

theorem WeightedNetKAT.RPol.𝒜ₐ_iter_nonempty {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] {α α₀ β : Pk[F,N]} {xₙ : List Pk[F,N]} {n : ℕ} : 𝒜ₐ⟦~p⟧ n (α, α₀ :: xₙ, β) = ∑ i ∈ ..=‖xₙ‖, ∑ ξ : Pk[F,N], ∑ γ : Pk[F,N], p.𝒪ₐ_heart n α γ * 𝒜⟦~p⟧ (γ, α₀ :: xₙ[..i], ξ) * 𝒜ₐ⟦~p⟧ n (ξ, xₙ[i..], β)

theorem WeightedNetKAT.RPol.𝒜ₐ_iter_eq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] {α β : Pk[F,N]} {xₙ : List Pk[F,N]} {n : ℕ} : 𝒜ₐ⟦~p⟧ n (α, xₙ, β) = if xₙ = [] then p.𝒪ₐ_heart n α β else ∑ i ∈ Finset.range ‖xₙ‖, ∑ ξ : Pk[F,N], ∑ γ : Pk[F,N], p.𝒪ₐ_heart n α γ * 𝒜⟦~p⟧ (γ, xₙ[..i + 1], ξ) * 𝒜ₐ⟦~p⟧ n (ξ, xₙ[i + 1..], β)

@[simp]

theorem WeightedNetKAT.RPol.M'_zero {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) : M'⟦~p⟧ 0 = 0

theorem WeightedNetKAT.RPol.M'_succ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n : ℕ} : M'⟦~p⟧ (n + 1) = M'⟦~p⟧ n + M⟦~p⟧ [] ^ n

theorem WeightedNetKAT.RPol.M'_succ' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n : ℕ} : M'⟦~p⟧ (n + 1) = M⟦~p⟧ [] ^ n + M'⟦~p⟧ n

theorem WeightedNetKAT.RPol.G_eq_M {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {a : Pk[F,N]} {xs : List Pk[F,N]} {b : Pk[F,N]} : G⟦~p⟧ (a, xs, b) = M⟦~p⟧ xs a b

theorem WeightedNetKAT.RPol.M_seq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p p' : RPol 𝒮) (xs : List Pk[F,N]) : M⟦~p; ~p'⟧ xs = ∑ c ∈ ..=‖xs‖, M⟦~p⟧ (xs[..c]) * M⟦~p'⟧ (xs[c..])

theorem WeightedNetKAT.RPol.M_skip {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] {xs : List Pk[F,N]} : M⟦skip⟧ xs = if xs = [] then 1 else 0

@[simp]

theorem WeightedNetKAT.RPol.M_iter_nil {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n : ℕ} : M⟦~(p.iter n)⟧ [] = M⟦~p⟧ [] ^ n

theorem WeightedNetKAT.RPol.M_iter_eq_buckets {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {xs : List Pk[F,N]} {n : ℕ} : ∑ i ∈ Finset.range n, M⟦~p; ~(p.iter i)⟧ xs = ∑ ys ∈ (Finset.range n).biUnion fun (x : ℕ) => xs.buckets x.succ, (List.map M⟦~p⟧ ys).prod

theorem WeightedNetKAT.RPol.𝒪ₐ_heart_apply {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n : ℕ} {α β : Pk[F,N]} : p.𝒪ₐ_heart n α β = ∑ i ∈ Finset.range n, ((p.ι ⊠ p.𝒪) ^ i) α β

@[simp]

theorem WeightedNetKAT.RPol.𝒪ₐ_heart_le_succ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n : ℕ} {α β : Pk[F,N]} : p.𝒪ₐ_heart n α β ≤ p.𝒪ₐ_heart (n + 1) α β

theorem WeightedNetKAT.RPol.𝒪ₐ_heart_le_apply_of_le {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n m : ℕ} {α β : Pk[F,N]} (h : n ≤ m) : p.𝒪ₐ_heart n α β ≤ p.𝒪ₐ_heart m α β

theorem WeightedNetKAT.RPol.𝒪ₐ_heart_le_of_le {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n m : ℕ} (h : n ≤ m) : p.𝒪ₐ_heart n ≤ p.𝒪ₐ_heart m

theorem WeightedNetKAT.RPol.𝒜ₐ_eq_Qₐ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) {n : ℕ} {g : GS F N} : 𝒜ₐ⟦~p⟧ n g = Qₐ⟦~p⟧ n g.2.1 g.1 g.2.2

theorem WeightedNetKAT.RPol.Qₐ_iter_eq' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] {xs : List Pk[F,N]} {n : ℕ} (ihp : G⟦~p⟧ = 𝒜⟦~p⟧) : Qₐ⟦~p⟧ n xs = if xs = [] then M'⟦~p⟧ n else M'⟦~p⟧ n * ∑ i ∈ Finset.range ‖xs‖, M⟦~p⟧ (xs[..i + 1]) * Qₐ⟦~p⟧ n (xs[i + 1..])

theorem WeightedNetKAT.RPol.Qₐ_iter_eq {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] {xs : List Pk[F,N]} {n : ℕ} (ihp : G⟦~p⟧ = 𝒜⟦~p⟧) : Qₐ⟦~p⟧ n xs = M'⟦~p⟧ n * ∑ ys ∈ xs.partitions, (List.map (fun (y : List Pk[F,N]) => M⟦~p⟧ y * M'⟦~p⟧ n) ys).prod

theorem WeightedNetKAT.RPol.Qₐ_iter_eq_partitionsFill' {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] {xs : List Pk[F,N]} {n : ℕ} (ihp : G⟦~p⟧ = 𝒜⟦~p⟧) : Qₐ⟦~p⟧ (n + 1) xs = ∑ ys ∈ xs.partitionsFill' n, (List.map M⟦~p⟧ ys).prod

@[simp]

theorem WeightedNetKAT.RPol.𝒜ₐ_le_succ {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] {n : ℕ} : 𝒜ₐ⟦~p⟧ n ≤ 𝒜ₐ⟦~p⟧ (n + 1)

theorem WeightedNetKAT.RPol.𝒜ₐ_monotone {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] : Monotone 𝒜ₐ⟦~p⟧

theorem WeightedNetKAT.RPol.𝒜ₐ_apply_monotone {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] {x : GS F N} : Monotone fun (x_1 : ℕ) => 𝒜ₐ⟦~p⟧ x_1 x

theorem WeightedNetKAT.RPol.𝒜_iter_nonempty {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {α α₀ β : Pk[F,N]} {xₙ : List Pk[F,N]} : 𝒜⟦~p*⟧ (α, α₀ :: xₙ, β) = ∑ x ∈ ..=‖xₙ‖, ∑ x_1 : Pk[F,N], ∑ x_2 : Pk[F,N], (ω∑ (x : ℕ), (𝒜⟦~p⟧ ^ x) (α, [], x_2)) * 𝒜⟦~p⟧ (x_2, α₀ :: xₙ[..x], x_1) * 𝒜⟦~p*⟧ (x_1, xₙ[x..], β)

theorem WeightedNetKAT.RPol.𝒜_iter_eq_ωSup_approx {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {α β : Pk[F,N]} {xₙ : List Pk[F,N]} : 𝒜⟦~p*⟧ (α, xₙ, β) = OmegaCompletePartialOrder.ωSup { toFun := fun (n : ℕ) => 𝒜ₐ⟦~p⟧ n (α, xₙ, β), monotone' := ⋯ }

In the limit the automata semantics are equal to the approximate.

theorem ωSup_nat_eq_succ {α : Type u_1} [OmegaCompletePartialOrder α] (f : OmegaCompletePartialOrder.Chain α) : OmegaCompletePartialOrder.ωSup f = OmegaCompletePartialOrder.ωSup { toFun := fun (x : ℕ) => f (x + 1), monotone' := ⋯ }

theorem WeightedNetKAT.RPol.𝒜_iter {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] (p : RPol 𝒮) [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (ihp : 𝒜⟦~p⟧ = G⟦~p⟧) : 𝒜⟦~p*⟧ = G⟦~p*⟧

theorem WeightedNetKAT.RPol.𝒜_eq_G {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : 𝒜⟦~p⟧ = G⟦~p⟧

theorem WeightedNetKAT.Pol.sem_eq_toRPol_𝒜 {F : Type} [Listed F] {N : Type} [Listed N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq N] [DecidableEq F] [KStar 𝒮] [LawfulKStar 𝒮] [Inhabited Pk[F,N]] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : Pol[F,N,𝒮]) (π : Pk[F,N]) (h : Pk[F,N] × List Pk[F,N]) : (p.sem (π, [])) h = RPol.𝒜⟦~p.toRPol⟧ (π, h.2.reverse, h.1)