The file yv.mol represents Yv K, where K=Lg.Lx.M(g,x). In the mol file M(g,x)=gx, so M is a node A, but it can be any A-FO graph instead (i.e. it satisfies the property that when connected to a FO node it reduces eventually as an A node, described in [1] as a "distributor" of the type A).
The file kyvk.mol represents K(Yv K).
The algorithm has been run in the deterministic regime (i.e. all wei_*=0; ).
It proves visually the theorem 5.1 by showing that both graphs (yv.mol and kyvk.mol) reduce to the same graph.
The reduction of yv.mol is this. You may click and drag the nodes.
The reduction of kyvk.mol is this. Click and drag the nodes to move the end graph so that it is visibly the same as the previous one.
The interpretation is that if we assume that M behaves like an A distributor graph and if we suppose that if the reduction of M is "canned" in one step as a DIST-A move, then Y_v K and K(Y_v K) reduce both to the same graph, so they are equivalent in the sense that if the reduction of any of these graphs is "canned" (as a single reduction step), then it results in the same graph.
yv.mol:
A yv a1 out ,
L a2 ag a1 ,
L al ax a2 ,
A ag ax al ,
L 1 f yv ,
L 2 x 1 ,
A 3 4 2 ,
FO f f1 f2 ,
L 5 g1 3 ,
A f1 6 5 ,
L 7 x1 6 ,
A 8 x1 7 ,
A 9 10 8 ,
FO g1 9 10 ,
A 11 x 4 ,
L 12 g2 11 ,
A f2 13 12 ,
L 14 x2 13 ,
A 15 x2 14 ,
A 16 17 15 ,
FO g2 16 17
kyvk.mol:
A yv a12 outi ,
A a11 outi out ,
FO a1 a11 a12 ,
L a2 ag a1 ,
L al ax a2 ,
A ag ax al ,
L 1 f yv ,
L 2 x 1 ,
A 3 4 2 ,
FO f f1 f2 ,
L 5 g1 3 ,
A f1 6 5 ,
L 7 x1 6 ,
A 8 x1 7 ,
A 9 10 8 ,
FO g1 9 10 ,
A 11 x 4 ,
L 12 g2 11 ,
A f2 13 12 ,
L 14 x2 13 ,
A 15 x2 14 ,
A 16 17 15 ,
FO g2 16 17
