Traza — Heap_H clásico

Construcción con 6 Inserts (15, 12, 3, 7, 9, 11) seguida de DeleteMin. Ejercita las tres reglas de Insert con anidamiento profundo y un DeleteMin con SiftDown de dos niveles.
Término a evaluar: 
Heap_DeleteMin(
    Heap_Insert(
        Heap_Insert(
            Heap_Insert(
                Heap_Insert(
                    Heap_Insert(
                        Heap_Insert(Heap_Empty() as Heap_H, 15),
                        12),
                    3),
                7),
            9),
        11))
Spec: Heap_H_complete.nereus. Convención: · = Heap_Empty() as Heap_H.

Fase 1 — Construcción del heap (6 Inserts)

A1 — Insert 15 (caso base)

Sobre Heap_Empty → singleton.
BTree_Create(·, ·, 15) as Heap_H
tras Insert 15 — size 1
15

A2 — Insert 12 (Regla A: |L|=|R|=0)

Regla A (descender por L). Recursivo: Heap_Insert(·, 12) = BTree_Create(·, ·, 12).
Heap_CombineL(BTree_Create(·, ·, 12), ·, 15): m=12 < x=15 → swap. 
BTree_Create(BTree_Create(·, ·, 15) as Heap_H, ·, 12) as Heap_H
tras Insert 12 — size 2
12 / 15

A3 — Insert 3 (Regla C: |L|=1>|R|=0, L perfecto)

Regla C (descender por R, porque L singleton ya está perfecto). Recursivo: Heap_Insert(·, 3) = BTree_Create(·, ·, 3).
Heap_CombineR(L, BTree_Create(·, ·, 3), 12): m=3 < x=12 → swap: 12 baja al subárbol derecho, 3 sube a la raíz. 
BTree_Create(
    BTree_Create(·, ·, 15) as Heap_H,
    BTree_Create(·, ·, 12) as Heap_H,
    3) as Heap_H
tras Insert 3 — size 3
3 / \ 15 12

A4 — Insert 7 (Regla A: |L|=|R|=1)

Regla A (descender por L). Sub-recursión interna en L=BTree_Create(·,·,15): Vuelta al outer: Heap_CombineL(BTree_Create(BTree_Create(·,·,15), ·, 7), BTree_Create(·,·,12), 3): m=7 ≥ x=3 → no swap. 
BTree_Create(
    BTree_Create(BTree_Create(·, ·, 15) as Heap_H, ·, 7) as Heap_H,
    BTree_Create(·, ·, 12) as Heap_H,
    3) as Heap_H
tras Insert 7 — size 4
3 / \ 7 12 / 15

A5 — Insert 9 (Regla B: |L|=2>|R|=1, L no perfecto)

L tiene |LL|=1, |LR|=0 → no perfecto. Regla B (descender L para completarlo). Sub-recursión en L: Vuelta al outer: Heap_CombineL(..., BTree_Create(·,·,12), 3): 7 ≥ 3 → no swap. 
BTree_Create(
    BTree_Create(BTree_Create(·, ·, 15) as Heap_H,
                 BTree_Create(·, ·, 9) as Heap_H, 7) as Heap_H,
    BTree_Create(·, ·, 12) as Heap_H,
    3) as Heap_H
tras Insert 9 — size 5
3 / \ 7 12 / \ 15 9

A6 — Insert 11 (Regla C: |L|=3>|R|=1, L perfecto)

Ahora L tiene |LL|=|LR|=1, ambos singletons, → perfecto (3 nodos: árbol completo de altura 2). Regla C (descender R). Sub-recursión en R=BTree_Create(·,·,12): Vuelta al outer: Heap_CombineR(L_perfecto, BTree_Create(BTree_Create(·,·,12), ·, 11), 3): m=11 ≥ x=3 → no swap. 
BTree_Create(
    BTree_Create(BTree_Create(·, ·, 15) as Heap_H,
                 BTree_Create(·, ·, 9) as Heap_H, 7) as Heap_H,
    BTree_Create(BTree_Create(·, ·, 12) as Heap_H, ·, 11) as Heap_H,
    3) as Heap_H
tras Insert 11 — size 6, heap construido
3 / \ 7 11 /\ / 15 9 12

Posiciones BFS: 1=3, 2=7, 3=11, 4=15, 5=9, 6=12. Forma OK (completo niveles 1–2, último nivel parcial llenado izquierda → derecha hasta posición 6). Heap order OK: 3≤7, 3≤11, 7≤15, 7≤9, 11≤12.

Fase 2 — Heap_DeleteMin sobre el heap construido

Llamemos T al heap construido (BTree_Create(LT, RT, 3) as Heap_H). Como T no es singleton, se aplica el axioma general:

not (BTree_IsEmpty(L) and BTree_IsEmpty(R)) implies
Heap_DeleteMin(BTree_Create(L, R, x) as Heap_H) =
    Heap_SiftDown(
      Heap_ReplaceRoot(
        Heap_RemoveLast(BTree_Create(L, R, x) as Heap_H),
        Heap_Last(BTree_Create(L, R, x) as Heap_H)
      )
    );

D1 — Calcular Heap_Last(T)

T: |LT|=3, |RT|=2, |LT|>|RT| ✓.
perfect(LT)? LT tiene |LL|=|LR|=1, ambos perfectos → sí.
perfect(RT)? RT = BTree_Create(BTree_Create(·,·,12), ·, 11) con |RTL|=1, |RTR|=0 → no.
Condición "último en L": |L|>|R| ∧ (¬perfect(L) ∨ perfect(R)) = T ∧ (F ∨ F) = F → último en R.

Recursión en RT = BTree_Create(BTree_Create(·,·,12), ·, 11):

Resultado: Heap_Last(T) = 12.

D2 — Calcular Heap_RemoveLast(T)

Mismo análisis: último en RT. Aplico axioma:
Heap_RemoveLast(T) = BTree_Create(LT, Heap_RemoveLast(RT), 3).

Recursión: Heap_RemoveLast(RT) con último en L' →
= BTree_Create(Heap_RemoveLast(BTree_Create(·,·,12)), ·, 11)
= BTree_Create(Heap_Empty, ·, 11) (caso singleton)
= BTree_Create(·, ·, 11) as Heap_H. 
BTree_Create(
    BTree_Create(BTree_Create(·, ·, 15) as Heap_H,
                 BTree_Create(·, ·, 9) as Heap_H, 7) as Heap_H,
    BTree_Create(·, ·, 11) as Heap_H,
    3) as Heap_H
T sin la última posición (raíz aún 3) — size 5
3 / \ 7 11 /\ 15 9

D3 — Heap_ReplaceRoot(..., 12)

Axioma: Heap_ReplaceRoot(BTree_Create(L, R, x), m) = BTree_Create(L, R, m). Reemplazo 3 por 12: 
BTree_Create(
    BTree_Create(BTree_Create(·, ·, 15) as Heap_H,
                 BTree_Create(·, ·, 9) as Heap_H, 7) as Heap_H,
    BTree_Create(·, ·, 11) as Heap_H,
    12) as Heap_H
Antes de SiftDown (la raíz 12 viola la propiedad heap)
12 / \ 7 11 /\ 15 9

12 está por encima de 7 (hijo izq) y de 11 (hijo der). El SiftDown lo baja al lugar correcto.

D4 — Heap_SiftDown: nivel 1 (SDBoth, caso b)

Ambos hijos no vacíos → Heap_SDBoth(L, R, 12) con m1=7 (raíz de L), m2=11 (raíz de R), x=12.
CasoCondiciónAplica
(a)¬(7<12) ∧ ¬(11<12) = F ∧ FNo
(b)(7<12) ∧ ¬(11<7) = T ∧ TSí ←
(c)(11<12) ∧ (11<7) = T ∧ FNo
Caso (b): el menor hijo es m1=7, swap con izquierda y recurrir.
RHS: BTree_Create(Heap_SiftDown(BTree_Create(LL, LR, 12)), R, 7) con LL=BTree_Create(·,·,15), LR=BTree_Create(·,·,9).

Sub-término pendiente de SiftDown: BTree_Create(BTree_Create(·,·,15), BTree_Create(·,·,9), 12).

D5 — Heap_SiftDown recursivo: nivel 2 (SDBoth, caso c)

Sub-árbol: BTree_Create(BTree_Create(·,·,15), BTree_Create(·,·,9), 12). Ambos hijos no vacíos → SDBoth con m1=15, m2=9, x=12.
CasoCondiciónAplica
(a)¬(15<12) ∧ ¬(9<12) = T ∧ FNo
(b)(15<12) ∧ ¬(9<15) = F ∧ TNo
(c)(9<12) ∧ (9<15) = T ∧ TSí ←
Caso (c): el menor hijo es m2=9 (estrictamente menor que m1=15), swap con derecha y recurrir.
RHS: BTree_Create(BTree_Create(·,·,15), Heap_SiftDown(BTree_Create(·,·,12)), 9).

Sub-término pendiente: Heap_SiftDown(BTree_Create(·, ·, 12)) — hoja, no hace nada → BTree_Create(·, ·, 12). 
BTree_Create(
    BTree_Create(·, ·, 15) as Heap_H,
    BTree_Create(·, ·, 12) as Heap_H,
    9) as Heap_H

Sub-árbol post-sift: 9 a la raíz, 15 a la izquierda, 12 a la derecha. Propiedad heap localmente OK: 9 ≤ 15, 9 ≤ 12.

D6 — Sustituir resultado del sift recursivo en el árbol del paso D4

BTree_Create(
    BTree_Create(BTree_Create(·, ·, 15) as Heap_H,
                 BTree_Create(·, ·, 12) as Heap_H, 9) as Heap_H,
    BTree_Create(·, ·, 11) as Heap_H,
    7) as Heap_H
Forma normal del DeleteMin — size 5
7 / \ 9 11 /\ 15 12

Verificación y resumen

AspectoAntes del DeleteMinDespués del DeleteMin
Elementos{3, 7, 9, 11, 12, 15}{7, 9, 11, 12, 15}
Mínimo37
Tamaño65
Posiciones BFS1=3, 2=7, 3=11, 4=15, 5=9, 6=121=7, 2=9, 3=11, 4=15, 5=12
Forma (completo + último izq→der)✓✓
Heap order3 ≤ 7, 11 ; 7 ≤ 15, 9 ; 11 ≤ 12 ✓7 ≤ 9, 11 ; 9 ≤ 15, 12 ✓
Recorrido del "último" 12: al iniciar el DeleteMin, 12 estaba en la posición 6 (hoja izquierda del subárbol derecho). El proceso fue:
  1. Detección (D1): Heap_Last recorrió por RT (porque LT ya era perfecto), luego por L' (porque ahí estaba el último BFS), y encontró 12.
  2. Promoción a raíz (D3): 12 subió temporalmente a la raíz, violando el heap order.
  3. Descenso por sift (D4–D6): bajó por la izquierda (porque 7 era el menor hijo y 7 < 12), llegando al subárbol con raíz vieja 7. Después, dentro de ese subárbol, bajó por la derecha (porque 9 era estrictamente menor que 15) y quedó como hoja derecha de 9.
Resultado: 12 terminó dos niveles abajo de donde empezó, atravesando el árbol diagonalmente. Eso es lo que hace el sift-down clásico.
Comparación con el ejemplo anterior (Insert 5, 3, 8, 1 + DeleteMin): en aquél el SiftDown se resolvió en un solo nivel (D4: caso b, recursión sobre hoja). Acá el SiftDown atravesó dos niveles (D4 caso b → D5 caso c) porque el último elemento (12) era mayor que dos descendientes seguidos. Eso ilustra que el costo de SiftDown crece con la altura del árbol — O(log n) en el peor caso.