Small step operational semantics for pGCL

Main definitions

• pGCL.SmallStep: The inductive definition of the probabilistic small step semantics of pGCL.

inductive pGCL.SmallStep {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] : Conf₀ Γ → Act → ENNReal → Conf₁ Γ → Prop

Probabilistic small step operational semantics for pGCL

• skip {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} : (pgcl {skip}, σ) ⤳[Act.N,1] (Sum.inr Termination.term, σ)
• assign {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {x : 𝒱} {e : State Γ → Γ x} {σ : State Γ} : (pgcl {@x := @e}, σ) ⤳[Act.N,1] (Sum.inr Termination.term, σ[x ↦ e σ])
• prob {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C : pGCL Γ} {p : ProbExp Γ} {σ : State Γ} : (pgcl {{ @C } [@p] { @C }}, σ) ⤳[Act.N,1] (Sum.inl C, σ)
• prob_L {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C₁ C₂ : pGCL Γ} {p : ProbExp Γ} {σ : State Γ} (h : ¬C₁ = C₂) (h' : 0 < p σ) : (pgcl {{ @C₁ } [@p] { @C₂ }}, σ) ⤳[Act.N,p σ] (Sum.inl C₁, σ)
• prob_R {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C₁ C₂ : pGCL Γ} {p : ProbExp Γ} {σ : State Γ} (h : ¬C₁ = C₂) (h' : p σ < 1) : (pgcl {{ @C₁ } [@p] { @C₂ }}, σ) ⤳[Act.N,1 - p σ] (Sum.inl C₂, σ)
• nonDet_L {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C₁ C₂ : pGCL Γ} {σ : State Γ} : (pgcl {{ @C₁ } [] { @C₂ }}, σ) ⤳[Act.L,1] (Sum.inl C₁, σ)
• nonDet_R {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C₁ C₂ : pGCL Γ} {σ : State Γ} : (pgcl {{ @C₁ } [] { @C₂ }}, σ) ⤳[Act.R,1] (Sum.inl C₂, σ)
• tick {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {r : State Γ → ENNReal} {σ : State Γ} : (pgcl {tick(@r)}, σ) ⤳[Act.N,1] (Sum.inr Termination.term, σ)
• observe₁ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {b : State Γ → Prop} {σ : State Γ} : b σ → (pgcl {observe(@b)}, σ) ⤳[Act.N,1] (Sum.inr Termination.term, σ)
• observe₂ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {b : State Γ → Prop} {σ : State Γ} : ¬b σ → (pgcl {observe(@b)}, σ) ⤳[Act.N,1] (Sum.inr Termination.fault, σ)
• seq_L {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C₁ : pGCL Γ} {σ : State Γ} {α : Act} {p : ENNReal} {τ : State Γ} {C₂ : pGCL Γ} : ((C₁, σ) ⤳[α,p] (Sum.inr Termination.term, τ)) → (pgcl {@C₁ ; @C₂}, σ) ⤳[α,p] (Sum.inl C₂, τ)
• seq_R {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C₁ : pGCL Γ} {σ : State Γ} {α : Act} {p : ENNReal} {C₁' : pGCL Γ} {τ : State Γ} {C₂ : pGCL Γ} : ((C₁, σ) ⤳[α,p] (Sum.inl C₁', τ)) → (pgcl {@C₁ ; @C₂}, σ) ⤳[α,p] (Sum.inl (pgcl {@C₁' ; @C₂}), τ)
• seq_F {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C₁ : pGCL Γ} {σ : State Γ} {C₂ : pGCL Γ} : ((C₁, σ) ⤳[Act.N,1] (Sum.inr Termination.fault, σ)) → (pgcl {@C₁ ; @C₂}, σ) ⤳[Act.N,1] (Sum.inr Termination.fault, σ)
• loop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {b : State Γ → Prop} {C : pGCL Γ} {σ : State Γ} : ¬b σ → (pgcl {while @b { @C }}, σ) ⤳[Act.N,1] (Sum.inr Termination.term, σ)
• loop' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {b : State Γ → Prop} {C : pGCL Γ} {σ : State Γ} : b σ → (pgcl {while @b { @C }}, σ) ⤳[Act.N,1] (Sum.inl (pgcl {@C ; while @b { @C }}), σ)

def pGCL.«term_⤳[_,_]_» : Lean.TrailingParserDescr

Probabilistic small step operational semantics for pGCL

Equations

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

@[simp]

theorem pGCL.SmallStep.p_pos {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {c' : Conf₁ Γ} {α : Act} {p : ENNReal} (h : c ⤳[α,p] c') : 0 < p

@[simp]

theorem pGCL.SmallStep.p_ne_zero {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {c' : Conf₁ Γ} {α : Act} {p : ENNReal} (h : c ⤳[α,p] c') : ¬p = 0

@[simp]

theorem pGCL.SmallStep.p_le_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {c' : Conf₁ Γ} {α : Act} {p : ENNReal} (h : c ⤳[α,p] c') : p ≤ 1

@[simp]

theorem pGCL.SmallStep.skip_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {α : Act} {p : ENNReal} : ((pgcl {skip}, σ) ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = (Sum.inr Termination.term, σ)

theorem pGCL.SmallStep.to_fault {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {σ : State Γ} {α : Act} {p : ENNReal} : (c ⤳[α,p] (Sum.inr Termination.fault, σ)) ↔ p = 1 ∧ α = Act.N ∧ ((∃ (C₁ : pGCL Γ) (C₂ : pGCL Γ), c = (pgcl {@C₁ ; @C₂}, σ) ∧ (C₁, σ) ⤳[Act.N,p] (Sum.inr Termination.fault, σ)) ∨ ∃ (b : State Γ → Prop), c = (pgcl {observe(@b)}, σ) ∧ ¬b σ)

theorem pGCL.SmallStep.of_to_fault_p {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {σ : State Γ} {α : Act} {p : ENNReal} (h : c ⤳[α,p] (Sum.inr Termination.fault, σ)) : p = 1

theorem pGCL.SmallStep.of_to_fault_act {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {σ : State Γ} {α : Act} {p : ENNReal} (h : c ⤳[α,p] (Sum.inr Termination.fault, σ)) : α = Act.N

theorem pGCL.SmallStep.of_to_fault_mem {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {C : pGCL Γ} {α : Act} {p : ENNReal} {σ' : State Γ} (h : (C, σ) ⤳[α,p] (Sum.inr Termination.fault, σ')) : σ = σ'

theorem pGCL.SmallStep.of_to_fault_succ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {σ : State Γ} {α : Act} {p : ENNReal} (h : c ⤳[α,p] (Sum.inr Termination.fault, σ)) (α' : Act) (p' : ENNReal) (c' : Conf₁ Γ) : (c ⤳[α',p'] c') ↔ α' = α ∧ p' = p ∧ c' = (Sum.inr Termination.fault, σ)

@[simp]

theorem pGCL.SmallStep.assign_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {x : 𝒱} {e : State Γ → Γ x} {α : Act} {p : ENNReal} : ((pgcl {@x := @e}, σ) ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = (Sum.inr Termination.term, σ[x ↦ e σ])

@[simp]

theorem pGCL.SmallStep.prob_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {C₁ : pGCL Γ} {p : ProbExp Γ} {C₂ : pGCL Γ} {α : Act} {p' : ENNReal} : ((pgcl {{ @C₁ } [@p] { @C₂ }}, σ) ⤳[α,p'] c') ↔ α = Act.N ∧ if C₁ = C₂ then p' = 1 ∧ c' = (Sum.inl C₁, σ) else p' = p σ ∧ 0 < p' ∧ c' = (Sum.inl C₁, σ) ∨ p' = 1 - p σ ∧ 0 < p' ∧ c' = (Sum.inl C₂, σ)

@[simp]

theorem pGCL.SmallStep.nonDet_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {C₁ C₂ : pGCL Γ} {α : Act} {p' : ENNReal} : ((pgcl {{ @C₁ } [] { @C₂ }}, σ) ⤳[α,p'] c') ↔ p' = 1 ∧ (α = Act.L ∧ c' = (Sum.inl C₁, σ) ∨ α = Act.R ∧ c' = (Sum.inl C₂, σ))

@[simp]

theorem pGCL.SmallStep.tick_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {r : State Γ → ENNReal} {α : Act} {p : ENNReal} : ((pgcl {tick(@r)}, σ) ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = (Sum.inr Termination.term, σ)

@[simp]

theorem pGCL.SmallStep.observe_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {b : State Γ → Prop} {α : Act} {p : ENNReal} : ((pgcl {observe(@b)}, σ) ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = if b σ then (Sum.inr Termination.term, σ) else (Sum.inr Termination.fault, σ)

@[simp]

theorem pGCL.SmallStep.seq_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {α : Act} {p : ENNReal} {C₁ C₂ : pGCL Γ} : ((pgcl {@C₁ ; @C₂}, σ) ⤳[α,p] c') ↔ (∃ (C' : pGCL Γ) (σ' : State Γ), ((C₁, σ) ⤳[α,p] (Sum.inl C', σ')) ∧ c' = (Sum.inl (pgcl {@C' ; @C₂}), σ')) ∨ (∃ (σ' : State Γ), ((C₁, σ) ⤳[α,p] (Sum.inr Termination.term, σ')) ∧ c' = (Sum.inl C₂, σ')) ∨ ((C₁, σ) ⤳[α,p] (Sum.inr Termination.fault, σ)) ∧ c' = (Sum.inr Termination.fault, σ) ∧ α = Act.N ∧ p = 1

@[simp]

theorem pGCL.SmallStep.loop_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c' : Conf₁ Γ} {σ : State Γ} {b : State Γ → Prop} {C : pGCL Γ} {α : Act} {p : ENNReal} : ((pgcl {while @b { @C }}, σ) ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = if b σ then (Sum.inl (pgcl {@C ; while @b { @C }}), σ) else (Sum.inr Termination.term, σ)

def pGCL.SmallStep.act {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (c : Conf₀ Γ) : Set Act

Equations

• pGCL.SmallStep.act c = {α : pGCL.Act | ∃ (p : ENNReal) (c' : pGCL.Conf₁ Γ), c ⤳[α,p] c'}

@[implicit_reducible]

noncomputable instance pGCL.SmallStep.instDecidableMemActSetAct {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {α : Act} : Decidable (α ∈ act c)

Equations

• pGCL.SmallStep.instDecidableMemActSetAct = Classical.propDecidable (α ∈ pGCL.SmallStep.act c)

instance pGCL.SmallStep.instFiniteElemActAct {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} : Finite ↑(act c)

@[implicit_reducible]

noncomputable instance pGCL.SmallStep.instFintypeElemActAct {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} : Fintype ↑(act c)

Equations

• pGCL.SmallStep.instFintypeElemActAct = Fintype.ofFinite ↑(pGCL.SmallStep.act c)

@[simp]

theorem pGCL.SmallStep.act_skip {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} : act (pgcl {skip}, σ) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_assign {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {x : 𝒱} {e : State Γ → Γ x} : act (pgcl {@x := @e}, σ) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_seq {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {C₁ C₂ : pGCL Γ} : act (pgcl {@C₁ ; @C₂}, σ) = act (C₁, σ)

@[simp]

theorem pGCL.SmallStep.act_prob {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {C₁ : pGCL Γ} {p : ProbExp Γ} {C₂ : pGCL Γ} : act (pgcl {{ @C₁ } [@p] { @C₂ }}, σ) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_nonDet {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {C₁ C₂ : pGCL Γ} : act (pgcl {{ @C₁ } [] { @C₂ }}, σ) = {Act.L, Act.R}

@[simp]

theorem pGCL.SmallStep.act_loop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {b : State Γ → Prop} {C : pGCL Γ} : act (pgcl {while @b { @C }}, σ) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_tick {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {r : State Γ → ENNReal} : act (pgcl {tick(@r)}, σ) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_observe {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {r : State Γ → Prop} : act (pgcl {observe(@r)}, σ) = {Act.N}

instance pGCL.SmallStep.act_nonempty {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (s : Conf₀ Γ) : Nonempty ↑(act s)

theorem pGCL.SmallStep.progress {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (s : Conf₀ Γ) : ∃ (p : ENNReal) (a : Act) (x : Conf₁ Γ), s ⤳[a,p] x

@[simp]

theorem pGCL.SmallStep.iInf_act_const {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {C : Conf₀ Γ} {x : ENNReal} : ⨅ α ∈ act C, x = x

@[implicit_reducible]

noncomputable instance pGCL.SmallStep.instDecidable {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {c' : Conf₁ Γ} {α : Act} {p : ENNReal} : Decidable (c ⤳[α,p] c')

Equations

• pGCL.SmallStep.instDecidable = Classical.propDecidable (c ⤳[α,p] c')

@[implicit_reducible]

noncomputable instance pGCL.SmallStep.instDecidableExistsActENNReal {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {c' : Conf₁ Γ} : Decidable (∃ (α : Act) (p : ENNReal), c ⤳[α,p] c')

Equations

• pGCL.SmallStep.instDecidableExistsActENNReal = Classical.propDecidable (∃ (α : pGCL.Act) (p : ENNReal), c ⤳[α,p] c')

@[simp]

theorem pGCL.SmallStep.tsum_p {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {c' : Conf₁ Γ} {α : Act} : ∑' (p : { p : ENNReal // c ⤳[α,p] c' }), ↑p = ∑' (p : ENNReal), if c ⤳[α,p] c' then p else 0

def pGCL.SmallStep.succs {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (c : Conf₀ Γ) (α : Act) : Set (Conf₁ Γ)

Equations

• pGCL.SmallStep.succs c α = {c' : pGCL.Conf₁ Γ | ∃ (p : ENNReal), c ⤳[α,p] c'}

@[irreducible]

noncomputable def pGCL.SmallStep.succs_fin {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (c : Conf₀ Γ) (α : Act) : Finset (Conf₁ Γ)

Equations

• pGCL.SmallStep.succs_fin (pgcl {skip}, σ) pGCL.Act.N = {(Sum.inr pGCL.Termination.term, σ)}
• pGCL.SmallStep.succs_fin (pgcl {tick(@a)}, σ) pGCL.Act.N = {(Sum.inl (pgcl {skip}), σ)}
• pGCL.SmallStep.succs_fin (pgcl {observe(@b)}, σ) pGCL.Act.N = if b σ then {(Sum.inl (pgcl {skip}), σ)} else {(Sum.inr pGCL.Termination.fault, σ)}
• pGCL.SmallStep.succs_fin (pgcl {@x := @E}, σ) pGCL.Act.N = {(Sum.inl (pgcl {skip}), σ[x ↦ E σ])}
• pGCL.SmallStep.succs_fin (pgcl {{ @C₁ } [@p] { @C₂ }}, σ) pGCL.Act.N = if p σ = 0 then {(Sum.inl C₂, σ)} else if p σ = 1 then {(Sum.inl C₁, σ)} else {(Sum.inl C₁, σ), (Sum.inl C₂, σ)}
• pGCL.SmallStep.succs_fin (pgcl {{ @C₁ } [] { @a }}, σ) pGCL.Act.L = {(Sum.inl C₁, σ)}
• pGCL.SmallStep.succs_fin (pgcl {{ @a } [] { @C₂ }}, σ) pGCL.Act.R = {(Sum.inl C₂, σ)}
• pGCL.SmallStep.succs_fin (pgcl {while @b { @C }}, σ) pGCL.Act.N = if b σ then {(Sum.inl (pgcl {@C ; while @b { @C }}), σ)} else {(Sum.inl (pgcl {skip}), σ)}
• pGCL.SmallStep.succs_fin (pgcl {skip ; @C₂}, σ) pGCL.Act.N = {(Sum.inl C₂, σ)}
• pGCL.SmallStep.succs_fin (pgcl {@C₁ ; @C₂}, σ) α = Finset.map { toFun := C₂.after, inj' := ⋯ } (pGCL.SmallStep.succs_fin (C₁, σ) α)
• pGCL.SmallStep.succs_fin c α = ∅

@[irreducible]

noncomputable def pGCL.SmallStep.succs_univ_fin {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (c : Conf₀ Γ) : Finset (Act × Conf₁ Γ)

Equations

• One or more equations did not get rendered due to their size.
• pGCL.SmallStep.succs_univ_fin (pgcl {skip}, σ) = {(pGCL.Act.N, Sum.inr pGCL.Termination.term, σ)}
• pGCL.SmallStep.succs_univ_fin (pgcl {tick(@a)}, σ) = {(pGCL.Act.N, Sum.inl (pgcl {skip}), σ)}
• pGCL.SmallStep.succs_univ_fin (pgcl {observe(@b)}, σ) = if b σ then {(pGCL.Act.N, Sum.inl (pgcl {skip}), σ)} else {(pGCL.Act.N, Sum.inr pGCL.Termination.fault, σ)}
• pGCL.SmallStep.succs_univ_fin (pgcl {@x := @E}, σ) = {(pGCL.Act.N, Sum.inl (pgcl {skip}), σ[x ↦ E σ])}
• pGCL.SmallStep.succs_univ_fin (pgcl {{ @C₁ } [] { @C₂ }}, σ) = {(pGCL.Act.L, Sum.inl C₁, σ), (pGCL.Act.R, Sum.inl C₂, σ)}
• pGCL.SmallStep.succs_univ_fin (pgcl {while @b { @C }}, σ) = if b σ then {(pGCL.Act.N, Sum.inl (pgcl {@C ; while @b { @C }}), σ)} else {(pGCL.Act.N, Sum.inl (pgcl {skip}), σ)}
• pGCL.SmallStep.succs_univ_fin (pgcl {skip ; @C₂}, σ) = {(pGCL.Act.N, Sum.inl C₂, σ)}
• pGCL.SmallStep.succs_univ_fin (pgcl {@C₁ ; @C₂}, σ) = Finset.map { toFun := Prod.map id C₂.after, inj' := ⋯ } (pGCL.SmallStep.succs_univ_fin (C₁, σ))

@[irreducible]

noncomputable def pGCL.SmallStep.succs_univ_fin' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (c : Conf₀ Γ) : Finset (Act × ENNReal × Conf₁ Γ)

Equations

• One or more equations did not get rendered due to their size.
• pGCL.SmallStep.succs_univ_fin' (pgcl {skip}, σ) = {(pGCL.Act.N, 1, Sum.inr pGCL.Termination.term, σ)}
• pGCL.SmallStep.succs_univ_fin' (pgcl {tick(@a)}, σ) = {(pGCL.Act.N, 1, Sum.inr pGCL.Termination.term, σ)}
• pGCL.SmallStep.succs_univ_fin' (pgcl {observe(@b)}, σ) = if b σ then {(pGCL.Act.N, 1, Sum.inr pGCL.Termination.term, σ)} else {(pGCL.Act.N, 1, Sum.inr pGCL.Termination.fault, σ)}
• pGCL.SmallStep.succs_univ_fin' (pgcl {@x := @E}, σ) = {(pGCL.Act.N, 1, Sum.inr pGCL.Termination.term, σ[x ↦ E σ])}
• pGCL.SmallStep.succs_univ_fin' (pgcl {{ @C₁ } [] { @C₂ }}, σ) = {(pGCL.Act.L, 1, Sum.inl C₁, σ), (pGCL.Act.R, 1, Sum.inl C₂, σ)}
• pGCL.SmallStep.succs_univ_fin' (pgcl {while @b { @C }}, σ) = if b σ then {(pGCL.Act.N, 1, Sum.inl (pgcl {@C ; while @b { @C }}), σ)} else {(pGCL.Act.N, 1, Sum.inr pGCL.Termination.term, σ)}
• pGCL.SmallStep.succs_univ_fin' (pgcl {@C₁ ; @C₂}, σ) = Finset.map { toFun := Prod.map id (Prod.map id C₂.after), inj' := ⋯ } (pGCL.SmallStep.succs_univ_fin' (C₁, σ))

theorem pGCL.SmallStep.succs_univ_fin'_eq_r {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (c : Conf₀ Γ) (α : Act) (p : ENNReal) (c' : Conf₁ Γ) : (α, p, c') ∈ succs_univ_fin' c ↔ c ⤳[α,p] c'

theorem pGCL.SmallStep.sums_to_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {c : Conf₀ Γ} {α : Act} {p₀ : ENNReal} {c₀ : Conf₁ Γ} (h₀ : c ⤳[α,p₀] c₀) : ∑' (c' : Conf₁ Γ) (p : { p : ENNReal // c ⤳[α,p] c' }), ↑p = 1