Library ATBR.ChurchRosser_Points_vs_Algebraic
- Standard proof: binary relations relate points to points
- Algebraic proof, using standard properties of binary relations
Library ATBR.ChurchRosser
Library ATBR.Examples
Library ATBR.ATBR_Matrices
Library ATBR.ATBR
Library ATBR.StrictKleeneAlgebra
Library ATBR.DecideKleeneAlgebra
Library ATBR.DKA_DFA_Equiv
Library ATBR.DKA_DFA_Language
Library ATBR.DKA_Merge
Library ATBR.DKA_Determinisation
Library ATBR.DKA_Epsilon
Library ATBR.DKA_Construction
Library ATBR.DKA_CheckLabels
Library ATBR.DKA_StateSetSets
Library ATBR.DKA_Definitions
Library ATBR.MxFunctors
Library ATBR.MxKleeneAlgebra
Library ATBR.MxSemiRing
Library ATBR.MxSemiLattice
Library ATBR.MxGraph
Library ATBR.StrictStarForm
Library ATBR.Model_MinPlus
Library ATBR.Model_RegExp
Library ATBR.Model_Languages
Library ATBR.Model_StdRelations
Library ATBR.Model_Relations
Library ATBR.Converse
Library ATBR.KleeneAlgebra
Library ATBR.SemiRing
Library ATBR.Monoid
Library ATBR.SemiLattice
Library ATBR.Graph
Library ATBR.Functors
Library ATBR.Reification
Library ATBR.Classes
Library ATBR.DisjointSets
Library ATBR.Force
Library ATBR.Utils_WF
Library ATBR.Numbers
- The NUM interface
- Notations, lemmas and tactics derivable from the NUM interface
- num_analyse : destroys the boolean expressions
- num_prop : transforms atoms like leb x y = true into le x y
- num_omega : injects every prop about nums into equivalent props about nats, then call omega
- Instance of NUM with positive as base type
Library ATBR.MyFMapProperties
Library ATBR.MyFSetProperties
Library ATBR.MyFSets
Library ATBR.BoolView
- bool_simpl is a tactic that simplifies boolean operations in the context and in the goal
- bool_connectors takes hypothesis like ((x && y) || negb z) = true and transforms them into