test-adt-19.ucl

module main {
    datatype tree = join(left: tree, right: tree) | leaf(node: integer);

    var t1: tree;
    var t2: tree; 

    invariant test : is_join(join(t1, t2));

    control {
        induction;
        check;
        print_results;
    }
}