extreme cases, $\mathrm{IoU}=0.00$ implies the smallest detection set with no
overlapping detections and $\mathrm{IoU}=1.00$ corresponds to the largest
detection set, practically without NMS. Similar to AP, oLRP Error can be used
to tune IoU threshold of NMS, set to $0.50$ as default (Table A.15).

NMS-free methods. As a different set of methods, recently proposed attention-
based visual detectors do not require NMS. Table A.16 presents oLRP Error can
also properly rank these NMS-free visual detectors, i.e. DETR [57], Sparse
R-CNN [58] and Deformable DETR [59] with the same R50 backbone.

TABLE A.15: Tuning IoU threshold of NMS on Faster R-CNN+R50. For both AP and oLRP Error, IoU=0.50 is chosen as the best IoU threshold (underlined).  |  AP $\uparrow$ |  oLRP Error $\downarrow$
---|---|---
IoU | AP | $\mathrm{AP_{50}}$ | $\mathrm{AP_{75}}$ | oLRP | $\mathrm{oLRP_{Loc}}$ | $\mathrm{oLRP_{FP}}$ | $\mathrm{oLRP_{FN}}$
0.00 | $33.3$ | $50.8$ | $36.6$ | $71.5$ | $17.2$ | $26.0$ | $51.4$
0.25 | $36.5$ | $56.9$ | $39.8$ | $69.4$ | $17.5$ | $27.5$ | $46.3$
0.50 | $37.8$ | $58.6$ | $41.0$ | $69.1$ | $17.5$ | $27.5$ | $45.4$
0.75 | $36.0$ | $53.3$ | $40.7$ | $72.5$ | $17.3$ | $31.7$ | $51.6$
0.90 | $27.6$ | $38.2$ | $31.7$ | $79.8$ | $16.1$ | $47.8$ | $61.7$
1.00 | $11.2$ | $14.8$ | $12.7$ | $90.5$ | $14.3$ | $76.2$ | $75.9$
TABLE A.16: Evaluating NMS-free methods.  |  AP $\uparrow$ |  oLRP $\downarrow$
---|---|---
Method | AP | $\mathrm{AP_{50}}$ | $\mathrm{AP_{75}}$ | oLRP | $\mathrm{oLRP_{Loc}}$ | $\mathrm{oLRP_{FP}}$ | $\mathrm{oLRP_{FN}}$
DETR | $40.1$ | $60.6$ | $42.0$ | $66.8$ | $17.1$ | $23.5$ | $43.9$
Sp. R-CNN | $45.0$ | $64.1$ | $48.9$ | $63.6$ | $14.6$ | $24.1$ | $41.6$
DDETR | $46.8$ | $66.3$ | $50.7$ | $62.1$ | $14.3$ | $24.5$ | $39.0$

###  G.2 Effect of performance aspects on LRP Error

In order to provide more insight on LRP Error, this section investigates the
effect of the performance aspects (i.e. localisation error, false positive
rate and false negative rate) on LRP Error using Panoptic FPN. In Table A.17,
we gradually remove the errors originating from each performance aspect and
then present the resulting error. Note that (i) the localisation errors
contribute to LRP Error after a normalisation by $1-\tau$ (Eq. (3)) and
$\tau=0.50$ in this case, and (ii) Number of TPs, FPs and FNs will also have
an effect on the error besides the component values (Eq. 3). Still, we can
deduce that (i) removing the errors originating from a performance measure
decreases LRP Error and it decreases the most when the errors of FN rate is
removed since $\mathrm{LRP_{FN}}$ is the largest error, (ii) Removing two
components decreases LRP Error more than removing one component, and (iii)
Once all errors are removed, as expected, LRP Error decreases to $0$, i.e. the
detection and the ground truth sets are equal.

TABLE A.17: Effect of performance aspects on LRP Error on COCO dataset (with COCO-stuff). We use Panoptic FPN+R50 trained for 12 epochs. ✓: We keep the performance aspect as it is, ✗: We remove the errors originating from the performance aspect.  Performance Aspects | LRP | $\mathrm{LRP_{Loc}}$ | $\mathrm{LRP_{FP}}$ | $\mathrm{LRP_{FN}}$
---|---|---|---|---
Loc. Error | FP rate | FN rate
✓ | ✓ | ✓ | $77.5$ | $21.0$ | $39.3$ | $57.2$
✗ | ✓ | ✓ | $64.9$ | $0.0$ | $39.3$ | $57.2$
✓ | ✗ | ✓ | $72.8$ | $21.0$ | $0.0$ | $57.2$
✓ | ✓ | ✗ | $62.4$ | $21.0$ | $39.3$ | $0.0$
✓ | ✗ | ✗ | $42.0$ | $21.0$ | $0.0$ | $0.0$
✗ | ✓ | ✗ | $39.3$ | $0.0$ | $39.3$ | $0.0$
✗ | ✗ | ✓ | $57.2$ | $0.0$ | $0.0$ | $57.2$
✗ | ✗ | ✗ | $0.0$ | $0.0$ | $0.0$ | $0.0$

###  G.3 A Use-Case of LRP-Optimal Thresholds in Video Object Detection

Related Work on Setting the thresholds of the classifiers. Employing visual
detectors for a practical application requires a confidence threshold that
balances precision, recall and localisation performance since, otherwise, the
resulting output would be dominated by several false positives with low
confidence scores. However, this topic has not received much attention from
the research community and is usually handled by practitioners in a problem or
deployment-specific manner. Conventionally, the thresholds of classifiers are
set by finding the optimal F-measure on the PR curve or G-mean on the receiver
operating characteristics curve, which do not consider localisation quality.
Prior work on setting the classifier thresholds focused on the probabilistic
models [60, 61]. Parambath et al. [62] present a theoretical analysis of the
F-measure, and propose a practical algorithm discretizing the confidence
scores in order to search for the optimal F-measure. Currently, for object
detection, a general single threshold is used for all classes instead of
class-specific thresholds [27].

The Experimental Setup. Here, we demonstrate a use-case where oLRP Error helps
us to set class-specific optimal thresholds as an alternative to the naive
approach of using a general, class-independent threshold. To this end, we
develop a simple, online video object detection framework where we use an off-
the-shelf still-image object detector (RetinaNet-50 [32] trained on COCO [1])
and built three different versions of the video object detector. The first
version, denoted with $B$, uses the still-image object detector to process
each frame of the video independently. The second and third versions, denoted
with $G$ and $S$, respectively, again use the still-image object detector to
process each frame and in addition, they link bounding boxes across subsequent
frames using the Hungarian matching algorithm [12] and update the scores of
these linked boxes using a simple Bayesian rule (details of this simple online
video object detector is given below). For the sake of efficiency in
linking888Note that Hungarian matching has a time complexity of
$\mathcal{O}(N^{3})$ and RetinaNet can output thousands of detections without
any thresholding., both of these detectors discard the low-precision
detections. Accordingly, the only difference between $G$ and $S$ is that while
$G$ uses a validated threshold of $0.50$ (see Fig. 11(a) in the paper to
notice that the LRP-Optimal threshold distribution of RetinaNet has a mean
around $0.50$) as the confidence score threshold for all classes, $S$ uses
LRP-Optimal threshold per class. We test these three detectors on 346 videos
of ImageNet VID validation set [2] for 15 object classes which also happen to
be included in COCO.

Details of the Online Video Object Detectors. There are two online video
object detectors: $G$ and $S$ which respectively use the general, class-
independent thresholding approach with $0.50$ as threshold and the class-
specific thresholds. For each of the online detectors, at each time interval,
the detections from the previous and current frames are associated using the
Hungarian algorithm [12] considering a box linking function and the confidence
scores of associated BBs of the current frame are updated using the score
distributions from both frames. Since an online tracker, specifically [63], is
also used in our method, we use the L1 norm of the difference of confidence
score distributions of neighbouring frames and the IoU overlap of the tracker
prediction and the detection at current frame. While choosing this box linking
function, we inspired from the tube linking score of [26]. The updated score
is estimated using the Bayes Theorem such that the prior is the updated
tubelet score in the previous frame and likelihood is the currently associated
high confidence detection with that tubelet. In such an update method, even
though the updated scores converge to $1$ quickly, which is harmful for lower
recall, precision improves in larger recall portions. Also, we call a BB as
“dominant object” if its updated score increases by $0.20$. In order to
increase the recall, the disappearance of a “dominant object” is closely
inspected by using the tracker again to predict the possible location, then
the cropped region is classified by class-wise binary classifiers (object vs.
background).

TABLE A.18: Comparison among $B$, $G$, $S$ with respect to AP & oLRP Error and their best class-specific configurations. The mean of class thresholds are assigned as N/A since the thresholds are set class-specific and the mean is not used. $s^{*}$ denotes the LRP-Optimal thresholds. Note that unlike AP, lower scores are better for LRP Error. |  Method |  airplane |  bicycle |  bird |  bus |  car |  cow |  dog |  cat |  elephant |  horse |  motorcycle |  sheep |  train |  boat |  zebra |  mean
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$\mathrm{AP_{50}}$ | B | $\mathbf{68.1}$ | $\mathbf{63.0}$ | $\mathbf{54.7}$ | $\mathbf{56.5}$ | $\mathbf{55.5}$ | $\mathbf{58.7}$ | $\mathbf{46.3}$ | $\mathbf{60.1}$ | $\mathbf{66.1}$ | $\mathbf{47.3}$ | $\mathbf{60.2}$ | $\mathbf{56.1}$ | $\mathbf{71.3}$ | $\mathbf{82.9}$ | $\mathbf{81.6}$ | $\mathbf{61.9}$
G | $62.1$ | $44.5$ | $49.2$ | $39.8$ | $41.7$ | $51.0$ | $41.6$ | $56.8$ | $58.8$ | $44.1$ | $57.1$ | $54.7$ | $60.0$ | $76.9$ | $76.5$ | $54.4$
S | $64.5$ | $53.5$ | $50.0$ | $48.5$ | $41.9$ | $49.2$ | $43.4$ | $56.9$ | $58.9$ | $44.4$ | $57.3$ | $54.5$ | $60.9$ | $79.2$ | $78.2$ | $56.1$
oLRP | B | $62.7$ | $77.6$ | $71.8$ | $70.2$ | $75.9$ | $69.2$ | $72.8$ | $70.0$ | $62.5$ | $72.3$ | $69.2$ | $67.7$ | $\mathbf{58.3}$ | $59.4$ | $43.6$ | $66.9$
G | $60.6$ | $78.3$ | $69.1$ | $72.7$ | $\mathbf{75.8}$ | $67.9$ | $71.4$ | $\mathbf{69.7}$ | $61.4$ | $\mathbf{69.9}$ | $\mathbf{65.4}$ | $\mathbf{64.8}$ | $58.6$ | $55.3$ | $43.2$ | $65.6$
S | $\mathbf{60.3}$ | $\mathbf{76.2}$ | $\mathbf{68.7}$ | $\mathbf{68.8}$ | $75.9$ | $\mathbf{67.8}$ | $\mathbf{71.2}$ | $\mathbf{69.7}$ | $\mathbf{61.3}$ | $70.1$ | $65.5$ | $64.9$ | $\mathbf{58.3}$ | $\mathbf{55.1}$ | $\mathbf{42.5}$ | $\mathbf{65.1}$
$\mathrm{oLRP_{Loc}}$ | B | $18.2$ | $27.1$ | $16.9$ | $17.7$ | $20.7$ | $14.5$ | $16.6$ | $20.3$ | $17.0$ | $15.5$ | $19.2$ | $15.4$ | $15.9$ | $19.9$ | $12.8$ | $17.9$
G | $18.1$ | $25.8$ | $17.0$ | $16.0$ | $20.7$ | $15.1$ | $16.5$ | $20.0$ | $17.0$ | $16.0$ | $19.5$ | $15.5$ | $15.6$ | $19.5$ | $12.8$ | $17.7$
S | $18.6$ | $27.0$ | $17.0$ | $17.3$ | $20.7$ | $14.8$ | $17.0$ | $20.0$ | $17.0$ | $16.0$ | $19.4$ | $15.5$ | $15.9$ | $19.7$ | $13.1$ | $17.9$
$\mathrm{oLRP_{FP}}$ | B | $8.0$ | $22.8$ | $30.0$ | $20.3$ | $30.3$ | $22.4$ | $24.2$ | $24.8$ | $9.5$ | $24.6$ | $15.8$ | $14.1$ | $9.9$ | $16.3$ | $3.4$ | $18.4$
G | $8.6$ | $11.6$ | $17.4$ | $13.7$ | $31.1$ | $21.8$ | $22.9$ | $27.9$ | $7.1$ | $22.1$ | $4.9$ | $7.8$ | $9.1$ | $7.7$ | $1.6$ | $14.2$
S | $8.7$ | $22.6$ | $18.4$ | $19.3$ | $32.0$ | $18.2$ | $26.9$ | $28.3$ | $7.5$ | $23.1$ | $8.4$ | $7.8$ | $11.0$ | $8.9$ | $3.0$ | $16.3$
$\mathrm{oLRP_{FN}}$ | B | $38.3$ | $42.7$ | $47.8$ | $47.7$ | $49.9$ | $50.4$ | $53.3$ | $39.4$ | $39.5$ | $54.0$ | $44.8$ | $49.4$ | $34.4$ | $22.4$ | $22.0$ | $42.4$
G | $35.9$ | $52.3$ | $48.0$ | $57.1$ | $49.3$ | $47.3$ | $51.2$ | $37.2$ | $38.8$ | $49.4$ | $41.5$ | $46.7$ | $36.0$ | $22.1$ | $22.7$ | $42.4$
S | $32.6$ | $38.9$ | $48.9$ | $46.1$ | $48.8$ | $49.0$ | $48.0$ | $36.9$ | $38.5$ | $49.3$ | $40.6$ | $46.8$ | $33.9$ | $20.3$ | $20.2$ | $39.8$
$s^{*}$ | B | $0.38$ | $0.31$ | $0.44$ | $0.27$ | $0.49$ | $0.61$ | $0.42$ | $0.49$ | $0.49$ | $0.52$ | $0.45$ | $0.51$ | $0.41$ | $0.45$ | $0.31$ | N/A
G | $0.00$ | $0.69$ | $0.97$ | $0.68$ | $0.00$ | $0.96$ | $0.48$ | $0.70$ | $0.33$ | $0.64$ | $0.60$ | $0.84$ | $0.59$ | $0.90$ | $0.00$ | N/A
S | $0.00$ | $0.54$ | $0.98$ | $0.45$ | $0.00$ | $0.91$ | $0.49$ | $0.64$ | $0.39$ | $0.58$ | $0.63$ | $0.85$ | $0.55$ | $0.89$ | $0.54$ | N/A
Figure A.13: Example PR curves of the methods on three example classes.
Optimal PR pairs are marked with crosses. Using a LRP-Optimal threshold
balances FP and FN errors resulting in a stretched PR curve either in recall
(e.g.(a)) or precision (e.g.(b)) axis depending on the chosen general
threshold. Furthermore, using AP for these pruned PR curves does not provide
consistent performance evaluation.

AP vs. oLRP Error for Video Object Detection: We compare $G$ with $B$ in order
to represent the evaluation perspectives of AP and oLRP Error – see Fig. A.13
and Table A.18. Since $B$ is a conventional object detector, with conventional
PR curves as illustrated in Fig. A.13. On the other hand, in order to be
faster, $G$ ignores some of the detections causing its maximum recall to be
less than that of $B$. Thus, these shorter ranges in the recall set a big
problem in the evaluation with respect to AP. Quantitatively, $B$ surpasses
$G$ by $7.5\%$ AP. On the other hand, despite limited recall coverage, $G$
obtains higher precision than $B$ especially through the end of its PR curve.
To illustrate, for the “boat” class in Fig. A.13, $G$ has significantly better
precision after approximately between $0.5$ and $0.9$ recall even though its
AP is lower by $6\%$. Since oLRP Error compares methods concerning their best
configurations, this difference is clearly addressed comparing their oLRP
Error in which $G$ surpasses $S$ by $4.1\%$. Furthermore, the superiority of
$G$ is shown to be its higher precision since FN components of $G$ and $S$ are
very close while FP component of $G$ is $8.6\%$ better, which is also the
exact difference of precisions in their peaks of PR curves.

Therefore, while $G$ seems to have very low performance in terms of AP, for 12
classes $G$ reaches better peaks than $B$ as illustrated by the oLRP Errors in
Table A.18. This suggests that oLRP Error is better than AP in capturing the
performance details of this kind methods that uses thresholding.

Effect of the Class-specific LRP-Optimal Thresholds: Compared to $G$, owing to
the class-specific thresholds, $S$ has $1.7\%$ better AP and $0.5\%$ better
oLRP Error as shown in Table A.18. However, since the mean is dominated by
$s^{*}$ around $0.50$, it is better to focus on classes with low or high
$s^{*}$ values in order to grasp the effect of the approach. The “bus” class
has the lowest $s^{*}$ with $27\%$. For this class, $S$ surpasses $G$ by
$8.7\%$ in AP and $3.9\%$ in oLRP Error. This performance increase is also
observed for other classes with very low thresholds, such as “airplane”,
“bicycle” and “zebra”. For these classes with lower thresholds, the effect of
LRP-Optimal threshold on the PR curve is to stretch the curve in the recall
domain (maybe by accepting some loss in precision) as shown in the “bus”
example in Fig. A.13. Not surprisingly, “cow” is one of the two classes for
which AP of $S$ is lower since its threshold is the highest and thereby
causing recall to be more limited. On the other hand, regarding oLRP Error,
the result is not worse since this time the PR curve is stretched through the
positive precision, as shown in Fig. A.13, allowing better FP errors. Thus, in
any case, lower or higher, the LRP-Optimal threshold aims to discover the best
PR curve. There are four classes in total for which $G$ is better than $S$ in
terms of oLRP Error. However, note that the maximum difference is $0.2\%$ in
oLRP Error and these are the classes with thresholds around $0.5$. These
suggest that choosing class-specific thresholds rather than the general,
class-independent thresholding approach increases the performance of the
detector especially for classes with low or high class-specific thresholds.

###  G.4 Analysing Latency of LRP Error Computation

Since the PQ and LRP Error are very similar in formulation (Section 6 in the
paper), it is obvious that they require very similar time to compute. Hence,
in this section we focus on how much time computing LRP Error adds to the AP
computation. Using COCO api [1], COCO evaluation follows a five-step algorithm
to compute AP: (i) loading annotations into memory, (ii) loading and preparing
results, (iii) per image evaluation, (iv) accumulating evaluation results, and
(v) summarizing (i.e. printing) the results. Since step (i) and (ii) are
independent of the performance measure, and (v) is a simple printing operation
(i.e. it takes less than $3$ seconds compute (i), (ii) and (v) in total) and
we do not change (iii) per image evaluation except returning the computed IoUs
of TPs, we analysed the additional latency of computing oLRP Error for step
(iv) accumulation, in which the per-image evaluation results are combined into
performance values. In order to do that using a standard CPU, we computed and
averaged the runtime of this step using all 36 SOTA models in Table 3 in the
paper on COCO 2017 val with 5000 images. We observed that LRP Error
computation (including LRP, oLRP, their components, class-specific LRP-Optimal
thresholds for different “size” and “maximum detection number” criteria as
done by COCO api - see [1] for details) introduces a negligible overhead with
around one second both for (iv) accumulate step (from $5.8$ seconds to $6.6$
seconds) and for entire computation (from $38.7$ to $39.6$ seconds).

Figure A.14: For each class from COCO, oLRP Error and its components for
Faster R-CNN (X101-12) are plotted against $\tau$. The mean represents the
mean of 80 classes.

###  G.5 Analyzing the Effect of TP Validation Threshold

Finally, we analyse how LRP Error is affected from the TP validation threshold
parameter, $\tau$. We use Faster R-CNN (X101-12) (Table 3 in the paper)
results of the first 10 classes and mean-error for clarity, the effect of the
$\tau$ parameter is analysed in Fig. A.14 on oLRP Error. As expected, larger
$\tau$ values imply lower localisation error ($\mathrm{oLRP_{Loc}}$). On the
other hand, a larger $\tau$ causes FP and FN components to increase rapidly,
leading to higher total error (oLRP Error). This is intuitive since at the
extreme case, i.e., when $\tau=1$, there are hardly any TP (i.e. all the
detections are FPs), which makes oLRP Error to be $1$. Therefore, LRP Error
allows measuring the performance of a detector designed for an application
that requires a different $\tau$ by also providing additional information. In
addition, investigating oLRP Error for different $\tau$ values represents a
good extension for ablation studies.

###  G.6 More Examples for s-LRP Curves

COCO Dataset: Fig. 10 provides s-LRP curves of different object detectors for
the “zebra” and “bus” classes whose PR curve is demonstrated in Fig. 7 of the
paper but not included in Fig. 10 due to space limitations.

(a) Zebra

(b) Bus

Figure A.15: s-LRP curves of different object detectors for the “zebra” and
“bus” classes from COCO dataset whose PR curve is demonstrated in Fig. 7 of
the paper but not included in Fig. 10 due to space limitations. The lines with
a different red tone represent a one-stage detector, while blue tones
correspond to two-stage detector F. R-CNN: Faster R-CNN, C. R-CNN: Cascade
R-CNN

LVIS Dataset: Using the s-LRP curves in Fig. A.16, one can observe the
following:

  * •

While “walking stick” and “weatherwane” (c.f. (a) and (b)) have equal
performance (i.e. $\mathrm{oLRP}=0.90$), “walking stick” is very sensitive to
thresholding but “weatherwane” is not. In particular, if the threshold of
“walking stick” is set slightly larger than $0.00$, then LRP Error increases
to $1$ implying no true positives. On the other hand, this is not very
critical for “weatherwane” since LRP Errors are similar for $s\in[0.00,0.80]$.

  * •

While “bottle cap” has better performance than “baseball bat” (c.f. (c) and
(d)), LRP-Optimal threshold of “bottle cap” is significantly lower, and
besides “bottle cap” is more sensitive to thresholding. Hence, the performance
superiority may not indicate neither less sensitivity to thresholding nor
larger LRP-Optimal threshold.

  * •

Since, unlike PR curves, we do not use interpolation in s-LRP curves (i.e. to
demonstrate the performance as it is - c.f. practicality in Section 3 to see
how PR curves are interpolated), s-LRP curves can include wiggles (c.f. (e),
(f) and (g)).

  * •

We provide s-LRP curves for “zebra” and “bus” classes (c.f. (h) and (i)) for
LVIS dataset as well to allow comparison those with COCO dataset. Note that
compared to Faster R-CNN in Fig. A.15, while the LRP-Optimal threshold of
“zebra” is larger, that of “bus” is lower.

  * •

Finally, note that, while “sour cream”, “cornice”, “zebra” and “bus” (c.f.
(f)-(i)) have similar performance, their s-LRP curves are different, i.e. they
have different sensitivity to threshold choice and different LRP-Optimal
thresholds.

(a) Walking stick

(b) Weatherwane

(c) Baseball bat

(d) Bottle cap

(e) Radiator

(f) Sour cream

(g) Cornice

(h) Zebra

(i) Bus

Figure A.16: s-LRP curves of various classes for Mask R-CNN with ResNet-50
backbone on LVIS dataset.

##  H The Repositories and Configurations of the Used Models in the
Experiments

In order to ensure reproducibility and facilitate direct usage of our results,
Table A.19 associates the models used in different tables in the paper with
the repositories from which we downloaded the trained models. For rare cases,
there may be multiple alternatives for the same backbone and number of trained
epochs owing to different design choices (e.g. using a different layer
normalisation such as group normalisation [64]). In such cases, one can infer
the corresponding model by comparing COCO-style AP values in the corresponding
repository and method.

TABLE A.19: The repositories of models that we downloaded, evaluated and utilized for comparison. Table | Repository | Method
---|---|---
Table 3 | mmdetection [30] | ATSS [36]
Carafe [45]
Cascade Mask R-CNN [20]
Cascade R-CNN [20]
DetectoRS [49]
FCOS [33]
FreeAnchor [39]
GHM [38]
Grid R-CNN [42]
GRoIE [46]
Guided Anchoring [43]
Hybrid Task Cascade [50]
Libra R-CNN [41]
Mask R-CNN [44]
Mask Scoring R-CNN [48]
NAS-FPN [37]
PointRend [47]
RPDet[40]
SSD [23]
detectron [65] | Faster R-CNN [24]
RetinaNet[32]
detectron2 [11] | Keypoint R-CNN [44]
official code [66] | aLRP Loss [19]
Table 5 | mmdetection [30] | Faster R-CNN [24]
RetinaNet[32]
Table 6 | detectron2 [11] | Panoptic FPN [51]
Table 7 | mmdetection [30] | Mask R-CNN [44]
Table 8 | detectron2 [11] | Mask R-CNN [44]
Table 9 | tensorflow [52] | Faster R-CNN [24]
Table 10 | mmdetection [30] | DC5 [67]
FPN [53]
RFP [49]
Table 11 | official code [68] | QPIC [54]
Table 12 | official code [69] | BLC [55]
Table S2 | mmdetection [30] | Mask R-CNN [44]
Table S3 | mmdetection [30] | Faster R-CNN [24]
Table S4 | mmdetection [30] | DETR [57]
Sparse R-CNN [58]
DDETR [59]
Table S5 | detectron2 [11] | Panoptic FPN [51]
|  Kemal Oksuz received his B.Sc. from the Land Forces Academy of Turkey in
2008 and his M.Sc. in 2016 from Bogazici University, Turkey. He received his
Ph.D. degree in 2021 from the Dept. of Computer Eng., Middle East Technical
University (METU), Turkey. Currently, he is working for the Turkish Armed
Forces. He is also a research associate at ImageLab, METU. His research
interests include computer vision with a focus on visual detection and
imbalance problems.
---|---
|  Baris Can Cam received his B.Sc. degree in Electrical and Electronics
Engineering from Eskisehir Osmangazi University, Turkey in 2016. He is
currently pursuing his M.Sc. in Middle East Technical University, Ankara,
Turkey. His research interests include computer vision with a focus on object
detection.
---|---
|  Sinan Kalkan received his M.Sc. degree in Computer Eng. from Middle East
Technical University (METU), Turkey in 2003, and his Ph.D. degree in
Informatics from the Uni. of Göttingen, Germany in 2008. After working as a
postdoctoral researcher at the Uni. of Göttingen and at METU, he joined METU
in 2010 as a faculty member and since then, has been working as an assoc.
prof. on problems within Computer Vision and Robotics.
---|---
|  Emre Akbas is an asst. prof. at the Dept. of Computer Eng., METU, Turkey.
He received his Ph.D. degree from the Dept. of Elect. and Comp. Eng., Uni. of
Illinois at Urbana-Champaign in 2011. His M.Sc. and B.Sc. degrees in computer
sci. are both from METU. Prior to joining METU, he was a postdoctoral
researcher at the Dept. of Psychological and Brain Sciences, Uni. of
California Santa Barbara. His research interests are in computer vision with a
focus on object detection and human pose estimation.
---|---


& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (

(

(exists z .

(j N.<= z)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T z)) a)))

)

)

| (exists k y . (j N.<= k)

& (

(

(k N.<= y)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T y)) a)))

)

| (exists l . ( (j N.<= l)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T l)) a)))

)

)

)

)

)

)

)

)

)

(!prove Lemma1-step10_3 [Lemma1-step10_2 model-step-axioms])

define Lemma1-step10_4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (

(

(exists z .

(j N.<= z)

& (i N.<= z)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T z)) a)))

)

)

| (exists k y . (j N.<= k)

& (

(

(k N.<= y)

& (j N.<= y)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T y)) a)))

)

| (exists l . (j N.<= l)

& (i N.<= l)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T l)) a)))

)

)

)

)

)

)

)

)

(!prove Lemma1-step10_4 [Lemma1-step10_3 N.Less=.transitive])

define Lemma1-step10_5 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j .

(

(

(exists z .

(i N.<= z)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T z)) a)))

)

)

| (exists y .

(

(

(j N.<= y)

& (i N.<= y)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T y)) a)))

)

| (exists l . (i N.<= l)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T l)) a)))

)

)

)

)

)

)

)

)

(!prove Lemma1-step10_5 [Lemma1-step10_4 N.Less=.transitive])

define Lemma1-step15 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

)

)

)

)

(!prove Lemma1-step15 [Lemma1-step10_5])

(!prove Lemma1 [Lemma1-step15])

#\-- Lemma2 (corresponds to Lemma 1 in NFM21 paper)

#\-- In a fair transition path, if eventually a nonfaulty proposer P becomes
ready to propose a ballot b that satisfies P1+P2-True,

#\-- to a quorum Q of nonfaulty acceptors, then 1b messages will be eventually
received by P from all members of Q for the ballot b

#\------------------------------------------------------------------------

define Lemma2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(exists j .

(i N.<= j)

& (has-promises (als (config (rho T j)) p) b Q)

)

)

define Lemma2-step1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

)

)

)

)

(!prove Lemma2-step1 [Lemma1 synod-quorum-axioms])

define Lemma2-step2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

)

)

)

)

(!prove Lemma2-step2 [Lemma2-step1 P1+P2-True-beta-def-axioms])

define Lemma2-step3 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

& (

(available (rho T j) a)

==>

(ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

)

)

)

)

(!prove Lemma2-step3 [Lemma2-step2 synod-ready-to-send-axioms])

define Lemma2-step4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

& (nonfaulty a)

#& (available (rho T j) a)

& (

(available (rho T j) a)

==>

(ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

)

)

)

)

(!prove Lemma2-step4 [Lemma2-step3])

define Lemma2-step5 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

& (

(available (rho T j) a)

| (exists k .

(j N.< k)

& (available (rho T k) a))

)

& (

(available (rho T j) a)

==>

(ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

)

)

)

)

(!prove Lemma2-step5 [Lemma2-step4 acceptor-nonfaulty2])

define Lemma2-step5_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

& (

(

(available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

| (exists k .

(j N.< k)

& (available (rho T k) a))

)

& (

(available (rho T j) a)

==>

(ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

)

)

)

)

(!prove Lemma2-step5_1 [Lemma2-step5])

define Lemma2-step5_2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

& (

(

(available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

| (exists k .

(j N.<= k)

& (i N.<= k)

& (available (rho T k) a)

)

)

)

)

)

)

(!prove Lemma2-step5_2 [Lemma2-step5_1 N.Less=.Implied-by-< collect-1b-from-
quorum N.Less=.transitive])

define Lemma2-step6 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

& (

(

(available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

| (exists k .

(j N.<= k)

& (i N.<= k)

& (available (rho T k) a)

& (

(inMSet (consM p a 1a b nilV) (amu (als (config (rho T k)) a)))

| (exists u v2 .

(j N.<= u)

& (inMSet (consM a p 1b b v2) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step6 [Lemma2-step5_2 persistent-unresponded-local-1a-msgs-
causes])

define Lemma2-step6_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j . (i N.<= j)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (acc a)

& ((beta (als (config (rho T j)) a)) < b)

& (

(

(available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

)

| (exists k .

(j N.<= k)

& (i N.<= k)

& (

(

(available (rho T k) a)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T k)) a)))

& ((beta (als (config (rho T k)) a)) < b)

)

| (exists u v2 .

(j N.<= u)

& (inMSet (consM a p 1b b v2) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step6_1 [Lemma2-step6 P1+P2-True-beta-def-axioms])

define Lemma2-step6_2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists j .

(

( (i N.<= j)

& (available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

& ((beta (als (config (rho T j)) a)) < b)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

)

| (exists k .

(j N.<= k)

& (i N.<= k)

& (

(

(available (rho T k) a)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T k)) a)))

& ((beta (als (config (rho T k)) a)) < b)

& (ready-to (rho T k) a (send a (consM a p 1b b (value (als (config (rho T k))
a))) ) )

)

| (exists u v2 .

(j N.<= u)

& (i N.<= u)

& (inMSet (consM a p 1b b v2) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step6_2 [Lemma2-step6_1 synod-ready-to-send-axioms
N.Less=.Implied-by-< N.Less=.transitive])

define Lemma2-step6_3 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (

(exists j .

( (i N.<= j)

& (available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

& ((beta (als (config (rho T j)) a)) < b)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

)

| (exists k .

(j N.<= k)

& (i N.<= k)

& (

(

(available (rho T k) a)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T k)) a)))

& ((beta (als (config (rho T k)) a)) < b)

& (ready-to (rho T k) a (send a (consM a p 1b b (value (als (config (rho T k))
a))) ) )

)

| (exists u v2 .

(j N.<= u)

& (i N.<= u)

& (inMSet (consM a p 1b b v2) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step6_3 [Lemma2-step6_2 ])

define Lemma2-step7 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (

(exists j y .

( (i N.<= j)

& (available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

& ((beta (als (config (rho T j)) a)) < b)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (j N.<= y)

& (inMSet (consM a p 1b b (value (als (config (rho T j)) a))) (mu (config (rho
T y))) )

)

| (exists k z .

(j N.<= k)

& (i N.<= k)

& (

(

(available (rho T k) a)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T k)) a)))

& ((beta (als (config (rho T k)) a)) < b)

& (ready-to (rho T k) a (send a (consM a p 1b b (value (als (config (rho T k))
a))) ) )

& (k N.<= z)

& (inMSet (consM a p 1b b (value (als (config (rho T k)) a))) (mu (config (rho
T z))) )

)

| (exists u v2 .

(j N.<= u)

& (i N.<= u)

& (inMSet (consM a p 1b b v2) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step7 [Lemma2-step6_3 Fair-Snd-Causes-Theorem])

define Lemma2-step7_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (

(exists j y .

( (i N.<= j)

& (available (rho T j) a)

& (ready-to (rho T j) a (send a (consM a p 1b b (value (als (config (rho T j))
a))) ) )

& ((beta (als (config (rho T j)) a)) < b)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T j)) a)))

& (j N.<= y)

& (inMSet (consM a p 1b b (value (als (config (rho T j)) a))) (mu (config (rho
T y))) )

)

| (exists k z .

(j N.<= k)

& (i N.<= k)

& (

(

(available (rho T k) a)

& (inMSet (consM p a 1a b nilV) (amu (als (config (rho T k)) a)))

& ((beta (als (config (rho T k)) a)) < b)

& (ready-to (rho T k) a (send a (consM a p 1b b (value (als (config (rho T k))
a))) ) )

& (k N.<= z)

& (inMSet (consM a p 1b b (value (als (config (rho T k)) a))) (mu (config (rho
T z))) )

)

| (exists u v2 .

(j N.<= u)

& (i N.<= u)

& (inMSet (consM a p 1b b v2) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step7_1 [Lemma2-step7 model-step-axioms])

define Lemma2-step7_2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (

(exists j y .

( (i N.<= j)

& (j N.<= y)

& (i N.<= y)

& (inMSet (consM a p 1b b (value (als (config (rho T j)) a))) (mu (config (rho
T y))) )

)

| (exists k z .

(j N.<= k)

& (i N.<= k)

& (

(

(k N.<= z)

& (i N.<= z)

& (inMSet (consM a p 1b b (value (als (config (rho T k)) a))) (mu (config (rho
T z))) )

)

| (exists u v2 .

(j N.<= u)

& (i N.<= u)

& (inMSet (consM a p 1b b v2) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step7_2 [Lemma2-step7_1 N.Less=.transitive])

define Lemma2-step7_3 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (

(exists v y .

( (i N.<= y)

& (inMSet (consM a p 1b b v) (mu (config (rho T y))) )

)

| (exists z v2 .

(

( (i N.<= z)

& (inMSet (consM a p 1b b v2) (mu (config (rho T z))) )

)

| (exists u v3 .

(j N.<= u)

& (i N.<= u)

& (inMSet (consM a p 1b b v3) (mu (config (rho T u))) )

)

)

)

)

)

)

)

)

(!prove Lemma2-step7_3 [Lemma2-step7_2])

define Lemma2-step7_4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (

(exists v y .

( (i N.<= y)

& (inMSet (consM a p 1b b v) (mu (config (rho T y))) )

)

)

)

)

)

)

(!prove Lemma2-step7_4 [Lemma2-step7_3])

define Lemma2-step8_4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

)

)

)

)

(!prove Lemma2-step8_4 [Lemma2-step7_4])

define Lemma2-step10 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

)

)

)

)

(!prove Lemma2-step10 [Lemma2-step8_4])

define Lemma2-step13 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (

(available (rho T k) p)

| (exists j .

(k N.< j)

& (available (rho T j) p))

)

)

)

)

)

(!prove Lemma2-step13 [Lemma2-step10 proposer-nonfaulty1])

define Lemma2-step14 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (

(

(available (rho T k) p)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

)

| (exists j .

(k N.<= j)

& (available (rho T j) p)

)

)

)

)

)

)

(!prove Lemma2-step14 [Lemma2-step13 N.Less=.Implied-by-<])

define Lemma2-step15 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))))

& (

(

(available (rho T k) p)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

)

| (exists j .

(k N.<= j)

& (available (rho T j) p)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))))

& (

(inMSet (consM a p 1b b v) (mu (config (rho T j))))

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

)

(!prove Lemma2-step15 [Lemma2-step14 1b-model-msg-persists-until-read-axiom-
lemma])

define Lemma2-step18 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (

(

#(~(lock (als (config (rho T k)) p)))

(inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (available (rho T k) p)

)

| (exists j .

(k N.<= j)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (

(

(inMSet (consM a p 1b b v) (mu (config (rho T j))))

#& (~(lock (als (config (rho T j)) p)))

& (available (rho T j) p)

)

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

)

(!prove Lemma2-step18 [Lemma2-step15 proposer-nonfaulty1])

define Lemma2-step19 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (

(

#(~(lock (als (config (rho T k)) p)))

(inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (available (rho T k) p)

& (ready-to (rho T k) p (receive p (consM a p 1b b v)))

)

| (exists j .

(k N.<= j)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (

(

(inMSet (consM a p 1b b v) (mu (config (rho T j))))

#& (~(lock (als (config (rho T j)) p)))

& (available (rho T j) p)

& (ready-to (rho T j) p (receive p (consM a p 1b b v)))

)

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

)

(!prove Lemma2-step19 [Lemma2-step18 synod-ready-to-receive-lemmas synod-
quorum-axioms])

define Lemma2-step20 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

(

(inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (available (rho T k) p)

& (ready-to (rho T k) p (receive p (consM a p 1b b v)))

& (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j z .

(k N.<= j)

& (inMSet (consM a p 1b b v) (mu (config (rho T k))) )

& (

(

(inMSet (consM a p 1b b v) (mu (config (rho T j))))

& (available (rho T j) p)

& (ready-to (rho T j) p (receive p (consM a p 1b b v)))

& (j N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

)

(!prove Lemma2-step20 [Lemma2-step19 Fair-Rcv-Causes-Theorem])

define Lemma2-step21 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j z .

(k N.<= j)

& (

( (k N.<= j)

& (j N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

)

(!prove Lemma2-step21 [Lemma2-step20 model-step-axioms])

define Lemma2-step22_helper1 :=

(forall v k y .

( (i N.<= k)

& (k N.<= y)

)

==> (i N.<= y)

)

(!prove Lemma2-step22_helper1 [Lemma2-step20 N.Less=.transitive])

define Lemma2-step22 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j z .

(k N.<= j)

& (

( (k N.<= j)

& (j N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

)

(!prove Lemma2-step22 [Lemma2-step21 Lemma2-step22_helper1])

define Lemma2-step22_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j .

(k N.<= j)

& (

(exists z .

(k N.<= j)

& (j N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

)

(!prove Lemma2-step22_1 [Lemma2-step22])

define Lemma2-step22_helper2 :=

(forall p T b i Q .

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j .

(k N.<= j)

& (

(exists z .

(k N.<= j)

& (j N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . ( (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j .

(k N.<= j)

& (

(exists z .

(k N.<= j)

& (j N.<= z)

& (k N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma2-step22_helper2 [N.Less=.transitive])

define Lemma2-step22_2:=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j .

(k N.<= j)

& (

(exists z .

(k N.<= j)

& (j N.<= z)

& (k N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

#\-- TAKES AGES, give it time (comment out this and assert this step to skip
while developing later proofs)

(!prove Lemma2-step22_2 [Lemma2-step22_1 Lemma2-step22_helper2])

define Lemma2-step22_3:=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j .

(k N.<= j)

& (

(exists z .

(k N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

| (exists l . (k N.<= l)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma2-step22_3 [Lemma2-step22_2])

define Lemma2-step22_4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= k)

& (

( (k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (exists j .

(k N.<= j)

& (

(exists z .

(k N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma2-step22_4 [Lemma2-step22_3])

define Lemma2-step22_5 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (

(exists y .

(k N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

| (

(

(exists z .

(k N.<= z)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma2-step22_5 [Lemma2-step22_4])

define Lemma2-step22_6 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k .

(i N.<= k)

& (

(exists y .

(k N.<= y)

& (i N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

)

)

)

)

)

(!prove Lemma2-step22_6 [Lemma2-step22_5 N.Less=.transitive])

define Lemma2-step22_7 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(nonfaulty a) & (acc a)

& (exists v k y .

(i N.<= y)

& (inMSet (consM a p 1b b v) (amu (als (config (rho T y)) p)))

)

)

)

)

(!prove Lemma2-step22_7 [Lemma2-step22_6])

define Lemma2-step24 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(forall a .

((inQ a Q)

==>

(exists v z .

(i N.<= z) # for each a, exists k . (rho T z) = then (rho T k) ... implies
that

& (inMSet (consM a p 1b b v) (amu (als (config (rho T z)) p))) # Did not
happen at the same time. k is important here

)

)

)

)

(!prove Lemma2-step24 [Lemma2-step22_7])

define Lemma2-step24_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(exists j . (i N.<= j)

& (forall a . (inQ a Q) ==> (exists v . (inMSet (consM a p 1b b v) (amu (als
(config (rho T j)) p))) )) )

)

(!prove Lemma2-step24_1 [Lemma2-step24 collect-1b-from-quorum])

(!prove Lemma2 [Lemma2-step24_1 synod-has-promises-def-axiom])

#\-- Lemma3

#\-- In a fair transition path, if eventually a nonfaulty proposer P receives
promises for a ballot b that satisfies P1+P2-True,

#\-- from a quorum Q of nonfaulty acceptors, then 2a messages from P will be
eventually received by all members of Q for b

#\------------------------------------------------------------------------

define Lemma3 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

)

)

)

)

define Lemma3-step1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a . (inQ a Q) ==> (exists v . (inMSet (consM a p 1b b v) (amu (als
(config (rho T i)) p))) ))

)

(!prove Lemma3-step1 [synod-has-promises-def-axiom])

define Lemma3-step2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists v . (inMSet (consM a p 1b b v) (amu (als (config (rho T i)) p))) )

)

& (

(available (rho T i) p)

==>

(exists v2 . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p a 2a b
v2))) ) )

)

)

)

(!prove Lemma3-step2 [Lemma3-step1 synod-ready-to-send-axioms])

define Lemma3-step4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists v . (inMSet (consM a p 1b b v) (amu (als (config (rho T i)) p))) )

)

& (

(available (rho T i) p)

==>

(exists v2 . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p a 2a b
v2))) ) )

)

)

& (

(available (rho T i) p)

| (exists j .

(i N.< j)

& (available (rho T j) p))

)

)

(!prove Lemma3-step4 [Lemma3-step2 proposer-nonfaulty2])

define Lemma3-step4_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists v . (inMSet (consM a p 1b b v) (amu (als (config (rho T i)) p))) )

)

& (

(available (rho T i) p)

==>

(exists v2 . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p a 2a b
v2))) ) )

)

)

& (

(

(available (rho T i) p)

& (forall a . exists v . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (available (rho T j) p))

)

)

(!prove Lemma3-step4_1 [Lemma3-step4 N.Less=.Implied-by-< N.Less=.transitive])

define Lemma3-step4_2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists v . (inMSet (consM a p 1b b v) (amu (als (config (rho T i)) p))) )

)

& (

(available (rho T i) p)

==>

(exists v2 . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p a 2a b
v2))) ) )

)

)

& (

(

(available (rho T i) p)

& (forall a . exists v . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (available (rho T j) p)

& (forall a .

(inQ a Q)

==>

(exists v . (inMSet (consM a p 1b b v) (amu (als (config (rho T i)) p))) )

)

)

)

)

(!prove Lemma3-step4_2 [Lemma3-step4_1])

define Lemma3-step4_2_2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . exists v . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (available (rho T j) p)

& (has-promises (als (config (rho T i)) p) b Q)

)

)

)

(!prove Lemma3-step4_2_2 [Lemma3-step4_2 synod-has-promises-def-axiom])

define persistent-unresponded-local-promises-subaxiom :=

(forall T i p Q b j .

(

(

(has-promises (als (config (rho T i)) p) b Q)

& (i N.<= j)

)

==> (

(has-promises (als (config (rho T j)) p) b Q)

| (exists k v .

(i N.<= k)

& (sent2A (als (config (rho T k)) p) b v Q k)

)

)

)

)

(!prove persistent-unresponded-local-promises-subaxiom [persistent-
unresponded-local-promises])

define Lemma3-step4_3 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . exists v . ((inQ a Q) ==> (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (available (rho T j) p)

& (has-promises (als (config (rho T i)) p) b Q)

& (

(has-promises (als (config (rho T j)) p) b Q)

| (exists k v .

(i N.<= k)

& (sent2A (als (config (rho T k)) p) b v Q k)

)

)

)

)

)

(!prove Lemma3-step4_3 [Lemma3-step4_2_2 persistent-unresponded-local-
promises-subaxiom])

define Lemma3-step4_4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . (inQ a Q) ==> (exists v . (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (available (rho T j) p)

& (has-promises (als (config (rho T i)) p) b Q)

& (

(

(has-promises (als (config (rho T j)) p) b Q)

& (available (rho T j) p)

& (forall a .

(inQ a Q)

==>

(exists v . (ready-to (rho T j) p (send p (consM p a 2a b v))) )

)

)

| (exists k v .

(i N.<= k)

& (sent2A (als (config (rho T k)) p) b v Q k)

)

)

)

)

)

(!prove Lemma3-step4_4 [Lemma3-step4_3 synod-ready-to-send-axioms])

define Lemma3-step4_6 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . (inQ a Q) ==> (exists v . (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (available (rho T j) p)

& (has-promises (als (config (rho T i)) p) b Q)

& (

(

(has-promises (als (config (rho T j)) p) b Q)

& (available (rho T j) p)

& (forall a .

(inQ a Q)

==>

(exists v . (ready-to (rho T j) p (send p (consM p a 2a b v))) )

)

)

| (exists k v .

(i N.<= k)

& (sent2A (als (config (rho T k)) p) b v Q k)

)

)

)

)

)

(!prove Lemma3-step4_6 [Lemma3-step4_4 Fair-Snd-Causes-Theorem])

define helper :=

(forall p T b i Q k v .

(

(i N.<= k)

& (sent2A (als (config (rho T k)) p) b v Q k)

)

==>

(forall a .

(inQ a Q)

==>

(exists u .

(k N.<= u)

#& (= (rho T (S u)) (then (rho T u) (send p (consM p a 2a b v))))

& (inMSet (consM p a 2a b v) (mu (config (rho T u))) )

)

)

)

(!prove helper [sent2A-def])

define Lemma3-step4_7 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . (inQ a Q) ==> (exists v . (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (available (rho T j) p)

& (has-promises (als (config (rho T i)) p) b Q)

& (

(

(has-promises (als (config (rho T j)) p) b Q)

& (available (rho T j) p)

& (forall a .

(inQ a Q)

==>

(exists v . (ready-to (rho T j) p (send p (consM p a 2a b v))) )

)

)

| (exists k v .

(i N.<= k)

& (sent2A (als (config (rho T k)) p) b v Q k)

& (forall a .

(inQ a Q)

==>

(exists u .

(k N.<= u)

#& (= (rho T (S u)) (then (rho T u) (send p (consM p a 2a b v))))

& (inMSet (consM p a 2a b v) (mu (config (rho T u))) )

)

)

)

)

)

)

)

(!prove Lemma3-step4_7 [Lemma3-step4_6 helper])

define Lemma3-step4_8 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . (inQ a Q) ==> (exists v . (ready-to (rho T i) p (send p (consM p
a 2a b v))) ) )

)

| (exists j .

(i N.<= j)

& (

(

(forall a .

(inQ a Q)

==>

(exists v . (ready-to (rho T j) p (send p (consM p a 2a b v))) )

)

)

| (exists k v .

(i N.<= k)

& (sent2A (als (config (rho T k)) p) b v Q k)

& (forall a .

(inQ a Q)

==>

(exists u .

(k N.<= u)

& (i N.<= u)

& (inMSet (consM p a 2a b v) (mu (config (rho T u))) )

)

)

)

)

)

)

)

(!prove Lemma3-step4_8 [Lemma3-step4_7 N.Less=.transitive N.Less=.Implied-
by-<])

define Lemma3-step5 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . (inQ a Q) ==> (exists v j . (i N.<= j) & (inMSet (consM p a 2a b
v) (mu (config (rho T j))) ) ) )

)

| (exists j .

(i N.<= j)

& (

(

(forall a .

(inQ a Q)

==>

(exists v z . (j N.<= z) & (inMSet (consM p a 2a b v) (mu (config (rho T z)))
) )

)

)

| (exists k v .

(i N.<= k)

& (forall a .

(inQ a Q)

==>

(

(inMSet (consM p a 2a b v) (mu (config (rho T k))) )

)

)

)

)

)

)

)

(!prove Lemma3-step5 [Lemma3-step4_8 Fair-Snd-Causes-Theorem])

define Lemma3-step6 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(available (rho T i) p)

& (forall a . (inQ a Q) ==> (exists v j . (i N.<= j) & (inMSet (consM p a 2a b
v) (mu (config (rho T j))) ) ) )

)

| (exists j .

(i N.<= j)

& (

(

(forall a .

(inQ a Q)

==>

(exists v z . (j N.<= z) & (i N.<= z) & (inMSet (consM p a 2a b v) (mu (config
(rho T z))) ) )

)

)

| (exists k v .

(i N.<= k)

& (forall a .

(inQ a Q)

==>

(

(inMSet (consM p a 2a b v) (mu (config (rho T k))) )

)

)

)

)

)

)

)

(!prove Lemma3-step6 [Lemma3-step5 N.Less=.transitive])

define Lemma3-step6_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(

(

(forall a . (inQ a Q) ==> (exists v j . (i N.<= j) & (inMSet (consM p a 2a b
v) (mu (config (rho T j))) ) ) )

)

| ( (

(

(forall a .

(inQ a Q)

==>

(exists v z . (i N.<= z) & (inMSet (consM p a 2a b v) (mu (config (rho T z)))
) )

)

)

| (

(forall a .

(inQ a Q)

==>

(

exists v k . (i N.<= k) & (inMSet (consM p a 2a b v) (mu (config (rho T k))) )

)

)

)

)

)

)

)

(!prove Lemma3-step6_1 [Lemma3-step6])

define Lemma3-step7 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

(inQ a Q)

==>

(exists v k .

(i N.<= k)

& (inMSet (consM p a 2a b v) (mu (config (rho T k))) )

)

)

)

(!prove Lemma3-step7 [Lemma3-step6_1])

define Lemma3-step8 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

(inQ a Q)

==>

(exists v j .

(i N.<= j)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))) )

& (

(available (rho T j) a)

| (exists k .

(j N.< k)

& (available (rho T k) a))

)

)

)

)

(!prove Lemma3-step8 [Lemma3-step7 nonfaulty-def-axioms acceptor-nonfaulty1
synod-quorum-axioms])

define Lemma3-step10 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v . (i N.<= j)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(

#(~(lock (als (config (rho T j)) a)))

(inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (available (rho T j) a)

)

| (exists k . (j N.<= k)

# & ~(lock (als (config (rho T k)) a))

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (available (rho T k) a)

)

)

)

)

)

)

(!prove Lemma3-step10 [Lemma3-step8 N.Less=.Implied-by-<])

define Lemma3-step11 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v . (i N.<= j)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(

(available (rho T j) a)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

)

| (exists k . (j N.<= k)

& (available (rho T k) a)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(inMSet (consM p a 2a b v) (mu (config (rho T k))))

| (exists l . ( (j N.<= l)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T l)) a)))

)

)

)

)

)

)

)

)

)

(!prove Lemma3-step11 [Lemma3-step10 synod-msg-persistance-axioms])

define Lemma3-step13 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v . (i N.<= j)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(

(inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (nonfaulty a)

& (available (rho T j) a)

& (ready-to (rho T j) a (receive a (consM p a 2a b v)))

)

| (exists k . (j N.<= k)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(

(inMSet (consM p a 2a b v) (mu (config (rho T k))))

& (nonfaulty a)

& (available (rho T k) a)

& (ready-to (rho T k) a (receive a (consM p a 2a b v)))

)

| (exists l . ( (j N.<= l)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T l)) a)))

)

)

)

)

)

)

)

)

)

(!prove Lemma3-step13 [Lemma3-step11 synod-ready-to-receive-lemmas synod-
quorum-axioms])

define Lemma3-step14 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v . (i N.<= j)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(

(exists y . (j N.<= y)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T y)) a))))

)

| (exists k . (j N.<= k)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(

(exists z . (k N.<= z)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T z)) a))))

)

| (exists l . (j N.<= l)

& (= (rho T l) (then (rho T j) (receive a (consM p a 2a b v))))

)

)

)

)

)

)

)

)

(!prove Lemma3-step14 [Lemma3-step13 Fair-Rcv-Causes-Theorem])

define Lemma3-step15 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v . (i N.<= j)

& (inMSet (consM p a 2a b v) (mu (config (rho T j))))

& (

(

(exists y . (j N.<= y)

& (i N.<= j)

& (i N.<= y)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T y)) a))))

)

| (exists k . (j N.<= k)

& (i N.<= j)

& (i N.<= k)

& (

(

(exists z . (k N.<= z)

& (j N.<= k)

& (j N.<= z)

& (i N.<= k)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T z)) a))))

)

| (exists l . (j N.<= l)

& (i N.<= j)

& (i N.<= l)

& (= (rho T l) (then (rho T j) (receive a (consM p a 2a b v))))

)

)

)

)

)

)

)

)

(!prove Lemma3-step15 [Lemma3-step14 N.Less=.transitive])

define Lemma3-step16 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v . (i N.<= j)

& (

(

(exists y . (i N.<= y)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T y)) a))))

)

| (exists k .

(

(

(exists z . (i N.<= z)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T z)) a))))

)

| (exists l . (i N.<= l)

& (= (rho T l) (then (rho T j) (receive a (consM p a 2a b v))))

)

)

)

)

)

)

)

)

(!prove Lemma3-step16 [Lemma3-step15 N.Less=.transitive])

define Lemma3-step17 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists v .

(

(

(exists y . (i N.<= y)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T y)) a))))

)

| (

(

(

(exists z . (i N.<= z)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T z)) a))))

)

| (exists l . (i N.<= l)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T l)) a)))

)

)

)

)

)

)

)

)

(!prove Lemma3-step17 [Lemma3-step16 model-step-axioms])

define Lemma3-step18 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v . (i N.<= j)

& (

(

(exists z .

(i N.<= z)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T z)) a)))

)

)

| (exists y .

(

(i N.<= y)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T y)) a)))

)

)

)

)

)

)

)

(!prove Lemma3-step18 [Lemma3-step17 model-step-axioms])

define Lemma3-step19 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists z v .

(i N.<= z)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T z)) a)))

)

)

)

)

(!prove Lemma3-step19 [Lemma3-step18])

(!prove Lemma3 [Lemma3-step19])

#\-- Lemma4 (corresponds to Lemma 2 in NFM21 paper)

#\-- In a fair transition path, if eventually a nonfaulty proposer P receives
promises for a ballot b that satisfies P1+P2-True,

#\-- from a quorum Q of nonfaulty acceptors, then P will eventually receive 2b
messages from all members of Q for b

#\------------------------------------------------------------------------

define Lemma4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(exists j .

(i N.<= j)

& (has-votes (als (config (rho T j)) p) b Q)

)

)

define Lemma4-step1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (acc a)

& (nonfaulty a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

)

)

)

)

(!prove Lemma4-step1 [Lemma3 synod-quorum-axioms])

define Lemma4-step2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (acc a)

& (nonfaulty a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

)

)

)

)

(!prove Lemma4-step2 [Lemma4-step1 P1+P2-True-beta-def-axioms])

define Lemma4-step4 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (acc a)

& (nonfaulty a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

& (

(available (rho T j) a)

| (exists k .

(j N.< k)

& (available (rho T k) a))

)

)

)

)

)

(!prove Lemma4-step4 [Lemma4-step2 acceptor-nonfaulty2])

define Lemma4-step4_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (acc a)

& (nonfaulty a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

& (

(

(available (rho T j) a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

)

| (exists k .

(j N.<= k)

& (available (rho T k) a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

)

)

)

)

)

)

(!prove Lemma4-step4_1 [Lemma4-step4 N.Less=.Implied-by-<])

define Lemma4-step5 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (acc a)

& (nonfaulty a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

& (

(

(available (rho T j) a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

)

| (exists k .

(j N.<= k)

& (available (rho T k) a)

& (

(

(inMSet (consM p a 2a b v) (amu (als (config (rho T k)) a)))

& (available (rho T k) a)

)

| (exists t .

(j N.<= t)

& (inMSet (consM a p 2b b v) (mu (config (rho T t))) )

)

)

)

)

)

)

)

)

(!prove Lemma4-step5 [Lemma4-step4_1 persistent-unresponded-local-2a-msgs-
causes P1+P2-True-beta-def-axioms])

define Lemma4-step6 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (acc a)

& (nonfaulty a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

& (

(

(available (rho T j) a)

& (inMSet (consM p a 2a b v) (amu (als (config (rho T j)) a)))

& ((beta (als (config (rho T j)) a)) =< b)

& (ready-to (rho T j) a (send a (consM a p 2b b v) ) )

)

| (exists k .

(j N.<= k)

& (available (rho T k) a)

& (

(

(inMSet (consM p a 2a b v) (amu (als (config (rho T k)) a)))

& (available (rho T k) a)

& ((beta (als (config (rho T k)) a)) =< b)

& (ready-to (rho T k) a (send a (consM a p 2b b v) ) )

)

| (exists t .

(j N.<= t)

& (inMSet (consM a p 2b b v) (mu (config (rho T t))) )

)

)

)

)

)

)

)

)

(!prove Lemma4-step6 [Lemma4-step5 synod-ready-to-send-axioms P1+P2-True-beta-
def-axioms])

define Lemma4-step6_1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (

(

(exists y . (j N.<= y)

& (i N.<= j)

& (inMSet (consM a p 2b b v) (mu (config (rho T y))) )

)

)

| (exists k .

(j N.<= k)

& (

(

(exists z . (k N.<= z)

& (j N.<= k)

& (inMSet (consM a p 2b b v) (mu (config (rho T z))) )

)

)

| (exists t .

(j N.<= t)

& (i N.<= j)

& (inMSet (consM a p 2b b v) (mu (config (rho T t))) )

)

)

)

)

)

)

)

)

(!prove Lemma4-step6_1 [Lemma4-step6 Fair-Snd-Causes-Theorem model-step-axioms
N.Less=.Implied-by-<])

define Lemma4-step6_2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(i N.<= j)

& (

(

(exists y . (i N.<= y)

& (inMSet (consM a p 2b b v) (mu (config (rho T y))) )

)

)

| (exists k .

(

(

(exists z . (j N.<= z)

& (i N.<= j)

& (inMSet (consM a p 2b b v) (mu (config (rho T z))) )

)

)

| (exists t .

(i N.<= t)

& (inMSet (consM a p 2b b v) (mu (config (rho T t))) )

)

)

)

)

)

)

)

)

(!prove Lemma4-step6_2 [Lemma4-step6_1 N.Less=.transitive])

define Lemma4-step6_3 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists j v .

(

(

(exists y . (i N.<= y)

& (inMSet (consM a p 2b b v) (mu (config (rho T y))) )

)

)

| (exists k .

(

(

(exists z . (i N.<= z)

& (inMSet (consM a p 2b b v) (mu (config (rho T z))) )

)

)

| (exists t .

(i N.<= t)

& (inMSet (consM a p 2b b v) (mu (config (rho T t))) )

)

)

)

)

)

)

)

)

(!prove Lemma4-step6_3 [Lemma4-step6_2 N.Less=.transitive])

define Lemma4-step7 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

)

)

)

)

(!prove Lemma4-step7 [Lemma4-step6_3])

define Lemma4-step8 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

& (

(available (rho T k) p)

| (exists j .

(k N.< j)

& (available (rho T j) p))

)

)

)

)

)

(!prove Lemma4-step8 [Lemma4-step7 proposer-nonfaulty1])

define Lemma4-step9 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (

(

(available (rho T k) p)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

)

| (exists j .

(k N.<= j)

& (available (rho T j) p)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

)

)

)

)

)

)

(!prove Lemma4-step9 [Lemma4-step8 N.Less=.Implied-by-<])

define Lemma4-step12 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (

(

(available (rho T k) p)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

)

| (exists j .

(k N.<= j)

& (available (rho T j) p)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

& (

(inMSet (consM a p 2b b v) (mu (config (rho T j))))

| (exists l .

(k N.<= l)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma4-step12 [Lemma4-step9 2b-model-msg-persists-until-read-axiom-
lemma])

define Lemma4-step14 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (

(

#(~(lock (als (config (rho T k)) p)))

(inMSet (consM a p 2b b v) (mu (config (rho T k))) )

& (available (rho T k) p)

)

| (exists j .

(k N.<= j)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

& (

(

(inMSet (consM a p 2b b v) (mu (config (rho T j))))

#& (~(lock (als (config (rho T j)) p)))

& (available (rho T j) p)

)

| (exists l .

(k N.<= l)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma4-step14 [Lemma4-step12 proposer-nonfaulty1])

define Lemma4-step15 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (

(

# (~(lock (als (config (rho T k)) p)))

(inMSet (consM a p 2b b v) (mu (config (rho T k))) )

& (available (rho T k) p)

& (ready-to (rho T k) p (receive p (consM a p 2b b v)))

)

| (exists j .

(k N.<= j)

& (inMSet (consM a p 2b b v) (mu (config (rho T k))) )

& (

(

(inMSet (consM a p 2b b v) (mu (config (rho T j))))

# & (~(lock (als (config (rho T j)) p)))

& (available (rho T j) p)

& (ready-to (rho T j) p (receive p (consM a p 2b b v)))

)

| (exists l .

(k N.<= l)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma4-step15 [Lemma4-step14 synod-ready-to-receive-lemmas synod-
quorum-axioms])

define Lemma4-step16 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (

(

(exists y . (k N.<= y)

& (i N.<= k)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T y)) p))))

)

| (exists j .

(k N.<= j)

& (

(

(exists z . (j N.<= z)

& (k N.<= j)

& (i N.<= k)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T z)) p))))

)

| (exists l . (k N.<= l)

& (i N.<= k)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma4-step16 [Lemma4-step15 Fair-Rcv-Causes-Theorem model-step-
axioms])

define Lemma4-step17 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v .

(i N.<= k)

& (

(

(exists y . (k N.<= y)

& (i N.<= k)

& (i N.<= y)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T y)) p))))

)

| (exists j .

(k N.<= j)

& (

(

(exists z . (j N.<= z)

& (k N.<= j)

& (i N.<= k)

& (k N.<= z)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T z)) p))))

)

| (exists l . (k N.<= l)

& (i N.<= k)

#& (i N.<= l)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma4-step17 [Lemma4-step16 N.Less=.transitive])

define Lemma4-step18 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(exists k v . (

(

(exists y . (i N.<= y)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T y)) p))))

)

| (exists j .

(k N.<= j)

& (

(

(exists z . (i N.<= z)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T z)) p))))

)

| (exists l . (i N.<= l)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T l)) p)))

)

)

)

)

)

)

)

)

(!prove Lemma4-step18 [Lemma4-step17 N.Less=.transitive])

define Lemma4-step19 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(forall a .

((inQ a Q)

==>

(

(exists z v . (i N.<= z)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T z)) p)))

)

)

)

)

)

(!prove Lemma4-step19 [Lemma4-step18])

define Lemma4-step20 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==> (

(forall a .

((inQ a Q)

==>

(

(exists z v . (i N.<= z)

& (inMSet (consM a p 2b b v) (amu (als (config (rho T z)) p)))

)

)

)

)

& (exists k . (i N.<= k)

& (forall a . (inQ a Q) ==> (exists v . (inMSet (consM a p 2b b v) (amu (als
(config (rho T k)) p))) ))

)

)

)

(!prove Lemma4-step20 [Lemma4-step19 collect-2b-from-quorum])

(!prove Lemma4 [Lemma4-step20 synod-has-votes-def-axiom])

#\----------------------------------------------------------------------------

#\-- PROVING THE MAIN PROGRESS THEOREM

#\----------------------------------------------------------------------------

define Main-Lemma1 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

==>

(exists j .

(i N.<= j)

& (has-promises (als (config (rho T j)) p) b Q)

)

)

(!prove Main-Lemma1 [Lemma2])

define Main-Lemma2 :=

(forall p T b i Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

& (has-promises (als (config (rho T i)) p) b Q)

)

==>

(exists j .

(i N.<= j)

& (has-votes (als (config (rho T j)) p) b Q)

)

)

(!prove Main-Lemma2 [Lemma4])

define Progress-Theorem-step1 :=

( progress_conditions

==>

(forall T .

(exists i p b Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

& (ready-to (rho T i) p (send p (consM p a 1a b nilV)))

)

)

&

(exists j .

(i N.<= j)

& (has-promises (als (config (rho T j)) p) b Q)

)

)

)

)

(!prove Progress-Theorem-step1 [Main-Lemma1])

define Progress-Theorem-step2 :=

( progress_conditions

==>

(forall T .

(exists i p b Q .

(

(prp p)

& (P1+P2-True b)

& (nonfaulty p)

& (has-promises (als (config (rho T i)) p) b Q)

& (forall a . (inQ a Q)

==>

(nonfaulty a)

)

)

& (exists j .

(i N.<= j)

& (has-votes (als (config (rho T j)) p) b Q)

)

)

)

)

(!prove Progress-Theorem-step2 [Progress-Theorem-step1 Main-Lemma2])

(!prove Progress-Theorem [Progress-Theorem-step1 Progress-Theorem-step2 synod-
learn-def-axiom])

}#close module