structure Semantics.Dynamic.BUS.BilateralDRS (S : Type u_1) : Type u_1

Bilateral DRS: positive and negative DRS meanings. This is Dynamic Ty2 lifted to bilateral form.

• positive : Core.DynProp.DRS S
• negative : Core.DynProp.DRS S

def Semantics.Dynamic.BUS.BilateralDRS.btest {S : Type u_1} (C : Core.DynProp.Condition S) : BilateralDRS S

Bilateral test

Equations

• Semantics.Dynamic.BUS.BilateralDRS.btest C = { positive := [C], negative := [fun (i : S) => ¬C i] }

def Semantics.Dynamic.BUS.BilateralDRS.bneg {S : Type u_1} (D : BilateralDRS S) : BilateralDRS S

Bilateral negation: swap

Equations

• ∼ᵇD = { positive := D.negative, negative := D.positive }

def Semantics.Dynamic.BUS.BilateralDRS.«term∼ᵇ_» : Lean.ParserDescr

Equations

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

@[simp]

theorem Semantics.Dynamic.BUS.BilateralDRS.bneg_bneg {S : Type u_1} (D : BilateralDRS S) : ∼ᵇ∼ᵇD = D

DNE is definitional

def Semantics.Dynamic.BUS.BilateralDRS.bseq {S : Type u_1} (D₁ D₂ : BilateralDRS S) : BilateralDRS S

Bilateral sequencing

Equations

• D₁ ⨟ᵇ D₂ = { positive := D₁.positive ⨟ D₂.positive, negative := fun (i j : S) => D₁.negative i j ∨ ∃ (k : S), D₁.positive i k ∧ D₂.negative k j }

def Semantics.Dynamic.BUS.BilateralDRS.«term_⨟ᵇ_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.BUS.BilateralDRS.bdisj {S : Type u_1} (D₁ D₂ : BilateralDRS S) : BilateralDRS S

Bilateral disjunction

Equations

• D₁.bdisj D₂ = { positive := fun (i j : S) => D₁.positive i j ∨ D₂.positive i j, negative := fun (i j : S) => D₁.negative i j ∧ D₂.negative i j }

def Semantics.Dynamic.BUS.BilateralDRS.ofDRS {S : Type u_1} (D : Core.DynProp.DRS S) : BilateralDRS S

Lift unilateral DRS to bilateral with complement negation. This is how standard dynamic systems embed into BUS.

Equations

• Semantics.Dynamic.BUS.BilateralDRS.ofDRS D = { positive := D, negative := fun (i j : S) => i = j ∧ ¬∃ (k : S), D i k }

theorem Semantics.Dynamic.BUS.BilateralDRS.ofDRS_positive {S : Type u_1} (D : Core.DynProp.DRS S) : (ofDRS D).positive = D

The positive dimension preserves the original DRS

theorem Semantics.Dynamic.BUS.BilateralDRS.ofDRS_negative {S : Type u_1} (D : Core.DynProp.DRS S) : (ofDRS D).negative = [∼D]

The negative dimension is the test-based negation

BilateralDen (from Core.Bilateral) uses InfoStates: BilateralDen W E = { positive, negative : InfoState W E → InfoState W E }

BilateralDRS uses DRS directly: BilateralDRS S = { positive, negative : S → S → Prop }

For worldless systems (W = Unit), we can relate them via: InfoState Unit E ≅ Set (Nat → E) CCP Unit E = InfoState Unit E → InfoState Unit E

The relation: a DRS D : S → S → Prop induces a CCP: λ s => { j | ∃ i ∈ s, D i j }

def Semantics.Dynamic.BUS.BilateralDRS.drsToUpdate {S : Type u_2} (D : Core.DynProp.DRS S) : Set S → Set S

Convert DRS to CCP (set-based update)

Equations

• Semantics.Dynamic.BUS.BilateralDRS.drsToUpdate D s = {j : S | ∃ (i : S), i ∈ s ∧ D i j}

def Semantics.Dynamic.BUS.BilateralDRS.toUpdatePair {S : Type u_1} (D : BilateralDRS S) : (Set S → Set S) × (Set S → Set S)

BilateralDRS induces pair of CCPs

Equations

• D.toUpdatePair = (Semantics.Dynamic.BUS.BilateralDRS.drsToUpdate D.positive, Semantics.Dynamic.BUS.BilateralDRS.drsToUpdate D.negative)

theorem Semantics.Dynamic.BUS.bus_dne {S : Type u_1} (D : BilateralDRS S) : (∼ᵇ∼ᵇD).positive = D.positive

BUS negation preserves DNE at the DRS level. This is the formal content of "bathroom sentences work in BUS".

theorem Semantics.Dynamic.BUS.bseq_positive_assoc {S : Type u_1} (D₁ D₂ D₃ : BilateralDRS S) : (D₁ ⨟ᵇ D₂ ⨟ᵇ D₃).positive = (D₁ ⨟ᵇ (D₂ ⨟ᵇ D₃)).positive

Sequencing positive dimensions is associative.