Assumption doesn't hold true currently

With Sat states only treated like other states in the second fixpoint
iteration, the outer fixpoint was not ncessarily monononously decreasing
causing wrong results when in the first round the same number of nodes
got removed as added due to sat states.

Acceptance test for cores is ∃ which is safe to use when non or only
some child states are created tus far

Should actually happen when the State changes from `Expandable` to
`Open` and trigger the propagateSatMu but for now just do it in
propagateSatMu so we can observe the algorithm working.

Not only finishing cycles but also plain sat nodes may cause a node to
be satisfiable

Only finishing nodes with enough Open / Sat children are to be
considered as startingpoints

Also accept already Satisfiable nodes when finding paths

This still produces wrong results: It assumes every node with empty
focus to be sat.

This makes the identifying information be of type bset*bset instead of
bset and adds tracking of deferrals for propositional reasoning and --
in case of K -- for modal reasoning

Now one step in the debugger removes exactly one element from the queue
(if it's not empty). If this action empties the queue, nominals are
propagated.

This fixes an assertion that failed for the PML+K formula

   sat "({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"

which is satisfiable.

Introduce a new generic data type lazylist, e.g. used for lazy rule
enumerations.

Propagation of satisfiability and unsatisfiability does not cover
disjunctions and I don't get how propagation works, so I won't touch it
yet. So this reverts the only partially implemented Disjunctive
ruleEnumerations,