def
definition
eventCost_decidable
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts on GitHub at line 114.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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) :
138 actionCost a b = 0 ↔ a = b := by
139 unfold actionCost
140 by_cases h : a = b
141 · simp [h]
142 · simp [h]
143
144def actionCost_decidable (a b : ActionState) : Decidable (a = b) :=