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

A

top next

A-adjacent-compatible
A-adjacent-compatible_wf
A-assign
A-assign2
A-assign2_wf
A-assign_wf
A-associative
A-associative'
A-bind
A-bind'
A-bind'_wf
A-bind2
A-bind2_wf
A-bind_wf
A-bind_wf2
A-bind_wf3
A-block
A-block_wf
A-coerce
A-coerce_wf
A-eval
A-eval_wf
A-eval_wf2
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
A-fetch
A-fetch'
A-fetch'_wf
A-fetch2
A-fetch2_wf
A-fetch_wf
A-leftunit
A-leftunit'
A-loop
A-loop_wf
A-loop_wf2
A-map
A-map'
A-map'_wf
A-map_wf
A-null
A-null-loop
A-null-property
A-null_wf
A-open-box
A-open-box-equal
A-open-box-image
A-open-box-image_wf
A-open-box_wf
A-post-val
A-post-val_wf
A-pre-val
A-pre-val_wf
A-return
A-return'
A-return'_wf
A-return_wf
A-rightunit
A-rightunit'
A-shift-spec
A-shift-spec_wf
A-shift-upto
A-shift-upto-spec
A-shift-upto-spec_wf
A-shift-upto_wf
Kan structure on Id_A a b
Kan-A-filler
Kan-A-filler_wf
The Type (Id_A a b)
add_grp_of_rng_wf_a
all_rng_quot_elim_a
bmsexists_char_a
bmsexists_char_a_rw
chrem_exists_a
chrem_exists_aux_a
comb_for_mk_perm_wf_a
comp_nat_ind_a
constant-A-open-box
coprime_elim_a
count_bsublist_a
csm-A-open-box
dec_alt_char_a
dneg_elim_a
exists_det_fun_a
extend-A-open-box
extend-A-open-box_wf
fills-A-faces
fills-A-faces_wf
fills-A-open-box
fills-A-open-box_wf
gcd_p_neg_arg_a
gcd_p_sym_a
grp_lt_is_sp_of_leq_a
int_entire_a
inv_image_ind_a
is-A-face
is-A-face_wf
lapp_fact_a
lookup_before_start_a
lookup_omral_scale_a
lookup_omral_times_a
lookups_same_a
mcopower_umap_comm_tri_a
mfact_exists_a
mk_perm_wf_a
mset_inc_a
mset_ind_a
mul_mon_of_rng_wf_a
nat_ind_a
not_over_or_a
oal_umap_char_a
oalist_cases_a
oalist_ind_a
omral_bilinear_a
omral_fact_a
omral_lookups_same_a
omral_times_assoc_a
omral_times_comm_a
omralist_ind_a
perm_induction_a
permr_iff_eq_counts_a
quot_ring_car_elim_a
set_lt_is_sp_of_leq_a
sq_stable_Kan-A-filler
sq_stable_fills-A-open-box
sq_stable_uniform-Kan-A-filler
sym_grp_is_swaps_a
term-A-face
term-A-face_wf
trans_imp_sp_trans_a
uniform-Kan-A-filler
uniform-Kan-A-filler_wf
utrans_imp_sp_utrans_a
xxconnex_iff_trichot_a
zero_ann_a

ABDMONOID

prev top next

abdmonoid
abdmonoid_abmonoid
abdmonoid_dmon
abdmonoid_inc
abdmonoid_properties
abdmonoid_wf
cdrng_is_abdmonoid
mk_abdmonoid
ocmon_subtype_abdmonoid

ABGRP

prev top next

abdgrp_subtype_abgrp
abgrp
abgrp_properties
abgrp_subtype_grp
abgrp_wf
ocgrp_subtype_abgrp

ABMON

prev top next

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
rng_abmon
rng_abmon_wf

ABMONOID

prev top next

abdmonoid_abmonoid
abmonoid
abmonoid_ac_1
abmonoid_ac_1_fps
abmonoid_comm
abmonoid_comm_fps
abmonoid_cumulative
abmonoid_inc
abmonoid_properties
abmonoid_subtype_iabmonoid
abmonoid_subtype_mon
abmonoid_wf
free_abmonoid
free_abmonoid_wf
mk_abmonoid

ABOUT

prev top next

pv11_p1_about_threshold
theorems about Kan structure

ABOVE

prev top next

bounded-above
bounded-above-strict
bounded-above_wf
is-above
is-above-axiom
is-above-inl
is-above-inr
is-above-int
is-above-pair
is-above-subtype
is-above_wf
totally-bounded-bounded-above

ABS

prev top next

abs-val
abs-val_wf
continuous-abs
continuous-abs-ext
continuous-abs-subtype
pv11_p1_abs_Ballot_Num
pv11_p1_abs_Ballot_Num_wf
rabs-abs
rroot-abs
rroot-abs-non-neg
rroot-abs-property
rroot-abs_wf

ABSOLUTELY

prev top next

converges-absolutely
converges-absolutely-converges
converges-absolutely_wf
fun-series-converges-absolutely
fun-series-converges-absolutely-converges
fun-series-converges-absolutely_wf

ABSORPTION

prev top next

band_bor_absorption
bor_band_absorption

ABSTRACT

prev top next

mFOL-abstract
mFOL-abstract-functionality
mFOL-abstract-rename
mFOL-abstract_wf
mFOL-sequent-abstract
mFOL-sequent-abstract_wf
mFOL-subst-abstract

ABSTRACTFOATOMIC

prev top next

AbstractFOAtomic
AbstractFOAtomic_wf

ABSTRACTFOFORMULA

prev top next

AbstractFOFormula
AbstractFOFormula_wf

ABSVAL

prev top next

absval
absval-as-imax
absval-diff-product-bound
absval-diff-symmetry
absval-imax-difference
absval-imin-difference
absval-implies-rneq
absval-minus
absval-positive
absval-sqequal-imax
absval-squeeze
absval_assoced
absval_div_decreases
absval_div_nat
absval_elim
absval_eq
absval_exp
absval_lbound
absval_mul
absval_neg
absval_pos
absval_square
absval_squared
absval_sum
absval_sym
absval_ubound
absval_unfold
absval_unfold2
absval_wf
absval_zero
comb_for_absval_wf
rem_bounds_absval
rem_bounds_absval_le
sign-absval

ABSVALS

prev top next

divides_of_absvals

AC

prev top next

AC_1_0
AC_1_0_wf
abmonoid_ac_1
abmonoid_ac_1_fps
bag-append-ac
crng_times_ac_1
mul_ac_1_fps
radd-ac
rmul-ac
rng_plus_ac_1

ACC

prev top next

list_acc_cons_red_lemma
list_acc_nil_red_lemma
pv11_p1_acc_fun_p2a
pv11_p1_acc_fun_p2a_pv
pv11_p1_acc_p2a
pv11_p1_acc_rcv_p2a
pv11_p1_acc_rcv_p2a2
pv11_p1_acc_state_from_p2a
pv11_p1_acc_state_from_p2a_fun
pv11_p1_acc_state_fun_eq
pv11_p1_acc_state_fun_eq2
pv11_p1_decision_from_p2a_acc
pv11_p1_inc_acc
pv11_p1_inc_acc_bnum_fun
pv11_p1_inc_acc_pvals_fun
pv11_p1_inv_acc
pv11_p1_scout_from_acc
pv11_p1_scout_fun_from_acc

ACC2

prev top next

pv11_p1_scout_fun_from_acc2

ACCELERATE

prev top next

accelerate
accelerate-bdd-diff
accelerate_wf

ACCEPTED

prev top next

pv11_p1_init_accepted
pv11_p1_init_accepted_wf

ACCEPTOR

prev top next

pv11_p1_Acceptor
pv11_p1_Acceptor-program
pv11_p1_Acceptor-program_wf
pv11_p1_Acceptor_wf
pv11_p1_adopted_from_acceptor
pv11_p1_init_acceptor
pv11_p1_init_acceptor_wf

ACCEPTORS

prev top next

pv11_p1_adopted_from_maj_acceptors
pv11_p1_decision_from_maj_acceptors

ACCEPTORSP1A

prev top next

pv11_p1_AcceptorsP1a
pv11_p1_AcceptorsP1a-program
pv11_p1_AcceptorsP1a-program_wf
pv11_p1_AcceptorsP1a_wf

ACCEPTORSP2A

prev top next

pv11_p1_AcceptorsP2a
pv11_p1_AcceptorsP2a-program
pv11_p1_AcceptorsP2a-program_wf
pv11_p1_AcceptorsP2a_wf

ACCEPTORSTATE

prev top next

pv11_p1_AcceptorState
pv11_p1_AcceptorState-classrel
pv11_p1_AcceptorState-functional
pv11_p1_AcceptorState-program
pv11_p1_AcceptorState-program_wf
pv11_p1_AcceptorState_wf
pv11_p1_valid-AcceptorState
pv11_p1_valid-AcceptorState_wf

ACCEPTORSTATEFUN

prev top next

pv11_p1_AcceptorStateFun
pv11_p1_AcceptorStateFun_wf

ACCM

prev top next

collect_accm
collect_accm-wf2
collect_accm_wf

ACCPTS

prev top next

pv11_p1_messages-delivered-w-omissions-accpts
pv11_p1_messages-delivered-w-omissions-accpts_wf

ACCS

prev top next

pv11_p1_overlapping_accs

ACCUM

prev top next

Accum-class
Accum-class-es-sv
Accum-class-es-sv1
Accum-class-invariant
Accum-class-progress
Accum-class-single-val
Accum-class-single-val0
Accum-class-top
Accum-class-trans
Accum-class-trans-refl
Accum-class_wf
Accum-classrel-Memory
Accum-classrel-Memory-sq
Accum-loc-class
Accum-loc-class-as-loop-class2
Accum-loc-class-es-sv
Accum-loc-class-es-sv1
Accum-loc-class-exists
Accum-loc-class_wf
Accum-loc-classrel-Memory
Accum-loc-classrel-Memory-sq
Prior-Accum-class-single-val0
accum-class
accum-class-programmable
accum-class-val
accum-class_wf
accum-induction
accum-induction-ext
accum-induction-factorial
accum-induction-lemma
accum-matching-indices
accum-matching-indices-comment
accum-matching-indices_wf
accum-matching-tagged-indices
accum-matching-tagged-indices_wf
accum_filter_rel
accum_filter_rel_nil
accum_filter_rel_wf
accum_induction
accum_list
accum_list_cons_lemma
accum_list_wf
accum_split
accum_split_inverse
accum_split_iseg
accum_split_iseg2
accum_split_one_one
accum_split_prefix
accum_split_prefix2
accum_split_wf
archive-condition-threshold-accum
archive-consensus-accum-num
bag-accum
bag-accum-map
bag-accum-single
bag-accum_wf
bag-filter-as-accum
bag-map-as-accum
bl-all-as-accum
bl-exists-as-accum
cbv_list_accum
cbv_list_accum-is-list_accum
cbv_list_accum_wf
collect_accum
collect_accum-wf2
collect_accum_wf
collect_filter_accum_fun
collect_filter_accum_fun_wf
consensus-accum
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
consensus-accum-state
consensus-accum-state_wf
consensus-accum_wf
cps-accum
cps-accum_wf
eager-accum
eager-accum-list_accum
eager-accum_wf
es-history-accum
es-interface-accum
es-interface-accum-programmable
es-interface-accum-val
es-interface-accum_wf
es-interface-buffer-as-accum
es-interface-count-as-accum
filter-as-accum-aux
filter-as-accum-aux2
filter-image-interface-accum-equal
fpf-accum
fpf-accum_wf
int_consensus_accum
int_consensus_accum_wf
is-accum-class
is-interface-accum
is_accum_splitting
is_accum_splitting_wf
l_sum_as_accum
last_induction_accum
lastn-as-accum
length-as-accum
list-accum
list-accum-append
list-accum_wf
list_accum
list_accum-map
list_accum-mapfilter
list_accum-remove-repeats
list_accum-set-equal-idemp
list_accum-triangle-inequality
list_accum_append
list_accum_as_reduce
list_accum_cons
list_accum_cons_lemma
list_accum_equality
list_accum_filter
list_accum_functionality
list_accum_invariant
list_accum_invariant2
list_accum_invariant3
list_accum_is_reduce
list_accum_iseg_inv
list_accum_nil_lemma
list_accum_pair
list_accum_pair-sq
list_accum_pair_wf
list_accum_permute
list_accum_permute1
list_accum_proper_iseg_inv
list_accum_set-equal
list_accum_split
list_accum_wf
longest-prefix-list_accum
map-interface-accum-equal
mapfilter-as-accum
mapfilter-as-accum-aux
member_list_accum_l_subset
member_list_accum_l_subset2
reduce-as-accum
sq_stable__is_accum_splitting
sqequal-list_accum
sqequal-list_accum-list_ind
sqle-list_accum
sqle-list_accum-list_ind
sqle-list_ind-list_accum
sublist_accum
sum-as-accum
sum-as-accum-filter
sum-as-bag-accum
threshold_accum
threshold_accum_wf
unzip-as-accum

ACCUM2

prev top next

sum-as-accum2

ACCUMULATE

prev top next

local-prior-state-accumulate

ACT

prev top next

act_locl_lemma
alg_act
alg_act_is_rng_chom
alg_act_wf
algebra_act_times_lr
algebra_act_times_r
module_act_grp_hom_l
module_act_is_grp_hom
module_act_minus_l
module_act_minus_r
module_act_plus
module_act_zero_l
module_act_zero_r
ses-act
ses-act-has-atom
ses-act_wf

ACTION

prev top next

action_p
action_p_wf
comb_for_omral_action_wf
decidable__ses-action
lookup_omral_action
mod_action_mssum_l
mod_action_mssum_r
mod_action_when_l
mod_action_when_r
module_action_p
module_hom_action
omral_action
omral_action_inj
omral_action_one
omral_action_plus_l
omral_action_plus_r
omral_action_times
omral_action_times_r1
omral_action_times_r2
omral_action_wf
omral_dom_action
protocol-action
protocol-action_wf
same-action
same-action_wf
ses-action
ses-action_wf
ses-is-protocol-action
ses-is-protocol-action-useable
ses-is-protocol-action-used
ses-is-protocol-action_wf
ses-sign-is-protocol-action
sq_stable__action_p

ACTIONS

prev top next

ses-is-protocol-actions
ses-is-protocol-actions-fresh
ses-is-protocol-actions-legal
ses-is-protocol-actions_wf

ACTIVE

prev top next

pv11_p1_init_active
pv11_p1_init_active_wf
pv11_p1_ldr_active
pv11_p1_ldr_active_fun

ACTIVE2

prev top next

pv11_p1_ldr_active2

ACTOF

prev top next

actof
actof_wf

ACYCLIC

prev top next

acyclic-rel
acyclic-rel_wf
finite-acyclic-rel
lg-acyclic
lg-acyclic-has-source
lg-acyclic-remove
lg-acyclic-well-founded
lg-acyclic_wf
wellfounded-acyclic-rel

ADD

prev top next

Wmul-add-properties
add def
add-add-zero-in-top
add-associates
add-cause
add-cause_wf
add-commutes
add-cut-conditions
add-cut-conditions_wf
add-div-when-divides
add-div-when-divides2
add-fresh-cname
add-fresh-cname_wf
add-graph-decls
add-graph-decls-declares-tag
add-graph-decls_wf
add-indices
add-indices_wf
add-inverse
add-inverse-unique
add-inverse2
add-mul-special
add-nat
add-nat-missing
add-nat-missing-prop
add-nat-missing_wf
add-nonneg
add-nth
add-nth_wf
add-one-mod-2
add-plus-1-div-2-implies-lt
add-positive
add-positive-nonneg
add-remove-fresh-cname
add-remove-fresh-cname
add-remove-fresh-sq
add-remove-nth
add-swap
add-wf
add-wf-bar
add-wf-bar-int
add-wf-bar-nat
add-wf-partial
add-wf-partial-nat
add-zero
add-zero-base
add_cancel_in_eq
add_cancel_in_le
add_cancel_in_lt
add_com
add_eqmod_zero
add_functionality_wrt_eq
add_functionality_wrt_eqmod
add_functionality_wrt_le
add_functionality_wrt_lt
add_grp_of_rng
add_grp_of_rng_wf
add_grp_of_rng_wf_a
add_grp_of_rng_wf_b
add_ident
add_mono_wrt_eq
add_mono_wrt_eq_rw
add_mono_wrt_le
add_mono_wrt_le_rw
add_mono_wrt_lt
add_mono_wrt_lt_rw
add_nat_wf
add_reduce_eqmod
bag-rep-add
bag-summation-add
bdd-diff-add
can-apply-fun-exp-add
can-apply-fun-exp-add-iff
ci-add-graph
consensus-rel-add-knowledge-step
consensus-rel-add-knowledge-step_wf
continuous-add
continuous-add-ext
derivative-add
div_mul_add_cancel
divides-add
divides_add
equipollent-add
es-cut-add
es-cut-add-at
es-cut-add_wf
eu-add-length
eu-add-length-assoc
eu-add-length-between
eu-add-length-between-iff
eu-add-length-cancel-left
eu-add-length-cancel-right
eu-add-length-comm
eu-add-length-zero
eu-add-length-zero2
eu-add-length-zero3
eu-add-length_wf
exp_add
expectation-rv-add
expectation-rv-add-cubed
expectation-rv-add-fourth
expectation-rv-add-squared
fix-of-add
fpf-add-single
fpf-add-single_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-compose-add
fps-elim-x-add
fps-exp-add
fps-scalar-mul-rng-add
fps-set-to-one-add
fset-add
fset-add-remove
fset-add_wf
fset-size-add
fun_exp_add
fun_exp_add-sq
fun_exp_add_apply
fun_exp_add_apply1
fun_exp_add_sq
fun_exp_add_sq_again
general_add_assoc
general_add_com
imax_add_r
imin_add_r
int-add-exception
int-decr-map-add
int-decr-map-add-prop
int-decr-map-add_wf
int-to-ring-add
int_add_grp
int_add_grp_wf
int_add_grp_wf2
is-dag-add
isEven-add
isOdd-add
isOdd-isEven-add
le-add-cancel
le-add-cancel-alt
le-add-cancel2
le-add-cancel3
le-add-cancel4
le-add-shift
left_mul_add_distrib
lg-add
lg-add_wf
lg-add_wf_dag
lg-edge-add
lg-size-add
lifting-add-isaxiom-1
lifting-add-isaxiom-2
lifting-add-ispair-1
lifting-add-ispair-2
lifting-add-spread-1
lifting-add-spread-2
lookup-list-map-add
lookup-list-map-add-prop
lookup-list-map-add_wf
map-sig-add
map-sig-add_wf
member-cut-add
member-cut-add-at
member-fset-add
minus-add
mklist-add
mon_nat_op_add
mul_add_distrib
mvp-add
mvp-add_wf
nat_add_mon
nat_add_mon_wf
nat_add_mon_wf2
nat_op_add
nat_op_on_nat_add_mon
ndiff_add_eq_imax
new_23_sig_add_to_quorum
new_23_sig_add_to_quorum_wf
non-homogeneous-add
nysiad_add_to_bag
nysiad_add_to_bag_wf
nysiad_add_waiting
nysiad_add_waiting_wf
p-fun-exp-add
p-fun-exp-add-sq
pi-add
pi-add-comment
pi-add_wf
poset-cat-dist-add
primrec_add
pv11_p1_add_if_new
pv11_p1_add_if_new_if
pv11_p1_add_if_new_iff
pv11_p1_add_if_new_iff2
pv11_p1_add_if_new_wf
qadd-add
real-vec-add
real-vec-add_wf
reg-seq-add
reg-seq-add_functionality_wrt_bdd-diff
reg-seq-add_wf
reg-seq-list-add
reg-seq-list-add-as-l_sum
reg-seq-list-add_functionality_wrt_bdd-diff
reg-seq-list-add_functionality_wrt_permutation
reg-seq-list-add_wf
rel-exp-add-1-iff
rel-exp-add-iff
rel_exp_add
rel_exp_add-ext
rel_exp_add_iff
rnexp-add
rng_nat_op_add
rv-add
rv-add_wf
rv-disjoint-rv-add
rv-iid-add
rv-iid-add-const
select-add-indices
seq-add
seq-add_wf
seq-add_wf_consistent
set-sig-add
set-sig-add-prop
set-sig-add_wf
simple-primrec-add
sqequal_n_add
strictly-increasing-seq-add
strictness-add-left
strictness-add-right
subtype-add-fresh-cname
test-add-member-elim
upto_add_1
zero-add
zero-add-base
zero-add-sqle

ADD1

prev top next

eu-le-add1
fun_exp_add1
fun_exp_add1-sq
fun_exp_add1-sq2
fun_exp_add1_sub
fun_exp_apply_add1
mklist-add1
mklist-general-add1
mklist-general_add1
mklist_add1
p-fun-exp-add1-sq
rem_add1
triangular-num-add1

ADD2

prev top next

rv-disjoint-rv-add2

ADD2BAG

prev top next

nysiad_add2bag'base
nysiad_add2bag'base-program
nysiad_add2bag'base-program_wf
nysiad_add2bag'base_wf
nysiad_add2bag'send
nysiad_add2bag'send_wf
nysiad_on_add2bag
nysiad_on_add2bag_wf

ADDITION

prev top next

rem_addition

ADDITIONS

prev top next

test-arith-length-additions

ADDVOTE

prev top next

new_23_sig_addvote
new_23_sig_addvote_wf

ADDWAITING

prev top next

nysiad_addwaiting'base
nysiad_addwaiting'base-program
nysiad_addwaiting'base-program_wf
nysiad_addwaiting'base_wf
nysiad_addwaiting'send
nysiad_addwaiting'send_wf
nysiad_on_addwaiting
nysiad_on_addwaiting_wf

ADELIVER

prev top next

nysiad_adeliver'send
nysiad_adeliver'send_wf

ADJACENT

prev top next

A-adjacent-compatible
A-adjacent-compatible_wf
adjacent
adjacent-append
adjacent-before
adjacent-compatible
adjacent-compatible-iff
adjacent-compatible_wf
adjacent-cons
adjacent-frs-points
adjacent-full-partition-points
adjacent-member
adjacent-nil
adjacent-partition-points
adjacent-reverse
adjacent-run-states
adjacent-singleton
adjacent-sublist
adjacent-to-last
adjacent-to-same
adjacent-to-same-sublist
adjacent-to-same-sublist2
adjacent-to-same2
adjacent_wf
before-adjacent
flip-adjacent
swap_adjacent_decomp

ADJACENT2

prev top next

before-adjacent2

ADJOIN

prev top next

cc-adjoin-cube
cc-adjoin-cube-restriction
cc-adjoin-cube_wf
cc-fst-csm-adjoin
cc-snd-csm-adjoin
csm-adjoin
csm-adjoin-ap
csm-adjoin-fst-snd
csm-adjoin_wf
csm-id-adjoin
csm-id-adjoin-ap
csm-id-adjoin_wf
cube-context-adjoin
cube-context-adjoin_wf
seq-adjoin
seq-adjoin_wf

ADJUST

prev top next

reg-seq-adjust
reg-seq-adjust-property
reg-seq-adjust_wf

ADMISSABLE

prev top next

bag-admissable
bag-admissable-well-founded
bag-admissable_wf
sub-bag-admissable

ADOPTED

prev top next

pv11_p1-adopted
pv11_p1_adopted'base
pv11_p1_adopted'base-program
pv11_p1_adopted'base-program_wf
pv11_p1_adopted'base_wf
pv11_p1_adopted'send
pv11_p1_adopted'send_wf
pv11_p1_adopted_from_acceptor
pv11_p1_adopted_from_init_or_preempted
pv11_p1_adopted_from_maj_acceptors
pv11_p1_adopted_prior
pv11_p1_ldr_fun_mem_adopted
pv11_p1_ldr_fun_state_adopted_pred
pv11_p1_ldr_mem_adopted
pv11_p1_ldr_state_adopted_pred
pv11_p1_leader_adopted
pv11_p1_leader_adopted_wf
pv11_p1_unique_adopted
pv11_p1_unique_adopted_fun
pv11_p1_unique_adopted_fun2
pv11_p1_valid-adopted-message
pv11_p1_valid-adopted-message_wf
pv11_p1_when_adopted
pv11_p1_when_adopted_wf

AF

prev top next

AF-induction
AF-induction-iff
AF-induction2
AF-induction3
AF-induction4
AF-path-barred
AF-spread-law
AF-spread-law_wf
AF-uniform-induction
AF-uniform-induction2
AF-uniform-induction3
AF-uniform-induction4
AF-uniform-induction4-ext

AFBAR

prev top next

AFbar
AFbar_wf
at_AFbar
decidable__AFbar

AGAIN

prev top next

fun_exp_add_sq_again
page55-again

AGREE

prev top next

agree_on
agree_on_common
agree_on_common_append
agree_on_common_cons
agree_on_common_cons2
agree_on_common_filter
agree_on_common_iseg
agree_on_common_nil
agree_on_common_symmetry
agree_on_common_weakening
agree_on_common_wf
agree_on_equiv
agree_on_wf
eo-local-agree
eo-local-agree_wf
local-class-output-agree
pcw-step-agree
pcw-step-agree_wf

AGREE2

prev top next

local-class-output-agree2

AGREEMENT

prev top next

local-simulation-agreement
new_23_sig_agreement
pv11_p1-agreement

AGREEMENT2

prev top next

pv11_p1-agreement2

AGREES

prev top next

da-agrees
da-agrees-on
da-agrees-on_wf
da-agrees_wf
ds-agrees
ds-agrees-on
ds-agrees-on_wf
ds-agrees_wf

ALG

prev top next

Moessner-alg
Moessner-alg_wf
Paasche-alg-1
Paasche-alg-1_wf
Paasche-alg-2
Paasche-alg-2_wf
alg_act
alg_act_is_rng_chom
alg_act_wf
alg_car
alg_car_wf
alg_div
alg_div_wf
alg_eq
alg_eq_wf
alg_from_rng
alg_from_rng_wf
alg_hom_p
alg_hom_p_wf
alg_le
alg_le_wf
alg_minus
alg_minus_wf
alg_one
alg_one_wf
alg_p
alg_p_wf
alg_plus
alg_plus_wf
alg_times
alg_times_wf
alg_zero
alg_zero_wf
fma_alg
fma_alg_wf
fps-alg
fps-alg_wf
omral_alg
omral_alg_umap
omral_alg_umap_is_hom
omral_alg_umap_tri_comm
omral_alg_umap_unique
omral_alg_umap_wf
omral_alg_wf
omral_alg_wf2
polynom_alg
polynom_alg_wf
rng_of_alg
rng_of_alg_wf
rng_of_alg_wf2
rng_to_alg
rng_to_alg_wf
sq_stable__alg_hom_p

ALGEBRA

prev top next

algebra
algebra_act_times_lr
algebra_act_times_r
algebra_bilinear
algebra_hom
algebra_hom_properties
algebra_hom_wf
algebra_properties
algebra_sig
algebra_sig_inc
algebra_sig_wf
algebra_subtype_algebra_sig
algebra_subtype_module
algebra_times_assoc
algebra_times_one
algebra_wf
subtype_rel_algebra

ALGORITHM

prev top next

Longs-algorithm
Longs-algorithm_wf

ALIASES

prev top next

Editor aliases for Constructive Geometry

ALIST

prev top next

alist-domain-first
apply-Id-alist-function
apply-alist
apply-alist-cases
apply-alist-count-repeats
apply-alist-function
apply-alist-no_repeats
apply-alist_wf
apply-updated-alist
apply_alist_cons_lemma
fpf-as-apply-alist
isl-apply-alist
no_repeats-update-alist
remove-alist
remove-alist_wf
update-alist
update-alist_wf
weak-update-alist
weak-update-alist_wf

ALIST1

prev top next

member-update-alist1

ALL

prev top next

E_interface_all_events_lemma
all
all-but-one
all-large
all-large-and
all-large_wf
all-nsub2
all-union
all-unit
all_fset_elim
all_functionality_wrt_iff
all_functionality_wrt_implies
all_functionality_wrt_uiff
all_functionality_wrt_uimplies
all_mset_elim
all_quot_elim
all_rng_quot_elim
all_rng_quot_elim_a
all_safety
all_wf
assert-bag-all
assert-bag_all
assert-bdd-all
assert-bl-all
assert-bl-all-2
assert-deq-all-disjoint
b_all
b_all-cons
b_all-inst
b_all-map
b_all-map2
b_all-squash-exists-bag
b_all-squash-exists-bag2
b_all-squash-exists-list
b_all-wf2
b_all_wf
bag-all
bag-all_wf
bag-summation-equal-implies-all-equal
bag-summation-equal-implies-all-equal-1
bag_all
bag_all-cons
bag_all-empty
bag_all-map
bag_all_wf
bdd-all
bdd-all-btrue
bdd-all_wf
bdd_all_zero_lemma
before_all_imp_before
before_all_imp_count_zero
before_imp_before_all
bl-all
bl-all-as-accum
bl-all-btrue
bl-all_wf
callbyvalueall_seq-lambdas-all
callbyvalueall_seq-partial-ap-all
cbv-all-identity
classical-all
comb_for_l_all_wf
count-all
crng_all_properties
decidable__all-list
decidable__all_fset
decidable__all_int_seg
decidable__all_length
decidable__all_length_bool
decidable__l_all
decidable__l_all-better-extract
decidable__l_all-proof
deq-all-disjoint
deq-all-disjoint_wf
drng_all_properties
es-all-events
es-all-events_wf
firstn_all
fpf-all
fpf-all-empty
fpf-all-join-decl
fpf-all-single
fpf-all-single-decl
fpf-all_wf
fset-all
fset-all-iff
fset-all_wf
imon_all_properties
int_seg_decide_all
interface-predecessors-all-events
is-prior-all-events
l-all
l-all-and
l-all-and-property
l-all-and_wf
l-all-decider
l-all-decider_wf
l-all-iff
l-all-property
l-all_wf
l_all
l_all-cons
l_all-interface-predecessors
l_all-l_contains
l_all-map
l_all-mapfilter
l_all-mapfilter-interface-predecessors
l_all-nil
l_all-set
l_all-squash-exists-list
l_all_append
l_all_assert_iff_reduce
l_all_cons
l_all_exists_injection
l_all_exists_max
l_all_filter
l_all_from-upto
l_all_functionality
l_all_functionality_wrt_permutation
l_all_fwd
l_all_iff
l_all_implies_b_all
l_all_map
l_all_nil
l_all_nil_iff
l_all_not
l_all_reduce
l_all_since
l_all_since_wf
l_all_single
l_all_sublist
l_all_subtype
l_all_wf
l_all_wf2
l_all_wf_nil
lg-all
lg-all-append
lg-all-map
lg-all-remove
lg-all-wf_dag
lg-all_functionality
lg-all_wf
list_all
list_all_iff
list_all_wf
not-all-int_seg
not-assert-bl-all
not-bl-exists-eq-bl-all
not-l_all-dec
not_all_sqequal
per-all
per-all_wf
prior-val-all-events
rng_all_properties
rng_before_all_imp_before
rng_before_imp_before_all
single-valued-classrel-all
single-valued-classrel-all-implies-bag
single-valued-classrel-all_wf
sq-all-large
sq-all-large-and
sq-all-large_wf
sq_stable__all
sq_stable__l_all
subtype-l_all

ALL0

prev top next

callbyvalueall_seq-lambdas-all0
callbyvalueall_seq-partial-ap-all0

ALL2

prev top next

l_all2
l_all2_cons
l_all2_wf

ALLE

prev top next

alle-at
alle-at-iff
alle-at-not-first
alle-at_wf
alle-between1
alle-between1-false
alle-between1-not-first-since
alle-between1-trivial
alle-between1-true
alle-between1_functionality_wrt_iff
alle-between1_wf
alle-between2
alle-between2-false
alle-between2-not-first-since
alle-between2-true
alle-between2_functionality_wrt_iff
alle-between2_wf
alle-between3
alle-between3-false
alle-between3_wf
alle-ge
alle-ge_wf
alle-le
alle-le-iff
alle-le_wf
alle-lt
alle-lt-iff
alle-lt_wf
decidable__alle-between1
decidable__alle-between2
decidable__alle-le
decidable__alle-lt
eo-forward-alle-lt
es-pplus-alle-between2
not-alle-lt

ALLFUNCTIONALITY

prev top next

experimental-allFunctionality def

ALLOWED

prev top next

decl-set-read-allowed
flow-allowed
state-var-allowed
state-var-read-allowed
sudoku-allowed
sudoku-allowed_wf

ALMOST

prev top next

almost-full
almost-full
almost-full_wf
almost-full_wf
almost_full
almost_full0
almost_full_wf

ALT

prev top next

Riemann-sum-alt
Riemann-sum-alt-req
Riemann-sum-alt_wf
alt-Riemann-sums-cauchy
alt-Riemann-sums-converge
alt-Riemann-sums-converge-ext
alt-swap-spec
alt-swap-spec_wf2
co-alt
co-alt_wf
dec_alt_char
dec_alt_char_a
fix_wf_corec-alt-proof
idom_alt_char
l_member-alt-def
le-add-cancel-alt
new_23_sig_vote_with_ballot_first_alt
new_23_sig_vote_with_ballot_first_alt_wf
triangular-num-alt

ALT1

prev top next

classrel-classfun-res-alt1

ALT2

prev top next

classrel-classfun-res-alt2

ALTERNATING

prev top next

alternating-series-converges

AMBIVALENT

prev top next

cs-ambivalent
cs-ambivalent_wf
cs-ref-map3-ambivalent

AMESSAGE

prev top next

nysiad_Amessage-deq
nysiad_Amessage-deq_wf

ANCESTRAL

prev top next

ancestral-logic-example1
ancestral-logic-example1-ext
ancestral-logic-example2
ancestral-logic-example2-ext
ancestral-logic-induction
ancestral-logic-induction-ext
ancestral-logic-lemma1

AND

prev top next

all-large-and
and
and-iff
and_assoc
and_comm
and_false_l
and_false_r
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
and_preserved_by
and_preserved_by2
and_true_l
and_true_r
and_wf
assert-has-header-and-in-locs
assert-test-msg-header-and-loc
band-to-and
bor-to-and
classical-and
combine-list-rel-and
cond_safety_and
decidable-predicate-and
decidable__and
decidable__pa-is-new-and
divide-and-conquer
divide-and-conquer-ext
equiv_rel_and
exists_over_and_r
global-order-pairwise-compat-msg-and-classrel
has-header-and-in-locs
has-header-and-in-locs_wf
interleaves-and-gets-comment
ite_and_reduce
l-all-and
l-all-and-property
l-all-and_wf
mFOL-sequent-evidence_and
member-per-and
new_23_sig_vote_with_ballot_and_id
new_23_sig_vote_with_ballot_and_id-assert-classrel
new_23_sig_vote_with_ballot_and_id-assert-type
new_23_sig_vote_with_ballot_and_id-forward
new_23_sig_vote_with_ballot_and_id-if-classrel
new_23_sig_vote_with_ballot_and_id-if-snd
new_23_sig_vote_with_ballot_and_id-implies
new_23_sig_vote_with_ballot_and_id-snd
new_23_sig_vote_with_ballot_and_id_wf
not_over_and
not_over_and_b
or-to-and-by-cases
pa-is-new-and
pa-is-new-and_wf
per-and
per-and_wf
predicate-and
predicate-and_wf
prop_and
prop_and_wf
safety_and
sq-all-large-and
sq_stable__and
sq_stable_and_decidable
sq_stable_and_left_false
squash_and
system-strongly-realizes-and
test-msg-header-and-loc
test-msg-header-and-loc_wf

AND1

prev top next

system-strongly-realizes-and1

AND2

prev top next

decidable__and2

ANDREW

prev top next

andrew
andrew_wf

ANN

prev top next

ndiff_ann_l
zero_ann
zero_ann_a
zero_ann_b

ANOTHER

prev top next

decidable__cs-inning-committable-another

ANTECEDENTS

prev top next

num-antecedents
num-antecedents-fun_exp
num-antecedents-property
num-antecedents_wf

ANTI

prev top next

anti_sym
anti_sym_functionality_wrt_iff
anti_sym_shift
anti_sym_wf
divides_anti_sym
divides_anti_sym_n
less_than_anti-reflexive
ocmon_anti_sym
poset_anti_sym
sq_stable__anti_sym
st_anti_sym
st_anti_sym_wf
wellfounded-anti-reflexive
xxst_anti_sym
xxst_anti_sym_wf

ANTIREFLEXIVE

prev top next

Wless_antireflexive
es-causal-antireflexive
es-locl-antireflexive

ANTISYM

prev top next

bm_compare_antisym_le
comparison-antisym
rem_antisym

ANTISYMMETRIC

prev top next

es-causal-antisymmetric
es-le-antisymmetric

ANTISYMMETRY

prev top next

binrel_le_antisymmetry
cut-order_antisymmetry
es-causle_antisymmetry
es-le_antisymmetry
f-subset_antisymmetry
fun-connected_antisymmetry
grp_leq_antisymmetry
implies_antisymmetry
iseg_antisymmetry
l_before_antisymmetry
le_antisymmetry
le_antisymmetry_iff
lg-contains_antisymmetry
psub_antisymmetry
rleq_antisymmetry
set_leq_antisymmetry
sub-bag_antisymmetry
sublist_antisymmetry
uimplies_antisymmetry

ANY

prev top next

any def
any_divs_zero
any_field_is_integ_dom
one_divs_any

ANYPROP

prev top next

anyprop
anyprop_wf

AP

prev top next

ap-con
ap-con_wf
ap-tuple
ap-tuple-as-tuple
ap-tuple_wf
ap_fpf_restrict_lemma
bag-count-ap-map
base-process-class-program-ap
binrel_ap
binrel_ap_functionality_wrt_breqv
binrel_ap_wf
callbyvalueall_seq-partial-ap-all
callbyvalueall_seq-partial-ap-all0
class-ap
class-ap-val
class-ap-val-classrel
class-ap-val_wf
class-ap_wf
colist-fix-ap-partial
const_df_ap_lemma
csm-adjoin-ap
csm-ap
csm-ap-comp-term
csm-ap-comp-type
csm-ap-csm-comp
csm-ap-cubical-app
csm-ap-cubical-fst
csm-ap-cubical-lambda
csm-ap-cubical-pair
csm-ap-cubical-snd
csm-ap-id-term
csm-ap-id-type
csm-ap-restriction
csm-ap-term
csm-ap-term_wf
csm-ap-type
csm-ap-type_wf
csm-ap_wf
csm-cubical-type-ap-morph
csm-id-adjoin-ap
cubical-interval-ap
cubical-interval-ap_wf
cubical-type-ap-morph
cubical-type-ap-morph-comp
cubical-type-ap-morph-id
cubical-type-ap-morph_wf
cubical-type-ap-rename-one-equal
dataflow-ap
dataflow-ap_wf
det_ideal_ap_elim
disj_un_tr_ap_inl_lemma
disj_un_tr_ap_inr_lemma
es-dt-ap
fpf-ap
fpf-ap-compose
fpf-ap-equal
fpf-ap-single
fpf-ap_functionality
fpf-ap_wf
fpf-join-ap
fpf-join-ap-left
fpf-join-ap-sq
fpf-join-list-ap
fpf-join-list-ap-disjoint
fpf-normalize-ap
fpf-rename-ap
fpf-restrict-ap
fpf-union-join-ap
fpf_ap_compose_lemma
fpf_ap_pair_lemma
fpf_ap_single_lemma
free-from-atom-fpf-ap
genrec-ap
hdf-ap
hdf-ap-inl
hdf-ap-invariant
hdf-ap-invariant2
hdf-ap-only-headers
hdf-ap-only-headers2
hdf-ap-run
hdf-ap-single-valued-except
hdf-ap-single-valued-except2
hdf-ap_wf
hdf-base-ap
hdf-base-ap-fst
hdf-bind-ap
hdf-bind-gen-ap
hdf-bind-gen-ap-eq
hdf-compose1-ap
hdf-compose2-ap
hdf-parallel-ap
hdf-union-ap
hdf-until-ap
hdf-until-ap-fst
hdf-until-ap-snd
hdf_ap_halt_lemma
infix_ap
infix_ap_wf
lnk-decl-ap
local-class-ap-member
mk_fpf_ap_lemma
name-morph-ap
partial_ap
partial_ap_compose
partial_ap_gen
partial_ap_gen_wf
partial_ap_is_gen
partial_ap_of_partial_ap_gen
partial_ap_of_partial_ap_gen1
partial_ap_wf
r-ap
r-ap_functionality
r-ap_wf
rec_dataflow_ap_lemma
select_fun_ap
select_fun_ap_is_last1
select_fun_ap_wf
select_fun_last_partial_ap_gen1
sq_stable__ex_int_seg_ap
sq_stable__ex_int_upper_ap
stateless_dataflow_ap_lemma
test-hidden-ap
uext-ap-name

AP1

prev top next

select_fun_last_partial_ap1

AP2

prev top next

ap2-tuple
ap2-tuple-as-tuple
ap2-tuple_wf
ap2-tuple_wf_ntuple
fpf-join-list-ap2
fpf-rename-ap2
grp_op_ap2_functionality_wrt_massoc
grp_op_ap2_functionality_wrt_mdivides
map-tuple-ap2-tuple

APP

prev top next

app_perm
app_perm_wf
app_permf
app_permf_comp
app_permf_id
app_permf_wf
comb_for_app_permf_wf
csm-ap-cubical-app
cubical-app
cubical-app_wf
rev_app_cons_lemma
rev_app_nil_lemma

APPEND

prev top next

adjacent-append
agree_on_common_append
append
append-append-nil
append-cancellation
append-cancellation-right
append-factors
append-impossible
append-impossible2
append-nil
append-nil-sqle
append-normal-form
append-strict-1
append-tuple
append-tuple-one-one
append-tuple-shorten-tuple
append-tuple-simplify
append-tuple-simplify2
append-tuple-split-tuple
append-tuple-zero
append-tuple_wf
append-unroll
append_assoc
append_assoc_sq
append_back_nil
append_cancel
append_cancel_nil
append_cancel_wrt_permutation
append_comm
append_comm_1
append_firstn_lastn
append_firstn_lastn_sq
append_functionality_wrt_permr
append_functionality_wrt_permutation
append_interleaving
append_is_nil
append_is_nil_test
append_iseg
append_nil_sq
append_overlapping_sublists
append_rel
append_rel_wf
append_segment
append_split
append_split2
append_wf
archive-condition-append-init
archive-condition-append-vote
bag-append
bag-append-ac
bag-append-assoc
bag-append-assoc-comm
bag-append-assoc2
bag-append-cancel
bag-append-comm
bag-append-comm-assoc
bag-append-empty
bag-append-eq-empty
bag-append-equal-bag-rep
bag-append-ident
bag-append-is-empty
bag-append-is-single
bag-append-is-single-iff
bag-append-is-single-iff2
bag-append-no-repeats
bag-append-no-repeats1
bag-append-union
bag-append_wf
bag-bind-append
bag-co-restrict-append
bag-combine-append-empty
bag-combine-append-left
bag-combine-append-right
bag-combine-bag-append-empty
bag-count-append
bag-empty-append
bag-filter-append
bag-map-append
bag-map-append-empty
bag-mapfilter-append
bag-maximal?-append
bag-member-append
bag-member-implies-hd-append
bag-no-repeats-append
bag-null-append
bag-product-append
bag-remove-append
bag-remove-repeats-append
bag-restrict-append
bag-size-append
bag-subtract-append
bag-summation-append
bag-union-append
bag-val-append
bl-exists-append
bsublist_append_diff
callbyvalueall-single-append-nil
comb_for_append_wf
combine-list-append
compat-append
concat_append
cons-bag-as-append
cons_bag_append_lemma
count-append
count_append
cycle-append
data-stream-append
decide-append
deq-member-append
descending-append
empty_bag_append_lemma
es-hist-is-append
es-interface-events-append
es-interface-vals-append
eval_list-append-nil-is-eval_list
eval_list-sqle-append-nil
evalall-append-implies-list
evalall-append-implies-list-base
evalall-append-implies-rec-value
evalall-append-nil
evalall-append-sqle
filter_append
filter_append_sq
firstn-append
firstn_append
firstn_append_front
firstn_append_front_singleton
fps-product-append
fseg_append
fun-path-append
general-append-cancellation
has-value-append
has-value-append-nil
has-valueall-append-nil
hd-append
hd-append-sq
imax-list-append
int-bag-product-append
int-bag-sum-append
int-list-index-append
int-list-member-append
is-dag-append
isaxiom-append-nil
iseg-append-nth_tl
iseg-append-one
iseg_append
iseg_append_iff
iseg_append_length
iseg_append_single
islist-append-nil-is-list
islist-append-nil-sqequal-islist
ispair-or-isaxiom-append-nil
iterate-dataflow-append
iterate-hdf-append
l-ordered-append
l_all_append
l_before_append
l_before_append_front
l_before_append_iff
l_contains-append
l_contains_append
l_disjoint_append
l_exists_append
l_subset_append
l_sum-append
last_append
last_append_singleton
last_append_singleton_sq
last_index_append
last_singleton_append
length-append
length-rev-append
length_append
less-append
lg-all-append
lg-append
lg-append-assoc
lg-append-contains
lg-append-nil
lg-append_assoc
lg-append_wf
lg-append_wf_dag
lg-edge-append
lg-label-append
lg-nil-append
lg-size-append
list-accum-append
list-if-has-value-rev-append
list_accum_append
list_append_ind
list_append_singleton_ind
loc-on-path-append
map-append-empty
map-append-empty2
map-rev-append-top
map_append
map_append_sq
map_is_append
mapfilter-append
mem_append
member_append
mon_for_append
mon_reduce_append
mul-list-append
nd-append
nil-append
no_repeats-append
no_repeats_append
no_repeats_append_iff
nth_tl-append
nth_tl_append
null_append
p-first-append
pairwise-append
pi1-if-ispair-append-nil
pi2-if-ispair-append-nil
prod-if-ispair-append-nil
proper-iseg-append
proper-iseg-append-one
pv11_p1_append_news
pv11_p1_append_news_iff
pv11_p1_append_news_iff2
pv11_p1_append_news_wf
radd-list-append
reduce-append
rel-path-between-append
remove-repeats-append
remove-repeats-append-one
remove-repeats-append-one-member
remove-repeats-append-sq
rev-append
rev-append-append
rev-append-axiom
rev-append-pair
rev-append-property
rev-append-property-top
rev-append-property-top-sqle
rev-append-rev-append
rev-append_wf
reverse-append
reverse_append
reverse_append_sq
select-append
select-rev-append
select_append
select_append_back
select_append_front
seq-append
seq-append-assoc
seq-append-normalize
seq-append_wf
seq-append_wf_consistent
seq-normalize-append
shorten-tuple-append-tuple
single-bag-append-nil
single-valued-bag-append
sorted-by-append
split-tuple-append-tuple
spread-append
spread-bag-append
sqequal-append-cbva-weak2
sqequal-append-cbva-weak3
sqle-append-nil-if-has-value4
star-append
star-append-iff
star-append_wf
strict4-append
sub-bag-append-left
sub-bag-append-left2
sub-system-append
sublist_append
sublist_append_front
sum-map-append
sv-bag-only-append
system-append
system-append_wf
tuple-type-append-equipollent
weak_l_before_append_front
zip-append

APPEND0

prev top next

iseg_append0
seq-append0

APPEND1

prev top next

fun-path-append1
llex-append1
seq-append1
seq-append1-assoc
sorted-by-append1
sublist_append1
sum-map-append1

APPEND2

prev top next

bag-bind-append2
compat-append2
imax-list-append2
l_contains_append2
l_disjoint_append2
last_append2
sublist_append2

APPEND3

prev top next

l_contains_append3

APPEND4

prev top next

l_contains-append4

APPLIES

prev top next

mk_applies
mk_applies_fun
mk_applies_fun2
mk_applies_ite
mk_applies_lambdas
mk_applies_lambdas1
mk_applies_lambdas2
mk_applies_lambdas_fun
mk_applies_lambdas_fun0
mk_applies_lambdas_fun1
mk_applies_roll
mk_applies_split
mk_applies_unroll
mk_applies_wf

APPLY

prev top next

Process-apply
Process-apply_wf
apply def
apply-Id-alist-function
apply-alist
apply-alist-cases
apply-alist-count-repeats
apply-alist-function
apply-alist-no_repeats
apply-alist_wf
apply-bar
apply-bottom
apply-cycle-member
apply-cycle-non-member
apply-ifthenelse
apply-ifthenelse-pi1
apply-ifthenelse-pi1-eq
apply-ifthenelse-pi2
apply-ifthenelse-pi2-eq
apply-ifthenelse2
apply-nth
apply-nth_wf
apply-partial
apply-partial-indep
apply-spread
apply-strict-fun
apply-updated-alist
apply-wf-per
apply?
apply?_wf
apply_alist_cons_lemma
apply_gen
apply_gen_wf
apply_gen_wf2
apply_larger_list
apply_uncurry
apply_wf_type-function
callbyvalueall-apply
can-apply
can-apply-compose
can-apply-compose'
can-apply-compose-iff
can-apply-compose-sq
can-apply-es-search-back
can-apply-fun-exp
can-apply-fun-exp-add
can-apply-fun-exp-add-iff
can-apply-mu'
can-apply-p-co-filter
can-apply-p-co-restrict
can-apply-p-filter
can-apply-p-first
can-apply-p-lift
can-apply-p-restrict
can-apply_wf
conditional-apply
do-apply
do-apply-compose
do-apply-compose'
do-apply-mu'
do-apply-p-co-filter
do-apply-p-co-restrict
do-apply-p-filter
do-apply-p-first
do-apply-p-first-disjoint
do-apply-p-lift
do-apply-p-restrict
do-apply_wf
fpf-as-apply-alist
fun_exp_add_apply
fun_exp_apply_add1
has-valueall-apply
inl-do-apply
isl-apply-alist
lifting-apply-atom_eq
lifting-apply-callbyvalue
lifting-apply-callbyvalueall
lifting-apply-callbyvalueall
lifting-apply-decide
lifting-apply-int_eq
lifting-apply-isaxiom
lifting-apply-ispair
lifting-apply-less
lifting-apply-spread
oob-apply
oob-apply_wf
per-apply
per-apply_wf
per-function-type-apply
same-thread-do-apply
strictness-apply
t-sqle-apply
t-sqle-apply-dependent
test_stuck_apply
tf-apply
tf-apply_wf

APPLY1

prev top next

fun_exp_add_apply1
so_apply1

APPLY2

prev top next

callbyvalueall-apply2
so_apply2

APPLY3

prev top next

so_apply3

APPLY4

prev top next

so_apply4

APPLY5

prev top next

so_apply5

APPLY6

prev top next

so_apply6

APPLY7

prev top next

so_apply7

APPLY8

prev top next

so_apply8

APPROX

prev top next

Taylor-approx
Taylor-approx_functionality
Taylor-approx_wf
derivative-Taylor-approx
has-value-is-list-approx-is-type
i-approx
i-approx-approx
i-approx-closed
i-approx-compact
i-approx-containing2
i-approx-finite
i-approx-is-subinterval
i-approx-monotonic
i-approx-of-compact
i-approx-rep
i-approx-rep2
i-approx_wf
i-member-approx
is-list-approx
is-list-approx-step
is-list-approx_wf
neg-approx-of-nonneg-real
old-i-approx
rabs-approx
rational-approx
rational-approx-property
rational-approx-property-ext
rational-approx-property1
rational-approx-property2
rational-approx_wf
trivial-Taylor-approx

APPROX0

prev top next

is-list-approx0

APS

prev top next

count_aps

ARCHIMEDEAN

prev top next

r-archimedean
r-archimedean-rabs

ARCHIMEDEAN2

prev top next

r-archimedean2

ARCHIVE

prev top next

archive-condition
archive-condition-append-init
archive-condition-append-vote
archive-condition-innings
archive-condition-nil
archive-condition-one-one
archive-condition-single
archive-condition-threshold-accum
archive-condition_wf
archive-consensus-accum-num
archive-event
archive-event_wf
consensus-rel-knowledge-archive-step
consensus-rel-knowledge-archive-step_wf
consensus-ts5-archive-invariant
cs-archive-blocked
cs-archive-blocked_wf
decidable__archive-condition
decidable__cs-archive-blocked
three-cs-archive-condition
three-cs-archive-invariant

ARCHIVED

prev top next

consensus-ts4-archived-invariant
consensus-ts4-archived-stable
cs-archived
cs-archived-listable
cs-archived_wf
decidable__cs-archived

ARCHIVES

prev top next

consensus-accum-num-archives

ARG

prev top next

gcd_p_neg_arg
gcd_p_neg_arg_2
gcd_p_neg_arg_a
neg_mul_arg_bounds
pos_mul_arg_bounds
rec-bind-class-arg
rec-bind-class-arg_wf

ARGS

prev top next

gcd_eq_args
gcd_p_eq_args
rem_eq_args
rem_eq_args_z

ARITH

prev top next

arith-example1
arith-example2
general_arith_equation1
general_arith_equation2
sum_arith
test-arith
test-arith-length-additions
trivial-arith

ARITH1

prev top next

sum_arith1

ARITHMETIC

prev top next

fund-theorem-arithmetic

ARR

prev top next

Arr
Arr_wf
DVp_Array-arr
DVp_Array-arr_wf

ARRAY

prev top next

C_Array
C_Array-elem_vs_DVALp
C_Array-elems
C_Array-elems_wf
C_Array-length
C_Array-length_wf
C_Array?
C_Array?_wf
C_Array_vs_DVALp
C_Array_wf
DVp_Array
DVp_Array-arr
DVp_Array-arr_wf
DVp_Array-lower
DVp_Array-lower_wf
DVp_Array-upper
DVp_Array-upper_wf
DVp_Array?
DVp_Array?_wf
DVp_Array_wf
array
array-model
array-model-type
array-model-type_wf
array-model_wf
array-monad
array-monad'
array-monad'_wf
array-monad_wf
array_subtype
array_wf
fn_array
fn_array_wf
mk_array
mk_array_wf

ARROW

prev top next

cat-arrow
cat-arrow
cat-arrow_wf
cat-arrow_wf
functor-arrow
functor-arrow
functor-arrow-comp
functor-arrow-comp
functor-arrow-id
functor-arrow-id
functor-arrow_wf
functor-arrow_wf
member-poset-cat-arrow
poset-cat-arrow-cases
poset-cat-arrow-equals
poset-cat-arrow-filter-nil
poset-cat-arrow-flip
poset-cat-arrow-iff
poset-cat-arrow-not-equal
poset-cat-arrow-unique
poset-cat-arrow_subtype
trivial-void-arrow

ARROWS

prev top next

edge-arrows-commute
edge-arrows-commute_wf
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

ASSERT

prev top next

assert
assert-C_TYPE_eq
assert-b-exists
assert-bag-all
assert-bag-deq-member
assert-bag-eq
assert-bag-has-no-repeats
assert-bag-null
assert-bag-null-sq
assert-bag_all
assert-bdd-all
assert-bl-all
assert-bl-all-2
assert-bl-exists
assert-bl-exists2
assert-bnot
assert-co-w-null
assert-cs-is-committed
assert-cs-is-considering
assert-cs-is-decided
assert-dectt
assert-deq
assert-deq-all-disjoint
assert-deq-disjoint
assert-deq-fset-member
assert-deq-member
assert-deq-sub-bag
assert-eo-forward-first
assert-eq-cname
assert-eq-cname
assert-eq-id
assert-eq-knd
assert-eq-lnk
assert-eq_mFO
assert-equal-test
assert-es-ble
assert-es-ble-base
assert-es-bless
assert-es-eq-E
assert-es-eq-E-2
assert-es-eq-E-base
assert-es-first
assert-es-first-locl
assert-es-locless
assert-face-name-eq
assert-fpf-is-empty
assert-fset-null
assert-graph-rcvset
assert-has-header-and-in-locs
assert-has-src
assert-hasloc
assert-in-missing
assert-in-missing-iff
assert-in-missing-nat
assert-in-missing-nat-iff
assert-int-deq
assert-int-list-member
assert-int-palindrome-test
assert-is-filter-image
assert-is-qrep
assert-isEven
assert-isOdd
assert-is_prime
assert-isname
assert-isrcvl
assert-lg-is-source
assert-member-eclass
assert-member-nat-missing
assert-name-deq
assert-name_eq
assert-null-base
assert-pair-blex
assert-palindrome-test
assert-product-deq
assert-pushdown-test
assert-pushdownC-test
assert-qeq
assert-rcvd-inning-eq
assert-rcvd-inning-gt
assert-rcvset
assert-regular-upto
assert-ses-is-fresh
assert-ses-is-legal
assert-slow-int-palindrome-test
assert-test-msg-header-and-loc
assert-union-deq
assert_dec2bool
assert_elim
assert_equal
assert_functionality_wrt_bimplies
assert_functionality_wrt_uiff
assert_of_band
assert_of_band2
assert_of_bimplies
assert_of_bnot
assert_of_bor
assert_of_bpermr
assert_of_dset_eq
assert_of_eq_atom
assert_of_eq_atom1
assert_of_eq_atom2
assert_of_eq_bool
assert_of_eq_int
assert_of_eq_int_rw
assert_of_eq_list
assert_of_eq_mset
assert_of_eq_pair
assert_of_ff
assert_of_grp_blt
assert_of_le_int
assert_of_lt_int
assert_of_mon_eq
assert_of_null
assert_of_oal_blt
assert_of_oal_null
assert_of_rng_eq
assert_of_set_leq
assert_of_set_lt
assert_of_tt
assert_pushup_example
assert_wf
assert_witness
comb_for_assert_wf
decidable__assert
eqff_assert_2
eqff_to_assert
eqtt_assert_2
eqtt_to_assert
int-decr-map-isEmpty-assert
l_all_assert_iff_reduce
member-assert
member-decide-assert
neg_assert_of_eq_atom
neg_assert_of_eq_atom1
neg_assert_of_eq_int
new_23_sig_assert_newvote
new_23_sig_decided_with_id-assert-classrel
new_23_sig_decided_with_id-assert-type
new_23_sig_vote_with_ballot-assert-classrel
new_23_sig_vote_with_ballot-assert-type
new_23_sig_vote_with_ballot_and_id-assert-classrel
new_23_sig_vote_with_ballot_and_id-assert-type
new_23_sig_vote_with_ballot_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
not-assert
not-assert-bl-all
not-assert-bl-exists
not-assert-isname
not-isl-assert-isr
not-isr-assert-isl
not-not-assert
not_assert_elim
pv11_p1_eq_bnums-assert
safe-assert-deq
sq_stable__assert
sqeqff_to_assert
sqeqtt_to_assert
sqequal-ff-to-assert
sqequal-tt-to-assert
squash-assert

ASSIGN

prev top next

A-assign
A-assign_wf

ASSIGN2

prev top next

A-assign2
A-assign2_wf

ASSIGNMENT

prev top next

update-assignment
update-assignment_wf

ASSOC

prev top next

Wadd-assoc
Wmul-assoc
algebra_times_assoc
and_assoc
append_assoc
append_assoc_sq
assoc
assoc_reln
assoc_shift
assoc_wf
bag-append-assoc
bag-append-assoc-comm
bag-append-comm-assoc
bag-bind-assoc
bag-combine-assoc
bag-partitions-assoc
band_assoc
bind-class-assoc
bor-assoc
bor_assoc
cat-comp-assoc
cat-comp-assoc
comp_assoc
concat-map-assoc
csm-comp-assoc
equipollent-product-assoc
eu-add-length-assoc
fpf-join-assoc
fps-add-assoc
fps-mul-assoc
functor-comp-assoc
functor-comp-assoc
gcd_assoc
general_add_assoc
grp_inv_assoc
iabgrp_op_inv_assoc
iabgrp_op_inv_assoc_fps
imax_assoc
imin_assoc
lg-append-assoc
lg-append_assoc
lmax_assoc
lmin_assoc
module_plus_assoc
mon_assoc
mon_assoc_fps
mset_inter_assoc
mset_sum_assoc
mset_union_assoc
mul_assoc
mul_assoc_fps
name-comp-assoc
neg_assoc_fps
ni-max-assoc
ni-min-assoc
oal_merge_assoc
omral_plus_assoc
omral_times_assoc
omral_times_assoc_a
or_assoc
parallel-class-assoc
perm_assoc
perm_grp_inv_assoc
perm_mon_assoc
qmul_assoc
radd-assoc
radd-rminus-assoc
radd_assoc
reg-seq-mul-assoc
residue-mul-assoc
rmax-assoc
rmin-assoc
rmul-assoc
rmul_assoc
rng_plus_assoc
rng_plus_inv_assoc
rng_times_assoc
seq-append-assoc
seq-append1-assoc
sp-join-assoc
sp-meet-assoc
sq_stable__assoc
trans-comp-assoc
trans-comp-assoc

ASSOC2

prev top next

bag-append-assoc2
mdivisor_of_atom_is_assoc2

ASSOCED

prev top next

absval_assoced
assoced
assoced_elim
assoced_equiv_rel
assoced_functionality_wrt_assoced
assoced_inversion
assoced_nelim
assoced_transitivity
assoced_weakening
assoced_wf
comb_for_assoced_wf
decidable__assoced
divides-iff-gcd-assoced
divides_functionality_wrt_assoced
exp-assoced-one
exp_assoced
exp_functionality_wrt_assoced
gcd_p_functionality_wrt_assoced
mul-assoced-one
mul_cancel_in_assoced
multiply_functionality_wrt_assoced
neg_assoced

ASSOCIATES

prev top next

add-associates
mul-associates

ASSOCIATIVE

prev top next

A-associative
A-associative'
M-associative
fset-intersection-associative
fset-union-associative
p-compose-associative

AT

prev top next

alle-at
alle-at-iff
alle-at-not-first
alle-at_wf
at_AFbar
at_cWObar
class-at
class-at-es-sv
class-at-loc-bounded
class-at-program
class-at-program-eq-hdf
class-at-program-wf-hdf
class-at-program_wf
class-at-single-val
class-at_wf
classrel-at
constant-cubical-type-at
csm-type-at
cu-cube-family-Kan-type-at
cubical-sigma-at
cubical-term-at
cubical-term-at-morph
cubical-term-at_wf
cubical-type-at
cubical-type-at_wf
empty-cut-at
equal-cubical-identity-at
es-cut-add-at
es-cut-at
es-cut-at-property
es-cut-at-property1
es-cut-at_wf
es-empty-fset-at
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-fset-at
es-fset-at-loc
es-fset-at-property
es-fset-at_wf
es-fset-at_wf-interface
es-functional-class-at
es-functional-class-at_wf
es-functional-class-implies-at
es-interface-at
es-interface-at_wf
existse-at
existse-at_wf
filter-interface-predecessors-first-at
first-at-filter-interface-predecessors
first-at-filter-interface-predecessors-or
first-at-filter-interface-predecessors1
hdf-at-locs
hdf-at-locs_wf
interface-at-subtype
interface-at-val
is-interface-at
member-class-at
member-cut-add-at
member-interface-at
split-at-first
split-at-first-gap
split-at-first-gap-ext
split-at-first-rel

ATOM

prev top next

assert_of_eq_atom
atom def
atom-deq
atom-deq-aux
atom-deq_wf
atom-free-decl
atom-implies-ispair-right
atom-product-disjoint
atom-sdata
atom-sdata-has-atom
atom-sdata-not-pair
atom-sdata-not-pair2
atom-sdata-one-one
atom-sdata_wf
atom-test1
atom-value-type
atom-valueall-type
atom_dset
atom_dset_wf
atom_eq def
atom_eq_sq_normalize
atom_eq_wf
atom_sq
atom_subtype_base
decidable__atom_equal
decidable__atom_equal_1
decidable__atom_equal_2
decide-atom-if-has-value
encryption-key-free-from-atom
eq_atom
eq_atom-reflexive
eq_atom_eq_false_elim
eq_atom_eq_false_elim_sqequal
eq_atom_eq_true_elim
eq_atom_eq_true_elim_sqequal
eq_atom_wf
eq_atom_wf1
eq_atom_wf2
evalall-atom
fps-atom
fps-atom_wf
fps-compose-atom
fps-compose-atom-eq
fps-compose-atom-neq
fps-elim-x-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
id-sdata-has-atom
int-atom-disjoint
int-product-union-atom-disjoint
lifting-apply-atom_eq
lifting-callbyvalue-atom_eq
lifting-callbyvalueall-atom_eq
lifting-strict-atom_eq
lifting-strict-atom_eq1
lifting-strict-atom_eq2
mdivisor_of_atom_is_assoc2
neg_assert_of_eq_atom
not-atom-member-int
posint_atom_imp_prime
product-union-atom-disjoint
sdata-free-from-atom
sdata-has-atom
sdata-pair-free-from-atom
sdata-pair-has-atom
sdata_atoms_atom_lemma
sdata_pair_atom_lemma
ses-act-has-atom
ses-legal-thread-has-atom
ses-sign-has-atom
sq-decider-atom-deq
st-atom
st-atom-encrypt
st-atom_wf
strictness-atom_eq-left
strictness-atom_eq-right
union-atom-disjoint

ATOM1

prev top next

assert_of_eq_atom1
atom1-value-type
atom1-valueall-type
atom1_sq
atom1_subtype_base
eq_atom1_self
evalall-atom1
neg_assert_of_eq_atom1
strictness-atom1_eq-left
strictness-atom1_eq-right

ATOM2

prev top next

assert_of_eq_atom2
atom2-deq
atom2-deq-aux
atom2-deq_wf
atom2-value-type
atom2-valueall-type
atom2_sq
atom2_subtype_base
decide-atom2-if-has-value
eq_atom2_self
evalall-atom2
strictness-atom2_eq-left
strictness-atom2_eq-right

ATOMDEQ

prev top next

atomdeq_reduce_lemma

ATOMEQN

prev top next

atomeqn def

ATOMIC

prev top next

atomic
atomic-values
atomic-values-evalall
atomic-values_subtype_base
atomic-values_wf
atomic_char
atomic_imp_prime
atomic_wf
is-atomic
is-atomic_wf
mFO-dest-atomic
mFO-dest-atomic_wf
prime_imp_atomic

ATOMN

prev top next

atomn def
eq_atomn

ATOMS

prev top next

encryption-key-atoms
encryption-key-atoms_wf
member-useable-atoms
member-used-atoms
sdata-atoms
sdata-atoms_wf
sdata_atoms_atom_lemma
sdata_atoms_id_lemma
sdata_atoms_pair_lemma
ses-private-key-atoms
ses-public-key-atoms
ses-useable-atoms
ses-useable-atoms_wf
ses-used-atoms
ses-used-atoms_wf
st-atoms-distinct
st-atoms-distinct_wf
symmetric-key-atoms

ATTACH

prev top next

nat-inf-attach
nat-inf-attach-unit

AUTH

prev top next

es-info-auth
es-info-auth_wf

AUTHENTIC

prev top next

es-authentic
es-authentic_wf
make-Authentic-Msg
make-Authentic-Msg_wf
msg-authentic
msg-authentic_wf

AUTHENTICATION

prev top next

CR-authentication-theorem
CRX-authentication-theorem
NSL-authentication-property
NSL-authentication-property_wf
authentication
authentication_wf

AUTO

prev top next

funtype-auto-test-case

AUX

prev top next

Comm-process-q_aux
Comm-process-q_aux_wf
Moessner-aux
Moessner-aux_wf
atom-deq-aux
atom2-deq-aux
bag_remove1_aux
bag_remove1_aux_property
bag_remove1_aux_wf
bm_foldli_aux
bm_foldli_aux_wf
bool-deq-aux
bool-to-dcdr-aux
bool-to-neg-dcdr-aux
chrem_exists_aux
chrem_exists_aux_a
combinations_aux
combinations_aux_linear
combinations_aux_rem
combinations_aux_rem_property
combinations_aux_rem_wf
combinations_aux_wf
combinations_aux_wf_int
csm-aux
csm-aux_wf
filter-as-accum-aux
int-deq-aux
itop_aux_wf
length-map-index_aux
list-max-aux
list-max-aux-property
list-max-aux_wf
map-index_aux
map-index_aux_wf
mapfilter-as-accum-aux
member-f-union-aux
nat-deq-aux
pi-guarded-aux
pi-guarded-aux_wf
pi-rank-pi-simple-subst-aux
pi-simple-subst-aux
pi-simple-subst-aux_wf
pi-subst-aux
pi-subst-aux_wf
proper-divisor-aux
proper-divisor-aux_wf
sbcode_aux
select-indices-aux
select-indices-aux_wf
select-map-index_aux
select-tagged-indices-aux
select-tagged-indices-aux_wf
sum_aux
sum_aux-as-primrec
sum_aux_wf

AUX2

prev top next

filter-as-accum-aux2

AVOID

prev top next

mFOL-rename-bound-to-avoid
mFOL-rename-bound-to-avoid_wf

AVOIDS

prev top next

es-decl-set-avoids
es-decl-set-avoids-tag
es-decl-set-avoids-tag_wf
es-decl-set-avoids_wf

AWF

prev top next

awf
awf-example1
awf-example1_wf
awf-leaf
awf-leaf_wf
awf-solution
awf-solution_wf
awf-subtype
awf-system
awf-system-subtype
awf-system_wf
awf_sum
awf_sum_wf
awf_wf
unique-awf

AX

prev top next

ax_choice
dep_ax_choice
is-list-if-has-value-fun-ax-mem

AXIOM

prev top next

axiom def
axiom-choice-00-quot
axiom-choice-0X-quot
axiom-choice-1X-quot
axiom-choice-quot
axiom-list
axiom-listunion
decide-axiom-if-has-value
evalall-axiom
exception-not-axiom
hdf-with-state-pair-left-axiom
is-above-axiom
is_list_axiom_lemma
is_list_fun_axiom_lemma
map-axiom
non-axiom-list
non-axiom-listunion
not-axiom-member-int
pair-sq-axiom-wf
pi1-axiom
rev-append-axiom
ses-flow-axiom
ses-flow-axiom-ordering
ses-flow-axiom_wf
spread-axiom-sqequal-bottom

AXIOMS

prev top

eo_axioms
eo_axioms_wf
euclidean-axioms
euclidean-axioms_wf
event_ordering_axioms
pes-axioms
ses-axioms
ses-axioms-imply
ses-axioms_wf
sq_stable__eo_axioms
sq_stable_euclidean-axioms
sth-axioms