RESULTADO PROLOG: ARBOL COMPLETO
Objetivo alcanzable en el grafo: t_riemann
Nodos formales totales: 45
Formulas extraidas como hechos: 187
Nodos de la clausura deductiva del objetivo: 24
Nodos fuera de la clausura del objetivo: 21
Estos nodos NO se consideran errores por si mismos.
Pueden pertenecer a comprobaciones o ramas independientes.
Nodos externos: [a_7,d_lap,p_f,p_f1,p_f1_2,p_f2,p_f3,p_f3_2,p_lap_z,p_lap_z_2,p_st_2,p_ved_completo,p_ved_completo_2,p_ved_e_2,p_ved_i,p_ved_k_e,p_ved_k_e_2,p_ved_k_i,p_ved_r_c,p_vs,p_w]
Raices de ramas externas al objetivo: [p_f3_2,p_lap_z_2,p_ved_completo_2,p_ved_e_2,p_ved_k_e_2]
Cadena deductiva utilizada para el objetivo:
  a_l.
  d_f.
  d_finv :- d_f.
  d_k.
  d_l.
  d_lambda.
  d_rho.
  d_rho_r.
  d_rim.
  d_t_prime.
  d_u.
  p_a :- a_l, p_st, p_v.
  p_coord :- d_u.
  p_rho_iso :- t_iso.
  p_rim_s :- t_iso, p_rho_iso, d_rim.
  p_st :- p_coord, d_t_prime, a_l.
  p_v :- d_t_prime, a_l, p_st.
  p_ved_e :- p_ved_inv, d_k, d_rho.
  p_ved_inv :- p_a, d_lambda, d_l.
  p_vr_e :- p_vr_rho.
  p_vr_rho :- p_ved_e.
  p_z :- p_rim_s, p_vr_rho, p_vr_e, d_rim.
  t_iso :- d_f, d_finv.
  t_riemann :- t_iso, p_rho_iso, p_rim_s, p_z, d_rho_r, p_vr_rho, d_rim.

--- AUDITORIA DEL RECORRIDO LEAN ---
ARCHIVO: c:/users/vedq/desktop/desarrollo/src-ved/demuestra/proyectos/es_46_rv6/es_46_rv6.lean
--- SALIDA LEAN ---
Compilacion Lean ya realizada por el proceso llamador.
--- FIN SALIDA LEAN ---
% GENERADO_POR: C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA\vendor\PUBLICAR\PackPublica\formal_lean_backend.py
% FECHA_HORA_GENERACION: 2026-09-26T16:24:04+02:00
% ARGUMENTO_GENERACION: C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA\ES_46_RV6.md
% RESPONSABLE_DE_CORRECCION: C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA\vendor\PUBLICAR\PackPublica\formal_lean_backend.py
RESULTADO AUDITOR LEAN: CERTIFICADO
COMPILACION_LEAN: CORRECTA
NODOS_FORMALES: 39
ENLACES_DEDUCTIVOS: 45
RELACIONES_FORMALIZADAS: 72
DERIVACIONES_CERTIFICADAS: 26
Warning: c:/users/vedq/desktop/desarrollo/src-ved/demuestra/pckdemuestra/audita_lean.pl:570:
Warning:    Clauses of structural_issue/6 are not together in the source-file
Warning:    Earlier definition at c:/users/vedq/desktop/desarrollo/src-ved/demuestra/pckdemuestra/audita_lean.pl:498
Warning:    Current predicate: legitimate_source_node/1
Warning:    Use :- discontiguous structural_issue/6. to suppress this message