-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathstabilization_names.txt
2266 lines (2266 loc) · 49.9 KB
/
stabilization_names.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
a_after_pred_merge_point
a_before_pred_merge_point
active_nodes
active_nodes_invar
adding_nodes_did_not_affect_live_node
adding_nodes_does_not_affect_best_succ
adding_nodes_does_not_affect_dead_node
adding_nodes_does_not_affect_live_node
addr
addr_eq_dec
addr_of
add_tick
add_tick_definition
adopting_succs_decreases_succs_error
ahr_related_preserved
ahr_unrelated_channel_unchanged
all
all_first_succs_best
all_in_dec
all_measures_drop_when_succs_error_nonzero
all_measures_nonincreasing_always_each_nonincreasing
all_nodes_cur_request_timeouts_related
all_succs_correct
always_all_measures_drop_when_succs_error_nonzero
always_and_tl_comm
always_and_tl_eq
always_bound_on_local_measures_bounds_max
always_busy_or_not_busy
always_continuously_and_tl
always_zero_phase_two_error_phase_two
and
andb
andb_prop
andb_true_intro
and_comm
and_ind
and_tl_always_P
app
apply_handler_result
apply_handler_result_updates_sigma
Ascii:ascii
Ascii:Ascii
Ascii:ascii_dec
Ascii:ascii_rec
Ascii:ascii_rect
ascii_to_id
at_most_one_request_timeout
at_most_one_request_timeout'
at_most_one_request_timeout'_cons
at_most_one_request_timeout'_cons_neq
at_most_one_request_timeout'_drop
at_most_one_request_timeout_invariant
at_most_one_request_timeout'_none
at_most_one_request_timeout'_remove
at_most_one_request_timeout'_remove_drops_all
at_most_one_request_timeout'_swap
at_most_one_request_timeout_uniqueness
at_most_one_request_timeout'_uniqueness
auxiliary:Zegal_left
auxiliary:Zge_left
auxiliary:Zgt_left
auxiliary:Zle_left
auxiliary:Zlt_left
auxiliary:Zne_left
Basics:flip
Basics:impl
best_predecessor
best_succ
best_succ_preserved
better_pred
better_pred_bool
better_pred_eventually_improves_succ
better_succ
better_succ_better_succ_bool_true
better_succ_bool
better_succ_intro
better_succ_same
between
between_between_bool_equiv
between_bool
between_bool_between
between_bool_false_not_between
between_bool_yz_antisymmetric
between_bool_yz_total
BetweenMono
BetweenWrapL
BetweenWrapR
between_xyx
BinInt.Pos2Z:inj_succ
BinInt.Pos2Z:opp_neg
BinInt.Z:A'A_left
BinInt.Z:A'A_right
BinInt.Z:add
BinInt.Z:add_0_l
BinInt.Z:add_0_r
BinInt.Z:add_1_l
BinInt.Z:add_1_r
BinInt.Z:add_assoc
BinInt.Z:add_cancel_l
BinInt.Z:add_cancel_r
BinInt.Z:add_comm
BinInt.Z:add_le_mono
BinInt.Z:add_le_mono_l
BinInt.Z:add_le_mono_r
BinInt.Z:add_lt_mono
BinInt.Z:add_lt_mono_l
BinInt.Z:add_lt_mono_r
BinInt.Z:add_move_0_l
BinInt.Z:add_move_0_r
BinInt.Z:add_move_l
BinInt.Z:add_move_r
BinInt.Z:add_nonneg_nonneg
BinInt.Z:add_opp_diag_l
BinInt.Z:add_opp_diag_r
BinInt.Z:add_opp_l
BinInt.Z:add_opp_r
BinInt.Z:add_pred_l
BinInt.Z:add_pred_r
BinInt.Z:add_shuffle0
BinInt.Z:add_shuffle1
BinInt.Z:add_shuffle3
BinInt.Z:add_sub_assoc
BinInt.Z:add_succ_l
BinInt.Z:add_succ_r
BinInt.Z:add_wd
BinInt.Z:bi_induction
BinInt.Z:central_induction
BinInt.Z:compare
BinInt.Z:compare_antisym
BinInt.Z:compare_eq_iff
BinInt.Z:compare_gt_iff
BinInt.Z:compare_le_iff
BinInt.Z:compare_lt_iff
BinInt.Z:compare_nge_iff
BinInt.Z:compare_ngt_iff
BinInt.Z:compare_nle_iff
BinInt.Z:compare_refl
BinInt.Z:compare_spec
BinInt.Z:compare_sub
BinInt.Z:double
BinInt.Z:eq
BinInt.Z:eq_decidable
BinInt.Z:eq_equiv
BinInt.Z:eq_le_incl
BinInt.Z:eq_mul_0
BinInt.Z:ge
BinInt.Z:ge_le
BinInt.Z:ge_le_iff
BinInt.Z:gt
BinInt.Z:gt_lt_iff
BinInt.Z:lbase
BinInt.Z:le
BinInt.Z:le_0_sub
BinInt.Z:leb
BinInt.Z:leb_gt
BinInt.Z:leb_le
BinInt.Z:leb_nle
BinInt.Z:le_decidable
BinInt.Z:left_induction
BinInt.Z:le_gt_cases
BinInt.Z:le_le_succ_r
BinInt.Z:le_lt_add_lt
BinInt.Z:le_lteq
BinInt.Z:le_lt_trans
BinInt.Z:le_ngt
BinInt.Z:le_preorder
BinInt.Z:le_refl
BinInt.Z:le_succ_l
BinInt.Z:le_succ_r
BinInt.Z:le_trans
BinInt.Z:le_wd
BinInt.Z:ls_ls'
BinInt.Z:ls'_ls''
BinInt.Z:lt
BinInt.Z:lt_0_1
BinInt.Z:lt_0_sub
BinInt.Z:lt_1_2
BinInt.Z:lt_asymm
BinInt.Z:ltb
BinInt.Z:ltb_antisym
BinInt.Z:ltb_ge
BinInt.Z:ltb_irrefl
BinInt.Z:ltb_lt
BinInt.Z:ltb_nlt
BinInt.Z:lt_compat
BinInt.Z:lt_eq_cases
BinInt.Z:lt_exists_pred
BinInt.Z:lt_exists_pred_strong
BinInt.Z:lt_gt_cases
BinInt.Z:lt_ind
BinInt.Z:lt_irrefl
BinInt.Z:lt_le_incl
BinInt.Z:lt_le_pred
BinInt.Z:lt_lt_succ_r
BinInt.Z:lt_neq
BinInt.Z:lt_strorder
BinInt.Z:lt_succ_diag_r
BinInt.Z:lt_succ_l
BinInt.Z:lt_succ_r
BinInt.Z:lt_total
BinInt.Z:lt_trans
BinInt.Z:lt_trichotomy
BinInt.Z:lt_wd
BinInt.Z:max
BinInt.Z:max_l
BinInt.Z:max_r
BinInt.Z:max_spec
BinInt.Z:mul
BinInt.Z:mul_0_l
BinInt.Z:mul_0_r
BinInt.Z:mul_1_l
BinInt.Z:mul_1_r
BinInt.Z:mul_add_distr_l
BinInt.Z:mul_add_distr_r
BinInt.Z:mul_assoc
BinInt.Z:mul_comm
BinInt.Z:mul_eq_0
BinInt.Z:mul_le_mono_nonneg
BinInt.Z:mul_le_mono_nonneg_l
BinInt.Z:mul_le_mono_nonneg_r
BinInt.Z:mul_lt_mono_neg_l
BinInt.Z:mul_lt_mono_neg_r
BinInt.Z:mul_lt_mono_nonneg
BinInt.Z:mul_lt_mono_pos_l
BinInt.Z:mul_lt_mono_pos_r
BinInt.Z:mul_lt_pred
BinInt.Z:mul_neg_neg
BinInt.Z:mul_neg_pos
BinInt.Z:mul_nonneg_nonneg
BinInt.Z:mul_opp_l
BinInt.Z:mul_opp_r
BinInt.Z:mul_pos_cancel_r
BinInt.Z:mul_pos_neg
BinInt.Z:mul_pos_pos
BinInt.Z:mul_succ_l
BinInt.Z:mul_succ_r
BinInt.Z:mul_wd
BinInt:Zne
BinInt.Z:neq_succ_diag_l
BinInt.Z:nle_gt
BinInt.Z:nle_succ_diag_l
BinInt.Z:nlt_ge
BinInt.Z:nlt_succ_diag_l
BinInt.Z:of_N
BinInt.Z:of_nat
BinInt.Z:one_succ
BinInt.Z:opp
BinInt.Z:opp_0
BinInt.Z:opp_add_distr
BinInt.Z:opp_eq_mul_m1
BinInt.Z:opp_involutive
BinInt.Z:opp_le_mono
BinInt:Zopp_mult_distr_r
BinInt.Z:opp_nonneg_nonpos
BinInt.Z:opp_nonpos_nonneg
BinInt.Z:opp_pred
BinInt.Z:opp_sub_distr
BinInt.Z:opp_succ
BinInt.Z:opp_wd
BinInt.Z:order_induction
BinInt.Z:order_induction_0
BinInt.Z:peano_ind
BinInt:Zplus_assoc_reverse
BinInt.Z:pos_sub
BinInt.Z:pos_sub_diag
BinInt.Z:pos_sub_opp
BinInt.Z:pos_sub_spec
BinInt.Z:pred
BinInt.Z:pred_double
BinInt.Z:pred_inj
BinInt.Z:pred_inj_wd
BinInt.Z:pred_succ
BinInt.Z:pred_wd
BinInt.Z.Private_BootStrap:add_0_r
BinInt.Z.Private_BootStrap:add_assoc
BinInt.Z.Private_BootStrap:add_assoc_pos
BinInt.Z.Private_BootStrap:add_comm
BinInt.Z.Private_BootStrap:add_opp_diag_r
BinInt.Z.Private_BootStrap:mul_0_r
BinInt.Z.Private_BootStrap:mul_1_l
BinInt.Z.Private_BootStrap:mul_add_distr_pos
BinInt.Z.Private_BootStrap:mul_add_distr_r
BinInt.Z.Private_BootStrap:mul_opp_r
BinInt.Z.Private_BootStrap:opp_add_distr
BinInt.Z.Private_BootStrap:opp_inj
BinInt.Z.Private_BootStrap:pos_sub_add
BinInt.Z.Private_OrderTac.IsTotal:eq_equiv
BinInt.Z.Private_OrderTac.IsTotal:le_lteq
BinInt.Z.Private_OrderTac.IsTotal:lt_compat
BinInt.Z.Private_OrderTac.IsTotal:lt_strorder
BinInt.Z.Private_OrderTac.IsTotal:lt_total
BinInt.Z.Private_OrderTac.Tac:eq_lt
BinInt.Z.Private_OrderTac.Tac:eq_neq
BinInt.Z.Private_OrderTac.Tac:eq_refl
BinInt.Z.Private_OrderTac.Tac:eq_sym
BinInt.Z.Private_OrderTac.Tac:eq_trans
BinInt.Z.Private_OrderTac.Tac:interp_ord
BinInt.Z.Private_OrderTac.Tac:le_antisym
BinInt.Z.Private_OrderTac.Tac:le_eq
BinInt.Z.Private_OrderTac.Tac:le_lt_trans
BinInt.Z.Private_OrderTac.Tac:le_refl
BinInt.Z.Private_OrderTac.Tac:lt_eq
BinInt.Z.Private_OrderTac.Tac:lt_irrefl
BinInt.Z.Private_OrderTac.Tac:lt_trans
BinInt.Z.Private_OrderTac.Tac:not_ge_lt
BinInt.Z.Private_OrderTac.Tac:not_gt_le
BinInt.Z.Private_OrderTac.Tac:not_neq_eq
BinInt.Z.Private_OrderTac.Tac:trans
BinInt.Z:rbase
BinInt.Z:right_induction
BinInt.Z:rs_rs'
BinInt.Z:rs'_rs''
BinInt.Z:strong_left_induction
BinInt.Z:strong_right_induction
BinInt.Z:sub
BinInt.Z:sub_0_l
BinInt.Z:sub_0_r
BinInt.Z:sub_cancel_r
BinInt.Z:sub_diag
BinInt.Z:sub_move_0_r
BinInt.Z:sub_move_r
BinInt.Z:sub_opp_r
BinInt.Z:sub_simpl_r
BinInt.Z:sub_sub_distr
BinInt.Z:sub_succ_l
BinInt.Z:sub_succ_r
BinInt.Z:sub_wd
BinInt.Z:succ
BinInt.Z:succ_double
BinInt.Z:succ_inj
BinInt.Z:succ_inj_wd
BinInt.Z:succ_le_mono
BinInt.Z:succ_lt_mono
BinInt.Z:succ_pred
BinInt.Z:succ_wd
BinInt.Z:to_N
BinInt.Z:to_nat
BinInt.Z:two_succ
BinNat.N:add
BinNat.N:compare
BinNat.N:compare_antisym
BinNat.N:compare_eq_iff
BinNat.N:compare_lt_iff
BinNat.N:compare_spec
BinNat.N:le
BinNat.N:lt
BinNat.N:max
BinNat.N:of_nat
BinNat.N:sub
BinNat.N:to_nat
BinNums:N
BinNums:N0
BinNums:Npos
BinNums:positive
BinNums:positive_ind
BinNums:xH
BinNums:xI
BinNums:xO
BinNums:Z
BinNums:Z0
BinNums:Zneg
BinNums:Zpos
BinPosDef.Pos:add
BinPosDef.Pos:succ
BinPos.Pos:add
BinPos.Pos:add_1_l
BinPos.Pos:add_1_r
BinPos.Pos:add_assoc
BinPos.Pos:add_cancel_l
BinPos.Pos:add_carry
BinPos.Pos:add_carry_add
BinPos.Pos:add_carry_spec
BinPos.Pos:add_comm
BinPos.Pos:add_compare_mono_l
BinPos.Pos:add_compare_mono_r
BinPos.Pos:add_lt_mono
BinPos.Pos:add_lt_mono_l
BinPos.Pos:add_lt_mono_r
BinPos.Pos:add_no_neutral
BinPos.Pos:add_reg_l
BinPos.Pos:add_reg_r
BinPos.Pos:add_sub
BinPos.Pos:add_sub_assoc
BinPos.Pos:add_succ_l
BinPos.Pos:add_succ_r
BinPos.Pos:add_xI_pred_double
BinPos.Pos:compare
BinPos.Pos:compare_antisym
BinPos.Pos:compare_cont
BinPos.Pos:compare_cont_antisym
BinPos.Pos:compare_cont_spec
BinPos.Pos:compare_eq_iff
BinPos.Pos:compare_lt_iff
BinPos.Pos:compare_refl
BinPos.Pos:compare_spec
BinPos.Pos:compare_sub_mask
BinPos.Pos:compare_succ_l
BinPos.Pos:compare_succ_r
BinPos.Pos:compare_succ_succ
BinPos.Pos:compare_xI_xI
BinPos.Pos:compare_xI_xO
BinPos.Pos:compare_xO_xI
BinPos.Pos:compare_xO_xO
BinPos.Pos:double_mask
BinPos.Pos:double_pred_mask
BinPos.Pos:eq_equiv
BinPos.Pos:gt
BinPos.Pos:gt_lt
BinPos.Pos:gt_lt_iff
BinPos.Pos:IsNeg
BinPos.Pos:IsNul
BinPos.Pos:IsPos
BinPos.Pos:iter_op
BinPos.Pos:iter_op_succ
BinPos.Pos:le
BinPos.Pos:le_1_l
BinPos.Pos:lt
BinPos.Pos:lt_1_succ
BinPos.Pos:lt_add_r
BinPos.Pos:lt_gt
BinPos.Pos:lt_iff_add
BinPos.Pos:lt_succ_diag_r
BinPos.Pos:lt_succ_r
BinPos.Pos:lt_trans
BinPos.Pos:mask
BinPos.Pos:mask2cmp
BinPos.Pos:mul
BinPos.Pos:mul_1_r
BinPos.Pos:mul_add_distr_l
BinPos.Pos:mul_add_distr_r
BinPos.Pos:mul_comm
BinPos.Pos:mul_compare_mono_l
BinPos.Pos:mul_compare_mono_r
BinPos.Pos:mul_lt_mono_l
BinPos.Pos:mul_sub_distr_l
BinPos.Pos:mul_sub_distr_r
BinPos.Pos:mul_xI_r
BinPos.Pos:mul_xO_r
BinPos.Pos:of_nat
BinPos.Pos:of_nat_succ
BinPos.Pos:of_succ_nat
BinPos.Pos:peano_ind
BinPos.Pos:peano_rect
BinPos.Pos:pred
BinPos.Pos:pred_double
BinPos.Pos:pred_mask
BinPos.Pos:sub
BinPos.Pos:sub_add
BinPos.Pos:sub_add_distr
BinPos.Pos:SubIsNeg
BinPos.Pos:SubIsNul
BinPos.Pos:SubIsPos
BinPos.Pos:sub_mask
BinPos.Pos:sub_mask_add
BinPos.Pos:sub_mask_add_diag_l
BinPos.Pos:sub_mask_add_diag_r
BinPos.Pos:sub_mask_carry
BinPos.Pos:sub_mask_carry_spec
BinPos.Pos:sub_mask_diag
BinPos.Pos:sub_mask_neg
BinPos.Pos:sub_mask_neg_iff
BinPos.Pos:sub_mask_neg_iff'
BinPos.Pos:sub_mask_nul_iff
BinPos.Pos:sub_mask_pos
BinPos.Pos:sub_mask_pos'
BinPos.Pos:sub_mask_pos_iff
BinPos.Pos:sub_mask_spec
BinPos.Pos:SubMaskSpec
BinPos.Pos:sub_sub_distr
BinPos.Pos:sub_xI_xI
BinPos.Pos:sub_xI_xO
BinPos.Pos:sub_xO_xI
BinPos.Pos:sub_xO_xO
BinPos.Pos:succ
BinPos.Pos:succ_double_mask
BinPos.Pos:succ_inj
BinPos.Pos:succ_not_1
BinPos.Pos:succ_pred_double
BinPos.Pos:succ_pred_or
BinPos.Pos:switch_Eq
BinPos.Pos:to_nat
bit_len
Bitvectors:ascii_to_vec
Bitvectors:fixed_length_string_to_vec
Bitvectors:string_to_vec
Bitvectors:string_to_vec_helper
bool
Bool:absurd_eq_true
Bool:andb_false_iff
Bool:andb_true_iff
Bool:bool_dec
Bool:diff_false_true
Bool:eqb
Bool:eqb_true_iff
Bool:eq_iff_eq_true
Bool:eq_true_iff_eq
Bool:negb_true_iff
Bool:not_true_iff_false
bool_rec
bool_rect
Bool:reflect
Bool:ReflectF
Bool:ReflectT
Bool:trans_eq_bool
Busy
busy_if_live
Bvector:Bnil
Bvector:Bvector
channel
channel_contents
channel_empty_not_in
channel_stays_empty
channel_stays_empty'
chop_succs
Chord:addr
Chord:addr_eq_dec
Chord:client_addr
chord_fail_invariant
chord_fail_pre_post
chord_fail_pre_post_conj
chord_fail_pre_post_strengthen_r
Chord:hash
Chord:id
Chord:id_eq_dec
ChordIDParams:binary_value_inj
ChordIDParams:bit_adds_equal
ChordIDParams:hash
ChordIDParams:id
ChordIDParams:id_eq_dec
ChordIDParams:lt
ChordIDParams:lt_asymm
ChordIDParams:ltb
ChordIDParams:ltb_correct
ChordIDParams:ltb_leb
ChordIDParams:lt_irrefl
ChordIDParams:lt_total
ChordIDParams:lt_trans
ChordIDParams:name
ChordIDParams:name_eq_dec
ChordIDParams:plus_2x_inj
ChordIDSpace:hash
ChordIDSpace:id
chord_init_invariant
chord_input_invariant
chord_input_pre_post
chord_keepalive_invariant
chord_keepalive_pre_post
chord_net_invariant
chord_output_invariant
chord_output_pre_post
chord_rectify_invariant
chord_rectify_pre_post
chord_recv_handler_invariant
chord_recv_handler_pre_post
chord_request_invariant
chord_request_pre_post
ChordSemantics:addr
ChordSemantics:addr_eq_dec
ChordSemantics:Build_global_state
ChordSemantics:client_addr
ChordSemantics:client_payload
ChordSemantics:data
ChordSemantics:e_recv
ChordSemantics:e_recv
ChordSemantics:e_recv
ChordSemantics:e_recv
ChordSemantics:e_send
ChordSemantics:e_send
ChordSemantics:e_send
ChordSemantics:e_send
ChordSemantics:e_timeout
ChordSemantics:e_timeout
ChordSemantics:e_timeout
ChordSemantics:e_timeout
ChordSemantics:event
ChordSemantics:event
ChordSemantics:event
ChordSemantics:event
ChordSemantics:failed_nodes
ChordSemantics:failure_constraint
ChordSemantics:global_state
ChordSemantics:Input
ChordSemantics:label
ChordSemantics:label_input
ChordSemantics:label_output
ChordSemantics:msg
ChordSemantics:msgs
ChordSemantics:nodes
ChordSemantics:payload
ChordSemantics:recv_handler
ChordSemantics:recv_handler_l
ChordSemantics:recv_handler_labeling
ChordSemantics:res
ChordSemantics:sigma
ChordSemantics:start_constraint
ChordSemantics:start_handler
ChordSemantics:timeout
ChordSemantics:Timeout
ChordSemantics:timeout_constraint
ChordSemantics:timeout_eq_dec
ChordSemantics:timeout_handler
ChordSemantics:timeout_handler_l
ChordSemantics:timeout_handler_labeling
ChordSemantics:timeouts
ChordSemantics:trace
chord_stabilization
chord_start_invariant
chord_start_pre_post
chord_start_pre_post_conj
chord_start_pre_post_strengthen_r
chord_start_pre_post_weaken_l
chord_start_pre_post_weaken_r
ChordSystem:addr
ChordSystem:addr_eq_dec
ChordSystem:add_tick
ChordSystem:best_predecessor
ChordSystem:Busy
ChordSystem:chop_succs
ChordSystem:clear_delayed_queries
ChordSystem:clear_query
ChordSystem:clear_rectify_with
ChordSystem:cur_request
ChordSystem:data
ChordSystem:_data
ChordSystem:delayed_queries
ChordSystem:delay_query
ChordSystem:DetectFailure
ChordSystem:do_delayed_queries
ChordSystem:do_rectify
ChordSystem:end_query
ChordSystem:GetBestPredecessor
ChordSystem:GetPredAndSuccs
ChordSystem:GetSuccList
ChordSystem:GotBestPredecessor
ChordSystem:GotPredAndSuccs
ChordSystem:GotSuccList
ChordSystem:handle_delayed_query
ChordSystem:handle_msg
ChordSystem:handle_query_req
ChordSystem:handle_query_req_busy
ChordSystem:handle_query_res
ChordSystem:handle_query_timeout
ChordSystem:handle_rectify
ChordSystem:handle_stabilize
ChordSystem:Ineffective
ChordSystem:Input
ChordSystem:is_request
ChordSystem:Join
ChordSystem:Join2
ChordSystem:joined
ChordSystem:keepalive_handler
ChordSystem:KeepaliveTick
ChordSystem:known
ChordSystem:_label
ChordSystem:make_request
ChordSystem:make_succs
ChordSystem:mkData
ChordSystem:next_msg_for_join
ChordSystem:Notify
ChordSystem:option_eq_dec
ChordSystem:Output
ChordSystem:payload
ChordSystem:_payload
ChordSystem:payload_eq_dec
ChordSystem:_payload_rect
ChordSystem:Ping
ChordSystem:Pong
ChordSystem:pred
ChordSystem:ptr
ChordSystem:query
ChordSystem:_query
ChordSystem:Rectify
ChordSystem:RectifyTick
ChordSystem:rectify_with
ChordSystem:recv_handler
ChordSystem:recv_handler_l
ChordSystem:recv_handler_labeling
ChordSystem:RecvMsg
ChordSystem:Request
ChordSystem:request_timeout_handler
ChordSystem:res
ChordSystem:schedule_rectify_with
ChordSystem:send_eq_dec
ChordSystem:send_keepalives
ChordSystem:SendKeepalives
ChordSystem:SetPred
ChordSystem:set_rectify_with
ChordSystem:sort_by_between
ChordSystem:sort_by_between_permutes
ChordSystem:Stabilize
ChordSystem:Stabilize2
ChordSystem:start_query
ChordSystem:StartRectify
ChordSystem:StartStabilize
ChordSystem:succ_list
ChordSystem:Tick
ChordSystem:tick_handler
ChordSystem:timeout
ChordSystem:_timeout
ChordSystem:Timeout
ChordSystem:timeout_effect
ChordSystem:timeout_eq_dec
ChordSystem:timeout_handler
ChordSystem:timeout_handler_eff
ChordSystem:timeout_handler_l
ChordSystem:timeout_handler_labeling
ChordSystem:_timeout_rect
ChordSystem:timeouts_in
ChordSystem:update_for_join
ChordSystem:update_pred
ChordSystem:update_query
ChordSystem:update_succ_list
chord_tick_invariant
chord_tick_pre_post
circular_wait
Classical_Prop:classic
classical:weak_until_until_or_always
clear_delayed_queries
clear_query
clear_rectify_with
client_addr
_client_payload
client_payload
clients_not_in_failed
Compare_dec:dec_ge
Compare_dec:dec_gt
Compare_dec:dec_le
Compare_dec:dec_lt
Compare_dec:le_dec
Compare_dec:le_gt_dec
Compare_dec:le_lt_dec
Compare_dec:lt_dec
Compare_dec:nat_compare_ge
Compare_dec:nat_compare_gt
Compare_dec:nat_compare_le
Compare_dec:nat_compare_lt
Compare_dec:not_ge
Compare_dec:not_gt
Compare_dec:not_le
Compare_dec:not_lt
CompareSpec
comparison
CompEq
CompGt
CompLt
CompOpp
CompOpp_iff
CompOpp_inj
CompOpp_involutive
compute_principals
compute_principals_correct
conj
cons
constrained_Request_not_cleared_by_recv_handler
cont_enabled
continuously_bound_on_local_measures_bounds_max
continuously_bound_on_local_measures_max_measure_bounded
continuously_forall_list_comm
continuously_zero_phase_two_error_phase_two
continuously_zero_total_leading_failed_nodes_implies_phase_one
correct_succs
counting_opt_error
cur_request
CurRequestAndKeepaliveTickClearedPossible
CurRequestClearedPossible
cur_request_join2_not_joined
cur_request_matches_joined
cur_request_timeouts_ok
cur_request_timeouts_ok'
cur_request_timeouts_ok'_complete
cur_request_timeouts_ok'_sound
cur_request_timeouts_related_fail
cur_request_timeouts_related_init
cur_request_timeouts_related_input
cur_request_timeouts_related_invariant
cur_request_timeouts_related_invariant_elim
cur_request_timeouts_related_keepalive
cur_request_timeouts_related_output
cur_request_timeouts_related_rectify
cur_request_timeouts_related_recv_invariant
cur_request_timeouts_related_request
cur_request_timeouts_related_start
cur_request_timeouts_related_tick
cur_request_valid
data
_data
dead_node
dead_node_channel_empties_out
dead_nodes_go_quiet
Decidable:decidable
Decidable:dec_not_not
Decidable:imp_simp
Dedup:dedup
Dedup:dedup_In
Dedup:in_dedup_was_in
Dedup:NoDup_dedup
define_msg_from_recv_step_equality
delayed_queries
delay_query
Deliver_client
Deliver_node
DetectFailure
do_delayed_queries
do_delayed_queries_definition
do_delayed_queries_never_clears_tick
do_delayed_queries_ptr
do_rectify
do_rectify_definition
e_fail
effective_Tick_occurred_sent_request
effective_Tick_sends_request
effective_Tick_sends_request'
empty_start_res
enabled
end_query
end_query_definition
eq
Eq
eq_add_S
eq_ind
eq_ind_r
EqNat:eq_nat
EqNat:eq_nat_eq
EqNat:eq_nat_is_eq
EqNat:eq_nat_refl
eq_rec
eq_rec_r
eq_rect
eq_refl
eq_sym
eq_trans
e_recv
error_decreases_at_merge_point
error_decreases_when_succs_right
error_means_merge_point_or_wrong_pred
e_send
e_timeout
event
eventually_idempotent
ex
ex_ind
ex_intro
failed_nodes
failed_nodes_eq
failed_nodes_never_added
failed_nodes_never_removed
fail_node
failure_constraint
false
False
False_ind
False_rec
False_rect
f_equal
f_equal_nat
FilterMap:filterMap
FilterMap:filterMap_all_None
FilterMap:filterMap_app
FilterMap:filterMap_In
FilterMap:In_filterMap
find_pred
find_succs
first_succ_and_second_distinct
first_succ_correct
first_succ_correct_invar
first_succ_correct_phase_two
first_succ_error
first_succ_error_always_nonincreasing
first_succ_error_nonincreasing
first_succ_improvement_suffices_local
first_succ_improves
first_succ_improves_improves_abj
first_succ_improves_pred_and_succ_improves
first_succ_is_best_succ
first_succ_same_until_improvement
first_succs_correct
first_succs_correct_succs_nonempty
fold_left_acc_comm
fold_left_max_comm
fold_max_const_is_const
forallb_exists
fst
ge
GetBestPredecessor
get_open_request_to_from_open_stabilize_request
get_open_stabilize_request_to_first_succ_from_req_to
GetPredAndSuccs
GetSuccList
global_measure
global_state
GotBestPredecessor
GotPredAndSuccs
GotSuccList
gt
Gt
Gt:gt_irrefl
Gt:gt_le_S
Gt:gt_not_le
Gt:gt_S_n
Gt:gt_Sn_O
handle_delayed_queries_GotPredAndSuccs_response_accurate
handle_delayed_queries_GotSuccList_response_accurate
handle_delayed_query
handle_msg
handle_msg_adds_tick_when_setting_joined
handle_msg_definition
handle_msg_never_clears_tick
handle_msg_ptr
handle_msg_stabilize_response_pred_worse_sets_succs
handle_query_req
handle_query_req_busy
handle_query_req_busy_definition
handle_query_req_GotPredAndSuccs_response_accurate
handle_query_req_GotSuccList_response_accurate
handle_query_res
handle_query_res_definition
handle_query_timeout
handle_query_timeout_definition
handle_rectify
handle_rectify_definition
handle_stabilize
handle_stabilize_definition
handle_stabilize_sends_Notify_None
handle_stabilize_sends_Notify_Some
has_dead_first_succ
has_dead_first_succ_implies_error_nonzero
has_first_succ
has_first_succ_inj
has_first_succ_intro
has_first_succ_sigma
has_first_succ_stable
has_first_succ_succ_list
hash_injective_invariant
hash_injective_on
has_pred
has_pred_eq
has_pred_intro
has_succ_has_pred_inv
has_succs
have_principals
hd_error_make_succs
hd_in_chop_succs
I
id
ideal
id_eq_dec
id_ltb
id_of
IDProp
if_branches_same
iff
iff_refl
iff_stepl
iff_sym
iff_trans
in_active_in_nodes
in_active_not_failed
in_channel_in_msgs
incoming_GotPredAndSuccs_with_a_after_p_causes_improvement
incoming_GotPredAndSuccs_with_pred_None_causes_improvement
in_concat
Ineffective
in_failed_in_nodes
inf_enabled
in_find_succs
inf_occurred
Info: read file ../verdi-chord/systems/chord/chord_stabilization.dpd
infseq:always
infseq:Always
infseq:always_always
infseq:always_and_tl
infseq:always_Cons
infseq:always_continuously
infseq:always_inf_often
infseq:always_inv
infseq:always_invar
infseq:always_monotonic
infseq:always_now
infseq:always_now'
infseq:always_true
infseq:and_tl
infseq:and_tl_comm
infseq:Cons
infseq:consecutive
infseq:continuously
infseq:continuously_and_tl
infseq:continuously_inf_often
infseq:continuously_invar
infseq:continuously_monotonic
infseq:cumul_eventually_always
infseq:cumul_inf_often_always
infseq:E0
infseq:E_next
infseq:eventually
infseq:eventually_Cons
infseq:eventually_ind
infseq:eventually_monotonic
infseq:eventually_monotonic_simple
infseq:eventually_next
infseq:eventually_or_tl_introl