[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]
W
top next
W
W-bars
W-bars_wf
W-elimination-facts
W-ext
W-induction
W-induction-extract
W-measure-induction
W-null
W-path-lemma
W-path-lemma2
W-rec
W-rec_wf
W-rel
W-rel_wf
W-select
W-select_wf
W-sup
W-sup_wf
W-to-not-not-sig
W-to-not-not-sig2
W-type
W-type-ext
W-type-induction
W-type_wf
W-uniform-measure-induction
W-uwellfounded
W-uwellfounded_witness
W_corec
W_corec_wf
W_iterate_functor
W_iterate_functor_wf
W_sel
W_sel_wf
W_select_nil_lemma
W_subtype
W_wf
assert-co-w-null
co-W
co-W-ext
co-W_wf
co-w
co-w-ext
co-w-null
co-w-null_wf
co-w-select
co-w-select-wfd
co-w-select_wf
co-w_wf
co_w_select_nil_lemma
equal-implies-member-param-W
fix_wf_dataflow_w_state
max_w_ord
max_w_ord_wf
max_w_unit_l_tree
max_w_unit_l_tree_wf
min_w_ord
min_w_ord_wf
min_w_unit_l_tree
min_w_unit_l_tree_wf
not-not-sig-to-W
not-not-sig-to-W-implies-stable
param-W
param-W-ext
param-W-induction
param-W-rel
param-W-rel_wf
param-W_wf
param-co-W
param-co-W-ext
param-co-W_wf
pcw-pp-barred-W
pcw-pp-barred-W-decidable
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
sig-to-W
sq_stable__W-bars
w-bars
w-bars_wf
w-nil
w-nil_wf
WADD
prev top next
Wadd
Wadd-Wzero
Wadd-assoc
Wadd_wf
Wleq-Wadd
Wless-Wadd
Wmul-Wadd
WADD2
prev top next
Wleq-Wadd2
WADD3
prev top next
Wleq-Wadd3
WAIT
prev top next
three-intersecting-wait-set
three-intersecting-wait-set-exists
two-intersecting-wait-set
two-intersecting-wait-set-exists
two-intersecting-wait-set-exists'
WAITING
prev top next
Comm-waiting
Comm-waiting_wf
nysiad_add_waiting
nysiad_add_waiting_wf
WCMP
prev top next
Wcmp
Wcmp_transitivity
Wcmp_wf
WCP
prev top next
unsquashed-WCP
unsquashed-WCP_wf
WEAK
prev top next
TI-weak-TI
bag-member-empty-weak
bag-member-single-weak
bind-class-rel-weak
causal-weak-predecessor
causal-weak-predecessor_wf
disjoint-union-classrel-ite-weak
disjoint-union-comb-classrel-weak
es-weak-broadcast
es-weak-broadcast_wf
es-weak-joint-embedding
es-weak-joint-embedding_wf
fan+weak-continuity-implies-uniform-continuity
hdf-sqequal2-weak
nat-weak-overt
once-classrel-weak
parallel-classrel-weak
rel_plus-weak-TI
ses-thread-weak-order
simple-comb-1-classrel-weak
simple-comb-1-concat-classrel-weak
simple-comb-2-classrel-weak
simple-comb-2-concat-classrel-weak
simple-loc-comb-1-classrel-weak
simple-loc-comb-1-concat-classrel-weak
simple-loc-comb-2-classrel-weak
simple-loc-comb-2-concat-classrel-weak
sqequal-spread-cbva-weak
strong-continuity2-implies-weak-skolem
strong-continuity2-implies-weak-skolem-cantor
strong-continuity2-implies-weak-skolem-cantor-nat
unsquashed-weak-continuity-base-false
unsquashed-weak-continuity-false
weak-TI
weak-TI_wf
weak-antecedent-conditional
weak-antecedent-function
weak-antecedent-function-property
weak-antecedent-function_functionality_wrt_pred_equiv
weak-antecedent-function_wf
weak-antecedent-functions-compose
weak-antecedent-surjection
weak-antecedent-surjection-conditional
weak-antecedent-surjection-conditional2
weak-antecedent-surjection-property
weak-antecedent-surjection_functionality_wrt_pred_equiv
weak-antecedent-surjection_wf
weak-antecedent-surjections-compose
weak-connex
weak-connex_wf
weak-continuity
weak-continuity-implies-strong1
weak-continuity_wf
weak-joint-embedding-preserves-causal-invariant
weak-joint-embedding-preserves-squash-causal-invariant
weak-konig-lemma!
weak-linorder
weak-linorder_wf
weak-overt
weak-overt-implies-overt
weak-overt_wf
weak-update-alist
weak-update-alist_wf
weak-xmiddle
weak-xmiddle_wf
weak_l_before_append_front
WEAK2
prev top next
disjoint-union-classrel-ite-weak2
sqequal-append-cbva-weak2
WEAK3
prev top next
sqequal-append-cbva-weak3
WEAKEN
prev top next
le_to_lt_weaken
WEAKENING
prev top next
Wleq_weakening
agree_on_common_weakening
assoced_weakening
bdd-diff_weakening
bimplies_weakening
binrel_eqv_weakening
binrel_le_weakening
bsublist_weakening
bsubmset_weakening
cut-order_weakening
cut-order_weakening-le
dataflow-equiv_weakening
divides_weakening
eqmod_weakening
equipollent_weakening
equipollent_weakening_ext-eq
es-causl_weakening
es-causl_weakening_p-locl
es-causle_weakening
es-causle_weakening_eq
es-causle_weakening_locl
es-causle_weakening_p-le
es-le_weakening
es-le_weakening_eq
es-p-le_weakening
es-p-le_weakening_eq
eu-seg-congruent_weakening
ext-eq_weakening
f-subset_weakening
fpf-sub_weakening
frs-refines_weakening
fseg_weakening
fun-connected_weakening
fun-connected_weakening_eq
grp_leq_weakening_eq
grp_leq_weakening_lt
iff_weakening_equal
iff_weakening_uiff
implies_weakening_uimplies
iseg_weakening
l_contains_weakening
le_weakening
lg-contains_weakening
massoc_weakening
mdivides_weakening
partition-refines_weakening
path-eq_weakening
permr_massoc_weakening
permr_upto_weakening
permr_weakening
permutation_weakening
predicate_equivalent_weakening
predicate_implies_weakening
predicate_rev_implies_weakening
psub_weakening
rel-connected_weakening
rel_equivalent_weakening
rel_implies_weakening
rel_rev_implies_weakening
rel_star_weakening
req_weakening
rev_implies_weakening_rev_uimplies
rev_subtype_rel_weakening
rfun-eq_weakening
rleq_weakening
rleq_weakening_equal
rleq_weakening_rless
rseteq_weakening
same-thread_weakening
set_leq_weakening_eq
set_leq_weakening_lt
sp-le_weakening
sub-bag_weakening
sub-mset_weakening
sub-system_weakening
sublist_weakening
subtype_rel_weakening
uiff_weakening
WEAKENING2
prev top next
Wleq_weakening2
iseg_weakening2
le_weakening2
WEAKLY
prev top next
no-weakly-safe-extensions
weakly-infinite
weakly-infinite-cases
weakly-infinite_wf
weakly-safe-extension
weakly-safe-seq
weakly-safe-seq_wf
WEIGHTED
prev top next
weighted-sum
weighted-sum-linear
weighted-sum-nil
weighted-sum-split
weighted-sum_wf
weighted-sum_wf2
WELL
prev top next
bag-admissable-well-founded
closure-well-founded-total
int_lower_well_founded
int_mag_well_founded
int_seg_well_founded_down
int_seg_well_founded_up
int_upper_well_founded
lexico_well_fnd
lg-acyclic-well-founded
locally-ranked-is-well-founded
nat_well_founded
pair-lex_well_fnd
posint_well_fnd
power-set-lift-well-founded-implies
product_well_fnd
well-founded-run-lt
well-founded-run-pred
WELLFND
prev top next
es-causl-wellfnd
es-locl-wellfnd
WELLFOUND
prev top next
decidable__wellfound-bounded-exists
WELLFOUNDED
prev top next
bag-ordering-wellfounded
causal-pred-wellfounded
comb_for_wellfounded_wf
descending-chain-barred-implies-wellfounded
no-descending-chain-implies-wellfounded
non-forking-wellfounded-linorder
unique-minimal-wellfounded-implies
wellfounded
wellfounded-acyclic-rel
wellfounded-anti-reflexive
wellfounded-irreflexive
wellfounded-lex
wellfounded-llex
wellfounded-llex-ext
wellfounded-minimal
wellfounded-minimal-field
wellfounded_functionality_wrt_iff
wellfounded_functionality_wrt_implies
wellfounded_wf
WELLTYPED
prev top next
C_STOREp-welltyped
C_STOREp-welltyped_wf
WF0
prev top next
bar_recursion_wf0
dset_of_mon_wf0
es-prior-interface_wf0
oset_of_ocmon_wf0
pcw-pp-barred_wf0
WF1
prev top next
Kan_id_filler_wf1
bag-remove1_wf1
base-process-class-program_wf1
cantor-to-interval_wf1
comb_for_length_wf1
eq_atom_wf1
es-prior-interface_wf1
fix_wf1
oal_grp_wf1
per-union-implies-wf1
sp-lub_wf1
WF2
prev top next
A-bind_wf2
A-eval_wf2
A-loop_wf2
I-path-morph_wf2
alt-swap-spec_wf2
apply_gen_wf2
b_all-wf2
bag-decomp_wf2
bag-filter-wf2
bag-mapfilter-wf2
bag-only_wf2
bag-parts'_wf2
binary_map_case-wf2
binary_map_ind-wf2
bm_E-wf2
bm_T-wf2
branch_wf2
collect_accm-wf2
collect_accum-wf2
collect_filter-wf2
comb_for_length_wf2
comb_for_mk_mset_wf2
comb_for_mon_nat_op_wf2
conditional_wf2
corec-family-wf2
cs-decided_wf2
cycle_wf2
dset_of_mon_wf2
eclass-val_wf2
eclass_wf2
eq_atom_wf2
es-before_wf2
es-first_wf2
es-fix_wf2
es-interface-pred_wf2
es-interface-val_wf2
es-interval_wf2
es-le-before_wf2
es-local-pred_wf2
exp_wf2
face-map_wf2
filter_wf2
fpf-compatible-wf2
fpf-domain_wf2
fpf-restrict_wf2
fpf-single_wf2
free-from-atom_wf2
fset-filter_wf2
fset_of_mset_wf2
funinv_wf2
graph-rcvs_wf2
grp_id_wf2
grp_of_module_wf2
grp_op_wf2
hgrp_of_ocgrp_wf2
int_add_grp_wf2
isect-family-wf2
l_all_wf2
length_wf2
loc-Server_wf2
locknd-spread_wf2
map-wf2
mapfilter-wf2
mk-tagged_wf2
mk_mset_wf2
mon_nat_op_wf2
mset_prod_wf2
msg-body_wf2
msg-type_wf2
mu-ge_wf2
mu-wf2
nat_add_mon_wf2
nerve-box-common-face_wf2
nerve_box_edge_wf2
null_wf2
oal_dom_wf2
oal_grp_wf2
oal_hgp_wf2
oal_merge_wf2
oal_neg_wf2
omral_alg_wf2
omral_dom_wf2
omral_fma_wf2
omral_plus_wf2
omral_scale_wf2
omral_times_wf2
p-graph_wf2
pRun_wf2
pairwise_wf2
per-union-implies-wf2
primrec-wf2
processChoose_wf2
processComm_wf2
qeq_wf2
rec-comb_wf2
rec-dataflow_wf2
record-select_wf2
reg-seq-mul_wf2
rinv_wf2
rng_of_alg_wf2
shorten-tuple_wf2
simple-loc-comb0_wf2
st-ptr-wf2
stream-zip_wf2
tagged-list-messages-wf2
tagged-tag_wf2
tagged-val_wf2
uncurry-gen_wf2
unit_wf2
weighted-sum_wf2
WF3
prev top next
A-bind_wf3
bag-filter-wf3
eclass_wf3
es-before_wf3
exp_wf3
filter_wf3
fpf-single_wf3
funinv_wf3
null_wf3
WF4
prev top next
exp_wf4
filter_wf4
filter_wf4_2
WF5
prev top next
filter_wf5
WFA
prev top next
divide_wfa
remainder_wfa
WFD
prev top next
co-w-select-wfd
empty-wfd-tree
empty-wfd-tree_wf
mk-wfd-tree
mk-wfd-tree_wf
wfd-subtrees
wfd-subtrees_wf
wfd-tree
wfd-tree
wfd-tree-cases
wfd-tree-induction
wfd-tree-induction
wfd-tree-induction-ext
wfd-tree-rec
wfd-tree-rec_wf
wfd-tree2_wf
wfd-tree_wf
wfd_tree_rec_leaf_lemma
wfd_tree_rec_node_lemma
WFDSPREAD
prev top next
WfdSpread
WfdSpread-ext
WfdSpread-induction
WfdSpread_wf
WFO
prev top next
WFO
WFO_wf
WFTO
prev top next
max-WFTO
max-WFTO_wf
WFTRO
prev top next
WFTRO
WFTRO_wf
WHAT
prev top next
What is uniformity conjecture?
WHEN
prev top next
E-prior-class-when
add-div-when-divides
add-div-when-divides2
comb_for_mon_when_wf
comb_for_rng_when_wf
cube-set-restriction-when-id
es-prior-class-when
es-prior-class-when-programmable
es-prior-class-when_wf
fset_for_when_eq
fset_for_when_unique
is-prior-class-when
l-first-when-none
mod_action_when_l
mod_action_when_r
mon_for_when_none
mon_for_when_swap
mon_for_when_unique
mon_when
mon_when_false
mon_when_hom_swap
mon_when_is_hom
mon_when_of_id
mon_when_swap
mon_when_thru_op
mon_when_true
mon_when_wf
mon_when_when
mset_for_when_dom_shift
mset_for_when_none
mset_for_when_unique
new_23_sig_when_new_proposal
new_23_sig_when_new_proposal_wf
new_23_sig_when_new_round
new_23_sig_when_new_round_wf
new_23_sig_when_quorum
new_23_sig_when_quorum_wf
permutation-when-no_repeats
prior-class-when-val
pv11_p1_when_adopted
pv11_p1_when_adopted_wf
pv11_p1_when_preempted
pv11_p1_when_preempted_wf
rng_fset_for_when_eq
rng_lsum_when_swap
rng_mssum_when_swap
rng_times_when_l
rng_times_when_r
rng_when
rng_when_of_zero
rng_when_swap
rng_when_thru_plus
rng_when_wf
rng_when_when
run-event-state-when
run-event-state-when_wf
WHOLE
prev top next
whole_segment
WILSON
prev top next
wilson-theorem
WITH
prev top next
bag-partitions-with-one-given
complete_nat_ind_with_y
delivered-with-headers
delivered-with-headers-no_repeats
delivered-with-headers_wf
es-with-internal
filter-vote-with-ballot-lemma
fun_with_inv_is_bij
fun_with_inv_is_bij2
hdf-with-state-pair-left-axiom
last_with_property
messages-delivered-with-omissions
messages-delivered-with-omissions-sub
messages-delivered-with-omissions-sub_wf
messages-delivered-with-omissions_wf
msgs-interface-delivered-with-omissions
msgs-interface-delivered-with-omissions_wf
msgs-interface-with-omissions-sub
msgs-interface-with-omissions-sub_wf
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
new_23_sig_vote_with_ballot
new_23_sig_vote_with_ballot-assert-classrel
new_23_sig_vote_with_ballot-assert-type
new_23_sig_vote_with_ballot-forward
new_23_sig_vote_with_ballot-header
new_23_sig_vote_with_ballot-if-classrel
new_23_sig_vote_with_ballot_and_id
new_23_sig_vote_with_ballot_and_id-assert-classrel
new_23_sig_vote_with_ballot_and_id-assert-type
new_23_sig_vote_with_ballot_and_id-forward
new_23_sig_vote_with_ballot_and_id-if-classrel
new_23_sig_vote_with_ballot_and_id-if-snd
new_23_sig_vote_with_ballot_and_id-implies
new_23_sig_vote_with_ballot_and_id-snd
new_23_sig_vote_with_ballot_and_id_wf
new_23_sig_vote_with_ballot_first
new_23_sig_vote_with_ballot_first-assert
new_23_sig_vote_with_ballot_first-assert-forward
new_23_sig_vote_with_ballot_first-assert-forward2
new_23_sig_vote_with_ballot_first-assert-type
new_23_sig_vote_with_ballot_first-forward
new_23_sig_vote_with_ballot_first-not
new_23_sig_vote_with_ballot_first-not2
new_23_sig_vote_with_ballot_first_alt
new_23_sig_vote_with_ballot_first_alt_wf
new_23_sig_vote_with_ballot_first_wf
new_23_sig_vote_with_ballot_wf
remove-repeats-mapfilter-with-fun
std-ma-with-omissions
std-ma-with-omissions_wf
WITHDRAWN
prev top next
cs-withdrawn
cs-withdrawn_wf
decidable__equal_cs-withdrawn
WITHOUT
prev top next
Rules of MLTT without type formers
WITNESS
prev top next
W-uwellfounded_witness
assert_witness
cut-order_witness
deq-runEvents-witness
deq-runEvents-witness_wf
deq-witness
deq-witness_wf
disjoint_sublists_witness
fpf-sub_witness
fset-member_witness
i-member-witness
i-witness
i-witness-property
i-witness_wf
member-filter-witness
member-filter-witness_wf
member-mapfilter-witness
member-mapfilter-witness_wf
no_repeats_witness
page55_witness
req_witness
rless-witness
rless-witness-property
rless-witness_wf
rv-le_witness
ses-honest_witness
ses-key-rel_witness
strong-subtype_witness
WKL
prev top next
fan-iff-wkl!
wkl!
wkl!-iff-nwkl!
wkl!-iff-twkl!-bool
wkl!_wf
WLEQ
prev top next
Wleq-Wadd
Wleq-Wadd2
Wleq-Wadd3
Wleq-Wmul
Wleq_weakening
Wleq_weakening2
WLESS
prev top next
Wless-Wadd
Wless_antireflexive
WMUL
prev top next
Wleq-Wmul
Wmul
Wmul-Wadd
Wmul-Wzero
Wmul-add-properties
Wmul-assoc
Wmul_wf
WO
prev top next
max-WO
max-WO_wf
WQO
prev top next
Wqo
Wqo_wf
wqo-less
wqo-less_wf
WRT
prev top next
Q-R-pre-preserving_functionality_wrt_implies
add_functionality_wrt_eq
add_functionality_wrt_eqmod
add_functionality_wrt_le
add_functionality_wrt_lt
add_mono_wrt_eq
add_mono_wrt_eq_rw
add_mono_wrt_le
add_mono_wrt_le_rw
add_mono_wrt_lt
add_mono_wrt_lt_rw
all_functionality_wrt_iff
all_functionality_wrt_implies
all_functionality_wrt_uiff
all_functionality_wrt_uimplies
alle-between1_functionality_wrt_iff
alle-between2_functionality_wrt_iff
and_functionality_wrt_iff
and_functionality_wrt_implies
and_functionality_wrt_rev_uimplies
and_functionality_wrt_uiff
and_functionality_wrt_uiff2
and_functionality_wrt_uiff3
and_functionality_wrt_uimplies
antecedent-function_functionality_wrt_iff
antecedent-surjection_functionality_wrt_iff
anti_sym_functionality_wrt_iff
append_cancel_wrt_permutation
append_functionality_wrt_permr
append_functionality_wrt_permutation
assert_functionality_wrt_bimplies
assert_functionality_wrt_uiff
assoced_functionality_wrt_assoced
bag-summation_functionality_wrt_le
bag-summation_functionality_wrt_le_1
ball_functionality_wrt_bimplies
ball_functionality_wrt_permr
binrel_ap_functionality_wrt_breqv
binrel_eqv_functionality_wrt_breqv
bsublist_functionality_wrt_bsublist
bsublist_functionality_wrt_permr
bsubmset_functionality_wrt_bsubmset
cand_functionality_wrt_iff
compact_functionality_wrt_equipollent
compact_functionality_wrt_surject
connex_functionality_wrt_iff
connex_functionality_wrt_implies
cons_cancel_wrt_permutation
cons_functionality_wrt_lequiv
cons_functionality_wrt_permr
cons_functionality_wrt_permr_massoc
cons_functionality_wrt_permr_upto
cons_functionality_wrt_permutation
continuous_functionality_wrt_rfun-eq
continuous_functionality_wrt_subinterval
coprime_functionality_wrt_eqmod
coprime_functionality_wrt_eqmod2
derivative_functionality_wrt_subinterval
diff_functionality_wrt_permr
divides_functionality_wrt_assoced
eqmod_functionality_wrt_eqmod
equal_functionality_wrt_subtype_rel
equal_functionality_wrt_subtype_rel2
equipollent_functionality_wrt_equipollent
equipollent_functionality_wrt_equipollent2
equipollent_functionality_wrt_equipollent3
equipollent_functionality_wrt_ext-eq
equipollent_functionality_wrt_ext-eq-left
equipollent_functionality_wrt_ext-eq-right
equiv_rel_functionality_wrt_iff
es-first-since_functionality_wrt_iff
es-pplus_functionality_wrt_iff
es-pplus_functionality_wrt_implies
es-pplus_functionality_wrt_rev_implies
es-pstar-q_functionality_wrt_iff
es-pstar-q_functionality_wrt_implies
es-pstar-q_functionality_wrt_rev_implies
exists_functionality_wrt_iff
exists_functionality_wrt_implies
existse-between1_functionality_wrt_iff
existse-between2_functionality_wrt_iff
existse-between3_functionality_wrt_iff
exp_functionality_wrt_assoced
exp_functionality_wrt_eqmod
filter_functionality_wrt_permutation
finite_functionality_wrt_equipollent
fpf-cap-subtype_functionality_wrt_sub
fpf-cap-subtype_functionality_wrt_sub2
fpf-cap_functionality_wrt_sub
function_functionality_wrt_equipollent
function_functionality_wrt_equipollent_left
function_functionality_wrt_equipollent_right
gcd_functionality_wrt_eqmod
gcd_p_functionality_wrt_assoced
grp_op_ap2_functionality_wrt_massoc
grp_op_ap2_functionality_wrt_mdivides
grp_op_functionality_wrt_massoc
guard_functionality_wrt_iff
iff_functionality_wrt_iff
ifthenelse_functionality_wrt_iff
ifthenelse_functionality_wrt_iff2
ifthenelse_functionality_wrt_iff3
ifthenelse_functionality_wrt_implies
ifthenelse_functionality_wrt_implies2
ifthenelse_functionality_wrt_implies3
ifthenelse_functionality_wrt_rev_implies
ifthenelse_functionality_wrt_rev_implies2
ifthenelse_functionality_wrt_rev_implies3
ifthenelse_functionality_wrt_uimplies
ifthenelse_functionality_wrt_uimplies2
ifthenelse_functionality_wrt_uimplies3
implies_functionality_wrt_iff
implies_functionality_wrt_implies
isect2_functionality_wrt_subtype_rel
isect_functionality_wrt_equipollent_dependent
l_all_functionality_wrt_permutation
l_member_functionality_wrt_permutation
l_sum_functionality_wrt_permutation
length_functionality_wrt_permr
linorder_functionality_wrt_ext-eq
linorder_functionality_wrt_iff
list-to-set_functionality_wrt_permutation
lmax_functionality_wrt_permr
lmin_functionality_wrt_permr
map_functionality_wrt_sq
massoc_functionality_wrt_massoc
mem_functionality_wrt_permr
minus_functionality_wrt_eq
minus_functionality_wrt_eqmod
minus_functionality_wrt_le
minus_functionality_wrt_lt
minus_mono_wrt_eq
minus_mono_wrt_le
minus_mono_wrt_lt
mon_for_functionality_wrt_permr
mon_reduce_functionality_wrt_permr
mset_for_functionality_wrt_bsubmset
mset_mem_functionality_wrt_bsubmset
mul_functionality_wrt_eq
multiply_functionality_wrt_assoced
multiply_functionality_wrt_eqmod
multiply_functionality_wrt_le
no_repeats_functionality_wrt_permutation
not_functionality_wrt_iff
not_functionality_wrt_implies
not_functionality_wrt_uiff
not_functionality_wrt_uimplies
null_functionality_wrt_permr
or_functionality_wrt_iff
or_functionality_wrt_implies
or_functionality_wrt_uiff
or_functionality_wrt_uiff2
or_functionality_wrt_uiff3
order_functionality_wrt_iff
permr_functionality_wrt_permr
permr_upto_functionality_wrt_permr_upto
permutation_functionality_wrt_permutation
power-sum_functionality_wrt_eqmod
power-sum_functionality_wrt_le
product_functionality_wrt_equipollent
product_functionality_wrt_equipollent_dependent
product_functionality_wrt_equipollent_left
product_functionality_wrt_equipollent_right
rabs_functionality_wrt_bdd-diff
radd-list_functionality_wrt_permutation
radd-list_functionality_wrt_rleq
radd_functionality_wrt_rleq
radd_functionality_wrt_rless1
radd_functionality_wrt_rless2
refl_functionality_wrt_iff
reg-seq-add_functionality_wrt_bdd-diff
reg-seq-list-add_functionality_wrt_bdd-diff
reg-seq-list-add_functionality_wrt_permutation
reg-seq-mul_functionality_wrt_bdd-diff
rel-immediate_functionality_wrt_breqv
rel-immediate_functionality_wrt_iff
rel_exp_functionality_wrt_breqv
rel_exp_functionality_wrt_brle
rel_exp_functionality_wrt_iff
rel_exp_functionality_wrt_rel_implies
rel_plus_functionality_wrt_breqv
rel_plus_functionality_wrt_brle
rel_plus_functionality_wrt_iff
rel_plus_functionality_wrt_rel_implies
rel_star_functionality_wrt_breqv
rel_star_functionality_wrt_brle
rel_star_functionality_wrt_rel_implies
remove-repeats_functionality_wrt_permutation
remove1_functionality_wrt_permr
rleq_functionality_wrt_implies
rless_functionality_wrt_implies
rmax_functionality_wrt_bdd-diff
rmax_functionality_wrt_rleq
rmaximum_functionality_wrt_rleq
rmin_functionality_wrt_bdd-diff
rminus_functionality_wrt_bdd-diff
rminus_functionality_wrt_rleq
rmul_functionality_wrt_rleq
rmul_functionality_wrt_rleq2
rmul_functionality_wrt_rless
rmul_functionality_wrt_rless2
rng_mssum_functionality_wrt_bsubmset
rng_mssum_functionality_wrt_equal
rsub_functionality_wrt_rleq
rsub_functionality_wrt_rless
rsum_functionality_wrt_rleq
rsum_functionality_wrt_rleq2
rsum_functionality_wrt_rleq3
s_part_functionality_wrt_breqv
set_blt_functionality_wrt_set_lt_r
sq_or_functionality_wrt_iff
squash_functionality_wrt_iff
squash_functionality_wrt_implies
squash_functionality_wrt_uiff
sub_functionality_wrt_le
subtract_functionality_wrt_eqmod
subtype_rel_functionality_wrt_iff
subtype_rel_functionality_wrt_implies
sum_functionality_wrt_sqequal
sym_functionality_wrt_iff
trans_functionality_wrt_iff
trans_rel_func_wrt_sym_self
uall_functionality_wrt_iff
uanti_sym_functionality_wrt_iff
uconnex_functionality_wrt_iff
uconnex_functionality_wrt_implies
uequiv_rel_functionality_wrt_iff
uiff_functionality_wrt_uiff
uiff_functionality_wrt_uiff2
uimplies_functionality_wrt_uiff
uimplies_functionality_wrt_uiff2
uimplies_functionality_wrt_uiff3
uimplies_functionality_wrt_uimplies
ulinorder_functionality_wrt_iff
union_functionality_wrt_equipollent
union_functionality_wrt_iff
union_functionality_wrt_uiff
union_functionality_wrt_uiff2
union_functionality_wrt_uiff3
uorder_functionality_wrt_iff
urefl_functionality_wrt_iff
usym_functionality_wrt_iff
utrans_functionality_wrt_iff
weak-antecedent-function_functionality_wrt_pred_equiv
weak-antecedent-surjection_functionality_wrt_pred_equiv
wellfounded_functionality_wrt_iff
wellfounded_functionality_wrt_implies
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
WS
prev top next
ws-constant
ws-linear
ws-lower-bound
ws-monotone
ws_nil_lemma
ws_single_lemma
WSELECT
prev top next
Wselect
Wselect_wf
WSUCC
prev top next
Wsucc
Wsucc_wf
WSUP
prev top next
Wsup
Wsup_wf
WT
prev top next
bm_wt
bm_wt_wf
WZERO
prev top
Wadd-Wzero
Wmul-Wzero
Wzero
Wzero-leq
Wzero-unique
Wzero_wf