pith. machine review for the scientific record. sign in
def definition def or abbrev

fullSafety

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 112def fullSafety : SafetyRequirements where
 113  has_watchdog := true

proof body

Definition body.

 114  has_overcurrent_protection := true
 115  has_overvoltage_protection := true
 116  has_thermal_protection := true
 117  has_loss_of_load_detection := true
 118  has_deterministic_shutdown := true
 119  all_satisfied := ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
 120
 121end IndisputableMonolith.Superhuman.TechnologicalAccess

depends on (1)

Lean names referenced from this declaration's body.