Documentation

PGCL.Conf

inductive pGCL.Act :

L : Act
R : Act
N : Act

Instances For

instance pGCL.instBEqAct :

Equations

pGCL.instBEqAct = { beq := pGCL.beqAct✝ }

instance pGCL.instDecidableEqAct :

DecidableEq Act

Equations

pGCL.instDecidableEqAct x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance pGCL.instInhabitedAct :

Equations

pGCL.instInhabitedAct = { default := pGCL.Act.L }

noncomputable instance pGCL.Act.instFintype :

Equations

pGCL.Act.instFintype = { elems := {pGCL.Act.L , pGCL.Act.R , pGCL.Act.N }, complete := pGCL.Act.instFintype._proof_3 }

@[reducible]

def pGCL.Conf (ϖ : Type u_1) :

Type u_1

Equations

pGCL.Conf ϖ = Option (Option (pGCL ϖ) × pGCL.States ϖ)

Instances For

def pGCL.Conf.«term·⟨⇓_,_⟩» :

Lean.ParserDescr

Equations

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

Instances For

def pGCL.Conf.«term·⟨_,_⟩» :

Lean.ParserDescr

Equations

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

Instances For

def pGCL.Conf.«term·⟨skip,_⟩» :

Lean.ParserDescr

Equations

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

Instances For

def pGCL.Conf.«term·⟨if_Then_Else_,_⟩» :

Lean.ParserDescr

Equations

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

Instances For

def pGCL.Conf.«term·⟨_[]_,_⟩» :

Lean.ParserDescr

Equations

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

Instances For

def pGCL.Conf.«term·⟨_[_]_,_⟩» :

Lean.ParserDescr

Equations

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

Instances For

def pGCL.Conf.«term·⟨tick_,_⟩» :

Lean.ParserDescr

Equations

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

Instances For

instance pGCL.Conf.instBot {ϖ : Type u_1} :

Equations

pGCL.Conf.instBot = { bot := none }

instance pGCL.Conf.instCoeProdOptionStates {ϖ : Type u_1} :

Coe (Option (pGCL ϖ) × States ϖ) (Conf ϖ)

Equations

pGCL.Conf.instCoeProdOptionStates = { coe := some }

noncomputable instance pGCL.Conf.decidableEq {ϖ : Type u_1} :

DecidableEq (Conf ϖ)

Equations

pGCL.Conf.decidableEq = Classical.typeDecidableEq (pGCL.Conf ϖ)

@[simp]

theorem pGCL.seq_ne_right {ϖ✝ : Type u_1} {C₁ C₂ : pGCL ϖ✝} :

¬C₁ ;; C₂ = C₂

@[simp]

theorem pGCL.right_ne_seq {ϖ✝ : Type u_1} {C₂ C₁ : pGCL ϖ✝} :

¬C₂ = C₁ ;; C₂

@[simp]

theorem pGCL.left_ne_seq {ϖ✝ : Type u_1} {C₁ C₂ : pGCL ϖ✝} :

¬C₁ = C₁ ;; C₂

@[simp]

theorem pGCL.seq_ne_left {ϖ✝ : Type u_1} {C₁ C₂ : pGCL ϖ✝} :

¬C₁ ;; C₂ = C₁

def pGCL.after {ϖ : Type u_1} (C' : pGCL ϖ) :

Conf ϖ → Conf ϖ

Equations

Instances For

def pGCL.after_inj {ϖ : Type u_1} (C' : pGCL ϖ) :

Function.Injective C'.after

Equations

⋯ = ⋯

Instances For

@[simp]

theorem pGCL.after_eq_seq_iff {ϖ✝ : Type u_1} {C₁ C₂ : pGCL ϖ✝} {σ : States ϖ✝} {c : Conf ϖ✝} :

C₂.after c = ·⟨C₁ ;; C₂,σ⟩ ↔ c = ·⟨C₁,σ⟩

@[simp]

theorem pGCL.after_none {ϖ✝ : Type u_1} {C₂ : pGCL ϖ✝} :

C₂.after none = none

@[simp]

theorem pGCL.after_sink {ϖ✝ : Type u_1} {C₂ : pGCL ϖ✝} {σ : States ϖ✝} :

C₂.after (some (none , σ)) = ·⟨C₂,σ⟩

@[simp]

theorem pGCL.after_eq_right {ϖ✝ : Type u_1} {C₂ : pGCL ϖ✝} {a : Conf ϖ✝} {σ : States ϖ✝} :

C₂.after a = ·⟨C₂,σ⟩ ↔ a = some (none , σ)

@[simp]

theorem pGCL.after_neq_sink {ϖ✝ : Type u_1} {C₂ : pGCL ϖ✝} {c' : Conf ϖ✝} {σ : States ϖ✝} :

¬C₂.after c' = some (none , σ)

@[simp]

theorem pGCL.after_eq_none {ϖ✝ : Type u_1} {C₂ : pGCL ϖ✝} {c' : Conf ϖ✝} :

C₂.after c' = none ↔ c' = none

theorem pGCL.tsum_after_eq {ϖ : Type u_1} (C₂ : pGCL ϖ) {f g : Conf ϖ → ENNReal} (hg₁ : f none = 0 → g none = 0) (hg₂ : ∀ (σ : States ϖ), g (some (none , σ)) = 0) (hg₃ : ∀ (C : pGCL ϖ) (σ : States ϖ), ¬g (·⟨C,σ⟩) = 0 → ∃ (a : Conf ϖ), ¬f a = 0 ∧ C₂.after a = ·⟨C,σ⟩) (hf₁ : ¬f none = 0 → f none = g none) (hf₂ : ∀ (σ : States ϖ), ¬f (some (none , σ)) = 0 → f (some (none , σ)) = g (·⟨C₂,σ⟩)) (hf₃ : ∀ (C : pGCL ϖ) (σ : States ϖ), ¬f (·⟨C,σ⟩) = 0 → f (·⟨C,σ⟩) = g (·⟨C ;; C₂,σ⟩)) :

∑' (s : Conf ϖ), g s = ∑' (s : Conf ϖ), f s

theorem pGCL.tsum_after_le {ϖ : Type u_1} (C₂ : pGCL ϖ) {f g : Conf ϖ → ENNReal} (h₁ : g none ≤ f none) (h₂ : ∀ (σ : States ϖ), g (some (none , σ)) ≤ f (·⟨C₂,σ⟩)) :

(∀ (C : pGCL ϖ) (σ : States ϖ), g (·⟨C,σ⟩) ≤ f (·⟨C ;; C₂,σ⟩)) → ∑' (s : Conf ϖ), g s ≤ ∑' (s : Conf ϖ), f s