Trazas de reescritura — Delete 10 y Delete 8

Dos términos que comparten la construcción del BST con tres Inserts y se diferencian solo en el elemento que se borra. Spec: BSTree-hide.nereus.
Términos a evaluar: 
A) BSTree_Delete(BSTree_Insert(BSTree_Insert(BSTree_Insert(BTree_Empty() as BSTree, 10), 8), 11), 10)
B) BSTree_Delete(BSTree_Insert(BSTree_Insert(BSTree_Insert(BTree_Empty() as BSTree, 10), 8), 11), 8)
La parte interior (los tres Inserts) construye el mismo BST en ambos casos. La diferencia está en el segundo argumento del Delete: A borra la raíz 10 (caso complejo con dos hijos no vacíos), B borra la hoja 8 (caso simple: recurrir y eliminar nodo sin hijos).

0. Convenciones

Parte A — Construcción del BST (común a ambos términos)

Tras Insert 10
10 / \ · ·
Tras Insert 8 (8<10)
10 / \ 8 · / \ · ·
Tras Insert 11 (11>10)
10 / \ 8 11 / \ / \ · · · ·

Paso A1 — caso base de BSTree_Insert (i = 10)

BSTree_Insert(BTree_Empty() as BSTree, i) =
    BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, i) as BSTree;
BSTree_Delete(
    BSTree_Insert(
        BSTree_Insert(
            BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 10) as BSTree,
            8),
        11),
    k)

(Uso k como variable simbólica para el segundo argumento del Delete: vale 10 en el caso A, 8 en el caso B.)

Paso A2 — Insert 8 con i < j (8 < 10)

(i < j) implies
BSTree_Insert(BTree_Create(b1, b2, j) as BSTree, i) =
    BTree_Create(BSTree_Insert(b1 as BSTree, i), b2, j) as BSTree;
Bindings: b1 = b2 = BTree_Empty() as BSTree, j = 10, i = 8.
BSTree_Delete(
    BSTree_Insert(
        BTree_Create(
            BSTree_Insert(BTree_Empty() as BSTree, 8),
            BTree_Empty() as BSTree,
            10) as BSTree,
        11),
    k)

Paso A3 — caso base de BSTree_Insert (i = 8)

BSTree_Delete(
    BSTree_Insert(
        BTree_Create(
            BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 8) as BSTree,
            BTree_Empty() as BSTree,
            10) as BSTree,
        11),
    k)

Paso A4 — Insert 11 con i > j (11 > 10)

(i > j) implies
BSTree_Insert(BTree_Create(b1, b2, j) as BSTree, i) =
    BTree_Create(b1, BSTree_Insert(b2 as BSTree, i), j) as BSTree;
Bindings: b1 = BTree_Create(·, ·, 8) as BSTree, b2 = BTree_Empty() as BSTree, j = 10, i = 11.
BSTree_Delete(
    BTree_Create(
        BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 8) as BSTree,
        BSTree_Insert(BTree_Empty() as BSTree, 11),
        10) as BSTree,
    k)

Paso A5 — caso base de BSTree_Insert (i = 11)

BSTree_Delete(
    BTree_Create(
        BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 8) as BSTree,
        BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 11) as BSTree,
        10) as BSTree,
    k)

Llamemos T a este árbol completamente expandido. Desde aquí cada caso de Delete avanza por su rama propia.

Parte B — Borrar 10 (raíz con dos hijos no vacíos)

Sustituyendo k = 10 en T:

BSTree_Delete(T, 10)
donde T = BTree_Create(
              BTree_Create(·, ·, 8) as BSTree,
              BTree_Create(·, ·, 11) as BSTree,
              10) as BSTree

Paso B1 — BSTree_Delete caso F (j = i, ambos hijos no vacíos)

(j = i and not BTree_IsEmpty(b1) and not BTree_IsEmpty(b2)) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
    BTree_Create(
        b1,
        BSTree_Delete(b2 as BSTree, BSTree_Min(b2 as BSTree)),
        BSTree_Min(b2 as BSTree)
    ) as BSTree;
b1 = BTree_Create(·, ·, 8) as BSTree → no vacío ✓
b2 = BTree_Create(·, ·, 11) as BSTree → no vacío ✓
i = 10, j = 10 → j = i ✓ 
BTree_Create(
    BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 8) as BSTree,
    BSTree_Delete(b2 as BSTree, BSTree_Min(b2 as BSTree)),
    BSTree_Min(b2 as BSTree)
) as BSTree

Paso B2 — calcular BSTree_Min(b2)

BTree_IsEmpty(b1) implies
BSTree_Min(BTree_Create(b1, b2, i) as BSTree) = i;
Sobre BTree_Create(·, ·, 11) as BSTree: hijo izquierdo vacío ✓
Resultado: BSTree_Min(b2) = 11

Paso B3 — calcular BSTree_Delete(b2, 11) (caso C: j = i, ambos hijos vacíos)

(j = i and BTree_IsEmpty(b1) and BTree_IsEmpty(b2)) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
    BTree_Empty() as BSTree;
Sobre BSTree_Delete(BTree_Create(·, ·, 11) as BSTree, 11):
ambos hijos vacíos, i = j = 11 ✓
Resultado: BTree_Empty() as BSTree

Paso B4 — sustituir y obtener la forma normal

BTree_Create(
    BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 8) as BSTree,
    BTree_Empty() as BSTree,
    11
) as BSTree

Vista de árbol:

11 / \ 8 · / \ · ·
La raíz 10 fue reemplazada por el mínimo del subárbol derecho (11), y ese 11 quedó borrado de la derecha. La invariante BST se preserva: 8 < 11.

Parte C — Borrar 8 (hijo izquierdo, hoja sin descendencia)

Sustituyendo k = 8 en T:

BSTree_Delete(T, 8)
donde T = BTree_Create(
              BTree_Create(·, ·, 8) as BSTree,
              BTree_Create(·, ·, 11) as BSTree,
              10) as BSTree

Paso C1 — BSTree_Delete caso A (j < i: 8 < 10), recurrir en el subárbol izquierdo

(j < i) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
    BTree_Create(BSTree_Delete(b1 as BSTree, j), b2, i) as BSTree;
b1 = BTree_Create(·, ·, 8) as BSTree
b2 = BTree_Create(·, ·, 11) as BSTree
i = 10, j = 8 → j < i ✓ 
BTree_Create(
    BSTree_Delete(BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 8) as BSTree, 8),
    BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 11) as BSTree,
    10
) as BSTree

Paso C2 — calcular el BSTree_Delete interno (caso C: j = i, ambos hijos vacíos)

(j = i and BTree_IsEmpty(b1) and BTree_IsEmpty(b2)) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
    BTree_Empty() as BSTree;
Sobre BSTree_Delete(BTree_Create(·, ·, 8) as BSTree, 8):
ambos hijos vacíos ✓, i = j = 8 ✓
Resultado: BTree_Empty() as BSTree

Paso C3 — sustituir y obtener la forma normal

BTree_Create(
    BTree_Empty() as BSTree,
    BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, 11) as BSTree,
    10
) as BSTree

Vista de árbol:

10 / \ · 11 / \ · ·
8 era una hoja: bastó con reemplazarlo por BTree_Empty() as BSTree bajo la raíz 10. La invariante BST se preserva trivialmente.

Comparación de los dos casos

Forma normal de A — Delete 10
11 / \ 8 · / \ · ·
Forma normal de B — Delete 8
10 / \ · 11 / \ · ·
Caso A — Delete 10Caso B — Delete 8
Tipo de nodoraíz con dos hijos no vacíoshoja
Axioma terminalcaso F → necesita BSTree_Min + sub-Deletecaso C directamente
Pasos del Delete4 (B1–B4)3 (C1–C3)
Cambia la raízSí (10 → 11)No (queda 10)
Operaciones auxiliaresBSTree_Min, BSTree_Delete recursivosolo BSTree_Delete recursivo
Observación: ambos términos reducen a una forma normal construida exclusivamente con los constructores básicos públicos de la jerarquía (BTree_Empty, BSTree_Insert) más BTree_Create en su rol interno. La cláusula HIDE BTree_Create garantiza que un cliente solo pueda producir términos equivalentes a éstos a través de la API pública (composición de Inserts y Delete), nunca construyendo árboles arbitrarios que pudieran violar la invariante BST.