Traza — Heap_H clásico (completo por niveles)

Construcción de un heap con Insert 5, 3, 8, 1 y borrado del mínimo; ejercita las tres reglas de Insert y el DeleteMin clásico (último BFS + sift-down).
Términos a evaluar: 
Heap_DeleteMin(
    Heap_Insert(
        Heap_Insert(
            Heap_Insert(
                Heap_Insert(Heap_Empty() as Heap_H, 5),
                3),
            8),
        1))
Spec: Heap_H_complete.nereus. Convención: · = Heap_Empty() as Heap_H.

Fase 1 — Construcción del heap

Insert 5 — caso base

Sobre Heap_Empty, axioma base: produce singleton.
BTree_Create(·, ·, 5) as Heap_H
Estado
5

Insert 3 — Regla A (|L|=|R|=0)

Sobre BTree_Create(·, ·, 5): |L|=0, |R|=0, not(0>0) ✓ → Regla A, descender a L.
Recursión: Heap_Insert(·, 3) = BTree_Create(·, ·, 3).
Heap_CombineL(BTree_Create(·, ·, 3), ·, 5): m=3 < x=5 → swap. 
BTree_Create(BTree_Create(·, ·, 5) as Heap_H, ·, 3) as Heap_H
Estado
3 / 5

Insert 8 — Regla C (|L|=1>|R|=0, L perfecto)

Sobre BTree_Create(BTree_Create(·, ·, 5), ·, 3): |L|=1, |R|=0, |L|>|R| ✓, perfect(L) ✓ (singleton) → Regla C, descender a R.
Recursión: Heap_Insert(·, 8) = BTree_Create(·, ·, 8).
Heap_CombineR(L, BTree_Create(·, ·, 8), 3): m=8 ≥ x=3 → no swap. 
BTree_Create(
    BTree_Create(·, ·, 5) as Heap_H,
    BTree_Create(·, ·, 8) as Heap_H,
    3) as Heap_H
Estado
3 / \ 5 8

Insert 1 — Regla A con sift-up doble

Sobre BTree_Create(BTree_Create(·,·,5), BTree_Create(·,·,8), 3): |L|=1, |R|=1, not(1>1) ✓ → Regla A, descender a L.

Sub-paso: Heap_Insert(BTree_Create(·, ·, 5), 1): Vuelta al outer: Heap_CombineL(BTree_Create(BTree_Create(·, ·, 5), ·, 1), BTree_Create(·, ·, 8), 3): m=1 < x=3 → swap. 
BTree_Create(
    BTree_Create(BTree_Create(·, ·, 5) as Heap_H, ·, 3) as Heap_H,
    BTree_Create(·, ·, 8) as Heap_H,
    1) as Heap_H
Estado (heap completo de 4 nodos)
1 / \ 3 8 / 5

Forma OK: posiciones 1, 2, 3, 4 llenas; el "1" subió desde la posición 4 hasta la raíz. Propiedad heap OK: 1 ≤ 3, 1 ≤ 8, 3 ≤ 5.

Fase 2 — DeleteMin sobre el heap construido

Aplicamos Heap_DeleteMin(T) donde T es el heap del paso anterior. Como T no es singleton, se aplica el axioma:

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)
      )
    );

Paso D1 — Calcular Heap_Last(T)

T = BTree_Create(L, R, 1) con |L|=2, |R|=1. |L|>|R| ✓.
perfect(L)? L = BTree_Create(BTree_Create(·,·,5), ·, 3): |LL|=1≠|LR|=0 → no perfecto.
Condición "último en L": |L|>|R| ∧ (¬perfect(L) ∨ perfect(R)) = T ∧ (T ∨ T) = T → último en L.

Recursión: Heap_Last(L) con L = BTree_Create(BTree_Create(·,·,5), ·, 3):
|L'|=1, |R'|=0, |L'|>|R'|, perfect(L') (singleton). Último en L'.
Heap_Last(BTree_Create(·, ·, 5)): singleton → 5.

Resultado: Heap_Last(T) = 5.

Paso D2 — Calcular Heap_RemoveLast(T)

Mismo análisis que Heap_Last: último en L. Aplico el axioma:
Heap_RemoveLast(BTree_Create(L, R, x)) = BTree_Create(Heap_RemoveLast(L), R, x) as Heap_H.

Recursión: Heap_RemoveLast(L) con L = BTree_Create(BTree_Create(·,·,5), ·, 3):
último en L' → BTree_Create(Heap_RemoveLast(BTree_Create(·,·,5)), ·, 3).
Heap_RemoveLast(BTree_Create(·,·,5)) = Heap_Empty (caso singleton).
Resultado interno: BTree_Create(·, ·, 3) as Heap_H. 
BTree_Create(
    BTree_Create(·, ·, 3) as Heap_H,
    BTree_Create(·, ·, 8) as Heap_H,
    1) as Heap_H
T sin la última posición (raíz sigue siendo 1)
1 / \ 3 8

Paso D3 — Heap_ReplaceRoot(..., 5)

Axioma: Heap_ReplaceRoot(BTree_Create(L, R, x), m) = BTree_Create(L, R, m).
Reemplazo 1 (la raíz vieja) por 5 (el "último" que retiramos): 
BTree_Create(
    BTree_Create(·, ·, 3) as Heap_H,
    BTree_Create(·, ·, 8) as Heap_H,
    5) as Heap_H
Antes de sift-down (la raíz 5 puede violar la propiedad heap)
5 / \ 3 8

La propiedad de heap se violó (5 > 3, raíz mayor que su hijo izquierdo). Heap_SiftDown la restaura.

Paso D4 — Heap_SiftDown

Sobre BTree_Create(BTree_Create(·,·,3), BTree_Create(·,·,8), 5): ambos hijos no vacíos → Heap_SDBoth(L, R, 5).

SDBoth con m1 = 3 (raíz de L), m2 = 8 (raíz de R), x = 5:

CasoCondiciónAplicable
(a)¬(m1<x) ∧ ¬(m2<x) = ¬(3<5) ∧ ¬(8<5) = F ∧ TNo
(b)(m1<x) ∧ ¬(m2<m1) = (3<5) ∧ ¬(8<3) = T ∧ TSí ←
(c)(m2<x) ∧ (m2<m1) = (8<5) ∧ (8<3) = F ∧ FNo
Caso (b): el menor de los hijos es m1=3. Swap con izquierda y recursar sobre el nuevo L.

Sub-paso: Heap_SiftDown(BTree_Create(·, ·, 5)) — hoja → no hace nada. Devuelve BTree_Create(·, ·, 5). 
BTree_Create(
    BTree_Create(·, ·, 5) as Heap_H,
    BTree_Create(·, ·, 8) as Heap_H,
    3) as Heap_H
Forma normal: heap tras DeleteMin
3 / \ 5 8

Resumen y verificación

Antes / DespuésHeapMínTamañoFormaHeap order
Antes (4 nodos) {1, 3, 5, 8} 1 4 ✓ (posiciones 1–4) ✓
Después (3 nodos) {3, 5, 8} 3 3 ✓ (posiciones 1–3) ✓ (3 ≤ 5, 3 ≤ 8)
Lectura semántica: el heap contenía {1, 3, 5, 8} con 1 a la raíz. DeleteMin sacó el mínimo (1) y dejó el heap clásico con 3 elementos: 3 a la raíz, 5 a la izquierda, 8 a la derecha. El "5" venía de la última posición y trepó vía el sift-down hacia donde estaba 3, mientras que 3 (el nuevo mínimo) subió a la raíz.
Verificación de invariantes: