This is a detailed WWW representation of the KIV project VerifyThis3 with specifications, theorems, and proofs.
You should begin with a look at the specification graph to get an overview over the specifications and their structure. From there you can browse the individual specifications and then the proofs.
The project statistic contains information about the number of theorems, proofs, proof steps, user interactions, etc.
The formulas use logical symbols like and, or, always, quantifiers, and mathematical symbols like empty set, union etc. To check which symbols are available in your browser you can take a look at the KIV symbols.
The meaning of colors in proof trees is explained here.
The development graph on the right hand side gives an overview of all specifications used in the project and their dependencies. Green specifications are defined in the current project and have completed proofs for all defined theorems. Orange specifications are imported from another project (typically a library). To view the details of a specification click the corresponding link on the left hand side.
Project VerifyThis3
Library
|  |