... Q [Q] loop ... False [Q] loop ------------------------ ...
Gentzen diagram.
if not basis.
if basis