theorem Semantics.Dynamic.CDRT.register_eq {E : Type u_1} : Register E = (ℕ → E)

CDRT Register = Dynamic Ty2 Assignment

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

CDRT dref: register lookup

Equations

• Semantics.Dynamic.CDRT.dref n r = r n

def Semantics.Dynamic.CDRT.toDRS {E : Type u_1} (φ : DProp E) : Core.DynProp.DRS (Register E)

CDRT DProp IS a DRS

Equations

• Semantics.Dynamic.CDRT.toDRS φ = φ

def Semantics.Dynamic.CDRT.ofDRS {E : Type u_1} (D : Core.DynProp.DRS (Register E)) : DProp E

DRS IS CDRT DProp

Equations

• Semantics.Dynamic.CDRT.ofDRS D = D

@[simp]

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

@[simp]

theorem Semantics.Dynamic.CDRT.ofDRS_toDRS {E : Type u_1} (D : Core.DynProp.DRS (Register E)) : toDRS (ofDRS D) = D

theorem Semantics.Dynamic.CDRT.ofStatic_eq_test {E : Type u_1} (p : SProp E) : toDRS (DProp.ofStatic p) = [p]

theorem Semantics.Dynamic.CDRT.seq_eq_dseq {E : Type u_1} (φ ψ : DProp E) : toDRS (φ ;; ψ) = toDRS φ ⨟ toDRS ψ

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

theorem Semantics.Dynamic.CDRT.impl_eq_test_dimpl {E : Type u_1} (φ ψ : DProp E) : toDRS (φ.impl ψ) = [Core.DynProp.dimpl (toDRS φ) (toDRS ψ)]

theorem Semantics.Dynamic.CDRT.trueAt_eq_closure {E : Type u_1} (φ : DProp E) (i : Register E) : φ.true_at i ↔ Core.DynProp.closure (toDRS φ) i

theorem Semantics.Dynamic.CDRT.ddisj_eq_test_ddisj {E : Type u_1} (φ ψ : DProp E) : toDRS (φ.ddisj ψ) = [Core.DynProp.ddisj (toDRS φ) (toDRS ψ)]