[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]
F
top next
F-bisimulation
F-bisimulation_wf
comb_for_mset_inj_wf_f
decidable__f-subset
f-singleton-subset
f-subset
f-subset-union
f-subset_antisymmetry
f-subset_transitivity
f-subset_weakening
f-subset_wf
f-union
f-union-subset
f-union_wf
indexed-F-bisimulation
indexed-F-bisimulation_wf
is-max-f-class
list_in_mem_f_list
max-f-class
max-f-class-val
max-f-class_wf
mem_f
mem_f_wf
mem_iff_mem_f
member-f-union
member-f-union-aux
mset_diff_wf_f
mset_inj_wf_f
mset_inter_wf_f
mset_union_wf_f
null_mset_wf_f
perm_b_f_cancel
perm_b_to_f
perm_f
perm_f_b_cancel
perm_f_inj
perm_f_wf
FABGRP
prev top next
fabgrp
fabgrp_grp
fabgrp_grp_wf
fabgrp_inj
fabgrp_inj_wf
fabgrp_sig
fabgrp_sig_wf
fabgrp_umap
fabgrp_umap_wf
fabgrp_wf
FABMON
prev top next
fabmon_of_nat_mcp
fabmon_of_nat_mcp_wf
mk_fabmon
oal_fabmon
oal_fabmon_wf
FACE
prev top next
A-face
A-face-compatible
A-face-compatible-image
A-face-compatible_wf
A-face-image
A-face-image_wf
A-face-name
A-face-name-image
A-face-name_wf
A-face_wf
I-face
I-face_wf
assert-face-name-eq
cube-set-restriction-face-map
extend-face-map-same
extend-name-morph-face-map
extended-face-map
extended-face-map1
face-compatible
face-compatible-cubical-nerve1
face-compatible-image
face-compatible-symmetry
face-compatible_wf
face-cube
face-cube_wf
face-dimension
face-dimension_wf
face-direction
face-direction_wf
face-image
face-image_wf
face-map
face-map-comp
face-map-comp-id
face-map-comp-trivial
face-map-comp2
face-map-idempotent
face-map-property
face-map_wf
face-map_wf2
face-map_wf_fresh-cname
face-maps-commute
face-maps-comp
face-maps-comp-property
face-maps-comp_wf
face-name
face-name-eq
face-name-eq_wf
face-name-image
face-name_wf
get_face
get_face-dimension
get_face-direction
get_face-wf
get_face_image
get_face_unique
get_face_wf
iota-face-map
iota-two-face-maps
is-A-face
is-A-face_wf
is-face
is-face_wf
lift-id-face
lift-id-face_wf
lift-reduce-face-map
name-morph-extend-face-map
name-morph-flip-face-map
name-morph-flip-face-map1
nerve-box-common-face
nerve-box-common-face_wf
nerve-box-common-face_wf2
nerve-box-face
nerve-box-face_wf
poset_functor_extend-face-map
poset_functor_extend-face-map1
same-face-edge-arrows-commute
same-face-edge-arrows-commute0
same-face-edge-arrows-commute1
same-face-edge-arrows-commute2
same-face-edge-arrows-commute3
same-face-edge-arrows-commute4
same-face-square-commutes
same-face-square-commutes2
term-A-face
term-A-face_wf
FACES
prev top next
fills-A-faces
fills-A-faces_wf
fills-faces
fills-faces_wf
lift-id-faces
lift-id-faces-wf
lift-id-faces_wf
poset-functor-extends-box-faces
poset-functor-extends-box-faces-1
FACT
prev top next
divides-fact
exp-2-3-fact
fact
fact-bound
fact-greater-exp
fact-increasing
fact-non-decreasing
fact-non-zero
fact-positive
fact_unroll
fact_unroll_1
fact_wf
lapp_fact
lapp_fact_a
lapp_fact_b
mset_fact
oalist_fact
omral_fact
omral_fact_a
posint_fact_exists
super-fact
super-fact-int-prod-exp
super-fact-unroll
super-fact_wf
FACT0
prev top next
fact0_redex_lemma
FACTOR
prev top next
exp_difference_factor
firstn_factor
int-prod-factor
least-factor
least-factor_wf
nth_tl_factor
segment_factor
FACTORIAL
prev top next
accum-induction-factorial
cont-induction-factorial
equipollent-factorial
primrec-induction-factorial
rdiv-factorial-lemma1
rdiv-factorial-lemma2
rdiv-factorial-limit-zero
FACTORIT
prev top next
factorit
factorit_wf
FACTORIZATION
prev top next
factorization
factorization_wf
FACTORIZATIONS
prev top next
bag-member-two-factorizations
two-factorizations
two-factorizations-no-repeats
two-factorizations_wf
FACTORS
prev top next
append-factors
divides-iff-factors
factors
factors-prime-product
factors_wf
norm-factors
norm-factors_wf
prime-factors
prime-factors-unique
product-factors
FACTORS2
prev top next
prime-factors2
FACTORS3
prev top next
prime-factors3
FACTS
prev top next
W-elimination-facts
FADD
prev top next
fadd
fadd_increasing
fadd_wf
FAIL
prev top next
es-class-causal-mrel-fail
es-class-causal-mrel-fail_wf
es-class-causal-rel-fail
es-class-causal-rel-fail_wf
es-class-mcast-fail
es-class-mcast-fail_wf
es-class-reply-or-fail
es-class-reply-or-fail_wf
FAILS
prev top next
lookup_fails
FAILURE
prev top next
failure-known
failure-known-causle
failure-known-effective
failure-known_wf
oar-failure-model
oar-failure-model_wf
FAITHFUL
prev top next
full-faithful-functor
full-faithful-functor
full-faithful-functor_wf
full-faithful-functor_wf
FALSE
prev top next
alle-between1-false
alle-between2-false
alle-between3-false
and_false_l
and_false_r
bm_compare_greater_greater_false
bm_compare_less_less_false
bool_sim_false
church-false
church-false_wf
church_ite_false_lemma
decidable__false
eq_atom_eq_false_elim
eq_atom_eq_false_elim_sqequal
eq_int_eq_false
eq_int_eq_false_elim
eq_int_eq_false_elim_sqequal
eq_int_eq_false_intro
existse-between1-false
existse-between2-false
existse-between3-false
false
false-using-ispair-cases
false_wf
ifthenelse-false-left
ifthenelse-false-right
ite_false
ite_rw_false
known_false
known_not_false
lt_int_eq_false_elim
lt_int_eq_false_elim_sqequal
mon_when_false
not-false
or_false_l
or_false_r
sq_stable_and_left_false
squash_false
unsquashed-weak-continuity-base-false
unsquashed-weak-continuity-false
FAMILY
prev top next
Spread-family
Spread-family-ext
Spread-family_wf
base-type-family
base-type-family-implies
base-type-family_wf
corec-family
corec-family-ext
corec-family-wf2
corec-family_wf
corec-sub-family
csm-cubical-pi-family
cu-cube-family
cu-cube-family-Kan-type-at
cu-cube-family-comp
cu-cube-family_wf
cubical-pi-family
cubical-pi-family-comp
cubical-pi-family_wf
ext-family
ext-family-iff
ext-family_wf
family-monotone
family-monotone_wf
interleaved_family
interleaved_family_occurence
interleaved_family_occurence_wf
interleaved_family_wf
isect-family
isect-family-wf2
isect-family_wf
per-function_wf_base_family
sub-corec-family
sub-family
sub-family_transitivity
sub-family_wf
sub-isect-family
type-family-continuous
type-family-continuous_wf
FAN
prev top next
Coquand-fan-theorem
fan
fan+weak-continuity-implies-uniform-continuity
fan-iff-dfan-bool
fan-iff-nwkl!
fan-iff-wkl!
fan-implies-PFan
fan-implies-bar-sep
fan-implies-barred-not-unbounded
fan-implies-nwkl!-using-PFan
fan-realizer
fan-realizer_test
fan-realizer_test2
fan-realizer_wf
fan-theorem
fan_theorem
fan_theorem-ext
fan_wf
nwkl!-implies-fan
simple-fan-theorem
simple_fan_theorem
simple_fan_theorem-ext
unit-interval-fan
unit-interval-fan_wf
FAPPEND
prev top next
fappend
fappend_wf
FAST
prev top next
bag-mapfilter-fast
bag-mapfilter-fast-eq
bag-mapfilter-fast-eq2
bag-mapfilter-fast-map
bag-mapfilter-fast_wf
fast-fib
fast-fib-ext
fast-mapfilter
fast-mapfilter_wf
fast-rsqrt
less-fast-fib
less-fast-fib-ext
mapfilter-as-fast-mapfilter
reduce-fast-mapfilter1
reduce-fast-mapfilter2
FASTEXP
prev top next
exp-fastexp
fastexp
fastexp_wf
FASTFIB
prev top next
fastfib
FB
prev top next
cantor-to-fb
cantor-to-fb_wf
fb-to-cantor
fb-to-cantor_wf
FERMAT
prev top next
Euler-Fermat
fermat-little
fermat-little2
FETCH
prev top next
A-fetch
A-fetch'
A-fetch'_wf
A-fetch_wf
coerce-fetch'-commutes
fetch'-commutes
FETCH2
prev top next
A-fetch2
A-fetch2_wf
FF
prev top next
assert_of_ff
band_ff_simp
bnot-ff
bool-tt-or-ff
bor_ff_simp
eq_bool_ff
priority-select-ff
sqequal-ff-to-assert
FFOR
prev top next
ffor
ffor_wf
FIB
prev top next
comb_for_fib_wf
fast-fib
fast-fib-ext
fib
fib-exists
fib_coprime
fib_wf
less-fast-fib
less-fast-fib-ext
FIBS
prev top next
better-fibs
better-fibs-equal-map
better-fibs_wf
fibs
fibs-equal-map
fibs_wf
nth-better-fibs
nth-fibs
FIELD
prev top next
C_field_of
C_field_of_wf
C_type_of_field
C_type_of_field_wf
any_field_is_integ_dom
field
field_p
field_p_wf
field_wf
rel_plus_field
restriction-to-field
wellfounded-minimal-field
FIELDS
prev top next
C_Struct-fields
C_Struct-fields_wf
FIFO
prev top next
fifo-information-flow
fifo-information-flow_wf
interface-fifo
interface-fifo_wf
strong-interface-fifo
strong-interface-fifo-order-preserving
strong-interface-fifo_wf
FILLER
prev top next
Kan-A-filler
Kan-A-filler_wf
Kan-filler
Kan-filler_wf
Kan_id_filler
Kan_id_filler_uniform
Kan_id_filler_wf
Kan_id_filler_wf1
Kan_sigma_filler
Kan_sigma_filler_uniform
Kan_sigma_filler_wf
cu-cube-filler
cu-cube-filler-fills
cu-cube-filler-uniform
cu-cube-filler_wf
cu-filler-cases
cu_filler_1
cu_filler_1_wf
cu_filler_2
cubical-interval-filler
cubical-interval-filler-fills
cubical-interval-filler_wf
groupoid-nerve-filler
groupoid-nerve-filler-fills
groupoid-nerve-filler-uniform
groupoid-nerve-filler_wf
sq_stable_Kan-A-filler
sq_stable_uniform-Kan-A-filler
uniform-Kan-A-filler
uniform-Kan-A-filler_wf
uniform-Kan-filler
uniform-Kan-filler_wf
FILLER0
prev top next
groupoid-nerve-filler0
groupoid-nerve-filler0_wf
FILLER1
prev top next
groupoid-nerve-filler1
groupoid-nerve-filler1_wf
FILLER2
prev top next
groupoid-nerve-filler2
groupoid-nerve-filler2_wf
FILLS
prev top next
cu-cube-filler-fills
cubical-interval-filler-fills
fills-A-faces
fills-A-faces_wf
fills-A-open-box
fills-A-open-box_wf
fills-faces
fills-faces_wf
fills-open_box
fills-open_box_wf
groupoid-nerve-filler-fills
sq_stable_fills-A-open-box
FILTER
prev top next
accum_filter_rel
accum_filter_rel_nil
accum_filter_rel_wf
agree_on_common_filter
assert-is-filter-image
bag-bind-filter
bag-combine-filter
bag-count-filter
bag-filter
bag-filter-append
bag-filter-as-accum
bag-filter-combine
bag-filter-combine2
bag-filter-empty
bag-filter-empty-iff
bag-filter-equal
bag-filter-filter
bag-filter-filter2
bag-filter-is-empty
bag-filter-is-nil
bag-filter-is-sub-bag
bag-filter-map
bag-filter-map2
bag-filter-no-repeats
bag-filter-no-repeats2
bag-filter-same
bag-filter-singleton
bag-filter-split
bag-filter-trivial
bag-filter-trivial2
bag-filter-union
bag-filter-union2
bag-filter-wf2
bag-filter-wf3
bag-filter_wf
bag-map-filter
bag-member-filter
bag-member-filter-implies1
bag-member-filter-implies2
bag-member-filter-set
bag-no-repeats-filter
bag-null-filter
bag-remove-repeats-filter
bag-size-filter-member-bound
bag-summation-filter
bag_filter_cons_lemma
bag_filter_empty_lemma
bl-exists-filter
can-apply-p-co-filter
can-apply-p-filter
causal_order_filter_iseg
collect_filter
collect_filter-wf2
collect_filter_accum_fun
collect_filter_accum_fun_wf
collect_filter_wf
count-as-filter
count-length-filter
decidable-filter
deq-member-length-filter
do-apply-p-co-filter
do-apply-p-filter
equipollent-filter
es-E-filter-image
es-filter-image
es-filter-image-val
es-filter-image-val2
es-filter-image_wf
es-interface-filter
es-interface-filter-val
es-interface-filter_wf
es-is-filter-image
es-is-filter-image2
es-is-interface-filter
es-le-before-filter
filter
filter-as-accum-aux
filter-as-accum-aux2
filter-as-mapfilter
filter-commutes
filter-concat
filter-cons
filter-equal
filter-equals
filter-filter
filter-filter2
filter-for-max
filter-fpf-vals
filter-image-interface-accum-equal
filter-image_functionality
filter-index
filter-index_wf
filter-interface-predecessors-first-at
filter-interface-predecessors-lower-bound
filter-interface-predecessors-lower-bound-implies
filter-interface-predecessors-lower-bound2
filter-interface-predecessors-lower-bound3
filter-le
filter-less
filter-list-diff
filter-map
filter-nil
filter-normal-form
filter-reverse
filter-singleton
filter-split-length
filter-sq
filter-upto-length
filter-vote-with-ballot-lemma
filter_append
filter_append_sq
filter_before
filter_cons_lemma
filter_filter
filter_filter2
filter_filter_reduce
filter_fseg
filter_functionality
filter_functionality_wrt_permutation
filter_interleaving
filter_interleaving_occurence
filter_is_empty
filter_is_interleaving
filter_is_nil
filter_is_nil2
filter_is_nil3
filter_is_nil_implies
filter_is_nil_implies2
filter_is_singleton
filter_is_singleton2
filter_is_sublist
filter_iseg
filter_iseg2
filter_map
filter_map_upto
filter_map_upto2
filter_nil_lemma
filter_of_filter2
filter_safety
filter_strong_safety
filter_sublist
filter_trivial
filter_trivial2
filter_tt
filter_type
filter_type2
filter_wf
filter_wf2
filter_wf3
filter_wf4
filter_wf4_2
filter_wf5
filter_wf_top
find-hd-filter
first-at-filter-interface-predecessors
first-at-filter-interface-predecessors-or
first-at-filter-interface-predecessors1
firstn-filter
fset-filter
fset-filter_wf
fset-filter_wf2
hd-filter
imax-list-filter-member
implies-filter-equal
interface-predecessors-filter-image
interleaving_as_filter
interleaving_as_filter_2
is-filter-image-sq
iseg-as-filter
iseg-filter-es-interval
iseg-remainder-as-filter
iseg_filter
iseg_filter_last
l-ordered-filter
l_all_filter
l_before-filter
l_before_filter
l_before_filter_set_type
l_before_filter_subtype
l_member-iff-length-filter
length-filter
length-filter-bnot
length-filter-decreases
length-filter-le
length-filter-lower-bound
length-filter-pos
length_filter
lg-filter
lg-filter_wf
list-to-set-filter
list_accum_filter
loc-ordered-filter
map-concat-filter-lemma1
map-concat-filter-lemma2
map-filter
map-filter-proof2
member-filter
member-filter-witness
member-filter-witness_wf
member-fset-filter
member_filter
member_filter_2
member_map_filter
no_repeats_filter
non_null_filter
non_null_filter_iff
null-bag-filter-map
null-filter
null_filter
p-co-filter
p-co-filter_wf
p-filter
p-filter_wf
pairwise-filter
permutation-filter
poset-cat-arrow-filter-nil
remove-repeats-filter
remove-repeats-fun-as-filter
s-filter
s-filter_wf
single-valued-bag-filter
sorted-by-filter
sorted-filter
sub-bag-filter
sublist*_filter
sublist_filter
sublist_filter_2
sublist_filter_set_type
sum-as-accum-filter
sv-bag-only-filter
swap-filter-filter
sys-antecedent-filter-image
test-bag-filter-empty
FILTER0
prev top next
l_sum_filter0
FILTER1
prev top next
last-filter1
FILTER2
prev top next
bag-filter-filter2
bag-member-filter2
cons_filter2
deq-member-length-filter2
filter-filter2
filter2
filter2_functionality
filter2_nil_lemma
filter2_wf
filter_filter2
filter_of_filter2
interleaving_filter2
iseg_filter2
l-ordered-filter2
member_filter2
no_repeats_filter2
null-filter2
sub-bag-filter2
FILTER3
prev top next
member-filter3
sub-bag-filter3
FIN
prev top next
fin_type
fin_type_inc
fin_type_properties
fin_type_wf
FINAL
prev top next
final-iterate
final-iterate-property
final-iterate_wf
pcw-final-step
pcw-final-step_wf
same-final-iterate-one-one
ts-final
ts-final_wf
FIND
prev top next
bm_find
bm_find_wf
can-find-first
can-find-first-ext
can-find-first1-ext
can-find-first2
find
find-combine
find-combine-cons
find-combine-nil
find-combine_wf
find-first
find-first_wf
find-ge
find-ge_wf
find-hd-filter
find-maximal-consecutive
find-maximal-consecutive_wf
find-random
find-random_wf
find-real-neq
find-real-neq2
find-xover
find-xover-print
find-xover_wf
find_property
find_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
l_find
l_find_wf
lookup-list-map-find
lookup-list-map-find_wf
map-sig-find
map-sig-find_wf
quick-find
quick-find_wf
FINITE
prev top next
cardinality-le-finite
compact-finite
decidable-exists-finite
decidable-exists-finite-type
decidable-finite-cantor
decidable-finite-cantor-ext
decidable-finite-cantor-to-int
decidable__i-finite
decidable__inject-finite-type
decidable__rel_exp_finite
finite
finite-acyclic-rel
finite-cantor-decider
finite-cantor-decider_wf
finite-decidable-set
finite-deriv-seq
finite-deriv-seq_wf
finite-double-negation-shift
finite-double-negation-shift-extract
finite-function-equipollent
finite-function-equipollent-tuple
finite-function-type-equality
finite-injection
finite-max
finite-partition
finite-partition-property
finite-prob-space
finite-prob-space_wf
finite-run-lt
finite-run-pred
finite-sequence-coding-exists
finite-set-type
finite-set-type-cases
finite-subtype
finite-type
finite-type-bool
finite-type-equipollent
finite-type-iff-list
finite-type-implies-finite
finite-type-int_seg
finite-type-list
finite-type-product
finite-type-union
finite-type-unit
finite-type_wf
finite_functionality_wrt_equipollent
finite_set
finite_set_wf
finite_wf
i-approx-finite
i-closed-finite-rep
i-finite
i-finite_wf
i-member-finite
i-member-finite-closed
locally-non-zero-finite-deriv-seq
nsub_finite
rel_finite
rel_finite-restrict
rel_finite_wf
simple-decidable-finite-cantor
simple-decidable-finite-cantor-ext
simple-finite-cantor-decider
simple-finite-cantor-decider_wf
surjection-cantor-finite-branching
FIRST
prev top next
Q-R-glued-first
alist-domain-first
alle-at-not-first
alle-between1-not-first-since
alle-between2-not-first-since
assert-eo-forward-first
assert-es-first
assert-es-first-locl
bl-exists-first
bm_first
bm_first_wf
but-first-class
but-first-class_wf
can-apply-p-first
can-find-first
can-find-first-ext
do-apply-p-first
do-apply-p-first-disjoint
eager_first
eo-forward-first
eo-forward-first-trivial
eo-forward-not-first
eo-strict-forward-first
es-E-interface-first
es-E-interface-first-class
es-before-is-nil-if-first
es-first
es-first-at
es-first-at-exists
es-first-at-exists-cases
es-first-at-exists2
es-first-at-implies
es-first-at-implies-first-at
es-first-at-since
es-first-at-since'
es-first-at-since'_wf
es-first-at-since-iff
es-first-at-since_wf
es-first-at-unique
es-first-at_wf
es-first-before
es-first-before2
es-first-event
es-first-event_wf
es-first-exists
es-first-implies
es-first-init
es-first-le
es-first-since
es-first-since_functionality_wrt_iff
es-first-since_wf
es-first-unique
es-first_wf
es-first_wf2
es-interface-history-first
es-is-interface-p-first
es-le-before-if-first
es-le-first
es-locl-first
es-pplus-first-since
es-pplus-first-since-exit
expectation-monotone-in-first
filter-interface-predecessors-first-at
find-first
find-first_wf
first-25-rationals
first-at-filter-interface-predecessors
first-at-filter-interface-predecessors-or
first-at-filter-interface-predecessors1
first-choosable
first-choosable-property
first-choosable-property2
first-choosable_wf
first-class
first-class-val
first-class_wf
first-eclass
first-eclass-val
first-eclass_wf
first-event
first-event-property
first-event_wf
first-interface-implies-prior-interface
first-iseg
first-member
first-member-cons
first-member-iff
first-member_wf
first_index
first_index-positive
first_index_bounds
first_index_cons
first_index_equal
first_index_property
first_index_wf
global-eo-first
glued-first
hd-es-le-before-is-first
in-first-eclass
is-first-class
is-first-class2
l-first
l-first-when-none
l-first_wf
l_member-first
length-remove-first
length-remove-first-le
list-eo-first
mk_lambdas-fun-unroll-first
mk_lambdas_fun-unroll-first
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
no_repeats-remove-first
on-first-class
on-first-class_wf
p-conditional-to-p-first
p-first
p-first-append
p-first-cons
p-first-singleton
p-first_wf
p_first_nil_lemma
prior-val-first
ranked-eo-first
remove-first
remove-first-cons
remove-first-member-implies
remove-first-no_repeats-member
remove-first_wf
rsum-split-first
rv-disjoint-monotone-in-first
select-remove-first
send-first-class
send-first-class_wf
skip-first-class
skip-first-class-is-empty-if-first
skip-first-class-property
skip-first-class-property-iff
skip-first-class_wf
split-at-first
split-at-first-gap
split-at-first-gap-ext
split-at-first-rel
strict-majority-or-first
strict-majority-or-first_wf
sum_split_first
test-es-first-reasoning
the-first-event
FIRST0
prev top next
first0
FIRST1
prev top next
can-find-first1-ext
FIRST2
prev top next
can-find-first2
eo-forward-first2
eo-forward-not-first2
permutation-swap-first2
FIRSTI
prev top next
bm_firsti
bm_firsti_wf
FIRSTN
prev top next
append_firstn_lastn
append_firstn_lastn_sq
comb_for_firstn_wf
deq-member-firstn
firstn
firstn-append
firstn-before
firstn-data-stream
firstn-es-open-interval
firstn-filter
firstn-iseg
firstn-le-before
firstn-mklist
firstn-mklist1
firstn-partition
firstn_all
firstn_append
firstn_append_front
firstn_append_front_singleton
firstn_decomp
firstn_decomp2
firstn_factor
firstn_firstn
firstn_is_iseg
firstn_last
firstn_last_mklist
firstn_last_mklist_sq
firstn_last_sq
firstn_length
firstn_map
firstn_map_upto
firstn_nth_tl
firstn_nth_tl_decomp
firstn_upto
firstn_wf
iseg-iff-firstn
l_contains-firstn
length_firstn
length_firstn_eq
member-firstn
member-firstn-implies-member
member_firstn
no_repeats-firstn
reject_eq_firstn_nth_tl
select-firstn
select_firstn
FIVE
prev top next
eu-colinear-five-segment
eu-five-segment
eu-inner-five-segment
FIX
prev top next
bottom-sqequal-fix-id
colist-fix-ap-partial
colist-fix-partial
es-fix
es-fix-cases
es-fix-causl
es-fix-causle
es-fix-connected
es-fix-equal
es-fix-equal-E-interface
es-fix-fun-exp
es-fix-last-prior-fixedpoints
es-fix-order-preserving
es-fix-sqequal
es-fix-step
es-fix-test
es-fix-unique
es-fix_property
es-fix_property2
es-fix_wf
es-fix_wf2
es-fix_wf_antecedent
es-prior-fixedpoints-fix
fix
fix def
fix-connected
fix-corec-partial1
fix-diverges
fix-not-exception
fix-of-add
fix-of-id
fix-step
fix-strict
fix_property
fix_strict_diverge
fix_wf
fix_wf1
fix_wf_bar
fix_wf_corec
fix_wf_corec-alt-proof
fix_wf_corec-partial1
fix_wf_corec1
fix_wf_corec2
fix_wf_corec2'
fix_wf_corec_3parameter
fix_wf_corec_parameter
fix_wf_corec_parameter2
fix_wf_corec_parameter3
fix_wf_corec_partial_nat
fix_wf_corec_system
fix_wf_dataflow
fix_wf_dataflow_w_state
has-value-equality-fix
has-value-equality-fix-bar
list_ind-as-fix
member-es-fix-prior-fixedpoints
special-fix
sqequal-fix-lemma1
strictness-fix
FIXED
prev top next
es-prior-fixedpoints-fixed
FIXEDPOINT
prev top next
fun-connected-fixedpoint
fun-path-fixedpoint
fun_exp-fixedpoint
retraction-fixedpoint
sys-antecedent-fixedpoint
urec-is-fixedpoint
urec-is-least-fixedpoint
FIXEDPOINTS
prev top next
eqmod-prime-order-fixedpoints
es-fix-last-prior-fixedpoints
es-prior-fixedpoints
es-prior-fixedpoints-causle
es-prior-fixedpoints-fix
es-prior-fixedpoints-fixed
es-prior-fixedpoints-iseg
es-prior-fixedpoints-no_repeats
es-prior-fixedpoints-non-null
es-prior-fixedpoints-unequal
es-prior-fixedpoints_wf
member-es-fix-prior-fixedpoints
FIXPOINT
prev top next
fixpoint-induction
fixpoint-induction-bottom
fixpoint-induction-bottom-bar
fixpoint-induction-bottom-base
fixpoint-induction-bottom2
fixpoint-induction2
fixpoint-upper-bound
fixpoint_ub
near-fixpoint-on-0-1
FLIP
prev top next
combine-list-flip
cycle-flip-lemma
eu-congruent-flip
eu-congruent-flip-seg
eu-length-flip
flip
flip-adjacent
flip-conjugate-rotate
flip-conjugation
flip-conjugation1
flip-generators
flip-injection
flip_bijection
flip_identity
flip_inverse
flip_symmetry
flip_twice
flip_wf
groupoid-nerve-functor-flip
name-comp-flip
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
nsub2-flip
poset-cat-arrow-flip
poset-cat-dist-flip
poset_functor_extend-flip
FLIPS
prev top next
compose-flips
compose-flips_wf
cycle-as-flips
name-morph-flips-commute
FLOOR
prev top next
div_floor
div_floor_mod_sum
div_floor_wf
FLOW
prev top next
convergent-flow
convergent-flow-order-preserving
convergent-flow_wf
fifo-information-flow
fifo-information-flow_wf
flow-allowed
flow-graph
flow-graph-information-flow-relation
flow-graph_wf
flow-state-compression
flow-state-compression_wf
glues-via-flow-lemma1
information-flow
information-flow-relation
information-flow-relation_wf
information-flow-to
information-flow-to_wf
information-flow_wf
ses-flow
ses-flow-axiom
ses-flow-axiom-ordering
ses-flow-axiom_wf
ses-flow-causle
ses-flow-has
ses-flow-has*
ses-flow-implies
ses-flow-implies'
ses-flow-induction
ses-flow_wf
ses-info-flow
ses-info-flow-exp_functionality
ses-info-flow_functionality
ses-info-flow_wf
solves-information-flow
solves-information-flow_wf
tree-flow
tree-flow-convergent
tree-flow-order-preserving
tree-flow_wf
FMA
prev top next
fma_alg
fma_alg_wf
fma_from_gcp
fma_from_gcp_wf
fma_inj
fma_inj_wf
fma_sig
fma_sig_wf
fma_umap
fma_umap_wf
omral_fma
omral_fma_wf
omral_fma_wf2
FMAP
prev top next
mset_mem_fmap
FMON
prev top next
mset_fmon
mset_fmon_wf
FMONALG
prev top next
fmonalg
fmonalg_properties
fmonalg_wf
FN
prev top next
fn_array
fn_array_wf
FND
prev top next
lexico_well_fnd
pair-lex_well_fnd
posint_well_fnd
product_well_fnd
FO
prev top next
fo-logic-test1
fo-logic-test2
fo-logic-xmiddle
FOASSIGNMENT
prev top next
FOAssignment
FOAssignment_wf
FOCONNECTIVE
prev top next
FOConnective
FOConnective_wf
FOLDL
prev top next
bm_foldl
bm_foldl_wf
FOLDLI
prev top next
bm_foldli
bm_foldli_aux
bm_foldli_aux_wf
bm_foldli_wf
FOO
prev top next
RankEx4_Foo
RankEx4_Foo-foo
RankEx4_Foo-foo_wf
RankEx4_Foo?
RankEx4_Foo?_wf
RankEx4_Foo_wf
foo
vr_test_foo_bar345566
vr_test_foo_bar345566546
FOQUANTIFIER
prev top next
FOQuantifier
FOQuantifier_wf
FOR
prev top next
Editor aliases for Constructive Geometry
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
OARcast_orderer_for_sender
OARcast_orderer_for_sender_outputs
OARcast_orderer_for_sender_outputs_wf
OARcast_orderer_for_sender_wf
Rice-theorem-for-Type_1
Rice-theorem-for-Type_2
Rice-theorem-for-Type_3
Tactics for Constructive Geometry
comb_for_absval_wf
comb_for_app_permf_wf
comb_for_append_wf
comb_for_assert_wf
comb_for_assoced_wf
comb_for_b2i_wf
comb_for_ball_wf
comb_for_band_wf
comb_for_before_wf
comb_for_bimplies_wf
comb_for_bnot_wf
comb_for_bor_wf
comb_for_choose_wf
comb_for_comp_perm_wf
comb_for_compose_wf
comb_for_compose_wf_for_mon_hom
comb_for_cons_wf_listp
comb_for_coprime_wf
comb_for_count_wf
comb_for_divides_wf
comb_for_eqmod_wf
comb_for_extend_perm_wf
comb_for_extend_permf_wf
comb_for_fib_wf
comb_for_firstn_wf
comb_for_fun_exp_wf
comb_for_gcd_p_wf
comb_for_gcd_wf
comb_for_ge_wf
comb_for_grp_car_wf
comb_for_grp_leq_wf
comb_for_grp_lt_wf
comb_for_gt_wf
comb_for_hd_wf_listp
comb_for_iff_wf
comb_for_ifthenelse_wf
comb_for_imax_wf
comb_for_imin_wf
comb_for_int_op_wf
comb_for_int_seg_wf
comb_for_int_upper_wf
comb_for_interleaving_wf
comb_for_iseg_wf
comb_for_itop_wf
comb_for_l_all_wf
comb_for_l_member_wf
comb_for_l_succ_wf
comb_for_le_wf
comb_for_length_wf1
comb_for_length_wf2
comb_for_listify_wf
comb_for_lookup_wf
comb_for_lt_int_wf
comb_for_map_wf
comb_for_massoc_wf
comb_for_mdivides_wf
comb_for_mem_wf
comb_for_mk_mset_wf
comb_for_mk_mset_wf2
comb_for_mk_perm_wf
comb_for_mk_perm_wf_a
comb_for_mod_mssum_wf
comb_for_mon_for_wf
comb_for_mon_itop_wf
comb_for_mon_nat_op_wf
comb_for_mon_nat_op_wf2
comb_for_mon_reduce_wf
comb_for_mon_when_wf
comb_for_mset_count_wf
comb_for_mset_for_wf
comb_for_mset_inj_wf
comb_for_mset_inj_wf_f
comb_for_mset_map_wf
comb_for_mset_mem_wf
comb_for_mset_sum_wf
comb_for_nat_op_wf
comb_for_ndiff_wf
comb_for_not_wf
comb_for_nth_tl_wf
comb_for_oal_bpos_wf
comb_for_oal_inj_wf
comb_for_omral_action_wf
comb_for_omral_inj_wf
comb_for_perm_igrp_wf
comb_for_perm_sig_wf
comb_for_perm_wf
comb_for_permr_wf
comb_for_pi1_wf
comb_for_reduce2_wf
comb_for_remainder_wf
comb_for_remove1_wf
comb_for_rev_implies_wf
comb_for_rng_mssum_wf
comb_for_rng_nat_op_wf
comb_for_rng_nexp_wf
comb_for_rng_sum_wf
comb_for_rng_when_wf
comb_for_sd_ordered_wf
comb_for_segment_wf
comb_for_set_blt_wf
comb_for_sublist_wf
comb_for_swap_wf
comb_for_txpose_perm_wf
comb_for_wellfounded_wf
compose_wf_for_mon_hom
dist_hom_over_mon_for
dist_hom_over_mset_for
filter-for-max
for
for_cons_lemma
for_hdtl
for_hdtl_cons_lemma
for_hdtl_nil_lemma
for_hdtl_wf
for_nil_lemma
for_wf
fset_for_when_eq
fset_for_when_unique
length_mon_for_char
member-values-for-distinct
member-values-for-distinct2
mon_for
mon_for_append
mon_for_cons_lemma
mon_for_eq_itop
mon_for_functionality_wrt_permr
mon_for_map
mon_for_nil_lemma
mon_for_of_id
mon_for_of_op
mon_for_swap
mon_for_wf
mon_for_when_none
mon_for_when_swap
mon_for_when_unique
mset_count_bound_for_union
mset_for
mset_for_dom_shift
mset_for_elim_lemma
mset_for_functionality
mset_for_functionality_wrt_bsubmset
mset_for_inj_lemma
mset_for_mset_inj
mset_for_mset_sum
mset_for_null_lemma
mset_for_of_id
mset_for_of_op
mset_for_swap
mset_for_wf
mset_for_when_dom_shift
mset_for_when_none
mset_for_when_unique
mset_mem_mon_for_union
mset_mon_for_elim
rng_fset_for_when_eq
tidentity_wf_for_mon_hom
type_inj_wf_for_qrng
type_inj_wf_for_quot
values-for-distinct
values-for-distinct-nil
values-for-distinct-property
values-for-distinct_wf
FORALL
prev top next
forall
forall_wf
FOREST
prev top next
MMTree_Node-forest
MMTree_Node-forest_wf
FORKABLE
prev top next
forkable-process
forkable-process_wf
FORKING
prev top next
non-forking
non-forking-rel_exp
non-forking-wellfounded-linorder
non-forking_wf
FORM
prev top next
append-normal-form
filter-normal-form
id-member-normal-form
kind-member-normal-form
length-normal-form
rational-form-has-value
remove-repeats-normal-form
FORMATION
prev top next
grp_hom_formation
FORMERS
prev top next
Rules of MLTT type formers
Rules of MLTT without type formers
FORMULA
prev top next
choose-formula
combinations-formula
formula
formula-definition
formula-ext
formula-induction
formula_ind
formula_ind_wf
formula_ind_wf_simple
formula_size
formula_size_wf
formula_wf
mFOL-proveable-formula
mFOL-proveable-formula-evidence
mFOL-proveable-formula-evidence-ext
mFOL-proveable-formula-evidence-ext2
mFOL-proveable-formula_wf
FORMULACO
prev top next
formulaco
formulaco-ext
formulaco_size
formulaco_size_wf
formulaco_wf
FORSOME
prev top next
forsome
forsome_wf
FORWARD
prev top next
assert-eo-forward-first
eo-forward
eo-forward-E
eo-forward-E-member
eo-forward-E-subtype
eo-forward-E-subtype2
eo-forward-alle-lt
eo-forward-base-E
eo-forward-base-classfun
eo-forward-base-classfun-res
eo-forward-base-classfun-res-sq
eo-forward-base-classfun-sq
eo-forward-base-classrel
eo-forward-base-pred
eo-forward-before
eo-forward-ble
eo-forward-bless
eo-forward-causl
eo-forward-causle
eo-forward-causle-implies
eo-forward-eq
eo-forward-equal-info-body
eo-forward-first
eo-forward-first-trivial
eo-forward-first2
eo-forward-forward
eo-forward-forward2
eo-forward-has-es-info-type
eo-forward-header
eo-forward-info
eo-forward-info-body
eo-forward-info-type
eo-forward-interval
eo-forward-le
eo-forward-le-before
eo-forward-le-subtype
eo-forward-le2
eo-forward-less
eo-forward-loc
eo-forward-locl
eo-forward-member-eclass
eo-forward-no-classrel-in-interval
eo-forward-no-prior-classrel
eo-forward-not-first
eo-forward-not-first2
eo-forward-pred
eo-forward-pred?
eo-forward-split-before
eo-forward-trivial
eo-forward-wf
eo-forward_wf
eo-strict-forward
eo-strict-forward-E
eo-strict-forward-E-member
eo-strict-forward-E-subtype
eo-strict-forward-E-subtype2
eo-strict-forward-base-E
eo-strict-forward-before
eo-strict-forward-ble
eo-strict-forward-bless
eo-strict-forward-eq
eo-strict-forward-first
eo-strict-forward-info
eo-strict-forward-le
eo-strict-forward-less
eo-strict-forward-loc
eo-strict-forward-locl
eo-strict-forward-pred
eo-strict-forward-pred?
eo-strict-forward_wf
equal-eo-forward-E
equal-eo-strict-forward-E
es-closed-open-interval-forward
es-init-forward
member-eo-forward-E
member-eo-strict-forward-E
new_23_sig_quorum_state_eq1-forward
new_23_sig_vote_with_ballot-forward
new_23_sig_vote_with_ballot_and_id-forward
new_23_sig_vote_with_ballot_first-assert-forward
new_23_sig_vote_with_ballot_first-forward
pv11_p1_valid-proposal-forward
pv11_p1_valid-proposal-transitivity-forward
strong-subtype-eo-forward-E
FORWARD2
prev top next
eo-forward-forward2
new_23_sig_vote_with_ballot_first-assert-forward2
FOSATWITH
prev top next
FOSatWith
FOSatWith_wf
FOSTRUCT
prev top next
FOStruct
FOStruct_wf
FOUNDED
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_uwell_founded
int_upper_well_founded
lg-acyclic-well-founded
locally-ranked-is-well-founded
nat_well_founded
power-set-lift-well-founded-implies
well-founded-run-lt
well-founded-run-pred
FOURTH
prev top next
expectation-rv-add-fourth
FPF
prev top next
ap_fpf_restrict_lemma
assert-fpf-is-empty
compose-fpf
compose-fpf-dom
compose-fpf_wf
domain_fpf_restrict_lemma
filter-fpf-vals
fpf
fpf-accum
fpf-accum_wf
fpf-add-single
fpf-add-single_wf
fpf-all
fpf-all-empty
fpf-all-join-decl
fpf-all-single
fpf-all-single-decl
fpf-all_wf
fpf-ap
fpf-ap-compose
fpf-ap-equal
fpf-ap-single
fpf-ap_functionality
fpf-ap_wf
fpf-as-apply-alist
fpf-cap
fpf-cap-compatible
fpf-cap-join-subtype
fpf-cap-join-subtype2
fpf-cap-single
fpf-cap-single-join
fpf-cap-single1
fpf-cap-subtype_functionality
fpf-cap-subtype_functionality_wrt_sub
fpf-cap-subtype_functionality_wrt_sub2
fpf-cap-void-subtype
fpf-cap-wf-univ
fpf-cap_functionality
fpf-cap_functionality_wrt_sub
fpf-cap_wf
fpf-compatible
fpf-compatible-join
fpf-compatible-join-cap
fpf-compatible-join-iff
fpf-compatible-join2
fpf-compatible-mod
fpf-compatible-mod_wf
fpf-compatible-self
fpf-compatible-single
fpf-compatible-single-iff
fpf-compatible-single2
fpf-compatible-singles
fpf-compatible-singles-iff
fpf-compatible-singles-trivial
fpf-compatible-symmetry
fpf-compatible-triple
fpf-compatible-update
fpf-compatible-update2
fpf-compatible-update3
fpf-compatible-wf2
fpf-compatible_monotonic
fpf-compatible_monotonic-guard
fpf-compatible_wf
fpf-compose
fpf-compose_wf
fpf-const
fpf-const-dom
fpf-const_wf
fpf-contains
fpf-contains-union-join-left2
fpf-contains-union-join-right2
fpf-contains_self
fpf-contains_wf
fpf-conversion-test
fpf-decompose
fpf-disjoint-compatible
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-domain
fpf-domain-join
fpf-domain-union-join
fpf-domain_wf
fpf-domain_wf2
fpf-empty
fpf-empty-compatible-left
fpf-empty-compatible-right
fpf-empty-join
fpf-empty-sub
fpf-empty_wf
fpf-inv-rename
fpf-inv-rename_wf
fpf-is-empty
fpf-is-empty_wf
fpf-join
fpf-join-ap
fpf-join-ap-left
fpf-join-ap-sq
fpf-join-assoc
fpf-join-cap
fpf-join-cap-sq
fpf-join-compatible-left
fpf-join-compatible-right
fpf-join-dom
fpf-join-dom-da
fpf-join-dom-decl
fpf-join-dom-sq
fpf-join-dom2
fpf-join-domain
fpf-join-empty
fpf-join-empty-sq
fpf-join-idempotent
fpf-join-is-empty
fpf-join-list
fpf-join-list-ap
fpf-join-list-ap-disjoint
fpf-join-list-ap2
fpf-join-list-dom
fpf-join-list-dom2
fpf-join-list-domain
fpf-join-list-domain2
fpf-join-list_wf
fpf-join-range
fpf-join-single-property
fpf-join-sub
fpf-join-sub2
fpf-join-wf
fpf-join_wf
fpf-map
fpf-map_wf
fpf-normalize
fpf-normalize-ap
fpf-normalize-dom
fpf-normalize_wf
fpf-null-domain
fpf-rename
fpf-rename-ap
fpf-rename-ap2
fpf-rename-cap
fpf-rename-cap2
fpf-rename-cap3
fpf-rename-dom
fpf-rename-dom2
fpf-rename_wf
fpf-restrict
fpf-restrict-ap
fpf-restrict-cap
fpf-restrict-compatible
fpf-restrict-compatible2
fpf-restrict-dom
fpf-restrict-domain
fpf-restrict_wf
fpf-restrict_wf2
fpf-single
fpf-single-dom
fpf-single-dom-sq
fpf-single-sub-reflexive
fpf-single-valued
fpf-single-valued_wf
fpf-single_wf
fpf-single_wf2
fpf-single_wf3
fpf-split
fpf-sub
fpf-sub-compatible-left
fpf-sub-compatible-right
fpf-sub-functionality
fpf-sub-functionality2
fpf-sub-join
fpf-sub-join-left
fpf-sub-join-left2
fpf-sub-join-right
fpf-sub-join-right2
fpf-sub-join-symmetry
fpf-sub-reflexive
fpf-sub-set
fpf-sub-val
fpf-sub-val2
fpf-sub-val3
fpf-sub_functionality
fpf-sub_functionality2
fpf-sub_transitivity
fpf-sub_weakening
fpf-sub_wf
fpf-sub_witness
fpf-trivial-subtype-set
fpf-trivial-subtype-top
fpf-type
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
fpf-val
fpf-val-single1
fpf-val_wf
fpf-vals
fpf-vals-nil
fpf-vals-singleton
fpf-vals_wf
fpf_ap_compose_lemma
fpf_ap_pair_lemma
fpf_ap_single_lemma
fpf_dom_compose_lemma
fpf_join_cons_lemma
fpf_join_nil_lemma
fpf_wf
free-from-atom-fpf-ap
l_disjoint-fpf-dom
l_disjoint-fpf-join-dom
member-fpf-dom
member-fpf-domain
member-fpf-domain-variant
member-fpf-vals
member-fpf-vals2
mk_fpf
mk_fpf_ap_lemma
mk_fpf_dom_lemma
mk_fpf_wf
no_repeats-pairs-fpf
pairs-fpf
pairs-fpf_property
pairs-fpf_wf
sq_stable__fpf-sub
subtype-fpf
subtype-fpf-cap
subtype-fpf-cap-top
subtype-fpf-cap-top2
subtype-fpf-cap-void
subtype-fpf-cap-void-list
subtype-fpf-cap-void2
subtype-fpf-cap5
subtype-fpf-general
subtype-fpf-variant
subtype-fpf-void
system-fpf
system-fpf_wf
FPF2
prev top next
subtype-fpf2
FPF3
prev top next
subtype-fpf3
FPS
prev top next
abmonoid_ac_1_fps
abmonoid_comm_fps
binary-fps
binary-fps_wf
fps-Pascal
fps-Pascal-iff
fps-Pascal_wf
fps-add
fps-add-assoc
fps-add-comm
fps-add-grp
fps-add-grp_wf
fps-add-slice
fps-add-ucont
fps-add_wf
fps-alg
fps-alg_wf
fps-atom
fps-atom_wf
fps-coeff
fps-coeff_wf
fps-compose
fps-compose-add
fps-compose-atom
fps-compose-atom-eq
fps-compose-atom-neq
fps-compose-compose
fps-compose-exp
fps-compose-fps-product
fps-compose-identity
fps-compose-mul
fps-compose-neg
fps-compose-one
fps-compose-scalar-mul
fps-compose-single
fps-compose-single-disjoint
fps-compose-sub
fps-compose-ucont
fps-compose-zero
fps-compose_wf
fps-degree-bound
fps-degree-bound_wf
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
fps-elim-div
fps-elim-hom
fps-elim-x
fps-elim-x-add
fps-elim-x-atom
fps-elim-x-elim-x
fps-elim-x-elim-y
fps-elim-x-mul
fps-elim-x-neg
fps-elim-x-one
fps-elim-x-sub
fps-elim-x-zero
fps-elim-x_wf
fps-elim_wf
fps-exp
fps-exp-add
fps-exp-linear-coeff
fps-exp-one
fps-exp-unroll
fps-exp-zero
fps-exp_wf
fps-ext
fps-geometric-slice
fps-geometric-slice1
fps-geometric-slice_lemma
fps-geometric-slice_lemma2
fps-id-ucont
fps-linear-ucont-equal
fps-moebius
fps-moebius-eq
fps-moebius-inversion
fps-moebius_wf
fps-mul
fps-mul-assoc
fps-mul-coeff-bag-rep-simple
fps-mul-comm
fps-mul-single
fps-mul-single-general
fps-mul-slice
fps-mul-ucont
fps-mul_wf
fps-neg
fps-neg-slice
fps-neg_wf
fps-non-trivial
fps-not-null
fps-one
fps-one-slice
fps-one_wf
fps-pascal
fps-pascal-elim
fps-pascal-slice
fps-pascal-symmetry
fps-pascal_wf
fps-product
fps-product-append
fps-product-reindex
fps-product-single
fps-product-upto
fps-product_wf
fps-restrict
fps-restrict-empty
fps-restrict-summation
fps-restrict_wf
fps-rng
fps-rng_wf
fps-scalar-mul
fps-scalar-mul-one
fps-scalar-mul-property
fps-scalar-mul-rng-add
fps-scalar-mul-slice
fps-scalar-mul-zero
fps-scalar-mul_wf
fps-set-to-one
fps-set-to-one-add
fps-set-to-one-neg
fps-set-to-one-one
fps-set-to-one-scalar-mul
fps-set-to-one-single
fps-set-to-one-slice
fps-set-to-one-sub
fps-set-to-one-ucont
fps-set-to-one-zero
fps-set-to-one_wf
fps-single
fps-single-slice
fps-single_wf
fps-slice
fps-slice-slice
fps-slice-ucont
fps-slice_wf
fps-sub
fps-sub-slice
fps-sub_wf
fps-summation
fps-summation-coeff
fps-summation_wf
fps-support
fps-support-degree-bound
fps-support_wf
fps-ucont
fps-ucont-composition
fps-ucont_wf
fps-zero
fps-zero-slice
fps-zero_wf
iabgrp_op_inv_assoc_fps
mon_assoc_fps
mon_ident_fps
mul_ac_1_fps
mul_assoc_fps
mul_comm_fps
mul_one_fps
mul_over_minus_fps
mul_over_plus_fps
mul_zero_fps
neg_assoc_fps
neg_id_fps
neg_inv_fps
neg_thru_op_fps
negerse_fps
ternary-fps
ternary-fps_wf
uniform-fps
uniform-fps_wf
unit-fps
unit-fps_wf
FRACTIONS
prev top next
decidable__rless-int-fractions
radd-int-fractions
req-int-fractions
rleq-int-fractions
rless-int-fractions
rmul-int-fractions
FRACTIONS2
prev top next
req-int-fractions2
rleq-int-fractions2
rless-int-fractions2
FREE
prev top next
atom-free-decl
encryption-key-free-from-atom
free-from-atom
free-from-atom-Id
free-from-atom-Id-rw
free-from-atom-IdLnk
free-from-atom-Knd
free-from-atom-atom
free-from-atom-bool
free-from-atom-bool-subtype
free-from-atom-fpf-ap
free-from-atom-int
free-from-atom-l_member
free-from-atom-nat
free-from-atom-outl
free-from-atom-outl2
free-from-atom-outr
free-from-atom-outr2
free-from-atom-pair
free-from-atom-pair-components
free-from-atom-pair-iff
free-from-atom-rational
free-from-atom-subtype
free-from-atom_wf
free-from-atom_wf2
free-from-atom_wf_general
free_abmon_endomorph_is_id
free_abmon_inj
free_abmon_inj_wf
free_abmon_mon
free_abmon_mon_wf
free_abmon_umap
free_abmon_umap_properties
free_abmon_umap_properties_1
free_abmon_umap_wf
free_abmon_unique
free_abmonoid
free_abmonoid_wf
free_in_prefix
free_in_prefix_wf
sdata-free-from-atom
sdata-pair-free-from-atom
FREEVARS
prev top next
mFOL-freevars
mFOL-freevars_wf
FREQUENCY
prev top next
frequency
frequency_wf
FRESH
prev top next
CR-protocol-fresh
add-fresh-cname
add-fresh-cname_wf
add-remove-fresh-cname
add-remove-fresh-cname
add-remove-fresh-sq
assert-ses-is-fresh
decidable-ses-fresh-sequence
face-map_wf_fresh-cname
fresh-cname
fresh-cname
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
fresh-cname_wf
fresh-cname_wf
fresh-inning-reachable
fresh-sig-protocol1
fresh-sig-protocol1_property
fresh-sig-protocol1_wf
ses-fresh-sequence
ses-fresh-sequence_wf
ses-fresh-thread
ses-fresh-thread_wf
ses-is-fresh
ses-is-fresh_wf
ses-is-protocol-actions-fresh
subtype-add-fresh-cname
FROM
prev top next
Comm-req_from
Comm-req_from_wf
alg_from_rng
alg_from_rng_wf
bag-from-member-function
bag-from-member-function-exists
bag-member-from-upto
bag-summation-from-upto
encryption-key-free-from-atom
equalf_from_lef
equalf_from_lef_wf
es-interface-from-decidable
fma_from_gcp
fma_from_gcp_wf
free-from-atom
free-from-atom-Id
free-from-atom-Id-rw
free-from-atom-IdLnk
free-from-atom-Knd
free-from-atom-atom
free-from-atom-bool
free-from-atom-bool-subtype
free-from-atom-fpf-ap
free-from-atom-int
free-from-atom-l_member
free-from-atom-nat
free-from-atom-outl
free-from-atom-outl2
free-from-atom-outr
free-from-atom-outr2
free-from-atom-pair
free-from-atom-pair-components
free-from-atom-pair-iff
free-from-atom-rational
free-from-atom-subtype
free-from-atom_wf
free-from-atom_wf2
free-from-atom_wf_general
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
last-from-upto
length-from-upto
links-from-to
links-from-to_wf
member-from-upto
member-links-from-to
member-votes-from-inning
new_23_sig_commands_from_votes
new_23_sig_commands_from_votes_wf
new_23_sig_replica_state_from_proposal
new_23_sig_replica_state_from_proposal_fun
no_repeats_from-upto
pDVguards-from
pDVguards-from_wf
property-from-l_member
pv11_p1_acc_state_from_p2a
pv11_p1_acc_state_from_p2a_fun
pv11_p1_adopted_from_acceptor
pv11_p1_adopted_from_init_or_preempted
pv11_p1_adopted_from_maj_acceptors
pv11_p1_commander_state_from_p2bs
pv11_p1_decision_from_maj_acceptors
pv11_p1_decision_from_p2a
pv11_p1_decision_from_p2a_acc
pv11_p1_from-p2a
pv11_p1_from-p2a_wf
pv11_p1_pvalue_from_p2a
pv11_p1_scout_from_acc
pv11_p1_scout_fun_from_acc
pv11_p1_scout_fun_from_acc2
pv11_p1_scout_state_from_p1bs
rcvs-on-links-from-to
rng_from_grp
rng_from_grp_wf
sdata-free-from-atom
sdata-pair-free-from-atom
select-from-upto
ses-nonce-from-ordering
sq_stable__from_stable
sq_stable_from_decidable
stable__from_decidable
votes-from-inning
votes-from-inning-is-nil
votes-from-inning_wf
FRONT
prev top next
firstn_append_front
firstn_append_front_singleton
l_before_append_front
permute-to-front
permute-to-front-permutation
permute-to-front_wf
select-front-as-reduce
select_append_front
sublist_append_front
weak_l_before_append_front
FRS
prev top next
adjacent-frs-points
frs-increasing
frs-increasing-non-dec
frs-increasing-separated-common-refinement
frs-increasing-sorted-by
frs-increasing_wf
frs-mesh
frs-mesh-bound
frs-mesh-nonneg
frs-mesh_wf
frs-non-dec
frs-non-dec-sorted-by
frs-non-dec_wf
frs-refines
frs-refines_transitivity
frs-refines_weakening
frs-refines_wf
frs-separated
frs-separated_wf
sq_stable__frs-non-dec
FSEG
prev top next
filter_fseg
fseg
fseg-iseg-reverse
fseg-test
fseg_append
fseg_cons
fseg_cons2
fseg_cons_left
fseg_extend
fseg_length
fseg_member
fseg_nil
fseg_select
fseg_transitivity
fseg_weakening
fseg_wf
new_23_sig_quorum_fseg
nil_fseg
nth_tl_is_fseg
sq_stable__fseg
FSET
prev top next
all_fset_elim
assert-deq-fset-member
assert-fset-null
decidable__all_fset
decidable__equal_fset
decidable__es-fset-loc
decidable__fset-closed
decidable__fset-member
deq-fset-member
deq-fset-member_wf
empty-fset
empty-fset-closed
empty-fset_wf
empty-fset_wf-cut
es-empty-fset-at
es-fset-at
es-fset-at-loc
es-fset-at-property
es-fset-at_wf
es-fset-at_wf-interface
es-fset-last
es-fset-last_wf
es-fset-loc
es-fset-loc-iff
es-fset-loc_wf
es-fset-loc_wf-cut
fset
fset-add
fset-add-remove
fset-add_wf
fset-all
fset-all-iff
fset-all_wf
fset-closed
fset-closed_wf
fset-closure
fset-closure-exists
fset-closure-exists2
fset-closure-unique
fset-closure_wf
fset-extensionality
fset-filter
fset-filter_wf
fset-filter_wf2
fset-image
fset-image_wf
fset-induction
fset-intersection
fset-intersection-associative
fset-intersection-commutes
fset-intersection_wf
fset-item
fset-item-member
fset-item_wf
fset-list-union
fset-list-union_wf
fset-max
fset-max_property
fset-max_wf
fset-member
fset-member_wf
fset-member_wf-cut
fset-member_witness
fset-null
fset-null_wf
fset-only
fset-only_wf
fset-remove
fset-remove_wf
fset-singleton
fset-singleton_wf
fset-size
fset-size-add
fset-size-empty
fset-size-one
fset-size-remove
fset-size-union
fset-size_wf
fset-some
fset-some-iff
fset-some-iff2
fset-some_wf
fset-subtype
fset-to-list
fset-union
fset-union-associative
fset-union-closed
fset-union-commutes
fset-union-idempotent
fset-union_wf
fset_for_when_eq
fset_for_when_unique
fset_map
fset_map_wf
fset_mem_union
fset_of_mset
fset_of_mset_count_bound
fset_of_mset_mem
fset_of_mset_wf
fset_of_mset_wf2
fset_properties
fset_wf
member-fset-add
member-fset-filter
member-fset-image
member-fset-image-iff
member-fset-intersection
member-fset-list-union
member-fset-remove
member-fset-singleton
member-fset-union
rng_fset_for_when_eq
strong-subtype-fset-member-type
subtype_rel_fset
FSHIFT
prev top next
fshift
fshift_increasing
fshift_wf
FSIZE
prev top next
fsize_empty_lemma
FST
prev top next
cc-fst
cc-fst-csm-adjoin
cc-fst_wf
church-fst
church-fst_wf
church_fst_lemma
csm-adjoin-fst-snd
csm-ap-cubical-fst
cubical-fst
cubical-fst-pair
cubical-fst_wf
fst-recode-tuple
hdf-base-ap-fst
hdf-until-ap-fst
is-max-fst
max-fst-class
max-fst-class_wf
max-fst-property
max-fst-val
norm-fst
norm-fst_wf
sigma-box-fst
sigma-box-fst_wf
FTYPE
prev top next
ftype
ftype_properties
ftype_wf
FULL
prev top next
adjacent-full-partition-points
almost-full
almost-full
almost-full_wf
almost-full_wf
almost_full
almost_full_wf
full-evd-proof-step
full-faithful-functor
full-faithful-functor
full-faithful-functor_wf
full-faithful-functor_wf
full-partition
full-partition-non-dec
full-partition-point-member
full-partition_wf
FULL0
prev top next
almost_full0
FULPRUNTYPE
prev top next
fulpRunType
fulpRunType-subtype
fulpRunType_wf
FUN
prev top next
CLK_headers_fun
CLK_headers_fun_wf
C_TYPE_eq_fun
C_TYPE_eq_fun_wf
OARcast_headers_fun
OARcast_headers_fun_wf
State-comb-fun-eq
State-comb-fun-eq2
State-loc-comb-fun-eq
State-loc-comb-fun-eq-non-loc
State-loc-comb-fun-eq2
apply-strict-fun
between-fun-connected
callbyvalueall-seq-fun
can-apply-fun-exp
can-apply-fun-exp-add
can-apply-fun-exp-add-iff
ci-fun
collect_filter_accum_fun
collect_filter_accum_fun_wf
comb_for_fun_exp_wf
compare-fun
compare-fun_wf
const-fun-converges
decidable__fun-connected
detach_fun
detach_fun_properties
detach_fun_wf
div_fun_sat_div_nrel
eqmod_fun
es-fix-fun-exp
exists_det_fun
exists_det_fun_a
fun-cauchy
fun-cauchy_wf
fun-comparison-test
fun-connected
fun-connected-causle
fun-connected-fixedpoint
fun-connected-iff-fun_exp
fun-connected-induction
fun-connected-induction2
fun-connected-relation
fun-connected-step
fun-connected-step-back
fun-connected-test
fun-connected-test2
fun-connected-to-same
fun-connected-tree
fun-connected_antisymmetry
fun-connected_transitivity
fun-connected_weakening
fun-connected_weakening_eq
fun-connected_wf
fun-converges
fun-converges-iff-cauchy
fun-converges-on-compact
fun-converges-rmul
fun-converges-to
fun-converges-to-continuous
fun-converges-to_wf
fun-converges_functionality
fun-converges_wf
fun-equiv
fun-equiv-rel
fun-equiv_wf
fun-not-int
fun-path
fun-path-append
fun-path-append1
fun-path-before
fun-path-cons
fun-path-fixedpoint
fun-path-induction
fun-path-member
fun-path-member-connected
fun-path-no_repeats
fun-path_wf
fun-ratio-test
fun-series-converges
fun-series-converges-absolutely
fun-series-converges-absolutely-converges
fun-series-converges-absolutely_wf
fun-series-converges-on-compact
fun-series-converges-tail
fun-series-converges_wf
fun-series-sum
fun-series-sum_wf
fun_exp
fun_exp-fixedpoint
fun_exp-id
fun_exp-increasing
fun_exp-injection
fun_exp-mul
fun_exp-rem
fun_exp0_lemma
fun_exp1_lemma
fun_exp_add
fun_exp_add-sq
fun_exp_add1
fun_exp_add1-sq
fun_exp_add1-sq2
fun_exp_add1_sub
fun_exp_add_apply
fun_exp_add_apply1
fun_exp_add_sq
fun_exp_add_sq_again
fun_exp_apply_add1
fun_exp_com
fun_exp_compose
fun_exp_compose2
fun_exp_unroll
fun_exp_unroll_1
fun_exp_wf
fun_thru_1op
fun_thru_1op_wf
fun_thru_2op
fun_thru_2op_wf
fun_thru_ite
fun_thru_spread
fun_with_inv_is_bij
fun_with_inv_is_bij2
id-fun
id-fun-set
id-fun-subtype
id-fun_wf
int-decr-map-fun
int_pi_det_fun
int_pi_det_fun_wf
is-list-fun
is-list-fun_wf
is-list-if-has-value-fun
is-list-if-has-value-fun-ax-mem
is-list-if-has-value-fun_wf
is-strict-fun
is_list_fun_axiom_lemma
is_list_fun_pair_lemma
iterate-fun-stream
iterate-fun-stream_wf
l-ordered-remove-repeats-fun
loop-class-memory-fun-eq
loop-class-state-fun-eq
map-iterate-fun-stream
mapfilter-no-rep-fun
memory-class3-fun-eq
mk_applies_fun
mk_applies_lambdas_fun
mk_lambdas-fun
mk_lambdas-fun-eta
mk_lambdas-fun-shift-init
mk_lambdas-fun-unroll
mk_lambdas-fun-unroll-first
mk_lambdas-fun_wf
mk_lambdas_as_lambdas_fun
mk_lambdas_fun
mk_lambdas_fun-eta
mk_lambdas_fun-unroll
mk_lambdas_fun-unroll-first
mk_lambdas_fun-unroll-ite
mk_lambdas_fun_compose
mk_lambdas_fun_compose1
mk_lambdas_fun_compose2
mk_lambdas_fun_lambdas
mk_lambdas_fun_lambdas1
mk_lambdas_fun_lambdas2
mk_lambdas_fun_wf
mklist-general-fun
nat-id-fun-example
nat-id-fun-ext
new_23_sig_headers_fun
new_23_sig_headers_fun_wf
new_23_sig_quorum_inv_vote2_fun
new_23_sig_quorum_inv_vote_fun
new_23_sig_quorum_invariant_fun
new_23_sig_quorum_state_fun_eq
new_23_sig_replica_state_from_proposal_fun
new_23_sig_replica_state_mem_fun
new_23_sig_rounds_mem_fun
new_23_sig_rounds_pos_fun
num-antecedents-fun_exp
nysiad-inst-msg-fun
nysiad-inst-msg-fun_wf
nysiad_headers_fun
nysiad_headers_fun_wf
p-fun-exp
p-fun-exp-add
p-fun-exp-add-sq
p-fun-exp-add1-sq
p-fun-exp-compose
p-fun-exp-injection
p-fun-exp-one
p-fun-exp_wf
pv11_p1_acc_fun_p2a
pv11_p1_acc_fun_p2a_pv
pv11_p1_acc_state_from_p2a_fun
pv11_p1_acc_state_fun_eq
pv11_p1_acc_state_fun_eq2
pv11_p1_commander_state_fun_eq
pv11_p1_headers_fun
pv11_p1_headers_fun_wf
pv11_p1_inc_acc_bnum_fun
pv11_p1_inc_acc_pvals_fun
pv11_p1_ldr_active_fun
pv11_p1_ldr_fun_loc_bnum
pv11_p1_ldr_fun_mem_adopted
pv11_p1_ldr_fun_mem_propose
pv11_p1_ldr_fun_mem_propose2
pv11_p1_ldr_fun_ord
pv11_p1_ldr_fun_pos
pv11_p1_ldr_fun_proposal3
pv11_p1_ldr_fun_state_adopted_pred
pv11_p1_ldr_fun_state_propose_pred
pv11_p1_ldr_state_fun_eq
pv11_p1_scout_fun_from_acc
pv11_p1_scout_fun_from_acc2
pv11_p1_scout_state_fun_eq
pv11_p1_unique_adopted_fun
rem_fun_sat_rem_nrel
remove-repeats-fun
remove-repeats-fun-as-filter
remove-repeats-fun-as-remove-repeats-map
remove-repeats-fun-length-as-remove-repeats-map
remove-repeats-fun-map
remove-repeats-fun-map2
remove-repeats-fun-member
remove-repeats-fun-nil
remove-repeats-fun-sublist
remove-repeats-fun_wf
remove-repeats-mapfilter-with-fun
retraction-fun-path
retraction-fun-path-before
retraction-fun-path-squash
select_fun_ap
select_fun_ap_is_last1
select_fun_ap_wf
select_fun_last
select_fun_last_partial_ap1
select_fun_last_partial_ap_gen1
select_fun_last_wf
sq-id-fun
sq-id-fun_wf
sq_stable__fun_thru_1op
sq_stable__fun_thru_2op
sq_stable__is-list-if-has-value-fun
state-class1-fun-eq
state-class2-fun-eq
state-class3-fun-eq
strict-fun
strict-fun
strict-fun-connected
strict-fun-connected-induction
strict-fun-connected-step
strict-fun-connected_irreflexivity
strict-fun-connected_transitivity1
strict-fun-connected_transitivity2
strict-fun-connected_transitivity3
strict-fun-connected_wf
strict-fun_wf
strong-fun-connected-induction
subtype-iff-id-mem-fun
trivial_nat1_fun
type-monotone-fun_exp
type-monotone_fun_exp_top
FUN0
prev top next
mk_applies_lambdas_fun0
FUN1
prev top next
callbyvalueall-seq-fun1
callbyvalueall_seq-fun1
mk_applies_lambdas_fun1
FUN2
prev top next
callbyvalueall-seq-fun2
callbyvalueall_seq-fun2
mk_applies_fun2
pv11_p1_unique_adopted_fun2
FUN2LISTCANTOR
prev top next
fun2listCantor
FUN3
prev top next
callbyvalueall_seq-fun3
FUN4
prev top next
callbyvalueall_seq-fun4
FUNA
prev top next
pv11_p1_A4_C1_funA
FUNC
prev top next
map_permr_func
pv11_p1_A4_C1_funC
trans_rel_func_wrt_sym_self
FUNCTION
prev top next
antecedent-function
antecedent-function_functionality_wrt_iff
antecedent-function_wf
apply-Id-alist-function
apply-alist-function
apply_wf_type-function
bag-from-member-function
bag-from-member-function-exists
bag-function
base-member-per-function
bottom_wf_function
canonical-function
canonical-function_wf
canonicalizable-function
continuous-function
continuous-monotone-function
decidable__equal_function
equipollent-function-function
equipollent-function-product
equipollent-union-function
finite-function-equipollent
finite-function-equipollent-tuple
finite-function-type-equality
function def
function-eq
function-eq-implies
function-eq-symmetry
function-eq-symmetry-type-function
function-eq-transitivity
function-eq-transitivity-type-function
function-eq_wf
function-eq_wf_type_function
function-mono
function-not-int
function-subtype-top
function-value-type
function-valueall-type
function-wf
function_functionality_wrt_equipollent
function_functionality_wrt_equipollent_left
function_functionality_wrt_equipollent_right
markov-streamless-function
monotone-upper-bound-function
not-quotient-function-subtype
note-is-function
per-function
per-function-ext
per-function-type-apply
per-function_wf
per-function_wf_base_family
per-function_wf_type
quotient-dep-function-subtype
quotient-function-subtype
restart-function
singleton-type-function
stable__function_equal
step-function
step-function-example
step-function-example-member
step-function-example-monotone
step-function-example_wf
step-function_wf
strict-bag-function
strict-bag-function_wf
strong-continuous-function
subtype_rel_dep_function
subtype_rel_dep_function_iff
subtype_rel_function
system-function
system-function_wf
top-subtype-function
type-function
type-function-eta
type-function_wf
void-function-equipollent
weak-antecedent-function
weak-antecedent-function-property
weak-antecedent-function_functionality_wrt_pred_equiv
weak-antecedent-function_wf
FUNCTIONAL
prev top next
CLK_Clock-functional
Memory-class-functional
Memory-loc-class-functional
Memory1-functional
Memory2-functional
Memory3-functional
OARcast_SenderState-functional
State-comb-functional
State-loc-comb-functional
State1-functional
State2-functional
continuous-implies-functional
eclass3-functional
es-functional-class
es-functional-class-at
es-functional-class-at_wf
es-functional-class-implies-at
es-functional-class_wf
loop-class-memory-functional
loop-class-state-functional
memory-class3-functional
new_23_sig_NewRoundsState-functional
new_23_sig_QuorumState-functional
new_23_sig_ReplicaState-functional
nysiad_MessageBagState-functional
nysiad_QueueState-functional
pv11_p1_AcceptorState-functional
pv11_p1_CommanderState-functional
pv11_p1_LeaderState-functional
pv11_p1_ScoutState-functional
FUNCTIONALITY
prev top next
I-path-morph_functionality
Q-R-glues_functionality
Q-R-pre-preserving_functionality_wrt_implies
Taylor-approx_functionality
ab_binrel_functionality
add_functionality_wrt_eq
add_functionality_wrt_eqmod
add_functionality_wrt_le
add_functionality_wrt_lt
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_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
bar-converges_functionality
bar-diverges_functionality
bdd-diff_functionality
biject_functionality
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
combination_functionality
compact_functionality_wrt_equipollent
compact_functionality_wrt_surject
connex_functionality_wrt_iff
connex_functionality_wrt_implies
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
converges-to_functionality
coprime_functionality_wrt_eqmod
coprime_functionality_wrt_eqmod2
count_functionality
dataflow-to-Process_functionality
decidable_functionality
deliver-msg_functionality
derivative_functionality
derivative_functionality_wrt_subinterval
diff_functionality_wrt_permr
divides_functionality_wrt_assoced
dot-product_functionality
double_sum_functionality
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
equiv_rel_self_functionality
es-E-interface_functionality
es-E-interface_functionality-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
eu-seg-extend_functionality
event-has_functionality
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-image_functionality
filter2_functionality
filter_functionality
filter_functionality_wrt_permutation
finite_functionality_wrt_equipollent
fpf-ap_functionality
fpf-cap-subtype_functionality
fpf-cap-subtype_functionality_wrt_sub
fpf-cap-subtype_functionality_wrt_sub2
fpf-cap_functionality
fpf-cap_functionality_wrt_sub
fpf-dom_functionality
fpf-sub-functionality
fpf-sub_functionality
fun-converges_functionality
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
i-member_functionality
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
imax-list_functionality
implies_functionality_wrt_iff
implies_functionality_wrt_implies
inject_functionality
isect2_functionality_wrt_subtype_rel
isect_functionality_wrt_equipollent_dependent
l_all_functionality
l_all_functionality_wrt_permutation
l_exists_functionality
l_member_functionality_wrt_permutation
l_sum_functionality_wrt_permutation
le_functionality
length_functionality_wrt_permr
less_than_functionality
lg-all_functionality
linorder_functionality_wrt_ext-eq
linorder_functionality_wrt_iff
list-diff_functionality
list-functionality-induction
list-to-set_functionality_wrt_permutation
list_accum_functionality
lmax_functionality_wrt_permr
lmin_functionality_wrt_permr
locknd_functionality_isrcv
mFOL-abstract-functionality
map-class_functionality
map_functionality
map_functionality
map_functionality_2
map_functionality_wrt_sq
mapfilter-class_functionality
massoc_functionality_wrt_massoc
mem_functionality_wrt_permr
minus_functionality_wrt_eq
minus_functionality_wrt_eqmod
minus_functionality_wrt_le
minus_functionality_wrt_lt
mod_mssum_functionality
mon_for_functionality_wrt_permr
mon_reduce_functionality_wrt_permr
monot_functionality
mset_for_functionality
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
pRun_functionality
partition-sum_functionality
permr_functionality_wrt_permr
permr_massoc_functionality
permr_upto_functionality_wrt_permr_upto
permutation_functionality_wrt_permutation
power-sum_functionality_wrt_eqmod
power-sum_functionality_wrt_le
prank_functionality
primed-class-opt_functionality
primed-class-opt_functionality-locl
product_functionality_wrt_equipollent
product_functionality_wrt_equipollent_dependent
product_functionality_wrt_equipollent_left
product_functionality_wrt_equipollent_right
qeq-functionality
quadratic-residue_functionality
r-ap_functionality
rabs_functionality
rabs_functionality_wrt_bdd-diff
radd-list_functionality
radd-list_functionality_wrt_permutation
radd-list_functionality_wrt_rleq
radd_functionality
radd_functionality_wrt_rleq
radd_functionality_wrt_rless1
radd_functionality_wrt_rless2
rdiv_functionality
real-vec-norm_functionality
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_implies_functionality
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
req_functionality
rinv-functionality-lemma
rinv_functionality
rleq2_functionality
rleq_functionality
rleq_functionality_wrt_implies
rless_functionality
rless_functionality_wrt_implies
rmax_functionality
rmax_functionality_wrt_bdd-diff
rmax_functionality_wrt_rleq
rmaximum_functionality
rmaximum_functionality_wrt_rleq
rmin_functionality
rmin_functionality_wrt_bdd-diff
rminus_functionality
rminus_functionality_wrt_bdd-diff
rminus_functionality_wrt_rleq
rmul_functionality
rmul_functionality_wrt_rleq
rmul_functionality_wrt_rleq2
rmul_functionality_wrt_rless
rmul_functionality_wrt_rless2
rneq_functionality
rnexp_functionality
rng_mssum_functionality_wrt_bsubmset
rng_mssum_functionality_wrt_equal
rnonneg2_functionality
rnonneg_functionality
rnonzero_functionality
rpoly-nth-deriv_functionality
rpositive2_functionality
rpositive_functionality
rroot_functionality
rset-member_functionality
rsqrt_functionality
rsub_functionality
rsub_functionality_wrt_rleq
rsub_functionality_wrt_rless
rsum_functionality
rsum_functionality_wrt_rleq
rsum_functionality_wrt_rleq2
rsum_functionality_wrt_rleq3
s_part_functionality_wrt_breqv
ses-info-flow-exp_functionality
ses-info-flow_functionality
set_blt_functionality_wrt_set_lt_r
sq_or_functionality_wrt_iff
squash_functionality_wrt_iff
squash_functionality_wrt_implies
squash_functionality_wrt_uiff
strict-majority_functionality
strict-upper-bound_functionality
strong-subtype_functionality
sub_functionality_wrt_le
subtract_functionality_wrt_eqmod
subtype_rel_functionality_wrt_iff
subtype_rel_functionality_wrt_implies
sum_functionality
sum_functionality_wrt_sqequal
sym_functionality_wrt_iff
system-strongly-realizes_functionality
trans_functionality_wrt_iff
trans_rel_self_functionality
tree-secures_functionality
uall_functionality_wrt_iff
uanti_sym_functionality_wrt_iff
uconnex_functionality_wrt_iff
uconnex_functionality_wrt_implies
uequiv_rel_functionality_wrt_iff
uequiv_rel_self_functionality
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
unordered-combination_functionality
uorder_functionality_wrt_iff
upper-bound_functionality
urefl_functionality_wrt_iff
usym_functionality_wrt_iff
utrans_functionality_wrt_iff
utrans_rel_self_functionality
value-type_functionality
valueall-type_functionality
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
FUNCTIONALITY2
prev top next
converges-to_functionality2
fpf-dom_functionality2
fpf-sub-functionality2
fpf-sub_functionality2
rinv_functionality2
rsum_functionality2
FUNCTIONS
prev top next
weak-antecedent-functions-compose
FUNCTOR
prev top next
W_iterate_functor
W_iterate_functor_wf
cat-functor
cat-functor
cat-functor_wf
cat-functor_wf
constant-type-functor
constant-type-functor_wf
cubical-set-is-functor
full-faithful-functor
full-faithful-functor
full-faithful-functor_wf
full-faithful-functor_wf
functor-arrow
functor-arrow
functor-arrow-comp
functor-arrow-comp
functor-arrow-id
functor-arrow-id
functor-arrow_wf
functor-arrow_wf
functor-cat
functor-cat
functor-cat_wf
functor-cat_wf
functor-comp
functor-comp
functor-comp-assoc
functor-comp-assoc
functor-comp-id
functor-comp-id
functor-comp_wf
functor-comp_wf
functor-ob
functor-ob
functor-ob_wf
functor-ob_wf
groupoid-nerve-functor-flip
id_functor
id_functor
id_functor_wf
id_functor_wf
identity-functor
identity-functor_wf
iterate_functor
iterate_functor_wf
list-functor
poset-functor
poset-functor-comp
poset-functor-extends
poset-functor-extends-box-faces
poset-functor-extends-box-faces-1
poset-functor-extends_wf
poset-functor-id
poset-functor_wf
poset-id-functor
poset_functor_extend
poset_functor_extend-extends
poset_functor_extend-face-map
poset_functor_extend-face-map1
poset_functor_extend-flip
poset_functor_extend-is-functor
poset_functor_extend_id
poset_functor_extend_same
poset_functor_extend_wf
type-functor
type-functor-compose
type-functor-compose_wf
type-functor-iterate
type-functor-iterate_wf
type-functor-product
type-functor-product_wf
type-functor-sum
type-functor-sum_wf
type-functor_wf
unique-poset-functor
FUNCTORS
prev top next
equal-functors
equal-functors
poset-functors-equal
FUND
prev top next
fund-theorem-arithmetic
FUNINV
prev top next
funinv
funinv-compose
funinv-funinv
funinv-property
funinv-unique
funinv_wf
funinv_wf2
funinv_wf3
FUNS
prev top next
equipollent-iff-inverse-funs
inv_funs
inv_funs-iff
inv_funs_sym
inv_funs_wf
sq_stable__inv_funs
FUNTYPE
prev top next
C-comb_wf_funtype
funtype
funtype-auto-test-case
funtype-split
funtype-unroll
funtype-unroll-last
funtype-unroll-last-eq
funtype_wf
FWD
prev top
es-fwd-propagation
es-fwd-propagation-via
es-fwd-propagation-via-unique
es-fwd-propagation-via_wf
es-fwd-propagation_wf
l_all_fwd