def Semantics.Dynamic.DPL.dref {E : Type u_1} (n : ℕ) : Core.DynamicTy2.Dref (Core.Assignment E) E

DPL dref: projection function for variable n

Equations

• Semantics.Dynamic.DPL.dref n g = g n

@[reducible, inline]

abbrev Semantics.Dynamic.DPL.extend {E : Type u_1} (g : Core.Assignment E) (n : ℕ) (e : E) : Core.Assignment E

DPL extend is Assignment.update.

Equations

• Semantics.Dynamic.DPL.extend g n e = g.update n e

theorem Semantics.Dynamic.DPL.extend_at {E : Type u_1} (g : Core.Assignment E) (n : ℕ) (e : E) : dref n (extend g n e) = e

theorem Semantics.Dynamic.DPL.extend_other {E : Type u_1} (g : Core.Assignment E) (n m : ℕ) (e : E) (h : n ≠ m) : dref m (extend g n e) = dref m g

def Semantics.Dynamic.DPL.toDRS {E : Type u_1} (φ : DPLRel E) : Core.DynamicTy2.DRS (Core.Assignment E)

DPL relation IS a DRS

Equations

• Semantics.Dynamic.DPL.toDRS φ = φ

def Semantics.Dynamic.DPL.ofDRS {E : Type u_1} (D : Core.DynamicTy2.DRS (Core.Assignment E)) : DPLRel E

DRS IS a DPL relation

Equations

• Semantics.Dynamic.DPL.ofDRS D = D

@[simp]

theorem Semantics.Dynamic.DPL.toDRS_ofDRS {E : Type u_1} (φ : DPLRel E) : ofDRS (toDRS φ) = φ

@[simp]

theorem Semantics.Dynamic.DPL.ofDRS_toDRS {E : Type u_1} (D : Core.DynamicTy2.DRS (Core.Assignment E)) : toDRS (ofDRS D) = D

theorem Semantics.Dynamic.DPL.atom_eq_test {E : Type u_1} (p : Core.Assignment E → Prop) : toDRS (DPLRel.atom p) = [fun (g : Core.Assignment E) => p g]

theorem Semantics.Dynamic.DPL.conj_eq_dseq {E : Type u_1} (φ ψ : DPLRel E) : toDRS (φ.conj ψ) = toDRS φ ⨟ toDRS ψ

theorem Semantics.Dynamic.DPL.neg_eq_test_dneg {E : Type u_1} (φ : DPLRel E) : toDRS φ.neg = [∼toDRS φ]

theorem Semantics.Dynamic.DPL.exists_eq {E : Type u_1} (x : ℕ) (φ : DPLRel E) : toDRS (DPLRel.exists_ x φ) = fun (g h : Core.Assignment E) => ∃ (d : E), toDRS φ (extend g x d) h