// Description: A module with a long chain of type synonyms. Type t0 refers to type t1, which refers to type t2, etc., until type t9 is an uninterpreted type.

module main {
    type t0 = t1;
    type t1 = t2;
    type t2 = t3;
    type t3 = t4;
    type t4 = t5;
    type t5 = t6;
    type t6 = t7;
    type t7 = t8;
    type t8 = t9;
    type t9;

    var x : t9;
    var y : t0;

    init {
        x = y;
    }

    invariant x_eq_y: x == y;

    control {
        induction;
        check;
        print_results;
    }
}
