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

N

top next

bezout_ident_n
bm_N
bm_N_wf
cbva_seq-sqequal-n
combinations-n-intersecting
divides_anti_sym_n
gcd_ex_n
gcd_exists_n
list_n
list_n_properties
list_n_wf
mk_lambdas-sqequal-n
n-intersecting
n-intersecting_wf
n-tuple
n-tuple-decomp
n-tuple_wf
quot_rem_exists_n
run-to-n
run-to-n_wf
simple-cbva-seq-sqequal-n
sqequal_n def
sqequal_n-wf
sqequal_n_add
sqequal_n_wf
sqle_n def
sqle_n-wf
sqle_n_subtype_rel
sqle_n_wf
tuple-type-subtype-n-tuple

N2

prev top next

mk_lambdas-sqequal-n2

NAME

prev top next

A-face-name
A-face-name-image
A-face-name_wf
assert-face-name-eq
assert-name-deq
assert-name_eq
coordinate_name
coordinate_name
coordinate_name-value-type
coordinate_name-value-type
coordinate_name_wf
coordinate_name_wf
cubical-path-same-name
decidable__equal-coordinate_name
decidable__equal-coordinate_name
decidable__equal_name
equal-by-name-cases
extend-name-morph
extend-name-morph-comp
extend-name-morph-face-map
extend-name-morph-iota
extend-name-morph-irrelevant
extend-name-morph-rename-one
extend-name-morph_wf
face-name
face-name-eq
face-name-eq_wf
face-name-image
face-name_wf
isname-name
lifting-bag-combine-decide-name_eq
lifting-callbyvalueall-decide-name_eq
mFOatomic-name
mFOatomic-name_wf
name
name-case
name-case_wf
name-cat
name-cat_wf
name-comp
name-comp-assoc
name-comp-flip
name-comp-id-left
name-comp-id-right
name-comp_wf
name-deq
name-deq_wf
name-morph
name-morph-ap
name-morph-decomp
name-morph-degeneracy-map
name-morph-domain
name-morph-domain-inject
name-morph-domain_subtype
name-morph-domain_wf
name-morph-ext
name-morph-extend
name-morph-extend-comp
name-morph-extend-face-map
name-morph-extend-id
name-morph-extend_wf
name-morph-flip
name-morph-flip-face-map
name-morph-flip-face-map1
name-morph-flip-flip
name-morph-flip-id
name-morph-flip_wf
name-morph-flips-commute
name-morph-inv
name-morph-inv-eq
name-morph-inv-eq-domain
name-morph-inv_wf
name-morph-nil
name-morph-one-one
name-morph-range
name-morph-range_wf
name-morph_subtype
name-morph_subtype_domain
name-morph_subtype_remove1
name-morph_wf
name-morphs-equal
name-path-endpoints
name-path-endpoints_wf
name-subst
name-subst_wf
name-valueall-type
name_eq
name_eq-is-inl
name_eq-normalize
name_eq-normalize-left
name_eq-normalize-name
name_eq-normalize-name2
name_eq-normalize2
name_eq-normalize3
name_eq-normalize4
name_eq_spread
name_eq_symmetry
name_eq_wf
name_wf
not-name_eq-implies-sq-bfalse
pDVloc_tag-name
pDVloc_tag-name_wf
path-eq-same-name
pinew-name
pinew-name_wf
pvar-name
pvar-name_wf
rename-one-extend-name-morph
rename-one-name
rename-one-name_wf
set-path-name
set-path-name_wf
sq-decider-name-deq
thread-name
thread-name_wf
uext-ap-name

NAME2

prev top next

name_eq-normalize-name2

NAMED

prev top next

equal-named-paths
named-path
named-path-equal-implies
named-path-morph
named-path-morph_wf
named-path-subtype
named-path_wf

NAMES

prev top next

pi-names
pi-names_wf
pi-prefix-names
pi-prefix-names_wf
swap-names
swap-names_wf

NAMESET

prev top next

decidable__nameset
decidable__nameset
extd-nameset
extd-nameset-nil
extd-nameset_subtype
extd-nameset_subtype_base
extd-nameset_subtype_int
extd-nameset_wf
isname-nameset
member-nameset-diff
member-nameset-diff
nameset
nameset
nameset-equipollent
nameset-equipollent
nameset-value-type
nameset-value-type
nameset_sq
nameset_sq
nameset_subtype
nameset_subtype
nameset_subtype_base
nameset_subtype_base
nameset_subtype_cons_diff
nameset_subtype_cons_diff
nameset_subtype_extd-nameset
nameset_wf
nameset_wf
nsub2_subtype_extd-nameset

NARY

prev top next

nary-rel
nary-rel-predicate
nary-rel-predicate_wf
nary-rel_wf

NAT

prev top next

absval_div_nat
add-nat
add-nat-missing
add-nat-missing-prop
add-nat-missing_wf
add-wf-bar-nat
add-wf-partial-nat
add_nat_wf
assert-in-missing-nat
assert-in-missing-nat-iff
assert-member-nat-missing
bag-sum_wf_nat
canonicalizable-nat-to-nat
comb_for_mon_nat_op_wf
comb_for_mon_nat_op_wf2
comb_for_nat_op_wf
comb_for_rng_nat_op_wf
comp-nat-ind-ext
comp_nat_ind_a
comp_nat_ind_tp
compact-nat-inf
complete-nat-induction
complete-nat-induction-ext
complete_nat_ind
complete_nat_ind_with_y
complete_nat_measure_ind
decidable__equal_nat
decidable__equal_nat_plus
div_div_nat
div_nat_induction
div_nat_induction-ext
empty-nat-missing
empty-nat-missing-prop
empty-nat-missing_wf
equal-nat-inf-infinity
equal-nat-inf-infinity2
equipollent-int-nat
equipollent-int_upper-nat
equipollent-nat-decidable-subset
equipollent-nat-list-as-product
equipollent-nat-list-nat
equipollent-nat-powered
equipollent-nat-powered2
equipollent-nat-powered3
equipollent-nat-prod-nsub
equipollent-nat-rationals
equipollent-nat-rationals-ext
equipollent-nat-sequences
equipollent-nat-squared
equipollent-nat-subset
equipollent-nat-union-nsub
exp_wf_nat_plus
fabmon_of_nat_mcp
fabmon_of_nat_mcp_wf
fix_wf_corec_partial_nat
free-from-atom-nat
from-upto-member-nat
gcd_sym_nat
imax-list-is-nat
imax-wf-bar-nat
int-prod_wf_nat
int_hgrp_to_nat
int_hgrp_to_nat_wf
int_seg_subtype-nat
int_upper_subtype_nat
isEmpty-nat-missing
isEmpty-nat-missing-prop
isEmpty-nat-missing_wf
l-ordered-from-upto-lt-nat
l-ordered-from-upto-lt-nat-true
length-nat-if-has-value
length_wf_nat
list-decomp-nat
list-decomp-nat-iseg
map_length_nat
map_length_nat
member-nat-missing
member-nat-missing_wf
member-nat-to-str
mk-set-nat-missing
mk-set-nat-missing_wf
mon_nat_op
mon_nat_op_add
mon_nat_op_hom_swap
mon_nat_op_id
mon_nat_op_mul
mon_nat_op_one
mon_nat_op_op
mon_nat_op_unroll
mon_nat_op_wf
mon_nat_op_wf2
mon_nat_op_zero
mul-nat
multiply_nat_wf
nat
nat-deq
nat-deq-aux
nat-deq_wf
nat-id-fun-example
nat-id-fun-ext
nat-inf
nat-inf-attach
nat-inf-attach-unit
nat-inf-infinity
nat-inf-infinity-new
nat-inf-infinity_wf
nat-inf_wf
nat-missing-type
nat-missing-type_wf
nat-mono
nat-overt
nat-retractible
nat-strong-overt-implies-Markov
nat-to-incomparable
nat-to-incomparable-property
nat-to-incomparable_wf
nat-to-str
nat-to-str_wf
nat-trans
nat-trans
nat-trans-equal
nat-trans-equal
nat-trans_wf
nat-trans_wf
nat-weak-overt
nat_add_mon
nat_add_mon_wf
nat_add_mon_wf2
nat_inc
nat_ind
nat_ind_a
nat_int_grp_sig_hom
nat_op
nat_op_add
nat_op_mon_hom_1
nat_op_mon_hom_2
nat_op_on_nat_add_mon
nat_op_wf
nat_op_zero
nat_plus
nat_plus_inc
nat_plus_inc_int_nzero
nat_plus_inc_nat
nat_plus_properties
nat_plus_subtype_nat
nat_plus_wf
nat_properties
nat_sq
nat_subtype
nat_well_founded
nat_wf
ni-max-nat
ni-min-nat
primrec-wf-nat-plus
rec-nat-induction
reducible-nat
remove-nat-missing
remove-nat-missing-prop
remove-nat-missing_wf
rng_nat_op
rng_nat_op-int
rng_nat_op_add
rng_nat_op_one
rng_nat_op_wf
rng_times_nat_op
rng_times_nat_op_r
select-last-in-nat-missing
select-last-in-nat-missing_wf
singleton-nat-missing
singleton-nat-missing-prop
singleton-nat-missing_wf
sq_stable__ex_nat
str-to-nat
str-to-nat-plus
str-to-nat-plus-property
str-to-nat-plus_wf
str-to-nat-to-str
str-to-nat_wf
str1-to-nat
str1-to-nat_wf
strong-continuity2-implies-uniform-continuity-nat
strong-continuity2-implies-uniform-continuity-nat-ext
strong-continuity2-implies-weak-skolem-cantor-nat
sum-nat
sum-nat-le
sum-nat-less
sum-partial-nat
test-nat-param
uniform-comp-nat-induction
uniform_nat_measure_ind
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
zero-le-nat
zhgrp_to_nat_is_hom

NAT1

prev top next

trivial_nat1_fun

NAT2INF

prev top next

nat2inf
nat2inf-injection
nat2inf-one-one
nat2inf_wf

NAT2INT

prev top next

nat2int
nat2int_wf

NATREC

prev top next

natrec
natrec-unroll
natrec_wf
natrec_wf_intseg

NATS

prev top next

nats
nats_wf
nth-nats

NATURAL

prev top next

natural_number def
natural_number_wf_p-outcome

NBOT

prev top next

test-bnot-nbot

NCHAR

prev top next

divides_nchar

ND

prev top next

nd-append

NDIFF

prev top next

comb_for_ndiff_wf
ndiff
ndiff_add_eq_imax
ndiff_ann_l
ndiff_id_r
ndiff_inv
ndiff_ndiff
ndiff_ndiff_eq_imin
ndiff_wf
ndiff_zero

NDIVIDES

prev top next

coprime_iff_ndivides

NDLIST

prev top next

cons-ndlist
ndlist
ndlist_wf
nil-ndlist

NEAR

prev top next

Riemann-sums-near
compact-proper-interval-near-member
near-fixpoint-on-0-1
near-root
near-root-rational
near-root-rational-ext
near-root_wf

NEG

prev top next

absval_neg
bool-to-neg-dcdr
bool-to-neg-dcdr-aux
bool-to-neg-dcdr_wf
es-interface-sum-non-neg
expectation-non-neg
fps-compose-neg
fps-elim-x-neg
fps-neg
fps-neg-slice
fps-neg_wf
fps-set-to-one-neg
gcd-non-neg
gcd_p_neg_arg
gcd_p_neg_arg_2
gcd_p_neg_arg_a
linorder_le_neg
linorder_lt_neg
lookup_oal_neg
member_rset_neg_lemma
neg-approx-of-nonneg-real
neg_assert_of_eq_atom
neg_assert_of_eq_atom1
neg_assert_of_eq_int
neg_assoc_fps
neg_assoced
neg_id_fps
neg_inv_fps
neg_mul_arg_bounds
neg_thru_op_fps
non_neg_length
non_neg_mset_size
non_neg_sum
non_neg_sum-map
oal_dom_neg
oal_lk_neg
oal_lv_neg
oal_neg
oal_neg_eq_nil
oal_neg_keys_invar
oal_neg_left_inv
oal_neg_non_id_vals
oal_neg_right_inv
oal_neg_sd_ordered
oal_neg_wf
oal_neg_wf2
rroot-abs-non-neg
rset-neg
rset-neg_wf
square_non_neg
subtype_neg_polymorphism_test
totally-bounded-neg
ulinorder_le_neg
ulinorder_lt_neg

NEG1

prev top next

mul-non-neg1

NEGATION

prev top next

classical-double-negation
double-negation-hyp-elim
double-negation-iff-xmiddle
double-negation-shift
double-negation-shift_wf
finite-double-negation-shift
finite-double-negation-shift-extract
minimal-double-negation-hyp-elim
no-uniform-double-negation-elim

NEGATIVE

prev top next

rinv-negative
rmul-is-negative

NEGATIVE1

prev top next

rmul-is-negative1

NEGERSE

prev top next

negerse_fps

NELIM

prev top next

assoced_nelim

NEQ

prev top next

btrue_neq_bfalse
cons_neq_nil
find-real-neq
fps-compose-atom-neq
rabs-neq-zero
rinv-neq-zero
rmul-neq-zero

NEQ2

prev top next

find-real-neq2

NEQUAL

prev top next

nequal
nequal-le-implies
nequal_wf

NERVE1

prev top next

face-compatible-cubical-nerve1

NESTED

prev top next

subtype_rel_nested_set
subtype_rel_nested_set2

NEWARRAY

prev top next

newarray
newarray_wf

NEWROUNDS

prev top next

new_23_sig_NewRounds
new_23_sig_NewRounds-program
new_23_sig_NewRounds-program_wf
new_23_sig_NewRounds_wf

NEWROUNDSSTATE

prev top next

new_23_sig_NewRoundsState
new_23_sig_NewRoundsState-classrel
new_23_sig_NewRoundsState-functional
new_23_sig_NewRoundsState-program
new_23_sig_NewRoundsState-program_wf
new_23_sig_NewRoundsState_wf

NEWROUNDSSTATEFUN

prev top next

new_23_sig_NewRoundsStateFun
new_23_sig_NewRoundsStateFun_wf

NEWS

prev top next

pv11_p1_append_news
pv11_p1_append_news_iff
pv11_p1_append_news_iff2
pv11_p1_append_news_wf

NEWTON

prev top next

integer-sqrt-newton
integer-sqrt-newton-ext
isqrt_newton
isqrt_newton_wf

NEWVOTE

prev top next

new_23_sig_assert_newvote
new_23_sig_newvote
new_23_sig_newvote_wf

NEWVOTERS

prev top next

new_23_sig_NewVoters
new_23_sig_NewVoters-program
new_23_sig_NewVoters-program_wf
new_23_sig_NewVoters_wf

NEXP

prev top next

comb_for_rng_nexp_wf
reg-seq-nexp
reg-seq-nexp_wf
rng_nexp
rng_nexp-int
rng_nexp_unroll
rng_nexp_wf
rng_nexp_zero

NEXT

prev top next

Comm-next-comment
Comm-next-continue
Comm-next-continue_wf
Comm-next-guards
Comm-next-guards_wf
Comm-next-selex
Comm-next-selex_wf
bm_collate_next
bm_collate_next_wf
es-next
next
next-unfold
next_wf
next_wf_bound
run-event-state-next
st-next
st-next_wf

NEXT2

prev top next

run-event-state-next2

NFOLDUNION

prev top next

nfoldunion
nfoldunion_wf

NI

prev top next

ni-eventually-equal
ni-eventually-equal-equiv
ni-eventually-equal_wf
ni-iterated-min
ni-iterated-min_wf
ni-max
ni-max-assoc
ni-max-com
ni-max-idemp
ni-max-identity
ni-max-nat
ni-max-zero
ni-max_wf
ni-min
ni-min-assoc
ni-min-com
ni-min-idemp
ni-min-identity
ni-min-nat
ni-min-zero
ni-min_wf
ni-selector
ni-selector-property
ni-selector_wf
not-ni-eventually-equal-inf

NID

prev top next

oal_lv_nid

NIL

prev top next

W_select_nil_lemma
accum_filter_rel_nil
adjacent-nil
agree_on_common_nil
append-append-nil
append-nil
append-nil-sqle
append_back_nil
append_cancel_nil
append_is_nil
append_is_nil_test
append_nil_sq
archive-condition-nil
bag-filter-is-nil
ball_nil_lemma
before_nil_lemma
bexists_nil_lemma
bl-exists-nil
callbyvalueall-nil
callbyvalueall-single-append-nil
case_nil
church-nil
church-nil_wf
church_null_nil_lemma
co-list-nil
co-list-nil_wf
co_w_select_nil_lemma
concat-is-nil
concat-map-nil
concat-nil
concat_conv_single_nil_lemma
cons_neq_nil
cons_sublist_nil
count_nil_lemma
data_stream_nil_lemma
deq_member_nil_lemma
diff_nil_lemma
distinct_nil_lemma
equal-nil-lists
equal-nil-sq-nil
es-before-is-nil-if-first
es-closed-open-interval-nil
es-interface-predecessors-nil
es-interface-vals-nil
es-interval-is-nil
es-interval-nil
es-open-interval-nil
es-prior-interface-vals-nil
eval_list-append-nil-is-eval_list
eval_list-sqle-append-nil
eval_list_nil_lemma
evalall-append-nil
evalall_nil_lemma
extd-nameset-nil
filter-nil
filter2_nil_lemma
filter_is_nil
filter_is_nil_implies
filter_is_nil_implies2
filter_nil_lemma
find-combine-nil
for_hdtl_nil_lemma
for_nil_lemma
fpf-vals-nil
fpf_join_nil_lemma
from-upto-is-nil
from-upto-nil
fseg_nil
has-value-append-nil
has-valueall-append-nil
hd-nil
insert-combine-nil
insert-not-nil
insert_nil_lemma
interleaving_of_nil
isaxiom-append-nil
iseg_nil
islist-append-nil-is-list
islist-append-nil-sqequal-islist
ispair-or-isaxiom-append-nil
iter_df_nil_lemma
iter_hdf_nil_lemma
l-last-nil
l-ordered-nil
l-ordered-nil-true
l-union-nil
l_all-nil
l_all_nil
l_all_nil_iff
l_all_wf_nil
l_contains_nil
l_disjoint_nil
l_disjoint_nil_iff
l_exists_nil
l_exists_wf_nil
l_ind_nil_lemma
l_intersection_nil
l_member_non_nil
l_subset_nil_left
l_subset_nil_left_true
l_sum_nil_lemma
last_nil
lastn-nil
len_nil_lemma
length-nil
length-zero-implies-nil
length-zero-implies-sq-nil
length_nil
length_of_nil_lemma
length_of_not_nil
length_wf_nil
lg-append-nil
lg-nil
lg-nil-append
lg-nil_wf
lg-nil_wf_dag
lg-size-nil
list_acc_nil_red_lemma
list_accum_nil_lemma
list_ind_nil_lemma
list_to_set_nil_lemma
listid_nil_lemma
listp-not-nil
loc-on-path-nil
longest-prefix-is-nil
lookup_nil_lemma
manames-overlap-nil
map_is_nil
map_nil_lemma
mapcons_nil_lemma
mapfilter-nil
mapfilter-not-nil
mapfilter_nil_lemma
mem_nil_lemma
member_not_nil
mon_for_nil_lemma
mon_htfor_nil_lemma
mul_list_nil_lemma
name-morph-nil
nil
nil-append
nil-contains
nil-iff-no-member
nil-llex
nil-ndlist
nil-sublist
nil_before
nil_fseg
nil_in_oalist
nil_interleaving
nil_interleaving2
nil_iseg
nil_member
nil_member!
nil_member-variant
nil_sublist
nil_wf
no-member-sq-nil
no_repeats_nil
no_repeats_nil_uiff
non_nil_length
not_permr_cons_nil
nth_tl_is_nil
nth_tl_nil
null_nil_lemma
oal_merge_left_nil_lemma
oal_merge_right_nil_lemma
oal_neg_eq_nil
oal_nil
oal_nil_ident_l
oal_nil_ident_r
oal_nil_wf
open_box-nil
p_first_nil_lemma
pairwise-nil
partition-mesh-nil
permr_nil_is_nil
permutation-nil
permutation-nil-iff
pi1-if-ispair-append-nil
pi2-if-ispair-append-nil
poset-cat-arrow-filter-nil
prod-if-ispair-append-nil
quicksort-int-nil
radd_list_nil_lemma
rcvd-innings-nil
reduce2_nil_lemma
reduce_nil_lemma
reduce_tl_nil_lemma
remove-combine-nil
remove-repeats-fun-nil
remove1_nil_lemma
remove_leading_eq_nil
remove_repeats_nil_lemma
rev_app_nil_lemma
reverse_nil_lemma
safety_nil
sd_ordered_nil_lemma
select-nil
set-equal-nil
single-bag-append-nil
sorted-by-nil
sorted-by_wf_nil
sqequal-nil
sqle-append-nil-if-has-value4
stump-nil
sublist-rec-nil
sublist-rec-nil-iff
sublist_nil
sum_map_nil_lemma
test-select-nil
tupletype_nil_lemma
upto_equal_nil
upto_is_nil
values-for-distinct-nil
votes-from-inning-is-nil
w-nil
w-nil_wf
weighted-sum-nil
ws_nil_lemma
zip_cons_nil_lemma
zip_nil_lemma

NIL2

prev top next

callbyvalueall-nil2
filter_is_nil2
l_disjoint_nil2
manames-overlap-nil2
set-equal-nil2

NIL3

prev top next

filter_is_nil3

NO

prev top next

CLK_headers_no_inputs
CLK_headers_no_inputs_types
CLK_headers_no_inputs_types_wf
CLK_headers_no_inputs_wf
CLK_headers_no_rep
CLK_headers_no_rep_wf
OARcast_headers_no_inputs
OARcast_headers_no_inputs_types
OARcast_headers_no_inputs_types_wf
OARcast_headers_no_inputs_wf
OARcast_headers_no_rep
OARcast_headers_no_rep_wf
apply-alist-no_repeats
assert-bag-has-no-repeats
bag-append-no-repeats
bag-append-no-repeats1
bag-combine-no-repeats
bag-combine-no-repeats2
bag-count-member-no-repeats
bag-drop-no-repeats
bag-extensionality-no-repeats
bag-filter-no-repeats
bag-filter-no-repeats2
bag-has-no-repeats
bag-has-no-repeats_wf
bag-map-no-repeats
bag-moebius-no-repeats
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-parts'-no-repeats
bag-parts-no-repeats
bag-product-no-repeats
bag-remove-repeats-if-no-repeats
bag-remove-repeats-no-repeats
bag-remove-size-member-no-repeats
bag-single-no-repeats
bag-subtract-member-if-no-repeats
bag-subtract-no-repeats
bag-summation-single-non-zero-no-repeats
cardinality-le-no_repeats-length
class-output-support-no-repeats
class-output-support-no_repeats
compat-no_repeats_common-member
decidable__no_repeats
delivered-with-headers-no_repeats
empty-bag-iff-no-member
empty-bag-no-repeats
eo-forward-no-classrel-in-interval
eo-forward-no-prior-classrel
es-before-no_repeats
es-interface-predecessors-no_repeats
es-interface-predecessors-no_repeats2
es-le-before-no_repeats
es-prior-fixedpoints-no_repeats
fun-path-no_repeats
has-no-path
has-no-path_wf
insert-by-no-repeats
insert-no-combine
insert-no-combine-permutation
insert-no-combine-sorted-by
insert-no-combine_wf
l-ordered-no_repeats
l_before_no_repeats
l_contains-eq_set-no_repeats
l_contains-no_repeats-length
list-decomp-no_repeats
loop-class-memory-no-input
mapfilter-no-rep-fun
member-insert-no-combine
new_23_sig_headers_no_inputs
new_23_sig_headers_no_inputs_types
new_23_sig_headers_no_inputs_types_wf
new_23_sig_headers_no_inputs_wf
new_23_sig_headers_no_rep
new_23_sig_headers_no_rep_wf
nil-iff-no-member
no-classrel-iff-empty
no-classrel-in-interval
no-classrel-in-interval-trivial
no-classrel-in-interval_wf
no-descending-chain
no-descending-chain-implies-wellfounded
no-descending-chain_wf
no-excluded-middle
no-excluded-middle
no-excluded-middle-quot-true
no-excluded-middle-quot-true1
no-excluded-middle-quot-true2
no-excluded-middle-squash
no-halt-decider
no-member-sq-nil
no-prior-classrel
no-prior-classrel_wf
no-prior-val
no-repeats-bag-partitions
no-repeats-bag-to-set
no-repeats-iff-count
no-repeats-list-to-set
no-repeats-pairwise
no-uniform-Peirce's-law
no-uniform-double-negation-elim
no-uniform-xmiddle
no-value-bottom
no-value-bottom
no-value-bottom-base
no-weakly-safe-extensions
no_rel_repeats
no_rel_repeats_wf
no_repeats
no_repeats-append
no_repeats-bag
no_repeats-before-equality
no_repeats-concat
no_repeats-concat-iff
no_repeats-count-repeats1
no_repeats-firstn
no_repeats-insert
no_repeats-l_member!
no_repeats-merge
no_repeats-pairs-fpf
no_repeats-permute
no_repeats-remove-first
no_repeats-residues-mod
no_repeats-settype
no_repeats-single
no_repeats-strong-subtype
no_repeats-sublist
no_repeats-subtype
no_repeats-union-list
no_repeats-update-alist
no_repeats_append
no_repeats_append_iff
no_repeats_concat
no_repeats_cons
no_repeats_filter
no_repeats_filter2
no_repeats_from-upto
no_repeats_functionality_wrt_permutation
no_repeats_iff
no_repeats_inject
no_repeats_l_index
no_repeats_l_index-inj
no_repeats_list-diff
no_repeats_map
no_repeats_map_uiff
no_repeats_member
no_repeats_mu_index
no_repeats_nil
no_repeats_nil_uiff
no_repeats_reverse
no_repeats_safety
no_repeats_singleton
no_repeats_singleton_uiff
no_repeats_union
no_repeats_upto
no_repeats_wf
no_repeats_witness
nysiad_headers_no_inputs
nysiad_headers_no_inputs_types
nysiad_headers_no_inputs_types_wf
nysiad_headers_no_inputs_wf
nysiad_headers_no_rep
nysiad_headers_no_rep_wf
old_no_repeats
pairwise-mapl-no-repeats
permutation-when-no_repeats
pv11_p1_headers_no_inputs
pv11_p1_headers_no_inputs_types
pv11_p1_headers_no_inputs_types_wf
pv11_p1_headers_no_inputs_wf
pv11_p1_headers_no_rep
pv11_p1_headers_no_rep_wf
remove-first-no_repeats-member
remove-repeats-length-no-repeats
remove-repeats-length-no-repeats-iff
remove-repeats-no_repeats
remove-repeats-no_repeats-true
s-insert-no-repeats
send-once-no-prior-classrel
ses-thread-no_repeats
set-equal-no_repeats-length
sorted-by-no_repeats
sorted-by-strict-no_repeats
sq_stable__bag-no-repeats
sq_stable__no-classrel-in-interval
sq_stable__no-prior-classrel
sq_stable__no_repeats
strong-continuity2-no-inner-squash
strong-continuity2-no-inner-squash-cantor
strong-continuity2-no-inner-squash-cantor2
strong-continuity2-no-inner-squash-cantor3
strong-continuity2-no-inner-squash-cantor4
strong-continuity2-no-inner-squash-cantor5
strong-continuity2-no-inner-squash-unique
strong-message-constraint-no-rep
strong-message-constraint-no-rep-implies
strong-message-constraint-no-rep-large
strong-message-constraint-no-rep-large-1hdr
strong-message-constraint-no-rep-large-implies
strong-message-constraint-no-rep-large_wf
strong-message-constraint-no-rep_wf
sub-bag-list-if-bag-no-repeats-sq
sub-bag-no-repeats-iff
sub-bag-remove-repeats-if-no-repeats
sub-bags-no-repeats
sublist-if-no_repeats
three-cs-no-repeated-votes
two-factorizations-no-repeats

NOBRACKETS

prev top next

nobrackets

NODE

prev top next

MMTree_Node
MMTree_Node-forest
MMTree_Node-forest_wf
MMTree_Node?
MMTree_Node?_wf
MMTree_Node_wf
MTree_Node
MTree_Node-children
MTree_Node-children_wf
MTree_Node-labels
MTree_Node-labels_wf
MTree_Node?
MTree_Node?_wf
MTree_Node_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
l_tree_node
l_tree_node-left_subtree
l_tree_node-left_subtree_wf
l_tree_node-right_subtree
l_tree_node-right_subtree_wf
l_tree_node-val
l_tree_node-val_wf
l_tree_node?
l_tree_node?_wf
l_tree_node_wf
run-command-node
run-command-node_wf
tree_node
tree_node-left
tree_node-left_wf
tree_node-right
tree_node-right_wf
tree_node?
tree_node?_wf
tree_node_wf
wfd_tree_rec_node_lemma

NOLOC

prev top next

base-noloc-classrel
base-noloc-classrel-make-Msg
base-noloc-classrel-make-Msg2
base-noloc-classrel2

NON

prev top next

IVT-locally-non-constant
State-loc-comb-classrel-non-loc
State-loc-comb-fun-eq-non-loc
State-loc-comb-non-empty
State-loc-comb-non-empty-iff
apply-cycle-non-member
bag-summation-single-non-zero
bag-summation-single-non-zero-no-repeats
base-process-inputs-non-null
cubical-interval-non-trivial-box
decidable-non-minimal
decidable-non-minimal_wf
equipollent-non-zero
es-interface-sum-non-neg
es-interval-non-zero
es-prior-fixedpoints-non-null
exp-non-zero
expectation-non-neg
fact-non-decreasing
fact-non-zero
fps-non-trivial
frs-increasing-non-dec
frs-non-dec
frs-non-dec-sorted-by
frs-non-dec_wf
full-partition-non-dec
gcd-non-neg
gcd-non-zero
generic-non-empty
isqrt-non-decreasing
l_member_non_nil
last-concat-non-null
locally-non-constant
locally-non-constant-deriv-seq-test
locally-non-constant-rational
locally-non-constant-rational_wf
locally-non-constant-via-rational
locally-non-constant_wf
locally-non-zero-finite-deriv-seq
lookup_non_zero
member-eclass-iff-non-empty
mul-non-neg1
non-axiom-list
non-axiom-listunion
non-empty-bag-implies-non-void
non-empty-bag-mapfilter-union-of-list
non-empty-bag-union-of-list
non-forking
non-forking-rel_exp
non-forking-wellfounded-linorder
non-forking_wf
non-homogeneous-add
non-null-list-tactic-test
non-pair-list
non-pair-listunion
non-trivial-open-box
non-void-decl
non-void-decl-join
non-void-decl-single
non-void-decl_wf
non-zero-deriv-non-constant
non_munit_diff_imp_mpdivides
non_neg_length
non_neg_mset_size
non_neg_sum
non_neg_sum-map
non_nil_length
non_null_filter
non_null_filter_iff
non_null_iff_length
oal_merge_non_id_vals
oal_neg_non_id_vals
omral_plus_non_zero_vals
omral_scale_non_zero_vals
omral_times_non_zero_vals
poset-cat-dist-non-zero
prior-vals-non-null
ring_non_triv
ring_non_triv_wf
rpolynomial-locally-non-zero
rpolynomial-locally-non-zero-1
rroot-abs-non-neg
sq_stable__frs-non-dec
square_non_neg

NONCE

prev top next

nonce-release-lemma
nonce-release-lemma2
ses-legal-thread-has*-nonce
ses-nonce
ses-nonce-disjoint
ses-nonce-disjoint_wf
ses-nonce-from-ordering
ses-nonce-release
ses-nonce-unique
ses-nonce_wf

NONCELIKE

prev top next

noncelike-signatures
noncelike-signatures_wf

NONDECREASING

prev top next

const_nondecreasing
nondecreasing
nondecreasing_wf

NONE

prev top next

l-first-when-none
mon_for_when_none
mset_for_when_none

NONEMPTY

prev top next

es-interface-predecessors-nonempty
nonempty-es-interface-history

NONNEG

prev top next

add-nonneg
add-positive-nonneg
bag-sum-nonneg
dot-product-nonneg
frs-mesh-nonneg
icompact-length-nonneg
le-iff-nonneg
neg-approx-of-nonneg-real
partition-mesh-nonneg
rabs-nonneg
rabs-of-nonneg
real-vec-norm-nonneg
rmax-nonneg
rmin-nonneg
rminus-nonneg
rmul-nonneg
rnexp-even-nonneg
rnexp-nonneg
rsqrt_nonneg
rsum_nonneg
square-nonneg

NONNULL

prev top next

es-interface-predecessors-nonnull

NONPOS

prev top next

rabs-of-nonpos

NONTRIVIAL

prev top next

eu-nontrivial
eu-nontrivial_wf

NONVOID

prev top next

i-nonvoid
i-nonvoid_wf
totally-bounded-implies-nonvoid

NONZERO

prev top next

const-nonzero-on
nonzero-on
nonzero-on-implies
nonzero-on_wf
rabs-nonzero-on-compact
rinverse-nonzero
rmul-nonzero
rmul-nonzero-on
rpower-nonzero

NOOP

prev top next

lg-remove-noop

NORM

prev top next

norm-component
norm-component_wf
norm-components
norm-components_wf
norm-factors
norm-factors_wf
norm-fst
norm-fst_wf
norm-intransit
norm-intransit_wf
norm-lg
norm-lg_wf
norm-list
norm-list_wf
norm-list_wf_sq
norm-pair
norm-pair_wf
norm-pair_wf_sq
norm-runinfo
norm-runinfo_wf
norm-snd
norm-snd_wf
norm-system
norm-system_wf
norm-union
norm-union_wf
norm_subgrp
norm_subgrp_wf
norm_subset_p
norm_subset_p_wf
real-vec-norm
real-vec-norm-mul
real-vec-norm-nonneg
real-vec-norm-squared
real-vec-norm_functionality
real-vec-norm_wf

NORMAL

prev top next

append-normal-form
filter-normal-form
id-member-normal-form
implies-normal-ds
kind-member-normal-form
length-normal-form
normal-da
normal-da-join
normal-da-single
normal-da_wf
normal-decl-set
normal-decl-set_wf
normal-ds
normal-ds-join
normal-ds-single
normal-ds_wf
normal-p-outcome
normal-top
normal-type
normal-type_wf
pi-normal
pi-normal_wf
remove-repeats-normal-form

NORMALIZATION

prev top next

normalization-callbyvalueall-spread1
normalization-callbyvalueall-spread2
normalization-isaxiom
normalization-spread
normalization-spread2
normalization-spread3
normalization-spread4

NORMALIZE

prev top next

atom_eq_sq_normalize
fpf-normalize
fpf-normalize-ap
fpf-normalize-dom
fpf-normalize_wf
name_eq-normalize
name_eq-normalize-left
name_eq-normalize-name
name_eq-normalize-name2
normalize-decide-left
normalize-decide-right
seq-append-normalize
seq-normalize
seq-normalize-append
seq-normalize-equal
seq-normalize-normalize
seq-normalize_wf
test-cbv-normalize
test-cbva-normalize
test-cform-normalize
test-decide-normalize
test-int-cmp-normalize
test-spread-normalize
test2-cform-normalize
test3-cform-normalize
test4-cform-normalize
test5-cform-normalize

NORMALIZE0

prev top next

seq-normalize0

NORMALIZE2

prev top next

name_eq-normalize2

NORMALIZE3

prev top next

name_eq-normalize3

NORMALIZE4

prev top next

name_eq-normalize4

NOT

prev top next

DNS-iff-not-not-GMP
W-to-not-not-sig
W-to-not-not-sig2
alle-at-not-first
alle-between1-not-first-since
alle-between2-not-first-since
atom-sdata-not-pair
atom-sdata-not-pair2
bag-maximals-not-max
bag-member-not-bag-null
bar-converges-not-diverges
base-partial-not-exception
bm_insert_if_not_in
bm_insert_if_not_in_wf
comb_for_not_wf
cons_iseg_not_null
cs-not-completed
cs-not-completed_wf
decidable-predicate-not
decidable__cs-not-completed
decidable__not
eo-forward-not-first
eo-forward-not-first2
es-bless-not-ble
es-knows-not
es-le-before-not-null
es-le-not-locl
es-locl-not-le
es-not
es-not_wf
eu-not-colinear-OXY
eu-not-equal-OXY
eu-not-not-colinear
even-iff-not-odd
even-succ-implies-not-even
exception-not-axiom
exception-not-bottom
exception-not-bottom_1
exception-not-value
exception-not-value-or-bottom
exception-not-value2
exception-not-value_1
fan-implies-barred-not-unbounded
fix-not-exception
fps-not-null
fresh-cname-not-equal
fresh-cname-not-equal
fresh-cname-not-equal2
fresh-cname-not-equal2
fresh-cname-not-member
fresh-cname-not-member
fresh-cname-not-member2
fresh-cname-not-member2
fun-not-int
function-not-int
hd-wf-not-null
id-sdata-not-pair
id-sdata-not-pair2
insert-not-nil
int-decr-map-find-not-in
isatom-implies-not-isint
isatom-implies-not-ispair
isaxiom-implies-not-isint
isinl-implies-not-isatom
isinl-implies-not-isint
isinr-implies-not-isatom
isinr-implies-not-isint
isint-implies-not-isatom
isl-not-isr
islocal-not-isrcv
ispair-implies-not-isatom
ispair-implies-not-isint
isr-not-isl
known_not_false
l_all_not
last-not-before
length_of_not_nil
listp-not-nil
lnk-decl-dom-not
longer-list-not-member
mapfilter-not-nil
markov-streamless-iff-not-not-enum
mcomp_imp_not_unit
member_not_nil
minimal-not-not-excluded-middle
minimal-not-not-excluded-middle-ext
new_23_sig_vote_with_ballot_first-not
not
not-Sierpinski-bottom
not-Sierpinski-top
not-all-int_seg
not-alle-lt
not-assert
not-assert-bl-all
not-assert-bl-exists
not-assert-isname
not-atom-member-int
not-axiom-member-int
not-bfalse-sqle-btrue
not-bl-exists-eq-bl-all
not-btrue-sqeq-bfalse
not-btrue-sqeq-bottom
not-btrue-sqle-bfalse
not-btrue-sqle-bottom
not-diverges-converges
not-equal-2
not-even-succ-implies-even
not-exception-has-value
not-false
not-ge
not-ge-2
not-gt
not-gt-2
not-has-value-bottom
not-has-value-decidable-quot
not-id-sqle-bottom
not-inject
not-inl-sqeq-inr
not-is-exception-bottom
not-isl-assert-isr
not-isl-isr
not-isl-priority-select
not-ispair
not-isr-assert-isl
not-isr-isl
not-l_all-dec
not-l_exists
not-le
not-le-2
not-list-member-not-bag-member
not-name_eq-implies-sq-bfalse
not-ni-eventually-equal-inf
not-not-assert
not-not-excluded-middle
not-not-inner-pasch
not-not-sig-to-W
not-not-sig-to-W-implies-stable
not-nullset
not-pair-member-int
not-pv11_p1_leq_bnum
not-quotient-function-subtype
not-rless
not-rneq
not-rpositive
not-same-parity-implies
not-same-parity-implies-even-odd
not-self-starting
not-self-starting_wf
not-tree-big
not-true
not_all_sqequal
not_assert_elim
not_functionality_wrt_iff
not_functionality_wrt_implies
not_functionality_wrt_uiff
not_functionality_wrt_uimplies
not_has-value_decidable_on_base
not_id_sqeq_bottom
not_locl_rcv
not_mem_remove1
not_over_and
not_over_and_b
not_over_exists
not_over_exists_uniform
not_over_implies
not_over_not
not_over_or
not_over_or_a
not_permr_cons_nil
not_rcv_locl
not_squash
not_subtype_rel
not_wf
not_zero_sqequal_one
odd-iff-not-even
partial-not-exception
poset-cat-arrow-not-equal
predicate-not
predicate-not_wf
pv11_p1_lt_bnum_implies_not
req-iff-not-rneq
rleq-iff-not-rless
ses-private-not-public
ses-public-not-private
single-bag-not-null
sq_stable__not
squash_not
stable__not
streamless-implies-not-not-enum
subtype_rel_not

NOT2

prev top next

new_23_sig_vote_with_ballot_first-not2
pv11_p1_lt_bnum_implies_not2

NOT3

prev top next

pv11_p1_lt_bnum_implies_not3

NOTE

prev top next

note-is-function

NOTES

prev top next

NOTES_ON_JUNK
process model notes

NOTIFY

prev top next

new_23_sig-notify
new_23_sig_Notify
new_23_sig_Notify-program
new_23_sig_Notify-program_wf
new_23_sig_Notify_wf
new_23_sig_notify'broadcast
new_23_sig_notify'broadcast_wf

NR

prev top next

ses-NR
ses-NR_wf

NREL

prev top next

div_fun_sat_div_nrel
div_nrel
div_nrel_wf
rem_fun_sat_rem_nrel
rem_nrel
rem_nrel_wf

NSGRP

prev top next

nsgrp_of_ideal
nsgrp_of_ideal_wf

NSL

prev top next

NSL-authentication-property
NSL-authentication-property_wf
NSL-initiator1
NSL-initiator1_wf
NSL-initiator2
NSL-initiator2_wf
NSL-initiator3
NSL-initiator3_wf
NSL-protocol
NSL-protocol-legal
NSL-protocol_wf
NSL-responder0
NSL-responder0_wf
NSL-responder1
NSL-responder1_wf
NSL-responder2
NSL-responder2_wf
NSL-responder3
NSL-responder3_wf

NSUB

prev top next

equipollent-nat-prod-nsub
equipollent-nat-union-nsub
equipollent-nsub
nsub_finite
primrec-wf-nsub

NSUB2

prev top next

all-nsub2
nsub2-flip
nsub2_subtype_extd-nameset

NTH

prev top next

add-nth
add-nth_wf
add-remove-nth
apply-nth
apply-nth_wf
bexists_iff_exists_nth
comb_for_nth_tl_wf
firstn_nth_tl
firstn_nth_tl_decomp
general_length_nth_tl
integer-nth-root
integer-nth-root-ext
integer-nth-root2
iseg-append-nth_tl
l_contains-nth_tl
length_nth_tl
member-nth-tl-implies-member
member_nth_tl
nth-better-fibs
nth-fibs
nth-nats
nth-rational
nth-rational_wf
nth-stream-map
nth-stream-zip
nth_tl
nth_tl-append
nth_tl-es-before
nth_tl-es-open-interval
nth_tl-partition
nth_tl_append
nth_tl_decomp
nth_tl_decomp_eq
nth_tl_factor
nth_tl_is_fseg
nth_tl_is_nil
nth_tl_map
nth_tl_nil
nth_tl_nth_tl
nth_tl_wf
poly-nth-deriv
poly-nth-deriv-req
poly-nth-deriv_wf
reject_eq_firstn_nth_tl
remove-nth
remove-nth_wf
rpoly-nth-deriv
rpoly-nth-deriv-linear
rpoly-nth-deriv_functionality
rpoly-nth-deriv_wf
s-nth
s-nth_wf
select-nth_tl
select_nth_tl
tl_nth_tl

NTHTL

prev top next

select-nthtl

NTHTL0

prev top next

select-nthtl0

NTUPLE

prev top next

ap2-tuple_wf_ntuple
map-tuple_wf_ntuple
tuple_wf_ntuple

NU

prev top next

ses-NU
ses-NU_wf

NULL

prev top next

A-null
A-null-loop
A-null-property
A-null_wf
DVp_Null
DVp_Null-x
DVp_Null-x_wf
DVp_Null?
DVp_Null?_wf
DVp_Null_wf
W-null
assert-bag-null
assert-bag-null-sq
assert-co-w-null
assert-fset-null
assert-null-base
assert_of_null
assert_of_oal_null
bag-combine-null
bag-map-null
bag-mapfilter-null
bag-member-not-bag-null
bag-null
bag-null-append
bag-null-bag-union
bag-null-filter
bag-null-rep
bag-null_wf
bag_null_cons_lemma
bag_null_empty_lemma
base-process-inputs-non-null
church-null
church-null_wf
church_null_nil_lemma
church_null_pair_lemma
co-w-null
co-w-null_wf
cons_iseg_not_null
disjoint-iff-null-intersection
es-le-before-not-null
es-prior-fixedpoints-non-null
eu-le-null-segment
eu-length-null-segment
eu-lt-null-segment
eu-lt-null-segment2
fpf-null-domain
fps-not-null
fset-null
fset-null_wf
hd-wf-not-null
iterate-null-process
last-concat-non-null
length_of_null_list
lifting-null-spread
member-implies-null-eq-bfalse
member_null
mset_for_null_lemma
mset_mem_null_lemma
non-null-list-tactic-test
non_null_filter
non_null_filter_iff
non_null_iff_length
null
null-bag
null-bag-empty
null-bag-filter-map
null-bag-mapfilter
null-bag-size
null-class
null-class-is-empty
null-class-program
null-class-program_wf
null-class-property
null-class_wf
null-data-stream
null-es-hist
null-filter
null-filter2
null-ite
null-map
null-mapfilter
null-process
null-process_wf
null-seq
null-seq_wf
null-strict
null-upto
null_append
null_cons_lemma
null_filter
null_functionality_wrt_permr
null_member
null_mset
null_mset_wf
null_mset_wf_f
null_nil_lemma
null_remove_leading
null_wf
null_wf2
null_wf3
oal_null
oal_null_wf
pcw-pp-null
pcw-pp-null_wf
pi-null-trans
pi-null-trans_wf
prior-vals-non-null
quicksort-int-null
single-bag-not-null
typed-null-ite

NULLSET

prev top next

not-nullset
nullset
nullset-monotone
nullset-union
nullset_wf

NUM

prev top next

archive-consensus-accum-num
consensus-accum-num
consensus-accum-num-archives
consensus-accum-num-property1
consensus-accum-num-property2
consensus-accum-num-property3
consensus-accum-num-state
consensus-accum-num-state_wf
consensus-accum-num_wf
num-antecedents
num-antecedents-fun_exp
num-antecedents-property
num-antecedents_wf
pv11_p1_Ballot_Num
pv11_p1_Ballot_Num_wf
pv11_p1_abs_Ballot_Num
pv11_p1_abs_Ballot_Num_wf
pv11_p1_init_ballot_num
pv11_p1_init_ballot_num_wf
pv11_p1_init_slot_num
pv11_p1_init_slot_num_wf
pv11_p1_rep_Ballot_Num
pv11_p1_rep_Ballot_Num_wf
triangular-num
triangular-num-add1
triangular-num-alt
triangular-num-le
triangular-num_wf

NUMBER

prev top next

natural_number def
natural_number_wf_p-outcome

NUMBERED

prev top next

es-interface-numbered
es-interface-numbered-def
es-interface-numbered_wf

NUMBERS

prev top next

strong-law-of-large-numbers

NUMERATOR

prev top next

rounded-numerator
rounded-numerator_wf

NUMITEMS

prev top next

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

NWKL

prev top next

fan-iff-nwkl!
fan-implies-nwkl!-using-PFan
nwkl!
nwkl!-iff-twkl!-bool
nwkl!-implies-fan
nwkl!_wf
wkl!-iff-nwkl!

NXT

prev top next

bind-nxt
bind-nxt_wf
rec-bind-nxt
rec-bind-nxt_wf
simple-bind-nxt
simple-bind-nxt_wf

NZERO

prev top

int_nzero
int_nzero_properties
int_nzero_wf
mem_iff_count_nzero
mset_mem_iff_count_nzero
mul_nzero
mul_wf_nzero
nat_plus_inc_int_nzero