inductive WeightedNetKAT.RPol {F : Type} [Listed F] {N : Type} (W : Type) : Type

• Drop {F : Type} [Listed F] {N W : Type} : RPol W
• Skip {F : Type} [Listed F] {N W : Type} : RPol W
• Test {F : Type} [Listed F] {N W : Type} (pk : Pk[F,N]) : RPol W
• Mod {F : Type} [Listed F] {N W : Type} (pk : Pk[F,N]) : RPol W
• Dup {F : Type} [Listed F] {N W : Type} : RPol W
• Seq {F : Type} [Listed F] {N W : Type} (p q : RPol W) : RPol W
• Weight {F : Type} [Listed F] {N W : Type} (w : W) (p : RPol W) : RPol W
• Add {F : Type} [Listed F] {N W : Type} (p q : RPol W) : RPol W
• Iter {F : Type} [Listed F] {N W : Type} (p : RPol W) : RPol W

def WeightedNetKAT.instDecidableEqRPol.decEq {F✝ : Type} {inst✝ : Listed F✝} {N✝ W✝ : Type} [DecidableEq F✝] [DecidableEq N✝] [DecidableEq W✝] (x✝ x✝¹ : RPol W✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop WeightedNetKAT.RPol.Drop = isTrue ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {@test ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {@mod ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {~p; ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {~w ⨀ ~p} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {~p ⨁ ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq WeightedNetKAT.RPol.Drop wnk_rpol {~p*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {skip} = isTrue ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {@test ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {@mod ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {~p; ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {~w ⨀ ~p} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {~p ⨁ ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {skip} wnk_rpol {~p*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~a} wnk_rpol {@test ~b} = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} wnk_rpol {@mod ~pk_1} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} wnk_rpol {~p; ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} wnk_rpol {~w ⨀ ~p} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} wnk_rpol {~p ⨁ ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@test ~pk} wnk_rpol {~p*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} wnk_rpol {@test ~pk_1} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~a} wnk_rpol {@mod ~b} = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} wnk_rpol {~p; ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} wnk_rpol {~w ⨀ ~p} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} wnk_rpol {~p ⨁ ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {@mod ~pk} wnk_rpol {~p*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {@test ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {@mod ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {dup} = isTrue ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {~p; ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {~w ⨀ ~p} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {~p ⨁ ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {dup} wnk_rpol {~p*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} wnk_rpol {@test ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} wnk_rpol {@mod ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} wnk_rpol {~w ⨀ ~p_1} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} wnk_rpol {~p_1 ⨁ ~q_1} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p; ~q} wnk_rpol {~p_1*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} wnk_rpol {@test ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} wnk_rpol {@mod ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} wnk_rpol {~p_1; ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} wnk_rpol {~p_1 ⨁ ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~w ⨀ ~p} wnk_rpol {~p_1*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} wnk_rpol {@test ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} wnk_rpol {@mod ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} wnk_rpol {~p_1; ~q_1} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} wnk_rpol {~w ⨀ ~p_1} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p ⨁ ~q} wnk_rpol {~p_1*} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} WeightedNetKAT.RPol.Drop = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} wnk_rpol {skip} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} wnk_rpol {@test ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} wnk_rpol {@mod ~pk} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} wnk_rpol {dup} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} wnk_rpol {~p_1; ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} wnk_rpol {~w ⨀ ~p_1} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~p*} wnk_rpol {~p_1 ⨁ ~q} = isFalse ⋯
• WeightedNetKAT.instDecidableEqRPol.decEq wnk_rpol {~a*} wnk_rpol {~b*} = if h : a = b then h ▸ have inst := WeightedNetKAT.instDecidableEqRPol.decEq a a; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WeightedNetKAT.instDecidableEqRPol {F✝ : Type} {inst✝ : Listed F✝} {N✝ W✝ : Type} [DecidableEq F✝] [DecidableEq N✝] [DecidableEq W✝] : DecidableEq (RPol W✝)

Equations

• WeightedNetKAT.instDecidableEqRPol = WeightedNetKAT.instDecidableEqRPol.decEq

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

Equations

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

def Lean.Parser.Category.cwnk_rpol : Category

Equations

• Lean.Parser.Category.cwnk_rpol = { }

def WeightedNetKAT.cwnk_rpol : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_rpol~_» : Lean.ParserDescr

Equations

• WeightedNetKAT.«cwnk_rpol~_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_rpol~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

def WeightedNetKAT.cwnk_rpol.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwnk_pk : Category

Equations

• Lean.Parser.Category.cwnk_pk = { }

def WeightedNetKAT.«cwnk_pk~_» : Lean.ParserDescr

Equations

• WeightedNetKAT.«cwnk_pk~_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_pk~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

def WeightedNetKAT.cwnk_pk.quot : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_pk : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_rpol_ : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_rpol_ = Lean.ParserDescr.node `WeightedNetKAT.cwnk_rpol_ 1022 (Lean.ParserDescr.cat `cwnk_pk 10)

def WeightedNetKAT.«cwnk_rpol_←_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_rpolDup : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_rpolDup = Lean.ParserDescr.node `WeightedNetKAT.cwnk_rpolDup 1024 (Lean.ParserDescr.symbol "dup")

def WeightedNetKAT.«cwnk_rpol_;_» : Lean.TrailingParserDescr

Equations

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

def WeightedNetKAT.«cwnk_rpol_⨀_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_rpol_⨁_» : Lean.TrailingParserDescr

Equations

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

def WeightedNetKAT.«cwnk_rpol_*» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«cwnk_rpol_*» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«cwnk_rpol_*» 1022 0 (Lean.ParserDescr.symbol "*")

def WeightedNetKAT.«cwnk_rpol(_)» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_rpol@test__» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_rpol@mod__» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_rpolSkip : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_rpolSkip = Lean.ParserDescr.node `WeightedNetKAT.cwnk_rpolSkip 1024 (Lean.ParserDescr.symbol "skip")

def WeightedNetKAT.cwnk_rpolDrop : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_rpolDrop = Lean.ParserDescr.node `WeightedNetKAT.cwnk_rpolDrop 1024 (Lean.ParserDescr.symbol "drop")

def WeightedNetKAT.cwnk_rpolIf___Then___Else__ : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_rpolWhile___Do__ : Lean.ParserDescr

Equations

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

def WeightedNetKAT.RPol.unexpandTest : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.RPol.unexpandSkip : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.RPol.unexpandDup : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.RPol.unexpandSeq : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.RPol.unexpandMod : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.RPol.unexpandAdd : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.RPol.unexpandWeight : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.RPol.unexpandIter : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.cwnk_pk.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer

Equations

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

def WeightedNetKAT.cwnk_rpol.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer

Equations

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

def WeightedNetKAT.RPol.iter {𝒮 F : Type} [Listed F] {N : Type} (p : RPol 𝒮) : ℕ → RPol 𝒮

Equations

• p.iter 0 = wnk_rpol {skip}
• p.iter n.succ = wnk_rpol {~p; ~(p.iter n)}

@[reducible]

instance WeightedNetKAT.RPol.instHPow {𝒮 F : Type} [Listed F] {N : Type} : HPow (RPol 𝒮) ℕ (RPol 𝒮)

Equations

• WeightedNetKAT.RPol.instHPow = { hPow := fun (p : WeightedNetKAT.RPol 𝒮) (n : ℕ) => p.iter n }

@[simp]

theorem WeightedNetKAT.RPol.pow_eq_iter {𝒮 F : Type} [Listed F] {N : Type} (p : RPol 𝒮) (n : ℕ) : p ^ n = p.iter n

def WeightedNetKAT.RPol.iterDepth {𝒮 F : Type} [Listed F] {N : Type} : RPol 𝒮 → ℕ

Equations

• wnk_rpol {skip}.iterDepth = 0
• WeightedNetKAT.RPol.Drop.iterDepth = 0
• wnk_rpol {@test ~pk}.iterDepth = 0
• wnk_rpol {@mod ~pk}.iterDepth = 0
• wnk_rpol {dup}.iterDepth = 0
• wnk_rpol {~p ⨁ ~q}.iterDepth = max p.iterDepth q.iterDepth
• wnk_rpol {~p; ~q}.iterDepth = max p.iterDepth q.iterDepth
• wnk_rpol {~w ⨀ ~q}.iterDepth = q.iterDepth
• wnk_rpol {~p*}.iterDepth = p.iterDepth + 1

@[simp]

theorem WeightedNetKAT.RPol.iterDepth_iter {𝒮 F : Type} [Listed F] {N : Type} {p : RPol 𝒮} {n : ℕ} : (p.iter n).iterDepth = if n = 0 then 0 else p.iterDepth

def WeightedNetKAT.RPol.repr {𝒮 N F : Type} [i : Fintype F] [e : Encodable F] [Repr F] [Repr N] [Repr 𝒮] [Listed F] : RPol 𝒮 → String

Equations

• wnk_rpol {@test ~t}.repr = toString "@test " ++ toString (reprStr t)
• wnk_rpol {@mod ~t}.repr = toString "@mod " ++ toString (reprStr t)
• wnk_rpol {dup}.repr = toString "dup"
• wnk_rpol {~p; ~q}.repr = toString p.repr ++ toString " ; " ++ toString q.repr
• wnk_rpol {~w ⨀ ~p}.repr = toString (reprStr w) ++ toString " ⨀ " ++ toString p.repr
• wnk_rpol {~p ⨁ ~q}.repr = toString p.repr ++ toString " ⨁ " ++ toString q.repr
• wnk_rpol {~p*}.repr = toString p.repr ++ toString "*"
• wnk_rpol {skip}.repr = toString "skip"
• WeightedNetKAT.RPol.Drop.repr = toString "drop"

@[implicit_reducible]

instance WeightedNetKAT.instReprRPolOfFintypeOfEncodable {𝒮 N F : Type} [i : Fintype F] [e : Encodable F] [Repr F] [Repr N] [Repr 𝒮] [Listed F] : Repr (RPol 𝒮)

Equations

• WeightedNetKAT.instReprRPolOfFintypeOfEncodable = { reprPrec := fun (p : WeightedNetKAT.RPol 𝒮) (x : ℕ) => Std.Format.text p.repr }