#define NULL 0
typedef struct linked_list_tree_struct tree_t;
struct linked_list_tree_struct {
    tree_t* next_sibling;
};
/*@ inductive are_siblings{L} (tree_t *a, tree_t *b) {
    }
*/
/*@ inductive reachable{L} (tree_t *root, tree_t *node) {
    }
*/
/*@ predicate well_formed(tree_t *root) =
      (root->next_sibling == NULL || well_formed(root->next_sibling));
*/
int main(int argc, char *argv[argc]) {
    tree_t grandchild1 = {     };
    /*@ assert well_formed(&grandchild1); */
}