-
Notifications
You must be signed in to change notification settings - Fork 1
/
preamble.tex
21 lines (18 loc) · 1.14 KB
/
preamble.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
This is the proof report generated by the automated prover.
The document contains, in order, the following
\begin{itemize}
\item A list of the templates the were given as input to the prover.
\item For each square in each template, a report giving the output of the proof
for that particular square.
\item For each square on the boundary of the template ``X-Full Boundary'', a
report giving the output of the boundary proof for that square. Squares that are
on multiple boundaries will have one report for each side that they touch.
\end{itemize}
Each square that was checked was assigned a number, and for easy referencing, in the drawing for each
template the number of each square is displayed. If a square's number is black,
then this indicates that the automated proof verified that the lemma holds for particular square,
whereas if a square's number is red, then this indicates that the automated
proof falsified the lemma for that particular square.
It can be verified that the red squares appear only at the starts and ends of
PPAD lines, as well as at solutions in the PLS labyrinth, which is exactly where
we expect solutions of the instances to be.