 104
 105open Narrative
 106
 107theorem eventCost_zero_iff (a b : EventState) :
 108    eventCost a b = 0 ↔ a = b := by
 109  unfold eventCost
 110  by_cases h : a = b
 111  · simp [h]
 112  · simp [h]
 113
 114def eventCost_decidable (a b : EventState) : Decidable (a = b) :=
 115  inferInstance
 116
 117theorem eventCompose_assoc (a b c : EventState) :
 118    eventCompose (eventCompose a b) c = eventCompose a (eventCompose b c) := by
 119  unfold eventCompose
 120  congr 1
 121  · exact Nat.add_assoc _ _ _
 122  · exact Nat.add_assoc _ _ _
 123
 124theorem eventCompose_left_id (a : EventState) :
 125    eventCompose narrativeZero a = a := by
 126  unfold eventCompose narrativeZero
 127  cases a; simp
 128
 129end NarrativeRich
 130
 131/-! ## Ethics -/
 132
 133namespace EthicsRich
 134
 135open Ethics
 136
 137theorem actionCost_zero_iff (a b : ActionState) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.