Function is_countdown_morphism 

pub fn is_countdown_morphism(system: &TransitionSystem, measure: &[u64]) -> bool

Is measure a coalgebra morphism to the countdown coalgebra? Every transition s → t must strictly decrease it (measure[t] < measure[s]) — the morphism square commuting with n ↦ n-1. Because the countdown is well-founded, a true here witnesses that the system is well-founded.