% ============================================================
% DEMUESTRA / PUBLICAR
% Auditoria logica Prolog
%
% Fuente unica:
%     Markdown
%
% Cadena:
%     Markdown
%       -> FormalGraph
%       -> FormalGraphCompiler
%       -> Prolog
%
% Este archivo NO se genera desde el JSON de ADEC.
% Este archivo NO modifica el Markdown.
% Este archivo NO modifica JSON, Lean ni otros derivados.
%
% Prolog verifica:
%   - integridad estructural del grafo
%   - dependencias declaradas
%   - ausencia de ciclos
%   - ausencia de autorreferencias
%   - ausencia de referencias inexistentes
%   - cierre del arbol de dependencias del objetivo
%   - cobertura de formulas extraidas como hechos estructurados
%   - referencias a conjuntos con definicion unica
%   - cobertura deductiva respecto del objetivo
% No valida todas las implicaciones matematicas del Markdown.
%
% IMPORTANTE:
% Un nodo fuera de la clausura del objetivo no es
% automaticamente un error. Puede pertenecer a una rama
% independiente del documento.
% ============================================================

:- set_prolog_flag(double_quotes, string).
:- discontiguous fact/1.
:- discontiguous rule/2.
:- discontiguous declared_node/2.
:- discontiguous graph_error/1.
:- discontiguous formula_count/2.
:- discontiguous source_formula/3.
:- discontiguous defines_set/2.
:- discontiguous uses_defined_set/2.
:- dynamic unresolved_dependency/2.

goal(t_riemann).

declared_node(d_u, definition).
declared_node(d_t_prime, definition).
declared_node(a_l, foundation).
declared_node(d_lambda, definition).
declared_node(d_l, definition).
declared_node(d_k, definition).
declared_node(d_rho, definition).
declared_node(d_rim, definition).
declared_node(d_rho_r, definition).
declared_node(d_f, definition).
declared_node(d_finv, definition).
declared_node(p_coord, proposition).
declared_node(t_iso, theorem).
declared_node(p_st, proposition).
declared_node(p_rho_iso, proposition).
declared_node(p_v, proposition).
declared_node(p_rim_s, proposition).
declared_node(p_a, proposition).
declared_node(p_ved_inv, proposition).
declared_node(p_ved_e, proposition).
declared_node(p_ved_i, proposition).
declared_node(p_vr_rho, proposition).
declared_node(p_ved_k_e, proposition).
declared_node(p_vr_e, proposition).
declared_node(p_ved_k_i, proposition).
declared_node(p_z, proposition).
declared_node(p_ved_r_c, proposition).
declared_node(t_riemann, theorem).
declared_node(p_ved_completo, proposition).
declared_node(p_vs, proposition).
declared_node(p_f, proposition).
declared_node(p_f1, proposition).
declared_node(p_w, proposition).
declared_node(p_f2, proposition).
declared_node(p_f3, proposition).
declared_node(d_lap, definition).
declared_node(p_lap_z, proposition).

formula_count(d_u, 1).
source_formula(d_u, 1, ast(binary, "EQ", [ast(identifier, "U", []), ast(binary, "PLUS", [ast(binary, "MUL", [ast(number, "3", []), ast(identifier, "S", [])]), ast(identifier, "T", [])])])).
formula_count(d_t_prime, 4).
source_formula(d_t_prime, 1, ast(binary, "DIV", [ast(identifier, "dt'", []), ast(identifier, "dt", [])])).
source_formula(d_t_prime, 2, ast(identifier, "t'", [])).
source_formula(d_t_prime, 3, ast(identifier, "t'", [])).
source_formula(d_t_prime, 4, ast(identifier, "dt'", [])).
formula_count(a_l, 5).
source_formula(a_l, 1, ast(binary, "EQ", [ast(identifier, "dt'", []), ast(binary, "MUL", [ast(identifier, "dt", []), ast(call, "sqrt", [ast(binary, "MINUS", [ast(number, "1", []), ast(binary, "DIV", [ast(power, none, [ast(identifier, "v", []), ast(number, "2", [])]), ast(power, none, [ast(identifier, "c", []), ast(number, "2", [])])])])])])])).
source_formula(a_l, 2, ast(binary, "EQ", [ast(identifier, "v", []), ast(binary, "DIV", [ast(identifier, "ds", []), ast(identifier, "dt", [])])])).
source_formula(a_l, 3, ast(binary, "EQ", [ast(identifier, "c", []), ast(number, "1", [])])).
source_formula(a_l, 4, ast(binary, "EQ", [ast(power, none, [ast(identifier, "dt'", []), ast(number, "2", [])]), ast(binary, "MINUS", [ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])]), ast(power, none, [ast(identifier, "ds", []), ast(number, "2", [])])])])).
source_formula(a_l, 5, ast(identifier, "v", [])).
formula_count(d_lambda, 5).
source_formula(d_lambda, 1, ast(binary, "EQ", [ast(identifier, "E", []), ast(binary, "DIV", [ast(identifier, "hc", []), ast(identifier, "lambda", [])])])).
source_formula(d_lambda, 2, ast(binary, "EQ", [ast(identifier, "E", []), ast(power, none, [ast(identifier, "Mc", []), ast(number, "2", [])])])).
source_formula(d_lambda, 3, ast(binary, "EQ", [ast(power, none, [ast(identifier, "Mc", []), ast(number, "2", [])]), ast(binary, "DIV", [ast(identifier, "hc", []), ast(identifier, "lambda", [])])])).
source_formula(d_lambda, 4, ast(binary, "EQ", [ast(identifier, "lambda", []), ast(binary, "DIV", [ast(identifier, "h", []), ast(identifier, "Mc", [])])])).
source_formula(d_lambda, 5, ast(identifier, "lambda", [])).
formula_count(d_l, 3).
source_formula(d_l, 1, ast(binary, "EQ", [ast(identifier, "L", []), ast(binary, "MUL", [ast(identifier, "n", []), ast(identifier, "lambda", [])])])).
source_formula(d_l, 2, ast(binary, "IN", [ast(identifier, "n", []), ast(power, none, [ast(identifier, "R", []), ast(sign, "PLUS", [])])])).
source_formula(d_l, 3, ast(identifier, "L", [])).
formula_count(d_k, 1).
source_formula(d_k, 1, ast(binary, "IN", [ast(identifier, "k", []), ast(power, none, [ast(identifier, "N", []), ast(sign, "PLUS", [])])])).
formula_count(d_rho, 6).
source_formula(d_rho, 1, ast(binary, "EQ", [ast(identifier, "rho", []), ast(apply, none, [ast(identifier, "dist", []), ast(identifier, "n", []), ast(power, none, [ast(identifier, "N", []), ast(sign, "PLUS", [])])])])).
source_formula(d_rho, 2, ast(binary, "AND", [ast(binary, "LE", [ast(number, "0", []), ast(identifier, "rho", [])]), ast(binary, "LE", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])).
source_formula(d_rho, 3, ast(tuple, "LBRACE", [ast(binary, "EQ", [ast(identifier, "n", []), ast(binary, "PM", [ast(identifier, "k", []), ast(identifier, "rho", [])])]), ast(binary, "IN", [ast(identifier, "k", []), ast(power, none, [ast(identifier, "N", []), ast(sign, "PLUS", [])])]), ast(binary, "AND", [ast(binary, "LE", [ast(number, "0", []), ast(identifier, "rho", [])]), ast(binary, "LE", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])])).
source_formula(d_rho, 4, ast(binary, "EQ", [ast(call, "L", [ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(binary, "MUL", [ast(binary, "PM", [ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(identifier, "lambda", [])])])).
source_formula(d_rho, 5, ast(binary, "EQ", [ast(apply, none, [ast(subscript, none, [ast(identifier, "R", []), ast(identifier, "VED", [])]), ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(binary, "DIV", [ast(binary, "MUL", [ast(binary, "PM", [ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(identifier, "lambda", [])]), ast(binary, "MUL", [ast(number, "2", []), ast(constant, "PI", [])])])])).
source_formula(d_rho, 6, ast(binary, "EQ", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
formula_count(d_rim, 9).
source_formula(d_rim, 1, ast(binary, "EQ", [ast(identifier, "z", []), ast(binary, "PM", [ast(identifier, "a", []), ast(identifier, "ib", [])])])).
source_formula(d_rim, 2, ast(binary, "EQ", [ast(apply, none, [ast(identifier, "zeta", []), ast(identifier, "s", [])]), ast(binary, "MUL", [ast(power, none, [ast(subscript, none, [ast(identifier, "sum", []), ast(binary, "EQ", [ast(identifier, "n", []), ast(number, "1", [])])]), ast(constant, "INFINITY", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(power, none, [ast(identifier, "n", []), ast(identifier, "s", [])])])])])).
source_formula(d_rim, 3, ast(binary, "EQ", [ast(identifier, "s", []), ast(number, "1", [])])).
source_formula(d_rim, 4, ast(binary, "AND", [ast(binary, "EQ", [ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "triv", [])]), ast(set, none, [ast(unary, "NEG", [ast(number, "2", [])]), ast(unary, "NEG", [ast(number, "4", [])]), ast(unary, "NEG", [ast(number, "6", [])]), ast(identifier, "ldots", [])])]), ast(binary, "EQ", [ast(set, none, [ast(unary, "NEG", [ast(number, "2", [])]), ast(unary, "NEG", [ast(number, "4", [])]), ast(unary, "NEG", [ast(number, "6", [])]), ast(identifier, "ldots", [])]), ast(set_builder, none, [ast(binary, "MUL", [ast(unary, "NEG", [ast(number, "2", [])]), ast(identifier, "m", [])]), ast(binary, "IN", [ast(identifier, "m", []), ast(power, none, [ast(identifier, "N", []), ast(sign, "PLUS", [])])])])])])).
source_formula(d_rim, 5, ast(binary, "EQ", [ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])]), ast(set_builder, none, [ast(identifier, "z", []), ast(binary, "AND", [ast(binary, "AND", [ast(binary, "IN", [ast(identifier, "z", []), ast(identifier, "C", [])]), ast(binary, "EQ", [ast(apply, none, [ast(identifier, "zeta", []), ast(identifier, "z", [])]), ast(number, "0", [])])]), ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(call, "Re", [ast(identifier, "z", [])])]), ast(binary, "LT", [ast(call, "Re", [ast(identifier, "z", [])]), ast(number, "1", [])])])])])])).
source_formula(d_rim, 6, ast(tuple, "LBRACE", [ast(binary, "EQ", [ast(identifier, "z", []), ast(binary, "PM", [ast(identifier, "a", []), ast(identifier, "ib", [])])]), ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(identifier, "a", [])]), ast(binary, "LT", [ast(identifier, "a", []), ast(number, "1", [])])])])).
source_formula(d_rim, 7, ast(binary, "MINUS", [ast(binary, "MUL", [ast(binary, "MUL", [ast(identifier, "a", []), ast(identifier, "longleftrightarrow", [])]), ast(number, "1", [])]), ast(identifier, "a", [])])).
source_formula(d_rim, 8, ast(binary, "EQ", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(d_rim, 9, ast(binary, "GT", [ast(call, "Re", [ast(identifier, "s", [])]), ast(number, "1", [])])).
formula_count(d_rho_r, 8).
source_formula(d_rho_r, 1, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])])).
source_formula(d_rho_r, 2, ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(identifier, "a", [])]), ast(binary, "LT", [ast(identifier, "a", []), ast(number, "1", [])])])).
source_formula(d_rho_r, 3, ast(binary, "AND", [ast(binary, "LE", [ast(number, "0", []), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])])]), ast(binary, "LT", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])).
source_formula(d_rho_r, 4, ast(binary, "EQ", [ast(identifier, "a", []), ast(binary, "PLUS", [ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])]), ast(binary, "MUL", [ast(identifier, "varepsilon", []), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])])])])])).
source_formula(d_rho_r, 5, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "z", []), ast(tuple, "LBRACE", [ast(identifier, "varepsilon", []), ast(sign, "PM", [])])]), ast(binary, "PM", [ast(binary, "PLUS", [ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])]), ast(binary, "MUL", [ast(identifier, "varepsilon", []), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])])])]), ast(identifier, "ib", [])])])).
source_formula(d_rho_r, 6, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(call, "abs", [ast(binary, "MINUS", [ast(call, "Re", [ast(identifier, "z", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])])).
source_formula(d_rho_r, 7, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(d_rho_r, 8, ast(binary, "EQ", [ast(identifier, "varepsilon", []), ast(unary, "PM", [ast(number, "1", [])])])).
formula_count(d_f, 6).
source_formula(d_f, 1, ast(binary, "EQ", [ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])]), ast(identifier, "rho", [])]), ast(set_builder, none, [ast(identifier, "x", []), ast(binary, "IN", [ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])]), ast(identifier, "x", [])]), ast(interval, "LBRACK", [ast(number, "0", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])])])).
source_formula(d_f, 2, ast(binary, "EQ", [ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])]), ast(identifier, "rho", [])]), ast(set_builder, none, [ast(identifier, "z", []), ast(binary, "IN", [ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(identifier, "z", [])]), ast(interval, "LBRACK", [ast(number, "0", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])])])).
source_formula(d_f, 3, ast(binary, "COLON", [ast(identifier, "f", []), ast(binary, "MAPSTO", [ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])]), ast(identifier, "rho", [])]), ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])]), ast(identifier, "rho", [])])])])).
source_formula(d_f, 4, ast(identifier, "rho", [])).
source_formula(d_f, 5, ast(binary, "EQ", [ast(identifier, "a", []), ast(call, "Re", [ast(identifier, "z", [])])])).
source_formula(d_f, 6, ast(binary, "EQ", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
formula_count(d_finv, 2).
source_formula(d_finv, 1, ast(binary, "COLON", [ast(power, none, [ast(identifier, "f", []), ast(unary, "NEG", [ast(number, "1", [])])]), ast(binary, "MAPSTO", [ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])]), ast(identifier, "rho", [])]), ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])]), ast(identifier, "rho", [])])])])).
source_formula(d_finv, 2, ast(tuple, "LBRACE", [ast(binary, "EQ", [ast(apply, none, [ast(power, none, [ast(identifier, "f", []), ast(unary, "NEG", [ast(number, "1", [])])]), ast(call, "f", [ast(identifier, "x", [])])]), ast(identifier, "x", [])]), ast(binary, "EQ", [ast(call, "f", [ast(apply, none, [ast(power, none, [ast(identifier, "f", []), ast(unary, "NEG", [ast(number, "1", [])])]), ast(identifier, "z", [])])]), ast(identifier, "z", [])])])).
formula_count(p_coord, 1).
source_formula(p_coord, 1, ast(binary, "MUL", [ast(number, "3", []), ast(identifier, "S", [])])).
formula_count(t_iso, 5).
source_formula(t_iso, 1, ast(binary, "CONG", [ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])]), ast(identifier, "rho", [])]), ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])]), ast(identifier, "rho", [])])])).
source_formula(t_iso, 2, ast(identifier, "f", [])).
source_formula(t_iso, 3, ast(power, none, [ast(identifier, "f", []), ast(unary, "NEG", [ast(number, "1", [])])])).
source_formula(t_iso, 4, ast(binary, "EQ", [ast(identifier, "rho", []), ast(number, "0", [])])).
source_formula(t_iso, 5, ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(identifier, "rho", [])]), ast(binary, "LE", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])).
formula_count(p_st, 2).
source_formula(p_st, 1, ast(binary, "EQ", [ast(power, none, [ast(identifier, "ds", []), ast(number, "2", [])]), ast(binary, "MINUS", [ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])]), ast(power, none, [ast(identifier, "dt'", []), ast(number, "2", [])])])])).
source_formula(p_st, 2, ast(binary, "EQ", [ast(power, none, [ast(identifier, "ds", []), ast(number, "2", [])]), ast(binary, "MUL", [ast(binary, "MINUS", [ast(identifier, "dt", []), ast(identifier, "dt'", [])]), ast(binary, "PLUS", [ast(identifier, "dt", []), ast(identifier, "dt'", [])])])])).
formula_count(p_rho_iso, 6).
source_formula(p_rho_iso, 1, ast(tuple, "LBRACE", [ast(binary, "EQ", [ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(call, "f", [ast(identifier, "x", [])])]), ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])]), ast(identifier, "x", [])])]), ast(binary, "EQ", [ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])]), ast(apply, none, [ast(power, none, [ast(identifier, "f", []), ast(unary, "NEG", [ast(number, "1", [])])]), ast(identifier, "z", [])])]), ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(identifier, "z", [])])])])).
source_formula(p_rho_iso, 2, ast(binary, "IFF", [ast(binary, "EQ", [ast(identifier, "rho", []), ast(number, "0", [])]), ast(text, "clase_estable", [])])).
source_formula(p_rho_iso, 3, ast(binary, "IFF", [ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(identifier, "rho", [])]), ast(binary, "LE", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])]), ast(text, "clase_no_estable", [])])).
source_formula(p_rho_iso, 4, ast(identifier, "rho", [])).
source_formula(p_rho_iso, 5, ast(identifier, "f", [])).
source_formula(p_rho_iso, 6, ast(power, none, [ast(identifier, "f", []), ast(unary, "NEG", [ast(number, "1", [])])])).
formula_count(p_v, 3).
source_formula(p_v, 1, ast(binary, "EQ", [ast(binary, "DIV", [ast(identifier, "ds", []), ast(identifier, "dt", [])]), ast(identifier, "v", [])])).
source_formula(p_v, 2, ast(binary, "EQ", [ast(binary, "DIV", [ast(binary, "MUL", [ast(power, none, [ast(identifier, "d", []), ast(number, "2", [])]), ast(identifier, "s", [])]), ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])])]), ast(number, "0", [])])).
source_formula(p_v, 3, ast(identifier, "v", [])).
formula_count(p_rim_s, 8).
source_formula(p_rim_s, 1, ast(quantifier, "FORALL", [ast(identifier, "z", []), ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])]), ast(binary, "IFF", [ast(apply, none, [ast(subscript, none, [ast(identifier, "Stable", []), ast(identifier, "Rim", [])]), ast(identifier, "z", [])]), ast(binary, "EQ", [ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(identifier, "z", [])]), ast(number, "0", [])])])])).
source_formula(p_rim_s, 2, ast(binary, "IMPLIES", [ast(binary, "IN", [ast(identifier, "z", []), ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])])]), ast(binary, "IMPLIES", [ast(apply, none, [ast(subscript, none, [ast(identifier, "Stable", []), ast(identifier, "Rim", [])]), ast(identifier, "z", [])]), ast(binary, "EQ", [ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(identifier, "z", [])]), ast(number, "0", [])])])])).
source_formula(p_rim_s, 3, ast(identifier, "rho", [])).
source_formula(p_rim_s, 4, ast(identifier, "f", [])).
source_formula(p_rim_s, 5, ast(power, none, [ast(identifier, "f", []), ast(unary, "NEG", [ast(number, "1", [])])])).
source_formula(p_rim_s, 6, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])])).
source_formula(p_rim_s, 7, ast(binary, "NE", [ast(apply, none, [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(identifier, "z", [])]), ast(number, "0", [])])).
source_formula(p_rim_s, 8, ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])])).
formula_count(p_a, 3).
source_formula(p_a, 1, ast(binary, "AND", [ast(binary, "EQ", [ast(binary, "DIV", [ast(binary, "MUL", [ast(power, none, [ast(identifier, "d", []), ast(number, "2", [])]), ast(identifier, "s", [])]), ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])])]), ast(binary, "DIV", [ast(identifier, "dv", []), ast(identifier, "dt", [])])]), ast(binary, "EQ", [ast(binary, "DIV", [ast(identifier, "dv", []), ast(identifier, "dt", [])]), ast(identifier, "a", [])])])).
source_formula(p_a, 2, ast(identifier, "t", [])).
source_formula(p_a, 3, ast(identifier, "t'", [])).
formula_count(p_ved_inv, 4).
source_formula(p_ved_inv, 1, ast(identifier, "L", [])).
source_formula(p_ved_inv, 2, ast(identifier, "lambda", [])).
source_formula(p_ved_inv, 3, ast(identifier, "n", [])).
source_formula(p_ved_inv, 4, ast(identifier, "rho", [])).
formula_count(p_ved_e, 2).
source_formula(p_ved_e, 1, ast(binary, "IFF", [ast(binary, "IFF", [ast(binary, "IFF", [ast(binary, "IFF", [ast(binary, "EQ", [ast(identifier, "rho", []), ast(number, "0", [])]), ast(binary, "AND", [ast(binary, "EQ", [ast(identifier, "n", []), ast(identifier, "k", [])]), ast(binary, "IN", [ast(identifier, "k", []), ast(power, none, [ast(identifier, "N", []), ast(sign, "PLUS", [])])])])]), ast(binary, "EQ", [ast(identifier, "L", []), ast(binary, "MUL", [ast(identifier, "k", []), ast(identifier, "lambda", [])])])]), ast(text, "cierre_exacto_en_fase", [])]), ast(text, "estado_estable", [])])).
source_formula(p_ved_e, 2, ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(identifier, "rho", [])]), ast(binary, "LE", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])).
formula_count(p_ved_i, 2).
source_formula(p_ved_i, 1, ast(binary, "IFF", [ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(identifier, "rho", [])]), ast(binary, "LE", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])]), ast(text, "cierre_no_estable", [])])).
source_formula(p_ved_i, 2, ast(binary, "EQ", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
formula_count(p_vr_rho, 2).
source_formula(p_vr_rho, 1, ast(binary, "AND", [ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])]), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])])]), ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])])])).
source_formula(p_vr_rho, 2, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
formula_count(p_ved_k_e, 3).
source_formula(p_ved_k_e, 1, ast(binary, "EQ", [ast(subscript, none, [ast(decorated, "mathcal", [ast(identifier, "E", [])]), ast(identifier, "VED", [])]), ast(set_builder, none, [ast(tuple, "LPAREN", [ast(identifier, "k", []), ast(number, "0", [])]), ast(binary, "IN", [ast(identifier, "k", []), ast(power, none, [ast(identifier, "N", []), ast(sign, "PLUS", [])])])])])).
source_formula(p_ved_k_e, 2, ast(binary, "AND", [ast(binary, "AND", [ast(binary, "AND", [ast(binary, "EQ", [ast(identifier, "k", []), ast(number, "1", [])]), ast(number, "2", [])]), ast(number, "3", [])]), ast(identifier, "ldots", [])])).
source_formula(p_ved_k_e, 3, ast(binary, "EQ", [ast(identifier, "rho", []), ast(number, "0", [])])).
formula_count(p_vr_e, 3).
source_formula(p_vr_e, 1, ast(binary, "IFF", [ast(text, "estado_estable", []), ast(binary, "EQ", [ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])]), ast(number, "0", [])])])).
source_formula(p_vr_e, 2, ast(binary, "IFF", [ast(text, "estado_estable", []), ast(binary, "EQ", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])).
source_formula(p_vr_e, 3, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
formula_count(p_ved_k_i, 2).
source_formula(p_ved_k_i, 1, ast(binary, "EQ", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(p_ved_k_i, 2, ast(identifier, "k", [])).
formula_count(p_z, 1).
source_formula(p_z, 1, ast(binary, "IMPLIES", [ast(binary, "IN", [ast(identifier, "z", []), ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])])]), ast(assertion, "clasifica_su_localización_transversal", [ast(binary, "AND", [ast(binary, "CONTEXT", [ast(binary, "EQ", [ast(apply, none, [ast(identifier, "zeta", []), ast(identifier, "z", [])]), ast(number, "0", [])]), ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])])]), ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])])])])])])).
formula_count(p_ved_r_c, 2).
source_formula(p_ved_r_c, 1, ast(binary, "AND", [ast(binary, "LE", [ast(number, "0", []), ast(identifier, "rho", [])]), ast(binary, "LE", [ast(identifier, "rho", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])).
source_formula(p_ved_r_c, 2, ast(identifier, "k", [])).
formula_count(t_riemann, 33).
source_formula(t_riemann, 1, ast(binary, "EQ", [ast(identifier, "z", []), ast(binary, "PM", [ast(identifier, "a", []), ast(identifier, "ib", [])])])).
source_formula(t_riemann, 2, ast(binary, "EQ", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(t_riemann, 3, ast(binary, "EQ", [ast(apply, none, [ast(identifier, "zeta", []), ast(identifier, "z", [])]), ast(number, "0", [])])).
source_formula(t_riemann, 4, ast(binary, "AND", [ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])]), ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])]), ast(binary, "EQ", [ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])]), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])])])])).
source_formula(t_riemann, 5, ast(binary, "IFF", [ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])]), ast(number, "0", [])]), ast(text, "estado_estable", [])])).
source_formula(t_riemann, 6, ast(binary, "IFF", [ast(binary, "AND", [ast(binary, "LT", [ast(number, "0", []), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])])]), ast(binary, "LE", [ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "VED", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])]), ast(text, "estado_no_estable", [])])).
source_formula(t_riemann, 7, ast(binary, "NE", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(t_riemann, 8, ast(binary, "GT", [ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])]), ast(number, "0", [])])).
source_formula(t_riemann, 9, ast(binary, "AND", [ast(binary, "EQ", [ast(identifier, "rho", []), ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])]), ast(binary, "GT", [ast(call, "abs", [ast(binary, "MINUS", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])]), ast(number, "0", [])])])).
source_formula(t_riemann, 10, ast(binary, "IMPLIES", [ast(binary, "GT", [ast(identifier, "rho", []), ast(number, "0", [])]), ast(text, "estado_no_estable", [])])).
source_formula(t_riemann, 11, ast(binary, "EQ", [ast(identifier, "rho", []), ast(number, "0", [])])).
source_formula(t_riemann, 12, ast(binary, "NE", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(t_riemann, 13, ast(binary, "EQ", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(t_riemann, 14, ast(quantifier, "FORALL", [ast(identifier, "z", []), ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])]), ast(binary, "EQ", [ast(call, "Re", [ast(identifier, "z", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])).
source_formula(t_riemann, 15, ast(binary, "SUBSETEQ", [ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])]), ast(set_builder, none, [ast(identifier, "s", []), ast(binary, "AND", [ast(binary, "IN", [ast(identifier, "s", []), ast(identifier, "C", [])]), ast(binary, "EQ", [ast(call, "Re", [ast(identifier, "s", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])])])])).
source_formula(t_riemann, 16, ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])])).
source_formula(t_riemann, 17, ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])])).
source_formula(t_riemann, 18, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])])).
source_formula(t_riemann, 19, ast(subscript, none, [ast(identifier, "D", []), ast(subscript, none, [ast(identifier, "rho", []), ast(identifier, "R", [])])])).
source_formula(t_riemann, 20, ast(apply, none, [ast(subscript, none, [ast(identifier, "P", []), ast(identifier, "VR", [])]), ast(identifier, "rho", [])])).
source_formula(t_riemann, 21, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
source_formula(t_riemann, 22, ast(apply, none, [ast(subscript, none, [ast(identifier, "P", []), ast(identifier, "VR", [])]), ast(identifier, "rho", [])])).
source_formula(t_riemann, 23, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
source_formula(t_riemann, 24, ast(binary, "EQ", [ast(apply, none, [ast(identifier, "zeta", []), ast(identifier, "z", [])]), ast(number, "0", [])])).
source_formula(t_riemann, 25, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])])).
source_formula(t_riemann, 26, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
source_formula(t_riemann, 27, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
source_formula(t_riemann, 28, ast(binary, "NE", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(t_riemann, 29, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Rim", [])])).
source_formula(t_riemann, 30, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
source_formula(t_riemann, 31, ast(binary, "EQ", [ast(apply, none, [ast(identifier, "zeta", []), ast(identifier, "z", [])]), ast(number, "0", [])])).
source_formula(t_riemann, 32, ast(identifier, "z", [])).
source_formula(t_riemann, 33, ast(power, none, [ast(subscript, none, [ast(identifier, "Z", []), ast(identifier, "Rim", [])]), ast(identifier, "nt", [])])).
formula_count(p_ved_completo, 2).
source_formula(p_ved_completo, 1, ast(binary, "UNION", [ast(binary, "EQ", [ast(power, none, [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])]), ast(identifier, "cerrado", [])]), ast(subscript, none, [ast(decorated, "mathcal", [ast(identifier, "E", [])]), ast(identifier, "VED", [])])]), ast(subscript, none, [ast(decorated, "mathcal", [ast(identifier, "I", [])]), ast(identifier, "VED", [])])])).
source_formula(p_ved_completo, 2, ast(limit, none, [ast(identifier, "n", []), ast(constant, "INFINITY", [])])).
formula_count(p_vs, 6).
source_formula(p_vs, 1, ast(binary, "CONG", [ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])]), ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Sch", [])])])).
source_formula(p_vs, 2, ast(binary, "EQ", [ast(call, "G", [ast(number, "2", [])]), ast(identifier, "G", [])])).
source_formula(p_vs, 3, ast(binary, "EQ", [ast(binary, "MUL", [ast(subscript, none, [ast(identifier, "lim", []), ast(limit, none, [ast(identifier, "n", []), ast(constant, "INFINITY", [])])]), ast(call, "G", [ast(identifier, "n", [])])]), ast(number, "0", [])])).
source_formula(p_vs, 4, ast(identifier, "n", [])).
source_formula(p_vs, 5, ast(binary, "EQ", [ast(identifier, "n", []), ast(number, "2", [])])).
source_formula(p_vs, 6, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "Sch", [])])).
formula_count(p_f, 3).
source_formula(p_f, 1, ast(binary, "EQ", [ast(identifier, "F", []), ast(binary, "PLUS", [ast(binary, "MINUS", [ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])]), ast(power, none, [ast(identifier, "dt'", []), ast(number, "2", [])])]), ast(binary, "MUL", [ast(binary, "DIV", [ast(identifier, "d", []), ast(identifier, "dt", [])]), ast(binary, "MINUS", [ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])]), ast(power, none, [ast(identifier, "dt'", []), ast(number, "2", [])])])])])])).
source_formula(p_f, 2, ast(identifier, "dt'", [])).
source_formula(p_f, 3, ast(identifier, "t", [])).
formula_count(p_f1, 3).
source_formula(p_f1, 1, ast(binary, "EQ", [ast(identifier, "F", []), ast(binary, "MINUS", [ast(binary, "PLUS", [ast(binary, "MINUS", [ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])]), ast(power, none, [ast(identifier, "dt'", []), ast(number, "2", [])])]), ast(binary, "MUL", [ast(number, "2", []), ast(identifier, "dt", [])])]), ast(binary, "MUL", [ast(binary, "MUL", [ast(number, "2", []), ast(identifier, "dt'", [])]), ast(binary, "DIV", [ast(identifier, "dt'", []), ast(identifier, "dt", [])])])])])).
source_formula(p_f1, 2, ast(identifier, "dt'", [])).
source_formula(p_f1, 3, ast(binary, "DIV", [ast(identifier, "dt'", []), ast(identifier, "dt", [])])).
formula_count(p_w, 10).
source_formula(p_w, 1, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "v", []), ast(identifier, "onda", [])]), ast(identifier, "c", [])])).
source_formula(p_w, 2, ast(binary, "EQ", [ast(identifier, "c", []), ast(number, "1", [])])).
source_formula(p_w, 3, ast(binary, "EQ", [ast(identifier, "v", []), ast(binary, "DIV", [ast(identifier, "ds", []), ast(identifier, "dt", [])])])).
source_formula(p_w, 4, ast(binary, "EQ", [ast(binary, "DIV", [ast(identifier, "ds", []), ast(identifier, "dt", [])]), ast(number, "1", [])])).
source_formula(p_w, 5, ast(binary, "EQ", [ast(identifier, "ds", []), ast(identifier, "dt", [])])).
source_formula(p_w, 6, ast(binary, "EQ", [ast(identifier, "dt'", []), ast(binary, "MUL", [ast(identifier, "dt", []), ast(call, "sqrt", [ast(binary, "MINUS", [ast(number, "1", []), ast(binary, "DIV", [ast(power, none, [ast(identifier, "v", []), ast(number, "2", [])]), ast(power, none, [ast(identifier, "c", []), ast(number, "2", [])])])])])])])).
source_formula(p_w, 7, ast(limit, none, [ast(identifier, "v", []), ast(identifier, "c", [])])).
source_formula(p_w, 8, ast(limit, none, [ast(identifier, "dt'", []), ast(number, "0", [])])).
source_formula(p_w, 9, ast(limit, none, [ast(power, none, [ast(identifier, "dt'", []), ast(number, "2", [])]), ast(number, "0", [])])).
source_formula(p_w, 10, ast(limit, none, [ast(binary, "DIV", [ast(identifier, "dt'", []), ast(identifier, "dt", [])]), ast(number, "0", [])])).
formula_count(p_f2, 2).
source_formula(p_f2, 1, ast(binary, "EQ", [ast(identifier, "F", []), ast(binary, "PLUS", [ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])]), ast(binary, "MUL", [ast(number, "2", []), ast(identifier, "dt", [])])])])).
source_formula(p_f2, 2, ast(binary, "EQ", [ast(binary, "PLUS", [ast(power, none, [ast(identifier, "dt", []), ast(number, "2", [])]), ast(binary, "MUL", [ast(number, "2", []), ast(identifier, "dt", [])])]), ast(binary, "MUL", [ast(number, "2", []), ast(call, "dt", [ast(binary, "PLUS", [ast(number, "1", []), ast(binary, "MUL", [ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])]), ast(identifier, "dt", [])])])])])])).
formula_count(p_f3, 3).
source_formula(p_f3, 1, ast(binary, "EQ", [ast(identifier, "F", []), ast(binary, "MUL", [ast(number, "2", []), ast(call, "dt", [ast(binary, "PLUS", [ast(number, "1", []), ast(binary, "MUL", [ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])]), ast(identifier, "dt", [])])])])])])).
source_formula(p_f3, 2, ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])).
source_formula(p_f3, 3, ast(identifier, "F", [])).
formula_count(d_lap, 11).
source_formula(d_lap, 1, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "s", []), ast(sign, "PM", [])]), ast(binary, "PM", [ast(identifier, "a", []), ast(identifier, "ib", [])])])).
source_formula(d_lap, 2, ast(binary, "EQ", [ast(identifier, "a", []), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(d_lap, 3, ast(binary, "EQ", [ast(call, "T", [ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(binary, "MUL", [ast(binary, "PM", [ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(identifier, "lambda", [])])])).
source_formula(d_lap, 4, ast(binary, "EQ", [ast(power, none, [ast(identifier, "e", []), ast(unary, "PM", [ast(identifier, "ibT", [])])]), ast(number, "1", [])])).
source_formula(d_lap, 5, ast(binary, "EQ", [ast(identifier, "bT", []), ast(binary, "MUL", [ast(number, "2", []), ast(constant, "PI", [])])])).
source_formula(d_lap, 6, ast(binary, "EQ", [ast(call, "b", [ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(binary, "DIV", [ast(binary, "MUL", [ast(number, "2", []), ast(constant, "PI", [])]), ast(binary, "MUL", [ast(binary, "PM", [ast(identifier, "k", []), ast(identifier, "rho", [])]), ast(identifier, "lambda", [])])])])).
source_formula(d_lap, 7, ast(binary, "EQ", [ast(identifier, "rho", []), ast(number, "0", [])])).
source_formula(d_lap, 8, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "b", []), ast(identifier, "k", [])]), ast(binary, "DIV", [ast(binary, "MUL", [ast(number, "2", []), ast(constant, "PI", [])]), ast(binary, "MUL", [ast(identifier, "k", []), ast(identifier, "lambda", [])])])])).
source_formula(d_lap, 9, ast(binary, "EQ", [ast(subscript, none, [ast(identifier, "Z", []), ast(limit, none, [ast(identifier, "VED", []), ast(identifier, "Lap", [])])]), ast(set_builder, none, [ast(binary, "PM", [ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])]), ast(binary, "MUL", [ast(identifier, "i", []), ast(binary, "DIV", [ast(binary, "MUL", [ast(number, "2", []), ast(constant, "PI", [])]), ast(binary, "MUL", [ast(identifier, "k", []), ast(identifier, "lambda", [])])])])]), ast(binary, "IN", [ast(identifier, "k", []), ast(power, none, [ast(identifier, "N", []), ast(sign, "PLUS", [])])])])])).
source_formula(d_lap, 10, ast(subscript, none, [ast(identifier, "P", []), ast(identifier, "F3", [])])).
source_formula(d_lap, 11, ast(binary, "EQ", [ast(identifier, "c", []), ast(number, "1", [])])).
formula_count(p_lap_z, 4).
source_formula(p_lap_z, 1, ast(binary, "EQ", [ast(call, "Re", [ast(identifier, "s", [])]), ast(binary, "DIV", [ast(number, "1", []), ast(number, "2", [])])])).
source_formula(p_lap_z, 2, ast(subscript, none, [ast(identifier, "U", []), ast(identifier, "VED", [])])).
source_formula(p_lap_z, 3, ast(identifier, "k", [])).
source_formula(p_lap_z, 4, ast(identifier, "k", [])).
defines_set(d_f, u_rim_rho).
defines_set(d_f, u_ved_rho).
defines_set(d_rim, z_rim_nt).
uses_defined_set(d_rim, z_rim_nt).
uses_defined_set(d_f, u_rim_rho).
uses_defined_set(d_f, u_ved_rho).
uses_defined_set(d_finv, u_rim_rho).
uses_defined_set(d_finv, u_ved_rho).
uses_defined_set(t_iso, u_rim_rho).
uses_defined_set(t_iso, u_ved_rho).
uses_defined_set(p_rim_s, z_rim_nt).
uses_defined_set(p_z, z_rim_nt).
uses_defined_set(t_riemann, z_rim_nt).

fact(d_u).
fact(d_t_prime).
fact(a_l).
fact(d_lambda).
fact(d_l).
fact(d_k).
fact(d_rho).
fact(d_rim).
fact(d_rho_r).
fact(d_f).
fact(d_finv).
rule(p_coord, [d_u]).
rule(t_iso, [d_f, d_finv]).
rule(p_st, [p_coord, d_t_prime, a_l]).
rule(p_rho_iso, [t_iso]).
rule(p_v, [d_t_prime, a_l, p_st]).
rule(p_rim_s, [t_iso, p_rho_iso]).
rule(p_a, [a_l, p_st, p_v]).
rule(p_ved_inv, [p_a, d_lambda, d_l]).
rule(p_ved_e, [p_ved_inv, d_k, d_rho]).
rule(p_ved_i, [d_k, d_rho, p_ved_e]).
rule(p_vr_rho, [p_ved_e]).
rule(p_ved_k_e, [d_rho, p_ved_e, p_ved_i]).
rule(p_vr_e, [p_vr_rho]).
rule(p_ved_k_i, [p_ved_e, p_ved_i, p_ved_k_e]).
rule(p_z, [p_rim_s, p_vr_rho, p_vr_e]).
rule(p_ved_r_c, [p_ved_i, p_ved_k_e, p_ved_k_i]).
rule(t_riemann, [t_iso, p_rho_iso, p_rim_s, p_z, d_rho_r, p_vr_rho]).
rule(p_ved_completo, [p_ved_k_e, p_ved_k_i, p_ved_r_c]).
rule(p_vs, [p_ved_k_i, p_ved_r_c, p_ved_completo]).
rule(p_f, [p_ved_r_c, p_ved_completo, p_vs]).
rule(p_f1, [p_ved_completo, p_vs, p_f]).
rule(p_w, [p_vs, p_f, p_f1]).
rule(p_f2, [p_f, p_f1, p_w]).
rule(p_f3, [p_f1, p_w, p_f2]).
rule(d_lap, [p_f3]).
rule(p_lap_z, [p_f2, p_f3, d_lap]).

% ============================================================
% MOTOR DE DEMOSTRACION
% ============================================================

prove(Goal, fact(Goal), _) :-
    fact(Goal).

prove(Goal, proof(Goal, Proofs), Seen) :-
    \+ memberchk(Goal, Seen),
    rule(Goal, Dependencies),
    prove_all(Dependencies, Proofs, [Goal|Seen]).

prove_all([], [], _).

prove_all([Goal|Goals], [Proof|Proofs], Seen) :-
    prove(Goal, Proof, Seen),
    prove_all(Goals, Proofs, Seen).

% ============================================================
% RELACIONES DE DEPENDENCIA
% ============================================================

depends_on(Node, Dependency) :-
    rule(Node, Dependencies),
    member(Dependency, Dependencies).

depends_transitively(Node, Dependency) :-
    depends_transitively_(Node, Dependency, [Node]).

depends_transitively_(Node, Dependency, _Seen) :-
    depends_on(Node, Dependency).

depends_transitively_(Node, Dependency, Seen) :-
    depends_on(Node, Intermediate),
    \+ memberchk(Intermediate, Seen),
    depends_transitively_(
        Intermediate,
        Dependency,
        [Intermediate|Seen]
    ).

% ============================================================
% AUDITORIA GLOBAL DEL GRAFO
% ============================================================

implemented_node(Node) :-
    fact(Node).

implemented_node(Node) :-
    rule(Node, _).

graph_error(reference_not_declared(Node, Dependency)) :-
    depends_on(Node, Dependency),
    \+ declared_node(Dependency, _).

graph_error(unresolved_dependency(Node, Dependency)) :-
    unresolved_dependency(Node, Dependency).

graph_error(node_without_fact_or_rule(Node)) :-
    declared_node(Node, _),
    \+ implemented_node(Node).

graph_error(formula_coverage_mismatch(Node, Expected, Actual)) :-
    formula_count(Node, Expected),
    findall(Index, source_formula(Node, Index, _), Indices),
    length(Indices, Actual),
    Expected =\= Actual.

graph_error(self_dependency(Node)) :-
    depends_on(Node, Node).

graph_error(cyclic_dependency(Node)) :-
    declared_node(Node, _),
    depends_transitively(Node, Node).

graph_error(conflicting_node_types(Node, Kinds)) :-
    declared_node(Node, _),
    findall(
        Kind,
        declared_node(Node, Kind),
        RawKinds
    ),
    sort(RawKinds, Kinds),
    length(Kinds, Count),
    Count > 1.

node_definition(Node, fact) :-
    fact(Node).

node_definition(Node, rule(Dependencies)) :-
    rule(Node, Dependencies).

graph_error(conflicting_definitions(Node, Definitions)) :-
    implemented_node(Node),
    findall(
        Definition,
        node_definition(Node, Definition),
        RawDefinitions
    ),
    sort(RawDefinitions, Definitions),
    length(Definitions, Count),
    Count > 1.

% ============================================================
% ADVERTENCIAS ESTRUCTURALES
% ============================================================

graph_warning(redundant_declaration(Node, Kind)) :-
    declared_node(Node, Kind),
    findall(
        Kind,
        declared_node(Node, Kind),
        Declarations
    ),
    length(Declarations, Count),
    Count > 1,
    findall(
        OtherKind,
        declared_node(Node, OtherKind),
        RawKinds
    ),
    sort(RawKinds, [Kind]).

graph_warning(redundant_definition(Node, Definition)) :-
    node_definition(Node, Definition),
    findall(
        Definition,
        node_definition(Node, Definition),
        Definitions
    ),
    length(Definitions, Count),
    Count > 1,
    findall(
        OtherDefinition,
        node_definition(Node, OtherDefinition),
        RawDefinitions
    ),
    sort(RawDefinitions, [Definition]).

% ============================================================
% AUDITORIA DEL OBJETIVO
% ============================================================

goal_error(Goal, goal_not_declared(Goal)) :-
    \+ declared_node(Goal, _).

goal_error(Goal, missing_definition_dependency(Node, Provider, Symbol)) :-
    used_by_goal(Goal, Node),
    uses_defined_set(Node, Symbol),
    defines_set(Provider, Symbol),
    Node \= Provider,
    \+ depends_transitively(Node, Provider).

audit_graph(Goal) :-
    findall(
        Error,
        (graph_error(Error) ; goal_error(Goal, Error)),
        RawErrors
    ),
    sort(RawErrors, Errors),

    findall(
        Warning,
        graph_warning(Warning),
        RawWarnings
    ),
    sort(RawWarnings, Warnings),

    forall(
        member(Warning, Warnings),
        format(
            'AVISO ESTRUCTURAL: ~q~n',
            [Warning]
        )
    ),

    (
        Errors = []
    ->
        true
    ;
        format(
            'RESULTADO PROLOG: ARBOL INCOMPLETO~n',
            []
        ),
        format(
            'Errores estructurales del grafo:~n',
            []
        ),
        forall(
            member(Error, Errors),
            format('  - ~q~n', [Error])
        ),
        fail
    ).

% ============================================================
% COBERTURA DEDUCTIVA
% ============================================================

% Un nodo pertenece a la prueba del objetivo si es el propio
% objetivo o una dependencia transitiva del mismo.

used_by_goal(Goal, Goal).

used_by_goal(Goal, Node) :-
    depends_transitively(Goal, Node).

% Los nodos externos a la clausura del objetivo se conservan.
% No se consideran automaticamente errores.

outside_goal(Goal, Node) :-
    declared_node(Node, _),
    \+ used_by_goal(Goal, Node).

% Raiz de una rama externa:
% nodo externo que no es dependencia de otro nodo externo.

external_root(Goal, Node) :-
    outside_goal(Goal, Node),
    \+ (
        outside_goal(Goal, Other),
        Other \= Node,
        depends_on(Other, Node)
    ).

% ============================================================
% INFORME
% ============================================================

write_atoms([]).

write_atoms([Atom]) :-
    format('~w', [Atom]).

write_atoms([Atom|Atoms]) :-
    format('~w, ', [Atom]),
    write_atoms(Atoms).

write_clause(Node) :-
    fact(Node),
    !,
    format('  ~w.~n', [Node]).

write_clause(Node) :-
    rule(Node, Dependencies),
    format('  ~w :- ', [Node]),
    write_atoms(Dependencies),
    format('.~n', []).

write_external_branch(Goal, Root) :-
    findall(
        Node,
        (
            Node = Root
        ;
            depends_transitively(Root, Node)
        ),
        RawNodes
    ),
    sort(RawNodes, Nodes),
    include(outside_goal(Goal), Nodes, ExternalNodes),
    format('  Rama externa desde ~w: ', [Root]),
    write_atoms(ExternalNodes),
    format('~n', []).

write_report(Goal) :-
    findall(
        Node,
        used_by_goal(Goal, Node),
        RawUsed
    ),
    sort(RawUsed, Used),

    findall(
        Node,
        outside_goal(Goal, Node),
        RawOutside
    ),
    sort(RawOutside, Outside),

    findall(
        Root,
        external_root(Goal, Root),
        RawRoots
    ),
    sort(RawRoots, Roots),

    findall(
        Node,
        declared_node(Node, _),
        RawAll
    ),
    sort(RawAll, All),

    length(All, TotalCount),
    length(Used, UsedCount),
    length(Outside, OutsideCount),
    findall((Node, Index), source_formula(Node, Index, _), FormulaFacts),
    length(FormulaFacts, FormulaCount),

    format(
        'RESULTADO PROLOG: ARBOL COMPLETO~n',
        []
    ),
    format(
        'Objetivo alcanzable en el grafo: ~w~n',
        [Goal]
    ),
    format(
        'Nodos formales totales: ~d~n',
        [TotalCount]
    ),
    format('Formulas extraidas como hechos: ~d~n', [FormulaCount]),
    format(
        'Nodos de la clausura deductiva del objetivo: ~d~n',
        [UsedCount]
    ),

    (
        Outside = []
    ->
        format(
            'Nodos fuera de la clausura del objetivo: 0~n',
            []
        )
    ;
        format(
            'Nodos fuera de la clausura del objetivo: ~d~n',
            [OutsideCount]
        ),
        format(
            'Estos nodos NO se consideran errores por si mismos.~n',
            []
        ),
        format(
            'Pueden pertenecer a comprobaciones o ramas independientes.~n',
            []
        ),
        format(
            'Nodos externos: ~w~n',
            [Outside]
        )
    ),

    (
        Roots = []
    ->
        true
    ;
        format(
            'Raices de ramas externas al objetivo: ~w~n',
            [Roots]
        )
    ),

    format(
        'Cadena deductiva utilizada para el objetivo:~n',
        []
    ),
    forall(
        member(Node, Used),
        write_clause(Node)
    ).

% ============================================================
% EJECUCION
% ============================================================

go(Goal) :-
    audit_graph(Goal),
    (
        prove(Goal, _Proof, [])
    ->
        write_report(Goal)
    ;
        format(
            'RESULTADO PROLOG: ARBOL INCOMPLETO~n',
            []
        ),
        format(
            'No se pudo cerrar el arbol del objetivo: ~w~n',
            [Goal]
        ),
        fail
    ).

go :-
    goal(Goal),
    go(Goal).

:- initialization(
    (go -> halt(0) ; halt(1)),
    main
).