Session INF_NF

Theories

Fundamentals

• Ground_Terms
• Basic_Utils
• Tree_Automata_Utils
• Tree_Automata_Pumping

Saturation procedure

• Saturation

Infinity predicate

• RRn_Automata
• RR2_Infinite

Executable Q infinity construction

• RR2_infinite_Impl

Regularity of normal form predicate

• NF