Library ATBR.Common

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

Library ATBR.MyFSets

Library ATBR.MyFSetProperties

Library ATBR.MyFMapProperties

• Destructor for find

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.Utils_WF

Library ATBR.Force

Library ATBR.DisjointSets

Library ATBR.Classes

• Graph : base class of the hierarchy
• Operations
• Structures
• Dual structures

Library ATBR.Reification

Library ATBR.Functors

Library ATBR.Graph

Library ATBR.SemiLattice

Library ATBR.Monoid

Library ATBR.SemiRing

Library ATBR.KleeneAlgebra

Library ATBR.Converse

Library ATBR.Model_Relations

Library ATBR.Model_StdRelations

Library ATBR.Model_Languages

Library ATBR.Model_RegExp

Library ATBR.Model_MinPlus

Library ATBR.StrictStarForm

Library ATBR.MxGraph

Library ATBR.MxSemiLattice

Library ATBR.MxSemiRing

Library ATBR.MxKleeneAlgebra

Library ATBR.MxFunctors

Library ATBR.DKA_Definitions

Library ATBR.DKA_StateSetSets

Library ATBR.DKA_CheckLabels

Library ATBR.DKA_Construction

Library ATBR.DKA_Epsilon

Library ATBR.DKA_Determinisation

Library ATBR.DKA_Merge

Library ATBR.DKA_DFA_Language

Library ATBR.DKA_DFA_Equiv

Library ATBR.DecideKleeneAlgebra

Library ATBR.StrictKleeneAlgebra

Library ATBR.ATBR

Library ATBR.ATBR_Matrices

Library ATBR.Examples

• Examples about uses of the ATBR library
  • Setting
  • Decision tactics
    • Rewriting tactics
  • Examples about matrices
  • Using concrete structures

Library ATBR.ChurchRosser

Library ATBR.ChurchRosser_Points_vs_Algebraic

• Standard proof: binary relations relate points to points
• Algebraic proof, using standard properties of binary relations