mb automata 3 Sections GenAutomata Doc

Def closed_pred(p) == r:rel(). r p closed_rel(r)

is mentioned by

Thm* Q:Fmla. closed_pred((Q)') closed_pred(Q)[closed_pred_addprime]

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc