About proving the algorithm

    Now I have to think about the method to prove the correctness of the algorithm. In this case, I need to show that the algorithm must satisfies two important things, the first one is the ability to produce a correct g'-expression and the second one is that it must be a primitive function.
    What is the ability to produce a correct g'-expression? What is the correctness of algorithm? It must have the same result as applying 2 different stages which means applying g-extend-expression on db and then applying f for that result.
          Currently, the new function runs correctly with 3 test cases. But it failed in the special case: using 1 variable in the template of f and using the same 2 variables in template of f with 1 variable in pattern (I didn't test in the later case).
    About the primitive function, I have to implement the function again so that it can process the graph in variable form, and then it can reuse the graph operators in the current system.
           I need to think about the example in this case.
           Think about the combination - or nested - or reuse some graph operators.
           Then implement a new function (primitive function).