inductive WGCL.Act : Type

• N : Act
• L : Act
• R : Act

instance WGCL.instToExprAct : Lean.ToExpr Act

Equations

• WGCL.instToExprAct = { toExpr := WGCL.toExprAct✝, toTypeExpr := Lean.Expr.const `WGCL.Act [] }

structure WGCL.Conf (D W Var : Type) : Type

• C : WithBot (wGCL D W Var)
• σ : Mem D Var
• n : ℕ
• β : List Act

noncomputable def WGCL.Conf.size {D W Var : Type} (κ : Conf D W Var) : ℕ

Equations

• κ.size = match κ.C with | none => 0 | some C => 1 + sizeOf C

def WGCL.«termConf_⟨_,_,_,_⟩» : Lean.ParserDescr

Equations

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

def WGCL.«termConf_⟨⊥,_,_,_⟩» : Lean.ParserDescr

Equations

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

def WGCL.Conf.unexpand : Lean.PrettyPrinter.Unexpander

Equations

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

inductive WGCL.Op {D W Var : Type} [DecidableEq Var] [One W] : Conf D W Var → W → Conf D W Var → Prop

• Assign {D W Var : Type} [DecidableEq Var] [One W] {x : Var} {σ : Mem D Var} {n : ℕ} {β : List Act} {E : AExpr D Var} : Op (conf ⟨~x := ~E,σ,n,β⟩) 1 conf ⟨⊥,σ[x ↦ E σ],n + 1,β⟩
• Weight {D W Var : Type} [DecidableEq Var] [One W] {a : 𝕎 W (Mem D Var)} {σ : Mem D Var} {n : ℕ} {β : List Act} : Op (conf ⟨⊙~a,σ,n,β⟩) (a σ) conf ⟨⊥,σ,n + 1,β⟩
• Seq₁ {D W Var : Type} [DecidableEq Var] [One W] {C₁ : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} {a : W} {σ' : Mem D Var} {C₂ : wGCL D W Var} : Op (Conf.mk (some C₁) σ n β) a conf ⟨⊥,σ',n + 1,β⟩ → Op (conf ⟨~C₁; ~C₂,σ,n,β⟩) a (Conf.mk (some C₂) σ' (n + 1) β)
• Seq₂ {D W Var : Type} [DecidableEq Var] [One W] {C₁ : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} {a : W} {C₁' : wGCL D W Var} {σ' : Mem D Var} {C₂ : wGCL D W Var} : Op (Conf.mk (some C₁) σ n β) a (Conf.mk (some C₁') σ' (n + 1) β) → Op (conf ⟨~C₁; ~C₂,σ,n,β⟩) a (conf ⟨~C₁'; ~C₂,σ',n + 1,β⟩)
• If {D W Var : Type} [DecidableEq Var] [One W] {φ : BExpr D Var} {C₁ C₂ : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} (h : φ σ) : Op (conf ⟨if (~φ) { ~C₁ } else { ~C₂ },σ,n,β⟩) 1 (Conf.mk (some C₁) σ (n + 1) β)
• Else {D W Var : Type} [DecidableEq Var] [One W] {φ : BExpr D Var} {C₁ C₂ : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} (h : ¬φ σ) : Op (conf ⟨if (~φ) { ~C₁ } else { ~C₂ },σ,n,β⟩) 1 (Conf.mk (some C₂) σ (n + 1) β)
• BranchL {D W Var : Type} [DecidableEq Var] [One W] {C₁ C₂ : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} : Op conf ⟨{ ~C₁ } ⊕ { ~C₂ },σ,n,β⟩ 1 (Conf.mk (some C₁) σ (n + 1) (Act.L :: β))
• BranchR {D W Var : Type} [DecidableEq Var] [One W] {C₁ C₂ : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} : Op conf ⟨{ ~C₁ } ⊕ { ~C₂ },σ,n,β⟩ 1 (Conf.mk (some C₂) σ (n + 1) (Act.R :: β))
• While {D W Var : Type} [DecidableEq Var] [One W] {φ : BExpr D Var} {C : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} (h : φ σ) : Op (conf ⟨while (~φ) { ~C },σ,n,β⟩) 1 (conf ⟨~C; while (~φ) { ~C },σ,n + 1,β⟩)
• Break {D W Var : Type} [DecidableEq Var] [One W] {φ : BExpr D Var} {C : wGCL D W Var} {σ : Mem D Var} {n : ℕ} {β : List Act} (h : ¬φ σ) : Op (conf ⟨while (~φ) { ~C },σ,n,β⟩) 1 conf ⟨⊥,σ,n + 1,β⟩

def WGCL.Conf.succ {D W Var : Type} [DecidableEq Var] [One W] (κ : Conf D W Var) : Set (Conf D W Var)

Equations

• κ.succ = {κ' : WGCL.Conf D W Var | ∃ (a : W), WGCL.Op κ a κ'}

@[irreducible]

def WGCL.Conf.wgt {D W Var : Type} [Zero W] [One W] [DecidableEq (wGCL D W Var)] (κ κ' : Conf D W Var) : W

Equations

• (WGCL.Conf.mk none σ n β).wgt (WGCL.Conf.mk none σ_1 n_1 β_1) = 1
• conf ⟨⊙~a,σ,n,β⟩.wgt κ' = a σ
• conf ⟨~C₁; ~C₂,σ,n,β⟩.wgt (conf ⟨~C₁'; ~C₂',σ',n',β'⟩) = if C₂ = C₂' then (WGCL.Conf.mk (some C₁) σ n β).wgt (WGCL.Conf.mk (some C₁') σ' n' β') else 0
• conf ⟨~C₁; ~C₂,σ,n,β⟩.wgt (WGCL.Conf.mk (some C₂') σ' n' β') = if C₂ = C₂' then (WGCL.Conf.mk (some C₁) σ n β).wgt conf ⟨⊥,σ',n',β'⟩ else 0
• conf ⟨~a := ~a_1,σ,n,β⟩.wgt κ' = 1
• conf ⟨{ ~a } ⊕ { ~a_1 },σ,n,β⟩.wgt κ' = 1
• conf ⟨if (~a) { ~a_1 } else { ~a_2 },σ,n,β⟩.wgt κ' = 1
• conf ⟨while (~a) { ~a_1 },σ,n,β⟩.wgt κ' = 1
• κ.wgt κ' = 0

theorem WGCL.Conf.exists_a_iff {D W Var : Type} [DecidableEq Var] [Zero W] [One W] [DecidableEq (wGCL D W Var)] {κ κ' : Conf D W Var} : (∃ (a : W), Op κ a κ') ↔ Op κ (κ.wgt κ') κ'

theorem WGCL.Conf.succ_eq_wgt {D W Var : Type} [DecidableEq Var] [Zero W] [One W] [DecidableEq (wGCL D W Var)] {κ κ' : Conf D W Var} : κ' ∈ κ.succ ↔ Op κ (κ.wgt κ') κ'

theorem WGCL.Conf.succ_unique {D W Var : Type} [DecidableEq Var] [One W] {κ κ' : Conf D W Var} (h : κ' ∈ κ.succ) : ∃! a : W, Op κ a κ'

structure WGCL.Path (D W Var : Type) [DecidableEq Var] [One W] : Type

• confs : List (Conf D W Var)
• prop (i : ℕ) (hi : i < self.confs.length - 1) : self.confs[i + 1] ∈ self.confs[i].succ

def WGCL.Path.wgt {D W Var : Type} [DecidableEq Var] [Zero W] [One W] [DecidableEq (wGCL D W Var)] [Monoid W] (π : Path D W Var) : W

Equations

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

def WGCL.Path.terminal {D W Var : Type} [DecidableEq Var] [One W] (π : Path D W Var) : Prop

Equations

• π.terminal = (Option.map (fun (x : WGCL.Conf D W Var) => x.C) π.confs.getLast? = some ⊥)

def WGCL.TPath {D W Var : Type} [DecidableEq Var] [One W] (κ₀ : Conf D W Var) : Set (Path D W Var)

Equations

• WGCL.TPath κ₀ = {π : WGCL.Path D W Var | π.confs[0]? = some κ₀ ∧ π.terminal}

@[simp]

def WGCL.TPath.nonempty {D W Var : Type} [DecidableEq Var] [One W] {κ₀ : Conf D W Var} (π : ↑(TPath κ₀)) : ¬(↑π).confs = []

Equations

• ⋯ = ⋯

def WGCL.TPath.getLast {D W Var : Type} [DecidableEq Var] [One W] {κ₀ : Conf D W Var} (π : ↑(TPath κ₀)) : Conf D W Var

Equations

• WGCL.TPath.getLast π = (↑π).confs.getLast ⋯

def WGCL.wGCL.terminatesCertainlyOn {D W Var : Type} [DecidableEq Var] [One W] (C : wGCL D W Var) (σ : Mem D Var) : Prop

Equations

• C.terminatesCertainlyOn σ = ∃ (n : ℕ), ∀ (π : WGCL.Path D W Var), π.confs[0]? = some (WGCL.Conf.mk (some C) σ 0 []) ∧ π.confs.length ≤ n

def WGCL.wGCL.terminatesCertainly {D W Var : Type} [DecidableEq Var] [One W] (C : wGCL D W Var) : Prop

Equations

• C.terminatesCertainly = ∀ (σ : WGCL.Mem D Var), C.terminatesCertainlyOn σ

noncomputable def WGCL.op {D M W Var : Type} [DecidableEq Var] [Zero W] [One W] [DecidableEq (wGCL D W Var)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [TopologicalSpace M] (C : wGCL D W Var) : Weighting D M Var → Weighting D M Var

Equations

• WGCL.op C f σ = ∑' (π : ↑(WGCL.TPath (WGCL.Conf.mk (some C) σ 0 []))), (↑π).wgt ⊗ f (WGCL.TPath.getLast π).σ

noncomputable def WGCL.op' {D M W Var : Type} [DecidableEq Var] [Zero W] [One W] [DecidableEq (wGCL D W Var)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [TopologicalSpace M] [OmegaCompletePartialOrder M] [CovariantClass W M HSMul.hSMul LE.le] [OrderClosedTopology M] [IsOrderedAddMonoid M] (C : wGCL D W Var) : Weighting D M Var →o Weighting D M Var

Equations

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