menu

Return to entry

Introduction
Process
Constant_Processes
Deterministic_Choice
Non_Deterministic_Choice
Sliding_Choice
Multi_Deterministic_Prefix_Choice
Multi_Non_Deterministic_Prefix_Choice
Global_Non_Deterministic_Choice
Sequential_Composition
Synchronization_Product
Renaming
Hiding
CSP_Refinements
CSP_Monotonies
Non_Deterministic_CSP_Distributivity
Basic_CSP_Laws
Step_CSP_Laws
Step_CSP_Laws_Extended
Read_Write_CSP_Laws
CSP_Laws
Events_Ticks_CSP_Laws
CSP_Assertions
Induct_CSP_Rules
HOL-CSP
Conclusion
CopyBuffer
MergeAnomaly

HOL-CSP.Induct_CSP_Rules

HTML Presentation