G v7 v2        == G v4 (F v1 v1)      : #1
F v1 (G v7 v2) == v3                  : #2
v3             == F (H v5) (G v0 v6)  : #3 
v3             == v4                  : #4
v4             == F v1 v1             : #5