Session Partial_Order_Reduction

Theories

• HOL-Library.Prefix_Order
• List_Prefixes
• List_Extensions
• Word_Prefixes
• Set_Extensions
• Basic_Extensions
• Relation_Extensions
• Transition_System_Extensions
• Traces
• Transition_System_Traces
• Stuttering_Equivalence.Samplers
• Stuttering_Equivalence.StutterEquivalence
• HOL-Library.Case_Converter
  • File ‹case_converter.ML›
• HOL-Library.Simps_Case_Conv
  • File ‹simps_case_conv.ML›
• HOL-Library.Complete_Partial_Order2
• Coinductive.Coinductive_Nat
• Coinductive.Coinductive_List
• Coinductive.Coinductive_List_Prefix
• Coinductive.Coinductive_Stream
• Functions
• ENat_Extensions
• CCPO_Extensions
• ESet_Extensions
• Coinductive_List_Extensions
• LList_Prefixes
• Stuttering
• Transition_System_Interpreted_Traces
• Ample_Abstract
• LTL.LTL
• Stuttering_Equivalence.PLTL
• Formula
• Ample_Correctness
• Ample_Analysis