Skip to main content

canonical_countdown_morphism

logicaffeine_proof::coalgebra

Function canonical_countdown_morphism 

Source 
pub fn canonical_countdown_morphism(
    system: &TransitionSystem,
) -> Option<Vec<u64>>
Expand description

The canonical countdown morphism of a well-founded system: the longest forward path from each state (sinks = 0). This is the terminal such morphism — the existence half of the theorem made constructive. Returns None if the system is not well-founded (no morphism exists).