Proving the correctness

        Until this time, I just recognize the complexity of proving the correctness of the algorithm. Actually, I don’t know how to prove the correctness of the algorithm over the database. The database is set up with 9 graph constructors, so I should prove over those cases (9 cases). However, currently, I just consider those cases of the graph constructors {}, (), $var and {l:G}. Moreover, I need to prove in 2 approaches.
        First, the g-extend expression affects to the source. In this case, I will consider many cases:

1. Use values only (Don’t use variables in the g-extend expression).
2. Use many variables. In this case, the g-extend expression will contains many variables in many levels, so in this case, the result g’-extend will contains WHERE-part corresponding to the variables in the g-extend expression.        

        Second, the g-extend expression doesn’t affect to the source, in those cases, the g’-extend expression just simply produce the update nothing to the current view.
        The technique using in the algorithm is tree-matching. Base on the tree-pattern of the f-select expression which contains template-tree and graph-pattern-tree, with the g-extend expression which contains template-tree-1, template-tree-2 and graph-pattern-tree also.
        The tree-matching is used to find out the matched pattern, and the corresponding variables which match with the pattern.


Fig 1. The result-trees after applying the tree-matching function.


Fig 2. The variables trees are extracted from the result-trees in Fig 1.

Fig 3. Replace the variables in the f-template-tree with the extracted-trees