theorem
proved
selfBootstrapCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.SelfBootstrapDistinguishability on GitHub at line 81.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
78 claim_not_its_negation : ∀ K : Type*, (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y)
79
80/-- The self-bootstrap certificate is theorem-backed. -/
81theorem selfBootstrapCert : SelfBootstrapCert where
82 meta_distinguishes := meta_language_distinguishes_props
83 claim_not_its_negation := dist_claim_self_distinguishes
84
85end SelfBootstrap
86end Foundation
87end IndisputableMonolith
papers checked against this theorem (showing 1 of 1)
-
Multi-robot service prototype runs on Aggregate Programming
"the self-stabilizing nature and resilience to changes of AP operators, has made it possible to deal naturally with several dynamic/failure scenarios"