`hasCycle`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethics.StakeGraph
domain: Ethics
line: 35 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethics.StakeGraph on GitHub at line 35.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  32def mutualReachable (G : StakeGraph) (nodes : List Stakeholder) (s t : Stakeholder) : Bool :=
  33  reachable G nodes s t && reachable G nodes t s
  34
  35def hasCycle (G : StakeGraph) (nodes : List Stakeholder) : Bool :=
  36  nodes.any (fun s => G.edge s s)
  37  || nodes.any (fun s =>
  38        nodes.any (fun t => (¬ decide (s = t)) && mutualReachable G nodes s t))
  39
  40end StakeGraph
  41end Ethics
  42end IndisputableMonolith
  43

papers checked against this theorem

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