[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]
I
top next
I-cube
I-cube_wf
I-face
I-face_wf
I-path
I-path-morph
I-path-morph-comp
I-path-morph-id
I-path-morph_functionality
I-path-morph_wf
I-path-morph_wf2
I-path_wf
csm-I-path
cubical-nerve-I-cube
cubical-universe-I-cube
decidable__i-closed
decidable__i-finite
equal-I-paths
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-closed
i-closed-closed
i-closed-finite-rep
i-closed_wf
i-finite
i-finite_wf
i-length
i-length_wf
i-member
i-member-approx
i-member-between
i-member-compact
i-member-diff-bound
i-member-finite
i-member-finite-closed
i-member-iff
i-member-proper-iff
i-member-witness
i-member_functionality
i-member_wf
i-nonvoid
i-nonvoid_wf
i-real
i-real_wf
i-type
i-type-member
i-type_wf
i-witness
i-witness-property
i-witness_wf
member-i-type
old-i-approx
rmax-i-member
rmin-i-member
sq_stable__i-member
unit-cube-I-cube
IABGRP
prev top next
iabgrp
iabgrp_op_inv_assoc
iabgrp_op_inv_assoc_fps
iabgrp_properties
iabgrp_wf
IABMONOID
prev top next
abmonoid_subtype_iabmonoid
iabmonoid
iabmonoid_properties
iabmonoid_subtype_imon
iabmonoid_wf
ICOMB
prev top next
icomb
icomb_wf
ICOMPACT
prev top next
icompact
icompact-endpoints
icompact-endpoints-rleq
icompact-length-nonneg
icompact_wf
rccint-icompact
sq_stable__icompact
ID
prev top next
I-path-morph-id
Id
Id-has-value
Id-has-valueall
Id-valueall-type
Id_sq
Id_wf
Kan structure on Id_A a b
Kan_id_filler
Kan_id_filler_uniform
Kan_id_filler_wf
Kan_id_filler_wf1
The Type (Id_A a b)
app_permf_id
apply-Id-alist-function
assert-eq-id
bottom-sqequal-fix-id
cat-id
cat-id
cat-id_wf
cat-id_wf
comp_id_l
comp_id_mon
comp_id_mon_wf
comp_id_r
continuous-id
continuous-id
continuous-monotone-id
coprime_bezout_id
csm-Kan-id
csm-Kan-unit-cube-id
csm-ap-id-term
csm-ap-id-type
csm-id
csm-id-adjoin
csm-id-adjoin-ap
csm-id-adjoin_wf
csm-id-comp
csm-id_wf
cu-cube-restriction-id
cube-set-restriction-id
cube-set-restriction-when-id
cubical-id-box
cubical-id-box_wf
cubical-type-ap-morph-id
decidable__equal_Id
derivative-id
eq_id
eq_id_self
eq_id_test
eq_id_wf
extend_perm_over_id
extend_permf_over_id
face-map-comp-id
fix-of-id
fps-id-ucont
free-from-atom-Id
free-from-atom-Id-rw
free_abmon_endomorph_is_id
fun_exp-id
functor-arrow-id
functor-arrow-id
functor-comp-id
functor-comp-id
grp_id
grp_id_wf
grp_id_wf2
grp_inv_id
id-biject
id-deq
id-deq_wf
id-fun
id-fun-set
id-fun-subtype
id-fun_wf
id-graph
id-graph-edge
id-graph-edge-implies-member
id-graph-edge_wf
id-graph_wf
id-member-normal-form
id-morph
id-morph_wf
id-sdata
id-sdata-has-atom
id-sdata-not-pair
id-sdata-not-pair2
id-sdata-one-one
id-sdata_wf
id_functor
id_functor
id_functor_wf
id_functor_wf
id_increasing
id_perm
id_perm_wf
increasing_is_id
lift-id-face
lift-id-face_wf
lift-id-faces
lift-id-faces-wf
lift-id-faces_wf
listify_select_id
lookup_oal_eq_id
map-id
map-id-map
map_id
mdivides_id
mon_for_of_id
mon_hom_p_id
mon_nat_op_id
mon_when_of_id
monoid_hom_id
mset_for_of_id
mset_map_id
name-comp-id-left
name-comp-id-right
name-morph-extend-id
name-morph-flip-id
nat-id-fun-example
nat-id-fun-ext
ndiff_id_r
neg_id_fps
new_23_sig_decided_with_id
new_23_sig_decided_with_id-assert-classrel
new_23_sig_decided_with_id-assert-type
new_23_sig_decided_with_id_wf
new_23_sig_vote_with_ballot_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-id-sqle-bottom
not_id_sqeq_bottom
oal_merge_non_id_vals
oal_neg_non_id_vals
p-compose-id
p-id
p-id-compose
p-id_wf
pDVloc-id
pDVloc-id_wf
pDVloc_tag-id
pDVloc_tag-id_wf
perm_grp_inv_id
polymorphic-id-unique
polymorphic-id-unique-sq
poset-functor-id
poset-id-functor
poset_functor_extend_id
reduce-id
rename-one-extend-id
rotate-by-id
rotate-by-is-id
sdata_atoms_id_lemma
sdata_pair_id_lemma
select_listify_id
sq-id-fun
sq-id-fun_wf
subtype-iff-id-mem-fun
swap_id
trans-id-property
trans-id-property
txpose_perm_id
unit-cube-map-id
ID0
prev top next
coprime_bezout_id0
ID1
prev top next
coprime_bezout_id1
ID2
prev top next
coprime_bezout_id2
IDEAL
prev top next
det_ideal_ap_elim
det_ideal_defines_eqv
ideal
ideal-detach-equiv
ideal_defines_eqv
ideal_of_prime
ideal_p
ideal_p_wf
ideal_wf
max_ideal_p
max_ideal_p_wf
nsgrp_of_ideal
nsgrp_of_ideal_wf
one_ideal
one_ideal_wf
prime_ideal_p
prime_ideal_p_wf
princ_ideal
princ_ideal_mem_cond
princ_ideal_wf
quot_by_prime_ideal
sq_stable__ideal_p
sq_stable__prime_ideal
zero_ideal
zero_ideal_wf
IDEALS
prev top next
prime_ideals_in_int_ring
IDEMP
prev top next
list_accum-set-equal-idemp
ni-max-idemp
ni-min-idemp
sp-join-idemp
sp-meet-idemp
IDEMPOTENT
prev top next
band-idempotent
conditional-idempotent
es-interface-restrict-idempotent
face-map-idempotent
fpf-join-idempotent
fset-union-idempotent
imax-idempotent
modulus-idempotent
predicate_or_idempotent
rel_or_idempotent
rel_plus_idempotent
rmax-idempotent
rmin-idempotent
rmin-idempotent-eq
IDENT
prev top next
add_ident
bag-append-ident
bezout_ident
bezout_ident_n
cat-comp-ident
cat-comp-ident
ident
ident_mon_hom_shift
ident_wf
module_plus_ident
mon_ident
mon_ident_fps
mset_sum_ident_r
mset_union_ident_l
mset_union_ident_r
mul_ident
oal_nil_ident_l
oal_nil_ident_r
omral_times_ident_l
omral_times_ident_r
perm_ident
perm_mon_ident
qmul_ident
rmul-ident-div
sq_stable__ident
IDENTICALLY
prev top next
rv-identically-distributed
rv-identically-distributed_wf
IDENTITIES
prev top next
LTL-identities
IDENTITY
prev top next
Kan-cubical-identity
Kan-cubical-identity_wf
cbv-all-identity
continuous'-monotone-identity
csm-Kan-cubical-identity
csm-cubical-identity
cubical-identity
cubical-identity_wf
equal-cubical-identity-at
equipollent-identity
equipollent-identity-left
equipollent-identity-right
es-init-identity
eu-congruence-identity
eu-congruence-identity-sym
flip_identity
fps-compose-identity
identity
identity-functor
identity-functor_wf
identity-injection
identity-record+-update
identity-record-update
identity-trans
identity-trans
identity-trans_wf
identity-trans_wf
identity_wf
iota'-identity
iota-identity
ni-max-identity
ni-min-identity
permute_list-identity
IDENTITY1
prev top next
rmul-identity1
IDENTITY2
prev top next
eu-congruence-identity2
iota-identity2
IDENTITY3
prev top next
eu-congruence-identity3
IDLNK
prev top next
IdLnk
IdLnk_sq
IdLnk_wf
decidable__equal_IdLnk
free-from-atom-IdLnk
idlnk-deq
idlnk-deq_wf
IDOM
prev top next
idom_alt_char
IDX
prev top next
LV_Index-idx
LV_Index-idx_wf
idx
idx_wf
IF
prev top next
bag-combine-is-single-if
bag-remove-repeats-if-no-repeats
bag-subtract-member-if-no-repeats
bag-union-is-single-if
bm_insert_if_not_in
bm_insert_if_not_in_wf
decide-atom-if-has-value
decide-atom2-if-has-value
decide-axiom-if-has-value
decide-inl-if-has-value
decide-inr-if-has-value
decide-int-if-has-value
decide-isatom-if-has-value
decide-isatom2-if-has-value
decide-isaxiom-if-has-value
decide-isinl-if-has-value
decide-isinr-if-has-value
decide-isint-if-has-value
decide-islambda-if-has-value
decide-ispair-if-has-value
decide-lambda-if-has-value
decide-pair-if-has-value
decomp-map-if-has-value
es-before-is-nil-if-first
es-causl-if-pred
es-le-before-if-first
has-value-if-has-value-map
has-value-is-list-map-if-has-value-is-list
has-valueall-if-has-value-callbyvalueall
if-per-void
injection-if-compose-injection
is-list-btrue-if-list
is-list-if-has-value
is-list-if-has-value-decomp
is-list-if-has-value-ext
is-list-if-has-value-fun
is-list-if-has-value-fun-ax-mem
is-list-if-has-value-fun_wf
is-list-if-has-value-hv-prp
is-list-if-has-value-rec
is-list-if-has-value-rec-decomp
is-list-if-has-value-rec-map
is-list-if-has-value-rec-pair-bot
is-list-if-has-value-rec-snd
is-list-if-has-value-rec-subtype-unit
is-list-if-has-value-rec_wf
is-list-if-has-value_wf
isatom-bool-if-has-value
isatom1-bool-if-has-value
isatom2-bool-if-has-value
isaxiom-bool-if-bunion-unit-prod
isaxiom-bool-if-has-value
isinl-bool-if-has-value
isinr-bool-if-has-value
isint-bool-if-has-value
islambda-bool-if-has-value
ispair-bool-if-bunion-unit-prod
ispair-bool-if-co-list
ispair-bool-if-has-value
length-if-co-list-sq
length-in-bar-int-if-co-list
length-in-prop-if-co-list
length-nat-if-has-value
list-if-has-value-length
list-if-has-value-length2
list-if-has-value-list_ind
list-if-has-value-rev-append
new_23_sig_proposal_if_vote
new_23_sig_vote_with_ballot-if-classrel
new_23_sig_vote_with_ballot_and_id-if-classrel
new_23_sig_vote_with_ballot_and_id-if-snd
pi1-if-ispair-append-nil
pi2-if-ispair-append-nil
prod-if-ispair-append-nil
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
pv11_p1_max_bnum_if_leq
single-valued-bag-if-le1
skip-first-class-is-empty-if-first
sq_stable__is-list-if-has-value-fun
sqle-append-nil-if-has-value4
sub-bag-list-if-bag-no-repeats-sq
sub-bag-remove-if
sub-bag-remove-repeats-if-no-repeats
sublist-if-no_repeats
IFF
prev top next
AF-induction-iff
DNS-iff-not-not-GMP
Peirce's-law-iff-xmiddle
State-comb-exists-iff
State-loc-comb-non-empty-iff
adjacent-compatible-iff
all_functionality_wrt_iff
alle-at-iff
alle-between1_functionality_wrt_iff
alle-between2_functionality_wrt_iff
alle-le-iff
alle-lt-iff
and-iff
and_functionality_wrt_iff
antecedent-function_functionality_wrt_iff
antecedent-surjection_functionality_wrt_iff
anti_sym_functionality_wrt_iff
assert-in-missing-iff
assert-in-missing-nat-iff
bag-append-is-single-iff
bag-filter-empty-iff
bag-maximal?-iff
bag-member-empty-iff
bag-member-iff
bag-member-iff-hd
bag-member-iff-size
bag-member-iff-sq-list-member
bar-diverges-iff
bdd-diff-iff-eventual
bexists_iff_exists_nth
bigrel-iff
bij_iff_1_1_corr
biject-iff
biject-iff-inverse
can-apply-compose-iff
can-apply-fun-exp-add-iff
cand_functionality_wrt_iff
comb_for_iff_wf
compat-iff-common-iseg
connex_functionality_wrt_iff
connex_iff_trichot
converges-iff-cauchy
converges-iff-cauchy-ext
coprime_iff_ndivides
cut-order-iff
dec_iff_ex_bvfun
decidable__iff
dfan-iff-twkl!
disjoint-iff-null-intersection
distinct_iff_counts_le_one
divides-iff-factors
divides-iff-gcd
divides-iff-gcd-assoced
divides_iff_div_exact
divides_iff_rem_zero
double-negation-iff-xmiddle
empty-bag-iff-no-member
empty-bag-iff-size
eq_mset_iff_eq_counts
equipollent-iff-inverse-funs
equipollent-iff-list
equipollent-one-iff
equiv_rel_functionality_wrt_iff
equiv_rel_iff
es-E-interface_functionality-iff
es-blocl-iff
es-class-causal-rel-iff-bijection
es-first-at-since-iff
es-first-since_functionality_wrt_iff
es-fset-loc-iff
es-iff
es-iff_wf
es-info-make-Msg-iff
es-init-le-iff
es-interface-conditional-domain-iff
es-is-le-interface-iff
es-le-iff
es-le-iff-causle
es-local-pred-iff-es-p-local-pred
es-locl-iff
es-open-interval-ordered-iff
es-pplus_functionality_wrt_iff
es-propagation-rule-iff
es-propagation-rule-iff_wf
es-pstar-q_functionality_wrt_iff
eu-add-length-between-iff
eu-congruent-iff-length
eu-extend-equal-iff-congruent
eu-seg-congruent-iff-length
even-iff-not-odd
event-has*-iff
exists_functionality_wrt_iff
existse-before-iff
existse-between1_functionality_wrt_iff
existse-between2_functionality_wrt_iff
existse-between3_functionality_wrt_iff
existse-le-iff
exp-le-iff
ext-family-iff
fan-iff-dfan-bool
fan-iff-nwkl!
fan-iff-wkl!
finite-type-iff-list
first-member-iff
fpf-compatible-join-iff
fpf-compatible-single-iff
fpf-compatible-singles-iff
fps-Pascal-iff
free-from-atom-pair-iff
fset-all-iff
fset-some-iff
fun-connected-iff-fun_exp
fun-converges-iff-cauchy
global-class-iff-bounded-local-class
glues-iff
groupoid-square-commutes-iff
groupoid-square-commutes-iff
grp_leq_iff_lt_or_eq
guard_functionality_wrt_iff
has-value-is-list-map-iff-has-value-is-list
i-member-iff
i-member-proper-iff
iff
iff_functionality_wrt_iff
iff_imp_equal_bool
iff_preserves_decidability
iff_symmetry
iff_transitivity
iff_weakening_equal
iff_weakening_uiff
iff_wf
ifthenelse_functionality_wrt_iff
implies_functionality_wrt_iff
inv_funs-iff
is-prior-val-iff-prior-interface
iseg-iff-firstn
iseg_append_iff
isl-prior-iff
islist-iff-length-has-value
iterated-classrel-exists-iff
iterated-classrel-iff
iterated_classrel-exists-iff
l-all-iff
l_all_assert_iff_reduce
l_all_iff
l_all_nil_iff
l_before-es-before-iff
l_before-es-le-before-iff
l_before_append_iff
l_disjoint_nil_iff
l_exists_iff
l_member-iff-length-filter
le-iff-imax
le-iff-imin
le-iff-less-or-equal
le-iff-nonneg
le_antisymmetry_iff
length-one-iff
less-iff-le
less-iff-positive
linorder_functionality_wrt_iff
list_all_iff
list_extensionality_iff
markov-streamless-iff
markov-streamless-iff-not-not-enum
mem_iff_count_nzero
mem_iff_exists
mem_iff_mem_f
member-base-class_iff
member-eclass-iff-non-empty
member-eclass-iff-size
member-eclass-iff-size1
member-eclass-simple-comb-1-iff
member-eclass-simple-comb-2-iff
member-eclass-simple-loc-comb-1-iff
member-eclass-simple-loc-comb-2-iff
member-fset-image-iff
member_iff_sublist
modulus-equal-iff-eqmod
mset_mem_iff_count_nzero
nil-iff-no-member
no-classrel-iff-empty
no-repeats-iff-count
no_repeats-concat-iff
no_repeats_append_iff
no_repeats_iff
non_null_filter_iff
non_null_iff_length
not_functionality_wrt_iff
nwkl!-iff-twkl!-bool
oal_lt_iff_grp_lt
odd-iff-not-even
or_functionality_wrt_iff
order_functionality_wrt_iff
permr_iff_eq_counts
permr_iff_eq_counts_a
permutation-iff-count
permutation-iff-count1
permutation-nil-iff
poset-cat-arrow-iff
pv11_p1_add_if_new_iff
pv11_p1_append_news_iff
pv11_p1_pmax_desc_iff
pv11_p1_upd_desc_iff
rabs-difference-bound-iff
rabs-positive-iff
refl_functionality_wrt_iff
regular-less-iff
rel-exp-add-1-iff
rel-exp-add-iff
rel-immediate_functionality_wrt_iff
rel-star-iff-rel-plus
rel-star-iff-rel-plus-or
rel_exp-iff-path
rel_exp_add_iff
rel_exp_functionality_wrt_iff
rel_exp_iff
rel_plus-iff-path
rel_plus_functionality_wrt_iff
rel_plus_iff
rel_star-iff-path
rel_star_iff
remove-repeats-length-no-repeats-iff
req-iff-bdd-diff
req-iff-not-rneq
req-iff-rabs-rleq
rleq-iff
rleq-iff-not-rless
rleq-iff-rleq2
rleq2-iff-rnonneg2
rless-iff
rless-iff-large-diff
rless-iff-rleq
rless-iff-rpositive
rmul_reverses_rleq_iff
rmul_reverses_rless_iff
rneq-iff-rabs
rnexp-req-iff
rnexp-req-iff-even
rnexp-req-iff-odd
rnexp-rleq-iff
rnonneg-iff
rnonzero-iff
rpositive-iff
set_leq_iff_lt_or_eq
skip-first-class-property-iff
sq_or_functionality_wrt_iff
sq_stable__iff
sq_stable_iff_stable
sq_stable_iff_uimplies
square-iff-isqrt
squash_functionality_wrt_iff
star-append-iff
stream-lex-iff
stream-pointwise-iff
strong-subtype-iff-preserves-singleton
sub-bag-iff
sub-bag-no-repeats-iff
sublist-rec-iff-sublist
sublist-rec-nil-iff
subtype-iff-id-mem-fun
subtype_rel_b-union_iff
subtype_rel_dep_function_iff
subtype_rel_dep_product_iff
subtype_rel_functionality_wrt_iff
subtype_rel_list-iff
sup-iff-closure
sv-class-iff
sym_functionality_wrt_iff
trans_functionality_wrt_iff
uall_functionality_wrt_iff
uanti_sym_functionality_wrt_iff
uconnex_functionality_wrt_iff
uconnex_iff_trichot
uequiv_rel_functionality_wrt_iff
uequiv_rel_iff
uimplies-iff-squash-implies
ulinorder_functionality_wrt_iff
union_functionality_wrt_iff
uorder_functionality_wrt_iff
urefl_functionality_wrt_iff
usym_functionality_wrt_iff
utrans_functionality_wrt_iff
wellfounded_functionality_wrt_iff
wkl!-iff-nwkl!
wkl!-iff-twkl!-bool
xxconnex_iff_trichot
xxconnex_iff_trichot_a
IFF1
prev top next
cut-order-iff1
es-propagate-iff1
es-propagate-iff1_wf
IFF2
prev top next
bag-append-is-single-iff2
es-info-make-Msg-iff2
es-propagate-iff2
es-propagate-iff2_wf
fset-some-iff2
groupoid-square-commutes-iff2
groupoid-square-commutes-iff2
ifthenelse_functionality_wrt_iff2
pv11_p1_add_if_new_iff2
pv11_p1_append_news_iff2
rel_exp_iff2
rel_plus_iff2
rel_star_iff2
rless-iff2
rless-iff2-ext
IFF3
prev top next
ifthenelse_functionality_wrt_iff3
IFF4
prev top next
rleq-iff4
rless-iff4
IFF8
prev top next
rless-iff8
IFLIFT
prev top next
iflift_1
iflift_sq_1
IFTHENELSE
prev top next
apply-ifthenelse
apply-ifthenelse-pi1
apply-ifthenelse-pi1-eq
apply-ifthenelse-pi2
apply-ifthenelse-pi2-eq
bag-member-ifthenelse
branch-ifthenelse
callbyvalueall-ifthenelse
comb_for_ifthenelse_wf
conditional-ifthenelse
decide-ifthenelse
evalall-ifthenelse
has-value-ifthenelse
has-value-ifthenelse-type
ifthenelse
ifthenelse-as-band
ifthenelse-as-band-bnot
ifthenelse-as-bor
ifthenelse-as-bor-bnot
ifthenelse-false-left
ifthenelse-false-right
ifthenelse-inl
ifthenelse-inr
ifthenelse-prop
ifthenelse-simplify0
ifthenelse-simplify1
ifthenelse-simplify2
ifthenelse-simplify3
ifthenelse-wf
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
ifthenelse_sqequal
ifthenelse_sqle
ifthenelse_wf
ifthenelse_wf-partial
ifthenelse_wf-partial-base
int_eq-as-ifthenelse
less-as-ifthenelse
lifting-strict-ifthenelse
map-ifthenelse
push-spread-into-ifthenelse
reduce-ifthenelse
spread-ifthenelse
strictness-ifthenelse
trivial-ifthenelse
IFTHENELSE2
prev top next
apply-ifthenelse2
IFUNION
prev top next
ifunion
IGRP
prev top next
comb_for_perm_igrp_wf
grp_subtype_igrp
igrp
igrp_properties
igrp_wf
mk_igrp
mk_igrp_wf
perm_igrp
perm_igrp_wf
IID
prev top next
rv-iid
rv-iid-add
rv-iid-add-const
rv-iid_wf
ILF
prev top next
CLK-ilf
OARcast-ilf
new_23_sig-ilf
pv11_p1-ilf
IMAGE
prev top next
A-face-compatible-image
A-face-image
A-face-image_wf
A-face-name-image
A-open-box-image
A-open-box-image_wf
Q-Q-glued-self-image
Q-Q-glues-to-self-image
assert-is-filter-image
es-E-filter-image
es-E-interface-image
es-filter-image
es-filter-image-val
es-filter-image-val2
es-filter-image_wf
es-interface-image
es-interface-image-derived
es-interface-image-trivial
es-interface-image-val
es-interface-image_wf
es-interface-left-as-image
es-interface-right-as-image
es-is-filter-image
es-is-interface-image
face-compatible-image
face-image
face-image_wf
face-name-image
filter-image-interface-accum-equal
filter-image_functionality
fset-image
fset-image_wf
get_face_image
image-type_def
image-type_wf
interface-predecessors-filter-image
inv_image_ind
inv_image_ind_a
inv_image_ind_tp
is-filter-image-sq
length-open_box_image
member-fset-image
member-fset-image-iff
open_box_image
open_box_image_wf
prod-image-is-image
set-is-image
subtype_rel_image
sys-antecedent-filter-image
tunion-is-image
IMAGE2
prev top next
es-is-filter-image2
IMAX
prev top next
E-imax-class
absval-as-imax
absval-imax-difference
absval-sqequal-imax
comb_for_imax_wf
expectation-imax-list
imax
imax-bag
imax-bag-lb
imax-bag-ub
imax-bag_wf
imax-class
imax-class-lb
imax-class-val
imax-class_wf
imax-idempotent
imax-left
imax-list
imax-list-append
imax-list-append2
imax-list-as-reduce
imax-list-cons
imax-list-eq-implies
imax-list-filter-member
imax-list-is-nat
imax-list-lb
imax-list-member
imax-list-strict-lb
imax-list-subset
imax-list-ub
imax-list-unique
imax-list-unique2
imax-list_functionality
imax-list_wf
imax-right
imax-wf-bar
imax-wf-bar-nat
imax_add_r
imax_assoc
imax_com
imax_lb
imax_strict_lb
imax_strict_ub
imax_ub
imax_unfold
imax_wf
is-imax-class
le-iff-imax
list-max-imax-list
minus_imax
mul-imax
ndiff_add_eq_imax
prior-imax-class-lb
prior-imax-class-lb2
IMIN
prev top next
absval-imin-difference
comb_for_imin_wf
imin
imin_add_r
imin_assoc
imin_com
imin_lb
imin_ub
imin_unfold
imin_wf
le-iff-imin
minus_imin
mul-imin
ndiff_ndiff_eq_imin
IMMEDIATE
prev top next
rel-immediate
rel-immediate-exists
rel-immediate-preserves-order
rel-immediate-property
rel-immediate-rel-plus
rel-immediate_functionality_wrt_breqv
rel-immediate_functionality_wrt_iff
rel-immediate_wf
rel-is-immediate
rel-plus-rel-immediate
IMON
prev top next
iabmonoid_subtype_imon
imon
imon_all_properties
imon_properties
imon_subtype_grp_sig
imon_wf
lapp_imon
lapp_imon_wf
mk_imon
IMP
prev top next
atomic_imp_prime
before_all_imp_before
before_all_imp_count_zero
before_imp_before_all
bij_imp_exists_inv
eq_cons_imp_eq_hds
eq_cons_imp_eq_tls
iff_imp_equal_bool
irrefl_trans_imp_sasym
list_eq_imp_sqeq
massoc_imp_unit_diff
mcomp_imp_not_unit
mem_bsublist_imp
mprime_imp_matomic
non_munit_diff_imp_mpdivides
omon_lt_mono_imp_leq_mono
posint_atom_imp_prime
prime_imp_atomic
rng_before_all_imp_before
rng_before_imp_before_all
simplify-equal-imp
trans_imp_sp_trans
trans_imp_sp_trans_a
trans_imp_sp_trans_b
uni_sat_imp_in_uni_set
utrans_imp_sp_utrans
utrans_imp_sp_utrans_a
utrans_imp_sp_utrans_b
xxtrans_imp_sp_trans
IMPLEMENTED
prev top next
implemented-class
implemented-class_wf
IMPLIES
prev top next
Q-R-pre-preserving_functionality_wrt_implies
absval-implies-rneq
add-plus-1-div-2-implies-lt
all_functionality_wrt_implies
and_functionality_wrt_implies
atom-implies-ispair-right
bag-member-implies-hd-append
bag-no-repeats-implies-disjoint
bag-summation-equal-implies-all-equal
bag-summation-equal-implies-all-equal-1
base-type-family-implies
classical-implies
classrel-implies-classfun-res
classrel-implies-member
comb_for_rev_implies_wf
cond_rel_implies
cond_rel_implies_wf
condition-implies-le
connex_functionality_wrt_implies
continuous-implies-functional
converges-implies-bounded
cs-is-committed-implies
cs-is-considering-implies
cut-order-implies
decidable-implies-es-interface
decidable__implies
decidable__implies_better
decidable__pa-is-sign-implies
derivative-implies-decreasing
derivative-implies-increasing
descending-chain-barred-implies-wellfounded
dfan-implies-twkl!
eo-forward-causle-implies
eqmod-divides-implies
equal-implies-member-param-W
equal-in-subtype-implies
es-E-interface-subtype_rel-implies
es-first-at-implies
es-first-at-implies-first-at
es-first-implies
es-functional-class-implies-at
es-implies
es-implies_wf
es-info-type-implies
es-interface-implies-decidable
es-pplus_functionality_wrt_implies
es-pplus_functionality_wrt_rev_implies
es-pred-locl-implies-le
es-pstar-q_functionality_wrt_implies
es-pstar-q_functionality_wrt_rev_implies
es-sv-class-implies-single-valued-classrel
eu-between-eq-implies-colinear
eu-between-eq-implies-colinear2
eu-between-eq-implies-colinear3
eu-between-implies-between-eq
eu-congruent-between-implies-equal
evalall-append-implies-list
evalall-append-implies-list-base
evalall-append-implies-rec-value
even-implies
even-implies-two-times
even-succ-implies-not-even
exists_functionality_wrt_implies
fan+weak-continuity-implies-uniform-continuity
fan-implies-PFan
fan-implies-bar-sep
fan-implies-barred-not-unbounded
fan-implies-nwkl!-using-PFan
filter-interface-predecessors-lower-bound-implies
filter_is_nil_implies
finite-type-implies-finite
first-interface-implies-prior-interface
function-eq-implies
has-value-implies-dec-isatom
has-value-implies-dec-isatom-2
has-value-implies-dec-isatom2
has-value-implies-dec-isatom2-2
has-value-implies-dec-isaxiom
has-value-implies-dec-isaxiom-2
has-value-implies-dec-isinl
has-value-implies-dec-isinl-2
has-value-implies-dec-isinr
has-value-implies-dec-isinr-2
has-value-implies-dec-isint
has-value-implies-dec-isint-2
has-value-implies-dec-islambda
has-value-implies-dec-islambda-2
has-value-implies-dec-ispair
has-value-implies-dec-ispair-2
id-graph-edge-implies-member
ifthenelse_functionality_wrt_implies
ifthenelse_functionality_wrt_rev_implies
imax-list-eq-implies
implies
implies-bar-equal
implies-bigrel
implies-es-le-pred
implies-es-pred
implies-es-pred2
implies-filter-equal
implies-is-partition-choice
implies-normal-ds
implies-prop-truncation
implies-real
implies-regular
implies-strictly-increasing-seq
implies-wf
implies_antisymmetry
implies_functionality_wrt_iff
implies_functionality_wrt_implies
implies_transitivity
implies_weakening_uimplies
increasing_implies
increasing_implies_le
interleaving_implies_occurence
is-interface-conditional-implies
isatom-implies-not-isint
isatom-implies-not-ispair
isaxiom-implies
isaxiom-implies-not-isint
isaxiom-implies-sq
iseg-implies-global-order-iseg
iseg_implies_member
isinl-implies
isinl-implies-not-isatom
isinl-implies-not-isint
isinr-implies
isinr-implies-not-isatom
isinr-implies-not-isint
isint-implies-not-isatom
islist-implies-is-list
islocal-implies
ispair-implies
ispair-implies-not-isatom
ispair-implies-not-isint
ispair-implies-sq
isrcv-implies
l_all_implies_b_all
l_disjoint_intersection_implies
length-zero-implies-nil
length-zero-implies-sq-nil
lnk-decl-dom-implies
member-firstn-implies-member
member-implies-classrel
member-implies-null-eq-bfalse
member-nth-tl-implies-member
named-path-equal-implies
nat-strong-overt-implies-Markov
nequal-le-implies
new_23_sig_vote_with_ballot_and_id-implies
no-descending-chain-implies-wellfounded
non-empty-bag-implies-non-void
nonzero-on-implies
not-even-succ-implies-even
not-name_eq-implies-sq-bfalse
not-not-sig-to-W-implies-stable
not-same-parity-implies
not-same-parity-implies-even-odd
not_functionality_wrt_implies
not_over_implies
nwkl!-implies-fan
occurence_implies_interleaving
odd-implies
odd-implies-succ-two-times
or_functionality_wrt_implies
pa-is-sign-implies
pa-is-sign-implies_wf
pairwise-implies
per-union-implies-wf1
per-union-implies-wf2
pigeon-hole-implies
pigeon-hole-implies-ext
power-set-lift-well-founded-implies
predicate_equivalent_implies
predicate_implies
predicate_implies_reflexivity
predicate_implies_transitivity
predicate_implies_weakening
predicate_implies_wf
predicate_rev_implies
predicate_rev_implies_weakening
predicate_rev_implies_wf
proof-by-cont-implies-LEM
prop-truncation-implies
pv11_p1_leq_bnum_implies_eq
pv11_p1_leq_bnum_implies_eq_or_lt
pv11_p1_lt_bnum_implies_not
pv11_p1_lt_bnum_implies_not2
pv11_p1_lt_bnum_implies_not3
pv11_p1_pmax_desc_implies
radd-positive-implies
rel-restriction-implies
rel_exp_functionality_wrt_rel_implies
rel_implies
rel_implies_functionality
rel_implies_or_left
rel_implies_or_right
rel_implies_transitivity
rel_implies_weakening
rel_implies_wf
rel_plus_functionality_wrt_rel_implies
rel_plus_implies
rel_rev_implies
rel_rev_implies_weakening
rel_rev_implies_wf
rel_star_functionality_wrt_rel_implies
rem-zero-implies-minus
remove-combine-implies-member
remove-combine-implies-member2
remove-combine-l-ordered-implies-member
remove-first-member-implies
rev_implies
rev_implies_weakening_rev_uimplies
rev_implies_wf
rleq-implies
rleq_functionality_wrt_implies
rless-implies
rless-implies-rleq
rless_functionality_wrt_implies
rpositive-implies-rnonneg
same-parity-implies
same-parity-implies-even-odd
ses-D-implies
ses-flow-implies
ses-flow-implies'
ses-ordering-implies
single-valued-class-implies-hdf
single-valued-classrel-all-implies-bag
single-valued-classrel-implies-bag
sq_stable__implies
squash_functionality_wrt_implies
squash_thru_implies_dec
streamless-implies-not-not-enum
strong-continuity2-implies-uniform-continuity
strong-continuity2-implies-uniform-continuity-ext
strong-continuity2-implies-uniform-continuity-int
strong-continuity2-implies-uniform-continuity-nat
strong-continuity2-implies-uniform-continuity-nat-ext
strong-continuity2-implies-uniform-continuity2
strong-continuity2-implies-uniform-continuity2-int
strong-continuity2-implies-weak-skolem
strong-continuity2-implies-weak-skolem-cantor
strong-continuity2-implies-weak-skolem-cantor-nat
strong-message-constraint-implies-message-constraint
strong-message-constraint-no-rep-implies
strong-message-constraint-no-rep-large-implies
strong-subtype-implies
strongwf-implies
sub-bag-mapfilter-implies
subtype_rel_functionality_wrt_implies
system-equiv-implies-equal
totally-bounded-implies-nonvoid
twkl!-implies-dfan
uconnex_functionality_wrt_implies
uimplies-iff-squash-implies
unique-minimal-wellfounded-implies
weak-continuity-implies-strong1
weak-overt-implies-overt
wellfounded_functionality_wrt_implies
xmiddle-implies-stable
IMPLIES1
prev top next
bag-member-filter-implies1
strong-continuity-implies1
strong-continuity-implies1-sp
IMPLIES2
prev top next
bag-member-filter-implies2
filter_is_nil_implies2
ifthenelse_functionality_wrt_implies2
ifthenelse_functionality_wrt_rev_implies2
l_disjoint_intersection_implies2
rel_plus_implies2
strong-continuity-implies2
IMPLIES3
prev top next
ifthenelse_functionality_wrt_implies3
ifthenelse_functionality_wrt_rev_implies3
strong-continuity-implies3
IMPLIES4
prev top next
strong-continuity-implies4
IMPLIESFUNCTIONALITY
prev top next
experimental-impliesFunctionality def
IMPLY
prev top next
ses-axioms-imply
IMPOSSIBLE
prev top next
append-impossible
impossible-equation-by-eqmod
IMPOSSIBLE2
prev top next
append-impossible2
IN
prev top next
Theorem 6.2 in Bezem,Coquand,Huber
add-add-zero-in-top
add_cancel_in_eq
add_cancel_in_le
add_cancel_in_lt
assert-has-header-and-in-locs
assert-in-missing
assert-in-missing-iff
assert-in-missing-nat
assert-in-missing-nat-iff
bar-induction (dup of thm in list_1)
bm_insert_if_not_in
bm_insert_if_not_in_wf
bound_in_prefix
bound_in_prefix_wf
causal-class-rel-in-out
causal-class-rel-in-out_wf
compute-in-context
cons_in_oalist
cons_pr_in_oalist
cu-box-in-box
cu-box-in-box_wf
divisor-in-range
eo-forward-no-classrel-in-interval
equal-in-bar
equal-in-subtype-implies
equal-in-unit
es-in-port-conds
event_in_sv_classrel_is_in_class
expectation-monotone-in-first
free_in_prefix
free_in_prefix_wf
has-header-and-in-locs
has-header-and-in-locs_wf
in-bar
in-bar-converges
in-bar-equal
in-bar_wf
in-eclass
in-eclass_wf
in-first-eclass
in-missing
in-missing_wf
in-open
in-open-isect
in-open-union
in-open_wf
in-simple-loc-comb-1-concat
int-decr-map-find-not-in
int-eq-in-rationals
int-equal-in-rationals
l_member_in_subtype
l_member_in_subtype2
length-in-bar-int-if-co-list
length-in-prop-if-co-list
lg-in-edges
lg-in-edges_wf
list_in_mem_f_list
maximal-in-list
mul_cancel_in_assoced
mul_cancel_in_eq
mul_cancel_in_le
mul_cancel_in_lt
nil_in_oalist
no-classrel-in-interval
no-classrel-in-interval-trivial
no-classrel-in-interval_wf
oal_lk_in_dom
only_value_of_sv_class_in_classrel
prime_ideals_in_int_ring
prior-as-rec-bind-class-in
prior-as-rec-bind-class-in-property
prior-as-rec-bind-class-in_wf
prod_in_mset_prod
pv11_p1_in_domain
pv11_p1_in_domain_wf
run-event-in-transit
run-event-in-transit_wf
rv-disjoint-monotone-in-first
select-last-in-nat-missing
select-last-in-nat-missing_wf
sq_stable__no-classrel-in-interval
uni_sat_imp_in_uni_set
IN2
prev top next
prior-as-rec-bind-class-in2
prior-as-rec-bind-class-in2-property
prior-as-rec-bind-class-in2_wf
INC
prev top next
CLK_stric_inc
abdmonoid_inc
abmonoid_inc
algebra_sig_inc
event-ordering+_inc
fin_type_inc
grp_car_inc
grp_sig_inc
int-minus-comparison-inc
int-minus-comparison-inc_wf
int_inc
int_inc_rationals
int_seg_inc
mset_inc
mset_inc_a
nat_inc
nat_plus_inc
nat_plus_inc_int_nzero
nat_plus_inc_nat
new_23_sig_rounds_inc
new_23_sig_rounds_strict_inc
omon_inc
poset_sig_inc
pv11_p1_inc_acc
pv11_p1_inc_acc_bnum_fun
pv11_p1_inc_acc_pvals_fun
rng_sig_inc
set_car_inc
INC2
prev top next
CLK_strict_inc2
INCLUSION
prev top next
cantor-interval-inclusion
inclusion-partial
inclusion-partial2
INCLUSION2
prev top next
cantor-interval-inclusion2
INCOMPARABLE
prev top next
bag-incomparable
bag-incomparable_wf
nat-to-incomparable
nat-to-incomparable-property
nat-to-incomparable_wf
INCONSISTENT
prev top next
inconsistent-bool-eq
inconsistent-bool-eq2
inconsistent-bool-eq3
inconsistent-bool-eq4
INCR
prev top next
monotone-incr-chain
type-incr-chain
type-incr-chain-subtype
type-incr-chain_wf
INCREASES
prev top next
enumerate-increases
INCREASING
prev top next
compose_increasing
derivative-implies-increasing
disjoint_increasing_onto
es-increasing-sequence
es-increasing-sequence2
fact-increasing
fadd_increasing
frs-increasing
frs-increasing-non-dec
frs-increasing-separated-common-refinement
frs-increasing-sorted-by
frs-increasing_wf
fshift_increasing
fun_exp-increasing
id_increasing
implies-strictly-increasing-seq
increasing
increasing-on-interval
increasing-on-interval_wf
increasing_implies
increasing_implies_le
increasing_inj
increasing_is_id
increasing_le
increasing_lower_bound
increasing_split
increasing_wf
new_23_sig_increasing_max
strictly-increasing-on-interval
strictly-increasing-on-interval_wf
strictly-increasing-seq
strictly-increasing-seq-add
strictly-increasing-seq_wf
uniform-partition-increasing
IND
prev top next
C_DVALUEp_ind
C_DVALUEp_ind_wf
C_DVALUEp_ind_wf_simple
C_LVALUE_ind
C_LVALUE_ind_wf
C_LVALUE_ind_wf_simple
C_TYPE_ind
C_TYPE_ind_wf
C_TYPE_ind_wf_simple
MultiTree_ind
MultiTree_ind_wf
MultiTree_ind_wf_simple
PiDataVal_ind
PiDataVal_ind_pDVcontinue_lemma
PiDataVal_ind_pDVfire_lemma
PiDataVal_ind_pDVguards_lemma
PiDataVal_ind_pDVloc_lemma
PiDataVal_ind_pDVloc_tag_lemma
PiDataVal_ind_pDVmsg_lemma
PiDataVal_ind_pDVrequest_lemma
PiDataVal_ind_pDVselex_lemma
PiDataVal_ind_wf
RankEx1_ind
RankEx1_ind_wf
RankEx1_ind_wf_simple
RankEx2_ind
RankEx2_ind-unroll
RankEx2_ind_wf
RankEx2_ind_wf_simple
RankEx4_ind
RankEx4_ind_wf
RankEx4_ind_wf_simple
TC-ind
TC-ind-ext
binary-tree_ind
binary-tree_ind_wf
binary-tree_ind_wf_simple
binary_map_ind
binary_map_ind-wf2
binary_map_ind_wf
binary_map_ind_wf_simple
bool_ind
comp-nat-ind-ext
comp_nat_ind_a
comp_nat_ind_tp
complete_nat_ind
complete_nat_ind_with_y
complete_nat_measure_ind
formula_ind
formula_ind_wf
formula_ind_wf_simple
ind def
int_lower_ind
int_seg_ind
int_upper_ind
int_upper_ind_uniform
inv_image_ind
inv_image_ind_a
inv_image_ind_tp
l-ind
l-ind-sqequal-list_ind
l-ind_wf
l_ind_cons_lemma
l_ind_nil_lemma
l_tree_ind
l_tree_ind_wf
l_tree_ind_wf_simple
list-if-has-value-list_ind
list_append_ind
list_append_singleton_ind
list_ind
list_ind-as-fix
list_ind-general-wf
list_ind-wf-co-list-islist
list_ind-wf-co-list-islist2
list_ind_cons_lemma
list_ind_nil_lemma
list_ind_reverse
list_ind_reverse_unfold
list_ind_reverse_unfold1
list_ind_reverse_wf
list_ind_reverse_wf_dependent
list_ind_wf
list_pr_length_ind
mFOLRule_ind
mFOLRule_ind_wf
mFOLRule_ind_wf_simple
mFOL_ind
mFOL_ind_wf
mFOL_ind_wf_simple
mset_ind_a
nat_ind
nat_ind_a
oalist_ind
oalist_ind_a
oalist_pr_length_ind
omralist_ind_a
one_or_both_ind
one_or_both_ind_oobboth_lemma
one_or_both_ind_oobright_lemma
one_or_both_ind_wf
pi_prefix_ind
pi_prefix_ind_wf
pi_prefix_ind_wf_simple
pi_term_ind
pi_term_ind_wf
pi_term_ind_wf_simple
rec_ind def
sqequal-list_accum-list_ind
sqequal-list_ind
sqle-list_accum-list_ind
sqle-list_ind
sqle-list_ind-list_accum
tree_ind
tree_ind_wf
tree_ind_wf_simple
uniform_nat_measure_ind
INDEP
prev top next
apply-partial-indep
INDEPENDENT
prev top next
es-E-equality-univ-independent
INDEX
prev top next
C_LVALUE-proper-Index
LV_Index
LV_Index-idx
LV_Index-idx_wf
LV_Index-lval
LV_Index-lval_wf
LV_Index?
LV_Index?_wf
LV_Index_wf
count_index_pairs
count_index_pairs_wf
filter-index
filter-index_wf
first_index
first_index-positive
first_index_bounds
first_index_cons
first_index_equal
first_index_property
first_index_wf
index-split
index-split-permutation
index-split_property
index-split_wf
int-list-index
int-list-index-append
int-list-index-property
int-list-index_wf
isl-list-index
l_before_l_index
l_before_l_index_le
l_index
l_index_hd
l_index_wf
last_index
last_index_append
last_index_cons
last_index_property
last_index_wf
length-map-index
length-map-index_aux
list-index
list-index-cmp
list-index-cmp-zero
list-index-cmp_wf
list-index-property
list-index_wf
map-index
map-index_aux
map-index_aux_wf
map-index_wf
no_repeats_l_index
no_repeats_l_index-inj
no_repeats_mu_index
pDVmsg-index
pDVmsg-index_wf
round-robin-list-index
select-map-index
select-map-index_aux
select_l_index
INDEXED
prev top next
C_LVALUE-proper-Indexed
indexed-F-bisimulation
indexed-F-bisimulation_wf
indexed-coinduction-principle
INDICES
prev top next
accum-matching-indices
accum-matching-indices-comment
accum-matching-indices_wf
accum-matching-tagged-indices
accum-matching-tagged-indices_wf
add-indices
add-indices_wf
select-add-indices
select-indices
select-indices-aux
select-indices-aux_wf
select-indices_wf
select-tagged-indices
select-tagged-indices-aux
select-tagged-indices-aux_wf
select-tagged-indices_wf
split-by-indices
INDOM
prev top next
int-decr-map-inDom
int-decr-map-inDom-cons
int-decr-map-inDom-prop
int-decr-map-inDom-prop1
int-decr-map-inDom-prop2
int-decr-map-inDom_wf
lookup-list-map-inDom
lookup-list-map-inDom-prop
lookup-list-map-inDom_wf
map-sig-inDom
map-sig-inDom-prop
map-sig-inDom_wf
INDOMAIN
prev top next
bm_inDomain
bm_inDomain_wf
INDUCED
prev top next
safety_induced
INDUCTION
prev top next
AF-induction
AF-induction-iff
AF-uniform-induction
C_DVALUEp-induction
C_LVALUE-induction
C_TYPE-induction
MMTree-induction
MultiTree-induction
PiDataVal-induction
RankEx1-induction
RankEx2-induction
RankEx4-induction
Sudoku-induction
W-induction
W-induction-extract
W-measure-induction
W-type-induction
W-uniform-measure-induction
WfdSpread-induction
accum-induction
accum-induction-ext
accum-induction-factorial
accum-induction-lemma
accum_induction
ancestral-logic-induction
ancestral-logic-induction-ext
bag-induction
bar-induction
bar-induction (dup of thm in list_1)
bar_induction
basic-bar-induction
basic_bar_induction
basic_strong_bar_induction
bigrel-induction
bigrel-induction-monotone
binary-tree-induction
binary_map-induction
bool-bar-induction
bool_bar_induction
cWO-induction
cWO-induction-extract-sqequal
cWO-induction_1
cWO-induction_1-ext
complete-nat-induction
complete-nat-induction-ext
cont-induction
cont-induction-ext
cont-induction-factorial
cont-induction-lemma
cut-order-induction
def-cont-induction-lemma
def-cont-induction-lemma-ext
div_induction
div_induction-ext
div_nat_induction
div_nat_induction-ext
es-cut-induction
es-cut-induction-ordered
es-cut-induction-sq-stable
es-interval-induction
es-local-prior-state-induction
evodd-induction
fixpoint-induction
fixpoint-induction-bottom
fixpoint-induction-bottom-bar
fixpoint-induction-bottom-base
fixpoint-induction-bottom2
formula-induction
fset-induction
fun-connected-induction
fun-path-induction
integer-induction
l_tree-induction
last_induction
last_induction_accum
lexico_induction
list-functionality-induction
list_induction
locally-ranked-induction
mFOL-induction
mFOLRule-induction
one_or_both-induction
param-W-induction
perm_induction
perm_induction_a
perm_induction_b
pi_prefix-induction
pi_term-induction
primrec-induction
primrec-induction-factorial
prior-interface-induction
prior-val-induction
rec-nat-induction
ses-flow-induction
sqequal-induction-test1
strict-fun-connected-induction
strong-fun-connected-induction
tcWO-induction
tcWO-induction-ext
transitive-closure-induction
transitive-closure-induction-ext
tree-induction
ts-reachable-induction
uniform-comp-nat-induction
urec_induction
wfd-tree-induction
wfd-tree-induction
wfd-tree-induction-ext
INDUCTION1
prev top next
co-list-islist-induction1
monotone-bar-induction1
INDUCTION2
prev top next
AF-induction2
AF-uniform-induction2
C_TYPE-induction2
MTree-induction2
es-interval-induction2
evodd-induction2
evodd-induction2-ext
fixpoint-induction2
fun-connected-induction2
prior-val-induction2
ts-reachable-induction2
INDUCTION3
prev top next
AF-induction3
AF-uniform-induction3
C_TYPE-induction3
prior-val-induction3
ts-reachable-induction3
INDUCTION4
prev top next
AF-induction4
AF-uniform-induction4
AF-uniform-induction4-ext
INDUCTIVE
prev top next
stump'-inductive
INEQUALITY
prev top next
Markov-inequality
exp-difference-inequality
int-triangle-inequality
l_sum-triangle-inequality
l_sum-triangle-inequality-general
list_accum-triangle-inequality
r-triangle-inequality
INEQUALITY1
prev top next
Minkowski-inequality1
binomial-inequality1
choose-inequality1
rsum-triangle-inequality1
INEQUALITY2
prev top next
Minkowski-inequality2
int-triangle-inequality2
r-triangle-inequality2
rsum-triangle-inequality2
INF
prev top next
compact-nat-inf
equal-nat-inf-infinity
equal-nat-inf-infinity2
inf
inf-as-sup
inf-range
inf_wf
nat-inf
nat-inf-attach
nat-inf-attach-unit
nat-inf-infinity
nat-inf-infinity-new
nat-inf-infinity_wf
nat-inf_wf
not-ni-eventually-equal-inf
range-inf
range-inf-property
range-inf_wf
totally-bounded-inf
INFINITE
prev top next
infinite-deriv-seq
infinite-deriv-seq_wf
infinite-domain-example
infinite-domain-example-ext
infinite-tree
infinite-tree_wf
test-infinite-domain-example
weakly-infinite
weakly-infinite-cases
weakly-infinite_wf
INFINITESMAL
prev top next
infinitesmal-difference
infinitesmal-zero
INFINITY
prev top next
converges-to-infinity
converges-to-infinity_wf
equal-nat-inf-infinity
nat-inf-infinity
nat-inf-infinity-new
nat-inf-infinity_wf
INFINITY2
prev top next
equal-nat-inf-infinity2
INFIX
prev top next
infix_ap
infix_ap_wf
INFO
prev top next
eo-forward-equal-info-body
eo-forward-has-es-info-type
eo-forward-info
eo-forward-info-body
eo-forward-info-type
eo-strict-forward-info
equal-info-body
equal-info-body_wf
es-info
es-info-auth
es-info-auth_wf
es-info-body
es-info-body-equal
es-info-body_wf
es-info-make-Msg
es-info-make-Msg-iff
es-info-make-Msg-iff2
es-info-mk-extended-eo
es-info-mk-msg
es-info-type
es-info-type-implies
es-info-type_wf
es-info_wf
global-eo-info
global-eo-info-before
global-eo-info-le-before
has-es-info-type
has-es-info-type-is-msg-has-type
has-es-info-type-subtype
has-es-info-type_wf
info-delivered
info-delivered_wf
intransit-to-info
intransit-to-info_wf
list-eo-info
list-eo-info-before
list-eo-info-le-before
local-simulation-event-info
new_23_sig_round_info_classrel2
ranked-eo-info
ranked-eo-info-before
ranked-eo-info-le-before
run-info
run-info_wf
ses-info
ses-info-flow
ses-info-flow-exp_functionality
ses-info-flow_functionality
ses-info-flow_wf
ses-info_wf
sq_stable__equal-info-body
sq_stable__has-es-info-type
trivial-equal-info-body
INFORMATION
prev top next
fifo-information-flow
fifo-information-flow_wf
flow-graph-information-flow-relation
information-flow
information-flow-relation
information-flow-relation_wf
information-flow-to
information-flow-to_wf
information-flow_wf
solves-information-flow
solves-information-flow_wf
INHABITED
prev top next
Message-inhabited
bool-inhabited
inhabited-classrel
inhabited-classrel_wf
INIT
prev top next
OARcast_init_odstate
OARcast_init_odstate_wf
OARcast_oastate_init
OARcast_oastate_init_wf
archive-condition-append-init
callbyvalueall_seq-shift-init
es-first-init
es-init
es-init-elim
es-init-elim2
es-init-eq
es-init-forward
es-init-identity
es-init-le
es-init-le-iff
es-init-locl
es-init_wf
es-loc-init
int_consensus_init
int_consensus_init_wf
mk_lambdas-fun-shift-init
pv11_p1_adopted_from_init_or_preempted
pv11_p1_init_accepted
pv11_p1_init_accepted_wf
pv11_p1_init_acceptor
pv11_p1_init_acceptor_wf
pv11_p1_init_active
pv11_p1_init_active_wf
pv11_p1_init_ballot_num
pv11_p1_init_ballot_num_wf
pv11_p1_init_leader
pv11_p1_init_leader_wf
pv11_p1_init_proposals
pv11_p1_init_proposals_wf
pv11_p1_init_pvalues
pv11_p1_init_pvalues_wf
pv11_p1_init_scout
pv11_p1_init_scout_wf
pv11_p1_init_slot_num
pv11_p1_init_slot_num_wf
ts-init
ts-init_wf
ts-init_wf_reachable
INIT0
prev top next
callbyvalueall_seq-shift-init0
INITIAL
prev top next
cs-initial
cs-initial-rcv
cs-initial-rcv_wf
cs-initial_wf
decidable__equal_cs-initial
mul-initial-seg
mul-initial-seg-property
mul-initial-seg-property2
mul-initial-seg-step
mul-initial-seg_wf
std-initial
std-initial-property
std-initial_wf
INITIALIZATION
prev top next
run-initialization
run-initialization-property
run-initialization_wf
INITIALSYSTEM
prev top next
InitialSystem
InitialSystem_wf
INITIATOR1
prev top next
CR-initiator1
CR-initiator1_wf
NSL-initiator1
NSL-initiator1_wf
INITIATOR2
prev top next
CR-initiator2
CR-initiator2_wf
NSL-initiator2
NSL-initiator2_wf
INITIATOR3
prev top next
CR-initiator3
CR-initiator3_wf
NSL-initiator3
NSL-initiator3_wf
INITIATOR4
prev top next
CR-initiator4
CR-initiator4_wf
INJ
prev top next
comb_for_mset_inj_wf
comb_for_mset_inj_wf_f
comb_for_oal_inj_wf
comb_for_omral_inj_wf
fabgrp_inj
fabgrp_inj_wf
fma_inj
fma_inj_wf
free_abmon_inj
free_abmon_inj_wf
gcopower_inj
gcopower_inj_wf
increasing_inj
inj_into_ocmon
inj_mon_hom
inj_mon_hom_properties
inj_mon_hom_wf
kind-rename-inj
lookup_oal_inj
lookup_omral_inj
mcopower_inj
mcopower_inj_is_hom
mcopower_inj_wf
mon_hom_inj_p
mon_hom_inj_p_wf
mset_count_inj
mset_for_inj_lemma
mset_for_mset_inj
mset_inj
mset_inj_wf
mset_inj_wf_f
mset_mem_inj_sum_lemma
no_repeats_l_index-inj
oal_dom_inj
oal_inj
oal_inj_mon_hom
oal_inj_wf
omral_action_inj
omral_dom_inj
omral_inj
omral_inj_mon_op
omral_inj_wf
perm_b_inj
perm_f_inj
sublist_map_inj
type_inj
type_inj_wf_for_qrng
type_inj_wf_for_quot
INJECT
prev top next
bag-inject
bag-inject_wf
decidable__inject-finite-type
inject
inject-compose
inject-composes
inject_functionality
inject_wf
inv-rel-inject
name-morph-domain-inject
no_repeats_inject
not-inject
p-compose-inject
p-inject
p-inject_wf
sq_stable__inject
INJECTION
prev top next
compose_wf-injection
cycle-injection
finite-injection
flip-injection
fun_exp-injection
identity-injection
injection
injection-bijection
injection-composition
injection-eta
injection-if-compose-injection
injection-inverse
injection-inverse2
injection-is-surjection
injection_le
injection_wf
l_all_exists_injection
list-injection
nat2inf-injection
p-fun-exp-injection
prime-product-injection
rotate-by-injection
rotate-injection
INJECTIONS
prev top next
compose-injections
injections-combinations
INL
prev top next
bag-diff-equal-inl
band-inl
band-is-inl
band-is-inl-base
band-sqequal-inl
bnot-inl
bor-inl
case_inl
decide-inl-if-has-value
disj_un_tr_ap_inl_lemma
evalall-inl
has-valueall-inl
hdf-ap-inl
hdf-halted-inl
hdf-out-inl
hdf_halted_inl_red_lemma
ifthenelse-inl
inl def
inl-class
inl-class_wf
inl-do-apply
inl-eta
inl-inr-disjoint
inl-one-one
inl_eq_btrue
inl_eq_inr
inl_equal
inr-inl-disjoint
inr_eq_inl
is-above-inl
lifting-callbyvalueall-inl
name_eq-is-inl
not-inl-sqeq-inr
INNER
prev top next
eu-between-eq-inner-trans
eu-inner-five-segment
eu-inner-pasch
eu-inner-pasch-property
eu-inner-pasch_wf
eu-inner-three-segment
not-not-inner-pasch
strong-continuity2-no-inner-squash
strong-continuity2-no-inner-squash-cantor
strong-continuity2-no-inner-squash-cantor2
strong-continuity2-no-inner-squash-cantor3
strong-continuity2-no-inner-squash-cantor4
strong-continuity2-no-inner-squash-cantor5
strong-continuity2-no-inner-squash-unique
INNING
prev top next
assert-rcvd-inning-eq
assert-rcvd-inning-gt
consensus-rel-knowledge-inning-step
consensus-rel-knowledge-inning-step_wf
consensus-ts4-inning-committed-stable
consensus-ts4-inning-rel
cs-inning
cs-inning-committable
cs-inning-committable-some1
cs-inning-committable-some2
cs-inning-committable-step
cs-inning-committable_wf
cs-inning-committed
cs-inning-committed-committable
cs-inning-committed-single
cs-inning-committed-single-stable
cs-inning-committed-some1
cs-inning-committed_wf
cs-inning_wf
decidable__cs-inning-committable
decidable__cs-inning-committable-another
decidable__cs-inning-committable-some
decidable__cs-inning-committed
decidable__cs-inning-committed-some
decidable__cs-inning-two-committable
fresh-inning-reachable
inning-event
inning-event_wf
is-inning-event
is-inning-event_wf
member-votes-from-inning
rcvd-inning-eq
rcvd-inning-eq_wf
rcvd-inning-gt
rcvd-inning-gt_wf
votes-from-inning
votes-from-inning-is-nil
votes-from-inning_wf
INNING0
prev top next
committed-inning0-reachable
INNINGS
prev top next
archive-condition-innings
rcvd-innings-nil
INORM
prev top next
Inorm
Inorm-bound
Inorm_wf
INPUT
prev top next
local-simulation-input-consistency
local-simulation-input-consistency_wf
local-simulation-input-validity
local-simulation-input-validity_wf
loop-class-memory-no-input
nysiad_on_input_message_bag
nysiad_on_input_message_bag_wf
nysiad_on_input_queue
nysiad_on_input_queue_wf
INPUTMSG
prev top next
nysiad_inputmsg'base
nysiad_inputmsg'base-program
nysiad_inputmsg'base-program_wf
nysiad_inputmsg'base_wf
INPUTQUEUE
prev top next
nysiad_InputQueue
nysiad_InputQueue-program
nysiad_InputQueue-program_wf
nysiad_InputQueue_wf
INPUTS
prev top next
CLK_headers_no_inputs
CLK_headers_no_inputs_types
CLK_headers_no_inputs_types_wf
CLK_headers_no_inputs_wf
OARcast_headers_no_inputs
OARcast_headers_no_inputs_types
OARcast_headers_no_inputs_types_wf
OARcast_headers_no_inputs_wf
base-process-inputs
base-process-inputs-non-null
base-process-inputs_wf
iseg-local-simulation-inputs
local-simulation-inputs
local-simulation-inputs_wf
member-local-simulation-inputs
new_23_sig_headers_no_inputs
new_23_sig_headers_no_inputs_types
new_23_sig_headers_no_inputs_types_wf
new_23_sig_headers_no_inputs_wf
nysiad_headers_no_inputs
nysiad_headers_no_inputs_types
nysiad_headers_no_inputs_types_wf
nysiad_headers_no_inputs_wf
pv11_p1_headers_no_inputs
pv11_p1_headers_no_inputs_types
pv11_p1_headers_no_inputs_types_wf
pv11_p1_headers_no_inputs_wf
sequential-composition-inputs
sequential-composition-inputs_wf
INR
prev top next
band-inr
bnot-inr
bor-inr
case_inr
decide-inr-if-has-value
disj_un_tr_ap_inr_lemma
evalall-inr
has-valueall-inr
hdf-halted-is-inr
ifthenelse-inr
inl-inr-disjoint
inl_eq_inr
inr def
inr-class
inr-class_wf
inr-eta
inr-inl-disjoint
inr-one-one
inr_eq_bfalse
inr_eq_inl
inr_equal
is-above-inr
lifting-callbyvalueall-inr
not-inl-sqeq-inr
priority-select-inr
INS
prev top next
bm_unionWith_ins
bm_unionWith_ins_wf
INSERT
prev top next
bm_insert
bm_insert'
bm_insert'_wf
bm_insert_if_not_in
bm_insert_if_not_in_wf
bm_insert_wf
insert
insert-by
insert-by-no-repeats
insert-by-sorted-by
insert-by_wf
insert-cases
insert-cases2
insert-combine
insert-combine-cons
insert-combine-nil
insert-combine-sorted-by
insert-combine_wf
insert-int
insert-int_wf
insert-no-combine
insert-no-combine-permutation
insert-no-combine-sorted-by
insert-no-combine_wf
insert-not-nil
insert-ordered-message
insert-ordered-message_wf
insert_nil_lemma
insert_property
insert_wf
l-ordered-insert-combine
member-insert
member-insert-by
member-insert-combine
member-insert-combine2
member-insert-no-combine
member-s-insert
mul-list-insert-int
no_repeats-insert
s-insert
s-insert-no-repeats
s-insert-sorted
s-insert_wf
INST
prev top next
b_all-inst
es-open-interval-ordered-inst
l-ordered-inst
nysiad-inst-msg-fun
nysiad-inst-msg-fun_wf
pi-example-inst
pi-example-inst_wf
INSTANCE
prev top next
divides_instance
uall_instance_test
INT
prev top next
C_Int
C_Int?
C_Int?_wf
C_Int_wf
DVp_Int
DVp_Int-int
DVp_Int-int_wf
DVp_Int?
DVp_Int?_wf
DVp_Int_wf
add-wf-bar-int
assert-int-deq
assert-int-list-member
assert-int-palindrome-test
assert-slow-int-palindrome-test
assert_of_eq_int
assert_of_eq_int_rw
assert_of_le_int
assert_of_lt_int
bag-summation-constant-int
band-simple-int_eq
bdd-diff-regular-int-seq
bigger-int
bigger-int-property
bigger-int-property2
bigger-int_wf
binomial-int
bm_compare_int
bm_compare_int_wf
bnot_of_le_int
bnot_of_lt_int
cantor-to-int-uniform-continuity
cardinality-le-int_seg
comb_for_int_op_wf
comb_for_int_seg_wf
comb_for_int_upper_wf
comb_for_lt_int_wf
combinations_aux_wf_int
combinations_wf_int
decidable-cantor-to-int
decidable-cantor-to-int-ext
decidable-exists-int_seg-subtype
decidable-finite-cantor-to-int
decidable__all_int_seg
decidable__equal_int
decidable__equal_int_seg
decidable__exists_int_seg
decidable__int_equal
decidable__rless-int-fractions
decide-int-if-has-value
decide-simple-int_eq
eq_int
eq_int-wf-bar
eq_int-wf-bar-int
eq_int-wf-partial
eq_int-wf-partial2
eq_int_cases_test
eq_int_eq_false
eq_int_eq_false_elim
eq_int_eq_false_elim_sqequal
eq_int_eq_false_intro
eq_int_eq_true
eq_int_eq_true_elim
eq_int_eq_true_elim_sqequal
eq_int_eq_true_intro
eq_int_wf
equipollent-int-nat
equipollent-int_mod
equipollent-int_seg
equipollent-int_upper-nat
evalall-int
extd-nameset_subtype_int
finite-type-int_seg
free-from-atom-int
fun-not-int
function-not-int
gen-divisors-sum-int-ring
has-value-length-member-int
insert-int
insert-int_wf
int def
int-add-exception
int-atom-disjoint
int-bag-product
int-bag-product-append
int-bag-product-positive
int-bag-product_wf
int-bag-sum
int-bag-sum-append
int-bag-sum_wf
int-between
int-decr-map-add
int-decr-map-add-prop
int-decr-map-add_wf
int-decr-map-empty
int-decr-map-empty-prop
int-decr-map-empty_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
int-decr-map-fun
int-decr-map-inDom
int-decr-map-inDom-cons
int-decr-map-inDom-prop
int-decr-map-inDom-prop1
int-decr-map-inDom-prop2
int-decr-map-inDom_wf
int-decr-map-isEmpty
int-decr-map-isEmpty-assert
int-decr-map-isEmpty-prop
int-decr-map-isEmpty_wf
int-decr-map-remove
int-decr-map-remove-prop
int-decr-map-remove_wf
int-decr-map-type
int-decr-map-type-member-sq-stable
int-decr-map-type_wf
int-decr-map-update
int-decr-map-update-prop
int-decr-map-update_wf
int-deq
int-deq-aux
int-deq_wf
int-div-exception
int-eq-in-rationals
int-equal-in-rationals
int-int-retraction-reals
int-list-index
int-list-index-append
int-list-index-property
int-list-index_wf
int-list-member
int-list-member-append
int-list-member_wf
int-minus-comparison
int-minus-comparison-inc
int-minus-comparison-inc_wf
int-minus-comparison_wf
int-moebius
int-moebius-inversion
int-moebius-inversion-general
int-moebius_wf
int-mono
int-mul-exception
int-palindrome-test
int-palindrome-test-sq
int-palindrome-test_wf
int-prod
int-prod-factor
int-prod-split
int-prod_wf
int-prod_wf_nat
int-product-disjoint
int-product-union-atom-disjoint
int-rational
int-rdiv
int-rdiv-int-rmul
int-rdiv-one
int-rdiv-req
int-rdiv_wf
int-rem-exception
int-rmul
int-rmul-one
int-rmul-req
int-rmul_wf
int-sq-root
int-sqrt-ext
int-subtype-rationals
int-to-real
int-to-real_wf
int-to-ring
int-to-ring-add
int-to-ring-hom
int-to-ring-int
int-to-ring-minus
int-to-ring-minus-one
int-to-ring-mul
int-to-ring-one
int-to-ring-zero
int-to-ring_wf
int-triangle-inequality
int-triangle-inequality2
int-union-disjoint
int-value-type
int-valueall-type
int-wf
int_add_grp
int_add_grp_wf
int_add_grp_wf2
int_consensus_accum
int_consensus_accum_wf
int_consensus_init
int_consensus_init_wf
int_consensus_test
int_consensus_test_wf
int_entire
int_entire_a
int_eq def
int_eq-as-ifthenelse
int_eq-sqle-lemma1
int_eq-sqle-lemma2
int_eq_as_ite
int_eq_wf
int_hgrp_el
int_hgrp_el_wf
int_hgrp_to_nat
int_hgrp_to_nat_wf
int_inc
int_inc_rationals
int_is_mono
int_iseg
int_iseg_properties
int_iseg_wf
int_le_to_int_upper
int_le_to_int_upper_uniform
int_loset
int_loset_wf
int_lower
int_lower_ind
int_lower_properties
int_lower_well_founded
int_lower_wf
int_lt_to_int_upper
int_lt_to_int_upper_uniform
int_mag_well_founded
int_mod
int_mod_2_isect_int_mod_3
int_mod_2_union_int_mod_3
int_mod_isect_int_mod
int_mod_union_int_mod
int_mod_wf
int_mul_mon
int_mul_mon_wf
int_nzero
int_nzero_properties
int_nzero_wf
int_op
int_op_minus
int_op_wf
int_pi_det_fun
int_pi_det_fun_wf
int_pi_detach
int_prod0_lemma
int_ring
int_ring_wf
int_seg
int_seg-cardinality-le
int_seg_decide
int_seg_decide_all
int_seg_decide_wf
int_seg_inc
int_seg_ind
int_seg_properties
int_seg_subtype
int_seg_subtype-nat
int_seg_well_founded_down
int_seg_well_founded_up
int_seg_wf
int_sq
int_subtype_base
int_trichot
int_upper
int_upper_ind
int_upper_ind_uniform
int_upper_properties
int_upper_subtype_int_upper
int_upper_subtype_nat
int_upper_uwell_founded
int_upper_well_founded
int_upper_wf
is-above-int
isint-int
le_int
le_int-wf-bar
le_int-wf-bar-int
le_int-wf-partial
le_int-wf-partial2
le_int_wf
length-in-bar-int-if-co-list
lifting-apply-int_eq
lifting-callbyvalue-int_eq
lifting-callbyvalueall-int_eq
lifting-decide-int_eq
lifting-strict-int_eq
lt_int
lt_int_eq_false_elim
lt_int_eq_false_elim_sqequal
lt_int_eq_true_elim
lt_int_eq_true_elim_sqequal
lt_int_wf
merge-int
merge-int_wf
mk-map-int-decr
mk-map-int-decr_wf
mul-list-insert-int
nat_int_grp_sig_hom
nat_plus_inc_int_nzero
neg_assert_of_eq_int
not-all-int_seg
not-atom-member-int
not-axiom-member-int
not-pair-member-int
per-int
per-int_wf
prime_ideals_in_int_ring
primrec-wf-int_seg
qdiv-int-elim
quicksort-int
quicksort-int-iseg
quicksort-int-last
quicksort-int-length
quicksort-int-member
quicksort-int-nil
quicksort-int-null
quicksort-int-prop1
quicksort-int-single
quicksort-int_wf
rabs-int
radd-int
radd-int-fractions
regular-int-seq
regular-int-seq_wf
req-int
req-int-fractions
req-int-fractions2
rleq-int
rleq-int-fractions
rleq-int-fractions2
rless-int
rless-int-fractions
rless-int-fractions2
rmax-int
rmin-int
rminus-int
rmul-int
rmul-int-fractions
rmul-int-rdiv
rmul-int-rdiv2
rneq-int
rnexp-int
rng_nat_op-int
rng_nexp-int
rng_sum-int
rnonneg-int
rpositive-int
rsub-int
slow-int-palindrome-test
slow-int-palindrome-test_wf
sq_stable__ex_int_seg_ap
sq_stable__ex_int_upper
sq_stable__ex_int_upper_ap
sq_stable__regular-int-seq
strictness-int_eq-left
strictness-int_eq-right
strong-continuity2-implies-uniform-continuity-int
strong-continuity2-implies-uniform-continuity2-int
subtract-wf-bar-int
subtype_rel-int_seg
subtype_rel_int_mod
super-fact-int-prod-exp
test-int-cmp-normalize
three-cs-int-safety
trivial-int-eq-test
trivial-int-eq1
INT2NAT
prev top next
int2nat
int2nat_wf
INT2NAT2INT
prev top next
int2nat2int
INTDEQ
prev top next
intdeq_reduce_lemma
INTEG
prev top next
any_field_is_integ_dom
integ_dom
integ_dom_p
integ_dom_p_wf
integ_dom_wf
sq_stable__integ_dom_p
INTEGER
prev top next
integer-bound
integer-class-bound-exists
integer-induction
integer-nth-root
integer-nth-root-ext
integer-nth-root2
integer-sqrt
integer-sqrt-bin-search
integer-sqrt-ext
integer-sqrt-newton
integer-sqrt-newton-ext
integer-sqrt-xover
INTEGRAL
prev top next
integral
integral_wf
INTER
prev top next
mset_count_inter
mset_inter
mset_inter_assoc
mset_inter_comm
mset_inter_wf
mset_inter_wf_f
mset_mem_inter
INTERFACE
prev top next
E-interface-pair
E_interface_all_events_lemma
concrete-interface
conditional_wf-interface
constrained-msg-interface
constrained-msg-interface-valueall-type
constrained-msg-interface_wf
decidable-implies-es-interface
decidable__equal_es-E-interface
eo-msg-interface-constraint
eo-msg-interface-constraint_wf
eo-msgs-interface-delivered
eo-msgs-interface-delivered_wf
es-E-empty-interface
es-E-interface
es-E-interface-co-restrict
es-E-interface-conditional
es-E-interface-conditional-subtype
es-E-interface-conditional-subtype1
es-E-interface-conditional-subtype2
es-E-interface-conditional-subtype_rel
es-E-interface-conditional2
es-E-interface-first
es-E-interface-first-class
es-E-interface-image
es-E-interface-predicate
es-E-interface-property
es-E-interface-restrict
es-E-interface-strong-subtype
es-E-interface-subtype
es-E-interface-subtype_rel
es-E-interface-subtype_rel-implies
es-E-interface_functionality
es-E-interface_functionality-iff
es-E-interface_wf
es-causle-interface-retraction
es-empty-interface
es-empty-interface-property
es-empty-interface_wf
es-eq_wf-interface
es-fix-equal-E-interface
es-fset-at_wf-interface
es-interface
es-interface-accum
es-interface-accum-programmable
es-interface-accum-val
es-interface-accum_wf
es-interface-at
es-interface-at_wf
es-interface-buffer
es-interface-buffer-as-accum
es-interface-buffer_wf
es-interface-co-restrict
es-interface-co-restrict_wf
es-interface-conditional-domain
es-interface-conditional-domain-iff
es-interface-conditional-domain-member
es-interface-conditional-predicate-equivalent
es-interface-count
es-interface-count-as-accum
es-interface-count-val
es-interface-count_wf
es-interface-disjoint
es-interface-disjoint_wf
es-interface-empty
es-interface-empty_wf
es-interface-equality-prior-recursion
es-interface-equality-recursion
es-interface-events-append
es-interface-extensionality
es-interface-filter
es-interface-filter-val
es-interface-filter_wf
es-interface-from-decidable
es-interface-history
es-interface-history-first
es-interface-history-iseg
es-interface-history-pred
es-interface-history-prior
es-interface-history_wf
es-interface-image
es-interface-image-derived
es-interface-image-trivial
es-interface-image-val
es-interface-image_wf
es-interface-implies-decidable
es-interface-le-pred
es-interface-le-pred-bool
es-interface-left
es-interface-left-as-image
es-interface-left_wf
es-interface-local-pred
es-interface-local-pred-bool
es-interface-local-state
es-interface-local-state-cases
es-interface-local-state-prior
es-interface-local-state_wf
es-interface-locs-list
es-interface-locs-list_wf
es-interface-map
es-interface-map-val
es-interface-map_wf
es-interface-match
es-interface-match_wf
es-interface-numbered
es-interface-numbered-def
es-interface-numbered_wf
es-interface-or
es-interface-or-getleft
es-interface-or-getright
es-interface-or-hasleft
es-interface-or-hasright
es-interface-or-left
es-interface-or-left-property
es-interface-or-left_wf
es-interface-or-right
es-interface-or-right-property
es-interface-or-right_wf
es-interface-or_wf
es-interface-pair
es-interface-pair-prior
es-interface-pair-prior-programmable
es-interface-pair-prior_wf
es-interface-pair_wf
es-interface-part
es-interface-part_wf
es-interface-pred
es-interface-pred_wf
es-interface-pred_wf2
es-interface-predecessors
es-interface-predecessors-cases
es-interface-predecessors-equal
es-interface-predecessors-equal-subtype
es-interface-predecessors-general-step
es-interface-predecessors-iseg
es-interface-predecessors-last
es-interface-predecessors-le
es-interface-predecessors-loc
es-interface-predecessors-member
es-interface-predecessors-member2
es-interface-predecessors-nil
es-interface-predecessors-no_repeats
es-interface-predecessors-no_repeats2
es-interface-predecessors-nonempty
es-interface-predecessors-nonnull
es-interface-predecessors-one-one
es-interface-predecessors-sorted-by-le
es-interface-predecessors-sorted-by-locl
es-interface-predecessors-sqequal
es-interface-predecessors-step
es-interface-predecessors-step-sq
es-interface-predecessors_wf
es-interface-predicate
es-interface-predicate_wf
es-interface-prior-vals
es-interface-prior-vals_wf
es-interface-restrict
es-interface-restrict-conditional
es-interface-restrict-disjoint
es-interface-restrict-idempotent
es-interface-restrict-trivial
es-interface-restrict_wf
es-interface-right
es-interface-right-as-image
es-interface-right_wf
es-interface-set-subtype
es-interface-state
es-interface-state_wf
es-interface-sublist
es-interface-sublist_wf
es-interface-subtype_rel
es-interface-subtype_rel2
es-interface-sum
es-interface-sum-cases
es-interface-sum-le-interface
es-interface-sum-non-neg
es-interface-sum_wf
es-interface-top
es-interface-triple
es-interface-triple-def
es-interface-triple_wf
es-interface-union
es-interface-union-left
es-interface-union-right
es-interface-union_wf
es-interface-unmatched
es-interface-unmatched_wf
es-interface-val
es-interface-val-co-restrict
es-interface-val-conditional
es-interface-val-disjoint
es-interface-val-restrict
es-interface-val-restrict-sq
es-interface-val?
es-interface-val?_wf
es-interface-val_wf
es-interface-val_wf2
es-interface-vals
es-interface-vals-append
es-interface-vals-nil
es-interface-vals-since
es-interface-vals-since_wf
es-interface-vals-singleton
es-interface-vals_wf
es-interface_wf
es-is-interface
es-is-interface-co-restrict
es-is-interface-filter
es-is-interface-image
es-is-interface-map
es-is-interface-p-first
es-is-interface-restrict
es-is-interface-restrict-guard
es-is-interface-restrict2
es-is-interface-union
es-is-interface_wf
es-is-interface_wf_top
es-is-le-interface
es-is-le-interface-iff
es-is-prior-interface
es-is-prior-interface-pred
es-le-interface
es-le-interface-causle
es-le-interface-le
es-le-interface-val
es-le-interface-val-cases
es-le-interface_wf
es-le-linorder-interface
es-le-prior-interface-val
es-loc-prior-interface
es-prior-interface
es-prior-interface-cases
es-prior-interface-cases-sq
es-prior-interface-causl
es-prior-interface-equal
es-prior-interface-locl
es-prior-interface-same
es-prior-interface-val
es-prior-interface-val-locl
es-prior-interface-val-pred
es-prior-interface-val-unique
es-prior-interface-val-unique2
es-prior-interface-vals
es-prior-interface-vals-nil
es-prior-interface-vals-property
es-prior-interface-vals_wf
es-prior-interface_wf
es-prior-interface_wf0
es-prior-interface_wf1
filter-image-interface-accum-equal
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
first-at-filter-interface-predecessors
first-at-filter-interface-predecessors-or
first-at-filter-interface-predecessors1
first-interface-implies-prior-interface
global-order-pairwise-compat-msg-interface-constraint
interface-at-subtype
interface-at-val
interface-buffer-val
interface-cmp
interface-cmp-zero
interface-cmp_wf
interface-fifo
interface-fifo_wf
interface-or-val
interface-order-preserving
interface-order-preserving_wf
interface-pair-val
interface-part-subtype
interface-part-val
interface-predecessors-all-events
interface-predecessors-filter-image
interface-predecessors-split
interface-predecessors-tagged-true
interface-union-val
interface_predicate_set_lemma
is-interface-accum
is-interface-at
is-interface-buffer
is-interface-conditional
is-interface-conditional-implies
is-interface-count
is-interface-left
is-interface-or
is-interface-pair
is-interface-part
is-interface-right
is-prior-interface
is-prior-val-iff-prior-interface
iseg-interface-predecessors
l_all-interface-predecessors
l_all-mapfilter-interface-predecessors
l_exists-interface-predecessors
length-es-interface-vals
make-msg-interface
make-msg-interface-equal
make-msg-interface_wf
map-interface-accum-equal
member-es-interface-events
member-es-interface-events2
member-es-interface-history
member-interface-at
member-interface-part
member-interface-predecessors
member-interface-predecessors-subtype
member-interface-predecessors2
mk-msg-interface
mk-msg-interface_wf
msg-interface
msg-interface-constraint
msg-interface-constraint-byzantine
msg-interface-constraint-byzantine_wf
msg-interface-constraint_wf
msg-interface-delay
msg-interface-delay_wf
msg-interface-destination
msg-interface-destination_wf
msg-interface-extensionality
msg-interface-hdf
msg-interface-hdf_wf
msg-interface-message
msg-interface-message_wf
msg-interface_wf
msgs-interface-delivered
msgs-interface-delivered-with-omissions
msgs-interface-delivered-with-omissions_wf
msgs-interface-delivered_wf
msgs-interface-with-omissions-sub
msgs-interface-with-omissions-sub_wf
nonempty-es-interface-history
prior-interface-induction
strong-interface-fifo
strong-interface-fifo-order-preserving
strong-interface-fifo_wf
INTERFACE2
prev top next
conditional_wf-interface2
INTERFACES
prev top next
es-E-interfaces-strong-subtype
INTERLEAVE1
prev top next
interleave1
interleave1_wf
INTERLEAVE2
prev top next
interleave2
interleave2_wf
INTERLEAVED
prev top next
interleaved_family
interleaved_family_occurence
interleaved_family_occurence_wf
interleaved_family_wf
interleaved_split
sublist_interleaved
INTERLEAVES
prev top next
interleaves-and-gets-comment
INTERLEAVING
prev top next
append_interleaving
comb_for_interleaving_wf
cons_interleaving
filter_interleaving
filter_interleaving_occurence
filter_is_interleaving
interleaving
interleaving_as_filter
interleaving_as_filter_2
interleaving_filter2
interleaving_implies_occurence
interleaving_occurence
interleaving_occurence_onto
interleaving_occurence_wf
interleaving_of_cons
interleaving_of_nil
interleaving_singleton
interleaving_split
interleaving_sublist
interleaving_symmetry
interleaving_wf
l_before_interleaving
length_interleaving
member_interleaving
nil_interleaving
occurence_implies_interleaving
INTERLEAVING2
prev top next
cons_interleaving2
nil_interleaving2
INTERMEDIATE
prev top next
intermediate-value-lemma
intermediate-value-theorem
intermediate-value-theorem-rpolynomial
INTERNAL
prev top next
CLK_headers_internal
CLK_headers_internal_wf
OARcast_headers_internal
OARcast_headers_internal_wf
es-with-internal
internal events
new_23_sig_headers_internal
new_23_sig_headers_internal_wf
nysiad_headers_internal
nysiad_headers_internal_wf
pv11_p1_headers_internal
pv11_p1_headers_internal_wf
INTERSECT
prev top next
empty_intersect_lemma
INTERSECTING
prev top next
combinations-n-intersecting
n-intersecting
n-intersecting_wf
three-intersecting-wait-set
three-intersecting-wait-set-exists
two-intersecting-wait-set
two-intersecting-wait-set-exists
two-intersecting-wait-set-exists'
INTERSECTION
prev top next
bag-intersection
disjoint-iff-null-intersection
fset-intersection
fset-intersection-associative
fset-intersection-commutes
fset-intersection_wf
generic-countable-intersection
l_disjoint_intersection
l_disjoint_intersection_implies
l_disjoint_intersection_implies2
l_intersection
l_intersection-size
l_intersection_nil
l_intersection_wf
member-fset-intersection
member-intersection
one-intersection
one-intersection_wf
three-intersection
three-intersection-two-intersection
three-intersection_wf
two-intersection
two-intersection-one-intersection
two-intersection_wf
INTERSECTION2
prev top next
l_disjoint_intersection2
INTERVAL
prev top next
Kan-interval
Kan-interval_wf
cantor-interval
cantor-interval-cauchy
cantor-interval-cauchy-ext
cantor-interval-converges
cantor-interval-converges-ext
cantor-interval-inclusion
cantor-interval-inclusion2
cantor-interval-length
cantor-interval-req
cantor-interval-rleq
cantor-interval-rless
cantor-interval_wf
cantor-to-interval
cantor-to-interval-onto-common
cantor-to-interval-onto-lemma
cantor-to-interval-onto-proper
cantor-to-interval-req
cantor-to-interval_wf
cantor-to-interval_wf1
cantor_to_interval
compact-proper-interval-near-member
cubical-interval
cubical-interval-ap
cubical-interval-ap_wf
cubical-interval-filler
cubical-interval-filler-fills
cubical-interval-filler_wf
cubical-interval-non-trivial-box
cubical-interval_wf
decreasing-on-interval
decreasing-on-interval_wf
eo-forward-interval
eo-forward-no-classrel-in-interval
equipollent_interval
es-closed-interval-vals
es-closed-interval-vals-decomp
es-closed-interval-vals_wf
es-closed-open-interval
es-closed-open-interval-decomp
es-closed-open-interval-decomp-last
es-closed-open-interval-decomp-mem
es-closed-open-interval-decomp-member
es-closed-open-interval-eq-before
es-closed-open-interval-forward
es-closed-open-interval-nil
es-closed-open-interval-sorted-by
es-closed-open-interval_wf
es-interval
es-interval-eq
es-interval-eq-le-before
es-interval-eq2
es-interval-induction
es-interval-induction2
es-interval-is-nil
es-interval-iseg
es-interval-last
es-interval-length-one-one
es-interval-less
es-interval-less-sq
es-interval-nil
es-interval-non-zero
es-interval-one-one
es-interval-open-interval
es-interval-ordered
es-interval-partition
es-interval-select
es-interval-sorted-by
es-interval_wf
es-interval_wf2
es-open-interval
es-open-interval-closed
es-open-interval-nil
es-open-interval-ordered
es-open-interval-ordered-iff
es-open-interval-ordered-inst
es-open-interval_wf
es-prior-interval-vals
es-prior-interval-vals_wf
firstn-es-open-interval
hd-es-interval
hd_l_interval
increasing-on-interval
increasing-on-interval_wf
interval
interval_wf
iseg-es-interval
iseg-filter-es-interval
l_before-es-interval
l_interval
l_interval_wf
last_l_interval
length_l_interval
member-es-closed-open-interval
member-es-interval
member-es-open-interval
member-run-event-interval
no-classrel-in-interval
no-classrel-in-interval-trivial
no-classrel-in-interval_wf
nth_tl-es-open-interval
pred-hd-es-open-interval
pred-member-es-open-interval
run-event-interval
run-event-interval-cases
run-event-interval_wf
select_l_interval
sq_stable__no-classrel-in-interval
strictly-decreasing-on-interval
strictly-decreasing-on-interval_wf
strictly-increasing-on-interval
strictly-increasing-on-interval_wf
unit-interval-fan
unit-interval-fan_wf
INTO
prev top next
inj_into_ocmon
push-spread-into-ifthenelse
INTRANSIT
prev top next
intransit-to-info
intransit-to-info_wf
norm-intransit
norm-intransit_wf
pRun-intransit-invariant
run-intransit
run-intransit_wf
INTRO
prev top next
cbv-intro-test
cbva-intro-test
cbva-intro-test3
coprime_intro
eq_int_eq_false_intro
eq_int_eq_true_intro
ex-do-Intro
INTS
prev top next
exists-type-equating-ints
INTSEG
prev top next
natrec_wf_intseg
INTSET
prev top next
max-of-intset
INV
prev top next
bij_imp_exists_inv
fpf-inv-rename
fpf-inv-rename_wf
fun_with_inv_is_bij
fun_with_inv_is_bij2
groupoid-inv
groupoid-inv
groupoid-inv_wf
groupoid-inv_wf
groupoid_inv
groupoid_inv
grp_hom_inv
grp_inv
grp_inv_assoc
grp_inv_diff
grp_inv_id
grp_inv_inv
grp_inv_thru_op
grp_inv_wf
iabgrp_op_inv_assoc
iabgrp_op_inv_assoc_fps
inv-rel
inv-rel-inject
inv-rel_wf
inv_funs
inv_funs-iff
inv_funs_sym
inv_funs_wf
inv_image_ind
inv_image_ind_a
inv_image_ind_tp
inv_perm
inv_perm_wf
ldst-inv
list_accum_iseg_inv
list_accum_proper_iseg_inv
lnk-inv
lnk-inv-inv
lnk-inv-one-one
lnk-inv_wf
lsrc-inv
module_plus_inv
name-morph-inv
name-morph-inv-eq
name-morph-inv-eq-domain
name-morph-inv_wf
ndiff_inv
neg_inv_fps
new_23_sig_quorum_inv_vote
new_23_sig_quorum_inv_vote2
new_23_sig_quorum_inv_vote2_fun
new_23_sig_quorum_inv_vote_fun
oal_neg_left_inv
oal_neg_right_inv
perm_grp_inv_assoc
perm_grp_inv_id
perm_grp_inv_inv
perm_grp_inv_thru_op
pv11_p1_inv_acc
pv11_p1_inv_comm
pv11_p1_inv_scout
quot_grp_inv_wf
reg-seq-inv
reg-seq-inv_wf
rng_plus_inv
rng_plus_inv_assoc
sq_stable__inv_funs
state-class2-inv
txpose_perm_inv
INVAR
prev top next
divides_invar_1
divides_invar_2
mon_itop_perm_invar
mon_itop_txpose_invar
oal_neg_keys_invar
INVARIANT
prev top next
Accum-class-invariant
Memory-class-invariant
Memory-class-invariant-sv
Memory-class-invariant-sv1
Memory-loc-class-invariant
Memory-loc-class-invariant-sv
Memory-loc-class-invariant-sv1
State-comb-invariant
State-comb-invariant-or
State-comb-invariant-sv
State-loc-comb-invariant
State-loc-comb-invariant-or
State-loc-comb-invariant-sv
State-loc-comb-invariant-sv1
State-loc-comb-invariant-sv2
causal-invariant
causal-invariant_wf
consensus-ts4-archived-invariant
consensus-ts5-archive-invariant
global-order-compat-invariant
global-order-compat-squash-invariant
global-order-pairwise-compat-invariant
global-order-pairwise-compat-squash-invariant
hdf-ap-invariant
hdf-invariant
hdf-invariant_wf
iterated-classrel-invariant
joint-embedding-preserves-causal-invariant
list_accum_invariant
new_23_sig_quorum_invariant
new_23_sig_quorum_invariant_fun
pRun-System-invariant
pRun-intransit-invariant
permutation-invariant
poss-maj-invariant
rem_invariant
squash-causal-invariant
squash-causal-invariant_wf
three-cs-archive-invariant
three-cs-vote-invariant
weak-joint-embedding-preserves-causal-invariant
weak-joint-embedding-preserves-squash-causal-invariant
INVARIANT0
prev top next
consensus-ts3-invariant0
INVARIANT1
prev top next
consensus-ts3-invariant1
iterated_classrel_invariant1
pRun-invariant1
INVARIANT2
prev top next
hdf-ap-invariant2
iterated-classrel-invariant2
iterated_classrel_invariant2
list_accum_invariant2
pRun-invariant2
permutation-invariant2
INVARIANT3
prev top next
iterated_classrel_invariant3
list_accum_invariant3
pRun-invariant3
INVERSE
prev top next
accum_split_inverse
add-inverse
add-inverse-unique
biject-iff-inverse
biject-inverse
equipollent-iff-inverse-funs
flip_inverse
grp_inverse
injection-inverse
inverse
inverse-rpower
inverse_grp_sig_hom_shift
inverse_wf
list_split_inverse
ocgrp_inverse
perm_grp_inverse
perm_inverse
rel_inverse
rel_inverse_exp
rel_inverse_star
rel_inverse_wf
residue-mul-inverse
rmul-inverse-is-rinv
rotate-inverse
sq_stable__inverse
surject-inverse
INVERSE1
prev top next
rotate-inverse1
INVERSE2
prev top next
add-inverse2
biject-inverse2
injection-inverse2
INVERSION
prev top next
assoced_inversion
bag-moebius-inversion
bdd-diff_inversion
binrel_eqv_inversion
coprime_inversion
dataflow-equiv_inversion
eqmod_inversion
equipollent_inversion
ext-eq_inversion
fps-moebius-inversion
int-moebius-inversion
int-moebius-inversion-general
massoc_inversion
permr_inversion
permr_upto_inversion
permutation_inversion
predicate_equivalent_inversion
rel_equivalent_inversion
req_inversion
rfun-eq_inversion
same-thread_inversion
uiff_inversion
INVERT
prev top next
invert-union
invert-union_wf
INVERTUNION
prev top next
invertunion
invertunion_wf
IOTA
prev top next
extend-name-morph-iota
iota
iota'
iota'-comp
iota'-identity
iota'_wf
iota-face-map
iota-identity
iota-identity2
iota-two-face-maps
iota-wf
iota_wf
rename-one-iota
IPROPER
prev top next
iproper
iproper_wf
IROOT
prev top next
general-iroot
general-iroot-property
general-iroot_wf
iroot
iroot-lemma
iroot-lemma2
iroot-positive
iroot-property
iroot-zero
iroot_wf
IRRATIONAL
prev top next
irrational
irrational_wf
rsqrt-irrational
rsqrt_2-irrational
IRREFL
prev top next
irrefl
irrefl_trans_imp_sasym
irrefl_wf
oal_lt_irrefl
pv11_p1_lt_bnum_irrefl
qoset_lt_irrefl
strict_part_irrefl
IRREFL2
prev top next
pv11_p1_lt_bnum_irrefl2
IRREFLEX
prev top next
es-locl-irreflex-test
IRREFLEXIVE
prev top next
llex-irreflexive
rel_plus_irreflexive
wellfounded-irreflexive
IRREFLEXIVITY
prev top next
es-causl_irreflexivity
es-locl_irreflexivity
grp_lt_irreflexivity
less_than_irreflexivity
rless_irreflexivity
rneq_irreflexivity
set_lt_irreflexivity
strict-fun-connected_irreflexivity
IRRELEVANT
prev top next
extend-name-morph-irrelevant
IS
prev top next
Memory-loc-class-is-prior-State-loc-comb
State-loc-comb-is-loop-class-state
What is uniformity conjecture?
alg_act_is_rng_chom
any_field_is_integ_dom
append_is_nil
append_is_nil_test
assert-cs-is-committed
assert-cs-is-considering
assert-cs-is-decided
assert-fpf-is-empty
assert-is-filter-image
assert-is-qrep
assert-is_prime
assert-lg-is-source
assert-ses-is-fresh
assert-ses-is-legal
bag-append-is-empty
bag-append-is-single
bag-append-is-single-iff
bag-append-is-single-iff2
bag-combine-is-map
bag-combine-is-single-if
bag-count-is-zero
bag-filter-is-empty
bag-filter-is-nil
bag-filter-is-sub-bag
bag-rep-is-single-valued
bag-size-is-zero
bag-summation-is-zero
bag-union-is-single
bag-union-is-single-if
band-is-inl
band-is-inl-base
bm_numItems_is_cnt_prop0
cbv_list_accum-is-list_accum
cdrng_is_abdgrp
cdrng_is_abdmonoid
concat-is-nil
cs-is-committed
cs-is-committed-implies
cs-is-committed_wf
cs-is-considering
cs-is-considering-implies
cs-is-considering_wf
cs-is-decided
cs-is-decided_wf
cube-set-map-is
cubical-set-is-functor
decidable__pa-is-new-and
decidable__pa-is-sign-implies
eqv_mod_subset_is_eqv
es-before-is-nil-if-first
es-blocl-is-bless
es-hist-is-append
es-hist-is-concat
es-interval-is-nil
es-is-filter-image
es-is-filter-image2
es-is-interface
es-is-interface-co-restrict
es-is-interface-filter
es-is-interface-image
es-is-interface-map
es-is-interface-p-first
es-is-interface-restrict
es-is-interface-restrict-guard
es-is-interface-restrict2
es-is-interface-union
es-is-interface_wf
es-is-interface_wf_top
es-is-le-interface
es-is-le-interface-iff
es-is-prior-interface
es-is-prior-interface-pred
eval_list-append-nil-is-eval_list
evalall-is-exception
event_in_sv_classrel_is_in_class
exception-sqle-is-exception
exp-is-zero
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
firstn_is_iseg
fpf-is-empty
fpf-is-empty_wf
fpf-join-is-empty
free_abmon_endomorph_is_id
from-upto-is-nil
from-upto-is-singleton
fun_with_inv_is_bij
fun_with_inv_is_bij2
gcd_is_divisor_1
gcd_is_divisor_2
gcd_is_gcd
grp_lt_is_sp_of_leq_a
has-es-info-type-is-msg-has-type
has-value-is-list-approx-is-type
has-value-is-list-map-if-has-value-is-list
has-value-is-list-map-iff-has-value-is-list
has-value-is-list-of-co-list
hd-es-le-before-is-first
hdf-halted-is-halt
hdf-halted-is-inr
i-approx-is-subinterval
imax-list-is-nat
implies-is-partition-choice
increasing_is_id
injection-is-surjection
int_is_mono
is-A-face
is-A-face_wf
is-above
is-above-axiom
is-above-inl
is-above-inr
is-above-int
is-above-pair
is-above-subtype
is-above_wf
is-accum-class
is-atomic
is-atomic_wf
is-basic-seq
is-basic-seq_wf
is-cond-class
is-consensus-message
is-consensus-message_wf
is-dag
is-dag-add
is-dag-append
is-dag-map
is-dag-remove
is-dag_wf
is-exception
is-exception-evalall
is-exception_wf
is-face
is-face_wf
is-filter-image-sq
is-first-class
is-first-class2
is-imax-class
is-inning-event
is-inning-event_wf
is-interface-accum
is-interface-at
is-interface-buffer
is-interface-conditional
is-interface-conditional-implies
is-interface-count
is-interface-left
is-interface-or
is-interface-pair
is-interface-part
is-interface-right
is-latest-pair
is-latest-val
is-list
is-list-approx
is-list-approx-step
is-list-approx0
is-list-approx_wf
is-list-btrue-if-list
is-list-fun
is-list-fun_wf
is-list-if-has-value
is-list-if-has-value-decomp
is-list-if-has-value-ext
is-list-if-has-value-fun
is-list-if-has-value-fun-ax-mem
is-list-if-has-value-fun_wf
is-list-if-has-value-hv-prp
is-list-if-has-value-rec
is-list-if-has-value-rec-decomp
is-list-if-has-value-rec-map
is-list-if-has-value-rec-pair-bot
is-list-if-has-value-rec-snd
is-list-if-has-value-rec-subtype-unit
is-list-if-has-value-rec_wf
is-list-if-has-value_wf
is-list-map
is-list-prop1
is-list-prop2
is-list-wf-co-list
is-list-wf-list
is-list_wf
is-map-class
is-mapfilter-class
is-max-f-class
is-max-fst
is-or-latest
is-pair-prior
is-parameter-class
is-partition-choice
is-partition-choice_wf
is-path
is-path_wf
is-prior-all-events
is-prior-class-when
is-prior-interface
is-prior-val
is-prior-val-iff-prior-interface
is-qrep
is-qrep_wf
is-rec-class
is-return-class
is-run-event
is-run-event_wf
is-strict-fun
is-tagged-true
is_accum_splitting
is_accum_splitting_wf
is_list_axiom_lemma
is_list_fun_axiom_lemma
is_list_fun_pair_lemma
is_list_pair_lemma
is_list_splitting
is_list_splitting_wf
is_prime
is_prime_wf
is_ufm
is_ufm_wf
iseg-es-before-is-before
iseg-es-le-before-is-before
iseg_is_sublist
islist-append-nil-is-list
islist-implies-is-list
l-last-is-last
l-ordered-is-sorted-by
lcm-is-lcm
length-is-colength
lg-is-source
lg-is-source-wf_dag
lg-is-source_wf
list-to-set-is-remove-repeats
list_accum_is_reduce
locally-ranked-is-well-founded
longest-prefix-is-nil
loop-class-memory-is-prior-loop-class-state
map-is-top-list
map_is_append
map_is_cons
map_is_nil
mcopower_inj_is_hom
mcopower_umap_is_hom
mdivisor_of_atom_is_assoc2
module_act_is_grp_hom
module_hom_is_grp_hom
mon_when_is_hom
name_eq-is-inl
not-is-exception-bottom
note-is-function
nth_tl_is_fseg
nth_tl_is_nil
null-class-is-empty
oal_le_is_order
omral_alg_umap_is_hom
pa-is-new-and
pa-is-new-and_wf
pa-is-sign-implies
pa-is-sign-implies_wf
partial_ap_is_gen
permr_nil_is_nil
poset_functor_extend-is-functor
posint_is_ufm
prior-val-is
process-equiv-is-equiv
prod-image-is-image
pv11_p1_is_bnum
pv11_p1_is_bnum_wf
rec-value-list-is-rec-value
refl_cl_is_order
rel-is-immediate
rmul-inverse-is-rinv
rmul-is-negative
rmul-is-negative1
rmul-is-positive
rnexp-is-positive
rotate-by-is-id
select-is-bottom
select_fun_ap_is_last1
ses-is-fresh
ses-is-fresh_wf
ses-is-legal
ses-is-legal_wf
ses-is-protocol-action
ses-is-protocol-action-useable
ses-is-protocol-action-used
ses-is-protocol-action_wf
ses-is-protocol-actions
ses-is-protocol-actions-fresh
ses-is-protocol-actions-legal
ses-is-protocol-actions_wf
ses-sign-is-protocol-action
set-is-image
set_lt_is_sp_of_leq
set_lt_is_sp_of_leq_a
single-valued-bag-is-list
single-valued-bag-is-rep
skip-first-class-is-empty-if-first
sp-join-is-bottom
sp-lub-is-bottom
sp-lub-is-top
sp-lub-is-top1
sp-meet-is-top
sq_stable__is-list-if-has-value-fun
sq_stable__is-partition-choice
sq_stable__is_accum_splitting
sq_stable__is_list_splitting
squash-exists-is-union-squash
squash-union-is-union-squash
subtract-is-less
sv-bag-is-bag-rep
sv-bag-is-bag-rep-lousy-proof
sym_grp_is_swaps
sym_grp_is_swaps_a
system-equiv-is-equiv
tunion-is-image
union-set-is-set-exists
unit-cube-is-yoneda
upto_is_nil
urec-is-fixedpoint
urec-is-least-fixedpoint
votes-from-inning-is-nil
zhgrp_to_nat_is_hom
ISALL
prev top next
mFOquant-isall
mFOquant-isall_wf
ISALLEVENTS
prev top next
isallevents_lemma
ISATOM
prev top next
decide-isatom-if-has-value
has-value-implies-dec-isatom
has-value-implies-dec-isatom-2
isatom def
isatom-bool-if-has-value
isatom-implies-not-isint
isatom-implies-not-ispair
isinl-implies-not-isatom
isinr-implies-not-isatom
isint-implies-not-isatom
ispair-implies-not-isatom
lifting-strict-isatom
strictness-isatom
ISATOM1
prev top next
isatom1
isatom1-bool-if-has-value
strictness-isatom1
ISATOM2
prev top next
decide-isatom2-if-has-value
has-value-implies-dec-isatom2
has-value-implies-dec-isatom2-2
isatom2
isatom2-bool-if-has-value
lifting-strict-isatom2
strictness-isatom2
ISAXIOM
prev top next
decide-isaxiom-if-has-value
has-value-implies-dec-isaxiom
has-value-implies-dec-isaxiom-2
isaxiom def
isaxiom-append-nil
isaxiom-bool-if-bunion-unit-prod
isaxiom-bool-if-has-value
isaxiom-implies
isaxiom-implies-not-isint
isaxiom-implies-sq
isaxiom-sqequal
isaxiom-wf-colist
isaxiom_wf_list
isaxiom_wf_listunion
ispair-or-isaxiom-append-nil
lifting-add-isaxiom-1
lifting-add-isaxiom-2
lifting-apply-isaxiom
lifting-callbyvalueall-isaxiom
lifting-decide-isaxiom
lifting-isaxiom-concat
lifting-isaxiom-decide
lifting-isaxiom-isaxiom
lifting-isaxiom-ispair
lifting-isaxiom-less
lifting-isaxiom-spread
lifting-ispair-isaxiom
lifting-spread-isaxiom
lifting-strict-isaxiom
normalization-isaxiom
strictness-isaxiom
ISAXIOM2
prev top next
lifting-ispair-isaxiom2
ISECT
prev top next
b-isect
continuous-monotone-isect
dep-isect
dep-isect-subtype
dep-isect-subtype2
dep-isect-value-type
dep-isect-wf
dep-isect_wf
double_isect_subtype_rel
in-open-isect
int_mod_2_isect_int_mod_3
int_mod_isect_int_mod
isect def
isect-family
isect-family-wf2
isect-family_wf
isect-mono
isect-rel
isect-rel_wf
isect-subtype-1
isect-subtype-2
isect-value-type
isect-valueall-type
isect_functionality_wrt_equipollent_dependent
isect_prod_lemma
isect_subtype
isect_subtype_base
isect_subtype_rel
isect_subtype_rel_trivial
isect_wf
member-dep-isect
open-isect
open-isect_wf
quotient-isect-base
quotient-isect-base2
strong-continuous-dep-isect
strong-subtype-isect-base
sub-isect-family
subtype_rel_double_isect
subtype_rel_isect
subtype_rel_isect-2
subtype_rel_isect_as_subtyping_lemma
subtype_rel_isect_general
ISECT2
prev top next
equiv_rel_isect2
isect2
isect2-b-union-subtype
isect2-record
isect2_decomp
isect2_functionality_wrt_subtype_rel
isect2_quotient
isect2_subtype_rel
isect2_subtype_rel2
isect2_subtype_rel3
isect2_wf
strong-continuous-isect2
subtype_rel_isect2
ISEG
prev top next
accum_split_iseg
agree_on_common_iseg
append_iseg
causal_order_filter_iseg
comb_for_iseg_wf
common_iseg_compat
compat-iff-common-iseg
compat-iseg
compat-iseg-cases
concat_iseg
cons-proper-iseg
cons_iseg
cons_iseg_not_null
decidable-exists-iseg
decidable__exists_iseg
decidable__iseg
es-hist-iseg
es-interface-history-iseg
es-interface-predecessors-iseg
es-interval-iseg
es-prior-fixedpoints-iseg
filter_iseg
first-iseg
firstn-iseg
firstn_is_iseg
fseg-iseg-reverse
global-order-iseg
global-order-iseg_wf
int_iseg
int_iseg_properties
int_iseg_wf
iseg
iseg-append-nth_tl
iseg-append-one
iseg-as-filter
iseg-es-before
iseg-es-before-is-before
iseg-es-embedding
iseg-es-hist
iseg-es-interval
iseg-es-le-before
iseg-es-le-before-is-before
iseg-filter-es-interval
iseg-global-order-history
iseg-global-order-loc
iseg-iff-firstn
iseg-implies-global-order-iseg
iseg-interface-predecessors
iseg-l-ordered
iseg-l_contains
iseg-local-property
iseg-local-relation
iseg-local-simulation-inputs
iseg-map
iseg-mapfilter
iseg-remainder-as-filter
iseg-sorted-by
iseg-subtype
iseg-transition-lemma
iseg_antisymmetry
iseg_append
iseg_append0
iseg_append_iff
iseg_append_length
iseg_append_single
iseg_extend
iseg_filter
iseg_filter2
iseg_filter_last
iseg_ge_length
iseg_implies_member
iseg_is_sublist
iseg_length
iseg_map
iseg_member
iseg_nil
iseg_product
iseg_product-positive
iseg_product-property
iseg_product-split
iseg_product_rem
iseg_product_rem_property
iseg_product_rem_wf
iseg_product_wf
iseg_same_length
iseg_select
iseg_select2
iseg_single
iseg_transitivity
iseg_transitivity2
iseg_weakening
iseg_weakening2
iseg_wf
l_before_iseg
list-decomp-nat-iseg
list_accum_iseg_inv
list_accum_proper_iseg_inv
list_split_iseg
member-iseg-sorted-by
nil_iseg
proper-iseg
proper-iseg-append
proper-iseg-append-one
proper-iseg-length
proper-iseg_wf
quicksort-int-iseg
single_iseg
sq_stable__iseg
sublist_iseg
unshuffle-iseg
upto_iseg
ISEG2
prev top next
accum_split_iseg2
compat-iseg2
filter_iseg2
list_split_iseg2
ISEMPTY
prev top next
bm_isEmpty
bm_isEmpty_wf
int-decr-map-isEmpty
int-decr-map-isEmpty-assert
int-decr-map-isEmpty-prop
int-decr-map-isEmpty_wf
isEmpty-nat-missing
isEmpty-nat-missing-prop
isEmpty-nat-missing_wf
isempty_lemma
lookup-list-map-isEmpty
lookup-list-map-isEmpty-prop
lookup-list-map-isEmpty_wf
map-sig-isEmpty
map-sig-isEmpty_wf
set-sig-isEmpty
set-sig-isEmpty_wf
ISEVEN
prev top next
assert-isEven
isEven
isEven-add
isEven_wf
isOdd-isEven-add
ISINL
prev top next
decide-isinl-if-has-value
has-value-implies-dec-isinl
has-value-implies-dec-isinl-2
isinl def
isinl-bool-if-has-value
isinl-implies
isinl-implies-not-isatom
isinl-implies-not-isint
isinl-member
strictness-isinl
ISINR
prev top next
decide-isinr-if-has-value
has-value-implies-dec-isinr
has-value-implies-dec-isinr-2
isinr def
isinr-bool-if-has-value
isinr-implies
isinr-implies-not-isatom
isinr-implies-not-isint
isinr-member
strictness-isinr
ISINT
prev top next
decide-isint-if-has-value
has-value-implies-dec-isint
has-value-implies-dec-isint-2
isatom-implies-not-isint
isaxiom-implies-not-isint
isinl-implies-not-isint
isinr-implies-not-isint
isint def
isint-bool-if-has-value
isint-implies-not-isatom
isint-int
ispair-implies-not-isint
lifting-strict-isint
ISL
prev top next
isl
isl-apply-alist
isl-es-search-back
isl-ite
isl-list-index
isl-not-isr
isl-prior
isl-prior-iff
isl_wf
isr-not-isl
not-isl-assert-isr
not-isl-isr
not-isl-priority-select
not-isr-assert-isl
not-isr-isl
ISLAMBDA
prev top next
decide-islambda-if-has-value
has-value-implies-dec-islambda
has-value-implies-dec-islambda-2
islambda def
islambda-bool-if-has-value
lifting-strict-islambda
strictness-islambda
ISLIST
prev top next
co-list-islist
co-list-islist-ext-eq-list
co-list-islist-ext-list
co-list-islist-induction1
co-list-islist-islist
co-list-islist-islist-new-compactness-base
co-list-islist_wf
islist
islist-append-nil-is-list
islist-append-nil-sqequal-islist
islist-iff-length-has-value
islist-implies-is-list
islist-list
islist_wf
length-wf-co-list-islist
list_ind-wf-co-list-islist
member-co-list-islist
ISLIST2
prev top next
list_ind-wf-co-list-islist2
ISLOCAL
prev top next
islocal
islocal-implies
islocal-not-isrcv
islocal_wf
ISNAME
prev top next
assert-isname
isname
isname-name
isname-nameset
isname_wf
not-assert-isname
ISO
prev top next
rels_iso
rels_iso_wf
ISODD
prev top next
assert-isOdd
isOdd
isOdd-add
isOdd-isEven-add
isOdd_wf
ISOLATE
prev top next
isolate_summand
ISPAIR
prev top next
atom-implies-ispair-right
decide-ispair-if-has-value
false-using-ispair-cases
has-value-implies-dec-ispair
has-value-implies-dec-ispair-2
isatom-implies-not-ispair
ispair def
ispair-bool-if-bunion-unit-prod
ispair-bool-if-co-list
ispair-bool-if-has-value
ispair-implies
ispair-implies-not-isatom
ispair-implies-not-isint
ispair-implies-sq
ispair-member
ispair-or-isaxiom-append-nil
ispair-pair
ispair-sqequal
ispair_wf_list
ispair_wf_listunion
lifting-add-ispair-1
lifting-add-ispair-2
lifting-apply-ispair
lifting-callbyvalueall-ispair
lifting-decide-ispair
lifting-isaxiom-ispair
lifting-ispair-concat
lifting-ispair-decide
lifting-ispair-isaxiom
lifting-ispair-isaxiom2
lifting-ispair-ispair
lifting-ispair-less
lifting-ispair-spread
lifting-spread-ispair
lifting-strict-ispair
not-ispair
pi1-if-ispair-append-nil
pi2-if-ispair-append-nil
prod-if-ispair-append-nil
spread-ispair-spread
strict4-ispair
strictness-ispair
ISQRT
prev top next
isqrt
isqrt-convex
isqrt-non-decreasing
isqrt-property
isqrt_newton
isqrt_newton_wf
isqrt_wf
square-iff-isqrt
ISQRTN
prev top next
isqrtn
isqrtn_wf
ISR
prev top next
isl-not-isr
isr
isr-not-isl
isr_wf
not-isl-assert-isr
not-isl-isr
not-isr-assert-isl
not-isr-isl
strictness-isr
ISRCV
prev top next
islocal-not-isrcv
isrcv
isrcv-implies
isrcv_locl_lemma
isrcv_rcv_lemma
isrcv_wf
locknd_functionality_isrcv
ISRCVL
prev top next
assert-isrcvl
isrcvl
isrcvl_wf
IT
prev top next
case_it
exposed-it
it
it_wf
ITCOMP
prev top next
extend_perm_over_itcomp
ITE
prev top next
church-ite
church-ite_wf
church_ite_false_lemma
church_ite_true_lemma
decide-ite
disjoint-union-classrel-ite
disjoint-union-classrel-ite-weak
disjoint-union-classrel-ite-weak2
fun_thru_ite
int_eq_as_ite
isl-ite
ite
ite-bool-1
ite-bool-2
ite-bool-3
ite-bool-4
ite-same
ite_and_reduce
ite_false
ite_rw_false
ite_rw_test
ite_rw_true
ite_wf
less_as_ite
member-ite
mk_applies_ite
mk_lambdas_fun-unroll-ite
mk_lambdas_unroll_ite
null-ite
sum-ite
trivial_ite_2
typed-null-ite
ITE2
prev top next
disjoint-union-classrel-ite2
ITEM
prev top next
fset-item
fset-item-member
fset-item_wf
ITER
prev top next
iter_df_cons_lemma
iter_df_nil_lemma
iter_hdf_cons_lemma
iter_hdf_nil_lemma
ITERATE
prev top next
W_iterate_functor
W_iterate_functor_wf
final-iterate
final-iterate-property
final-iterate_wf
hdf-halted-compose2-iterate
hdf-parallel-bag-iterate
iterate-Process
iterate-Process_wf
iterate-base-process-class-program
iterate-constant-dataflow
iterate-dataflow
iterate-dataflow-append
iterate-dataflow_wf
iterate-fun-stream
iterate-fun-stream_wf
iterate-hdataflow
iterate-hdataflow_wf
iterate-hdf-append
iterate-hdf-bind-simple
iterate-hdf-buffer-simple
iterate-hdf-buffer2-simple
iterate-hdf-halt
iterate-null-process
iterate-process
iterate-process_wf
iterate-rec-dataflow
iterate-rotate
iterate-rotate-by
iterate-rotate-rotate-by
iterate-stateless-dataflow
iterate_functor
iterate_functor_wf
map-iterate-fun-stream
same-final-iterate-one-one
type-functor-iterate
type-functor-iterate_wf
ITERATED
prev top next
decidable__exists-iterated-classrel
decidable__exists-iterated-classrel-between3-sv
decidable__exists-pred-iterated-classrel-between3-sv
decidable__exists-prior-iterated-classrel
decidable__exists_iterated_classrel
iterated-classrel
iterated-classrel-Memory-classrel
iterated-classrel-Memory-loc-classrel
iterated-classrel-as-prior
iterated-classrel-exists
iterated-classrel-exists-iff
iterated-classrel-iff
iterated-classrel-invariant
iterated-classrel-invariant2
iterated-classrel-mem
iterated-classrel-progress
iterated-classrel-single-val
iterated-classrel-trans
iterated-classrel_wf
iterated-conjugate
iterated-conjugate2
iterated-rotate
iterated_classrel
iterated_classrel-exists
iterated_classrel-exists-iff
iterated_classrel-single-val
iterated_classrel_invariant1
iterated_classrel_invariant2
iterated_classrel_invariant3
iterated_classrel_mem
iterated_classrel_mem2
iterated_classrel_progress
iterated_classrel_trans1
iterated_classrel_trans2
iterated_classrel_trans3
iterated_classrel_wf
ni-iterated-min
ni-iterated-min_wf
prior-iterated-classrel
prior-iterated-classrel_wf
prior_iterated_classrel
prior_iterated_classrel_wf
sq_stable__iterated_classrel
sq_stable__single-valued-iterated-classrel
sq_stable__single-valued-prior-iterated-classrel
squash-iterated_classrel
ITERATES
prev top next
orbit-iterates
ITERATION
prev top next
iteration_terminates
ITOP
prev top next
comb_for_itop_wf
comb_for_mon_itop_wf
itop
itop_aux_wf
itop_shift
itop_split
itop_unroll_base
itop_unroll_hi
itop_unroll_lo
itop_unroll_unit
itop_wf
mon_for_eq_itop
mon_itop
mon_itop_op
mon_itop_perm_invar
mon_itop_shift
mon_itop_split
mon_itop_split_el
mon_itop_txpose_invar
mon_itop_unroll_base
mon_itop_unroll_hi
mon_itop_unroll_lo
mon_itop_unroll_unit
mon_itop_wf
mon_reduce_eq_itop
IVL
prev top next
cantor_ivl
cantor_ivl-converges
cantor_ivl-converges-ext
cantor_ivl_wf
IVT
prev top
IVT-deriv-seq-test
IVT-locally-non-constant
IVT-rpolynomial1
IVT-rpolynomial2
IVT-test