Function temporal_symmetry_pairs 

pub fn temporal_symmetry_pairs(
    init: &ProofExpr,
    trans0: &ProofExpr,
    property0: &ProofExpr,
) -> Vec<(String, String)>

The temporal symmetries of a transition system: pairs of base signals interchangeable across all time — a swap that preserves the initial constraint, the transition relation (checked on the generic frame trans(0), hence on every frame by uniformity), and the property. Each surviving pair is a genuine system automorphism when lifted uniformly through the unrolling.