[0] [1] [2] [3] [4] [5] [6] [9] [A] [B] [C] [D] [E] [F] [G] [H] [I] [J] [K] [L] [M] [N] [O] [P] [Q] [R] [S] [T] [U] [V] [W] [X] [Y] [Z]

B

top next

Kan structure on Id_A a b
The Type (Id_A a b)
add_grp_of_rng_wf_b
assert-b-exists
b-exists
b-exists-bfalse
b-exists_wf
b-isect
b-union
b-union-base-equality
b-union-equality-disjoint
b-union-equality-disjoint2
b-union-void
b-union_wf
b_all
b_all-cons
b_all-inst
b_all-map
b_all-map2
b_all-squash-exists-bag
b_all-squash-exists-bag2
b_all-squash-exists-list
b_all-wf2
b_all_wf
isect2-b-union-subtype
l_all_implies_b_all
lapp_fact_b
lookup_omral_scale_b
mul_mon_of_rng_wf_b
not_over_and_b
oalist_cases_b
perm_b
perm_b_f_cancel
perm_b_inj
perm_b_to_f
perm_b_wf
perm_f_b_cancel
perm_induction_b
quot_ring_car_elim_b
strong-continuous-b-union
strong-subtype-b-union
strong-subtype-b-union-better
subtype_rel_b-union
subtype_rel_b-union-left
subtype_rel_b-union-right
subtype_rel_b-union_iff
trans_imp_sp_trans_b
utrans_imp_sp_utrans_b
zero_ann_b

B2I

prev top next

b2i
b2i_bounds
b2i_wf
comb_for_b2i_wf

BACK

prev top next

append_back_nil
can-apply-es-search-back
es-search-back
es-search-back-cases
es-search-back_wf
fun-connected-step-back
isl-es-search-back
select_append_back

BAG

prev top next

assert-bag-all
assert-bag-deq-member
assert-bag-eq
assert-bag-has-no-repeats
assert-bag-null
assert-bag-null-sq
assert-bag_all
assert-deq-sub-bag
b_all-squash-exists-bag
bag
bag-accum
bag-accum-map
bag-accum-single
bag-accum_wf
bag-admissable
bag-admissable-well-founded
bag-admissable_wf
bag-all
bag-all_wf
bag-append
bag-append-ac
bag-append-assoc
bag-append-assoc-comm
bag-append-assoc2
bag-append-cancel
bag-append-comm
bag-append-comm-assoc
bag-append-empty
bag-append-eq-empty
bag-append-equal-bag-rep
bag-append-ident
bag-append-is-empty
bag-append-is-single
bag-append-is-single-iff
bag-append-is-single-iff2
bag-append-no-repeats
bag-append-no-repeats1
bag-append-union
bag-append_wf
bag-bind
bag-bind-append
bag-bind-append2
bag-bind-assoc
bag-bind-com
bag-bind-empty-right
bag-bind-filter
bag-bind_wf
bag-cases
bag-co-restrict
bag-co-restrict-append
bag-co-restrict-disjoint
bag-co-restrict-property
bag-co-restrict-rep
bag-co-restrict_wf
bag-combine
bag-combine-append-empty
bag-combine-append-left
bag-combine-append-right
bag-combine-assoc
bag-combine-bag-append-empty
bag-combine-com
bag-combine-combine
bag-combine-cons-left
bag-combine-empty-left
bag-combine-empty-right
bag-combine-eq-out
bag-combine-eq-right
bag-combine-filter
bag-combine-is-map
bag-combine-is-single-if
bag-combine-map
bag-combine-mapfilter
bag-combine-member-wf
bag-combine-no-repeats
bag-combine-no-repeats2
bag-combine-null
bag-combine-restrict
bag-combine-restrict_wf
bag-combine-single-left
bag-combine-single-right
bag-combine-single-right-as-map
bag-combine-size
bag-combine-size-bound
bag-combine-size-bound2
bag-combine-unit-left
bag-combine-unit-left-top
bag-combine-unit-right
bag-combine_wf
bag-count
bag-count-ap-map
bag-count-append
bag-count-bag-lub
bag-count-combine
bag-count-drop
bag-count-drop-trivial
bag-count-empty
bag-count-filter
bag-count-is-zero
bag-count-map
bag-count-member
bag-count-member-no-repeats
bag-count-remove1
bag-count-rep
bag-count-single
bag-count-sqequal
bag-count_wf
bag-cover
bag-cover_wf
bag-covers
bag-covers_wf
bag-decomp
bag-decomp_wf
bag-decomp_wf2
bag-deq
bag-deq-member
bag-deq-member-bag-diff
bag-deq-member_wf
bag-deq_wf
bag-dickson-lemma
bag-diff
bag-diff-equal-inl
bag-diff-property
bag-diff_wf
bag-disjoint
bag-disjoint_wf
bag-double-summation
bag-double-summation2
bag-drop
bag-drop-commutes
bag-drop-head
bag-drop-no-repeats
bag-drop-property
bag-drop-property2
bag-drop_wf
bag-empty-append
bag-eq
bag-eq-subtype
bag-eq-subtype1
bag-eq_wf
bag-equality
bag-extensionality
bag-extensionality-no-repeats
bag-extensionality1
bag-extensionality2
bag-filter
bag-filter-append
bag-filter-as-accum
bag-filter-combine
bag-filter-combine2
bag-filter-empty
bag-filter-empty-iff
bag-filter-equal
bag-filter-filter
bag-filter-filter2
bag-filter-is-empty
bag-filter-is-nil
bag-filter-is-sub-bag
bag-filter-map
bag-filter-map2
bag-filter-no-repeats
bag-filter-no-repeats2
bag-filter-same
bag-filter-singleton
bag-filter-split
bag-filter-trivial
bag-filter-trivial2
bag-filter-union
bag-filter-union2
bag-filter-wf2
bag-filter-wf3
bag-filter_wf
bag-from-member-function
bag-from-member-function-exists
bag-function
bag-has-no-repeats
bag-has-no-repeats_wf
bag-incomparable
bag-incomparable_wf
bag-induction
bag-inject
bag-inject_wf
bag-intersection
bag-lex
bag-lub
bag-lub-comm
bag-lub-property
bag-lub_wf
bag-map
bag-map'
bag-map'_wf
bag-map-append
bag-map-append-empty
bag-map-as-accum
bag-map-combine
bag-map-cons
bag-map-equal
bag-map-filter
bag-map-list-map
bag-map-map
bag-map-mapfilter
bag-map-member-wf
bag-map-no-repeats
bag-map-null
bag-map-single
bag-map-trivial
bag-map-union
bag-map_wf
bag-mapfilter
bag-mapfilter-append
bag-mapfilter-combine
bag-mapfilter-empty
bag-mapfilter-fast
bag-mapfilter-fast-eq
bag-mapfilter-fast-eq2
bag-mapfilter-fast-map
bag-mapfilter-fast_wf
bag-mapfilter-map
bag-mapfilter-mapfilter
bag-mapfilter-null
bag-mapfilter-wf2
bag-mapfilter_wf
bag-max
bag-max-lb
bag-max-ub
bag-max_wf
bag-maximal?
bag-maximal?-append
bag-maximal?-cons
bag-maximal?-iff
bag-maximal?-max
bag-maximal?-single
bag-maximal?_wf
bag-maximals
bag-maximals-max
bag-maximals-not-max
bag-maximals_wf
bag-member
bag-member-append
bag-member-bag-diff
bag-member-classfun
bag-member-classfun-res
bag-member-combine
bag-member-cons
bag-member-count
bag-member-decidable2
bag-member-decomp
bag-member-empty
bag-member-empty-iff
bag-member-empty-weak
bag-member-evidence
bag-member-filter
bag-member-filter-implies1
bag-member-filter-implies2
bag-member-filter-set
bag-member-filter2
bag-member-from-upto
bag-member-iff
bag-member-iff-hd
bag-member-iff-size
bag-member-iff-sq-list-member
bag-member-ifthenelse
bag-member-implies-hd-append
bag-member-lifting-2
bag-member-lifting-loc-2
bag-member-list
bag-member-list-member
bag-member-map
bag-member-map2
bag-member-map3
bag-member-map3-deq
bag-member-mapfilter
bag-member-not-bag-null
bag-member-partitions
bag-member-parts
bag-member-parts'
bag-member-product
bag-member-remove
bag-member-remove-repeats
bag-member-select
bag-member-single
bag-member-single-weak
bag-member-size
bag-member-splits
bag-member-spread
bag-member-spread-to-pi
bag-member-sq-list-member
bag-member-strong-subtype
bag-member-subtype
bag-member-subtype-2
bag-member-sv-bag-only
bag-member-sv-list
bag-member-two-factorizations
bag-member-union
bag-member_wf
bag-merge
bag-merge_wf
bag-moebius
bag-moebius-inversion
bag-moebius-no-repeats
bag-moebius-property
bag-moebius-property1
bag-moebius_wf
bag-monad
bag-monad_wf
bag-no-repeats
bag-no-repeats-append
bag-no-repeats-cons
bag-no-repeats-count
bag-no-repeats-filter
bag-no-repeats-implies-disjoint
bag-no-repeats-le-bag-size
bag-no-repeats-list
bag-no-repeats-settype
bag-no-repeats-single
bag-no-repeats-subtype
bag-no-repeats-supertype
bag-no-repeats_wf
bag-null
bag-null-append
bag-null-bag-union
bag-null-filter
bag-null-rep
bag-null_wf
bag-only
bag-only_wf
bag-only_wf2
bag-order
bag-order_wf
bag-ordering-wellfounded
bag-partitions
bag-partitions-assoc
bag-partitions-symmetry
bag-partitions-with-one-given
bag-partitions_wf
bag-parts
bag-parts'
bag-parts'-no-repeats
bag-parts'_wf
bag-parts'_wf2
bag-parts-no-repeats
bag-parts_wf
bag-product
bag-product-append
bag-product-empty
bag-product-no-repeats
bag-product-primes
bag-product-single
bag-product_wf
bag-reduce
bag-reduce_wf
bag-remove
bag-remove-append
bag-remove-repeats
bag-remove-repeats-append
bag-remove-repeats-eq-remove-repeats
bag-remove-repeats-filter
bag-remove-repeats-if-no-repeats
bag-remove-repeats-no-repeats
bag-remove-repeats_wf
bag-remove-size
bag-remove-size-member-no-repeats
bag-remove-trivial
bag-remove1
bag-remove1-property
bag-remove1-property1
bag-remove1_wf
bag-remove1_wf1
bag-remove_wf
bag-rep
bag-rep-add
bag-rep-is-single-valued
bag-rep-size-restrict
bag-rep_wf
bag-restrict
bag-restrict-append
bag-restrict-disjoint
bag-restrict-rep
bag-restrict-size-bound
bag-restrict-split
bag-restrict_wf
bag-separate
bag-separate-merge
bag-separate_wf
bag-settype
bag-single-no-repeats
bag-size
bag-size-append
bag-size-as-summation
bag-size-bag-member
bag-size-bound
bag-size-cons
bag-size-filter-member-bound
bag-size-is-zero
bag-size-map
bag-size-one
bag-size-partition
bag-size-rep
bag-size-restrict
bag-size-zero
bag-size_wf
bag-split
bag-splits
bag-splits-permutation
bag-splits-permutation1
bag-splits_wf
bag-splits_wf_list
bag-subtract
bag-subtract-append
bag-subtract-member-if-no-repeats
bag-subtract-no-repeats
bag-subtract-size
bag-subtract_wf
bag-subtype
bag-subtype-list
bag-subtype2
bag-sum
bag-sum-count
bag-sum-nonneg
bag-sum_wf
bag-sum_wf_nat
bag-summation
bag-summation-add
bag-summation-append
bag-summation-cons
bag-summation-constant
bag-summation-constant-int
bag-summation-empty
bag-summation-equal
bag-summation-equal-implies-all-equal
bag-summation-equal-implies-all-equal-1
bag-summation-equal2
bag-summation-filter
bag-summation-from-upto
bag-summation-hom
bag-summation-is-zero
bag-summation-linear
bag-summation-linear-right
bag-summation-linear1
bag-summation-linear1-right
bag-summation-map
bag-summation-minus
bag-summation-partition
bag-summation-partitions-primes
bag-summation-partitions-primes-general
bag-summation-product
bag-summation-reindex
bag-summation-ring-linear1
bag-summation-single
bag-summation-single-non-zero
bag-summation-single-non-zero-no-repeats
bag-summation-split
bag-summation-zero
bag-summation_functionality_wrt_le
bag-summation_functionality_wrt_le_1
bag-summation_wf
bag-to-list
bag-to-list_wf
bag-to-set
bag-to-set_wf
bag-union
bag-union-append
bag-union-bagp
bag-union-cons
bag-union-is-single
bag-union-is-single-if
bag-union-single
bag-union_wf
bag-upto
bag-upto_wf
bag-val
bag-val-append
bag-val-empty
bag-val_wf
bag-value-type
bag-valueall-type
bag_all
bag_all-cons
bag_all-empty
bag_all-map
bag_all_wf
bag_combine_empty_lemma
bag_filter_cons_lemma
bag_filter_empty_lemma
bag_map_empty_lemma
bag_map_single_lemma
bag_null_cons_lemma
bag_null_empty_lemma
bag_only_single_lemma
bag_qinc
bag_remove1_aux
bag_remove1_aux_property
bag_remove1_aux_wf
bag_size_cons_lemma
bag_size_empty_lemma
bag_size_single_lemma
bag_to_squash_list
bag_union_cons_lemma
bag_union_empty_lemma
bag_wf
callbyvalueall-single-bag-combine1
callbyvalueall-single-bag-combine2
callbyvalueall-single-bag-combine3
callbyvalueall-single-bag-combine4
cond-msg-body-sv-bag-only
cons-bag
cons-bag-as-append
cons-bag_wf
cons_bag_append_lemma
cons_bag_empty_lemma
count-bag-remove-repeats
count-bag-to-set
decidable__bag-member
decidable__bag-member2
decidable__equal_bag
decidable__exists-single-valued-bag
decidable__exists_bag-member
decidable__sub-bag
deq-sub-bag
deq-sub-bag_wf
eclass0-bag
eclass0-bag-classrel
eclass0-bag-program
eclass0-bag-program_wf
eclass0-bag_wf
eclass2-bag
eclass2-bag-classrel
eclass2-bag_wf
empty-bag
empty-bag-iff-no-member
empty-bag-iff-size
empty-bag-no-repeats
empty-bag-union
empty-bag-union
empty-bag-wf-list-test
empty-bag_wf
empty-sub-bag
empty_bag_append_lemma
equal-bag-size-le1
equal-count-bag-to-set
equal-empty-bag
eval_bag
eval_bag_wf
fps-mul-coeff-bag-rep-simple
hdf-compose0-bag
hdf-compose0-bag_wf
hdf-parallel-bag
hdf-parallel-bag-iterate
hdf-parallel-bag_wf
imax-bag
imax-bag-lb
imax-bag-ub
imax-bag_wf
int-bag-product
int-bag-product-append
int-bag-product-positive
int-bag-product_wf
int-bag-sum
int-bag-sum-append
int-bag-sum_wf
l_member-bag-member
lifting-bag-combine-decide
lifting-bag-combine-decide-name_eq
list-member-bag-member
list-subtype-bag
map_wf_bag
member-bag-remove-repeats
member-bag-rep
member-bag-to-set
mk_bag
mk_bag_wf
mul-list-bag-product
no-repeats-bag-partitions
no-repeats-bag-to-set
no_repeats-bag
non-empty-bag-implies-non-void
non-empty-bag-mapfilter-union-of-list
non-empty-bag-union-of-list
not-list-member-not-bag-member
null-bag
null-bag-empty
null-bag-filter-map
null-bag-mapfilter
null-bag-size
nysiad_add_to_bag
nysiad_add_to_bag_wf
nysiad_on_input_message_bag
nysiad_on_input_message_bag_wf
only-bag-map
parallel-bag-class
parallel-bag-class_wf
parallel-bag-classrel
radd-list_wf-bag
remove-repeats-wf-bag
return-loc-bag-class
return-loc-bag-class-classrel
return-loc-bag-class-program
return-loc-bag-class-program-wf-hdf
return-loc-bag-class-program_wf
return-loc-bag-class_wf
reverse-bag
select-bag-rep
single-bag
single-bag-append-nil
single-bag-not-null
single-bag_wf
single-valued-bag
single-valued-bag-append
single-valued-bag-combine
single-valued-bag-empty
single-valued-bag-filter
single-valued-bag-hd
single-valued-bag-if-le1
single-valued-bag-is-list
single-valued-bag-is-rep
single-valued-bag-list
single-valued-bag-map
single-valued-bag-single
single-valued-bag-sv-list
single-valued-bag_wf
single-valued-classrel-all-implies-bag
single-valued-classrel-implies-bag
single-valued-list-sv-bag
single-valued-sub-bag
spread-bag-append
sq_stable__bag-member
sq_stable__bag-no-repeats
squash-bag-member
strict-bag-function
strict-bag-function_wf
strict4-bag-combine
strong-message-constraint-bag
strong-message-constraint-bag_wf
strong-subtype-bag
sub-bag
sub-bag-admissable
sub-bag-append-left
sub-bag-append-left2
sub-bag-cancel-right
sub-bag-combine
sub-bag-empty
sub-bag-equal
sub-bag-filter
sub-bag-filter2
sub-bag-filter3
sub-bag-iff
sub-bag-list-if-bag-no-repeats-sq
sub-bag-lub
sub-bag-map-equal
sub-bag-mapfilter-implies
sub-bag-member
sub-bag-no-repeats-iff
sub-bag-of-bag-rep
sub-bag-remove-if
sub-bag-remove-repeats-if-no-repeats
sub-bag-rep
sub-bag-singleton-left
sub-bag-size
sub-bag-union-of-list
sub-bag_antisymmetry
sub-bag_transitivity
sub-bag_weakening
sub-bag_wf
subtype-bag-empty
subtype-bag-only
subtype_rel_bag
sum-as-bag-accum
sv-bag-equals-list
sv-bag-is-bag-rep
sv-bag-is-bag-rep-lousy-proof
sv-bag-only
sv-bag-only-append
sv-bag-only-combine
sv-bag-only-filter
sv-bag-only-map
sv-bag-only-map2
sv-bag-only-single
sv-bag-only_wf
sv-bag-tail
sv-bag-tail-single-valued
sv-bag-tail_wf
sv_bag_only_single_lemma
test-bag-filter-empty
the-member-bag-rep

BAG2

prev top next

b_all-squash-exists-bag2

BAGP

prev top next

bag-union-bagp
bagp
bagp_properties
bagp_wf

BAGS

prev top next

member-sub-bags
residues-equal-bags
similar-bags
similar-bags_wf
single-bags-equal
sub-bags
sub-bags-no-repeats
sub-bags_wf

BALL

prev top next

ball
ball_char
ball_cons_lemma
ball_functionality_wrt_bimplies
ball_functionality_wrt_permr
ball_nil_lemma
ball_respects_bsublist
ball_wf
comb_for_ball_wf

BAND

prev top next

assert_of_band
band
band-bfalse
band-btrue
band-idempotent
band-inl
band-inr
band-is-inl
band-is-inl-base
band-simple-decide
band-simple-int_eq
band-simplify
band-sqequal-inl
band-to-and
band-wf-partial
band_assoc
band_bnot
band_bor_absorption
band_bor_distributive
band_commutes
band_ff_simp
band_mon
band_mon_wf
band_spread_left
band_tt_simp
band_wf
bnot_thru_band
bor_band_absorption
bor_band_distributive
comb_for_band_wf
has-value-band
has-value-band-type
ifthenelse-as-band
ifthenelse-as-band-bnot
strictness-band-left

BAND2

prev top next

assert_of_band2

BAR

prev top next

add-wf-bar
add-wf-bar-int
add-wf-bar-nat
apply-bar
bar def
bar-base
bar-base
bar-base-exteq
bar-base-subtype
bar-base_subtype
bar-base_wf
bar-converges
bar-converges-not-diverges
bar-converges-unique
bar-converges_functionality
bar-converges_wf
bar-delay
bar-delay-equal
bar-delay_wf
bar-diverges
bar-diverges-iff
bar-diverges_functionality
bar-diverges_wf
bar-equal
bar-equal-equiv
bar-equal_wf
bar-induction
bar-induction (dup of thm in list_1)
bar-recursion
bar-recursion_wf
bar-separation
bar-separation_wf
bar-type-continuous
bar-val
bar-val-diverge
bar-val-stable
bar-val_wf
bar-wf-base
bar_induction
bar_recursion
bar_recursion_wf
bar_recursion_wf0
bar_recursion_wf_strong
bar_wf
bar_wf_base
basic-bar-induction
basic_bar_induction
basic_strong_bar_induction
bool-bar-induction
bool_bar_induction
eq_int-wf-bar
eq_int-wf-bar-int
equal-in-bar
fan-implies-bar-sep
fix_wf_bar
fixpoint-induction-bottom-bar
has-value-equality-fix-bar
has-value_wf-bar
imax-wf-bar
imax-wf-bar-nat
implies-bar-equal
in-bar
in-bar-converges
in-bar-equal
in-bar_wf
le_int-wf-bar
le_int-wf-bar-int
length-in-bar-int-if-co-list
length_base_to_bar
member-bar-void
monotone-bar-induction1
pi-bar-trans
pi-bar-trans-comment
pi-bar-trans_wf
strong-subtype-bar
subtract-wf-bar
subtract-wf-bar-int
subtype_bar

BAR2

prev top next

subtype_bar2

BAR345566

prev top next

vr_test_foo_bar345566

BAR345566546

prev top next

vr_test_foo_bar345566546

BARRED

prev top next

AF-path-barred
cWO-rel-path-barred
decidable__pcw-pp-barred
descending-chain-barred-implies-wellfounded
fan-implies-barred-not-unbounded
pcw-pp-barred
pcw-pp-barred-W
pcw-pp-barred-W-decidable
pcw-pp-barred_wf
pcw-pp-barred_wf0

BARS

prev top next

W-bars
W-bars_wf
sq_stable__W-bars
stump-bars
tree-bars
tree-bars_wf
w-bars
w-bars_wf

BARSQTYPE

prev top next

subtype_barSqtype_base

BASE

prev top next

CLK_msg'base
CLK_msg'base-program
CLK_msg'base-program_wf
CLK_msg'base_wf
C_TYPE_subtype_base
OARcast_oarcast'base
OARcast_oarcast'base-program
OARcast_oarcast'base-program_wf
OARcast_oarcast'base_wf
TC-base
add-zero-base
assert-es-ble-base
assert-es-eq-E-base
assert-null-base
atom1_subtype_base
atom2_subtype_base
atom_subtype_base
atomic-values_subtype_base
b-union-base-equality
band-is-inl-base
bar-base
bar-base
bar-base-exteq
bar-base-subtype
bar-base_subtype
bar-base_wf
bar-wf-base
bar_wf_base
base def
base-CP
base-CP_wf
base-class-caused-by
base-class-caused-by_wf
base-class-program
base-class-program-wf-hdf
base-class-program-wf-sub
base-class-program_wf
base-classrel-equal
base-disjoint-classrel
base-equal-partial
base-headers-msg-val
base-headers-msg-val-es-sv
base-headers-msg-val-loc
base-headers-msg-val-loc_wf
base-headers-msg-val-single-val
base-headers-msg-val_wf
base-member-of-tagged+
base-member-partial
base-member-per-function
base-member-prop
base-noloc-classrel
base-noloc-classrel-make-Msg
base-noloc-classrel-make-Msg2
base-noloc-classrel2
base-partial
base-partial-not-exception
base-partial-partial
base-partial_wf
base-process-class
base-process-class-program
base-process-class-program-ap
base-process-class-program_wf
base-process-class-program_wf1
base-process-class_wf
base-process-inputs
base-process-inputs-non-null
base-process-inputs_wf
base-type-family
base-type-family-implies
base-type-family_wf
base_sq
base_wf
baseof_subtype_base
bool_subtype_base
canonicalizable-base
classfun-res-base
classfun-res-base-classrel
classfun-res-member-base
co-list-islist-islist-new-compactness-base
corec_subtype_base
decidable__equal-es-base-E
div_base_case
eclass0-base-classrel
eclass1-base-classrel
eo-forward-base-E
eo-forward-base-classfun
eo-forward-base-classfun-res
eo-forward-base-classfun-res-sq
eo-forward-base-classfun-sq
eo-forward-base-classrel
eo-forward-base-pred
eo-strict-forward-base-E
equal-wf-T-base
equal-wf-base
equal-wf-base-T
es-base-E
es-base-E_wf
es-base-pred
es-base-pred-le
es-base-pred-less
es-base-pred-properties
es-base-pred_wf
es-ble-wf-base
es-causl-swellfnd-base
es-causl-total-base
es-causl-wf-base
es-eq-E-wf-base
es-eq-wf-base
es-loc-wf-base
es-locless-wf-base
es-pred-less-base
es-pred-loc-base
es-pred-maximal-base
es-pred-wf-base
es-pred_property_base
es-rank-wf-base
es-rank_property-base
evalall-append-implies-list-base
extd-nameset_subtype_base
fixpoint-induction-bottom-base
global-eo-base-E
has-value-wf-base
has-value_wf_base
has-valueall_wf_base
hdf-base
hdf-base-ap
hdf-base-ap-fst
hdf-base-transformation1
hdf-base-transformation1-base
hdf-base-transformation2
hdf-base_wf
hdf-memory-base
hdf-state-base
ifthenelse_wf-partial-base
int_subtype_base
isect_subtype_base
iterate-base-process-class-program
itop_unroll_base
length_base_to_bar
list_subtype_base
member-base-class
member-base-class2
member-base-class_iff
modulus_base
mon_itop_unroll_base
nameset_subtype_base
nameset_subtype_base
new_23_sig_decided'base
new_23_sig_decided'base-program
new_23_sig_decided'base-program_wf
new_23_sig_decided'base_wf
new_23_sig_propose'base
new_23_sig_propose'base-program
new_23_sig_propose'base-program_wf
new_23_sig_propose'base_wf
new_23_sig_retry'base
new_23_sig_retry'base-program
new_23_sig_retry'base-program_wf
new_23_sig_retry'base_wf
new_23_sig_vote'base
new_23_sig_vote'base-program
new_23_sig_vote'base-program_wf
new_23_sig_vote'base_wf
no-value-bottom-base
not_has-value_decidable_on_base
nysiad_add2bag'base
nysiad_add2bag'base-program
nysiad_add2bag'base-program_wf
nysiad_add2bag'base_wf
nysiad_addwaiting'base
nysiad_addwaiting'base-program
nysiad_addwaiting'base-program_wf
nysiad_addwaiting'base_wf
nysiad_inputmsg'base
nysiad_inputmsg'base-program
nysiad_inputmsg'base-program_wf
nysiad_inputmsg'base_wf
nysiad_kdeliver'base
nysiad_kdeliver'base-program
nysiad_kdeliver'base-program_wf
nysiad_kdeliver'base_wf
nysiad_ready'base
nysiad_ready'base-program
nysiad_ready'base-program_wf
nysiad_ready'base_wf
parallel composition of base-process-class
partial-base
per-class-base
per-class-base-singleton
per-function_wf_base_family
per-value_subtype_base
polymorphic-constant-base
product_subtype_base
pv11_p1_adopted'base
pv11_p1_adopted'base-program
pv11_p1_adopted'base-program_wf
pv11_p1_adopted'base_wf
pv11_p1_decision'base
pv11_p1_decision'base_wf
pv11_p1_p1a'base
pv11_p1_p1a'base-program
pv11_p1_p1a'base-program_wf
pv11_p1_p1a'base_wf
pv11_p1_p1b'base
pv11_p1_p1b'base-program
pv11_p1_p1b'base-program_wf
pv11_p1_p1b'base_wf
pv11_p1_p2a'base
pv11_p1_p2a'base-program
pv11_p1_p2a'base-program_wf
pv11_p1_p2a'base_wf
pv11_p1_p2b'base
pv11_p1_p2b'base-program
pv11_p1_p2b'base-program_wf
pv11_p1_p2b'base_wf
pv11_p1_preempted'base
pv11_p1_preempted'base-program
pv11_p1_preempted'base-program_wf
pv11_p1_preempted'base_wf
pv11_p1_propose'base
pv11_p1_propose'base-program
pv11_p1_propose'base-program_wf
pv11_p1_propose'base_wf
quotient-isect-base
ranked-eo-base-E
rec-value_subype_base
rem_base_case
rem_base_case_z
rem_gen_base_case
rng_sum_unroll_base
sdata_subtype_base
set_subtype_base
simple-product_subtype_base
single-valued-base-classrel
single-valued-base-loc-classrel
sparse-rep-base
sparse-rep-base_wf
sqequal-wf-base
sqle_wf_base
stream_subtype_base
strong-subtype-isect-base
strong-subtype-union-base
subtype_barSqtype_base
subtype_base_sq
subtype_partial_sqtype_base
t-sqle-base
termination-equality-base
tree_subtype_base
tunion_subtype_base
typed-base-class
typed-base-class_wf
union_subtype_base
unit_subtype_base
unsquashed-weak-continuity-base-false
urec_subtype_base
zero-add-base

BASE2

prev top next

hdf-memory-base2-2
hdf-memory-base2-3
hdf-state-base2-2
hdf-state-base2-3
quotient-isect-base2

BASE3

prev top next

hdf-memory-base3-2
hdf-memory-base3-3
hdf-state-base3-2
hdf-state-base3-3

BASE4

prev top next

hdf-memory-base4-2
hdf-memory-base4-3
hdf-state-base4-2
hdf-state-base4-3

BASEOF

prev top next

baseof
baseof_sq
baseof_subtype
baseof_subtype_base
baseof_wf

BASIC

prev top next

basic-bar-induction
basic-continuity
basic-seq-1-1
basic-seq-1-1_wf
basic-seq-1-2
basic-seq-1-2_wf
basic-seq-1-3
basic-seq-1-3_wf
basic-seq-1-4
basic-seq-1-4_wf
basic-seq-1-5
basic-seq-1-5_wf
basic_bar_induction
basic_strong_bar_induction
is-basic-seq
is-basic-seq_wf
ses-basic-sequence1
ses-basic-sequence1_wf

BASICMESSAGE

prev top next

basicMessage
basicMessage-valueall-type
basicMessage_wf

BASICMSG

prev top next

make-basicMsg
make-basicMsg_wf

BBAR

prev top next

bbar-recursion
bbar-recursion_wf

BDD

prev top next

accelerate-bdd-diff
assert-bdd-all
bdd-all
bdd-all-btrue
bdd-all_wf
bdd-diff
bdd-diff-add
bdd-diff-equiv
bdd-diff-iff-eventual
bdd-diff-regular
bdd-diff-regular-int-seq
bdd-diff_functionality
bdd-diff_inversion
bdd-diff_transitivity
bdd-diff_weakening
bdd-diff_wf
bdd-val
bdd-val_wf
bdd_all_zero_lemma
rabs_functionality_wrt_bdd-diff
radd-bdd-diff
reg-seq-add_functionality_wrt_bdd-diff
reg-seq-list-add_functionality_wrt_bdd-diff
reg-seq-mul_functionality_wrt_bdd-diff
req-iff-bdd-diff
rmax_functionality_wrt_bdd-diff
rmin_functionality_wrt_bdd-diff
rminus_functionality_wrt_bdd-diff
rmul-bdd-diff-reg-seq-mul
trivial-bdd-diff

BE

prev top next

more-things-that-can-be-run
things-that-can-be-run

BEESON

prev top next

Beeson's Constructive Tarski Geometry

BEFORE

prev top next

adjacent-before
before
before-adjacent
before-adjacent2
before-hd
before-map
before-reverse
before-upto
before_all_imp_before
before_all_imp_count_zero
before_cons_lemma
before_imp_before_all
before_last
before_last_or
before_nil_lemma
before_trans
before_wf
class-le-before
class-le-before_wf
comb_for_before_wf
cons_before
decidable__existse-before
eo-forward-before
eo-forward-le-before
eo-forward-split-before
eo-strict-forward-before
es-before
es-before-decomp
es-before-is-nil-if-first
es-before-no_repeats
es-before-partition
es-before-pred-length
es-before-split-last
es-before_wf
es-before_wf2
es-before_wf3
es-closed-open-interval-eq-before
es-first-before
es-happened-before
es-happened-before_wf
es-interval-eq-le-before
es-le-before
es-le-before-filter
es-le-before-if-first
es-le-before-no_repeats
es-le-before-not-null
es-le-before-ordered
es-le-before-partition
es-le-before-partition2
es-le-before-pred
es-le-before-split-last
es-le-before_wf
es-le-before_wf2
existse-before
existse-before-iff
existse-before_wf
filter_before
firstn-before
firstn-le-before
fun-path-before
global-eo-before
global-eo-info-before
global-eo-info-le-before
hd-before
hd-es-le-before
hd-es-le-before-is-first
iseg-es-before
iseg-es-before-is-before
iseg-es-le-before
iseg-es-le-before-is-before
l_before
l_before-es-before
l_before-es-before-iff
l_before-es-interval
l_before-es-le-before-iff
l_before-filter
l_before-sorted-by
l_before_antisymmetry
l_before_append
l_before_append_front
l_before_append_iff
l_before_filter
l_before_filter_set_type
l_before_filter_subtype
l_before_interleaving
l_before_iseg
l_before_l_index
l_before_l_index_le
l_before_map
l_before_mapfilter
l_before_member
l_before_member2
l_before_no_repeats
l_before_select
l_before_sublist
l_before_swap
l_before_transitivity
l_before_wf
last-es-le-before
last-not-before
list-eo-before
list-eo-info-before
list-eo-info-le-before
lookup_before_start
lookup_before_start_a
member-class-le-before
member-es-before
member-es-le-before
nil_before
no_repeats-before-equality
nth_tl-es-before
ranked-eo-before
ranked-eo-info-before
ranked-eo-info-le-before
release-before
release-before_wf
retraction-fun-path-before
rng_before_all_imp_before
rng_before_imp_before_all
rng_lookup_before_start
singleton_before
strong_before
strong_before_wf
tl-es-le-before
weak_l_before_append_front

BEFORE2

prev top next

es-first-before2
member-es-le-before2

BEFORE3

prev top next

member-es-le-before3

BETA

prev top next

beta_expansion
cubical-beta

BETTER

prev top next

better-fibs
better-fibs-equal-map
better-fibs_wf
better-gcd
better-gcd-gcd
better-gcd_wf
better-q-elim
decidable__implies_better
decidable__l_all-better-extract
decidable__l_exists_better-extract
nth-better-fibs
strong-subtype-b-union-better

BETWEEN

prev top next

between-fun-connected
es-pred-exists-between
eu-add-length-between
eu-add-length-between-iff
eu-between
eu-between-eq
eu-between-eq-def
eu-between-eq-exchange3
eu-between-eq-exchange4
eu-between-eq-implies-colinear
eu-between-eq-implies-colinear2
eu-between-eq-implies-colinear3
eu-between-eq-inner-trans
eu-between-eq-outer-trans
eu-between-eq-same
eu-between-eq-same-side
eu-between-eq-same-side2
eu-between-eq-same2
eu-between-eq-symmetry
eu-between-eq-trivial-left
eu-between-eq-trivial-right
eu-between-eq_wf
eu-between-implies-between-eq
eu-between-same
eu-between-same2
eu-between-sym
eu-between-trans
eu-between-trans2
eu-between_wf
eu-congruent-between-exists
eu-congruent-between-implies-equal
eu-congruent-preserves-between
i-member-between
int-between
ravg-between
rel-path-between
rel-path-between-append
rel-path-between-cons
rel-path-between_wf
sq_stable__eu-between
sq_stable__eu-between-eq
stable__eu-between
stable__eu-between-eq
stable_eu-between-eq

BETWEEN1

prev top next

alle-between1
alle-between1-false
alle-between1-not-first-since
alle-between1-trivial
alle-between1-true
alle-between1_functionality_wrt_iff
alle-between1_wf
decidable__alle-between1
decidable__exists-classrel-between1
decidable__exists-classrel-between1-sv
decidable__existse-between1
existse-between1
existse-between1-false
existse-between1-true
existse-between1_functionality_wrt_iff
existse-between1_wf

BETWEEN2

prev top next

alle-between2
alle-between2-false
alle-between2-not-first-since
alle-between2-true
alle-between2_functionality_wrt_iff
alle-between2_wf
decidable__alle-between2
decidable__existse-between2
es-pplus-alle-between2
es-pred-exists-between2
existse-between2
existse-between2-false
existse-between2-true
existse-between2_functionality_wrt_iff
existse-between2_wf

BETWEEN3

prev top next

alle-between3
alle-between3-false
alle-between3_wf
decidable__exists-classrel-between3
decidable__exists-classrel-between3-sv
decidable__exists-iterated-classrel-between3-sv
decidable__exists-last-classrel-between3
decidable__exists-last-classrel-between3-sv
decidable__exists-pred-iterated-classrel-between3-sv
decidable__existse-between3
existse-between3
existse-between3-false
existse-between3-true
existse-between3_functionality_wrt_iff
existse-between3_wf

BEXISTS

prev top next

bexists
bexists_char
bexists_cons_lemma
bexists_iff_exists_nth
bexists_nil_lemma
bexists_wf

BEZEM

prev top next

Theorem 6.2 in Bezem,Coquand,Huber

BEZOUT

prev top next

bezout_ident
bezout_ident_n
coprime_bezout_id
coprime_bezout_id0
coprime_bezout_id1
coprime_bezout_id2

BFALSE

prev top next

b-exists-bfalse
band-bfalse
bfalse
bfalse_wf
bl-exists-bfalse
bor-bfalse
btrue_neq_bfalse
decide_bfalse_lemma
exposed-bfalse
inr_eq_bfalse
member-implies-null-eq-bfalse
not-bfalse-sqle-btrue
not-btrue-sqeq-bfalse
not-btrue-sqle-bfalse
not-name_eq-implies-sq-bfalse
reduce-bool-bfalse

BIG

prev top next

decidable__tree-big
not-tree-big
tree-big
tree-big-least
tree-big-monotone
tree-big_wf

BIGGER

prev top next

bigger-int
bigger-int-property
bigger-int-property2
bigger-int_wf

BIGREL

prev top next

bigrel
bigrel-iff
bigrel-induction
bigrel-induction-monotone
bigrel_wf
implies-bigrel

BIJ

prev top next

bij_iff_1_1_corr
bij_imp_exists_inv
fun_with_inv_is_bij

BIJ2

prev top next

fun_with_inv_is_bij2

BIJECT

prev top next

biject
biject-iff
biject-iff-inverse
biject-inverse
biject-inverse2
biject_functionality
biject_wf
id-biject

BIJECTION

prev top next

bijection_restriction
code-pair-bijection
code-seq-bijection
es-class-causal-rel-iff-bijection
flip_bijection
injection-bijection
stream-bijection

BILINEAR

prev top next

algebra_bilinear
bilinear
bilinear_comm_elim
bilinear_p
bilinear_p_wf
bilinear_wf
omral_bilinear
omral_bilinear_a
sq_stable__bilinear
sq_stable__bilinear_p

BIMPLIES

prev top next

assert_functionality_wrt_bimplies
assert_of_bimplies
ball_functionality_wrt_bimplies
bimplies
bimplies_transitivity
bimplies_weakening
bimplies_wf
comb_for_bimplies_wf
rev_bimplies
rev_bimplies_wf

BIN

prev top next

integer-sqrt-bin-search

BINARY

prev top next

binary-fps
binary-fps_wf
binary-map
binary-map_wf
binary-search
binary-search_wf
binary-tree
binary-tree-definition
binary-tree-ext
binary-tree-induction
binary-tree_ind
binary-tree_ind_wf
binary-tree_ind_wf_simple
binary-tree_size
binary-tree_size_wf
binary-tree_wf
binary-treeco
binary-treeco-ext
binary-treeco_size
binary-treeco_size_wf
binary-treeco_wf
binary_map
binary_map-definition
binary_map-ext
binary_map-induction
binary_map_case
binary_map_case-wf2
binary_map_case_E
binary_map_case_E_reduce_lemma
binary_map_case_T
binary_map_case_T_reduce_lemma
binary_map_case_wf
binary_map_ind
binary_map_ind-wf2
binary_map_ind_wf
binary_map_ind_wf_simple
binary_map_size
binary_map_size_wf
binary_map_wf
binary_mapco
binary_mapco-ext
binary_mapco_size
binary_mapco_size_wf
binary_mapco_wf

BIND2

prev top next

A-bind2
A-bind2_wf

BINOMIAL

prev top next

binomial
binomial-inequality1
binomial-int
real-binomial

BINREL

prev top next

ab_binrel
ab_binrel_functionality
ab_binrel_wf
binrel_ap
binrel_ap_functionality_wrt_breqv
binrel_ap_wf
binrel_eqv
binrel_eqv_functionality_wrt_breqv
binrel_eqv_inversion
binrel_eqv_transitivity
binrel_eqv_weakening
binrel_eqv_wf
binrel_le
binrel_le_antisymmetry
binrel_le_transitivity
binrel_le_weakening
binrel_le_wf
dec_binrel
dec_binrel_wf

BISIMULATION

prev top next

F-bisimulation
F-bisimulation_wf
indexed-F-bisimulation
indexed-F-bisimulation_wf

BL

prev top next

assert-bl-all
assert-bl-all-2
assert-bl-exists
assert-bl-exists2
bl-all
bl-all-as-accum
bl-all-btrue
bl-all_wf
bl-exists
bl-exists-append
bl-exists-as-accum
bl-exists-bfalse
bl-exists-cons
bl-exists-filter
bl-exists-first
bl-exists-map
bl-exists-nil
bl-exists-singleton
bl-exists-singleton-top
bl-exists_wf
bl-rev-exists
bl-rev-exists-sq
bl-rev-exists_wf
not-assert-bl-all
not-assert-bl-exists
not-bl-exists-eq-bl-all

BLACK

prev top next

red-black-example
red-black-example-ext
test-red-black-example

BLE

prev top next

assert-es-ble
assert-es-ble-base
eo-forward-ble
eo-strict-forward-ble
es-ble
es-ble-wf-base
es-ble_wf
es-bless-not-ble
oal_ble
oal_ble_wf

BLESS

prev top next

assert-es-bless
eo-forward-bless
eo-strict-forward-bless
es-bless
es-bless-not-ble
es-bless_wf
es-blocl-is-bless

BLEX

prev top next

assert-pair-blex
pair-blex
pair-blex_wf

BLOCK

prev top next

A-block
A-block_wf

BLOCKED

prev top next

cs-archive-blocked
cs-archive-blocked_wf
decidable__cs-archive-blocked

BLOCL

prev top next

es-blocl
es-blocl-iff
es-blocl-is-bless
es-blocl_wf

BLT

prev top next

assert_of_grp_blt
assert_of_oal_blt
comb_for_set_blt_wf
grp_blt
grp_blt_wf
oal_blt
oal_blt_wf
set_blt
set_blt_functionality_wrt_set_lt_r
set_blt_wf

BM

prev top next

bm_E
bm_E-wf2
bm_E?
bm_E?_wf
bm_E_wf
bm_N
bm_N_wf
bm_T
bm_T'
bm_T'_wf
bm_T-cnt
bm_T-cnt_wf
bm_T-key
bm_T-key_wf
bm_T-left
bm_T-left_wf
bm_T-right
bm_T-right_wf
bm_T-value
bm_T-value_wf
bm_T-wf2
bm_T_wf
bm_cnt_prop
bm_cnt_prop0
bm_cnt_prop0_E
bm_cnt_prop0_E_reduce_lemma
bm_cnt_prop0_T
bm_cnt_prop0_wf
bm_cnt_prop_E
bm_cnt_prop_E_reduce_lemma
bm_cnt_prop_T
bm_cnt_prop_pos
bm_cnt_prop_wf
bm_collate_left
bm_collate_left_wf
bm_collate_next
bm_collate_next_wf
bm_compare
bm_compare_antisym_le
bm_compare_connex_le
bm_compare_greater_greater_false
bm_compare_greater_to_less_eq
bm_compare_int
bm_compare_int_wf
bm_compare_less_less_false
bm_compare_less_to_greater_eq
bm_compare_refl_eq
bm_compare_refl_le
bm_compare_sym_eq
bm_compare_trans_le
bm_compare_wf
bm_count
bm_count_E
bm_count_E_reduce_lemma
bm_count_T
bm_count_prop
bm_count_prop_pos
bm_count_wf
bm_delete'
bm_delete'_wf
bm_delmin
bm_delmin_wf
bm_double_L
bm_double_L_wf
bm_double_R
bm_double_R_wf
bm_empty
bm_empty_wf
bm_exists
bm_exists_downeq
bm_exists_downeq_wf
bm_exists_wf
bm_find
bm_find_wf
bm_first
bm_first_wf
bm_firsti
bm_firsti_wf
bm_foldl
bm_foldl_wf
bm_foldli
bm_foldli_aux
bm_foldli_aux_wf
bm_foldli_wf
bm_inDomain
bm_inDomain_wf
bm_insert
bm_insert'
bm_insert'_wf
bm_insert_if_not_in
bm_insert_if_not_in_wf
bm_insert_wf
bm_isEmpty
bm_isEmpty_wf
bm_listItems
bm_listItems_d2l
bm_listItems_d2l_wf
bm_listItems_wf
bm_listItemsi
bm_listItemsi_d2l
bm_listItemsi_d2l_wf
bm_listItemsi_wf
bm_listKeys
bm_listKeys_d2l
bm_listKeys_d2l_wf
bm_listKeys_wf
bm_lookup
bm_lookup_wf
bm_map
bm_map_wf
bm_mapi
bm_mapi_wf
bm_min
bm_min_wf
bm_numItems
bm_numItems_E
bm_numItems_E_reduce_lemma
bm_numItems_T
bm_numItems_T_reduce_lemma
bm_numItems_is_cnt_prop0
bm_numItems_wf
bm_remove
bm_remove_wf
bm_single_L
bm_single_L_wf
bm_single_R
bm_single_R_wf
bm_singleton
bm_singleton_wf
bm_try_remove
bm_try_remove_wf
bm_unionWith
bm_unionWith_ins
bm_unionWith_ins_wf
bm_unionWith_wf
bm_wt
bm_wt_wf

BMSEXISTS

prev top next

bmsexists_char
bmsexists_char_a
bmsexists_char_a_rw
bmsexists_char_rw

BNF

prev top next

BNF-list-case0
BNF-list-case1

BNOT

prev top next

assert-bnot
assert_of_bnot
band_bnot
bnot
bnot-ff
bnot-inl
bnot-inr
bnot-tt
bnot-wf-partial
bnot_bnot
bnot_bnot_elim
bnot_of_le_int
bnot_of_lt_int
bnot_thru_band
bnot_thru_bor
bnot_thru_exists
bnot_wf
bor_bnot
comb_for_bnot_wf
decide-bnot
equal-bnot
has-value-bnot
has-value-bnot-type
ifthenelse-as-band-bnot
ifthenelse-as-bor-bnot
length-filter-bnot
test-bnot-nbot

BNUM

prev top next

not-pv11_p1_leq_bnum
pv11_p1_bnum_p2a
pv11_p1_bnum_p2a_loc
pv11_p1_inc_acc_bnum_fun
pv11_p1_is_bnum
pv11_p1_is_bnum_wf
pv11_p1_ldr_fun_loc_bnum
pv11_p1_ldr_loc_bnum
pv11_p1_leq_bnum
pv11_p1_leq_bnum'
pv11_p1_leq_bnum'_wf
pv11_p1_leq_bnum_dummy
pv11_p1_leq_bnum_dummy_eq
pv11_p1_leq_bnum_implies_eq
pv11_p1_leq_bnum_implies_eq_or_lt
pv11_p1_leq_bnum_linorder
pv11_p1_leq_bnum_max
pv11_p1_leq_bnum_max2
pv11_p1_leq_bnum_or
pv11_p1_leq_bnum_refl
pv11_p1_leq_bnum_wf
pv11_p1_lt_bnum
pv11_p1_lt_bnum'
pv11_p1_lt_bnum'_wf
pv11_p1_lt_bnum_implies_not
pv11_p1_lt_bnum_implies_not2
pv11_p1_lt_bnum_implies_not3
pv11_p1_lt_bnum_irrefl
pv11_p1_lt_bnum_irrefl2
pv11_p1_lt_bnum_trans
pv11_p1_lt_bnum_trans1
pv11_p1_lt_bnum_trans2
pv11_p1_lt_bnum_upd
pv11_p1_lt_bnum_wf
pv11_p1_max_bnum
pv11_p1_max_bnum_comm
pv11_p1_max_bnum_dummy
pv11_p1_max_bnum_if_leq
pv11_p1_max_bnum_wf
pv11_p1_mk_bnum
pv11_p1_mk_bnum_wf
pv11_p1_upd_bnum
pv11_p1_upd_bnum_wf

BNUMS

prev top next

pv11_p1_eq_bnums
pv11_p1_eq_bnums-assert
pv11_p1_eq_bnums_wf

BOARD

prev top next

board-cell
board-cell_wf
map-square-board
map-square-board-cell
map-square-board_wf
square-board
square-board-subtype
square-board_wf

BODY

prev top next

cond-msg-body
cond-msg-body-cbva
cond-msg-body-single-valued
cond-msg-body-sv-bag-only
cond-msg-body_wf
cond-verify-msg-body
cond-verify-msg-body_wf
eo-forward-equal-info-body
eo-forward-info-body
equal-info-body
equal-info-body_wf
es-info-body
es-info-body-equal
es-info-body_wf
mFOquant-body
mFOquant-body_wf
map-cond-msg-body
msg-body
msg-body-cmp
msg-body-cmp_wf
msg-body_wf
msg-body_wf2
picomm-body
picomm-body_wf
pinew-body
pinew-body_wf
pirep-body
pirep-body_wf
sq_stable__equal-info-body
trivial-equal-info-body

BODYMAKEMSG

prev top next

bodymakeMsg_lemma

BOOL

prev top next

assert_of_eq_bool
bool
bool-bar-induction
bool-cardinality-le
bool-cmp
bool-cmp-zero
bool-cmp_wf
bool-decider
bool-decider_wf
bool-deq
bool-deq-aux
bool-deq_wf
bool-inhabited
bool-mono
bool-size
bool-size_wf
bool-to-dcdr
bool-to-dcdr-aux
bool-to-dcdr_wf
bool-to-neg-dcdr
bool-to-neg-dcdr-aux
bool-to-neg-dcdr_wf
bool-tt-or-ff
bool_bar_induction
bool_cases
bool_cases_sqequal
bool_decision
bool_ind
bool_sim_false
bool_sim_true
bool_sq
bool_subtype_base
bool_wf
dcdr-to-bool
dcdr-to-bool-equivalence
dcdr-to-bool_wf
decidable__all_length_bool
decidable__bool
decidable__equal_bool
decidable__exists_length_bool
eq_bool
eq_bool_ff
eq_bool_tt
eq_bool_wf
es-interface-le-pred-bool
es-interface-local-pred-bool
fan-iff-dfan-bool
finite-type-bool
free-from-atom-bool
free-from-atom-bool-subtype
iff_imp_equal_bool
inconsistent-bool-eq
inconsistent-bool-eq2
inconsistent-bool-eq3
inconsistent-bool-eq4
isatom-bool-if-has-value
isatom1-bool-if-has-value
isatom2-bool-if-has-value
isaxiom-bool-if-bunion-unit-prod
isaxiom-bool-if-has-value
isinl-bool-if-has-value
isinr-bool-if-has-value
isint-bool-if-has-value
islambda-bool-if-has-value
ispair-bool-if-bunion-unit-prod
ispair-bool-if-co-list
ispair-bool-if-has-value
ite-bool-1
ite-bool-2
ite-bool-3
ite-bool-4
member-disjoint-union-comb-bool
member-parallel-class-bool
nwkl!-iff-twkl!-bool
polymorphic-constant-bool
reduce-bool-bfalse
wkl!-iff-twkl!-bool

BOOT

prev top next

boot-process
boot-process_wf

BOR

prev top next

assert_of_bor
band_bor_absorption
band_bor_distributive
bnot_thru_bor
bor
bor-assoc
bor-bfalse
bor-btrue
bor-inl
bor-inr
bor-simplify
bor-to-and
bor_assoc
bor_band_absorption
bor_band_distributive
bor_bnot
bor_ff_simp
bor_mon
bor_mon_wf
bor_tt_simp
bor_wf
comb_for_bor_wf
has-value-bor
has-value-bor-type
ifthenelse-as-bor
ifthenelse-as-bor-bnot
mapfilter-bor
mapfilter-bor-eq
mset_sum_bor_mon_hom
mset_union_bor_mon_hom

BOT

prev top next

is-list-if-has-value-rec-pair-bot

BOTH

prev top next

one_or_both
one_or_both-induction
one_or_both_ind
one_or_both_ind_oobboth_lemma
one_or_both_ind_oobright_lemma
one_or_both_ind_wf
one_or_both_oobleft_lemma
one_or_both_wf
radd-rminus-both
radd-zero-both
rmul-one-both
rmul-zero-both

BOTTOM

prev top next

Sierpinski-bottom
Sierpinski-bottom_wf
Sierpinski-equal-bottom
apply-bottom
bottom
bottom-member-prop
bottom-sqequal-fix-id
bottom-sqle
bottom_diverge
bottom_wf
bottom_wf-partial
bottom_wf_function
cbv_bottom_lemma
decide-bottom
equal-Sierpinski-bottom
exception-not-bottom
exception-not-bottom_1
exception-not-value-or-bottom
fixpoint-induction-bottom
fixpoint-induction-bottom-bar
fixpoint-induction-bottom-base
no-value-bottom
no-value-bottom
no-value-bottom-base
not-Sierpinski-bottom
not-btrue-sqeq-bottom
not-btrue-sqle-bottom
not-has-value-bottom
not-id-sqle-bottom
not-is-exception-bottom
not_id_sqeq_bottom
select-is-bottom
sp-join-bottom
sp-join-is-bottom
sp-le-bottom
sp-lub-is-bottom
sp-meet-bottom
spread-axiom-sqequal-bottom

BOTTOM2

prev top next

fixpoint-induction-bottom2

BOUND

prev top next

Inorm-bound
absval-diff-product-bound
bag-combine-size-bound
bag-restrict-size-bound
bag-size-bound
bag-size-filter-member-bound
bound_in_prefix
bound_in_prefix_wf
canonical-bound
canonical-bound_wf
class-loc-bound
class-loc-bound_wf
connection-bound
divisor_bound
divisors_bound
es-bound-list
es-bound-list2
exp_difference_bound
fact-bound
filter-interface-predecessors-lower-bound
filter-interface-predecessors-lower-bound-implies
fixpoint-upper-bound
fps-degree-bound
fps-degree-bound_wf
fps-support-degree-bound
frs-mesh-bound
fset_of_mset_count_bound
i-member-diff-bound
increasing_lower_bound
integer-bound
integer-class-bound-exists
l_sum-lower-bound
l_sum-upper-bound
l_sum-upper-bound-map
least-upper-bound
length-concat-lower-bound
length-filter-lower-bound
lower-bound
lower-bound_wf
mFOL-bound-rename
mFOL-rename-bound-to-avoid
mFOL-rename-bound-to-avoid_wf
monotone-upper-bound-function
mset_count_bound_for_union
mu-bound
mu-bound-property
mu-bound-property+
mu-bound-unique
mu-ge-bound
mu-ge-bound-property
next_wf_bound
omral_scale_dom_bound
pdivisor_bound
r-bound
r-bound-property
r-bound_wf
r-strict-bound-property
rabs-difference-bound-iff
rabs-difference-bound-rleq
rabs-difference-lower-bound
rem_mag_bound
strict-upper-bound
strict-upper-bound_functionality
strict-upper-bound_wf
sum_bound
sum_lower_bound
upper-bound
upper-bound_functionality
upper-bound_wf
ws-lower-bound

BOUND2

prev top next

bag-combine-size-bound2
filter-interface-predecessors-lower-bound2

BOUND3

prev top next

filter-interface-predecessors-lower-bound3

BOUNDED

prev top next

bounded-above
bounded-above-strict
bounded-above_wf
bounded-expectation
bounded-sequence
bounded-sequence_wf
class-at-loc-bounded
continuous-compact-range-totally-bounded
continuous-range-totally-bounded
converges-implies-bounded
decidable__wellfound-bounded-exists
global-class-iff-bounded-local-class
loc-bounded-class
loc-bounded-class_wf
parallel-class-loc-bounded
simple-loc-comb-2-concat-loc-bounded
simple-loc-comb-2-loc-bounded
totally-bounded
totally-bounded-bounded-above
totally-bounded-implies-nonvoid
totally-bounded-inf
totally-bounded-neg
totally-bounded-sup
totally-bounded_wf

BOUNDED2

prev top next

simple-loc-comb-2-concat-loc-bounded2
simple-loc-comb-2-loc-bounded2

BOUNDED3

prev top next

simple-loc-comb-2-concat-loc-bounded3
simple-loc-comb-2-loc-bounded3

BOUNDS

prev top next

b2i_bounds
count_bounds
div_bounds_1
div_bounds_2
div_bounds_3
div_bounds_4
first_index_bounds
mod_bounds
mul_bounds_1a
mul_bounds_1b
neg_mul_arg_bounds
oal_lk_bounds_dom
pos_mul_arg_bounds
rabs-bounds
rem_bounds_1
rem_bounds_2
rem_bounds_3
rem_bounds_4
rem_bounds_absval
rem_bounds_absval_le
rem_bounds_z
small-ctrex1-bounds
strict-upper-bounds
strict-upper-bounds_wf
upper-bounds
upper-bounds-closed
upper-bounds_wf

BOUNDVARS

prev top next

mFOL-boundvars
mFOL-boundvars-of-rename
mFOL-boundvars_wf

BOX

prev top next

A-open-box
A-open-box-equal
A-open-box-image
A-open-box-image_wf
A-open-box_wf
constant-A-open-box
csm-A-open-box
cu-box-in-box
cu-box-in-box_wf
cubical-id-box
cubical-id-box_wf
cubical-interval-non-trivial-box
es-box
es-box_wf
extend-A-open-box
extend-A-open-box_wf
fills-A-open-box
fills-A-open-box_wf
fills-open_box
fills-open_box_wf
length-open_box
length-open_box-ge-3
length-open_box-le-3
length-open_box_image
nerve-box-common-face
nerve-box-common-face_wf
nerve-box-common-face_wf2
nerve-box-face
nerve-box-face_wf
nerve_box_edge
nerve_box_edge'
nerve_box_edge'_wf
nerve_box_edge1
nerve_box_edge1_wf
nerve_box_edge_same
nerve_box_edge_same1
nerve_box_edge_wf
nerve_box_edge_wf2
nerve_box_label
nerve_box_label_same
nerve_box_label_wf
non-trivial-open-box
open_box
open_box-nil
open_box_image
open_box_image_wf
open_box_wf
poset-functor-extends-box-faces
poset-functor-extends-box-faces-1
sigma-box-fst
sigma-box-fst_wf
sigma-box-snd
sigma-box-snd_wf
sq_stable_fills-A-open-box

BPERMR

prev top next

assert_of_bpermr
bpermr
bpermr_wf

BPOS

prev top next

comb_for_oal_bpos_wf
oal_bpos
oal_bpos_trichot
oal_bpos_wf

BRANCH

prev top next

branch
branch-ifthenelse
branch_wf
branch_wf2
callbyvalueall-reduce-repeat-right-branch

BRANCHING

prev top next

surjection-cantor-finite-branching

BREQV

prev top next

binrel_ap_functionality_wrt_breqv
binrel_eqv_functionality_wrt_breqv
rel-immediate_functionality_wrt_breqv
rel_exp_functionality_wrt_breqv
rel_plus_functionality_wrt_breqv
rel_star_functionality_wrt_breqv
s_part_functionality_wrt_breqv
xxanti_sym_functionality_wrt_breqv
xxconnex_functionality_wrt_breqv
xxorder_functionality_wrt_breqv
xxrefl_functionality_wrt_breqv
xxsym_functionality_wrt_breqv
xxtrans_functionality_wrt_breqv

BRLE

prev top next

rel_exp_functionality_wrt_brle
rel_plus_functionality_wrt_brle
rel_star_functionality_wrt_brle

BROADCAST

prev top next

es-weak-broadcast
es-weak-broadcast_wf
new_23_sig_decided'broadcast
new_23_sig_decided'broadcast_wf
new_23_sig_notify'broadcast
new_23_sig_notify'broadcast_wf
new_23_sig_vote'broadcast
new_23_sig_vote'broadcast_wf
nysiad_tooarcast'broadcast
nysiad_tooarcast'broadcast_wf
pv11_p1_decision'broadcast
pv11_p1_decision'broadcast_wf
pv11_p1_p1a'broadcast
pv11_p1_p1a'broadcast_wf
pv11_p1_p2a'broadcast
pv11_p1_p2a'broadcast_wf

BS

prev top next

bs_l_tree
bs_l_tree_member
bs_l_tree_member_wf
bs_l_tree_wf

BSIGN

prev top next

OARcast_order'bsign
OARcast_order'bsign_wf
OARcast_ordered'bsign
OARcast_ordered'bsign_wf

BSUBLIST

prev top next

ball_respects_bsublist
bsublist
bsublist_append_diff
bsublist_functionality_wrt_bsublist
bsublist_functionality_wrt_permr
bsublist_transitivity
bsublist_weakening
bsublist_wf
count_bsublist
count_bsublist_a
mem_bsublist
mem_bsublist_imp

BSUBMSET

prev top next

bsubmset
bsubmset_elim
bsubmset_functionality_wrt_bsubmset
bsubmset_transitivity
bsubmset_weakening
bsubmset_wf
count_bsubmset
mem_bsubmset
mset_for_functionality_wrt_bsubmset
mset_mem_functionality_wrt_bsubmset
rng_mssum_functionality_wrt_bsubmset

BSUPLIST

prev top next

bsuplist
bsuplist_wf

BSUPMSET

prev top next

bsupmset
bsupmset_wf

BTR

prev top next

btr_Leaf
btr_Leaf-val
btr_Leaf-val_wf
btr_Leaf?
btr_Leaf?_wf
btr_Leaf_wf
btr_Node
btr_Node-left
btr_Node-left_wf
btr_Node-right
btr_Node-right_wf
btr_Node?
btr_Node?_wf
btr_Node_wf

BTRUE

prev top next

band-btrue
bdd-all-btrue
bl-all-btrue
bor-btrue
btrue
btrue_neq_bfalse
btrue_wf
eqof_eq_btrue
eqof_equal_btrue
exposed-btrue
inl_eq_btrue
is-list-btrue-if-list
not-bfalse-sqle-btrue
not-btrue-sqeq-bfalse
not-btrue-sqeq-bottom
not-btrue-sqle-bfalse
not-btrue-sqle-bottom

BUFFER

prev top next

es-interface-buffer
es-interface-buffer-as-accum
es-interface-buffer_wf
hdf-buffer
hdf-buffer-transformation2
hdf-buffer-transformation3
hdf-buffer_wf
interface-buffer-val
is-interface-buffer
iterate-hdf-buffer-simple
simple-hdf-buffer
simple-hdf-buffer_wf

BUFFER2

prev top next

hdf-buffer2
hdf-buffer2_wf
iterate-hdf-buffer2-simple
simple-hdf-buffer2
simple-hdf-buffer2_wf

BUFFERS

prev top next

ordered message buffers

BUNION

prev top next

bunion-value-type
bunion-valueall-type
continuous'-monotone-bunion
isaxiom-bool-if-bunion-unit-prod
ispair-bool-if-bunion-unit-prod

BUT

prev top next

all-but-one
but-first-class
but-first-class_wf

BVAL

prev top next

oobboth-bval
oobboth-bval_wf

BVFUN

prev top next

dec_iff_ex_bvfun

BXOR

prev top next

bxor
bxor_wf

BY

prev top next

and_preserved_by
base-class-caused-by
base-class-caused-by_wf
class-caused-by
class-caused-by-some
class-caused-by-some_wf
class-caused-by_wf
compose-rotate-by
count-by-decidable-equiv
count-by-equiv
count-by-orbits
divisibility-by-2-rule
divisibility-by-3-rule
divisibility-by-5-rule
divisibility-by-9-rule
eqmod-by-orbits
equal-by-name-cases
es-closed-open-interval-sorted-by
es-interface-predecessors-sorted-by-le
es-interface-predecessors-sorted-by-locl
es-interval-sorted-by
event-caused-by
event-caused-by_wf
frs-increasing-sorted-by
frs-non-dec-sorted-by
impossible-equation-by-eqmod
insert-by
insert-by-no-repeats
insert-by-sorted-by
insert-by_wf
insert-combine-sorted-by
insert-no-combine-sorted-by
iseg-sorted-by
iterate-rotate-by
iterate-rotate-rotate-by
l-ordered-is-sorted-by
l_before-sorted-by
member-insert-by
member-iseg-sorted-by
or-to-and-by-cases
permutation-sorted-by-unique
preserved_by
preserved_by_monotone
preserved_by_or
preserved_by_star
preserved_by_symmetric
preserved_by_wf
proof-by-cont-implies-LEM
quot_by_prime_ideal
rotate-by
rotate-by-cyclic-map
rotate-by-id
rotate-by-injection
rotate-by-is-id
rotate-by-rotate-by
rotate-by-transitive
rotate-by-trivial
rotate-by-trivial-test
rotate-by-zero
rotate-by_wf
sorted-by
sorted-by-append
sorted-by-append1
sorted-by-cons
sorted-by-eq-rels
sorted-by-exists
sorted-by-exists2
sorted-by-filter
sorted-by-nil
sorted-by-no_repeats
sorted-by-reverse
sorted-by-single
sorted-by-strict-no_repeats
sorted-by-strict-unique
sorted-by-unique
sorted-by_wf
sorted-by_wf_nil
split-by-indices
sq_stable__sorted-by
sublist-sorted-by
subtype_by_equality
subtype_rel-tag-by
tag-by
tag-by-subtype-tag-case
tag-by_wf

BY2

prev top next

and_preserved_by2
preserved_by2
preserved_by2_wf

BYZANTINE

prev top

msg-interface-constraint-byzantine
msg-interface-constraint-byzantine_wf