[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]
UALL
top next
sq_stable__uall
uall
uall-union
uall-unit
uall_functionality_wrt_iff
uall_instance_test
uall_subtype
uall_wf
UALLFUNCTIONALITY
prev top next
experimental-uallFunctionality def
UALLTEST1
prev top next
UallTest1
UAND
prev top next
uand
uand-subtype1
uand-subtype2
uand_wf
UANTI
prev top next
sq_stable__uanti_sym
uanti_sym
uanti_sym_functionality_wrt_iff
uanti_sym_shift
uanti_sym_wf
UB
prev top next
bag-max-ub
fixpoint_ub
imax-bag-ub
imax-list-ub
imax_strict_ub
imax_ub
imin_ub
rabs-ub
rmax_strict_ub
rmax_ub
rmaximum_ub
rmin_strict_ub
rmin_ub
UBAR
prev top next
ubar
ubar_wf
UBOUND
prev top next
absval_ubound
UCONNEX
prev top next
sq_stable__uconnex
uconnex
uconnex_functionality_wrt_iff
uconnex_functionality_wrt_implies
uconnex_iff_trichot
uconnex_wf
UCONT
prev top next
fps-add-ucont
fps-compose-ucont
fps-id-ucont
fps-linear-ucont-equal
fps-mul-ucont
fps-set-to-one-ucont
fps-slice-ucont
fps-ucont
fps-ucont-composition
fps-ucont_wf
UEQUIV
prev top next
squash_thru_uequiv_rel
uequiv_rel
uequiv_rel_functionality_wrt_iff
uequiv_rel_iff
uequiv_rel_self_functionality
uequiv_rel_subtyping
uequiv_rel_wf
UEXT
prev top next
uext
uext-ap-name
uext_wf
UFM
prev top next
is_ufm
is_ufm_wf
posint_is_ufm
ufm_char
UIFF
prev top next
all_functionality_wrt_uiff
and_functionality_wrt_uiff
assert_functionality_wrt_uiff
iff_weakening_uiff
no_repeats_map_uiff
no_repeats_nil_uiff
no_repeats_singleton_uiff
not_functionality_wrt_uiff
or_functionality_wrt_uiff
sq_stable__uiff
squash_functionality_wrt_uiff
uiff
uiff_functionality_wrt_uiff
uiff_functionality_wrt_uiff2
uiff_inversion
uiff_transitivity
uiff_transitivity2
uiff_transitivity3
uiff_weakening
uiff_wf
uimplies_functionality_wrt_uiff
union_functionality_wrt_uiff
UIFF2
prev top next
and_functionality_wrt_uiff2
or_functionality_wrt_uiff2
uiff_functionality_wrt_uiff2
uimplies_functionality_wrt_uiff2
union_functionality_wrt_uiff2
UIFF3
prev top next
and_functionality_wrt_uiff3
or_functionality_wrt_uiff3
uimplies_functionality_wrt_uiff3
union_functionality_wrt_uiff3
UIMPLIES
prev top next
all_functionality_wrt_uimplies
and_functionality_wrt_rev_uimplies
and_functionality_wrt_uimplies
decidable__uimplies
ifthenelse_functionality_wrt_uimplies
implies_weakening_uimplies
not_functionality_wrt_uimplies
rev_implies_weakening_rev_uimplies
rev_uimplies
rev_uimplies_wf
sq_stable__uimplies
sq_stable_iff_uimplies
uimplies
uimplies-iff-squash-implies
uimplies-wf
uimplies_antisymmetry
uimplies_functionality_wrt_uiff
uimplies_functionality_wrt_uiff2
uimplies_functionality_wrt_uiff3
uimplies_functionality_wrt_uimplies
uimplies_subtype
uimplies_transitivity
UIMPLIES2
prev top next
ifthenelse_functionality_wrt_uimplies2
UIMPLIES3
prev top next
ifthenelse_functionality_wrt_uimplies3
ULINORDER
prev top next
ulinorder
ulinorder_functionality_wrt_iff
ulinorder_le_neg
ulinorder_lt_neg
ulinorder_wf
ULIST
prev top next
ulist
ulist-ext
ulist_wf
UMAP
prev top next
fabgrp_umap
fabgrp_umap_wf
fma_umap
fma_umap_wf
free_abmon_umap
free_abmon_umap_properties
free_abmon_umap_properties_1
free_abmon_umap_wf
gcopower_umap
gcopower_umap_wf
mcopower_umap
mcopower_umap_comm_tri
mcopower_umap_comm_tri_a
mcopower_umap_is_hom
mcopower_umap_unique
mcopower_umap_wf
oal_umap
oal_umap_char
oal_umap_char_a
oal_umap_wf
omral_alg_umap
omral_alg_umap_is_hom
omral_alg_umap_tri_comm
omral_alg_umap_unique
omral_alg_umap_wf
UN
prev top next
disj_un_tr_ap_inl_lemma
disj_un_tr_ap_inr_lemma
un-ctrex1
un-ctrex1_wf
un-zip
un-zip_wf
unzip-un-zip
UNANIMOUS
prev top next
poss-maj-unanimous
UNBOUNDED
prev top next
fan-implies-barred-not-unbounded
rv-unbounded
rv-unbounded_wf
unbounded-list-predicate
unbounded-list-predicate_wf
UNCHANGED
prev top next
cs-ref-map-unchanged
UNCOUNTABLE
prev top next
reals-uncountable
reals-uncountable-simple
UNCURRY
prev top next
apply_uncurry
uncurry
uncurry-gen
uncurry-gen_wf
uncurry-gen_wf2
uncurry-rev
uncurry-rev_wf
uncurry_wf
UNCURRY1
prev top next
uncurry1_lemma
UNCURRY2
prev top next
uncurry2_lemma
UNDECIDED
prev top next
cs-undecided
cs-undecided_wf
UNEQUAL
prev top next
Sierpinski-unequal
Sierpinski-unequal-1
consensus-state3-unequal
es-prior-fixedpoints-unequal
mk-tagged_wf_unequal
UNFOLD
prev top next
absval_unfold
colist-unfold
colist-unfold_wf
imax_unfold
imin_unfold
list_ind_reverse_unfold
next-unfold
UNFOLD1
prev top next
list_ind_reverse_unfold1
UNFOLD2
prev top next
absval_unfold2
UNI
prev top next
exists_uni
exists_uni_upto
exists_uni_upto_char
exists_uni_upto_wf
exists_uni_wf
sq_stable__uni_sat
uni_sat
uni_sat_imp_in_uni_set
uni_sat_upto
uni_sat_upto_wf
uni_sat_wf
UNICITY
prev top next
eu-construction-unicity
UNIFORM
prev top next
AF-uniform-induction
AF-uniform-induction2
AF-uniform-induction3
AF-uniform-induction4
AF-uniform-induction4-ext
Kan_id_filler_uniform
Kan_sigma_filler_uniform
Kanfiller-uniform
TC-min-uniform
W-uniform-measure-induction
cantor-to-int-uniform-continuity
cu-cube-filler-uniform
fan+weak-continuity-implies-uniform-continuity
groupoid-nerve-filler-uniform
int_le_to_int_upper_uniform
int_lt_to_int_upper_uniform
int_upper_ind_uniform
mFO-uniform-evidence
mFO-uniform-evidence_wf
mesh-uniform-partition
no-uniform-Peirce's-law
no-uniform-double-negation-elim
no-uniform-xmiddle
not_over_exists_uniform
rel_plus-uniform-TI
sq_stable_uniform-Kan-A-filler
strong-continuity2-implies-uniform-continuity
strong-continuity2-implies-uniform-continuity-ext
strong-continuity2-implies-uniform-continuity-int
strong-continuity2-implies-uniform-continuity-nat
strong-continuity2-implies-uniform-continuity-nat-ext
strong-continuity2-implies-uniform-continuity2
strong-continuity2-implies-uniform-continuity2-int
transitive-closure-minimal-uniform
uniform-Kan-A-filler
uniform-Kan-A-filler_wf
uniform-Kan-filler
uniform-Kan-filler_wf
uniform-TI
uniform-TI-less
uniform-TI_wf
uniform-comp-nat-induction
uniform-continuity-pi
uniform-continuity-pi-dec
uniform-continuity-pi-pi
uniform-continuity-pi-pi-prop
uniform-continuity-pi-pi-prop2
uniform-continuity-pi-pi_wf
uniform-continuity-pi-search
uniform-continuity-pi-search-prop1
uniform-continuity-pi-search-prop2
uniform-continuity-pi-search_wf
uniform-continuity-pi2
uniform-continuity-pi2-dec
uniform-continuity-pi2-dec-ext
uniform-continuity-pi2_wf
uniform-continuity-pi_wf
uniform-evd-proof
uniform-evd-proof-check
uniform-evd-proof-checks
uniform-evd-to-proof
uniform-fps
uniform-fps_wf
uniform-partition
uniform-partition-increasing
uniform-partition-point
uniform-partition-refines
uniform-partition_wf
uniform_nat_measure_ind
UNIFORMITY
prev top next
What is uniformity conjecture?
UNION
prev top next
RankEx2_Union
RankEx2_Union-union
RankEx2_Union-union_wf
RankEx2_Union?
RankEx2_Union?_wf
RankEx2_Union_wf
all-union
assert-union-deq
b-union
b-union-base-equality
b-union-equality-disjoint
b-union-equality-disjoint2
b-union-void
b-union_wf
bag-append-union
bag-filter-union
bag-map-union
bag-member-union
bag-null-bag-union
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_union_cons_lemma
bag_union_empty_lemma
classfun-res-disjoint-union-comb-as-parallel-eclass1
classfun-res-disjoint-union-comb-left
classfun-res-disjoint-union-comb-right
compact-union
continuous-monotone-union
countable-p-union
countable-p-union_wf
decidable__equal_union
deq-member-union
disjoint-union-class
disjoint-union-class-single-val
disjoint-union-class_wf
disjoint-union-classrel
disjoint-union-classrel-ite
disjoint-union-classrel-ite-weak
disjoint-union-classrel-ite-weak2
disjoint-union-classrel-ite2
disjoint-union-comb
disjoint-union-comb-classrel
disjoint-union-comb-classrel-weak
disjoint-union-comb-disjoint-classrel
disjoint-union-comb-es-sv
disjoint-union-comb-single-val
disjoint-union-comb_wf
disjoint-union-tr
disjoint-union-tr_wf
disjoint-union-type
disjoint-union-type_wf
eclass-union
eclass-union-classrel
eclass-union_wf
empty-bag-union
empty-bag-union
equipollent-nat-union-nsub
equipollent-union-com
equipollent-union-function
equipollent-union-product
equipollent-union-sum
es-cut-union
es-interface-union
es-interface-union-left
es-interface-union-right
es-interface-union_wf
es-is-interface-union
exists-union
f-subset-union
f-union
f-union-subset
f-union_wf
finite-type-union
fpf-contains-union-join-left2
fpf-contains-union-join-right2
fpf-domain-union-join
fpf-union
fpf-union-compatible
fpf-union-compatible-property
fpf-union-compatible-self
fpf-union-compatible-subtype
fpf-union-compatible_symmetry
fpf-union-compatible_wf
fpf-union-contains
fpf-union-contains2
fpf-union-join
fpf-union-join-ap
fpf-union-join-dom
fpf-union-join-member
fpf-union-join_wf
fpf-union_wf
fset-list-union
fset-list-union_wf
fset-size-union
fset-union
fset-union-associative
fset-union-closed
fset-union-commutes
fset-union-idempotent
fset-union_wf
fset_mem_union
hdf-union
hdf-union-ap
hdf-union-eq-disju
hdf-union-halt
hdf-union_wf
in-open-union
int-product-union-atom-disjoint
int-union-disjoint
int_mod_2_union_int_mod_3
int_mod_union_int_mod
interface-union-val
invert-union
invert-union_wf
isect2-b-union-subtype
l-union
l-union'
l-union-list
l-union-list_wf
l-union-nil
l-union-same
l-union-subset
l-union_wf
member-countable-p-union
member-disjoint-union-comb
member-disjoint-union-comb-bool
member-f-union
member-f-union-aux
member-fset-list-union
member-fset-union
member-l-union-list
member-p-union
member-per-union-left
member-per-union-right
member-union
member-union-list2
mset_count_bound_for_union
mset_count_union
mset_mem_mon_for_union
mset_union
mset_union_assoc
mset_union_bor_mon_hom
mset_union_comm
mset_union_ident_l
mset_union_ident_r
mset_union_mon
mset_union_mon_wf
mset_union_wf
mset_union_wf_f
no_repeats-union-list
no_repeats_union
non-empty-bag-mapfilter-union-of-list
non-empty-bag-union-of-list
norm-union
norm-union_wf
nullset-union
open-union
open-union_wf
p-union
p-union_wf
per-union
per-union-elim
per-union-elim1
per-union-implies-wf1
per-union-implies-wf2
per-union_wf
product-union-atom-disjoint
set-sig-union
set-sig-union_wf
squash-exists-is-union-squash
squash-union-is-union-squash
strong-continuous-b-union
strong-continuous-union
strong-subtype-b-union
strong-subtype-b-union-better
strong-subtype-union
strong-subtype-union-base
sub-bag-union-of-list
subtype_rel_b-union
subtype_rel_b-union-left
subtype_rel_b-union-right
subtype_rel_b-union_iff
subtype_rel_union
subtype_rel_union_left
subtype_rel_union_right
type-monotone-union-continuous
uall-union
union def
union-atom-disjoint
union-contains
union-contains2
union-continuous
union-continuous-type-monotone
union-continuous_wf
union-deq
union-deq_wf
union-list2
union-list2-simplify1
union-list2_wf
union-mono
union-nat-missing
union-nat-missing-pos
union-nat-missing-pos-prop
union-nat-missing-pos_wf
union-nat-missing-prop
union-nat-missing_wf
union-product-disjoint
union-set-is-set-exists
union-value-type
union-valueall-type
union-wf
union_empty_lemma
union_functionality_wrt_equipollent
union_functionality_wrt_iff
union_functionality_wrt_uiff
union_functionality_wrt_uiff2
union_functionality_wrt_uiff3
union_subtype_base
val-union
val-union-l-union
val-union_wf
UNION2
prev top next
bag-filter-union2
UNIONLIST
prev top next
RankEx2_UnionList
RankEx2_UnionList-unionlist
RankEx2_UnionList-unionlist_wf
RankEx2_UnionList?
RankEx2_UnionList?_wf
RankEx2_UnionList_wf
UNIONWITH
prev top next
bm_unionWith
bm_unionWith_ins
bm_unionWith_ins_wf
bm_unionWith_wf
UNIQUE
prev top next
Wzero-unique
add-inverse-unique
bar-converges-unique
coprime-equiv-unique
coprime-equiv-unique-pair
derivative_unique
div_unique
eff-unique
eff-unique-path
eff-unique-path_wf
eff-unique_wf
es-first-at-unique
es-first-unique
es-fix-unique
es-fwd-propagation-via-unique
es-prior-interface-val-unique
fps-div-unique
free_abmon_unique
fset-closure-unique
fset_for_when_unique
funinv-unique
gcd_unique
get_face_unique
imax-list-unique
mcopower_umap_unique
mon_for_when_unique
mset_for_when_unique
mu-bound-unique
mu-unique
new_23_sig_voter_start_unique
omral_alg_umap_unique
permutation-sorted-by-unique
polymorphic-id-unique
polymorphic-id-unique-sq
poset-cat-arrow-unique
poset-extend-unique
prime-factors-unique
prior-val-unique
pv11_p1_unique_adopted
pv11_p1_unique_adopted_fun
pv11_p1_unique_adopted_fun2
rec-class-unique
ses-cipher-unique
ses-nonce-unique
ses-signature-unique
sorted-by-strict-unique
sorted-by-unique
special-mod4-decomp-unique
strong-continuity2-no-inner-squash-unique
sup-unique
tsqrt-unique
unique-awf
unique-corec-solution
unique-limit
unique-minimal
unique-minimal-wellfounded-implies
unique-minimal_wf
unique-poset-functor
unique-sig-protocol
unique-sig-protocol_wf
unique_mfact
unique_set
unique_set_wf
UNIQUE2
prev top next
div_unique2
es-prior-interface-val-unique2
imax-list-unique2
ses-cipher-unique2
ses-signature-unique2
UNIQUE3
prev top next
div_unique3
UNIT
prev top next
all-unit
bag-combine-unit-left
bag-combine-unit-left-top
bag-combine-unit-right
csm-Kan-unit-cube-comp
csm-Kan-unit-cube-id
decidable__equal_unit
decidable__ex_unit
equal-in-unit
equal-unit
equipollent-type-unit-pair
equipollent-unit
exists-unit
finite-type-unit
is-list-if-has-value-rec-subtype-unit
isaxiom-bool-if-bunion-unit-prod
ispair-bool-if-bunion-unit-prod
itop_unroll_unit
massoc_imp_unit_diff
max_w_unit_l_tree
max_w_unit_l_tree_wf
mcomp_imp_not_unit
min_w_unit_l_tree
min_w_unit_l_tree_wf
mon_itop_unroll_unit
nat-inf-attach-unit
posint_unit_dec
product-unit-disjoint
rng_sum_unroll_unit
top-equipollent-unit
uall-unit
unit
unit-cube
unit-cube-I-cube
unit-cube-cubical-type
unit-cube-is-yoneda
unit-cube-map
unit-cube-map-comp
unit-cube-map-id
unit-cube-map_wf
unit-cube_wf
unit-deq
unit-deq_wf
unit-fps
unit-fps_wf
unit-interval-fan
unit-interval-fan_wf
unit-mono
unit-product-disjoint
unit-subtype-co-list
unit_chars
unit_subtype_base
unit_subtype_list
unit_triviality
unit_wf
unit_wf2
UNIV
prev top next
es-E-equality-univ-independent
fpf-cap-wf-univ
member-mapfilter-univ
UNIVERSE
prev top next
cubical-universe
cubical-universe-I-cube
cubical-universe_wf
universe def
UNIVI
prev top next
per-univi
UNMATCHED
prev top next
es-interface-unmatched
es-interface-unmatched_wf
UNORDERED
prev top next
count-unordered-combinations
subtype_rel_unordered-combination
unordered-combination
unordered-combination_functionality
unordered-combination_wf
UNROLL
prev top next
RankEx2_ind-unroll
append-unroll
concat-unroll
fact_unroll
fact_unroll_1
fps-exp-unroll
fun_exp_unroll
fun_exp_unroll_1
funtype-unroll
funtype-unroll-last
funtype-unroll-last-eq
genrec-unroll
itop_unroll_base
itop_unroll_hi
itop_unroll_lo
itop_unroll_unit
mk_applies_unroll
mk_lambdas-fun-unroll
mk_lambdas-fun-unroll-first
mk_lambdas_fun-unroll
mk_lambdas_fun-unroll-first
mk_lambdas_fun-unroll-ite
mk_lambdas_unroll
mk_lambdas_unroll_ite
mon_itop_unroll_base
mon_itop_unroll_hi
mon_itop_unroll_lo
mon_itop_unroll_unit
mon_nat_op_unroll
mu-unroll
natrec-unroll
peval-unroll
primrec-unroll
primrec-unroll-1
rnexp_unroll
rng_nexp_unroll
rng_sum_unroll_base
rng_sum_unroll_hi
rng_sum_unroll_lo
rng_sum_unroll_unit
rpolynomial_unroll
rsum_unroll
rv-partial-sum-unroll
strong-continuity-test-unroll
sum-unroll
sum-unroll-1
super-fact-unroll
ycomb-unroll
UNROLL2
prev top next
mk_lambdas_unroll2
UNROLLS
prev top next
count_unrolls
UNSHUFFLE
prev top next
length-unshuffle
select-unshuffle
unshuffle
unshuffle-iseg
unshuffle-map
unshuffle-map'
unshuffle-odd-length
unshuffle-shuffle
unshuffle_wf
UNSQUASHED
prev top next
unsquashed-WCP
unsquashed-WCP_wf
unsquashed-weak-continuity-base-false
unsquashed-weak-continuity-false
UNTIL
prev top next
es-quiet-until
es-quiet-until_wf
es-until
es-until_wf
hdf-until
hdf-until-ap
hdf-until-ap-fst
hdf-until-ap-snd
hdf-until-halt-left
hdf-until-halt-right
hdf-until_wf
until-class
until-class-program
until-class-program_wf
until-class-simple-comb
until-class_local
until-class_wf
until-classrel
UNZIP
prev top next
unzip
unzip-as-accum
unzip-un-zip
unzip_wf
unzip_zip
zip_unzip
UORDER
prev top next
uorder
uorder_functionality_wrt_iff
uorder_split
uorder_wf
UP
prev top next
int_seg_well_founded_up
UPD
prev top next
CLK_upd_clock
CLK_upd_clock_wf
pv11_p1_lt_bnum_upd
pv11_p1_upd_bnum
pv11_p1_upd_bnum_wf
pv11_p1_upd_desc
pv11_p1_upd_desc_iff
pv11_p1_upd_left
pv11_p1_upd_right
upd
upd_wf
UPDATE
prev top next
OARcast_deliverer_for_sender_seq_update
OARcast_deliverer_for_sender_seq_update_wf
OARcast_deliverer_for_sender_update
OARcast_deliverer_for_sender_update_wf
OARcast_on_oarcast_update
OARcast_on_oarcast_update_wf
OARcast_on_order_update
OARcast_on_order_update_wf
OARcast_on_ordered_update
OARcast_on_ordered_update_wf
fpf-compatible-update
identity-record+-update
identity-record-update
int-decr-map-update
int-decr-map-update-prop
int-decr-map-update_wf
list_update
list_update_length
list_update_select
list_update_wf
lookup-list-map-update
lookup-list-map-update-prop
lookup-list-map-update_wf
map-sig-update
map-sig-update_wf
member-update-alist1
new_23_sig_update_replica
new_23_sig_update_replica_wf
new_23_sig_update_round
new_23_sig_update_round_wf
no_repeats-update-alist
pv11_p1_update_proposals
pv11_p1_update_proposals_wf
rec_select_update_lemma
record-select-update
record-update
record-update-update
record-update_wf
select-update-tuple
test-eq-E-update
trivial-record-update
update
update-alist
update-alist_wf
update-assignment
update-assignment_wf
update-oarcast-deliver
update-oarcast-deliver_wf
update-tuple
update-tuple_wf
update_wf
weak-update-alist
weak-update-alist_wf
UPDATE2
prev top next
fpf-compatible-update2
UPDATE3
prev top next
fpf-compatible-update3
UPDATED
prev top next
apply-updated-alist
UPPER
prev top next
DVp_Array-upper
DVp_Array-upper_wf
comb_for_int_upper_wf
equipollent-int_upper-nat
fixpoint-upper-bound
int_le_to_int_upper
int_le_to_int_upper_uniform
int_lt_to_int_upper
int_lt_to_int_upper_uniform
int_upper
int_upper_ind
int_upper_ind_uniform
int_upper_properties
int_upper_subtype_int_upper
int_upper_subtype_nat
int_upper_uwell_founded
int_upper_well_founded
int_upper_wf
l_sum-upper-bound
l_sum-upper-bound-map
least-upper-bound
monotone-upper-bound-function
primrec-wf-upper
sq_stable__ex_int_upper
sq_stable__ex_int_upper_ap
strict-upper-bound
strict-upper-bound_functionality
strict-upper-bound_wf
strict-upper-bounds
strict-upper-bounds_wf
upper-bound
upper-bound_functionality
upper-bound_wf
upper-bounds
upper-bounds-closed
upper-bounds_wf
UPREORDER
prev top next
upreorder
upreorder_wf
UPTO
prev top next
A-shift-upto
A-shift-upto-spec
A-shift-upto-spec_wf
A-shift-upto_wf
assert-regular-upto
bag-member-from-upto
bag-summation-from-upto
bag-upto
bag-upto_wf
before-upto
concat_map_upto
cons_functionality_wrt_permr_upto
exists_uni_upto
exists_uni_upto_char
exists_uni_upto_wf
filter-upto-length
filter_map_upto
firstn_map_upto
firstn_upto
fps-product-upto
from-upto
from-upto-decomp-last
from-upto-is-nil
from-upto-is-singleton
from-upto-member
from-upto-member-nat
from-upto-nil
from-upto-shift
from-upto-single
from-upto-singleton
from-upto-sorted
from-upto-split
from-upto_wf
l-ordered-from-upto-lt
l-ordered-from-upto-lt-nat
l-ordered-from-upto-lt-nat-true
l-ordered-from-upto-lt-true
l_all_from-upto
l_disjoint_from-upto
l_sum-mapfilter-upto
last-from-upto
last-upto
length-from-upto
length_upto
map-as-map-upto
map-upto
map-upto-length
member-from-upto
member_upto
no_repeats_from-upto
no_repeats_upto
null-upto
permr_upto
permr_upto_equiv_rel
permr_upto_functionality_wrt_permr_upto
permr_upto_inversion
permr_upto_split
permr_upto_transitivity
permr_upto_weakening
permr_upto_wf
regular-upto
regular-upto-regularize
regular-upto_wf
select-from-upto
select-upto
select_upto
uni_sat_upto
uni_sat_upto_wf
upto
upto_add_1
upto_decomp
upto_decomp1
upto_decomp2
upto_equal_nil
upto_is_nil
upto_iseg
upto_wf
UPTO2
prev top next
filter_map_upto2
member_upto2
UPWD
prev top next
decidable__upwd-closure
upwd-closure
upwd-closure_wf
URAND
prev top next
urand
urand_wf
UREC
prev top next
subtype_urec
urec
urec-is-fixedpoint
urec-is-least-fixedpoint
urec-level
urec-level-property
urec-level_wf
urec-lfp
urec_induction
urec_subtype
urec_subtype_base
urec_wf
UREFL
prev top next
sq_stable__urefl
urefl
urefl_functionality_wrt_iff
urefl_shift
urefl_wf
USEABLE
prev top next
member-useable-atoms
pa-useable
pa-useable_wf
ses-is-protocol-action-useable
ses-useable-atoms
ses-useable-atoms_wf
USED
prev top next
member-used-atoms
pa-used
pa-used_wf
ses-is-protocol-action-used
ses-used-atoms
ses-used-atoms_wf
USING
prev top next
false-using-ispair-cases
fan-implies-nwkl!-using-PFan
restrict_perm_using_txpose
USYM
prev top next
sq_stable__usym
usym
usym_functionality_wrt_iff
usym_shift
usym_wf
UT1
prev top next
ut1-test
ut1-test_wf
UTRANS
prev top next
sq_stable__utrans
utrans
utrans_functionality_wrt_iff
utrans_imp_sp_utrans
utrans_imp_sp_utrans_a
utrans_imp_sp_utrans_b
utrans_rel_self_functionality
utrans_shift
utrans_wf
UWELL
prev top next
int_upper_uwell_founded
UWELLFOUNDED
prev top
W-uwellfounded
W-uwellfounded_witness
uwellfounded
uwellfounded_wf