-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
1340 lines (1333 loc) · 96.3 KB
/
index.html
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
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Index</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<table>
<tr>
<td>Global Index</td>
<td><a href="index.html#global_A">A</a></td>
<td><a href="index.html#global_B">B</a></td>
<td><a href="index.html#global_C">C</a></td>
<td><a href="index.html#global_D">D</a></td>
<td><a href="index.html#global_E">E</a></td>
<td><a href="index.html#global_F">F</a></td>
<td>G</td>
<td><a href="index.html#global_H">H</a></td>
<td><a href="index.html#global_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="index.html#global_M">M</a></td>
<td><a href="index.html#global_N">N</a></td>
<td><a href="index.html#global_O">O</a></td>
<td><a href="index.html#global_P">P</a></td>
<td>Q</td>
<td>R</td>
<td><a href="index.html#global_S">S</a></td>
<td><a href="index.html#global_T">T</a></td>
<td><a href="index.html#global_U">U</a></td>
<td><a href="index.html#global_V">V</a></td>
<td><a href="index.html#global_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#global_Z">Z</a></td>
<td>_</td>
<td><a href="index.html#global_*">other</a></td>
<td>(388 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
<td><a href="index.html#lemma_A">A</a></td>
<td><a href="index.html#lemma_B">B</a></td>
<td><a href="index.html#lemma_C">C</a></td>
<td><a href="index.html#lemma_D">D</a></td>
<td><a href="index.html#lemma_E">E</a></td>
<td><a href="index.html#lemma_F">F</a></td>
<td>G</td>
<td><a href="index.html#lemma_H">H</a></td>
<td><a href="index.html#lemma_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="index.html#lemma_M">M</a></td>
<td><a href="index.html#lemma_N">N</a></td>
<td><a href="index.html#lemma_O">O</a></td>
<td><a href="index.html#lemma_P">P</a></td>
<td>Q</td>
<td>R</td>
<td><a href="index.html#lemma_S">S</a></td>
<td><a href="index.html#lemma_T">T</a></td>
<td><a href="index.html#lemma_U">U</a></td>
<td><a href="index.html#lemma_V">V</a></td>
<td><a href="index.html#lemma_W">W</a></td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(187 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
<td><a href="index.html#constructor_A">A</a></td>
<td><a href="index.html#constructor_B">B</a></td>
<td><a href="index.html#constructor_C">C</a></td>
<td><a href="index.html#constructor_D">D</a></td>
<td><a href="index.html#constructor_E">E</a></td>
<td>F</td>
<td>G</td>
<td><a href="index.html#constructor_H">H</a></td>
<td><a href="index.html#constructor_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td><a href="index.html#constructor_N">N</a></td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="index.html#constructor_S">S</a></td>
<td><a href="index.html#constructor_T">T</a></td>
<td><a href="index.html#constructor_U">U</a></td>
<td>V</td>
<td><a href="index.html#constructor_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#constructor_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(111 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td><a href="index.html#notation_*">other</a></td>
<td>(17 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
<td><a href="index.html#inductive_A">A</a></td>
<td><a href="index.html#inductive_B">B</a></td>
<td><a href="index.html#inductive_C">C</a></td>
<td><a href="index.html#inductive_D">D</a></td>
<td>E</td>
<td>F</td>
<td>G</td>
<td><a href="index.html#inductive_H">H</a></td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td><a href="index.html#inductive_N">N</a></td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td><a href="index.html#inductive_T">T</a></td>
<td><a href="index.html#inductive_U">U</a></td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(21 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
<td><a href="index.html#definition_A">A</a></td>
<td><a href="index.html#definition_B">B</a></td>
<td><a href="index.html#definition_C">C</a></td>
<td><a href="index.html#definition_D">D</a></td>
<td><a href="index.html#definition_E">E</a></td>
<td><a href="index.html#definition_F">F</a></td>
<td>G</td>
<td><a href="index.html#definition_H">H</a></td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td><a href="index.html#definition_P">P</a></td>
<td>Q</td>
<td>R</td>
<td><a href="index.html#definition_S">S</a></td>
<td>T</td>
<td><a href="index.html#definition_U">U</a></td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(46 entries)</td>
</tr>
<tr>
<td>Library Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td><a href="index.html#library_D">D</a></td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#library_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td><a href="index.html#library_P">P</a></td>
<td>Q</td>
<td>R</td>
<td><a href="index.html#library_S">S</a></td>
<td>T</td>
<td>U</td>
<td><a href="index.html#library_V">V</a></td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(6 entries)</td>
</tr>
</table>
<hr/>
<h1>Global Index</h1>
<a name="global_A"></a><h2>A </h2>
<a href="aeval.html#aeval">aeval</a> [definition, in <a href="aeval.html">aeval</a>]<br/>
<a href="aexp.html#aexp">aexp</a> [inductive, in <a href="aexp.html">aexp</a>]<br/>
<a href="aexp_sub.html#aexp_sub">aexp_sub</a> [definition, in <a href="aexp_sub.html">aexp_sub</a>]<br/>
<a href="Af_plus.html#Af_plus">Af_plus</a> [constructor, in <a href="Af_plus.html">Af_plus</a>]<br/>
<a href="Af_mult.html#Af_mult">Af_mult</a> [constructor, in <a href="Af_mult.html">Af_mult</a>]<br/>
<a href="Af_minus.html#Af_minus">Af_minus</a> [constructor, in <a href="Af_minus.html">Af_minus</a>]<br/>
<a href="Af_num.html#Af_num">Af_num</a> [constructor, in <a href="Af_num.html">Af_num</a>]<br/>
<a href="Af_id.html#Af_id">Af_id</a> [constructor, in <a href="Af_id.html">Af_id</a>]<br/>
<a href="Aid.html#Aid">Aid</a> [constructor, in <a href="Aid.html">Aid</a>]<br/>
<a href="AId.html#AId">AId</a> [constructor, in <a href="AId.html">AId</a>]<br/>
<a href="aid.html#aid">aid</a> [inductive, in <a href="aid.html">aid</a>]<br/>
<a href="all_zero.html#all_zero">all_zero</a> [inductive, in <a href="all_zero.html">all_zero</a>]<br/>
<a href="AMinus.html#AMinus">AMinus</a> [constructor, in <a href="AMinus.html">AMinus</a>]<br/>
<a href="AMult.html#AMult">AMult</a> [constructor, in <a href="AMult.html">AMult</a>]<br/>
<a href="ANum.html#ANum">ANum</a> [constructor, in <a href="ANum.html">ANum</a>]<br/>
<a href="APlus.html#APlus">APlus</a> [constructor, in <a href="APlus.html">APlus</a>]<br/>
<a href="Assign.html#Assign">Assign</a> [constructor, in <a href="Assign.html">Assign</a>]<br/>
<a href="assign_equiv.html#assign_equiv">assign_equiv</a> [lemma, in <a href="assign_equiv.html">assign_equiv</a>]<br/>
<a href="assign_lift.html#assign_lift">assign_lift</a> [lemma, in <a href="assign_lift.html">assign_lift</a>]<br/>
<a href="ax_id_free.html#ax_id_free">ax_id_free</a> [inductive, in <a href="ax_id_free.html">ax_id_free</a>]<br/>
<a href="a_sub_eq.html#a_sub_eq">a_sub_eq</a> [lemma, in <a href="a_sub_eq.html">a_sub_eq</a>]<br/>
<a href="a_free_imp.html#a_free_imp">a_free_imp</a> [lemma, in <a href="a_free_imp.html">a_free_imp</a>]<br/>
<a href="a_free_eq.html#a_free_eq">a_free_eq</a> [lemma, in <a href="a_free_eq.html">a_free_eq</a>]<br/>
<br/><br/><a name="global_B"></a><h2>B </h2>
<a href="BAnd.html#BAnd">BAnd</a> [constructor, in <a href="BAnd.html">BAnd</a>]<br/>
<a href="BAssign.html#BAssign">BAssign</a> [constructor, in <a href="BAssign.html">BAssign</a>]<br/>
<a href="bassign_equiv.html#bassign_equiv">bassign_equiv</a> [lemma, in <a href="bassign_equiv.html">bassign_equiv</a>]<br/>
<a href="bassign_lift.html#bassign_lift">bassign_lift</a> [lemma, in <a href="bassign_lift.html">bassign_lift</a>]<br/>
<a href="bass_steps.html#bass_steps">bass_steps</a> [lemma, in <a href="bass_steps.html">bass_steps</a>]<br/>
<a href="BEq.html#BEq">BEq</a> [constructor, in <a href="BEq.html">BEq</a>]<br/>
<a href="beq_bid_false_iff.html#beq_bid_false_iff">beq_bid_false_iff</a> [lemma, in <a href="beq_bid_false_iff.html">beq_bid_false_iff</a>]<br/>
<a href="beq_aid_eq.html#beq_aid_eq">beq_aid_eq</a> [lemma, in <a href="beq_aid_eq.html">beq_aid_eq</a>]<br/>
<a href="beq_bid.html#beq_bid">beq_bid</a> [definition, in <a href="beq_bid.html">beq_bid</a>]<br/>
<a href="beq_aid.html#beq_aid">beq_aid</a> [definition, in <a href="beq_aid.html">beq_aid</a>]<br/>
<a href="beq_aid_false_iff.html#beq_aid_false_iff">beq_aid_false_iff</a> [lemma, in <a href="beq_aid_false_iff.html">beq_aid_false_iff</a>]<br/>
<a href="beq_aid_refl.html#beq_aid_refl">beq_aid_refl</a> [lemma, in <a href="beq_aid_refl.html">beq_aid_refl</a>]<br/>
<a href="beq_bid_refl.html#beq_bid_refl">beq_bid_refl</a> [lemma, in <a href="beq_bid_refl.html">beq_bid_refl</a>]<br/>
<a href="beq_bid_eq.html#beq_bid_eq">beq_bid_eq</a> [lemma, in <a href="beq_bid_eq.html">beq_bid_eq</a>]<br/>
<a href="beval.html#beval">beval</a> [definition, in <a href="beval.html">beval</a>]<br/>
<a href="bexp.html#bexp">bexp</a> [inductive, in <a href="bexp.html">bexp</a>]<br/>
<a href="bexp_sub.html#bexp_sub">bexp_sub</a> [definition, in <a href="bexp_sub.html">bexp_sub</a>]<br/>
<a href="bexp_sub_b.html#bexp_sub_b">bexp_sub_b</a> [definition, in <a href="bexp_sub_b.html">bexp_sub_b</a>]<br/>
<a href="BFalse.html#BFalse">BFalse</a> [constructor, in <a href="BFalse.html">BFalse</a>]<br/>
<a href="Bf_eq.html#Bf_eq">Bf_eq</a> [constructor, in <a href="Bf_eq.html">Bf_eq</a>]<br/>
<a href="Bf_true_b.html#Bf_true_b">Bf_true_b</a> [constructor, in <a href="Bf_true_b.html">Bf_true_b</a>]<br/>
<a href="Bf_false.html#Bf_false">Bf_false</a> [constructor, in <a href="Bf_false.html">Bf_false</a>]<br/>
<a href="Bf_id.html#Bf_id">Bf_id</a> [constructor, in <a href="Bf_id.html">Bf_id</a>]<br/>
<a href="Bf_le_b.html#Bf_le_b">Bf_le_b</a> [constructor, in <a href="Bf_le_b.html">Bf_le_b</a>]<br/>
<a href="Bf_le.html#Bf_le">Bf_le</a> [constructor, in <a href="Bf_le.html">Bf_le</a>]<br/>
<a href="Bf_and_b.html#Bf_and_b">Bf_and_b</a> [constructor, in <a href="Bf_and_b.html">Bf_and_b</a>]<br/>
<a href="Bf_false_b.html#Bf_false_b">Bf_false_b</a> [constructor, in <a href="Bf_false_b.html">Bf_false_b</a>]<br/>
<a href="Bf_eq_b.html#Bf_eq_b">Bf_eq_b</a> [constructor, in <a href="Bf_eq_b.html">Bf_eq_b</a>]<br/>
<a href="Bf_not_b.html#Bf_not_b">Bf_not_b</a> [constructor, in <a href="Bf_not_b.html">Bf_not_b</a>]<br/>
<a href="Bf_true.html#Bf_true">Bf_true</a> [constructor, in <a href="Bf_true.html">Bf_true</a>]<br/>
<a href="Bf_id_b.html#Bf_id_b">Bf_id_b</a> [constructor, in <a href="Bf_id_b.html">Bf_id_b</a>]<br/>
<a href="Bf_and.html#Bf_and">Bf_and</a> [constructor, in <a href="Bf_and.html">Bf_and</a>]<br/>
<a href="Bf_not.html#Bf_not">Bf_not</a> [constructor, in <a href="Bf_not.html">Bf_not</a>]<br/>
<a href="BGe.html#BGe">BGe</a> [definition, in <a href="BGe.html">BGe</a>]<br/>
<a href="BGt.html#BGt">BGt</a> [definition, in <a href="BGt.html">BGt</a>]<br/>
<a href="bicondition_b.html#bicondition_b">bicondition_b</a> [definition, in <a href="bicondition_b.html">bicondition_b</a>]<br/>
<a href="bicondition01.html#bicondition01">bicondition01</a> [definition, in <a href="bicondition01.html">bicondition01</a>]<br/>
<a href="Bid.html#Bid">Bid</a> [constructor, in <a href="Bid.html">Bid</a>]<br/>
<a href="BId.html#BId">BId</a> [constructor, in <a href="BId.html">BId</a>]<br/>
<a href="bid.html#bid">bid</a> [inductive, in <a href="bid.html">bid</a>]<br/>
<a href="BIff.html#BIff">BIff</a> [definition, in <a href="BIff.html">BIff</a>]<br/>
<a href="biff_imp.html#biff_imp">biff_imp</a> [lemma, in <a href="biff_imp.html">biff_imp</a>]<br/>
<a href="BLe.html#BLe">BLe</a> [constructor, in <a href="BLe.html">BLe</a>]<br/>
<a href="ble_nat.html#ble_nat">ble_nat</a> [definition, in <a href="ble_nat.html">ble_nat</a>]<br/>
<a href="BLt.html#BLt">BLt</a> [definition, in <a href="BLt.html">BLt</a>]<br/>
<a href="BNot.html#BNot">BNot</a> [constructor, in <a href="BNot.html">BNot</a>]<br/>
<a href="BOr.html#BOr">BOr</a> [definition, in <a href="BOr.html">BOr</a>]<br/>
<a href="bor_eq.html#bor_eq">bor_eq</a> [lemma, in <a href="bor_eq.html">bor_eq</a>]<br/>
<a href="BToss.html#BToss">BToss</a> [constructor, in <a href="BToss.html">BToss</a>]<br/>
<a href="btoss_lift.html#btoss_lift">btoss_lift</a> [lemma, in <a href="btoss_lift.html">btoss_lift</a>]<br/>
<a href="btoss_equiv.html#btoss_equiv">btoss_equiv</a> [lemma, in <a href="btoss_equiv.html">btoss_equiv</a>]<br/>
<a href="BTrue.html#BTrue">BTrue</a> [constructor, in <a href="BTrue.html">BTrue</a>]<br/>
<a href="bx_id_free.html#bx_id_free">bx_id_free</a> [inductive, in <a href="bx_id_free.html">bx_id_free</a>]<br/>
<a href="bx_bid_free.html#bx_bid_free">bx_bid_free</a> [inductive, in <a href="bx_bid_free.html">bx_bid_free</a>]<br/>
<a href="b_free_eq.html#b_free_eq">b_free_eq</a> [lemma, in <a href="b_free_eq.html">b_free_eq</a>]<br/>
<a href="b_sub_eq.html#b_sub_eq">b_sub_eq</a> [lemma, in <a href="b_sub_eq.html">b_sub_eq</a>]<br/>
<a href="b_free_eq_b.html#b_free_eq_b">b_free_eq_b</a> [lemma, in <a href="b_free_eq_b.html">b_free_eq_b</a>]<br/>
<a href="b_free_imp_b.html#b_free_imp_b">b_free_imp_b</a> [lemma, in <a href="b_free_imp_b.html">b_free_imp_b</a>]<br/>
<a href="b_sub_eq_b.html#b_sub_eq_b">b_sub_eq_b</a> [lemma, in <a href="b_sub_eq_b.html">b_sub_eq_b</a>]<br/>
<a href="b_free_imp.html#b_free_imp">b_free_imp</a> [lemma, in <a href="b_free_imp.html">b_free_imp</a>]<br/>
<br/><br/><a name="global_C"></a><h2>C </h2>
<a href="ceval.html#ceval">ceval</a> [inductive, in <a href="ceval.html">ceval</a>]<br/>
<a href="Cf_seq_b'.html#Cf_seq_b'">Cf_seq_b'</a> [constructor, in <a href="Cf_seq_b'.html">Cf_seq_b'</a>]<br/>
<a href="Cf_toss_b'.html#Cf_toss_b'">Cf_toss_b'</a> [constructor, in <a href="Cf_toss_b'.html">Cf_toss_b'</a>]<br/>
<a href="Cf_if_b'.html#Cf_if_b'">Cf_if_b'</a> [constructor, in <a href="Cf_if_b'.html">Cf_if_b'</a>]<br/>
<a href="Cf_ass_b'.html#Cf_ass_b'">Cf_ass_b'</a> [constructor, in <a href="Cf_ass_b'.html">Cf_ass_b'</a>]<br/>
<a href="Cf_skip.html#Cf_skip">Cf_skip</a> [constructor, in <a href="Cf_skip.html">Cf_skip</a>]<br/>
<a href="Cf_bass.html#Cf_bass">Cf_bass</a> [constructor, in <a href="Cf_bass.html">Cf_bass</a>]<br/>
<a href="Cf_seq_b.html#Cf_seq_b">Cf_seq_b</a> [constructor, in <a href="Cf_seq_b.html">Cf_seq_b</a>]<br/>
<a href="Cf_ass_b.html#Cf_ass_b">Cf_ass_b</a> [constructor, in <a href="Cf_ass_b.html">Cf_ass_b</a>]<br/>
<a href="Cf_skip_b.html#Cf_skip_b">Cf_skip_b</a> [constructor, in <a href="Cf_skip_b.html">Cf_skip_b</a>]<br/>
<a href="Cf_while_b'.html#Cf_while_b'">Cf_while_b'</a> [constructor, in <a href="Cf_while_b'.html">Cf_while_b'</a>]<br/>
<a href="Cf_btoss_b'.html#Cf_btoss_b'">Cf_btoss_b'</a> [constructor, in <a href="Cf_btoss_b'.html">Cf_btoss_b'</a>]<br/>
<a href="Cf_while.html#Cf_while">Cf_while</a> [constructor, in <a href="Cf_while.html">Cf_while</a>]<br/>
<a href="Cf_toss_b.html#Cf_toss_b">Cf_toss_b</a> [constructor, in <a href="Cf_toss_b.html">Cf_toss_b</a>]<br/>
<a href="Cf_btoss.html#Cf_btoss">Cf_btoss</a> [constructor, in <a href="Cf_btoss.html">Cf_btoss</a>]<br/>
<a href="Cf_while_b.html#Cf_while_b">Cf_while_b</a> [constructor, in <a href="Cf_while_b.html">Cf_while_b</a>]<br/>
<a href="Cf_bass_b'.html#Cf_bass_b'">Cf_bass_b'</a> [constructor, in <a href="Cf_bass_b'.html">Cf_bass_b'</a>]<br/>
<a href="Cf_skip_b'.html#Cf_skip_b'">Cf_skip_b'</a> [constructor, in <a href="Cf_skip_b'.html">Cf_skip_b'</a>]<br/>
<a href="Cf_if_b.html#Cf_if_b">Cf_if_b</a> [constructor, in <a href="Cf_if_b.html">Cf_if_b</a>]<br/>
<a href="Cf_if.html#Cf_if">Cf_if</a> [constructor, in <a href="Cf_if.html">Cf_if</a>]<br/>
<a href="Cf_btoss_b.html#Cf_btoss_b">Cf_btoss_b</a> [constructor, in <a href="Cf_btoss_b.html">Cf_btoss_b</a>]<br/>
<a href="Cf_seq.html#Cf_seq">Cf_seq</a> [constructor, in <a href="Cf_seq.html">Cf_seq</a>]<br/>
<a href="Cf_toss.html#Cf_toss">Cf_toss</a> [constructor, in <a href="Cf_toss.html">Cf_toss</a>]<br/>
<a href="Cf_bass_b.html#Cf_bass_b">Cf_bass_b</a> [constructor, in <a href="Cf_bass_b.html">Cf_bass_b</a>]<br/>
<a href="Cf_ass.html#Cf_ass">Cf_ass</a> [constructor, in <a href="Cf_ass.html">Cf_ass</a>]<br/>
<a href="com.html#com">com</a> [inductive, in <a href="com.html">com</a>]<br/>
<a href="Combine.html#Combine">Combine</a> [constructor, in <a href="Combine.html">Combine</a>]<br/>
<a href="com_id_free.html#com_id_free">com_id_free</a> [inductive, in <a href="com_id_free.html">com_id_free</a>]<br/>
<a href="com_bid_free.html#com_bid_free">com_bid_free</a> [inductive, in <a href="com_bid_free.html">com_bid_free</a>]<br/>
<a href="condition.html#condition">condition</a> [definition, in <a href="condition.html">condition</a>]<br/>
<a href="conditionF.html#conditionF">conditionF</a> [definition, in <a href="conditionF.html">conditionF</a>]<br/>
<a href="conditionT.html#conditionT">conditionT</a> [definition, in <a href="conditionT.html">conditionT</a>]<br/>
<a href="condition_on_1.html#condition_on_1">condition_on_1</a> [lemma, in <a href="condition_on_1.html">condition_on_1</a>]<br/>
<br/><br/><a name="global_D"></a><h2>D </h2>
<a href="deterministic.html#deterministic">deterministic</a> [inductive, in <a href="deterministic.html">deterministic</a>]<br/>
<a href="deterministic_combine.html#deterministic_combine">deterministic_combine</a> [lemma, in <a href="deterministic_combine.html">deterministic_combine</a>]<br/>
<a href="deterministic_split.html#deterministic_split">deterministic_split</a> [lemma, in <a href="deterministic_split.html">deterministic_split</a>]<br/>
<a href="det_lit.html#det_lit">det_lit</a> [constructor, in <a href="det_lit.html">det_lit</a>]<br/>
<a href="det_conj.html#det_conj">det_conj</a> [constructor, in <a href="det_conj.html">det_conj</a>]<br/>
<a href="dist.html#dist">dist</a> [inductive, in <a href="dist.html">dist</a>]<br/>
<a href="Distributions.html">Distributions</a> [library]<br/>
<a href="dist_update_true.html#dist_update_true">dist_update_true</a> [lemma, in <a href="dist_update_true.html">dist_update_true</a>]<br/>
<a href="dist_update_b.html#dist_update_b">dist_update_b</a> [definition, in <a href="dist_update_b.html">dist_update_b</a>]<br/>
<a href="dist_update.html#dist_update">dist_update</a> [definition, in <a href="dist_update.html">dist_update</a>]<br/>
<a href="dist_update_false.html#dist_update_false">dist_update_false</a> [lemma, in <a href="dist_update_false.html">dist_update_false</a>]<br/>
<a href="dist_update_b_permute.html#dist_update_b_permute">dist_update_b_permute</a> [lemma, in <a href="dist_update_b_permute.html">dist_update_b_permute</a>]<br/>
<a href="dist_update_non_interference.html#dist_update_non_interference">dist_update_non_interference</a> [lemma, in <a href="dist_update_non_interference.html">dist_update_non_interference</a>]<br/>
<a href="dist_update_prob_permute_b.html#dist_update_prob_permute_b">dist_update_prob_permute_b</a> [lemma, in <a href="dist_update_prob_permute_b.html">dist_update_prob_permute_b</a>]<br/>
<a href="divide_by_lt.html#divide_by_lt">divide_by_lt</a> [lemma, in <a href="divide_by_lt.html">divide_by_lt</a>]<br/>
<a href="dstate.html#dstate">dstate</a> [definition, in <a href="dstate.html">dstate</a>]<br/>
<a href="dst_equiv_unit_split.html#dst_equiv_unit_split">dst_equiv_unit_split</a> [lemma, in <a href="dst_equiv_unit_split.html">dst_equiv_unit_split</a>]<br/>
<a href="dst_equiv_trans.html#dst_equiv_trans">dst_equiv_trans</a> [lemma, in <a href="dst_equiv_trans.html">dst_equiv_trans</a>]<br/>
<a href="dst_equiv_refl.html#dst_equiv_refl">dst_equiv_refl</a> [lemma, in <a href="dst_equiv_refl.html">dst_equiv_refl</a>]<br/>
<a href="dst_merge.html#dst_merge">dst_merge</a> [lemma, in <a href="dst_merge.html">dst_merge</a>]<br/>
<a href="dst_equiv.html#dst_equiv">dst_equiv</a> [definition, in <a href="dst_equiv.html">dst_equiv</a>]<br/>
<a href="dst_comm.html#dst_comm">dst_comm</a> [lemma, in <a href="dst_comm.html">dst_comm</a>]<br/>
<a href="dst_equiv_combine.html#dst_equiv_combine">dst_equiv_combine</a> [lemma, in <a href="dst_equiv_combine.html">dst_equiv_combine</a>]<br/>
<a href="dst_comm_hexp.html#dst_comm_hexp">dst_comm_hexp</a> [lemma, in <a href="dst_comm_hexp.html">dst_comm_hexp</a>]<br/>
<a href="dst_assoc.html#dst_assoc">dst_assoc</a> [lemma, in <a href="dst_assoc.html">dst_assoc</a>]<br/>
<a href="dst_equiv_symm.html#dst_equiv_symm">dst_equiv_symm</a> [lemma, in <a href="dst_equiv_symm.html">dst_equiv_symm</a>]<br/>
<a href="dst_equiv_iff.html#dst_equiv_iff">dst_equiv_iff</a> [lemma, in <a href="dst_equiv_iff.html">dst_equiv_iff</a>]<br/>
<a href="dst_equiv_hexp.html#dst_equiv_hexp">dst_equiv_hexp</a> [definition, in <a href="dst_equiv_hexp.html">dst_equiv_hexp</a>]<br/>
<a href="dst_equiv_split.html#dst_equiv_split">dst_equiv_split</a> [lemma, in <a href="dst_equiv_split.html">dst_equiv_split</a>]<br/>
<a href="dst_equiv_eq.html#dst_equiv_eq">dst_equiv_eq</a> [lemma, in <a href="dst_equiv_eq.html">dst_equiv_eq</a>]<br/>
<br/><br/><a name="global_E"></a><h2>E </h2>
<a href="empty_dstate.html#empty_dstate">empty_dstate</a> [definition, in <a href="empty_dstate.html">empty_dstate</a>]<br/>
<a href="empty_state.html#empty_state">empty_state</a> [definition, in <a href="empty_state.html">empty_state</a>]<br/>
<a href="equidistant.html#equidistant">equidistant</a> [lemma, in <a href="equidistant.html">equidistant</a>]<br/>
<a href="E_Seq.html#E_Seq">E_Seq</a> [constructor, in <a href="E_Seq.html">E_Seq</a>]<br/>
<a href="E_Toss.html#E_Toss">E_Toss</a> [constructor, in <a href="E_Toss.html">E_Toss</a>]<br/>
<a href="E_Assign.html#E_Assign">E_Assign</a> [constructor, in <a href="E_Assign.html">E_Assign</a>]<br/>
<a href="E_WhileEnd.html#E_WhileEnd">E_WhileEnd</a> [constructor, in <a href="E_WhileEnd.html">E_WhileEnd</a>]<br/>
<a href="E_IfFalse.html#E_IfFalse">E_IfFalse</a> [constructor, in <a href="E_IfFalse.html">E_IfFalse</a>]<br/>
<a href="E_IfTrue.html#E_IfTrue">E_IfTrue</a> [constructor, in <a href="E_IfTrue.html">E_IfTrue</a>]<br/>
<a href="E_Skip.html#E_Skip">E_Skip</a> [constructor, in <a href="E_Skip.html">E_Skip</a>]<br/>
<a href="E_BToss.html#E_BToss">E_BToss</a> [constructor, in <a href="E_BToss.html">E_BToss</a>]<br/>
<a href="E_WhileLoop.html#E_WhileLoop">E_WhileLoop</a> [constructor, in <a href="E_WhileLoop.html">E_WhileLoop</a>]<br/>
<a href="E_BAssign.html#E_BAssign">E_BAssign</a> [constructor, in <a href="E_BAssign.html">E_BAssign</a>]<br/>
<a href="E_Lift.html#E_Lift">E_Lift</a> [constructor, in <a href="E_Lift.html">E_Lift</a>]<br/>
<br/><br/><a name="global_F"></a><h2>F </h2>
<a href="fork_on_b.html#fork_on_b">fork_on_b</a> [lemma, in <a href="fork_on_b.html">fork_on_b</a>]<br/>
<a href="fork_on_b_plus.html#fork_on_b_plus">fork_on_b_plus</a> [lemma, in <a href="fork_on_b_plus.html">fork_on_b_plus</a>]<br/>
<a href="free.html#free">free</a> [definition, in <a href="free.html">free</a>]<br/>
<a href="free_eq_b.html#free_eq_b">free_eq_b</a> [lemma, in <a href="free_eq_b.html">free_eq_b</a>]<br/>
<a href="free_b.html#free_b">free_b</a> [definition, in <a href="free_b.html">free_b</a>]<br/>
<a href="free_eq.html#free_eq">free_eq</a> [lemma, in <a href="free_eq.html">free_eq</a>]<br/>
<a href="free_then_unassigned.html#free_then_unassigned">free_then_unassigned</a> [lemma, in <a href="free_then_unassigned.html">free_then_unassigned</a>]<br/>
<br/><br/><a name="global_H"></a><h2>H </h2>
<a href="HAnd.html#HAnd">HAnd</a> [constructor, in <a href="HAnd.html">HAnd</a>]<br/>
<a href="HEq.html#HEq">HEq</a> [constructor, in <a href="HEq.html">HEq</a>]<br/>
<a href="heval.html#heval">heval</a> [definition, in <a href="heval.html">heval</a>]<br/>
<a href="hexp.html#hexp">hexp</a> [inductive, in <a href="hexp.html">hexp</a>]<br/>
<a href="hexp_sub_b.html#hexp_sub_b">hexp_sub_b</a> [definition, in <a href="hexp_sub_b.html">hexp_sub_b</a>]<br/>
<a href="hexp_sub.html#hexp_sub">hexp_sub</a> [definition, in <a href="hexp_sub.html">hexp_sub</a>]<br/>
<a href="HFalse.html#HFalse">HFalse</a> [definition, in <a href="HFalse.html">HFalse</a>]<br/>
<a href="Hf_gt.html#Hf_gt">Hf_gt</a> [constructor, in <a href="Hf_gt.html">Hf_gt</a>]<br/>
<a href="Hf_gt_b.html#Hf_gt_b">Hf_gt_b</a> [constructor, in <a href="Hf_gt_b.html">Hf_gt_b</a>]<br/>
<a href="Hf_lt.html#Hf_lt">Hf_lt</a> [constructor, in <a href="Hf_lt.html">Hf_lt</a>]<br/>
<a href="Hf_and.html#Hf_and">Hf_and</a> [constructor, in <a href="Hf_and.html">Hf_and</a>]<br/>
<a href="Hf_eq_b.html#Hf_eq_b">Hf_eq_b</a> [constructor, in <a href="Hf_eq_b.html">Hf_eq_b</a>]<br/>
<a href="Hf_or.html#Hf_or">Hf_or</a> [constructor, in <a href="Hf_or.html">Hf_or</a>]<br/>
<a href="Hf_and_b.html#Hf_and_b">Hf_and_b</a> [constructor, in <a href="Hf_and_b.html">Hf_and_b</a>]<br/>
<a href="Hf_or_b.html#Hf_or_b">Hf_or_b</a> [constructor, in <a href="Hf_or_b.html">Hf_or_b</a>]<br/>
<a href="Hf_lt_b.html#Hf_lt_b">Hf_lt_b</a> [constructor, in <a href="Hf_lt_b.html">Hf_lt_b</a>]<br/>
<a href="Hf_eq.html#Hf_eq">Hf_eq</a> [constructor, in <a href="Hf_eq.html">Hf_eq</a>]<br/>
<a href="HGe.html#HGe">HGe</a> [definition, in <a href="HGe.html">HGe</a>]<br/>
<a href="HGe_simpl.html#HGe_simpl">HGe_simpl</a> [lemma, in <a href="HGe_simpl.html">HGe_simpl</a>]<br/>
<a href="HGt.html#HGt">HGt</a> [constructor, in <a href="HGt.html">HGt</a>]<br/>
<a href="HIf.html#HIf">HIf</a> [definition, in <a href="HIf.html">HIf</a>]<br/>
<a href="HLe.html#HLe">HLe</a> [definition, in <a href="HLe.html">HLe</a>]<br/>
<a href="HLe_simpl.html#HLe_simpl">HLe_simpl</a> [lemma, in <a href="HLe_simpl.html">HLe_simpl</a>]<br/>
<a href="HLt.html#HLt">HLt</a> [constructor, in <a href="HLt.html">HLt</a>]<br/>
<a href="HNe.html#HNe">HNe</a> [definition, in <a href="HNe.html">HNe</a>]<br/>
<a href="HNe_simpl.html#HNe_simpl">HNe_simpl</a> [lemma, in <a href="HNe_simpl.html">HNe_simpl</a>]<br/>
<a href="HNot.html#HNot">HNot</a> [definition, in <a href="HNot.html">HNot</a>]<br/>
<a href="hoare_toss.html#hoare_toss">hoare_toss</a> [lemma, in <a href="hoare_toss.html">hoare_toss</a>]<br/>
<a href="hoare_if_true.html#hoare_if_true">hoare_if_true</a> [lemma, in <a href="hoare_if_true.html">hoare_if_true</a>]<br/>
<a href="hoare_if_gen.html#hoare_if_gen">hoare_if_gen</a> [lemma, in <a href="hoare_if_gen.html">hoare_if_gen</a>]<br/>
<a href="hoare_while_end.html#hoare_while_end">hoare_while_end</a> [lemma, in <a href="hoare_while_end.html">hoare_while_end</a>]<br/>
<a href="hoare_pre_false.html#hoare_pre_false">hoare_pre_false</a> [lemma, in <a href="hoare_pre_false.html">hoare_pre_false</a>]<br/>
<a href="hoare_post_true.html#hoare_post_true">hoare_post_true</a> [lemma, in <a href="hoare_post_true.html">hoare_post_true</a>]<br/>
<a href="hoare_skip.html#hoare_skip">hoare_skip</a> [lemma, in <a href="hoare_skip.html">hoare_skip</a>]<br/>
<a href="hoare_if_det.html#hoare_if_det">hoare_if_det</a> [lemma, in <a href="hoare_if_det.html">hoare_if_det</a>]<br/>
<a href="hoare_asgn_free.html#hoare_asgn_free">hoare_asgn_free</a> [lemma, in <a href="hoare_asgn_free.html">hoare_asgn_free</a>]<br/>
<a href="hoare_seq.html#hoare_seq">hoare_seq</a> [lemma, in <a href="hoare_seq.html">hoare_seq</a>]<br/>
<a href="hoare_toss_b.html#hoare_toss_b">hoare_toss_b</a> [lemma, in <a href="hoare_toss_b.html">hoare_toss_b</a>]<br/>
<a href="hoare_if_gen'.html#hoare_if_gen'">hoare_if_gen'</a> [lemma, in <a href="hoare_if_gen'.html">hoare_if_gen'</a>]<br/>
<a href="hoare_while_gen.html#hoare_while_gen">hoare_while_gen</a> [lemma, in <a href="hoare_while_gen.html">hoare_while_gen</a>]<br/>
<a href="hoare_while_prob.html#hoare_while_prob">hoare_while_prob</a> [lemma, in <a href="hoare_while_prob.html">hoare_while_prob</a>]<br/>
<a href="hoare_if_prob.html#hoare_if_prob">hoare_if_prob</a> [lemma, in <a href="hoare_if_prob.html">hoare_if_prob</a>]<br/>
<a href="hoare_asgn_b.html#hoare_asgn_b">hoare_asgn_b</a> [lemma, in <a href="hoare_asgn_b.html">hoare_asgn_b</a>]<br/>
<a href="hoare_if_false.html#hoare_if_false">hoare_if_false</a> [lemma, in <a href="hoare_if_false.html">hoare_if_false</a>]<br/>
<a href="hoare_asgn_free_b.html#hoare_asgn_free_b">hoare_asgn_free_b</a> [lemma, in <a href="hoare_asgn_free_b.html">hoare_asgn_free_b</a>]<br/>
<a href="hoare_if_prob'.html#hoare_if_prob'">hoare_if_prob'</a> [lemma, in <a href="hoare_if_prob'.html">hoare_if_prob'</a>]<br/>
<a href="hoare_consequence_post.html#hoare_consequence_post">hoare_consequence_post</a> [lemma, in <a href="hoare_consequence_post.html">hoare_consequence_post</a>]<br/>
<a href="hoare_while_det.html#hoare_while_det">hoare_while_det</a> [lemma, in <a href="hoare_while_det.html">hoare_while_det</a>]<br/>
<a href="hoare_asgn.html#hoare_asgn">hoare_asgn</a> [lemma, in <a href="hoare_asgn.html">hoare_asgn</a>]<br/>
<a href="hoare_triple.html#hoare_triple">hoare_triple</a> [definition, in <a href="hoare_triple.html">hoare_triple</a>]<br/>
<a href="hoare_if_unscaled.html#hoare_if_unscaled">hoare_if_unscaled</a> [lemma, in <a href="hoare_if_unscaled.html">hoare_if_unscaled</a>]<br/>
<a href="hoare_consequence.html#hoare_consequence">hoare_consequence</a> [lemma, in <a href="hoare_consequence.html">hoare_consequence</a>]<br/>
<a href="hoare_consequence_pre.html#hoare_consequence_pre">hoare_consequence_pre</a> [lemma, in <a href="hoare_consequence_pre.html">hoare_consequence_pre</a>]<br/>
<a href="HOr.html#HOr">HOr</a> [constructor, in <a href="HOr.html">HOr</a>]<br/>
<a href="HTrue.html#HTrue">HTrue</a> [definition, in <a href="HTrue.html">HTrue</a>]<br/>
<a href="hx_id_free.html#hx_id_free">hx_id_free</a> [inductive, in <a href="hx_id_free.html">hx_id_free</a>]<br/>
<a href="hx_bid_free.html#hx_bid_free">hx_bid_free</a> [inductive, in <a href="hx_bid_free.html">hx_bid_free</a>]<br/>
<a href="h_sub_eq_b.html#h_sub_eq_b">h_sub_eq_b</a> [lemma, in <a href="h_sub_eq_b.html">h_sub_eq_b</a>]<br/>
<a href="h_sub_eq.html#h_sub_eq">h_sub_eq</a> [lemma, in <a href="h_sub_eq.html">h_sub_eq</a>]<br/>
<a href="h_implies.html#h_implies">h_implies</a> [definition, in <a href="h_implies.html">h_implies</a>]<br/>
<br/><br/><a name="global_I"></a><h2>I </h2>
<a href="If.html#If">If</a> [constructor, in <a href="If.html">If</a>]<br/>
<a href="if_false_equiv.html#if_false_equiv">if_false_equiv</a> [lemma, in <a href="if_false_equiv.html">if_false_equiv</a>]<br/>
<a href="if_equiv.html#if_equiv">if_equiv</a> [lemma, in <a href="if_equiv.html">if_equiv</a>]<br/>
<a href="if_true_lift.html#if_true_lift">if_true_lift</a> [lemma, in <a href="if_true_lift.html">if_true_lift</a>]<br/>
<a href="if_false_lift.html#if_false_lift">if_false_lift</a> [lemma, in <a href="if_false_lift.html">if_false_lift</a>]<br/>
<a href="if_steps.html#if_steps">if_steps</a> [lemma, in <a href="if_steps.html">if_steps</a>]<br/>
<a href="if_true_equiv.html#if_true_equiv">if_true_equiv</a> [lemma, in <a href="if_true_equiv.html">if_true_equiv</a>]<br/>
<a href="Intervals.html">Intervals</a> [library]<br/>
<a href="in_0_1_open.html#in_0_1_open">in_0_1_open</a> [lemma, in <a href="in_0_1_open.html">in_0_1_open</a>]<br/>
<a href="in_0_1_closed.html#in_0_1_closed">in_0_1_closed</a> [lemma, in <a href="in_0_1_closed.html">in_0_1_closed</a>]<br/>
<br/><br/><a name="global_M"></a><h2>M </h2>
<a href="mult_stable.html#mult_stable">mult_stable</a> [lemma, in <a href="mult_stable.html">mult_stable</a>]<br/>
<a href="mult_le_0_compat.html#mult_le_0_compat">mult_le_0_compat</a> [lemma, in <a href="mult_le_0_compat.html">mult_le_0_compat</a>]<br/>
<a href="mult_lt_0_compat.html#mult_lt_0_compat">mult_lt_0_compat</a> [lemma, in <a href="mult_lt_0_compat.html">mult_lt_0_compat</a>]<br/>
<a href="mult_by_lt_1.html#mult_by_lt_1">mult_by_lt_1</a> [lemma, in <a href="mult_by_lt_1.html">mult_by_lt_1</a>]<br/>
<br/><br/><a name="global_N"></a><h2>N </h2>
<a href="nd_conj.html#nd_conj">nd_conj</a> [constructor, in <a href="nd_conj.html">nd_conj</a>]<br/>
<a href="nd_eq.html#nd_eq">nd_eq</a> [constructor, in <a href="nd_eq.html">nd_eq</a>]<br/>
<a href="nd_gt.html#nd_gt">nd_gt</a> [constructor, in <a href="nd_gt.html">nd_gt</a>]<br/>
<a href="nd_lt.html#nd_lt">nd_lt</a> [constructor, in <a href="nd_lt.html">nd_lt</a>]<br/>
<a href="negation_flip.html#negation_flip">negation_flip</a> [lemma, in <a href="negation_flip.html">negation_flip</a>]<br/>
<a href="neg_b_all_zero.html#neg_b_all_zero">neg_b_all_zero</a> [lemma, in <a href="neg_b_all_zero.html">neg_b_all_zero</a>]<br/>
<a href="non_probabilistic.html#non_probabilistic">non_probabilistic</a> [inductive, in <a href="non_probabilistic.html">non_probabilistic</a>]<br/>
<a href="non_disjunctive.html#non_disjunctive">non_disjunctive</a> [inductive, in <a href="non_disjunctive.html">non_disjunctive</a>]<br/>
<a href="non_disjunctive_combine.html#non_disjunctive_combine">non_disjunctive_combine</a> [lemma, in <a href="non_disjunctive_combine.html">non_disjunctive_combine</a>]<br/>
<a href="non_probabilistic_split.html#non_probabilistic_split">non_probabilistic_split</a> [lemma, in <a href="non_probabilistic_split.html">non_probabilistic_split</a>]<br/>
<a href="np_disj.html#np_disj">np_disj</a> [constructor, in <a href="np_disj.html">np_disj</a>]<br/>
<a href="np_0.html#np_0">np_0</a> [constructor, in <a href="np_0.html">np_0</a>]<br/>
<a href="np_1.html#np_1">np_1</a> [constructor, in <a href="np_1.html">np_1</a>]<br/>
<a href="np_conj.html#np_conj">np_conj</a> [constructor, in <a href="np_conj.html">np_conj</a>]<br/>
<br/><br/><a name="global_O"></a><h2>O </h2>
<a href="one_minus_p.html#one_minus_p">one_minus_p</a> [lemma, in <a href="one_minus_p.html">one_minus_p</a>]<br/>
<br/><br/><a name="global_P"></a><h2>P </h2>
<a href="plus_by_gt_0.html#plus_by_gt_0">plus_by_gt_0</a> [lemma, in <a href="plus_by_gt_0.html">plus_by_gt_0</a>]<br/>
<a href="prb_false.html#prb_false">prb_false</a> [lemma, in <a href="prb_false.html">prb_false</a>]<br/>
<a href="prb_true.html#prb_true">prb_true</a> [lemma, in <a href="prb_true.html">prb_true</a>]<br/>
<a href="prb_complement_0.html#prb_complement_0">prb_complement_0</a> [lemma, in <a href="prb_complement_0.html">prb_complement_0</a>]<br/>
<a href="prb_complement_1.html#prb_complement_1">prb_complement_1</a> [lemma, in <a href="prb_complement_1.html">prb_complement_1</a>]<br/>
<a href="PrImp.html">PrImp</a> [library]<br/>
<a href="probability.html#probability">probability</a> [definition, in <a href="probability.html">probability</a>]<br/>
<a href="probability_preserved.html#probability_preserved">probability_preserved</a> [lemma, in <a href="probability_preserved.html">probability_preserved</a>]<br/>
<a href="prob_update.html#prob_update">prob_update</a> [definition, in <a href="prob_update.html">prob_update</a>]<br/>
<a href="prob_update_equiv.html#prob_update_equiv">prob_update_equiv</a> [lemma, in <a href="prob_update_equiv.html">prob_update_equiv</a>]<br/>
<a href="prob_update_b_equiv.html#prob_update_b_equiv">prob_update_b_equiv</a> [lemma, in <a href="prob_update_b_equiv.html">prob_update_b_equiv</a>]<br/>
<a href="prob_update_non_interference.html#prob_update_non_interference">prob_update_non_interference</a> [lemma, in <a href="prob_update_non_interference.html">prob_update_non_interference</a>]<br/>
<a href="prob_update_0.html#prob_update_0">prob_update_0</a> [lemma, in <a href="prob_update_0.html">prob_update_0</a>]<br/>
<a href="prob_update_1.html#prob_update_1">prob_update_1</a> [lemma, in <a href="prob_update_1.html">prob_update_1</a>]<br/>
<a href="prob_update_F.html#prob_update_F">prob_update_F</a> [lemma, in <a href="prob_update_F.html">prob_update_F</a>]<br/>
<a href="prob_update_T.html#prob_update_T">prob_update_T</a> [lemma, in <a href="prob_update_T.html">prob_update_T</a>]<br/>
<a href="prob_update_b.html#prob_update_b">prob_update_b</a> [definition, in <a href="prob_update_b.html">prob_update_b</a>]<br/>
<a href="pr_combine.html#pr_combine">pr_combine</a> [lemma, in <a href="pr_combine.html">pr_combine</a>]<br/>
<a href="pr_strengthen_0.html#pr_strengthen_0">pr_strengthen_0</a> [lemma, in <a href="pr_strengthen_0.html">pr_strengthen_0</a>]<br/>
<a href="pr_weaken.html#pr_weaken">pr_weaken</a> [lemma, in <a href="pr_weaken.html">pr_weaken</a>]<br/>
<a href="pr_conj_1.html#pr_conj_1">pr_conj_1</a> [lemma, in <a href="pr_conj_1.html">pr_conj_1</a>]<br/>
<a href="pr_sub_b.html#pr_sub_b">pr_sub_b</a> [lemma, in <a href="pr_sub_b.html">pr_sub_b</a>]<br/>
<a href="pr_tautology.html#pr_tautology">pr_tautology</a> [lemma, in <a href="pr_tautology.html">pr_tautology</a>]<br/>
<a href="pr_equivalence.html#pr_equivalence">pr_equivalence</a> [lemma, in <a href="pr_equivalence.html">pr_equivalence</a>]<br/>
<a href="pr_normality.html#pr_normality">pr_normality</a> [lemma, in <a href="pr_normality.html">pr_normality</a>]<br/>
<a href="pr_ge_bound.html#pr_ge_bound">pr_ge_bound</a> [lemma, in <a href="pr_ge_bound.html">pr_ge_bound</a>]<br/>
<a href="pr_sub.html#pr_sub">pr_sub</a> [lemma, in <a href="pr_sub.html">pr_sub</a>]<br/>
<a href="pr_weaken_1.html#pr_weaken_1">pr_weaken_1</a> [lemma, in <a href="pr_weaken_1.html">pr_weaken_1</a>]<br/>
<a href="pr_conj_1_l.html#pr_conj_1_l">pr_conj_1_l</a> [lemma, in <a href="pr_conj_1_l.html">pr_conj_1_l</a>]<br/>
<a href="pr_conj_1_r.html#pr_conj_1_r">pr_conj_1_r</a> [lemma, in <a href="pr_conj_1_r.html">pr_conj_1_r</a>]<br/>
<a href="pr_disjunction.html#pr_disjunction">pr_disjunction</a> [lemma, in <a href="pr_disjunction.html">pr_disjunction</a>]<br/>
<a href="pr_conj_0_l.html#pr_conj_0_l">pr_conj_0_l</a> [lemma, in <a href="pr_conj_0_l.html">pr_conj_0_l</a>]<br/>
<a href="pr_conj_0_r.html#pr_conj_0_r">pr_conj_0_r</a> [lemma, in <a href="pr_conj_0_r.html">pr_conj_0_r</a>]<br/>
<a href="pr_complement_0.html#pr_complement_0">pr_complement_0</a> [lemma, in <a href="pr_complement_0.html">pr_complement_0</a>]<br/>
<a href="pr_complement_1.html#pr_complement_1">pr_complement_1</a> [lemma, in <a href="pr_complement_1.html">pr_complement_1</a>]<br/>
<a href="pr_conj_le_l.html#pr_conj_le_l">pr_conj_le_l</a> [lemma, in <a href="pr_conj_le_l.html">pr_conj_le_l</a>]<br/>
<a href="pr_conj_le_r.html#pr_conj_le_r">pr_conj_le_r</a> [lemma, in <a href="pr_conj_le_r.html">pr_conj_le_r</a>]<br/>
<a href="pr_totality.html#pr_totality">pr_totality</a> [lemma, in <a href="pr_totality.html">pr_totality</a>]<br/>
<a href="pr_addition.html#pr_addition">pr_addition</a> [lemma, in <a href="pr_addition.html">pr_addition</a>]<br/>
<a href="pr_strengthen.html#pr_strengthen">pr_strengthen</a> [lemma, in <a href="pr_strengthen.html">pr_strengthen</a>]<br/>
<a href="pr_disj_ge_l.html#pr_disj_ge_l">pr_disj_ge_l</a> [lemma, in <a href="pr_disj_ge_l.html">pr_disj_ge_l</a>]<br/>
<a href="pr_disj_ge_r.html#pr_disj_ge_r">pr_disj_ge_r</a> [lemma, in <a href="pr_disj_ge_r.html">pr_disj_ge_r</a>]<br/>
<a href="pr_unit.html#pr_unit">pr_unit</a> [lemma, in <a href="pr_unit.html">pr_unit</a>]<br/>
<a href="pr_contradiction.html#pr_contradiction">pr_contradiction</a> [lemma, in <a href="pr_contradiction.html">pr_contradiction</a>]<br/>
<a href="pr_union_bound.html#pr_union_bound">pr_union_bound</a> [lemma, in <a href="pr_union_bound.html">pr_union_bound</a>]<br/>
<a href="pr_split_0.html#pr_split_0">pr_split_0</a> [lemma, in <a href="pr_split_0.html">pr_split_0</a>]<br/>
<a href="pr_split_1.html#pr_split_1">pr_split_1</a> [lemma, in <a href="pr_split_1.html">pr_split_1</a>]<br/>
<a href="pr_complement.html#pr_complement">pr_complement</a> [lemma, in <a href="pr_complement.html">pr_complement</a>]<br/>
<br/><br/><a name="global_S"></a><h2>S </h2>
<a href="scale.html#scale">scale</a> [definition, in <a href="scale.html">scale</a>]<br/>
<a href="scale_equiv_0.html#scale_equiv_0">scale_equiv_0</a> [lemma, in <a href="scale_equiv_0.html">scale_equiv_0</a>]<br/>
<a href="scale_equiv_1.html#scale_equiv_1">scale_equiv_1</a> [lemma, in <a href="scale_equiv_1.html">scale_equiv_1</a>]<br/>
<a href="scale_twice.html#scale_twice">scale_twice</a> [lemma, in <a href="scale_twice.html">scale_twice</a>]<br/>
<a href="scale_1.html#scale_1">scale_1</a> [lemma, in <a href="scale_1.html">scale_1</a>]<br/>
<a href="scale_cond.html#scale_cond">scale_cond</a> [lemma, in <a href="scale_cond.html">scale_cond</a>]<br/>
<a href="scale_eq.html#scale_eq">scale_eq</a> [lemma, in <a href="scale_eq.html">scale_eq</a>]<br/>
<a href="scale_equiv_0'.html#scale_equiv_0'">scale_equiv_0'</a> [lemma, in <a href="scale_equiv_0'.html">scale_equiv_0'</a>]<br/>
<a href="scale_gt.html#scale_gt">scale_gt</a> [lemma, in <a href="scale_gt.html">scale_gt</a>]<br/>
<a href="scale_equiv_1'.html#scale_equiv_1'">scale_equiv_1'</a> [lemma, in <a href="scale_equiv_1'.html">scale_equiv_1'</a>]<br/>
<a href="scale_inversion.html#scale_inversion">scale_inversion</a> [lemma, in <a href="scale_inversion.html">scale_inversion</a>]<br/>
<a href="scale_lt.html#scale_lt">scale_lt</a> [lemma, in <a href="scale_lt.html">scale_lt</a>]<br/>
<a href="Seq.html#Seq">Seq</a> [constructor, in <a href="Seq.html">Seq</a>]<br/>
<a href="seq_lift.html#seq_lift">seq_lift</a> [lemma, in <a href="seq_lift.html">seq_lift</a>]<br/>
<a href="seq_equiv.html#seq_equiv">seq_equiv</a> [lemma, in <a href="seq_equiv.html">seq_equiv</a>]<br/>
<a href="SfLib.html">SfLib</a> [library]<br/>
<a href="Skip.html#Skip">Skip</a> [constructor, in <a href="Skip.html">Skip</a>]<br/>
<a href="skip_lift.html#skip_lift">skip_lift</a> [lemma, in <a href="skip_lift.html">skip_lift</a>]<br/>
<a href="skip_equiv.html#skip_equiv">skip_equiv</a> [lemma, in <a href="skip_equiv.html">skip_equiv</a>]<br/>
<a href="state.html#state">state</a> [definition, in <a href="state.html">state</a>]<br/>
<a href="step_split.html#step_split">step_split</a> [lemma, in <a href="step_split.html">step_split</a>]<br/>
<a href="step_deterministic.html#step_deterministic">step_deterministic</a> [lemma, in <a href="step_deterministic.html">step_deterministic</a>]<br/>
<a href="Style.html">Style</a> [library]<br/>
<a href="sub_over_condition.html#sub_over_condition">sub_over_condition</a> [lemma, in <a href="sub_over_condition.html">sub_over_condition</a>]<br/>
<a href="sum_to_gt_0.html#sum_to_gt_0">sum_to_gt_0</a> [lemma, in <a href="sum_to_gt_0.html">sum_to_gt_0</a>]<br/>
<a href="sum_to_0.html#sum_to_0">sum_to_0</a> [lemma, in <a href="sum_to_0.html">sum_to_0</a>]<br/>
<a href="sum_to_1.html#sum_to_1">sum_to_1</a> [lemma, in <a href="sum_to_1.html">sum_to_1</a>]<br/>
<br/><br/><a name="global_T"></a><h2>T </h2>
<a href="terminates_in.html#terminates_in">terminates_in</a> [inductive, in <a href="terminates_in.html">terminates_in</a>]<br/>
<a href="term_split.html#term_split">term_split</a> [lemma, in <a href="term_split.html">term_split</a>]<br/>
<a href="term_combine.html#term_combine">term_combine</a> [lemma, in <a href="term_combine.html">term_combine</a>]<br/>
<a href="term_0.html#term_0">term_0</a> [constructor, in <a href="term_0.html">term_0</a>]<br/>
<a href="term_S.html#term_S">term_S</a> [constructor, in <a href="term_S.html">term_S</a>]<br/>
<a href="Toss.html#Toss">Toss</a> [constructor, in <a href="Toss.html">Toss</a>]<br/>
<a href="toss_equiv.html#toss_equiv">toss_equiv</a> [lemma, in <a href="toss_equiv.html">toss_equiv</a>]<br/>
<a href="toss_lift.html#toss_lift">toss_lift</a> [lemma, in <a href="toss_lift.html">toss_lift</a>]<br/>
<br/><br/><a name="global_U"></a><h2>U </h2>
<a href="unassigned.html#unassigned">unassigned</a> [inductive, in <a href="unassigned.html">unassigned</a>]<br/>
<a href="Unit.html#Unit">Unit</a> [constructor, in <a href="Unit.html">Unit</a>]<br/>
<a href="update.html#update">update</a> [definition, in <a href="update.html">update</a>]<br/>
<a href="update_interpermute.html#update_interpermute">update_interpermute</a> [lemma, in <a href="update_interpermute.html">update_interpermute</a>]<br/>
<a href="update_eq.html#update_eq">update_eq</a> [lemma, in <a href="update_eq.html">update_eq</a>]<br/>
<a href="update_permute_b.html#update_permute_b">update_permute_b</a> [lemma, in <a href="update_permute_b.html">update_permute_b</a>]<br/>
<a href="update_equiv_b.html#update_equiv_b">update_equiv_b</a> [lemma, in <a href="update_equiv_b.html">update_equiv_b</a>]<br/>
<a href="update_neq.html#update_neq">update_neq</a> [lemma, in <a href="update_neq.html">update_neq</a>]<br/>
<a href="update_same.html#update_same">update_same</a> [lemma, in <a href="update_same.html">update_same</a>]<br/>
<a href="update_permute.html#update_permute">update_permute</a> [lemma, in <a href="update_permute.html">update_permute</a>]<br/>
<a href="update_b.html#update_b">update_b</a> [definition, in <a href="update_b.html">update_b</a>]<br/>
<a href="update_equiv.html#update_equiv">update_equiv</a> [lemma, in <a href="update_equiv.html">update_equiv</a>]<br/>
<a href="update_non_interference.html#update_non_interference">update_non_interference</a> [lemma, in <a href="update_non_interference.html">update_non_interference</a>]<br/>
<br/><br/><a name="global_V"></a><h2>V </h2>
<a href="vacuous_P_l.html#vacuous_P_l">vacuous_P_l</a> [lemma, in <a href="vacuous_P_l.html">vacuous_P_l</a>]<br/>
<a href="vacuous_P_r.html#vacuous_P_r">vacuous_P_r</a> [lemma, in <a href="vacuous_P_r.html">vacuous_P_r</a>]<br/>
<a href="vacuous_P.html#vacuous_P">vacuous_P</a> [lemma, in <a href="vacuous_P.html">vacuous_P</a>]<br/>
<a href="VPHL.html">VPHL</a> [library]<br/>
<br/><br/><a name="global_W"></a><h2>W </h2>
<a href="While.html#While">While</a> [constructor, in <a href="While.html">While</a>]<br/>
<a href="while_end.html#while_end">while_end</a> [lemma, in <a href="while_end.html">while_end</a>]<br/>
<a href="while_terminates.html#while_terminates">while_terminates</a> [lemma, in <a href="while_terminates.html">while_terminates</a>]<br/>
<a href="while_loop_equiv.html#while_loop_equiv">while_loop_equiv</a> [lemma, in <a href="while_loop_equiv.html">while_loop_equiv</a>]<br/>
<a href="while_embed.html#while_embed">while_embed</a> [lemma, in <a href="while_embed.html">while_embed</a>]<br/>
<a href="while_end_lift.html#while_end_lift">while_end_lift</a> [lemma, in <a href="while_end_lift.html">while_end_lift</a>]<br/>
<a href="while_loop_lift.html#while_loop_lift">while_loop_lift</a> [lemma, in <a href="while_loop_lift.html">while_loop_lift</a>]<br/>
<a href="while_end_equiv.html#while_end_equiv">while_end_equiv</a> [lemma, in <a href="while_end_equiv.html">while_end_equiv</a>]<br/>
<a href="while_embed_special.html#while_embed_special">while_embed_special</a> [lemma, in <a href="while_embed_special.html">while_embed_special</a>]<br/>
<br/><br/><a name="global_Z"></a><h2>Z </h2>
<a href="zero_and.html#zero_and">zero_and</a> [constructor, in <a href="zero_and.html">zero_and</a>]<br/>
<a href="zero_eq.html#zero_eq">zero_eq</a> [constructor, in <a href="zero_eq.html">zero_eq</a>]<br/>
<a href="zero_gt.html#zero_gt">zero_gt</a> [constructor, in <a href="zero_gt.html">zero_gt</a>]<br/>
<a href="zero_or_l.html#zero_or_l">zero_or_l</a> [constructor, in <a href="zero_or_l.html">zero_or_l</a>]<br/>
<a href="zero_or_r.html#zero_or_r">zero_or_r</a> [constructor, in <a href="zero_or_r.html">zero_or_r</a>]<br/>
<a href="zero_lt.html#zero_lt">zero_lt</a> [constructor, in <a href="zero_lt.html">zero_lt</a>]<br/>
<br/><br/><a name="global_*"></a><h2>other </h2>
<a href=":hoare_spec_scope:x_'<<->>'_x.html#:hoare_spec_scope:x_'<<->>'_x">_ <<->> _ (hoare_spec_scope)</a> [notation, in <a href=":hoare_spec_scope:x_'<<->>'_x.html">:hoare_spec_scope:x_'<<->>'_x</a>]<br/>
<a href=":hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'.html#:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'">{{ _ }} _ {{ _ }} (hoare_spec_scope)</a> [notation, in <a href=":hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'.html">:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'</a>]<br/>
<a href=":hoare_spec_scope:x_'->>'_x.html#:hoare_spec_scope:x_'->>'_x">_ ->> _ (hoare_spec_scope)</a> [notation, in <a href=":hoare_spec_scope:x_'->>'_x.html">:hoare_spec_scope:x_'->>'_x</a>]<br/>
<a href="::x_'::='_x.html#::x_'::='_x">_ ::= _</a> [notation, in <a href="::x_'::='_x.html">::x_'::='_x</a>]<br/>
<a href="::x_'&&'_x.html#::x_'&&'_x">_ && _</a> [notation, in <a href="::x_'&&'_x.html">::x_'&&'_x</a>]<br/>
<a href="::x_';'_x.html#::x_';'_x">_ ; _</a> [notation, in <a href="::x_';'_x.html">::x_';'_x</a>]<br/>
<a href="::x_'$=('_x_','_x_')'.html#::x_'$=('_x_','_x_')'">_ $=( _ , _ )</a> [notation, in <a href="::x_'$=('_x_','_x_')'.html">::x_'$=('_x_','_x_')'</a>]<br/>
<a href="::x_'=='_x.html#::x_'=='_x">_ == _</a> [notation, in <a href="::x_'=='_x.html">::x_'=='_x</a>]<br/>
<a href="::x_'||'_x.html#::x_'||'_x">_ || _</a> [notation, in <a href="::x_'||'_x.html">::x_'||'_x</a>]<br/>
<a href="::x_':=='_x.html#::x_':=='_x">_ :== _</a> [notation, in <a href="::x_':=='_x.html">::x_':=='_x</a>]<br/>
<a href="::x_'$=['_x_','_x_']'.html#::x_'$=['_x_','_x_']'">_ $=[ _ , _ ]</a> [notation, in <a href="::x_'$=['_x_','_x_']'.html">::x_'$=['_x_','_x_']'</a>]<br/>
<a href="::x_'/'_x_'||'_x.html#::x_'/'_x_'||'_x">_ / _ || _</a> [notation, in <a href="::x_'/'_x_'||'_x.html">::x_'/'_x_'||'_x</a>]<br/>
<a href="::'IFB'_x_'THEN'_x_'ELSE'_x_'FI'.html#::'IFB'_x_'THEN'_x_'ELSE'_x_'FI'">IFB _ THEN _ ELSE _ FI</a> [notation, in <a href="::'IFB'_x_'THEN'_x_'ELSE'_x_'FI'.html">::'IFB'_x_'THEN'_x_'ELSE'_x_'FI'</a>]<br/>
<a href="::'Prb'_x_'in'_x.html#::'Prb'_x_'in'_x">Prb _ in _</a> [notation, in <a href="::'Prb'_x_'in'_x.html">::'Prb'_x_'in'_x</a>]<br/>
<a href="::'Pr'_x_'in'_x.html#::'Pr'_x_'in'_x">Pr _ in _</a> [notation, in <a href="::'Pr'_x_'in'_x.html">::'Pr'_x_'in'_x</a>]<br/>
<a href="::'WHILE'_x_'DO'_x_'END'.html#::'WHILE'_x_'DO'_x_'END'">WHILE _ DO _ END</a> [notation, in <a href="::'WHILE'_x_'DO'_x_'END'.html">::'WHILE'_x_'DO'_x_'END'</a>]<br/>
<a href="::'~'_x.html#::'~'_x">~ _</a> [notation, in <a href="::'~'_x.html">::'~'_x</a>]<br/>
<br/><br/><hr/>
<h1>Lemma Index</h1>
<a name="lemma_A"></a><h2>A </h2>
<a href="assign_equiv.html#assign_equiv">assign_equiv</a> [in <a href="assign_equiv.html">assign_equiv</a>]<br/>
<a href="assign_lift.html#assign_lift">assign_lift</a> [in <a href="assign_lift.html">assign_lift</a>]<br/>
<a href="a_sub_eq.html#a_sub_eq">a_sub_eq</a> [in <a href="a_sub_eq.html">a_sub_eq</a>]<br/>
<a href="a_free_imp.html#a_free_imp">a_free_imp</a> [in <a href="a_free_imp.html">a_free_imp</a>]<br/>
<a href="a_free_eq.html#a_free_eq">a_free_eq</a> [in <a href="a_free_eq.html">a_free_eq</a>]<br/>
<br/><br/><a name="lemma_B"></a><h2>B </h2>
<a href="bassign_equiv.html#bassign_equiv">bassign_equiv</a> [in <a href="bassign_equiv.html">bassign_equiv</a>]<br/>
<a href="bassign_lift.html#bassign_lift">bassign_lift</a> [in <a href="bassign_lift.html">bassign_lift</a>]<br/>
<a href="bass_steps.html#bass_steps">bass_steps</a> [in <a href="bass_steps.html">bass_steps</a>]<br/>
<a href="beq_bid_false_iff.html#beq_bid_false_iff">beq_bid_false_iff</a> [in <a href="beq_bid_false_iff.html">beq_bid_false_iff</a>]<br/>
<a href="beq_aid_eq.html#beq_aid_eq">beq_aid_eq</a> [in <a href="beq_aid_eq.html">beq_aid_eq</a>]<br/>
<a href="beq_aid_false_iff.html#beq_aid_false_iff">beq_aid_false_iff</a> [in <a href="beq_aid_false_iff.html">beq_aid_false_iff</a>]<br/>
<a href="beq_aid_refl.html#beq_aid_refl">beq_aid_refl</a> [in <a href="beq_aid_refl.html">beq_aid_refl</a>]<br/>
<a href="beq_bid_refl.html#beq_bid_refl">beq_bid_refl</a> [in <a href="beq_bid_refl.html">beq_bid_refl</a>]<br/>
<a href="beq_bid_eq.html#beq_bid_eq">beq_bid_eq</a> [in <a href="beq_bid_eq.html">beq_bid_eq</a>]<br/>
<a href="biff_imp.html#biff_imp">biff_imp</a> [in <a href="biff_imp.html">biff_imp</a>]<br/>
<a href="bor_eq.html#bor_eq">bor_eq</a> [in <a href="bor_eq.html">bor_eq</a>]<br/>
<a href="btoss_lift.html#btoss_lift">btoss_lift</a> [in <a href="btoss_lift.html">btoss_lift</a>]<br/>
<a href="btoss_equiv.html#btoss_equiv">btoss_equiv</a> [in <a href="btoss_equiv.html">btoss_equiv</a>]<br/>
<a href="b_free_eq.html#b_free_eq">b_free_eq</a> [in <a href="b_free_eq.html">b_free_eq</a>]<br/>
<a href="b_sub_eq.html#b_sub_eq">b_sub_eq</a> [in <a href="b_sub_eq.html">b_sub_eq</a>]<br/>
<a href="b_free_eq_b.html#b_free_eq_b">b_free_eq_b</a> [in <a href="b_free_eq_b.html">b_free_eq_b</a>]<br/>
<a href="b_free_imp_b.html#b_free_imp_b">b_free_imp_b</a> [in <a href="b_free_imp_b.html">b_free_imp_b</a>]<br/>
<a href="b_sub_eq_b.html#b_sub_eq_b">b_sub_eq_b</a> [in <a href="b_sub_eq_b.html">b_sub_eq_b</a>]<br/>
<a href="b_free_imp.html#b_free_imp">b_free_imp</a> [in <a href="b_free_imp.html">b_free_imp</a>]<br/>
<br/><br/><a name="lemma_C"></a><h2>C </h2>
<a href="condition_on_1.html#condition_on_1">condition_on_1</a> [in <a href="condition_on_1.html">condition_on_1</a>]<br/>
<br/><br/><a name="lemma_D"></a><h2>D </h2>
<a href="deterministic_combine.html#deterministic_combine">deterministic_combine</a> [in <a href="deterministic_combine.html">deterministic_combine</a>]<br/>
<a href="deterministic_split.html#deterministic_split">deterministic_split</a> [in <a href="deterministic_split.html">deterministic_split</a>]<br/>
<a href="dist_update_true.html#dist_update_true">dist_update_true</a> [in <a href="dist_update_true.html">dist_update_true</a>]<br/>
<a href="dist_update_false.html#dist_update_false">dist_update_false</a> [in <a href="dist_update_false.html">dist_update_false</a>]<br/>
<a href="dist_update_b_permute.html#dist_update_b_permute">dist_update_b_permute</a> [in <a href="dist_update_b_permute.html">dist_update_b_permute</a>]<br/>
<a href="dist_update_non_interference.html#dist_update_non_interference">dist_update_non_interference</a> [in <a href="dist_update_non_interference.html">dist_update_non_interference</a>]<br/>
<a href="dist_update_prob_permute_b.html#dist_update_prob_permute_b">dist_update_prob_permute_b</a> [in <a href="dist_update_prob_permute_b.html">dist_update_prob_permute_b</a>]<br/>
<a href="divide_by_lt.html#divide_by_lt">divide_by_lt</a> [in <a href="divide_by_lt.html">divide_by_lt</a>]<br/>
<a href="dst_equiv_unit_split.html#dst_equiv_unit_split">dst_equiv_unit_split</a> [in <a href="dst_equiv_unit_split.html">dst_equiv_unit_split</a>]<br/>
<a href="dst_equiv_trans.html#dst_equiv_trans">dst_equiv_trans</a> [in <a href="dst_equiv_trans.html">dst_equiv_trans</a>]<br/>
<a href="dst_equiv_refl.html#dst_equiv_refl">dst_equiv_refl</a> [in <a href="dst_equiv_refl.html">dst_equiv_refl</a>]<br/>
<a href="dst_merge.html#dst_merge">dst_merge</a> [in <a href="dst_merge.html">dst_merge</a>]<br/>
<a href="dst_comm.html#dst_comm">dst_comm</a> [in <a href="dst_comm.html">dst_comm</a>]<br/>
<a href="dst_equiv_combine.html#dst_equiv_combine">dst_equiv_combine</a> [in <a href="dst_equiv_combine.html">dst_equiv_combine</a>]<br/>
<a href="dst_comm_hexp.html#dst_comm_hexp">dst_comm_hexp</a> [in <a href="dst_comm_hexp.html">dst_comm_hexp</a>]<br/>
<a href="dst_assoc.html#dst_assoc">dst_assoc</a> [in <a href="dst_assoc.html">dst_assoc</a>]<br/>
<a href="dst_equiv_symm.html#dst_equiv_symm">dst_equiv_symm</a> [in <a href="dst_equiv_symm.html">dst_equiv_symm</a>]<br/>
<a href="dst_equiv_iff.html#dst_equiv_iff">dst_equiv_iff</a> [in <a href="dst_equiv_iff.html">dst_equiv_iff</a>]<br/>
<a href="dst_equiv_split.html#dst_equiv_split">dst_equiv_split</a> [in <a href="dst_equiv_split.html">dst_equiv_split</a>]<br/>
<a href="dst_equiv_eq.html#dst_equiv_eq">dst_equiv_eq</a> [in <a href="dst_equiv_eq.html">dst_equiv_eq</a>]<br/>
<br/><br/><a name="lemma_E"></a><h2>E </h2>
<a href="equidistant.html#equidistant">equidistant</a> [in <a href="equidistant.html">equidistant</a>]<br/>
<br/><br/><a name="lemma_F"></a><h2>F </h2>
<a href="fork_on_b.html#fork_on_b">fork_on_b</a> [in <a href="fork_on_b.html">fork_on_b</a>]<br/>
<a href="fork_on_b_plus.html#fork_on_b_plus">fork_on_b_plus</a> [in <a href="fork_on_b_plus.html">fork_on_b_plus</a>]<br/>
<a href="free_eq_b.html#free_eq_b">free_eq_b</a> [in <a href="free_eq_b.html">free_eq_b</a>]<br/>
<a href="free_eq.html#free_eq">free_eq</a> [in <a href="free_eq.html">free_eq</a>]<br/>
<a href="free_then_unassigned.html#free_then_unassigned">free_then_unassigned</a> [in <a href="free_then_unassigned.html">free_then_unassigned</a>]<br/>
<br/><br/><a name="lemma_H"></a><h2>H </h2>
<a href="HGe_simpl.html#HGe_simpl">HGe_simpl</a> [in <a href="HGe_simpl.html">HGe_simpl</a>]<br/>
<a href="HLe_simpl.html#HLe_simpl">HLe_simpl</a> [in <a href="HLe_simpl.html">HLe_simpl</a>]<br/>
<a href="HNe_simpl.html#HNe_simpl">HNe_simpl</a> [in <a href="HNe_simpl.html">HNe_simpl</a>]<br/>
<a href="hoare_toss.html#hoare_toss">hoare_toss</a> [in <a href="hoare_toss.html">hoare_toss</a>]<br/>
<a href="hoare_if_true.html#hoare_if_true">hoare_if_true</a> [in <a href="hoare_if_true.html">hoare_if_true</a>]<br/>
<a href="hoare_if_gen.html#hoare_if_gen">hoare_if_gen</a> [in <a href="hoare_if_gen.html">hoare_if_gen</a>]<br/>
<a href="hoare_while_end.html#hoare_while_end">hoare_while_end</a> [in <a href="hoare_while_end.html">hoare_while_end</a>]<br/>
<a href="hoare_pre_false.html#hoare_pre_false">hoare_pre_false</a> [in <a href="hoare_pre_false.html">hoare_pre_false</a>]<br/>
<a href="hoare_post_true.html#hoare_post_true">hoare_post_true</a> [in <a href="hoare_post_true.html">hoare_post_true</a>]<br/>
<a href="hoare_skip.html#hoare_skip">hoare_skip</a> [in <a href="hoare_skip.html">hoare_skip</a>]<br/>
<a href="hoare_if_det.html#hoare_if_det">hoare_if_det</a> [in <a href="hoare_if_det.html">hoare_if_det</a>]<br/>
<a href="hoare_asgn_free.html#hoare_asgn_free">hoare_asgn_free</a> [in <a href="hoare_asgn_free.html">hoare_asgn_free</a>]<br/>
<a href="hoare_seq.html#hoare_seq">hoare_seq</a> [in <a href="hoare_seq.html">hoare_seq</a>]<br/>
<a href="hoare_toss_b.html#hoare_toss_b">hoare_toss_b</a> [in <a href="hoare_toss_b.html">hoare_toss_b</a>]<br/>
<a href="hoare_if_gen'.html#hoare_if_gen'">hoare_if_gen'</a> [in <a href="hoare_if_gen'.html">hoare_if_gen'</a>]<br/>
<a href="hoare_while_gen.html#hoare_while_gen">hoare_while_gen</a> [in <a href="hoare_while_gen.html">hoare_while_gen</a>]<br/>
<a href="hoare_while_prob.html#hoare_while_prob">hoare_while_prob</a> [in <a href="hoare_while_prob.html">hoare_while_prob</a>]<br/>
<a href="hoare_if_prob.html#hoare_if_prob">hoare_if_prob</a> [in <a href="hoare_if_prob.html">hoare_if_prob</a>]<br/>
<a href="hoare_asgn_b.html#hoare_asgn_b">hoare_asgn_b</a> [in <a href="hoare_asgn_b.html">hoare_asgn_b</a>]<br/>
<a href="hoare_if_false.html#hoare_if_false">hoare_if_false</a> [in <a href="hoare_if_false.html">hoare_if_false</a>]<br/>
<a href="hoare_asgn_free_b.html#hoare_asgn_free_b">hoare_asgn_free_b</a> [in <a href="hoare_asgn_free_b.html">hoare_asgn_free_b</a>]<br/>
<a href="hoare_if_prob'.html#hoare_if_prob'">hoare_if_prob'</a> [in <a href="hoare_if_prob'.html">hoare_if_prob'</a>]<br/>
<a href="hoare_consequence_post.html#hoare_consequence_post">hoare_consequence_post</a> [in <a href="hoare_consequence_post.html">hoare_consequence_post</a>]<br/>
<a href="hoare_while_det.html#hoare_while_det">hoare_while_det</a> [in <a href="hoare_while_det.html">hoare_while_det</a>]<br/>
<a href="hoare_asgn.html#hoare_asgn">hoare_asgn</a> [in <a href="hoare_asgn.html">hoare_asgn</a>]<br/>
<a href="hoare_if_unscaled.html#hoare_if_unscaled">hoare_if_unscaled</a> [in <a href="hoare_if_unscaled.html">hoare_if_unscaled</a>]<br/>
<a href="hoare_consequence.html#hoare_consequence">hoare_consequence</a> [in <a href="hoare_consequence.html">hoare_consequence</a>]<br/>
<a href="hoare_consequence_pre.html#hoare_consequence_pre">hoare_consequence_pre</a> [in <a href="hoare_consequence_pre.html">hoare_consequence_pre</a>]<br/>
<a href="h_sub_eq_b.html#h_sub_eq_b">h_sub_eq_b</a> [in <a href="h_sub_eq_b.html">h_sub_eq_b</a>]<br/>
<a href="h_sub_eq.html#h_sub_eq">h_sub_eq</a> [in <a href="h_sub_eq.html">h_sub_eq</a>]<br/>
<br/><br/><a name="lemma_I"></a><h2>I </h2>
<a href="if_false_equiv.html#if_false_equiv">if_false_equiv</a> [in <a href="if_false_equiv.html">if_false_equiv</a>]<br/>
<a href="if_equiv.html#if_equiv">if_equiv</a> [in <a href="if_equiv.html">if_equiv</a>]<br/>
<a href="if_true_lift.html#if_true_lift">if_true_lift</a> [in <a href="if_true_lift.html">if_true_lift</a>]<br/>
<a href="if_false_lift.html#if_false_lift">if_false_lift</a> [in <a href="if_false_lift.html">if_false_lift</a>]<br/>
<a href="if_steps.html#if_steps">if_steps</a> [in <a href="if_steps.html">if_steps</a>]<br/>
<a href="if_true_equiv.html#if_true_equiv">if_true_equiv</a> [in <a href="if_true_equiv.html">if_true_equiv</a>]<br/>
<a href="in_0_1_open.html#in_0_1_open">in_0_1_open</a> [in <a href="in_0_1_open.html">in_0_1_open</a>]<br/>
<a href="in_0_1_closed.html#in_0_1_closed">in_0_1_closed</a> [in <a href="in_0_1_closed.html">in_0_1_closed</a>]<br/>
<br/><br/><a name="lemma_M"></a><h2>M </h2>
<a href="mult_stable.html#mult_stable">mult_stable</a> [in <a href="mult_stable.html">mult_stable</a>]<br/>
<a href="mult_le_0_compat.html#mult_le_0_compat">mult_le_0_compat</a> [in <a href="mult_le_0_compat.html">mult_le_0_compat</a>]<br/>
<a href="mult_lt_0_compat.html#mult_lt_0_compat">mult_lt_0_compat</a> [in <a href="mult_lt_0_compat.html">mult_lt_0_compat</a>]<br/>
<a href="mult_by_lt_1.html#mult_by_lt_1">mult_by_lt_1</a> [in <a href="mult_by_lt_1.html">mult_by_lt_1</a>]<br/>
<br/><br/><a name="lemma_N"></a><h2>N </h2>
<a href="negation_flip.html#negation_flip">negation_flip</a> [in <a href="negation_flip.html">negation_flip</a>]<br/>
<a href="neg_b_all_zero.html#neg_b_all_zero">neg_b_all_zero</a> [in <a href="neg_b_all_zero.html">neg_b_all_zero</a>]<br/>
<a href="non_disjunctive_combine.html#non_disjunctive_combine">non_disjunctive_combine</a> [in <a href="non_disjunctive_combine.html">non_disjunctive_combine</a>]<br/>
<a href="non_probabilistic_split.html#non_probabilistic_split">non_probabilistic_split</a> [in <a href="non_probabilistic_split.html">non_probabilistic_split</a>]<br/>
<br/><br/><a name="lemma_O"></a><h2>O </h2>
<a href="one_minus_p.html#one_minus_p">one_minus_p</a> [in <a href="one_minus_p.html">one_minus_p</a>]<br/>
<br/><br/><a name="lemma_P"></a><h2>P </h2>
<a href="plus_by_gt_0.html#plus_by_gt_0">plus_by_gt_0</a> [in <a href="plus_by_gt_0.html">plus_by_gt_0</a>]<br/>
<a href="prb_false.html#prb_false">prb_false</a> [in <a href="prb_false.html">prb_false</a>]<br/>
<a href="prb_true.html#prb_true">prb_true</a> [in <a href="prb_true.html">prb_true</a>]<br/>
<a href="prb_complement_0.html#prb_complement_0">prb_complement_0</a> [in <a href="prb_complement_0.html">prb_complement_0</a>]<br/>
<a href="prb_complement_1.html#prb_complement_1">prb_complement_1</a> [in <a href="prb_complement_1.html">prb_complement_1</a>]<br/>
<a href="probability_preserved.html#probability_preserved">probability_preserved</a> [in <a href="probability_preserved.html">probability_preserved</a>]<br/>
<a href="prob_update_equiv.html#prob_update_equiv">prob_update_equiv</a> [in <a href="prob_update_equiv.html">prob_update_equiv</a>]<br/>
<a href="prob_update_b_equiv.html#prob_update_b_equiv">prob_update_b_equiv</a> [in <a href="prob_update_b_equiv.html">prob_update_b_equiv</a>]<br/>
<a href="prob_update_non_interference.html#prob_update_non_interference">prob_update_non_interference</a> [in <a href="prob_update_non_interference.html">prob_update_non_interference</a>]<br/>
<a href="prob_update_0.html#prob_update_0">prob_update_0</a> [in <a href="prob_update_0.html">prob_update_0</a>]<br/>
<a href="prob_update_1.html#prob_update_1">prob_update_1</a> [in <a href="prob_update_1.html">prob_update_1</a>]<br/>
<a href="prob_update_F.html#prob_update_F">prob_update_F</a> [in <a href="prob_update_F.html">prob_update_F</a>]<br/>
<a href="prob_update_T.html#prob_update_T">prob_update_T</a> [in <a href="prob_update_T.html">prob_update_T</a>]<br/>
<a href="pr_combine.html#pr_combine">pr_combine</a> [in <a href="pr_combine.html">pr_combine</a>]<br/>
<a href="pr_strengthen_0.html#pr_strengthen_0">pr_strengthen_0</a> [in <a href="pr_strengthen_0.html">pr_strengthen_0</a>]<br/>
<a href="pr_weaken.html#pr_weaken">pr_weaken</a> [in <a href="pr_weaken.html">pr_weaken</a>]<br/>
<a href="pr_conj_1.html#pr_conj_1">pr_conj_1</a> [in <a href="pr_conj_1.html">pr_conj_1</a>]<br/>
<a href="pr_sub_b.html#pr_sub_b">pr_sub_b</a> [in <a href="pr_sub_b.html">pr_sub_b</a>]<br/>
<a href="pr_tautology.html#pr_tautology">pr_tautology</a> [in <a href="pr_tautology.html">pr_tautology</a>]<br/>
<a href="pr_equivalence.html#pr_equivalence">pr_equivalence</a> [in <a href="pr_equivalence.html">pr_equivalence</a>]<br/>
<a href="pr_normality.html#pr_normality">pr_normality</a> [in <a href="pr_normality.html">pr_normality</a>]<br/>
<a href="pr_ge_bound.html#pr_ge_bound">pr_ge_bound</a> [in <a href="pr_ge_bound.html">pr_ge_bound</a>]<br/>
<a href="pr_sub.html#pr_sub">pr_sub</a> [in <a href="pr_sub.html">pr_sub</a>]<br/>
<a href="pr_weaken_1.html#pr_weaken_1">pr_weaken_1</a> [in <a href="pr_weaken_1.html">pr_weaken_1</a>]<br/>
<a href="pr_conj_1_l.html#pr_conj_1_l">pr_conj_1_l</a> [in <a href="pr_conj_1_l.html">pr_conj_1_l</a>]<br/>
<a href="pr_conj_1_r.html#pr_conj_1_r">pr_conj_1_r</a> [in <a href="pr_conj_1_r.html">pr_conj_1_r</a>]<br/>
<a href="pr_disjunction.html#pr_disjunction">pr_disjunction</a> [in <a href="pr_disjunction.html">pr_disjunction</a>]<br/>
<a href="pr_conj_0_l.html#pr_conj_0_l">pr_conj_0_l</a> [in <a href="pr_conj_0_l.html">pr_conj_0_l</a>]<br/>
<a href="pr_conj_0_r.html#pr_conj_0_r">pr_conj_0_r</a> [in <a href="pr_conj_0_r.html">pr_conj_0_r</a>]<br/>
<a href="pr_complement_0.html#pr_complement_0">pr_complement_0</a> [in <a href="pr_complement_0.html">pr_complement_0</a>]<br/>
<a href="pr_complement_1.html#pr_complement_1">pr_complement_1</a> [in <a href="pr_complement_1.html">pr_complement_1</a>]<br/>
<a href="pr_conj_le_l.html#pr_conj_le_l">pr_conj_le_l</a> [in <a href="pr_conj_le_l.html">pr_conj_le_l</a>]<br/>
<a href="pr_conj_le_r.html#pr_conj_le_r">pr_conj_le_r</a> [in <a href="pr_conj_le_r.html">pr_conj_le_r</a>]<br/>
<a href="pr_totality.html#pr_totality">pr_totality</a> [in <a href="pr_totality.html">pr_totality</a>]<br/>
<a href="pr_addition.html#pr_addition">pr_addition</a> [in <a href="pr_addition.html">pr_addition</a>]<br/>
<a href="pr_strengthen.html#pr_strengthen">pr_strengthen</a> [in <a href="pr_strengthen.html">pr_strengthen</a>]<br/>
<a href="pr_disj_ge_l.html#pr_disj_ge_l">pr_disj_ge_l</a> [in <a href="pr_disj_ge_l.html">pr_disj_ge_l</a>]<br/>
<a href="pr_disj_ge_r.html#pr_disj_ge_r">pr_disj_ge_r</a> [in <a href="pr_disj_ge_r.html">pr_disj_ge_r</a>]<br/>
<a href="pr_unit.html#pr_unit">pr_unit</a> [in <a href="pr_unit.html">pr_unit</a>]<br/>
<a href="pr_contradiction.html#pr_contradiction">pr_contradiction</a> [in <a href="pr_contradiction.html">pr_contradiction</a>]<br/>
<a href="pr_union_bound.html#pr_union_bound">pr_union_bound</a> [in <a href="pr_union_bound.html">pr_union_bound</a>]<br/>
<a href="pr_split_0.html#pr_split_0">pr_split_0</a> [in <a href="pr_split_0.html">pr_split_0</a>]<br/>
<a href="pr_split_1.html#pr_split_1">pr_split_1</a> [in <a href="pr_split_1.html">pr_split_1</a>]<br/>
<a href="pr_complement.html#pr_complement">pr_complement</a> [in <a href="pr_complement.html">pr_complement</a>]<br/>
<br/><br/><a name="lemma_S"></a><h2>S </h2>
<a href="scale_equiv_0.html#scale_equiv_0">scale_equiv_0</a> [in <a href="scale_equiv_0.html">scale_equiv_0</a>]<br/>
<a href="scale_equiv_1.html#scale_equiv_1">scale_equiv_1</a> [in <a href="scale_equiv_1.html">scale_equiv_1</a>]<br/>
<a href="scale_twice.html#scale_twice">scale_twice</a> [in <a href="scale_twice.html">scale_twice</a>]<br/>
<a href="scale_1.html#scale_1">scale_1</a> [in <a href="scale_1.html">scale_1</a>]<br/>
<a href="scale_cond.html#scale_cond">scale_cond</a> [in <a href="scale_cond.html">scale_cond</a>]<br/>
<a href="scale_eq.html#scale_eq">scale_eq</a> [in <a href="scale_eq.html">scale_eq</a>]<br/>
<a href="scale_equiv_0'.html#scale_equiv_0'">scale_equiv_0'</a> [in <a href="scale_equiv_0'.html">scale_equiv_0'</a>]<br/>
<a href="scale_gt.html#scale_gt">scale_gt</a> [in <a href="scale_gt.html">scale_gt</a>]<br/>
<a href="scale_equiv_1'.html#scale_equiv_1'">scale_equiv_1'</a> [in <a href="scale_equiv_1'.html">scale_equiv_1'</a>]<br/>
<a href="scale_inversion.html#scale_inversion">scale_inversion</a> [in <a href="scale_inversion.html">scale_inversion</a>]<br/>
<a href="scale_lt.html#scale_lt">scale_lt</a> [in <a href="scale_lt.html">scale_lt</a>]<br/>
<a href="seq_lift.html#seq_lift">seq_lift</a> [in <a href="seq_lift.html">seq_lift</a>]<br/>
<a href="seq_equiv.html#seq_equiv">seq_equiv</a> [in <a href="seq_equiv.html">seq_equiv</a>]<br/>
<a href="skip_lift.html#skip_lift">skip_lift</a> [in <a href="skip_lift.html">skip_lift</a>]<br/>
<a href="skip_equiv.html#skip_equiv">skip_equiv</a> [in <a href="skip_equiv.html">skip_equiv</a>]<br/>
<a href="step_split.html#step_split">step_split</a> [in <a href="step_split.html">step_split</a>]<br/>
<a href="step_deterministic.html#step_deterministic">step_deterministic</a> [in <a href="step_deterministic.html">step_deterministic</a>]<br/>
<a href="sub_over_condition.html#sub_over_condition">sub_over_condition</a> [in <a href="sub_over_condition.html">sub_over_condition</a>]<br/>
<a href="sum_to_gt_0.html#sum_to_gt_0">sum_to_gt_0</a> [in <a href="sum_to_gt_0.html">sum_to_gt_0</a>]<br/>
<a href="sum_to_0.html#sum_to_0">sum_to_0</a> [in <a href="sum_to_0.html">sum_to_0</a>]<br/>
<a href="sum_to_1.html#sum_to_1">sum_to_1</a> [in <a href="sum_to_1.html">sum_to_1</a>]<br/>
<br/><br/><a name="lemma_T"></a><h2>T </h2>
<a href="term_split.html#term_split">term_split</a> [in <a href="term_split.html">term_split</a>]<br/>
<a href="term_combine.html#term_combine">term_combine</a> [in <a href="term_combine.html">term_combine</a>]<br/>
<a href="toss_equiv.html#toss_equiv">toss_equiv</a> [in <a href="toss_equiv.html">toss_equiv</a>]<br/>
<a href="toss_lift.html#toss_lift">toss_lift</a> [in <a href="toss_lift.html">toss_lift</a>]<br/>
<br/><br/><a name="lemma_U"></a><h2>U </h2>
<a href="update_interpermute.html#update_interpermute">update_interpermute</a> [in <a href="update_interpermute.html">update_interpermute</a>]<br/>
<a href="update_eq.html#update_eq">update_eq</a> [in <a href="update_eq.html">update_eq</a>]<br/>
<a href="update_permute_b.html#update_permute_b">update_permute_b</a> [in <a href="update_permute_b.html">update_permute_b</a>]<br/>
<a href="update_equiv_b.html#update_equiv_b">update_equiv_b</a> [in <a href="update_equiv_b.html">update_equiv_b</a>]<br/>
<a href="update_neq.html#update_neq">update_neq</a> [in <a href="update_neq.html">update_neq</a>]<br/>
<a href="update_same.html#update_same">update_same</a> [in <a href="update_same.html">update_same</a>]<br/>
<a href="update_permute.html#update_permute">update_permute</a> [in <a href="update_permute.html">update_permute</a>]<br/>
<a href="update_equiv.html#update_equiv">update_equiv</a> [in <a href="update_equiv.html">update_equiv</a>]<br/>
<a href="update_non_interference.html#update_non_interference">update_non_interference</a> [in <a href="update_non_interference.html">update_non_interference</a>]<br/>
<br/><br/><a name="lemma_V"></a><h2>V </h2>
<a href="vacuous_P_l.html#vacuous_P_l">vacuous_P_l</a> [in <a href="vacuous_P_l.html">vacuous_P_l</a>]<br/>
<a href="vacuous_P_r.html#vacuous_P_r">vacuous_P_r</a> [in <a href="vacuous_P_r.html">vacuous_P_r</a>]<br/>
<a href="vacuous_P.html#vacuous_P">vacuous_P</a> [in <a href="vacuous_P.html">vacuous_P</a>]<br/>
<br/><br/><a name="lemma_W"></a><h2>W </h2>
<a href="while_end.html#while_end">while_end</a> [in <a href="while_end.html">while_end</a>]<br/>
<a href="while_terminates.html#while_terminates">while_terminates</a> [in <a href="while_terminates.html">while_terminates</a>]<br/>
<a href="while_loop_equiv.html#while_loop_equiv">while_loop_equiv</a> [in <a href="while_loop_equiv.html">while_loop_equiv</a>]<br/>
<a href="while_embed.html#while_embed">while_embed</a> [in <a href="while_embed.html">while_embed</a>]<br/>
<a href="while_end_lift.html#while_end_lift">while_end_lift</a> [in <a href="while_end_lift.html">while_end_lift</a>]<br/>
<a href="while_loop_lift.html#while_loop_lift">while_loop_lift</a> [in <a href="while_loop_lift.html">while_loop_lift</a>]<br/>
<a href="while_end_equiv.html#while_end_equiv">while_end_equiv</a> [in <a href="while_end_equiv.html">while_end_equiv</a>]<br/>
<a href="while_embed_special.html#while_embed_special">while_embed_special</a> [in <a href="while_embed_special.html">while_embed_special</a>]<br/>
<br/><br/><hr/>
<h1>Constructor Index</h1>
<a name="constructor_A"></a><h2>A </h2>
<a href="Af_plus.html#Af_plus">Af_plus</a> [in <a href="Af_plus.html">Af_plus</a>]<br/>
<a href="Af_mult.html#Af_mult">Af_mult</a> [in <a href="Af_mult.html">Af_mult</a>]<br/>
<a href="Af_minus.html#Af_minus">Af_minus</a> [in <a href="Af_minus.html">Af_minus</a>]<br/>
<a href="Af_num.html#Af_num">Af_num</a> [in <a href="Af_num.html">Af_num</a>]<br/>
<a href="Af_id.html#Af_id">Af_id</a> [in <a href="Af_id.html">Af_id</a>]<br/>
<a href="Aid.html#Aid">Aid</a> [in <a href="Aid.html">Aid</a>]<br/>
<a href="AId.html#AId">AId</a> [in <a href="AId.html">AId</a>]<br/>
<a href="AMinus.html#AMinus">AMinus</a> [in <a href="AMinus.html">AMinus</a>]<br/>
<a href="AMult.html#AMult">AMult</a> [in <a href="AMult.html">AMult</a>]<br/>
<a href="ANum.html#ANum">ANum</a> [in <a href="ANum.html">ANum</a>]<br/>
<a href="APlus.html#APlus">APlus</a> [in <a href="APlus.html">APlus</a>]<br/>
<a href="Assign.html#Assign">Assign</a> [in <a href="Assign.html">Assign</a>]<br/>
<br/><br/><a name="constructor_B"></a><h2>B </h2>
<a href="BAnd.html#BAnd">BAnd</a> [in <a href="BAnd.html">BAnd</a>]<br/>
<a href="BAssign.html#BAssign">BAssign</a> [in <a href="BAssign.html">BAssign</a>]<br/>
<a href="BEq.html#BEq">BEq</a> [in <a href="BEq.html">BEq</a>]<br/>
<a href="BFalse.html#BFalse">BFalse</a> [in <a href="BFalse.html">BFalse</a>]<br/>
<a href="Bf_eq.html#Bf_eq">Bf_eq</a> [in <a href="Bf_eq.html">Bf_eq</a>]<br/>
<a href="Bf_true_b.html#Bf_true_b">Bf_true_b</a> [in <a href="Bf_true_b.html">Bf_true_b</a>]<br/>
<a href="Bf_false.html#Bf_false">Bf_false</a> [in <a href="Bf_false.html">Bf_false</a>]<br/>
<a href="Bf_id.html#Bf_id">Bf_id</a> [in <a href="Bf_id.html">Bf_id</a>]<br/>
<a href="Bf_le_b.html#Bf_le_b">Bf_le_b</a> [in <a href="Bf_le_b.html">Bf_le_b</a>]<br/>
<a href="Bf_le.html#Bf_le">Bf_le</a> [in <a href="Bf_le.html">Bf_le</a>]<br/>
<a href="Bf_and_b.html#Bf_and_b">Bf_and_b</a> [in <a href="Bf_and_b.html">Bf_and_b</a>]<br/>
<a href="Bf_false_b.html#Bf_false_b">Bf_false_b</a> [in <a href="Bf_false_b.html">Bf_false_b</a>]<br/>
<a href="Bf_eq_b.html#Bf_eq_b">Bf_eq_b</a> [in <a href="Bf_eq_b.html">Bf_eq_b</a>]<br/>
<a href="Bf_not_b.html#Bf_not_b">Bf_not_b</a> [in <a href="Bf_not_b.html">Bf_not_b</a>]<br/>
<a href="Bf_true.html#Bf_true">Bf_true</a> [in <a href="Bf_true.html">Bf_true</a>]<br/>
<a href="Bf_id_b.html#Bf_id_b">Bf_id_b</a> [in <a href="Bf_id_b.html">Bf_id_b</a>]<br/>
<a href="Bf_and.html#Bf_and">Bf_and</a> [in <a href="Bf_and.html">Bf_and</a>]<br/>
<a href="Bf_not.html#Bf_not">Bf_not</a> [in <a href="Bf_not.html">Bf_not</a>]<br/>
<a href="Bid.html#Bid">Bid</a> [in <a href="Bid.html">Bid</a>]<br/>
<a href="BId.html#BId">BId</a> [in <a href="BId.html">BId</a>]<br/>
<a href="BLe.html#BLe">BLe</a> [in <a href="BLe.html">BLe</a>]<br/>
<a href="BNot.html#BNot">BNot</a> [in <a href="BNot.html">BNot</a>]<br/>
<a href="BToss.html#BToss">BToss</a> [in <a href="BToss.html">BToss</a>]<br/>
<a href="BTrue.html#BTrue">BTrue</a> [in <a href="BTrue.html">BTrue</a>]<br/>
<br/><br/><a name="constructor_C"></a><h2>C </h2>
<a href="Cf_seq_b'.html#Cf_seq_b'">Cf_seq_b'</a> [in <a href="Cf_seq_b'.html">Cf_seq_b'</a>]<br/>
<a href="Cf_toss_b'.html#Cf_toss_b'">Cf_toss_b'</a> [in <a href="Cf_toss_b'.html">Cf_toss_b'</a>]<br/>
<a href="Cf_if_b'.html#Cf_if_b'">Cf_if_b'</a> [in <a href="Cf_if_b'.html">Cf_if_b'</a>]<br/>
<a href="Cf_ass_b'.html#Cf_ass_b'">Cf_ass_b'</a> [in <a href="Cf_ass_b'.html">Cf_ass_b'</a>]<br/>
<a href="Cf_skip.html#Cf_skip">Cf_skip</a> [in <a href="Cf_skip.html">Cf_skip</a>]<br/>
<a href="Cf_bass.html#Cf_bass">Cf_bass</a> [in <a href="Cf_bass.html">Cf_bass</a>]<br/>
<a href="Cf_seq_b.html#Cf_seq_b">Cf_seq_b</a> [in <a href="Cf_seq_b.html">Cf_seq_b</a>]<br/>
<a href="Cf_ass_b.html#Cf_ass_b">Cf_ass_b</a> [in <a href="Cf_ass_b.html">Cf_ass_b</a>]<br/>
<a href="Cf_skip_b.html#Cf_skip_b">Cf_skip_b</a> [in <a href="Cf_skip_b.html">Cf_skip_b</a>]<br/>
<a href="Cf_while_b'.html#Cf_while_b'">Cf_while_b'</a> [in <a href="Cf_while_b'.html">Cf_while_b'</a>]<br/>
<a href="Cf_btoss_b'.html#Cf_btoss_b'">Cf_btoss_b'</a> [in <a href="Cf_btoss_b'.html">Cf_btoss_b'</a>]<br/>
<a href="Cf_while.html#Cf_while">Cf_while</a> [in <a href="Cf_while.html">Cf_while</a>]<br/>
<a href="Cf_toss_b.html#Cf_toss_b">Cf_toss_b</a> [in <a href="Cf_toss_b.html">Cf_toss_b</a>]<br/>
<a href="Cf_btoss.html#Cf_btoss">Cf_btoss</a> [in <a href="Cf_btoss.html">Cf_btoss</a>]<br/>
<a href="Cf_while_b.html#Cf_while_b">Cf_while_b</a> [in <a href="Cf_while_b.html">Cf_while_b</a>]<br/>
<a href="Cf_bass_b'.html#Cf_bass_b'">Cf_bass_b'</a> [in <a href="Cf_bass_b'.html">Cf_bass_b'</a>]<br/>
<a href="Cf_skip_b'.html#Cf_skip_b'">Cf_skip_b'</a> [in <a href="Cf_skip_b'.html">Cf_skip_b'</a>]<br/>
<a href="Cf_if_b.html#Cf_if_b">Cf_if_b</a> [in <a href="Cf_if_b.html">Cf_if_b</a>]<br/>
<a href="Cf_if.html#Cf_if">Cf_if</a> [in <a href="Cf_if.html">Cf_if</a>]<br/>
<a href="Cf_btoss_b.html#Cf_btoss_b">Cf_btoss_b</a> [in <a href="Cf_btoss_b.html">Cf_btoss_b</a>]<br/>
<a href="Cf_seq.html#Cf_seq">Cf_seq</a> [in <a href="Cf_seq.html">Cf_seq</a>]<br/>
<a href="Cf_toss.html#Cf_toss">Cf_toss</a> [in <a href="Cf_toss.html">Cf_toss</a>]<br/>
<a href="Cf_bass_b.html#Cf_bass_b">Cf_bass_b</a> [in <a href="Cf_bass_b.html">Cf_bass_b</a>]<br/>
<a href="Cf_ass.html#Cf_ass">Cf_ass</a> [in <a href="Cf_ass.html">Cf_ass</a>]<br/>
<a href="Combine.html#Combine">Combine</a> [in <a href="Combine.html">Combine</a>]<br/>
<br/><br/><a name="constructor_D"></a><h2>D </h2>
<a href="det_lit.html#det_lit">det_lit</a> [in <a href="det_lit.html">det_lit</a>]<br/>
<a href="det_conj.html#det_conj">det_conj</a> [in <a href="det_conj.html">det_conj</a>]<br/>
<br/><br/><a name="constructor_E"></a><h2>E </h2>
<a href="E_Seq.html#E_Seq">E_Seq</a> [in <a href="E_Seq.html">E_Seq</a>]<br/>
<a href="E_Toss.html#E_Toss">E_Toss</a> [in <a href="E_Toss.html">E_Toss</a>]<br/>
<a href="E_Assign.html#E_Assign">E_Assign</a> [in <a href="E_Assign.html">E_Assign</a>]<br/>
<a href="E_WhileEnd.html#E_WhileEnd">E_WhileEnd</a> [in <a href="E_WhileEnd.html">E_WhileEnd</a>]<br/>
<a href="E_IfFalse.html#E_IfFalse">E_IfFalse</a> [in <a href="E_IfFalse.html">E_IfFalse</a>]<br/>
<a href="E_IfTrue.html#E_IfTrue">E_IfTrue</a> [in <a href="E_IfTrue.html">E_IfTrue</a>]<br/>
<a href="E_Skip.html#E_Skip">E_Skip</a> [in <a href="E_Skip.html">E_Skip</a>]<br/>
<a href="E_BToss.html#E_BToss">E_BToss</a> [in <a href="E_BToss.html">E_BToss</a>]<br/>
<a href="E_WhileLoop.html#E_WhileLoop">E_WhileLoop</a> [in <a href="E_WhileLoop.html">E_WhileLoop</a>]<br/>
<a href="E_BAssign.html#E_BAssign">E_BAssign</a> [in <a href="E_BAssign.html">E_BAssign</a>]<br/>
<a href="E_Lift.html#E_Lift">E_Lift</a> [in <a href="E_Lift.html">E_Lift</a>]<br/>
<br/><br/><a name="constructor_H"></a><h2>H </h2>
<a href="HAnd.html#HAnd">HAnd</a> [in <a href="HAnd.html">HAnd</a>]<br/>
<a href="HEq.html#HEq">HEq</a> [in <a href="HEq.html">HEq</a>]<br/>
<a href="Hf_gt.html#Hf_gt">Hf_gt</a> [in <a href="Hf_gt.html">Hf_gt</a>]<br/>
<a href="Hf_gt_b.html#Hf_gt_b">Hf_gt_b</a> [in <a href="Hf_gt_b.html">Hf_gt_b</a>]<br/>
<a href="Hf_lt.html#Hf_lt">Hf_lt</a> [in <a href="Hf_lt.html">Hf_lt</a>]<br/>
<a href="Hf_and.html#Hf_and">Hf_and</a> [in <a href="Hf_and.html">Hf_and</a>]<br/>
<a href="Hf_eq_b.html#Hf_eq_b">Hf_eq_b</a> [in <a href="Hf_eq_b.html">Hf_eq_b</a>]<br/>
<a href="Hf_or.html#Hf_or">Hf_or</a> [in <a href="Hf_or.html">Hf_or</a>]<br/>
<a href="Hf_and_b.html#Hf_and_b">Hf_and_b</a> [in <a href="Hf_and_b.html">Hf_and_b</a>]<br/>
<a href="Hf_or_b.html#Hf_or_b">Hf_or_b</a> [in <a href="Hf_or_b.html">Hf_or_b</a>]<br/>
<a href="Hf_lt_b.html#Hf_lt_b">Hf_lt_b</a> [in <a href="Hf_lt_b.html">Hf_lt_b</a>]<br/>
<a href="Hf_eq.html#Hf_eq">Hf_eq</a> [in <a href="Hf_eq.html">Hf_eq</a>]<br/>
<a href="HGt.html#HGt">HGt</a> [in <a href="HGt.html">HGt</a>]<br/>
<a href="HLt.html#HLt">HLt</a> [in <a href="HLt.html">HLt</a>]<br/>
<a href="HOr.html#HOr">HOr</a> [in <a href="HOr.html">HOr</a>]<br/>
<br/><br/><a name="constructor_I"></a><h2>I </h2>
<a href="If.html#If">If</a> [in <a href="If.html">If</a>]<br/>
<br/><br/><a name="constructor_N"></a><h2>N </h2>
<a href="nd_conj.html#nd_conj">nd_conj</a> [in <a href="nd_conj.html">nd_conj</a>]<br/>
<a href="nd_eq.html#nd_eq">nd_eq</a> [in <a href="nd_eq.html">nd_eq</a>]<br/>
<a href="nd_gt.html#nd_gt">nd_gt</a> [in <a href="nd_gt.html">nd_gt</a>]<br/>
<a href="nd_lt.html#nd_lt">nd_lt</a> [in <a href="nd_lt.html">nd_lt</a>]<br/>
<a href="np_disj.html#np_disj">np_disj</a> [in <a href="np_disj.html">np_disj</a>]<br/>
<a href="np_0.html#np_0">np_0</a> [in <a href="np_0.html">np_0</a>]<br/>
<a href="np_1.html#np_1">np_1</a> [in <a href="np_1.html">np_1</a>]<br/>
<a href="np_conj.html#np_conj">np_conj</a> [in <a href="np_conj.html">np_conj</a>]<br/>
<br/><br/><a name="constructor_S"></a><h2>S </h2>
<a href="Seq.html#Seq">Seq</a> [in <a href="Seq.html">Seq</a>]<br/>
<a href="Skip.html#Skip">Skip</a> [in <a href="Skip.html">Skip</a>]<br/>
<br/><br/><a name="constructor_T"></a><h2>T </h2>
<a href="term_0.html#term_0">term_0</a> [in <a href="term_0.html">term_0</a>]<br/>
<a href="term_S.html#term_S">term_S</a> [in <a href="term_S.html">term_S</a>]<br/>
<a href="Toss.html#Toss">Toss</a> [in <a href="Toss.html">Toss</a>]<br/>
<br/><br/><a name="constructor_U"></a><h2>U </h2>
<a href="Unit.html#Unit">Unit</a> [in <a href="Unit.html">Unit</a>]<br/>
<br/><br/><a name="constructor_W"></a><h2>W </h2>
<a href="While.html#While">While</a> [in <a href="While.html">While</a>]<br/>
<br/><br/><a name="constructor_Z"></a><h2>Z </h2>
<a href="zero_and.html#zero_and">zero_and</a> [in <a href="zero_and.html">zero_and</a>]<br/>
<a href="zero_eq.html#zero_eq">zero_eq</a> [in <a href="zero_eq.html">zero_eq</a>]<br/>
<a href="zero_gt.html#zero_gt">zero_gt</a> [in <a href="zero_gt.html">zero_gt</a>]<br/>
<a href="zero_or_l.html#zero_or_l">zero_or_l</a> [in <a href="zero_or_l.html">zero_or_l</a>]<br/>
<a href="zero_or_r.html#zero_or_r">zero_or_r</a> [in <a href="zero_or_r.html">zero_or_r</a>]<br/>
<a href="zero_lt.html#zero_lt">zero_lt</a> [in <a href="zero_lt.html">zero_lt</a>]<br/>
<br/><br/><hr/>
<h1>Notation Index</h1>
<a name="notation_*"></a><h2>other </h2>
<a href=":hoare_spec_scope:x_'<<->>'_x.html#:hoare_spec_scope:x_'<<->>'_x">_ <<->> _ (hoare_spec_scope)</a> [in <a href=":hoare_spec_scope:x_'<<->>'_x.html">:hoare_spec_scope:x_'<<->>'_x</a>]<br/>
<a href=":hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'.html#:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'">{{ _ }} _ {{ _ }} (hoare_spec_scope)</a> [in <a href=":hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'.html">:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}'</a>]<br/>
<a href=":hoare_spec_scope:x_'->>'_x.html#:hoare_spec_scope:x_'->>'_x">_ ->> _ (hoare_spec_scope)</a> [in <a href=":hoare_spec_scope:x_'->>'_x.html">:hoare_spec_scope:x_'->>'_x</a>]<br/>
<a href="::x_'::='_x.html#::x_'::='_x">_ ::= _</a> [in <a href="::x_'::='_x.html">::x_'::='_x</a>]<br/>
<a href="::x_'&&'_x.html#::x_'&&'_x">_ && _</a> [in <a href="::x_'&&'_x.html">::x_'&&'_x</a>]<br/>
<a href="::x_';'_x.html#::x_';'_x">_ ; _</a> [in <a href="::x_';'_x.html">::x_';'_x</a>]<br/>
<a href="::x_'$=('_x_','_x_')'.html#::x_'$=('_x_','_x_')'">_ $=( _ , _ )</a> [in <a href="::x_'$=('_x_','_x_')'.html">::x_'$=('_x_','_x_')'</a>]<br/>
<a href="::x_'=='_x.html#::x_'=='_x">_ == _</a> [in <a href="::x_'=='_x.html">::x_'=='_x</a>]<br/>
<a href="::x_'||'_x.html#::x_'||'_x">_ || _</a> [in <a href="::x_'||'_x.html">::x_'||'_x</a>]<br/>
<a href="::x_':=='_x.html#::x_':=='_x">_ :== _</a> [in <a href="::x_':=='_x.html">::x_':=='_x</a>]<br/>
<a href="::x_'$=['_x_','_x_']'.html#::x_'$=['_x_','_x_']'">_ $=[ _ , _ ]</a> [in <a href="::x_'$=['_x_','_x_']'.html">::x_'$=['_x_','_x_']'</a>]<br/>
<a href="::x_'/'_x_'||'_x.html#::x_'/'_x_'||'_x">_ / _ || _</a> [in <a href="::x_'/'_x_'||'_x.html">::x_'/'_x_'||'_x</a>]<br/>