+ private boolean destroyed = false;
+ public boolean check() {
+ boolean dead = true;
+ // - all nodes must have a parent
+ // - non-doomed nodes must either:
+ // - be on the frontier or
+ // - have a non-doomed node closer to the frontier than themself
+
+ if (phase.isFrontier()) dead = false;
+ for(Result r : children)
+ if (state.doomed) { if (r.usedByAnyNode()) dead = false; }
+ else { if (r.usedByNonDoomedNode()) dead = false; }
+ dead |= results.size()==0;
+ if (!dead || destroyed) return dead;
+ destroyed = true;
+ while(children.size()>0)
+ for(Result r : children) {
+ children.remove(r);
+ r.destroy();
+ break;
+ }
+ while(results.size()>0)
+ for(Result r : results) {
+ results.remove(r);
+ r.removeChild(this);
+ r.check();
+ break;
+ }
+ return dead;
+ }
+