# Theory FL_Formula

theory FL_Formula
imports
Nominal_Bounded_Set
Nominal_Wellfounded
Residual
FL_Transition_System
begin
section ‹Infinitary Formulas With Effects›
subsection ‹Infinitely branching trees›
text ‹First, we define a type of trees, with a constructor~@{term tConj} that maps (potentially
infinite) sets of trees into trees. To avoid paradoxes (note that there is no injection from the
powerset of trees into the set of trees), the cardinality of the argument set must be bounded.›
text ‹The effect consequence operator~‹⟨f⟩› is always and only used as a prefix to a
predicate or an action formula. So to simplify the representation of formula trees with effects, the
effect operator is merged into the predicate or action it precedes.›