[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]

D

top next

d-conv
d-conv_wf
lookup_omral_scale_d
ses-D
ses-D-implies
ses-D-private
ses-D-private_wf
ses-D-public
ses-D-public_wf
ses-D_wf

D2L

prev top next

bm_listItems_d2l
bm_listItems_d2l_wf
bm_listItemsi_d2l
bm_listItemsi_d2l_wf
bm_listKeys_d2l
bm_listKeys_d2l_wf

DA

prev top next

da-agrees
da-agrees-on
da-agrees-on_wf
da-agrees_wf
es-decl-set-da
es-decl-set-da_wf
fpf-join-dom-da
normal-da
normal-da-join
normal-da-single
normal-da_wf

DAG

prev top next

is-dag
is-dag-add
is-dag-append
is-dag-map
is-dag-remove
is-dag_wf
lg-add_wf_dag
lg-all-wf_dag
lg-append_wf_dag
lg-is-source-wf_dag
lg-label-wf_dag
lg-map-wf_dag
lg-nil_wf_dag
lg-remove_wf_dag
lg-size-wf_dag
make-lg_wf_dag

DATA

prev top next

constant-data-stream
data
data-stream
data-stream-append
data-stream-cons
data-stream_wf
data_stream_nil_lemma
data_wf
event-data
event-data_wf
firstn-data-stream
last-data-stream
length-data-stream
null-data-stream
select-data-stream
st-data
st-data_wf

DATAFLOW

prev top next

constant-dataflow
constant-dataflow_wf
dataflow
dataflow-ap
dataflow-ap_wf
dataflow-equiv
dataflow-equiv_inversion
dataflow-equiv_transitivity
dataflow-equiv_weakening
dataflow-equiv_wf
dataflow-ext-eq
dataflow-out
dataflow-out_wf
dataflow-to-Process
dataflow-to-Process_functionality
dataflow-to-Process_wf
dataflow-valueall-type
dataflow_subtype
dataflow_wf
datastream-dataflow-to-Process
fix_wf_dataflow
fix_wf_dataflow_w_state
iterate-constant-dataflow
iterate-dataflow
iterate-dataflow-append
iterate-dataflow_wf
iterate-rec-dataflow
iterate-stateless-dataflow
rec-dataflow
rec-dataflow-state
rec-dataflow-state_wf
rec-dataflow_wf
rec-dataflow_wf2
rec_dataflow_ap_lemma
stateless-dataflow
stateless-dataflow_wf
stateless_dataflow_ap_lemma

DATASTREAM

prev top next

datastream-dataflow-to-Process

DBAR

prev top next

dbar
dbar_wf

DCC

prev top next

DCC
DCC-order-type
DCC-order-type-less
DCC-order-type-less-ext
DCC-order-type_wf
DCC_wf

DCDR

prev top next

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
dcdr-to-bool
dcdr-to-bool-equivalence
dcdr-to-bool_wf
test-rewrite-dcdr

DD

prev top next

dd
dd_wf

DDR

prev top next

ddr
ddr_wf

DEBUG1

prev top next

debug1

DEBUG2

prev top next

debug2

DEC2BOOL

prev top next

assert_dec2bool
dec2bool
dec2bool_decidable
dec2bool_wf

DECIDABILITY

prev top next

iff_preserves_decidability

DECIDABLE

prev top next

count-by-decidable-equiv
dec2bool_decidable
decidable
decidable-cantor-to-int
decidable-cantor-to-int-ext
decidable-equal-deq
decidable-exists-finite
decidable-exists-finite-type
decidable-exists-int_seg-subtype
decidable-exists-iseg
decidable-filter
decidable-finite-cantor
decidable-finite-cantor-ext
decidable-finite-cantor-to-int
decidable-implies-es-interface
decidable-last-rel
decidable-non-minimal
decidable-non-minimal_wf
decidable-predicate-and
decidable-predicate-not
decidable-predicate-or
decidable-ses-fresh-sequence
decidable-subtype
decidable__AFbar
decidable__all-list
decidable__all_fset
decidable__all_int_seg
decidable__all_length
decidable__all_length_bool
decidable__alle-between1
decidable__alle-between2
decidable__alle-le
decidable__alle-lt
decidable__and
decidable__and2
decidable__archive-condition
decidable__assert
decidable__assoced
decidable__atom_equal
decidable__atom_equal_1
decidable__atom_equal_2
decidable__bag-member
decidable__bag-member2
decidable__bool
decidable__cWObar
decidable__cand
decidable__classrel
decidable__cmp-le
decidable__connection
decidable__cs-archive-blocked
decidable__cs-archived
decidable__cs-committed-change
decidable__cs-inning-committable
decidable__cs-inning-committable-another
decidable__cs-inning-committable-some
decidable__cs-inning-committed
decidable__cs-inning-committed-some
decidable__cs-inning-two-committable
decidable__cs-not-completed
decidable__cs-passed
decidable__cs-precondition
decidable__cut-order
decidable__divides
decidable__divides_ext
decidable__dset_eq
decidable__dstype_equal
decidable__eqmod
decidable__equal-coordinate_name
decidable__equal-coordinate_name
decidable__equal-es-E
decidable__equal-es-base-E
decidable__equal-poset-cat-ob
decidable__equal_Id
decidable__equal_IdLnk
decidable__equal_Kind
decidable__equal_MaName
decidable__equal_bag
decidable__equal_bool
decidable__equal_compact_domain
decidable__equal_consensus-rcv
decidable__equal_cs-initial
decidable__equal_cs-withdrawn
decidable__equal_equipollent
decidable__equal_es-E-interface
decidable__equal_fset
decidable__equal_function
decidable__equal_int
decidable__equal_int_seg
decidable__equal_list
decidable__equal_name
decidable__equal_nat
decidable__equal_nat_plus
decidable__equal_product
decidable__equal_runEvents
decidable__equal_set
decidable__equal_union
decidable__equal_unit
decidable__es-E-equal
decidable__es-causl-same-loc
decidable__es-fset-loc
decidable__es-le
decidable__es-locl
decidable__es-p-le-pred
decidable__es-p-local-pred
decidable__ex_unit
decidable__exists-classrel-between1
decidable__exists-classrel-between1-sv
decidable__exists-classrel-between3
decidable__exists-classrel-between3-sv
decidable__exists-es-p-le-pred
decidable__exists-es-p-local-pred
decidable__exists-iterated-classrel
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__exists-prior-iterated-classrel
decidable__exists-single-valued-bag
decidable__exists-single-valued-classrel
decidable__exists_bag-member
decidable__exists_classrel
decidable__exists_int_seg
decidable__exists_iseg
decidable__exists_iterated_classrel
decidable__exists_length
decidable__exists_length_bool
decidable__existse-before
decidable__existse-between1
decidable__existse-between2
decidable__existse-between3
decidable__existse-le
decidable__f-subset
decidable__false
decidable__fset-closed
decidable__fset-member
decidable__fun-connected
decidable__grp_lt
decidable__i-closed
decidable__i-finite
decidable__iff
decidable__implies
decidable__implies_better
decidable__inject-finite-type
decidable__int_equal
decidable__iseg
decidable__l_all
decidable__l_all-better-extract
decidable__l_all-proof
decidable__l_contains
decidable__l_disjoint
decidable__l_disjoint_manames
decidable__l_exists
decidable__l_exists-proof
decidable__l_exists_better-extract
decidable__l_member
decidable__le
decidable__lg-edge
decidable__llex
decidable__lt
decidable__mon_eq
decidable__nameset
decidable__nameset
decidable__no_repeats
decidable__not
decidable__oal_lt
decidable__or
decidable__p-outcome
decidable__pa-is-new-and
decidable__pa-is-sign-implies
decidable__path-goes-thru
decidable__pcw-pp-barred
decidable__prime
decidable__proper_divisor
decidable__quotient_equal
decidable__reducible
decidable__rel_exp
decidable__rel_exp_finite
decidable__rel_plus
decidable__rless-int-fractions
decidable__rng_eq
decidable__run-lt
decidable__run-pred
decidable__same-thread
decidable__ses-action
decidable__ses-legal-sequence
decidable__set_leq
decidable__set_lt
decidable__squash
decidable__sub-bag
decidable__sublist-rec
decidable__tree-big
decidable__true
decidable__uimplies
decidable__upwd-closure
decidable__wellfound-bounded-exists
decidable_decision
decidable_functionality
decidable_wf
equipollent-decidable-equal
equipollent-nat-decidable-subset
es-interface-from-decidable
es-interface-implies-decidable
extract-decider-of-decidable-prop
finite-decidable-set
l_member_decidable
last-decidable
not-has-value-decidable-quot
not_has-value_decidable_on_base
pcw-pp-barred-W-decidable
simple-decidable-finite-cantor
simple-decidable-finite-cantor-ext
sq_stable_and_decidable
sq_stable_from_decidable
stable__from_decidable

DECIDABLE2

prev top next

bag-member-decidable2

DECIDE1

prev top next

lift-simple-decide-decide1

DECIDE2

prev top next

decide-decide2
decide2
decide2_wf
lift-simple-decide-decide2

DECIDE3

prev top next

decide-decide3

DECIDED

prev top next

assert-cs-is-decided
cs-decided
cs-decided_wf
cs-decided_wf2
cs-is-decided
cs-is-decided_wf
cs-ref-map3-decided
new_23_sig-decided
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_decided'broadcast
new_23_sig_decided'broadcast_wf
new_23_sig_decided_property
new_23_sig_decided_with_id
new_23_sig_decided_with_id-assert-classrel
new_23_sig_decided_with_id-assert-type
new_23_sig_decided_with_id_wf
three-cs-decided
three-cs-decided_wf

DECIDER

prev top next

bool-decider
bool-decider_wf
extract-decider-of-decidable-prop
finite-cantor-decider
finite-cantor-decider_wf
l-all-decider
l-all-decider_wf
l-exists-decider
l-exists-decider_wf
no-halt-decider
p-mu-decider
simple-finite-cantor-decider
simple-finite-cantor-decider_wf
sq-decider
sq-decider-atom-deq
sq-decider-list-deq
sq-decider-name-deq
sq-decider_wf

DECIMAL

prev top next

decimal-digits
decimal-digits_wf

DECISION

prev top next

bool_decision
decidable_decision
decision
decision_wf
new_23_sig_decision
new_23_sig_decision_wf
pv11_p1-decision
pv11_p1_decision
pv11_p1_decision'base
pv11_p1_decision'base_wf
pv11_p1_decision'broadcast
pv11_p1_decision'broadcast_wf
pv11_p1_decision'send
pv11_p1_decision'send_wf
pv11_p1_decision_from_maj_acceptors
pv11_p1_decision_from_p2a
pv11_p1_decision_from_p2a_acc
pv11_p1_decision_wf

DECL

prev top next

atom-free-decl
decl-set-read-allowed
es-decl-set
es-decl-set-avoids
es-decl-set-avoids-tag
es-decl-set-avoids-tag_wf
es-decl-set-avoids_wf
es-decl-set-da
es-decl-set-da_wf
es-decl-set-declares-tag
es-decl-set-declares-tag_wf
es-decl-set-domain
es-decl-set-domain_wf
es-decl-set-ds
es-decl-set-ds_wf
es-decl-set-join
es-decl-set-join-domain
es-decl-set-join_wf
es-decl-set-single
es-decl-set-single_wf
es-decl-set_wf
es-decl-sets-compatible
es-decl-sets-compatible_wf
es-decl-sets-sub
es-decl-sets-sub_wf
fpf-all-join-decl
fpf-all-single-decl
fpf-join-dom-decl
lnk-decl
lnk-decl-ap
lnk-decl-cap
lnk-decl-cap2
lnk-decl-compatible-single
lnk-decl-compatible-single2
lnk-decl-dom
lnk-decl-dom-implies
lnk-decl-dom-join
lnk-decl-dom-not
lnk-decl-dom-single
lnk-decl-dom2
lnk-decl_wf
lnk-decl_wf-hasloc
non-void-decl
non-void-decl-join
non-void-decl-single
non-void-decl_wf
normal-decl-set
normal-decl-set_wf

DECLARES

prev top next

add-graph-decls-declares-tag
es-decl-set-declares-tag
es-decl-set-declares-tag_wf

DECLS

prev top next

R-decls-compat
add-graph-decls
add-graph-decls-declares-tag
add-graph-decls_wf
ci-decls
cp-decls
cp-decls_wf
lnk-decls-compatible
public-decls

DECODE

prev top next

sbcode-decode

DECOMP

prev top next

bag-decomp
bag-decomp_wf
bag-decomp_wf2
bag-member-decomp
callbyvalueall_seq-decomp-last
combination-decomp
concat-decomp
cycle-decomp
decomp
decomp-map-if-has-value
decomp_wf
es-before-decomp
es-closed-interval-vals-decomp
es-closed-open-interval-decomp
es-closed-open-interval-decomp-last
es-closed-open-interval-decomp-mem
es-closed-open-interval-decomp-member
firstn_decomp
firstn_nth_tl_decomp
from-upto-decomp-last
is-list-if-has-value-decomp
is-list-if-has-value-rec-decomp
isect2_decomp
l-ordered-decomp
l_member_decomp
length2-decomp
list-decomp-nat
list-decomp-nat-iseg
list-decomp-no_repeats
list_2_decomp
list_decomp
list_decomp_last
list_decomp_member
list_decomp_rev
list_decomp_rev_wf
list_decomp_reverse
listp_decomp
listp_decomp_last
loc-on-path-decomp
longest-prefix-decomp
n-tuple-decomp
name-morph-decomp
nth_tl_decomp
nth_tl_decomp_eq
orbit-decomp
special-mod4-decomp
special-mod4-decomp-unique
special-mod4-decomp_wf
stream-decomp
swap_adjacent_decomp
tuple-decomp
upto_decomp

DECOMP1

prev top next

upto_decomp1

DECOMP2

prev top next

firstn_decomp2
l-ordered-decomp2
orbit-decomp2
upto_decomp2

DECOMPOSE

prev top next

fpf-decompose
pi-comm-decompose
pi-new-decompose
pi-option-decompose
pi-par-decompose
pi-rep-decompose
rank-comm-decompose
rank-new-decompose
rank-option-decompose
rank-par-decompose
rank-rep-decompose

DECR

prev top next

int-decr-map-add
int-decr-map-add-prop
int-decr-map-add_wf
int-decr-map-empty
int-decr-map-empty-prop
int-decr-map-empty_wf
int-decr-map-find
int-decr-map-find-not-in
int-decr-map-find-prop
int-decr-map-find-prop2
int-decr-map-find-wf
int-decr-map-find_wf
int-decr-map-fun
int-decr-map-inDom
int-decr-map-inDom-cons
int-decr-map-inDom-prop
int-decr-map-inDom-prop1
int-decr-map-inDom-prop2
int-decr-map-inDom_wf
int-decr-map-isEmpty
int-decr-map-isEmpty-assert
int-decr-map-isEmpty-prop
int-decr-map-isEmpty_wf
int-decr-map-remove
int-decr-map-remove-prop
int-decr-map-remove_wf
int-decr-map-type
int-decr-map-type-member-sq-stable
int-decr-map-type_wf
int-decr-map-update
int-decr-map-update-prop
int-decr-map-update_wf
mk-map-int-decr
mk-map-int-decr_wf

DECREASES

prev top next

absval_div_decreases
length-filter-decreases

DECREASING

prev top next

decreasing-on-interval
decreasing-on-interval_wf
derivative-implies-decreasing
fact-non-decreasing
isqrt-non-decreasing
strictly-decreasing-on-interval
strictly-decreasing-on-interval_wf

DECRYPT

prev top next

ses-decrypt
ses-decrypt_wf
ses-legal-thread-decrypt
st-decrypt
st-decrypt_wf

DECRYPTED

prev top next

ses-decrypted
ses-decrypted_wf

DECRYPTION

prev top next

ses-decryption-key
ses-decryption-key_wf

DECTT

prev top next

assert-dectt
dectt
dectt_wf

DEF

prev top next

add def
any def
apply def
atom def
atom_eq def
atomeqn def
atomn def
axiom def
bar def
base def
computed_display def
decide def
def-cont-induction-lemma
def-cont-induction-lemma-ext
divide def
equal def
es-class-def
es-class-def_wf
es-interface-numbered-def
es-interface-triple-def
eu-between-eq-def
eu-colinear-def
experimental-allFunctionality def
experimental-impliesFunctionality def
experimental-orFunctionality def
experimental-uallFunctionality def
fix def
function def
image-type_def
ind def
inl def
inr def
int def
int_eq def
isatom def
isaxiom def
isect def
isinl def
isinr def
isint def
islambda def
ispair def
l_member-alt-def
lambda def
less def
minus def
natural_number def
object def
pair def
per-eq-def
per-eq-def_wf
product def
rec def
rec_ind def
remainder def
set def
spread def
sqequal def
sqequal_n def
sqle def
sqle_n def
sqntype def
token def
token1 def
token2 def
tunion_def
union def
universe def
void def

DEFAULT

prev top next

case_default
default-partition-choice
default-partition-choice_wf
has-value-l-last-default-list
l-last-default
l-last-default_wf
switch_default

DEFINES

prev top next

det_ideal_defines_eqv
ideal_defines_eqv

DEFINING

prev top next

defining the Kan structure

DEFINITION

prev top next

C_DVALUEp-definition
C_LVALUE-definition
C_TYPE-definition
MMTree-definition
MultiTree-definition
RankEx1-definition
RankEx2-definition
RankEx4-definition
binary-tree-definition
binary_map-definition
formula-definition
l_tree-definition
mFOL-definition
mFOLRule-definition
pi_prefix-definition
pi_term-definition
tree-definition

DEFINITIONS

prev top next

summary of definitions

DEFN2

prev top next

mklist_defn2

DEFOP

prev top next

RankEx2-defop
RankEx2-defop-extract

DEGENERACY

prev top next

degeneracy-map
degeneracy-map_wf
name-morph-degeneracy-map

DEGREE

prev top next

fps-degree-bound
fps-degree-bound_wf
fps-support-degree-bound

DELAY

prev top next

bar-delay
bar-delay-equal
bar-delay_wf
msg-interface-delay
msg-interface-delay_wf

DELETE

prev top next

bm_delete'
bm_delete'_wf

DELIVER

prev top next

OARcast_deliver'send
OARcast_deliver'send_wf
deliver ordered messages
deliver-msg
deliver-msg-to-comp
deliver-msg-to-comp_wf
deliver-msg_functionality
deliver-msg_wf
lg-label-deliver-msg
lg-size-deliver-msg
lg-size-deliver-msg-general
nysiad_deliver_to_replica
nysiad_deliver_to_replica_wf
oar-deliver
oar-deliver_wf
oarcast-deliver-output
oarcast-deliver-output_wf
update-oarcast-deliver
update-oarcast-deliver_wf

DELIVERED

prev top next

CLK_messages-delivered
CLK_messages-delivered_wf
OARcast_messages-delivered
OARcast_messages-delivered_wf
delivered-with-headers
delivered-with-headers-no_repeats
delivered-with-headers_wf
eo-msgs-interface-delivered
eo-msgs-interface-delivered_wf
info-delivered
info-delivered_wf
messages-delivered
messages-delivered-with-omissions
messages-delivered-with-omissions-sub
messages-delivered-with-omissions-sub_wf
messages-delivered-with-omissions_wf
messages-delivered_wf
msgs-interface-delivered
msgs-interface-delivered-with-omissions
msgs-interface-delivered-with-omissions_wf
msgs-interface-delivered_wf
new_23_sig_messages-delivered
new_23_sig_messages-delivered_wf
nysiad_messages-delivered
nysiad_messages-delivered_wf
pv11_p1_messages-delivered
pv11_p1_messages-delivered-w-omissions-accpts
pv11_p1_messages-delivered-w-omissions-accpts_wf
pv11_p1_messages-delivered-w-omissions-ldrs
pv11_p1_messages-delivered-w-omissions-ldrs_wf
pv11_p1_messages-delivered_wf

DELIVERER

prev top next

OARcast_Deliverer
OARcast_Deliverer-program
OARcast_Deliverer-program_wf
OARcast_Deliverer_wf
OARcast_deliverer_for_sender_output
OARcast_deliverer_for_sender_output_wf
OARcast_deliverer_for_sender_seq_output
OARcast_deliverer_for_sender_seq_output_wf
OARcast_deliverer_for_sender_seq_update
OARcast_deliverer_for_sender_seq_update_wf
OARcast_deliverer_for_sender_update
OARcast_deliverer_for_sender_update_wf

DELIVERERFORSENDER

prev top next

OARcast_DelivererForSender
OARcast_DelivererForSender-program
OARcast_DelivererForSender-program_wf
OARcast_DelivererForSender_wf

DELIVERERFORSENDERSEQ

prev top next

OARcast_DelivererForSenderSeq
OARcast_DelivererForSenderSeq-program
OARcast_DelivererForSenderSeq-program_wf
OARcast_DelivererForSenderSeq_wf

DELIVERERFORSENDERSEQSTATE

prev top next

OARcast_DelivererForSenderSeqState
OARcast_DelivererForSenderSeqState-program
OARcast_DelivererForSenderSeqState-program_wf
OARcast_DelivererForSenderSeqState_wf

DELIVERERFORSENDERSTATE

prev top next

OARcast_DelivererForSenderState
OARcast_DelivererForSenderState-program
OARcast_DelivererForSenderState-program_wf
OARcast_DelivererForSenderState_wf

DELIVERERSTATE

prev top next

OARcast_DelivererState
OARcast_DelivererState-program
OARcast_DelivererState-program_wf
OARcast_DelivererState_wf

DELIVERHDR

prev top next

OARcast-deliverhdr

DELMIN

prev top next

bm_delmin
bm_delmin_wf

DENOM

prev top next

qrep-denom

DENSE

prev top next

rationals-dense
rationals-dense-ext

DEP

prev top next

dep-eclass_subtype_rel
dep-eclass_subtype_rel2
dep-isect
dep-isect-subtype
dep-isect-subtype2
dep-isect-value-type
dep-isect-wf
dep-isect_wf
dep_ax_choice
member-dep-isect
quotient-dep-function-subtype
strong-continuous-dep-isect
strong-subtype-dep-product
subtype_rel_dep_function
subtype_rel_dep_function_iff
subtype_rel_dep_product_iff
void-dep-product

DEPENDENT

prev top next

isect_functionality_wrt_equipollent_dependent
list_ind_reverse_wf_dependent
product_functionality_wrt_equipollent_dependent
t-sqle-apply-dependent

DEPFUNCTION

prev top next

continuous-monotone-depfunction

DEPPRODUCT

prev top next

continuous-monotone-depproduct
strong-continuous-depproduct

DEQ

prev top next

Kind-deq
Kind-deq_wf
assert-bag-deq-member
assert-deq
assert-deq-all-disjoint
assert-deq-disjoint
assert-deq-fset-member
assert-deq-member
assert-deq-sub-bag
assert-int-deq
assert-name-deq
assert-product-deq
assert-union-deq
atom-deq
atom-deq-aux
atom-deq_wf
atom2-deq
atom2-deq-aux
atom2-deq_wf
bag-deq
bag-deq-member
bag-deq-member-bag-diff
bag-deq-member_wf
bag-deq_wf
bag-member-map3-deq
bool-deq
bool-deq-aux
bool-deq_wf
cname_deq
cname_deq
cname_deq_wf
cname_deq_wf
decidable-equal-deq
deq
deq-all-disjoint
deq-all-disjoint_wf
deq-disjoint
deq-disjoint_wf
deq-exists
deq-fset-member
deq-fset-member_wf
deq-mFO
deq-mFO_wf
deq-member
deq-member-append
deq-member-firstn
deq-member-length-filter
deq-member-length-filter2
deq-member-union
deq-member_wf
deq-runEvents-witness
deq-runEvents-witness_wf
deq-sub-bag
deq-sub-bag_wf
deq-witness
deq-witness_wf
deq_member_cons_lemma
deq_member_nil_lemma
deq_property
deq_property2
deq_subtype
deq_wf
es-LnkTag-deq
es-LnkTag-deq_wf
id-deq
id-deq_wf
idlnk-deq
idlnk-deq_wf
int-deq
int-deq-aux
int-deq_wf
list-deq
list-deq_wf
locknd-deq
locknd-deq_wf
maname-deq
maname-deq_wf
mk_deq
mk_deq-subtype
mk_deq_wf
name-deq
name-deq_wf
nat-deq
nat-deq-aux
nat-deq_wf
nysiad_Amessage-deq
nysiad_Amessage-deq_wf
product-deq
product-deq_wf
safe-assert-deq
sq-decider-atom-deq
sq-decider-list-deq
sq-decider-name-deq
strong-subtype-deq
strong-subtype-deq-subtype
subtype-deq
subtype_rel-deq
union-deq
union-deq_wf
unit-deq
unit-deq_wf

DERIV

prev top next

IVT-deriv-seq-test
finite-deriv-seq
finite-deriv-seq_wf
infinite-deriv-seq
infinite-deriv-seq_wf
locally-non-constant-deriv-seq-test
locally-non-zero-finite-deriv-seq
non-zero-deriv-non-constant
poly-deriv
poly-deriv-linear
poly-deriv_wf
poly-nth-deriv
poly-nth-deriv-req
poly-nth-deriv_wf
polynomial-deriv-seq
rpoly-deriv
rpoly-deriv_wf
rpoly-nth-deriv
rpoly-nth-deriv-linear
rpoly-nth-deriv_functionality
rpoly-nth-deriv_wf

DERIVATIVE

prev top next

derivative
derivative-Taylor-approx
derivative-add
derivative-const
derivative-const-mul
derivative-const-mul2
derivative-continuous
derivative-id
derivative-implies-decreasing
derivative-implies-increasing
derivative-minus
derivative-mul
derivative-rdiv
derivative-rdiv-const
derivative-rinv
derivative-rnexp
derivative-rpolynomial
derivative-rsum
derivative-sub
derivative_functionality
derivative_functionality_wrt_subinterval
derivative_unique
derivative_wf

DERIVED

prev top next

derived-seq
derived-seq_wf
eclass-compose1-derived
es-interface-image-derived

DES

prev top next

Des
Des_wf

DESC

prev top next

pv11_p1_pmax_desc
pv11_p1_pmax_desc_iff
pv11_p1_pmax_desc_implies
pv11_p1_upd_desc
pv11_p1_upd_desc_iff

DESCENDING

prev top next

descending
descending-append
descending-chain-barred-implies-wellfounded
descending_wf
no-descending-chain
no-descending-chain-implies-wellfounded
no-descending-chain_wf

DEST

prev top next

mFO-dest-atomic
mFO-dest-atomic_wf
mFO-dest-connective
mFO-dest-connective_wf
mFO-dest-quantifier
mFO-dest-quantifier_wf

DESTINATION

prev top next

msg-interface-destination
msg-interface-destination_wf

DESTRUCTOR

prev top next

destructor
destructor-const
destructor-product
destructor-sum
destructor_wf

DET

prev top next

det_ideal_ap_elim
det_ideal_defines_eqv
exists_det_fun
exists_det_fun_a
int_pi_det_fun
int_pi_det_fun_wf

DETACH

prev top next

detach
detach_fun
detach_fun_properties
detach_fun_wf
detach_msubset
detach_wf
ideal-detach-equiv
int_pi_detach

DF

prev top next

const_df_ap_lemma
iter_df_cons_lemma
iter_df_nil_lemma

DFAN

prev top next

dfan
dfan-iff-twkl!
dfan-implies-twkl!
dfan_wf
fan-iff-dfan-bool
twkl!-implies-dfan

DIAMOND

prev top next

es-diamond
es-diamond_wf

DICKSON

prev top next

Dickson's lemma
bag-dickson-lemma

DIFF

prev top next

absval-diff-product-bound
absval-diff-symmetry
accelerate-bdd-diff
bag-deq-member-bag-diff
bag-diff
bag-diff-equal-inl
bag-diff-property
bag-diff_wf
bag-member-bag-diff
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
bsublist_append_diff
count_diff
diff
diff_cons_lemma
diff_functionality_wrt_permr
diff_nil_lemma
diff_wf
filter-list-diff
grp_inv_diff
i-member-diff-bound
length-eq-lists-diff-elts
length-list-diff
list-diff
list-diff-cons
list-diff-cons-single
list-diff-diff
list-diff-disjoint
list-diff-property
list-diff-subset
list-diff_functionality
list-diff_wf
massoc_imp_unit_diff
mem_diff
member-list-diff
member-nameset-diff
member-nameset-diff
mset_count_diff
mset_diff
mset_diff_wf
mset_diff_wf_f
mset_mem_diff
nameset_subtype_cons_diff
nameset_subtype_cons_diff
no_repeats_list-diff
non_munit_diff_imp_mpdivides
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
rless-iff-large-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

DIFF2

prev top next

list-diff2
list-diff2-sym

DIFFERENCE

prev top next

absval-imax-difference
absval-imin-difference
double_sum_difference
exp-difference-inequality
exp_difference_bound
exp_difference_factor
infinitesmal-difference
rabs-difference-bound-iff
rabs-difference-bound-rleq
rabs-difference-lower-bound
rabs-difference-rmax
rabs-difference-symmetry
rsum-difference
sum_difference

DIFFERENCE2

prev top next

rsum-difference2

DIFFERENTIABLE

prev top next

differentiable-continuous

DIGITS

prev top next

decimal-digits
decimal-digits_wf

DIMENSION

prev top next

face-dimension
face-dimension_wf
get_face-dimension

DIRECTION

prev top next

face-direction
face-direction_wf
get_face-direction

DISCONTINUOUS

prev top next

discontinuous
discontinuous_wf

DISCRETE

prev top next

Kan-discrete
Kan-discrete_wf
discrete-cube
discrete-cube_wf
discrete-cubical-term
discrete-cubical-term_wf
discrete-cubical-type
discrete-cubical-type_wf
discrete_struct
discrete_struct_wf

DISJ

prev top next

disj_un_tr_ap_inl_lemma
disj_un_tr_ap_inr_lemma

DISJOINT2

prev top next

b-union-equality-disjoint2

DISJU

prev top next

eclass-disju
eclass-disju-bind-left
eclass-disju-classrel
eclass-disju-program
eclass-disju-program_wf
eclass-disju_wf
hdf-union-eq-disju

DISLIST

prev top next

dislist
dislist_properties
dislist_wf

DISPLAY

prev top next

computed_display def

DIST

prev top next

dist_1op_2op_lr
dist_1op_2op_lr_wf
dist_hom_over_mon_for
dist_hom_over_mset_for
poset-cat-dist
poset-cat-dist-add
poset-cat-dist-flip
poset-cat-dist-non-zero
poset-cat-dist-zero
poset-cat-dist_wf
ratio-dist
ratio-dist_wf
sq_stable__dist_1op_2op_lr

DISTINCT

prev top next

distinct
distinct-representatives
distinct_cons_lemma
distinct_iff_counts_le_one
distinct_nil_lemma
distinct_wf
equipollent-distinct-representatives
member-values-for-distinct
st-atoms-distinct
st-atoms-distinct_wf
st-lookup-distinct
values-for-distinct
values-for-distinct-nil
values-for-distinct-property
values-for-distinct_wf

DISTINCT2

prev top next

member-values-for-distinct2

DISTRIB

prev top next

left_mul_add_distrib
left_mul_subtract_distrib
mul_add_distrib
rmul-distrib
rmul-rsub-distrib
sp-join-meet-distrib
sp-meet-join-distrib

DISTRIB1

prev top next

rmul-distrib1

DISTRIB2

prev top next

rmul-distrib2

DISTRIBUTED

prev top next

rv-identically-distributed
rv-identically-distributed_wf

DISTRIBUTES

prev top next

mul-distributes
mul-distributes-right

DISTRIBUTIVE

prev top next

band_bor_distributive
bor_band_distributive

DIV

prev top next

absval_div_decreases
absval_div_nat
add-div-when-divides
add-div-when-divides2
add-plus-1-div-2-implies-lt
alg_div
alg_div_wf
div-cancel
div-cancel2
div-cancel3
div-mul-cancel
div-one
div-positive-1
div-search-lemma
div-search-lemma-ext
div-self
div_2_to_1
div_3_to_1
div_4_to_1
div_base_case
div_bounds_1
div_bounds_2
div_bounds_3
div_bounds_4
div_div
div_div_commutes
div_div_nat
div_elim
div_floor
div_floor_mod_sum
div_floor_wf
div_fun_sat_div_nrel
div_induction
div_induction-ext
div_lbound_1
div_mono1
div_mul_add_cancel
div_mul_cancel
div_nat_induction
div_nat_induction-ext
div_nrel
div_nrel_wf
div_preserves_le
div_rec_case
div_rem_sum
div_rem_sum2
div_unique
div_unique2
div_unique3
divides_iff_div_exact
eqmod-eqmod-div
fps-div
fps-div-coeff
fps-div-coeff-property
fps-div-coeff_wf
fps-div-one
fps-div-property
fps-div-unique
fps-div_wf
fps-elim-div
int-div-exception
mproper_div_cond
posint_div_dec
rem_to_div
rmul-ident-div
rmul-zero-div
rng_div
rng_div_wf
zero-div-rem

DIVERGE

prev top next

bar-val-diverge
bottom_diverge
diverge
diverge_wf
fix_strict_diverge

DIVERGES

prev top next

bar-converges-not-diverges
bar-diverges
bar-diverges-iff
bar-diverges_functionality
bar-diverges_wf
diverges
diverges_wf
fix-diverges
harmonic-series-diverges
not-diverges-converges
series-diverges
series-diverges-trivially
series-diverges_wf

DIVIDE

prev top next

divide def
divide-and-conquer
divide-and-conquer-ext
divide_wf
divide_wfa
strictness-divide-left
strictness-divide-right

DIVIDES

prev top next

add-div-when-divides
comb_for_divides_wf
coprime_divides_prod
decidable__divides
decidable__divides_ext
divides
divides-add
divides-combinations
divides-fact
divides-iff-factors
divides-iff-gcd
divides-iff-gcd-assoced
divides-mul
divides-prime
divides_add
divides_anti_sym
divides_anti_sym_n
divides_functionality_wrt_assoced
divides_iff_div_exact
divides_iff_rem_zero
divides_instance
divides_invar_1
divides_invar_2
divides_mul
divides_nchar
divides_of_absvals
divides_preorder
divides_product
divides_reflexivity
divides_subtract
divides_transitivity
divides_weakening
divides_wf
eqmod-divides-implies
exp-divides
exp-divides-exp
exp-divides-exp2
orbit-size-divides-order
positive-prime-divides-prime
positive-prime-divides-product
prime-divides-prime

DIVIDES2

prev top next

add-div-when-divides2

DIVISIBILITY

prev top next

divisibility-by-2-rule
divisibility-by-3-rule
divisibility-by-5-rule
divisibility-by-9-rule

DIVISION

prev top next

trial-division
trial-division_wf

DIVISOR

prev top next

decidable__proper_divisor
divisor-in-range
divisor-test
divisor-test_wf
divisor_bound
divisor_of_minus
divisor_of_mul
divisor_of_sum
gcd_is_divisor_1
gcd_is_divisor_2
proper-divisor
proper-divisor-aux
proper-divisor-aux_wf
proper-divisor_wf
self_divisor_mul

DIVISORS

prev top next

coprime_divisors_prod
divisors-sum
divisors-sum_wf
divisors_bound
gen-divisors-sum
gen-divisors-sum-int-ring
gen-divisors-sum_wf

DIVS

prev top next

any_divs_zero
mprime_divs_list_el
one_divs_any
only_pm_one_divs_one
prime_divs_prod
ring_divs
ring_divs_wf
zero_divs_only_zero

DMODULE

prev top next

dmodule
dmodule_wf

DMON

prev top next

abdmonoid_dmon
dmon
dmon_properties
dmon_subtype_mon
dmon_wf
mk_dmon

DNEG

prev top next

dneg_elim
dneg_elim_a

DNS

prev top next

DNS-iff-not-not-GMP

DNSF

prev top next

DNSF

DO

prev top next

do-apply
do-apply-compose
do-apply-compose'
do-apply-mu'
do-apply-p-co-filter
do-apply-p-co-restrict
do-apply-p-filter
do-apply-p-first
do-apply-p-first-disjoint
do-apply-p-lift
do-apply-p-restrict
do-apply_wf
do-chosen-command
do-chosen-command_wf
do-elimination-step
ex-do-Elim
ex-do-Intro
inl-do-apply
same-thread-do-apply

DOM

prev top next

any_field_is_integ_dom
compose-fpf-dom
eo-reset-dom
eo-reset-dom-reset-dom
eo-reset-dom_wf
eo-reset-dom_wf_extended
es-dom
es-dom_wf
es-dt-dom
fpf-const-dom
fpf-dom
fpf-dom-compose
fpf-dom-list
fpf-dom-list_wf
fpf-dom-type
fpf-dom-type2
fpf-dom_functionality
fpf-dom_functionality2
fpf-dom_wf
fpf-join-dom
fpf-join-dom-da
fpf-join-dom-decl
fpf-join-dom-sq
fpf-join-list-dom
fpf-normalize-dom
fpf-rename-dom
fpf-restrict-dom
fpf-single-dom
fpf-single-dom-sq
fpf-union-join-dom
fpf_dom_compose_lemma
global-eo-dom
integ_dom
integ_dom_p
integ_dom_p_wf
integ_dom_wf
l_disjoint-fpf-dom
l_disjoint-fpf-join-dom
lnk-decl-dom
lnk-decl-dom-implies
lnk-decl-dom-join
lnk-decl-dom-not
lnk-decl-dom-single
member-fpf-dom
mk_fpf_dom_lemma
mset_for_dom_shift
mset_for_when_dom_shift
oal_dom
oal_dom_inj
oal_dom_merge
oal_dom_neg
oal_dom_wf
oal_dom_wf2
oal_lk_bounds_dom
oal_lk_in_dom
oal_merge_dom_pred
omral_dom
omral_dom_action
omral_dom_inj
omral_dom_one
omral_dom_scale
omral_dom_wf
omral_dom_wf2
omral_plus_dom
omral_scale_dom_bound
omral_scale_dom_pred
omral_times_dom
ranked-eo-dom
rng_mssum_dom_shift
sq_stable__integ_dom_p

DOM2

prev top next

fpf-join-dom2
fpf-join-list-dom2
fpf-rename-dom2
lnk-decl-dom2

DOMAIN

prev top next

alist-domain-first
consensus-ts4-estimate-domain
cp-domain
cp-domain_wf
decidable__equal_compact_domain
domain_fpf_restrict_lemma
equipollent-void-domain
es-decl-set-domain
es-decl-set-domain_wf
es-decl-set-join-domain
es-interface-conditional-domain
es-interface-conditional-domain-iff
es-interface-conditional-domain-member
fpf-domain
fpf-domain-join
fpf-domain-union-join
fpf-domain_wf
fpf-domain_wf2
fpf-join-domain
fpf-join-list-domain
fpf-null-domain
fpf-restrict-domain
infinite-domain-example
infinite-domain-example-ext
member-fpf-domain
member-fpf-domain-variant
name-morph-domain
name-morph-domain-inject
name-morph-domain_subtype
name-morph-domain_wf
name-morph-inv-eq-domain
name-morph_subtype_domain
p-conditional-domain
pv11_p1_in_domain
pv11_p1_in_domain_wf
singleton-type-void-domain
test-infinite-domain-example

DOMAIN2

prev top next

fpf-join-list-domain2

DONE

prev top next

switch_done

DONTCARE

prev top next

dontcare
dontcare_wf

DOT

prev top next

dot-product
dot-product-comm
dot-product-linearity1
dot-product-linearity2
dot-product-nonneg
dot-product_functionality
dot-product_wf

DOUBLE

prev top next

bag-double-summation
bag-double-summation2
bm_double_L
bm_double_L_wf
bm_double_R
bm_double_R_wf
classical-double-negation
double-negation-hyp-elim
double-negation-iff-xmiddle
double-negation-shift
double-negation-shift_wf
double_isect_subtype_rel
double_sum
double_sum_difference
double_sum_functionality
double_sum_wf
finite-double-negation-shift
finite-double-negation-shift-extract
minimal-double-negation-hyp-elim
no-uniform-double-negation-elim
pair_support_double_sum
subtype_rel_double_isect

DOWN

prev top next

down-closed
down-closed_wf
int_seg_well_founded_down

DOWNEQ

prev top next

bm_exists_downeq
bm_exists_downeq_wf

DRNG

prev top next

drng
drng_all_properties
drng_properties
drng_subtype_rng
drng_wf

DROP

prev top next

bag-count-drop
bag-count-drop-trivial
bag-drop
bag-drop-commutes
bag-drop-head
bag-drop-no-repeats
bag-drop-property
bag-drop-property2
bag-drop_wf

DS

prev top next

ds-agrees
ds-agrees-on
ds-agrees-on_wf
ds-agrees_wf
ds_property
eq_ds
eq_ds_wf
es-decl-set-ds
es-decl-set-ds_wf
implies-normal-ds
normal-ds
normal-ds-join
normal-ds-single
normal-ds_wf
standard-ds
standard-ds_wf

DSDEQ

prev top next

dsdeq
dsdeq_wf

DSEQ

prev top next

dseq
dseq_wf

DSET

prev top next

assert_of_dset_eq
atom_dset
atom_dset_wf
decidable__dset_eq
dset
dset_eq_refl
dset_list
dset_list_wf
dset_of_mon
dset_of_mon_wf
dset_of_mon_wf0
dset_of_mon_wf2
dset_properties
dset_set
dset_set_wf
dset_wf
loset_subtype_dset
mk_dset
mk_dset_wf
qoset_subtype_dset

DST

prev top next

dst_vlnk_lemma

DSTYPE

prev top next

decidable__dstype_equal
dstype
dstype_wf

DT

prev top next

es-dt
es-dt-ap
es-dt-cap
es-dt-dom
es-dt_wf
es-tags-dt
es-tags-dt-cap
es-tags-dt_wf

DUMMY

prev top next

pv11_p1_dummy_ballot
pv11_p1_dummy_ballot_wf
pv11_p1_leq_bnum_dummy
pv11_p1_leq_bnum_dummy_eq
pv11_p1_max_bnum_dummy

DUP

prev top next

bar-induction (dup of thm in list_1)

DVALP

prev top next

C_Array-elem_vs_DVALp
C_Array_vs_DVALp
C_Struct_vs_DVALp
C_TYPE_vs_DVALp
C_TYPE_vs_DVALp_wf

DVALUEP

prev top next

C_DVALUEp
C_DVALUEp-definition
C_DVALUEp-ext
C_DVALUEp-induction
C_DVALUEp_ind
C_DVALUEp_ind_wf
C_DVALUEp_ind_wf_simple
C_DVALUEp_size
C_DVALUEp_size_wf
C_DVALUEp_wf

DVALUEPCO

prev top next

C_DVALUEpco
C_DVALUEpco-ext
C_DVALUEpco_size
C_DVALUEpco_size_wf
C_DVALUEpco_wf

DVP

prev top

DVp_Array
DVp_Array-arr
DVp_Array-arr_wf
DVp_Array-lower
DVp_Array-lower_wf
DVp_Array-upper
DVp_Array-upper_wf
DVp_Array?
DVp_Array?_wf
DVp_Array_wf
DVp_Int
DVp_Int-int
DVp_Int-int_wf
DVp_Int?
DVp_Int?_wf
DVp_Int_wf
DVp_Null
DVp_Null-x
DVp_Null-x_wf
DVp_Null?
DVp_Null?_wf
DVp_Null_wf
DVp_Pointer
DVp_Pointer-ptr
DVp_Pointer-ptr_wf
DVp_Pointer?
DVp_Pointer?_wf
DVp_Pointer_wf
DVp_Struct
DVp_Struct-lbls
DVp_Struct-lbls_wf
DVp_Struct-struct
DVp_Struct-struct_wf
DVp_Struct?
DVp_Struct?_wf
DVp_Struct_wf