inductive pGCL.Act : Type

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

def pGCL.instBEqAct.beq : Act → Act → Bool

Equations

• pGCL.instBEqAct.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance pGCL.instBEqAct : BEq Act

Equations

• pGCL.instBEqAct = { beq := pGCL.instBEqAct.beq }

@[implicit_reducible]

instance pGCL.instDecidableEqAct : DecidableEq Act

Equations

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

@[implicit_reducible]

instance pGCL.instInhabitedAct : Inhabited Act

Equations

• pGCL.instInhabitedAct = { default := pGCL.instInhabitedAct.default }

def pGCL.instInhabitedAct.default : Act

Equations

• pGCL.instInhabitedAct.default = pGCL.Act.L

@[implicit_reducible]

noncomputable instance pGCL.Act.instFintype : Fintype Act

Equations

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

inductive pGCL.Termination : Type

• fault : Termination
• term : Termination

@[reducible]

def pGCL.Conf₀ {𝒱 : Type u_1} (Γ : 𝒱 → Type u_3) : Type (max u_3 u_1)

Equations

• pGCL.Conf₀ Γ = (pGCL Γ × pGCL.State Γ)

@[reducible]

def pGCL.Conf₁ {𝒱 : Type u_1} (Γ : 𝒱 → Type u_3) : Type (max u_3 u_1)

Equations

• pGCL.Conf₁ Γ = ((pGCL Γ ⊕ pGCL.Termination) × pGCL.State Γ)

@[reducible]

def pGCL.Conf' {𝒱 : Type u_1} (Γ : 𝒱 → Type u_3) : Type (max u_3 u_1)

Equations

• pGCL.Conf' Γ = Conf (pGCL Γ) (pGCL.State Γ) pGCL.Termination

def Lean.Parser.Category.cpgcl_conf : Category

Equations

• Lean.Parser.Category.cpgcl_conf = { }

def pGCL.Conf.cpgcl_conf.quot : Lean.ParserDescr

Equations

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

def pGCL.Conf.«termConf[_,_]» : Lean.ParserDescr

Equations

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

def pGCL.Conf.«termConf[⊥]» : Lean.ParserDescr

Equations

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

def pGCL.Conf.cpgcl_conf₀.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cpgcl_conf₀ : Category

Equations

• Lean.Parser.Category.cpgcl_conf₀ = { }

def pGCL.Conf.«termConf₀[_,_]» : Lean.ParserDescr

Equations

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

def pGCL.Conf.cpgcl_conf₁.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cpgcl_conf₁ : Category

Equations

• Lean.Parser.Category.cpgcl_conf₁ = { }

def pGCL.Conf.«termConf₁[_,_]» : Lean.ParserDescr

Equations

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

def pGCL.Conf.«cpgcl_conf↯» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf↯» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf↯» 1024 (Lean.ParserDescr.symbol "↯")

def pGCL.Conf.«cpgcl_conf↯_» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf↯_» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf↯_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↯") (Lean.ParserDescr.cat `term 0))

def pGCL.Conf.«cpgcl_conf⇓» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf⇓» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf⇓» 1024 (Lean.ParserDescr.symbol "⇓")

def pGCL.Conf.«cpgcl_conf⇓_» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf⇓_» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf⇓_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⇓") (Lean.ParserDescr.cat `term 0))

def pGCL.Conf.cpgcl_conf_ : Lean.ParserDescr

Equations

• pGCL.Conf.cpgcl_conf_ = Lean.ParserDescr.node `pGCL.Conf.cpgcl_conf_ 1022 (Lean.ParserDescr.cat `cpgcl_prog 0)

def pGCL.Conf.cpgcl_conf₀_ : Lean.ParserDescr

Equations

• pGCL.Conf.cpgcl_conf₀_ = Lean.ParserDescr.node `pGCL.Conf.cpgcl_conf₀_ 1022 (Lean.ParserDescr.cat `cpgcl_prog 0)

def pGCL.Conf.«cpgcl_conf₁↯» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf₁↯» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf₁↯» 1024 (Lean.ParserDescr.symbol "↯")

def pGCL.Conf.«cpgcl_conf₁↯_» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf₁↯_» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf₁↯_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↯") (Lean.ParserDescr.cat `term 0))

def pGCL.Conf.«cpgcl_conf₁⇓» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf₁⇓» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf₁⇓» 1024 (Lean.ParserDescr.symbol "⇓")

def pGCL.Conf.«cpgcl_conf₁⇓_» : Lean.ParserDescr

Equations

• pGCL.Conf.«cpgcl_conf₁⇓_» = Lean.ParserDescr.node `pGCL.Conf.«cpgcl_conf₁⇓_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⇓") (Lean.ParserDescr.cat `term 0))

def pGCL.Conf.cpgcl_conf₁_ : Lean.ParserDescr

Equations

• pGCL.Conf.cpgcl_conf₁_ = Lean.ParserDescr.node `pGCL.Conf.cpgcl_conf₁_ 1022 (Lean.ParserDescr.cat `cpgcl_prog 0)

@[simp]

theorem pGCL.seq_ne_right {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₁ C₂ : pGCL Γ✝} : ¬pgcl {@C₁ ; @C₂} = C₂

@[simp]

theorem pGCL.right_ne_seq {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₂ C₁ : pGCL Γ✝} : ¬C₂ = pgcl {@C₁ ; @C₂}

@[simp]

theorem pGCL.left_ne_seq {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₁ C₂ : pGCL Γ✝} : ¬C₁ = pgcl {@C₁ ; @C₂}

@[simp]

theorem pGCL.seq_ne_left {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₁ C₂ : pGCL Γ✝} : ¬pgcl {@C₁ ; @C₂} = C₁

def pGCL.after {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C' : pGCL Γ) : Conf₁ Γ → Conf₁ Γ

Equations

• C'.after (Sum.inl c, σ) = (Sum.inl (pgcl {@c ; @C'}), σ)
• C'.after (Sum.inr pGCL.Termination.term, σ) = (Sum.inl C', σ)
• C'.after (Sum.inr pGCL.Termination.fault, σ) = (Sum.inr pGCL.Termination.fault, σ)

def pGCL.after_inj {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C' : pGCL Γ) : Function.Injective C'.after

Equations

• ⋯ = ⋯

@[simp]

theorem pGCL.after_eq_seq_iff {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₂ : pGCL Γ✝} {c : Conf₁ Γ✝} {C₁ : pGCL Γ✝} {σ : State Γ✝} : C₂.after c = (Sum.inl (pgcl {@C₁ ; @C₂}), σ) ↔ c = (Sum.inl C₁, σ)

@[simp]

theorem pGCL.after_term {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₂ : pGCL Γ✝} {σ : State Γ✝} : C₂.after (Sum.inr Termination.term, σ) = (Sum.inl C₂, σ)

@[simp]

theorem pGCL.after_fault {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₂ : pGCL Γ✝} {σ : State Γ✝} : C₂.after (Sum.inr Termination.fault, σ) = (Sum.inr Termination.fault, σ)

@[simp]

theorem pGCL.after_eq_right {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₂ : pGCL Γ✝} {a : Conf₁ Γ✝} {σ : State Γ✝} : C₂.after a = (Sum.inl C₂, σ) ↔ a = (Sum.inr Termination.term, σ)

@[simp]

theorem pGCL.after_neq_term {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {C₂ : pGCL Γ✝} {c' : Conf₁ Γ✝} {σ : State Γ✝} : ¬C₂.after c' = (Sum.inr Termination.term, σ)

theorem pGCL.tsum_after_eq {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C₂ : pGCL Γ) {f g : Conf₁ Γ → ENNReal} (hg₂ : ∀ (σ : State Γ), g (Sum.inr Termination.term, σ) = 0) (hg₂' : ∀ (σ : State Γ), f (Sum.inr Termination.fault, σ) = 0 → g (Sum.inr Termination.fault, σ) = 0) (hg₃ : ∀ (C : pGCL Γ) (σ : State Γ), ¬g (Sum.inl C, σ) = 0 → ∃ (a : Conf₁ Γ), ¬f a = 0 ∧ C₂.after a = (Sum.inl C, σ)) (hf₂ : ∀ (σ : State Γ), ¬f (Sum.inr Termination.term, σ) = 0 → f (Sum.inr Termination.term, σ) = g (Sum.inl C₂, σ)) (hf₂' : ∀ (σ : State Γ), ¬f (Sum.inr Termination.fault, σ) = 0 → f (Sum.inr Termination.fault, σ) = g (Sum.inr Termination.fault, σ)) (hf₃ : ∀ (C : pGCL Γ) (σ : State Γ), ¬f (Sum.inl C, σ) = 0 → f (Sum.inl C, σ) = g (Sum.inl (pgcl {@C ; @C₂}), σ)) : ∑' (s : Conf₁ Γ), g s = ∑' (s : Conf₁ Γ), f s

theorem pGCL.tsum_after_eq' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C₂ : pGCL Γ) {f g : ENNReal × Conf₁ Γ → ENNReal} (hg₂ : ∀ (p : ENNReal) (σ : State Γ), g (p, Sum.inr Termination.term, σ) = 0) (hg₂' : ∀ (p : ENNReal) (σ : State Γ), f (p, Sum.inr Termination.fault, σ) = 0 → g (p, Sum.inr Termination.fault, σ) = 0) (hg₃ : ∀ (p : ENNReal) (C : pGCL Γ) (σ : State Γ), ¬g (p, Sum.inl C, σ) = 0 → ∃ (a : Conf₁ Γ), ¬f (p, a) = 0 ∧ C₂.after a = (Sum.inl C, σ)) (hf₂ : ∀ (p : ENNReal) (σ : State Γ), ¬f (p, Sum.inr Termination.term, σ) = 0 → f (p, Sum.inr Termination.term, σ) = g (p, Sum.inl C₂, σ)) (hf₂' : ∀ (p : ENNReal) (σ : State Γ), ¬f (p, Sum.inr Termination.fault, σ) = 0 → f (p, Sum.inr Termination.fault, σ) = g (p, Sum.inr Termination.fault, σ)) (hf₃ : ∀ (p : ENNReal) (C : pGCL Γ) (σ : State Γ), ¬f (p, Sum.inl C, σ) = 0 → f (p, Sum.inl C, σ) = g (p, Sum.inl (pgcl {@C ; @C₂}), σ)) : ∑' (s : ENNReal × Conf₁ Γ), g s = ∑' (s : ENNReal × Conf₁ Γ), f s

theorem pGCL.tsum_after_eq'' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C₂ : pGCL Γ) {f g : ENNReal × Conf₁ Γ → ENNReal} (hg₂ : ∀ (p : ENNReal) (σ : State Γ), g (p, Sum.inr Termination.term, σ) = 0) (hg₂' : ∀ (p : ENNReal) (σ : State Γ), f (p, Sum.inr Termination.fault, σ) = 0 → g (p, Sum.inr Termination.fault, σ) = 0) (hg₃ : ∀ (p : ENNReal) (C : pGCL Γ) (σ : State Γ), ¬g (p, Sum.inl C, σ) = 0 → ∃ (a : Conf₁ Γ), ¬f (p, a) = 0 ∧ C₂.after a = (Sum.inl C, σ)) (hf : ∀ (a : ENNReal), (∀ (C : pGCL Γ) (σ : State Γ), ¬f (a, Sum.inl C, σ) = 0 → g (a, C₂.after (Sum.inl C, σ)) = f (a, Sum.inl C, σ)) ∧ ∀ (t : Termination) (σ : State Γ), ¬f (a, Sum.inr t, σ) = 0 → g (a, C₂.after (Sum.inr t, σ)) = f (a, Sum.inr t, σ)) : ∑' (s : ENNReal × Conf₁ Γ), g s = ∑' (s : ENNReal × Conf₁ Γ), f s

theorem pGCL.tsum_after_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C₂ : pGCL Γ) {f g : Conf₁ Γ → ENNReal} (h₂ : ∀ (σ : State Γ), g (Sum.inr Termination.term, σ) ≤ f (Sum.inl C₂, σ)) : (∀ (σ : State Γ), g (Sum.inr Termination.fault, σ) ≤ f (Sum.inr Termination.fault, σ)) → (∀ (C : pGCL Γ) (σ : State Γ), g (Sum.inl C, σ) ≤ f (Sum.inl (pgcl {@C ; @C₂}), σ)) → ∑' (s : Conf₁ Γ), g s ≤ ∑' (s : Conf₁ Γ), f s

theorem pGCL.tsum_after_le' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C₂ : pGCL Γ) {f g : ENNReal × Conf₁ Γ → ENNReal} (h₁ : ∀ (p : ENNReal) (σ : State Γ), g (p, Sum.inr Termination.term, σ) ≤ f (p, Sum.inl C₂, σ)) (h₂ : ∀ (p : ENNReal) (σ : State Γ), g (p, Sum.inr Termination.fault, σ) ≤ f (p, Sum.inr Termination.fault, σ)) (h₃ : ∀ (p : ENNReal) (C : pGCL Γ) (σ : State Γ), g (p, Sum.inl C, σ) ≤ f (p, Sum.inl (pgcl {@C ; @C₂}), σ)) : ∑' (s : ENNReal × Conf₁ Γ), g s ≤ ∑' (s : ENNReal × Conf₁ Γ), f s