if (head.equals("+")) return plus((ElementNode)walk(t.child(0)));
if (head.equals("++/")) return plusmaxfollow((ElementNode)walk(t.child(0)), (ElementNode)walk(t.child(1)));
if (head.equals("+/")) return plusfollow((ElementNode)walk(t.child(0)), (ElementNode)walk(t.child(1)));
if (head.equals("+")) return plus((ElementNode)walk(t.child(0)));
if (head.equals("++/")) return plusmaxfollow((ElementNode)walk(t.child(0)), (ElementNode)walk(t.child(1)));
if (head.equals("+/")) return plusfollow((ElementNode)walk(t.child(0)), (ElementNode)walk(t.child(1)));