Synthesis of a joint graph with minimal number of edges: an algorithm formalization and a proof of correctness

This paper relates to machine learning of algebraic Bayesian networks (ABN).
The paper's aim is to describe an algorithm for synthesis of the secondary structure of algebraic Bayesian network as a joint graph. There is an additional constraint: the joint graph must have minimal number of edges. After the algorithm description, it’s analysis is done.
Next, we formalize input data, problem statement, and goal. Then we introduce definitions of joint graphs and weight of vertex, and later on definitions of specific elements of graph theory. Load, universal set of loads, and also the order of weights are introduced.
The last section gives a proof of the algorithm correctness. The first two statements prove that the algorithm builds a joint graph. The next two ones prove that the synthesized joint graph contains minimal number of edges.