def WGCL.BExpr.not {D Var : Type} (B : BExpr D Var) : BExpr D Var

Equations

• B.not σ = ¬B σ

def WGCL.BExpr.iver {D M Var : Type} [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [OmegaCompletePartialOrder M] [Zero M] (B : BExpr D Var) : Weighting D M Var →o Weighting D M Var

Equations

• i[B] = { toFun := fun (f : WGCL.Weighting D M Var) (σ : WGCL.Mem D Var) => if B σ then f σ else 0, monotone' := ⋯ }

instance WGCL.instAddLeftMonoWeighting {D M Var : Type} [AddCommMonoid M] [OmegaCompletePartialOrder M] [AddLeftMono M] : AddLeftMono (Weighting D M Var)

instance WGCL.instCovariantClass𝕎MemWeightingHSMulLe {D M W Var : Type} [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [CovariantClass W M HSMul.hSMul LE.le] : CovariantClass (𝕎 W (Mem D Var)) (Weighting D M Var) HSMul.hSMul LE.le

instance WGCL.instCovariantClassHSMulLe_wGCL {𝒮 : Type} [Mul 𝒮] [Preorder 𝒮] [MulLeftMono 𝒮] : CovariantClass 𝒮 𝒮 HSMul.hSMul LE.le

theorem WGCL.asjkdkasj {D M Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [AddCommMonoid M] [OmegaCompletePartialOrder M] [OrderBot M] [AddLeftMono M] {σ : Mem D Var} {f : Weighting D M Var →o Weighting D M Var} (c : OmegaCompletePartialOrder.Chain (Weighting D M Var)) : OmegaCompletePartialOrder.ωSup (c.map f) σ = sorry

def WGCL.wGCL.wp' {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [OrderBot M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] : 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.

def WGCL.wGCL.wp {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [OrderBot M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] (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.

@[simp]

theorem WGCL.wGCL.wp'_eq_wp {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [OrderBot M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] (C : wGCL D W Var) : C.wp' = C.wp

def WGCL.wGCL.Φ {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [OrderBot M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] (φ : BExpr D Var) (C' : wGCL D W Var) (f : Weighting D M Var) : Weighting D M Var →o Weighting D M Var

Equations

• WGCL.wGCL.Φ φ C' f = { toFun := fun (X : WGCL.Weighting D M Var) => i[φ] (C'.wp X) + i[φ.not] f, monotone' := ⋯ }

theorem WGCL.wGCL.wp_loop {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [OrderBot M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] {φ : BExpr D Var} {f : Weighting D M Var} (C' : wGCL D W Var) : (wp⟦while (~φ) { ~C' }⟧) f = OmegaCompletePartialOrder.lfp (Φ φ C' f)

instance WGCL.instAddLeftMonoWeighting_1 {D M Var : Type} [AddCommMonoid M] [OmegaCompletePartialOrder M] [AddLeftMono M] : AddLeftMono (Weighting D M Var)

instance WGCL.instCovariantClass𝕎MemWeightingHSMulLe_1 {D M W Var : Type} [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [CovariantClass W M HSMul.hSMul LE.le] : CovariantClass (𝕎 W (Mem D Var)) (Weighting D M Var) HSMul.hSMul LE.le

instance WGCL.instCovariantClassHSMulLe_wGCL_1 {𝒮 : Type} [Mul 𝒮] [Preorder 𝒮] [MulLeftMono 𝒮] : CovariantClass 𝒮 𝒮 HSMul.hSMul LE.le

@[reducible, inline]

abbrev WGCL.conv {D M Var : Type} [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] (c : OmegaCompletePartialOrder.Chain (Weighting D M Var)ᵒᵈ) (σ : Mem D Var) : OmegaCompletePartialOrder.Chain Mᵒᵈ

Equations

• WGCL.conv c σ = { toFun := fun (i : ℕ) => c i σ, monotone' := ⋯ }

instance WGCL.instOmegaCompletePartialOrderOrderDualWeighting {D M Var : Type} [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] : OmegaCompletePartialOrder (Weighting D M Var)ᵒᵈ

Equations

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

instance WGCL.instOmegaCompletePartialOrderBiWeighting {D M Var : Type} [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] : OmegaCompletePartialOrderBi (Weighting D M Var)

def WGCL.wGCL.wlp' {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] [OrderTop M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] : 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.

def WGCL.wGCL.wlp {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] [OrderTop M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] (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.

@[simp]

theorem WGCL.wGCL.wlp'_eq_wlp {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] [OrderTop M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] (C : wGCL D W Var) : C.wlp' = C.wlp

def WGCL.wGCL.Φl {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] [OrderTop M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] (φ : BExpr D Var) (C' : wGCL D W Var) (f : Weighting D M Var) : Weighting D M Var →o Weighting D M Var

Equations

• WGCL.wGCL.Φl φ C' f = { toFun := fun (X : WGCL.Weighting D M Var) => i[φ] (C'.wlp X) + i[φ.not] f, monotone' := ⋯ }

theorem WGCL.wGCL.wlp_loop {D M W Var : Type} [DecidableEq Var] [(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)] [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [instD : OmegaCompletePartialOrder Mᵒᵈ] [instBi : OmegaCompletePartialOrderBi M] [OrderTop M] [AddLeftMono M] [CovariantClass W M HSMul.hSMul LE.le] {φ : BExpr D Var} {f : Weighting D M Var} (C' : wGCL D W Var) : (wlp⟦while (~φ) { ~C' }⟧) f = OmegaCompletePartialOrder.gfp (Φl φ C' f)

def WGCL.«termWp⟦_⟧» : Lean.ParserDescr

Equations

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

def WGCL.«termWp[_,_,_,_]⟦_⟧» : Lean.ParserDescr

Equations

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

def WGCL.«termWp⟦_⟧(_)» : Lean.ParserDescr

Equations

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

def WGCL.«termWp[_,_,_,_]⟦_⟧(_)» : Lean.ParserDescr

Equations

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

def WGCL.«termWlp⟦_⟧» : Lean.ParserDescr

Equations

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

def WGCL.«termWlp[_,_,_,_]⟦_⟧» : Lean.ParserDescr

Equations

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

def WGCL.«termWlp⟦_⟧(_)» : Lean.ParserDescr

Equations

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

def WGCL.«termWlp[_,_,_,_]⟦_⟧(_)» : Lean.ParserDescr

Equations

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

def WGCL.wGCL.unexpandWp : Lean.PrettyPrinter.Unexpander

Equations

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

def WGCL.wGCL.unexpandWlp : Lean.PrettyPrinter.Unexpander

Equations

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

def WGCL.«termI[_]» : Lean.ParserDescr

Equations

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

def WGCL.BExpr.unexpandIver : Lean.PrettyPrinter.Unexpander

Equations

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

instance WGCL.instAddLeftMonoWeighting_2 {D M Var : Type} [AddCommMonoid M] [OmegaCompletePartialOrder M] [AddLeftMono M] : AddLeftMono (Weighting D M Var)

instance WGCL.instCovariantClass𝕎MemWeightingHSMulLe_2 {D M W Var : Type} [Monoid W] [AddCommMonoid M] [inst : DistribMulAction W M] [OmegaCompletePartialOrder M] [CovariantClass W M HSMul.hSMul LE.le] : CovariantClass (𝕎 W (Mem D Var)) (Weighting D M Var) HSMul.hSMul LE.le

instance WGCL.instCovariantClassHSMulLe_wGCL_2 {𝒮 : Type} [Mul 𝒮] [Preorder 𝒮] [MulLeftMono 𝒮] : CovariantClass 𝒮 𝒮 HSMul.hSMul LE.le