Generating all possible PdlRule applications

Similar to LocalTableau.all, this is needed to define BuildTree as a finite tree.

def PDL.PdlRule.all (X : Sequent) : List ((Y : Sequent) × PdlRule X Y)

List of all PdlRules applicable to X. Code is based on part of theMoves. This is also similar to the definitions in LocalAll.lean.

Equations

• One or more equations did not get rendered due to their size.
• PDL.PdlRule.all X = []

theorem PDL.PdlRule.all_spec {X Y : Sequent} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈ all X

Specification that PdlRule.all is complete, almost: we demand X.basic here which is not part of the PdlRule type, but demanded by Tableau.pdl.