Adding Proof using annotations almost everywhere.
Thanks to Proofgeneral which insert them automatically.
Showing
- CaseStudies/Gathering/Definitions.v 5 additions, 5 deletionsCaseStudies/Gathering/Definitions.v
- CaseStudies/Gathering/InR2/Algorithm.v 93 additions, 90 deletionsCaseStudies/Gathering/InR2/Algorithm.v
- CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v 27 additions, 27 deletionsCaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
- CaseStudies/Gathering/InR2/Peleg.v 35 additions, 34 deletionsCaseStudies/Gathering/InR2/Peleg.v
- CaseStudies/Gathering/InR2/Viglietta.v 14 additions, 14 deletionsCaseStudies/Gathering/InR2/Viglietta.v
- Core/Configuration.v 22 additions, 22 deletionsCore/Configuration.v
- Core/Formalism.v 44 additions, 42 deletionsCore/Formalism.v
- Core/Identifiers.v 27 additions, 27 deletionsCore/Identifiers.v
- Models/ContinuousGraph.v 29 additions, 29 deletionsModels/ContinuousGraph.v
- Models/Flexible.v 2 additions, 2 deletionsModels/Flexible.v
- Models/GraphEquivalence.v 6 additions, 6 deletionsModels/GraphEquivalence.v
- Models/RigidFlexibleEquivalence.v 18 additions, 18 deletionsModels/RigidFlexibleEquivalence.v
- Models/Similarity.v 8 additions, 8 deletionsModels/Similarity.v
- Observations/LimitedMultisetObservation.v 5 additions, 5 deletionsObservations/LimitedMultisetObservation.v
- Observations/MultisetObservation.v 21 additions, 21 deletionsObservations/MultisetObservation.v
- Observations/PreCompositionObservation.v 0 additions, 1 deletionObservations/PreCompositionObservation.v
- Spaces/EuclideanSpace.v 34 additions, 34 deletionsSpaces/EuclideanSpace.v
- Spaces/Isomorphism.v 10 additions, 10 deletionsSpaces/Isomorphism.v
- Spaces/R2.v 187 additions, 187 deletionsSpaces/R2.v
- Spaces/RealNormedSpace.v 29 additions, 29 deletionsSpaces/RealNormedSpace.v
Loading
Please register or sign in to comment