Hola,
Estábamos trabajando es esta parte y no entendemos exactamente cuantos addAVLi hay que hacer. Hay que hacer uno por cada rotación? Cada vez que insertamos y rebalanceamos en este tipo de arboles la altura del árbol resultante sería siempre n o n+1 dependiendo del caso, bastaría con hacer dos?
Muchas gracias, saludos.
Hola.
Las rotaciones no son relevantes aquí, ya que nos enfocamos solo en la propiedad estructural de los AVL, que establece que para cada nodo las alturas de sus subárboles izquierdo y derecho pueden diferir en a lo sumo una unidad.
Para árboles AVL no vacíos se podrían definir tres operadores, tendiendo en cuenta que las alturas de los subárboles de un nodo pueden ser iguales o diferir en una unidad. Por ejemplo, uno de estos operadores puede ser:
Parameter addAVL1 : forall n:nat, nat -> AVLNat n -> AVLNat (n+1) -> AVLNat (n+2).
Saludos, Carlos
