for a, b being Ordinal
for g being Ordinal-Sequence-valued Sequence st a in dom g & b in dom (criticals g) holds
(criticals g) . b is_a_fixpoint_of g . a