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

R

top next

Q-R-glued
Q-R-glued-composes
Q-R-glued-conditional
Q-R-glued-empty
Q-R-glued-first
Q-R-glued_wf
Q-R-glues
Q-R-glues-composes
Q-R-glues-composes2
Q-R-glues-conditional
Q-R-glues-conditional2
Q-R-glues-empty
Q-R-glues-property
Q-R-glues-split
Q-R-glues-trivial-restrict
Q-R-glues-trivial-split
Q-R-glues_functionality
Q-R-glues_wf
Q-R-pre-preserving
Q-R-pre-preserving-1-1
Q-R-pre-preserving-compose
Q-R-pre-preserving-conditional
Q-R-pre-preserving-rewrite-test
Q-R-pre-preserving_functionality_wrt_implies
Q-R-pre-preserving_wf
R-closed
R-closed_wf
R-decls-compat
algebra_act_times_r
and_false_r
and_true_r
bm_double_R
bm_double_R_wf
bm_single_R
bm_single_R_wf
comp_id_r
exists_over_and_r
glued-Q-R-glued
grp_eq_op_r
grp_op_cancel_r
grp_op_r
imax_add_r
imin_add_r
mod_action_mssum_r
mod_action_when_r
mod_times_mssum_r
module_act_minus_r
module_act_zero_r
mset_sum_ident_r
mset_union_ident_r
ndiff_id_r
oal_nil_ident_r
omral_action_plus_r
omral_times_ident_r
or_false_r
or_true_r
r-ap
r-ap_functionality
r-ap_wf
r-archimedean
r-archimedean-rabs
r-archimedean2
r-bound
r-bound-property
r-bound_wf
r-rational
r-rational_wf
r-strict-bound-property
r-triangle-inequality
r-triangle-inequality2
rng_times_lsum_r
rng_times_mssum_r
rng_times_nat_op_r
rng_times_sum_r
rng_times_when_r
ses-R
ses-R_wf
set_blt_functionality_wrt_set_lt_r

R1

prev top next

omral_action_times_r1

R2

prev top next

omral_action_times_r2

RABS

prev top next

r-archimedean-rabs
rabs
rabs-Riemann-sum
rabs-abs
rabs-approx
rabs-as-rmax
rabs-bounds
rabs-difference-bound-iff
rabs-difference-bound-rleq
rabs-difference-lower-bound
rabs-difference-rmax
rabs-difference-symmetry
rabs-int
rabs-neq-zero
rabs-nonneg
rabs-nonzero-on-compact
rabs-of-nonneg
rabs-of-nonpos
rabs-positive
rabs-positive-iff
rabs-rabs
rabs-rdiv
rabs-rinv
rabs-rminus
rabs-rmul
rabs-rmul-rleq
rabs-rmul-rleq-rabs
rabs-rnexp
rabs-rsum
rabs-ub
rabs_functionality
rabs_functionality_wrt_bdd-diff
rabs_wf
radd-list-rabs
req-iff-rabs-rleq
rneq-iff-rabs
zero-rleq-rabs

RADD

prev top next

radd
radd-ac
radd-as-radd-list
radd-assoc
radd-bdd-diff
radd-int
radd-int-fractions
radd-limit
radd-list
radd-list-append
radd-list-cons
radd-list-linearity
radd-list-linearity1
radd-list-linearity2
radd-list-linearity3
radd-list-one
radd-list-rabs
radd-list_functionality
radd-list_functionality_wrt_permutation
radd-list_functionality_wrt_rleq
radd-list_wf
radd-list_wf-bag
radd-positive-implies
radd-preserves-req
radd-preserves-rleq
radd-preserves-rless
radd-rdiv
radd-rmax
radd-rmin
radd-rminus
radd-rminus-assoc
radd-rminus-both
radd-zero
radd-zero-both
radd_assoc
radd_comm
radd_comm_eq
radd_functionality
radd_functionality_wrt_rleq
radd_functionality_wrt_rless1
radd_functionality_wrt_rless2
radd_list_nil_lemma
radd_wf
rminus-radd
rnonneg-radd
rpositive-radd

RADD2

prev top next

rpositive-radd2

RAISE

prev top next

raise-left-endpoint
raise-left-endpoint-rless
raise-left-endpoint_wf
raise-lower-endpoints-rless

RAMSEY

prev top next

Veldman-Ramsey

RANDOM

prev top next

find-random
find-random_wf
open-random-variable
random
random-variable
random-variable_wf
random_wf
subtype_rel-random-variable

RANDOMNESS

prev top next

randomness

RANGE

prev top next

continuous-compact-range-totally-bounded
continuous-range-totally-bounded
divisor-in-range
fpf-join-range
inf-range
name-morph-range
name-morph-range_wf
range-inf
range-inf-property
range-inf_wf
range-sup
range-sup-property
range-sup_wf
range_sublist
sup-range

RANK

prev top next

C_TYPE-rank
C_TYPE-rank_wf
MMTree-rank
MMTree-rank_wf
MTree-rank
MTree-rank_wf
es-rank
es-rank-wf-base
es-rank_le
es-rank_property
es-rank_property-base
es-rank_wf
pi-rank
pi-rank-choices
pi-rank-choices_wf
pi-rank-pi-replace
pi-rank-pi-simple-subst
pi-rank-pi-simple-subst-aux
pi-rank_wf
rank-Ex1
rank-Ex1_wf
rank-comm
rank-comm-decompose
rank-new
rank-new-decompose
rank-option
rank-option-decompose
rank-par
rank-par-decompose
rank-pi-choices
rank-rep
rank-rep-decompose
rank-zero

RANKED

prev top next

locally-ranked-induction
locally-ranked-is-well-founded
ranked-eo
ranked-eo-E
ranked-eo-E-sq
ranked-eo-base-E
ranked-eo-before
ranked-eo-causl
ranked-eo-dom
ranked-eo-eq-E
ranked-eo-first
ranked-eo-info
ranked-eo-info-before
ranked-eo-info-le-before
ranked-eo-loc
ranked-eo-locl
ranked-eo-pred
ranked-eo-property
ranked-eo_wf
ranked-lists-to-extended-eo

RANKEX1

prev top next

RankEx1
RankEx1-definition
RankEx1-ext
RankEx1-induction
RankEx1_Leaf
RankEx1_Leaf-leaf
RankEx1_Leaf-leaf_wf
RankEx1_Leaf?
RankEx1_Leaf?_wf
RankEx1_Leaf_wf
RankEx1_List
RankEx1_List-list
RankEx1_List-list_wf
RankEx1_List?
RankEx1_List?_wf
RankEx1_List_wf
RankEx1_Prod
RankEx1_Prod-prod
RankEx1_Prod-prod_wf
RankEx1_Prod?
RankEx1_Prod?_wf
RankEx1_ProdL
RankEx1_ProdL-prodl
RankEx1_ProdL-prodl_wf
RankEx1_ProdL?
RankEx1_ProdL?_wf
RankEx1_ProdL_wf
RankEx1_ProdR
RankEx1_ProdR-prodr
RankEx1_ProdR-prodr_wf
RankEx1_ProdR?
RankEx1_ProdR?_wf
RankEx1_ProdR_wf
RankEx1_Prod_wf
RankEx1_ind
RankEx1_ind_wf
RankEx1_ind_wf_simple
RankEx1_size
RankEx1_size_wf
RankEx1_wf

RANKEX1CO

prev top next

RankEx1co
RankEx1co-ext
RankEx1co_size
RankEx1co_size_wf
RankEx1co_wf

RANKEX2

prev top next

RankEx2
RankEx2-definition
RankEx2-defop
RankEx2-defop-extract
RankEx2-ext
RankEx2-induction
RankEx2_LeafS
RankEx2_LeafS-leafs
RankEx2_LeafS-leafs_wf
RankEx2_LeafS?
RankEx2_LeafS?_wf
RankEx2_LeafS_wf
RankEx2_LeafT
RankEx2_LeafT-leaft
RankEx2_LeafT-leaft_wf
RankEx2_LeafT?
RankEx2_LeafT?_wf
RankEx2_LeafT_wf
RankEx2_ListProd
RankEx2_ListProd-listprod
RankEx2_ListProd-listprod_wf
RankEx2_ListProd?
RankEx2_ListProd?_wf
RankEx2_ListProd_wf
RankEx2_Prod
RankEx2_Prod-prod
RankEx2_Prod-prod_wf
RankEx2_Prod?
RankEx2_Prod?_wf
RankEx2_Prod_wf
RankEx2_Union
RankEx2_Union-union
RankEx2_Union-union_wf
RankEx2_Union?
RankEx2_Union?_wf
RankEx2_UnionList
RankEx2_UnionList-unionlist
RankEx2_UnionList-unionlist_wf
RankEx2_UnionList?
RankEx2_UnionList?_wf
RankEx2_UnionList_wf
RankEx2_Union_wf
RankEx2_ind
RankEx2_ind-unroll
RankEx2_ind_wf
RankEx2_ind_wf_simple
RankEx2_size
RankEx2_size_wf
RankEx2_wf

RANKEX2CO

prev top next

RankEx2co
RankEx2co-ext
RankEx2co_size
RankEx2co_size_wf
RankEx2co_wf

RANKEX4

prev top next

RankEx4
RankEx4-definition
RankEx4-ext
RankEx4-induction
RankEx4_Foo
RankEx4_Foo-foo
RankEx4_Foo-foo_wf
RankEx4_Foo?
RankEx4_Foo?_wf
RankEx4_Foo_wf
RankEx4_ind
RankEx4_ind_wf
RankEx4_ind_wf_simple
RankEx4_size
RankEx4_size_wf
RankEx4_wf

RANKEX4CO

prev top next

RankEx4co
RankEx4co-ext
RankEx4co_size
RankEx4co_size_wf
RankEx4co_wf

RAT

prev top next

rat-to-real
rat-to-real-req
rat-to-real_wf

RATIO

prev top next

exp-ratio
exp-ratio-property
exp-ratio_wf
fun-ratio-test
ratio-dist
ratio-dist_wf
ratio-test
ratio-test-ext

RATIONAL

prev top next

free-from-atom-rational
int-rational
locally-non-constant-rational
locally-non-constant-rational_wf
locally-non-constant-via-rational
mk-rational
mk-rational-qdiv
mk-rational_wf
near-root-rational
near-root-rational-ext
nth-rational
nth-rational_wf
r-rational
r-rational_wf
rational-approx
rational-approx-property
rational-approx-property-ext
rational-approx-property1
rational-approx-property2
rational-approx_wf
rational-form-has-value
rational-has-value
rational-has-value2

RATIONALS

prev top next

equipollent-nat-rationals
equipollent-nat-rationals-ext
equipollent-rationals
first-25-rationals
int-eq-in-rationals
int-equal-in-rationals
int-subtype-rationals
int_inc_rationals
rationals
rationals-dense
rationals-dense-ext
rationals-value-type
rationals-valueall-type
rationals_wf

RAVG

prev top next

ravg
ravg-between
ravg_wf

RBETWEEN

prev top next

rbetween
rbetween_wf

RCC

prev top next

rcc-subinterval

RCCINT

prev top next

left_endpoint_rccint_lemma
member_rccint_lemma
rccint
rccint-icompact
rccint_wf
right_endpoint_rccint_lemma

RCIINT

prev top next

member_rciint_lemma
rciint
rciint_wf

RCOINT

prev top next

member_rcoint_lemma
rcoint
rcoint_wf

RCV

prev top next

consensus-rcv
consensus-rcv-crosses-size
consensus-rcv-crosses-threshold
consensus-rcv_wf
cs-initial-rcv
cs-initial-rcv_wf
cs-rcv-vote
cs-rcv-vote_wf
decidable__equal_consensus-rcv
isrcv_rcv_lemma
kindcase-rcv
lnk_rcv_lemma
local_or_rcv
locl_rcv_lemma
not_locl_rcv
not_rcv_locl
pv11_p1_acc_rcv_p2a
pv11_p1_acc_rcv_p2a2
rcv
rcv-vote?
rcv-vote?_wf
rcv_locl_lemma
rcv_one_one
rcv_rcv_lemma
rcv_wf
send-rcv-match
send-rcv-match_wf
ses-rcv
ses-rcv_wf
tag_rcv_lemma

RCVD

prev top next

assert-rcvd-inning-eq
assert-rcvd-inning-gt
rcvd-inning-eq
rcvd-inning-eq_wf
rcvd-inning-gt
rcvd-inning-gt_wf
rcvd-innings-nil
rcvd-vote
rcvd-vote_wf

RCVS

prev top next

consensus-rcvs-to-consensus-events
consensus-rcvs-to-consensus-events_wf
graph-rcvs
graph-rcvs_wf
graph-rcvs_wf2
member-graph-rcvs
member-rcvs-on
pi2-consensus-rcvs-to-consensus-events
rcvs-on
rcvs-on-links-from-to
rcvs-on_wf

RCVSET

prev top next

assert-graph-rcvset
assert-rcvset
graph-rcvset
graph-rcvset_wf
rcvset
rcvset_wf

RDIV

prev top next

continuous-rdiv
derivative-rdiv
derivative-rdiv-const
int-rdiv
int-rdiv-int-rmul
int-rdiv-one
int-rdiv-req
int-rdiv_wf
rabs-rdiv
radd-rdiv
rdiv
rdiv-factorial-lemma1
rdiv-factorial-lemma2
rdiv-factorial-limit-zero
rdiv-rdiv
rdiv-self
rdiv-zero
rdiv_functionality
rdiv_wf
rminus-rdiv
rmul-int-rdiv
rmul-rdiv
rmul-rdiv-cancel
rmul-rdiv-cancel2
rmul-rdiv-cancel3
rmul-rdiv-cancel4
rmul-rdiv-cancel5
rmul-rdiv-cancel6
rmul-rdiv-cancel7
rmul-rdiv-cancel8
rmul-rdiv-cancel9
rmul-rdiv-one
rnexp-rdiv
rsub-rdiv

RDIV2

prev top next

rminus-rdiv2
rmul-int-rdiv2
rmul-rdiv2

REACHABILITY1

prev top next

consensus-ts6-reachability1

REACHABLE

prev top next

committed-inning0-reachable
consensus-reachable
cs-possible-state-reachable
fresh-inning-reachable
rel-preserving-star-reachable
ts-init_wf_reachable
ts-reachable
ts-reachable-induction
ts-reachable-induction2
ts-reachable-induction3
ts-reachable_wf
ts-refinement-reachable

REACHABLE2

prev top next

ts-refinement-reachable2

READ

prev top next

decl-set-read-allowed
state-var-read-allowed

READY

prev top next

nysiad_on_ready
nysiad_on_ready_wf
nysiad_ready'base
nysiad_ready'base-program
nysiad_ready'base-program_wf
nysiad_ready'base_wf
nysiad_ready'send
nysiad_ready'send_wf

REAL

prev top next

find-real-neq
find-real-neq2
i-real
i-real_wf
implies-real
int-to-real
int-to-real_wf
neg-approx-of-nonneg-real
proper-real-continuity
proper-real-continuity_wf
rat-to-real
rat-to-real-req
rat-to-real_wf
real
real-binomial
real-continuity-principle
real-continuity-principle_wf
real-continuity1
real-continuity1-ext
real-continuity2
real-continuity2-ext
real-continuity3
real-continuity4
real-continuity4-ext
real-has-value
real-has-valueall
real-list-has-valueall
real-valueall-type
real-vec
real-vec-add
real-vec-add_wf
real-vec-mul
real-vec-mul_wf
real-vec-norm
real-vec-norm-mul
real-vec-norm-nonneg
real-vec-norm-squared
real-vec-norm_functionality
real-vec-norm_wf
real-vec-sub
real-vec-sub_wf
real-vec_wf
real_wf
small-reciprocal-real
small-reciprocal-real-ext
valueall-type-real-list

REALIZER

prev top next

fan-realizer
fan-realizer_test
fan-realizer_test2
fan-realizer_wf

REALIZES

prev top next

system-realizes
system-realizes_wf
system-strongly-realizes
system-strongly-realizes-and
system-strongly-realizes-and1
system-strongly-realizes_functionality
system-strongly-realizes_wf

REALS

prev top next

int-int-retraction-reals
reals-uncountable
reals-uncountable-simple
sample reals lemmas

REASONING

prev top next

test-es-first-reasoning

RECEIPT

prev top next

nysiad_on_receipt_msg
nysiad_on_receipt_msg_wf

RECIND

prev top next

recind-ycomb

RECIPROCAL

prev top next

small-reciprocal-real
small-reciprocal-real-ext
small-reciprocal-rneq-zero
triangular-reciprocal-series-sum

RECODE

prev top next

fst-recode-tuple
recode-tuple
recode-tuple_wf

RECODING

prev top next

tuple-recoding
tuple-recoding_wf
type-recoding
type-recoding_wf

RECODINGS

prev top next

compose-tuple-recodings
compose-tuple-recodings_wf

RECORD

prev top next

eo-record-record
eo-record-record-eq
eo-record-type
eo-record-type_wf
eo_record
eo_record_cumulative
eo_record_wf
identity-record+-update
identity-record-update
isect2-record
mk-eo-record
mk-eo-record_wf
record
record+
record+_extensionality
record+_record
record+_subtype_rel
record+_wf
record-select
record-select-update
record-select_wf
record-select_wf2
record-update
record-update-update
record-update_wf
record_extensionality
record_wf
subtype_rel_record
subtype_rel_record+
subtype_rel_record+_easy
trivial-record-update

RECPROCESS

prev top next

recprocess
recprocess_wf

RECURSION

prev top next

bar-recursion
bar-recursion_wf
bar_recursion
bar_recursion_wf
bar_recursion_wf0
bar_recursion_wf_strong
bbar-recursion
bbar-recursion_wf
es-interface-equality-prior-recursion
es-interface-equality-recursion
mutual-primitive-recursion

RED

prev top next

hdf_halted_halt_red_lemma
hdf_halted_inl_red_lemma
hdf_halted_run_red_lemma
hdf_out_halt_red_lemma
list_acc_cons_red_lemma
list_acc_nil_red_lemma
red-black-example
red-black-example-ext
test-red-black-example

REDEX

prev top next

fact0_redex_lemma

REDUC

prev top next

posint_reduc_dec

REDUCE

prev top next

add_reduce_eqmod
atomdeq_reduce_lemma
bag-reduce
bag-reduce_wf
binary_map_case_E_reduce_lemma
binary_map_case_T_reduce_lemma
bm_cnt_prop0_E_reduce_lemma
bm_cnt_prop_E_reduce_lemma
bm_count_E_reduce_lemma
bm_numItems_E_reduce_lemma
bm_numItems_T_reduce_lemma
callbyvalueall-reduce-repeat
callbyvalueall-reduce-repeat-right-branch
cbv-reduce-strict
comb_for_mon_reduce_wf
combine-list-as-reduce
combine-reduce
evalall-reduce
filter_filter_reduce
gcd-reduce
gcd-reduce-ext
gcd_reduce
gcd_reduce_property
gcd_reduce_wf
hd-as-reduce
imax-list-as-reduce
intdeq_reduce_lemma
ite_and_reduce
l_all_assert_iff_reduce
l_all_reduce
l_exists_reduce
l_sum_as_reduce
l_sum_as_reduce_general
lift-reduce-face-map
list_accum_as_reduce
list_accum_is_reduce
map-simple-reduce
map_reduce_spread2_to_reduce
mapfilter-as-reduce
mapfilter-reduce
mon_reduce
mon_reduce_append
mon_reduce_eq_itop
mon_reduce_functionality_wrt_permr
mon_reduce_wf
proddeq_reduce_lemma
productdeq_reduce_lemma
reduce
reduce-append
reduce-as-accum
reduce-as-combine-list
reduce-bool-bfalse
reduce-fast-mapfilter1
reduce-fast-mapfilter2
reduce-id
reduce-ifthenelse
reduce-map
reduce-mapfilter
reduce-permutation
reduce_cons_lemma
reduce_hd_cons_lemma
reduce_nil_lemma
reduce_tl_cons_lemma
reduce_tl_nil_lemma
reduce_wf
select-as-reduce
select-front-as-reduce

REDUCE2

prev top next

comb_for_reduce2_wf
mapfilter-as-reduce2
reduce2
reduce2_cons_lemma
reduce2_nil_lemma
reduce2_shift
reduce2_wf

REDUCIBLE

prev top next

decidable__reducible
reducible
reducible-nat
reducible_wf

REF

prev top next

consensus-ts4-ref-map
consensus-ts4-ref-map1
cs-ref-map-changed
cs-ref-map-constraints
cs-ref-map-constraints_wf
cs-ref-map-equal
cs-ref-map-step
cs-ref-map-unchanged
cs-ref-map3
cs-ref-map3-ambivalent
cs-ref-map3-decided
cs-ref-map3-predecided
cs-ref-map3_wf
three-consensus-ref-map
three-consensus-ref-map_wf

REFINEMENT

prev top next

Riemann-sum-refinement
frs-increasing-separated-common-refinement
partition-refinement-sum
separated-partitions-have-common-refinement
ts-refinement
ts-refinement-composition
ts-refinement-reachable
ts-refinement-reachable2
ts-refinement_wf

REFINEMENT1

prev top next

consensus-refinement1

REFINEMENT2

prev top next

consensus-refinement2

REFINEMENT3

prev top next

consensus-refinement3

REFINEMENT4

prev top next

consensus-refinement4

REFINEMENT5

prev top next

consensus-refinement5

REFINES

prev top next

frs-refines
frs-refines_transitivity
frs-refines_weakening
frs-refines_wf
partition-refines
partition-refines-cons
partition-refines_transitivity
partition-refines_weakening
partition-refines_wf
uniform-partition-refines

REFL

prev top next

Accum-class-trans-refl
Memory-class-trans-refl
Memory-loc-class-trans-refl
State-comb-trans-refl
State-loc-comb-trans-refl
bm_compare_refl_eq
bm_compare_refl_le
comparison-refl
cubical-refl
cubical-refl_wf
dset_eq_refl
eu-congruent-refl
l_subset_refl
mdivides_refl
ocmon_refl
pv11_p1_leq_bnum_refl
qeq-refl
qeq_refl
qoset_refl
refl
refl-path
refl-path_wf
refl_cl
refl_cl_is_order
refl_cl_sp_cancel
refl_cl_sp_le_rel
refl_cl_wf
refl_functionality_wrt_iff
refl_shift
refl_wf
rel_le_refl_cl_sp
rel_le_sp_refl_cl
sp_refl_cl_cancel
sp_refl_cl_le_rel
sq_stable__refl

REFLEX

prev top next

per-partial-reflex
permr_reflex
set-equal-reflex

REFLEXIVE

prev top next

causal_order_reflexive
comparison-reflexive
eq_atom-reflexive
fpf-single-sub-reflexive
fpf-sub-reflexive
le_reflexive
less_than_anti-reflexive
t-sqle_reflexive
wellfounded-anti-reflexive

REFLEXIVITY

prev top next

divides_reflexivity
predicate_implies_reflexivity

REG

prev top next

reg-less
reg-less_wf
reg-seq-add
reg-seq-add_functionality_wrt_bdd-diff
reg-seq-add_wf
reg-seq-adjust
reg-seq-adjust-property
reg-seq-adjust_wf
reg-seq-inv
reg-seq-inv_wf
reg-seq-list-add
reg-seq-list-add-as-l_sum
reg-seq-list-add_functionality_wrt_bdd-diff
reg-seq-list-add_functionality_wrt_permutation
reg-seq-list-add_wf
reg-seq-mul
reg-seq-mul-assoc
reg-seq-mul-comm
reg-seq-mul-regular
reg-seq-mul_functionality_wrt_bdd-diff
reg-seq-mul_wf
reg-seq-mul_wf2
reg-seq-nexp
reg-seq-nexp_wf
rmul-bdd-diff-reg-seq-mul

REGULAR

prev top next

assert-regular-upto
bdd-diff-regular
bdd-diff-regular-int-seq
implies-regular
reg-seq-mul-regular
regular-consistency
regular-int-seq
regular-int-seq_wf
regular-less
regular-less-iff
regular-upto
regular-upto-regularize
regular-upto_wf
regularize-2-regular
rroot-odd-2-regular
sq_stable__regular-int-seq

REGULARITY

prev top next

rroot-regularity-lemma

REGULARIZE

prev top next

regular-upto-regularize
regularize
regularize-2-regular
regularize_wf

REINDEX

prev top next

bag-summation-reindex
fps-product-reindex
sum-reindex

REINDEX2

prev top next

sum-reindex2

REJECT

prev top next

reject
reject_cons_hd
reject_cons_hd_sq
reject_cons_tl
reject_cons_tl_sq
reject_eq_firstn_nth_tl
reject_wf
select_reject_permr

REL

prev top next

W-rel
W-rel_wf
accum_filter_rel
accum_filter_rel_nil
accum_filter_rel_wf
acyclic-rel
acyclic-rel_wf
append_rel
append_rel_wf
assoced_equiv_rel
bind-class-rel
bind-class-rel-weak
cWO-rel
cWO-rel-path-barred
cWO-rel_wf
causal-class-rel-in-out
causal-class-rel-in-out_wf
combine-list-rel-and
combine-list-rel-or
cond_rel_equivalent
cond_rel_exp_monotone
cond_rel_implies
cond_rel_implies_wf
cond_rel_star_equiv
cond_rel_star_monotone
cond_rel_star_monotonic
consensus-rel
consensus-rel-add-knowledge-step
consensus-rel-add-knowledge-step_wf
consensus-rel-knowledge
consensus-rel-knowledge-archive-step
consensus-rel-knowledge-archive-step_wf
consensus-rel-knowledge-inning-step
consensus-rel-knowledge-inning-step_wf
consensus-rel-knowledge-step
consensus-rel-knowledge-step_wf
consensus-rel-knowledge_wf
consensus-rel-mod
consensus-rel-mod_wf
consensus-rel_wf
consensus-ts4-estimate-rel
consensus-ts4-inning-rel
decidable-last-rel
decidable__rel_exp
decidable__rel_exp_finite
decidable__rel_plus
dep-eclass_subtype_rel
double_isect_subtype_rel
eclass_subtype_rel
eqmod_equiv_rel
equal_functionality_wrt_subtype_rel
equiv_rel
equiv_rel-wf-quotient
equiv_rel_and
equiv_rel_functionality_wrt_iff
equiv_rel_iff
equiv_rel_isect2
equiv_rel_quotient
equiv_rel_self_functionality
equiv_rel_squash
equiv_rel_subtype
equiv_rel_subtyping
equiv_rel_true
equiv_rel_wf
es-E-interface-conditional-subtype_rel
es-E-interface-subtype_rel
es-E-interface-subtype_rel-implies
es-class-causal-rel
es-class-causal-rel-fail
es-class-causal-rel-fail_wf
es-class-causal-rel-iff-bijection
es-class-causal-rel_wf
es-interface-subtype_rel
finite-acyclic-rel
fun-equiv-rel
gcd_p_zero_rel
inv-rel
inv-rel-inject
inv-rel_wf
isect-rel
isect-rel_wf
isect2_functionality_wrt_subtype_rel
isect2_subtype_rel
isect_subtype_rel
isect_subtype_rel_trivial
lifted-rel
lifted-rel_wf
massoc_equiv_rel
nary-rel
nary-rel-predicate
nary-rel-predicate_wf
nary-rel_wf
no_rel_repeats
no_rel_repeats_wf
non-forking-rel_exp
not_subtype_rel
param-W-rel
param-W-rel_wf
pcw-path-rel
pcw-path-rel_wf
per-partial-equiv_rel
permr_equiv_rel
permr_massoc_rel
permr_massoc_rel_wf
permr_upto_equiv_rel
record+_subtype_rel
refl_cl_sp_le_rel
rel-connected
rel-connected_transitivity
rel-connected_weakening
rel-connected_wf
rel-continuous
rel-continuous_wf
rel-exp-add-1-iff
rel-exp-add-iff
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-monotone
rel-monotone_wf
rel-path
rel-path-between
rel-path-between-append
rel-path-between-cons
rel-path-between_wf
rel-path_wf
rel-plus-rel-immediate
rel-plus-rel-star
rel-pre-preserving
rel-pre-preserving-compose
rel-pre-preserving_wf
rel-preserving
rel-preserving-composes
rel-preserving-star
rel-preserving-star-reachable
rel-preserving_wf
rel-rel-plus
rel-restriction
rel-restriction-implies
rel-restriction_wf
rel-star-iff-rel-plus
rel-star-iff-rel-plus-or
rel-star-rel-plus
rel-star-rel-plus2
rel-star-rel-plus3
rel_equivalent
rel_equivalent_inversion
rel_equivalent_transitivity
rel_equivalent_weakening
rel_equivalent_wf
rel_exp
rel_exp-iff-path
rel_exp-one-one
rel_exp0
rel_exp_add
rel_exp_add-ext
rel_exp_add_iff
rel_exp_functionality_wrt_breqv
rel_exp_functionality_wrt_brle
rel_exp_functionality_wrt_iff
rel_exp_functionality_wrt_rel_implies
rel_exp_iff
rel_exp_iff2
rel_exp_monotone
rel_exp_one
rel_exp_wf
rel_finite
rel_finite-restrict
rel_finite_wf
rel_implies
rel_implies_functionality
rel_implies_or_left
rel_implies_or_right
rel_implies_transitivity
rel_implies_weakening
rel_implies_wf
rel_inverse
rel_inverse_exp
rel_inverse_star
rel_inverse_wf
rel_le_refl_cl_sp
rel_le_sp_refl_cl
rel_or
rel_or-restriction
rel_or_idempotent
rel_or_wf
rel_path
rel_path_wf
rel_plus
rel_plus-TI
rel_plus-iff-path
rel_plus-of-restriction
rel_plus-restriction-equiv
rel_plus-uniform-TI
rel_plus-weak-TI
rel_plus_closure
rel_plus_field
rel_plus_functionality_wrt_breqv
rel_plus_functionality_wrt_brle
rel_plus_functionality_wrt_iff
rel_plus_functionality_wrt_rel_implies
rel_plus_idempotent
rel_plus_iff
rel_plus_iff2
rel_plus_implies
rel_plus_implies2
rel_plus_irreflexive
rel_plus_minimal
rel_plus_monotone
rel_plus_strongwellfounded
rel_plus_trans
rel_plus_wf
rel_rel_star
rel_rev_implies
rel_rev_implies_weakening
rel_rev_implies_wf
rel_star
rel_star-iff-path
rel_star_closure
rel_star_closure2
rel_star_functionality_wrt_breqv
rel_star_functionality_wrt_brle
rel_star_functionality_wrt_rel_implies
rel_star_iff
rel_star_iff2
rel_star_monotone
rel_star_monotonic
rel_star_of_equiv
rel_star_order
rel_star_symmetric
rel_star_symmetric_2
rel_star_trans
rel_star_transitivity
rel_star_transitivity_ext
rel_star_weakening
rel_star_wf
rev_subtype_rel
rev_subtype_rel_weakening
rev_subtype_rel_wf
ses-key-rel
ses-key-rel_wf
ses-key-rel_witness
sp_refl_cl_le_rel
split-at-first-rel
split_rel_last
split_tail_rel
sq_exists_subtype_rel
sq_stable__rel_path
sq_stable__subtype_rel
sqle_n_subtype_rel
squash_thru_equiv_rel
squash_thru_uequiv_rel
strongwellfounded_rel_exp
subtype_rel
subtype_rel-deq
subtype_rel-equal
subtype_rel-int_seg
subtype_rel-labeled-graph
subtype_rel-ldag
subtype_rel-per-set
subtype_rel-random-variable
subtype_rel-tag-by
subtype_rel-tag-case
subtype_rel_algebra
subtype_rel_b-union
subtype_rel_b-union-left
subtype_rel_b-union-right
subtype_rel_b-union_iff
subtype_rel_bag
subtype_rel_colist
subtype_rel_comparison
subtype_rel_dep_function
subtype_rel_dep_function_iff
subtype_rel_dep_product_iff
subtype_rel_double_isect
subtype_rel_fset
subtype_rel_function
subtype_rel_functionality_wrt_iff
subtype_rel_functionality_wrt_implies
subtype_rel_grp
subtype_rel_header-type-spec
subtype_rel_image
subtype_rel_int_mod
subtype_rel_isect
subtype_rel_isect-2
subtype_rel_isect2
subtype_rel_isect_as_subtyping_lemma
subtype_rel_isect_general
subtype_rel_list
subtype_rel_list-iff
subtype_rel_list_set
subtype_rel_nested_set
subtype_rel_nested_set2
subtype_rel_not
subtype_rel_partial
subtype_rel_per-class
subtype_rel_poset
subtype_rel_product
subtype_rel_quotient
subtype_rel_quotient_trivial
subtype_rel_record
subtype_rel_record+
subtype_rel_record+_easy
subtype_rel_rng_sig
subtype_rel_self
subtype_rel_set
subtype_rel_set_simple
subtype_rel_sets
subtype_rel_simple_product
subtype_rel_sum
subtype_rel_tagged+
subtype_rel_tagged+_general
subtype_rel_transitivity
subtype_rel_tunion
subtype_rel_tuple-type
subtype_rel_union
subtype_rel_union_left
subtype_rel_union_right
subtype_rel_unordered-combination
subtype_rel_vatype
subtype_rel_weakening
subtype_rel_wf
symmetric_rel_or
tagged+_subtype_rel
test-rel-connected
trans_rel_func_wrt_sym_self
trans_rel_self_functionality
ts-rel
ts-rel_wf
ts-stable-rel
ts-stable-rel_wf
two-class-equiv-rel
uequiv_rel
uequiv_rel_functionality_wrt_iff
uequiv_rel_iff
uequiv_rel_self_functionality
uequiv_rel_subtyping
uequiv_rel_wf
utrans_rel_self_functionality
wellfounded-acyclic-rel
xxequiv_rel
xxequiv_rel_wf

REL2

prev top next

dep-eclass_subtype_rel2
equal_functionality_wrt_subtype_rel2
es-interface-subtype_rel2
isect2_subtype_rel2

REL3

prev top next

isect2_subtype_rel3

RELATION

prev top next

causal-class-relation
causal-class-relation_wf
correct-causal-class-relation
correct-causal-class-relation_wf
embedding-preserves-local-relation
es-local-relation
es-local-relation_wf
flow-graph-information-flow-relation
fun-connected-relation
information-flow-relation
information-flow-relation_wf
iseg-local-relation

RELEASE

prev top next

nonce-release-lemma
nonce-release-lemma2
release-before
release-before_wf
ses-nonce-release
sig-release-thread
sig-release-thread_wf
signature-release-lemma
signature-release-lemma2

RELIABLE

prev top next

reliable-env
reliable-env-property
reliable-env-property1
reliable-env-property2
reliable-env_wf
std-env-reliable

RELN

prev top next

assoc_reln

RELS

prev top next

l-ordered-eq-rels
rels_iso
rels_iso_wf
sorted-by-eq-rels

REM

prev top next

combinations_aux_rem
combinations_aux_rem_property
combinations_aux_rem_wf
div_rem_sum
div_rem_sum2
divides_iff_rem_zero
exp-rem
exp-rem-property
exp-rem_wf
fun_exp-rem
int-rem-exception
iseg_product_rem
iseg_product_rem_property
iseg_product_rem_wf
one-rem
quot_rem_exists
quot_rem_exists_n
rem-mul
rem-one
rem-sign
rem-zero
rem-zero-implies-minus
rem_2_to_1
rem_3_to_1
rem_4_to_1
rem_add1
rem_addition
rem_antisym
rem_base_case
rem_base_case_z
rem_bounds_1
rem_bounds_2
rem_bounds_3
rem_bounds_4
rem_bounds_absval
rem_bounds_absval_le
rem_bounds_z
rem_eq_args
rem_eq_args_z
rem_fun_sat_rem_nrel
rem_gen_base_case
rem_invariant
rem_mag_bound
rem_mul
rem_mul2
rem_nrel
rem_nrel_wf
rem_rec_case
rem_rem_to_rem
rem_sym
rem_sym_1
rem_sym_1a
rem_sym_2
rem_to_div
zero-div-rem
zero-rem

REMAINDER

prev top next

Taylor-remainder
Taylor-remainder_wf
comb_for_remainder_wf
iseg-remainder-as-filter
remainder def
remainder_wf
remainder_wfa
strictness-remainder-left
strictness-remainder-right

REMAINDER1

prev top next

chinese-remainder1

REMAINDER2

prev top next

chinese-remainder2
chinese-remainder2-extract

REMOVE

prev top next

add-remove-fresh-cname
add-remove-fresh-cname
add-remove-fresh-sq
add-remove-nth
bag-member-remove
bag-member-remove-repeats
bag-remove
bag-remove-append
bag-remove-repeats
bag-remove-repeats-append
bag-remove-repeats-eq-remove-repeats
bag-remove-repeats-filter
bag-remove-repeats-if-no-repeats
bag-remove-repeats-no-repeats
bag-remove-repeats_wf
bag-remove-size
bag-remove-size-member-no-repeats
bag-remove-trivial
bag-remove_wf
bm_remove
bm_remove_wf
bm_try_remove
bm_try_remove_wf
count-bag-remove-repeats
es-cut-remove
es-cut-remove-1
fset-add-remove
fset-remove
fset-remove_wf
fset-size-remove
int-decr-map-remove
int-decr-map-remove-prop
int-decr-map-remove_wf
is-dag-remove
l-ordered-remove-combine
l-ordered-remove-repeats-fun
length-remove-first
length-remove-first-le
length-remove-repeats
length-remove-repeats-le
lg-acyclic-remove
lg-all-remove
lg-connected-remove
lg-edge-remove
lg-label-remove
lg-remove
lg-remove-noop
lg-remove_wf
lg-remove_wf_dag
lg-size-remove
list-to-set-is-remove-repeats
list_accum-remove-repeats
lookup-list-map-remove
lookup-list-map-remove-prop
lookup-list-map-remove_wf
map-sig-remove
map-sig-remove_wf
member-bag-remove-repeats
member-fset-remove
member-remove-repeats
no_repeats-remove-first
null_remove_leading
remove-alist
remove-alist_wf
remove-combine
remove-combine-cons
remove-combine-implies-member
remove-combine-implies-member2
remove-combine-l-ordered-implies-member
remove-combine-nil
remove-combine_wf
remove-first
remove-first-cons
remove-first-member-implies
remove-first-no_repeats-member
remove-first_wf
remove-nat-missing
remove-nat-missing-prop
remove-nat-missing_wf
remove-nth
remove-nth_wf
remove-repeats
remove-repeats-append
remove-repeats-append-one
remove-repeats-append-one-member
remove-repeats-append-sq
remove-repeats-filter
remove-repeats-fun
remove-repeats-fun-as-filter
remove-repeats-fun-as-remove-repeats-map
remove-repeats-fun-length-as-remove-repeats-map
remove-repeats-fun-map
remove-repeats-fun-map2
remove-repeats-fun-member
remove-repeats-fun-nil
remove-repeats-fun-sublist
remove-repeats-fun_wf
remove-repeats-l_contains
remove-repeats-length-leq
remove-repeats-length-no-repeats
remove-repeats-length-no-repeats-iff
remove-repeats-length-one
remove-repeats-mapfilter-with-fun
remove-repeats-no_repeats
remove-repeats-no_repeats-true
remove-repeats-normal-form
remove-repeats-set-equal
remove-repeats-wf-bag
remove-repeats_functionality_wrt_permutation
remove-repeats_property
remove-repeats_wf
remove_leading
remove_leading_eq_nil
remove_leading_property
remove_leading_property2
remove_leading_wf
remove_repeats_cons_lemma
remove_repeats_nil_lemma
select-remove-first
set-equal-remove-repeats
set-sig-remove
set-sig-remove_wf
sub-bag-remove-if
sub-bag-remove-repeats-if-no-repeats

REMOVE1

prev top next

bag-count-remove1
bag-remove1
bag-remove1-property
bag-remove1-property1
bag-remove1_wf
bag-remove1_wf1
bag_remove1_aux
bag_remove1_aux_property
bag_remove1_aux_wf
comb_for_remove1_wf
cons_remove1_permr
count_remove1
name-morph_subtype_remove1
not_mem_remove1
remove1
remove1_cons_lemma
remove1_functionality_wrt_permr
remove1_nil_lemma
remove1_wf

RENAME

prev top next

cubical-type-ap-rename-one-equal
extend-name-morph-rename-one
fpf-inv-rename
fpf-inv-rename_wf
fpf-rename
fpf-rename-ap
fpf-rename-ap2
fpf-rename-cap
fpf-rename-cap2
fpf-rename-cap3
fpf-rename-dom
fpf-rename-dom2
fpf-rename_wf
kind-rename
kind-rename-inj
kind-rename_wf
mFOL-abstract-rename
mFOL-bound-rename
mFOL-boundvars-of-rename
mFOL-rename
mFOL-rename-bound-to-avoid
mFOL-rename-bound-to-avoid_wf
mFOL-rename_wf
msg-rename
msg-rename_wf
rename-one-comp
rename-one-extend-id
rename-one-extend-name-morph
rename-one-iota
rename-one-name
rename-one-name_wf
rename-one-same

REORDER

prev top next

l-ordered-reorder

REP

prev top next

CLK_headers_no_rep
CLK_headers_no_rep_wf
OARcast_headers_no_rep
OARcast_headers_no_rep_wf
bag-append-equal-bag-rep
bag-co-restrict-rep
bag-count-rep
bag-null-rep
bag-rep
bag-rep-add
bag-rep-is-single-valued
bag-rep-size-restrict
bag-rep_wf
bag-restrict-rep
bag-size-rep
fps-mul-coeff-bag-rep-simple
i-approx-rep
i-closed-finite-rep
list-rep
list-rep_wf
mapfilter-no-rep-fun
member-bag-rep
new_23_sig_headers_no_rep
new_23_sig_headers_no_rep_wf
nysiad_headers_no_rep
nysiad_headers_no_rep_wf
pi-rep-decompose
pi-rep-trans
pi-rep-trans-comment
pi-rep-trans_wf
pv11_p1_headers_no_rep
pv11_p1_headers_no_rep_wf
pv11_p1_rep_Ballot_Num
pv11_p1_rep_Ballot_Num_wf
rank-rep
rank-rep-decompose
rep-pre-sheaf
rep-pre-sheaf
rep-pre-sheaf_wf
rep-pre-sheaf_wf
select-bag-rep
single-valued-bag-is-rep
small-sparse-rep
small-sparse-rep-ext
sparse-rep-base
sparse-rep-base_wf
sparse-signed-rep
sparse-signed-rep-exists
sparse-signed-rep-exists-ext
sparse-signed-rep-lemma1
sparse-signed-rep-lemma1-ext
sparse-signed-rep_wf
strong-message-constraint-no-rep
strong-message-constraint-no-rep-implies
strong-message-constraint-no-rep-large
strong-message-constraint-no-rep-large-1hdr
strong-message-constraint-no-rep-large-implies
strong-message-constraint-no-rep-large_wf
strong-message-constraint-no-rep_wf
sub-bag-of-bag-rep
sub-bag-rep
sv-bag-is-bag-rep
sv-bag-is-bag-rep-lousy-proof
the-member-bag-rep

REP2

prev top next

i-approx-rep2

REPEAT

prev top next

callbyvalueall-reduce-repeat
callbyvalueall-reduce-repeat-right-branch
callbyvalueall-single-repeat

REPEATED

prev top next

three-cs-no-repeated-votes

REPEATS1

prev top next

bag-append-no-repeats1
member-count-repeats1
no_repeats-count-repeats1

REPEATS2

prev top next

bag-combine-no-repeats2
bag-filter-no-repeats2
es-interface-predecessors-no_repeats2
member-count-repeats2

REPEATS3

prev top next

member-count-repeats3

REPLACE

prev top next

pi-level-pi-replace
pi-rank-pi-replace
pi-replace
pi-replace_wf
prefix-replace
prefix-replace_wf

REPLICA

prev top next

new_23_sig_Replica
new_23_sig_Replica-program
new_23_sig_Replica-program_wf
new_23_sig_Replica_wf
new_23_sig_replica_state_from_proposal
new_23_sig_replica_state_from_proposal_fun
new_23_sig_replica_state_mem
new_23_sig_replica_state_mem_fun
new_23_sig_update_replica
new_23_sig_update_replica_wf
nysiad_Replica
nysiad_Replica-program
nysiad_Replica-program_wf
nysiad_Replica_wf
nysiad_deliver_to_replica
nysiad_deliver_to_replica_wf

REPLICAS

prev top next

nysiad_Replicas
nysiad_Replicas-program
nysiad_Replicas-program_wf
nysiad_Replicas_wf

REPLICASTATE

prev top next

new_23_sig_ReplicaState
new_23_sig_ReplicaState-classrel
new_23_sig_ReplicaState-functional
new_23_sig_ReplicaState-program
new_23_sig_ReplicaState-program_wf
new_23_sig_ReplicaState_wf

REPLICASTATEFUN

prev top next

new_23_sig_ReplicaStateFun
new_23_sig_ReplicaStateFun_wf

REPLY

prev top next

CLK_Reply
CLK_Reply-program
CLK_Reply-program_wf
CLK_Reply_wf
CLK_mk_reply
CLK_mk_reply_wf
es-class-reply-or-fail
es-class-reply-or-fail_wf

REPN

prev top next

length-repn
repn
repn_wf
select-repn

REPRESENTATIVES

prev top next

distinct-representatives
equipollent-distinct-representatives
l_disjoint-representatives

REQ

prev top next

Comm-req_from
Comm-req_from_wf
Riemann-sum-alt-req
cantor-interval-req
cantor-to-interval-req
int-rdiv-req
int-rmul-req
pointwise-req
pointwise-req_wf
poly-nth-deriv-req
radd-preserves-req
rat-to-real-req
req
req-equiv
req-iff-bdd-diff
req-iff-not-rneq
req-iff-rabs-rleq
req-int
req-int-fractions
req-int-fractions2
req-vec
req-vec_wf
req_functionality
req_inversion
req_transitivity
req_weakening
req_wf
req_witness
rmax-req
rmin-req
rmin-req-rminus-rmax
rmul_preserves_req
rnexp-req
rnexp-req-iff
rnexp-req-iff-even
rnexp-req-iff-odd
sq_stable__req

REQ2

prev top next

rmax-req2
rmin-req2

RES

prev top next

bag-member-classfun-res
classfun-res
classfun-res-base
classfun-res-base-classrel
classfun-res-disjoint-union-comb-as-parallel-eclass1
classfun-res-disjoint-union-comb-left
classfun-res-disjoint-union-comb-right
classfun-res-eclass1
classfun-res-eclass3
classfun-res-member-base
classfun-res-parallel-class-left
classfun-res-parallel-class-right
classfun-res_wf
classrel-classfun-res
classrel-classfun-res-alt1
classrel-classfun-res-alt2
classrel-implies-classfun-res
eo-forward-base-classfun-res
eo-forward-base-classfun-res-sq

RESET

prev top next

eo-reset-dom
eo-reset-dom-reset-dom
eo-reset-dom_wf
eo-reset-dom_wf_extended

RESIDUE

prev top next

quadratic-residue
quadratic-residue_functionality
quadratic-residue_wf
residue
residue-mul
residue-mul-assoc
residue-mul-inverse
residue-mul_wf
residue_wf

RESIDUES

prev top next

member-residues-mod
no_repeats-residues-mod
residues-equal-bags
residues-mod
residues-mod_wf
residues-permute

RESIGNED

prev top next

resigned
resigned_wf

RESPECTS

prev top next

ball_respects_bsublist

RESPONDER0

prev top next

NSL-responder0
NSL-responder0_wf

RESPONDER1

prev top next

CR-responder1
CR-responder1_wf
NSL-responder1
NSL-responder1_wf

RESPONDER2

prev top next

CR-responder2
CR-responder2_wf
NSL-responder2
NSL-responder2_wf

RESPONDER3

prev top next

CR-responder3
CR-responder3_wf
NSL-responder3
NSL-responder3_wf

RESPONDER4

prev top next

CR-responder4
CR-responder4_wf

RESPONDER5

prev top next

CR-responder5
CR-responder5_wf

RESPONDER6

prev top next

CR-responder6
CR-responder6_wf

RESTART

prev top next

restart-function

RESTRICT2

prev top next

es-is-interface-restrict2

RESTRICTION

prev top next

bijection_restriction
cc-adjoin-cube-restriction
csm-ap-restriction
cu-cube-restriction
cu-cube-restriction-comp
cu-cube-restriction-id
cu-cube-restriction_wf
cube-set-restriction
cube-set-restriction-comp
cube-set-restriction-face-map
cube-set-restriction-id
cube-set-restriction-when-id
cube-set-restriction_wf
rel-restriction
rel-restriction-implies
rel-restriction_wf
rel_or-restriction
rel_plus-of-restriction
rel_plus-restriction-equiv
restriction-of-transitive
restriction-to-field

RETRACE

prev top next

retrace
retrace_wf

RETRACER

prev top next

retracer
retracer_wf

RETRACT

prev top next

retract
retract-compose
retract-compose_wf
retract_wf

RETRACTIBLE

prev top next

nat-retractible
retractible
retractible_wf

RETRACTION

prev top next

es-causle-interface-retraction
es-causle-retraction
es-causle-retraction-squash
int-int-retraction-reals
retraction
retraction-fixedpoint
retraction-fun-path
retraction-fun-path-before
retraction-fun-path-squash
retraction_wf
sys-antecedent-retraction

RETRY

prev top next

new_23_sig-retry
new_23_sig_retry'base
new_23_sig_retry'base-program
new_23_sig_retry'base-program_wf
new_23_sig_retry'base_wf
new_23_sig_retry'send
new_23_sig_retry'send_wf
new_23_sig_retry_property

RETURN

prev top next

A-return
A-return'
A-return'_wf
A-return_wf
M-return
M-return_wf
bind-return-left
bind-return-right
hdf-return
hdf-return-transformation1
hdf-return-transformation2
hdf-return_wf
is-return-class
return-class
return-class-val
return-class_wf
return-loc-bag-class
return-loc-bag-class-classrel
return-loc-bag-class-program
return-loc-bag-class-program-wf-hdf
return-loc-bag-class-program_wf
return-loc-bag-class_wf
return-loc-class
return-loc-class_wf

REV

prev top next

and_functionality_wrt_rev_uimplies
bl-rev-exists
bl-rev-exists-sq
bl-rev-exists_wf
comb_for_rev_implies_wf
es-pplus_functionality_wrt_rev_implies
es-pstar-q_functionality_wrt_rev_implies
groupoid-cube-lemma-rev
groupoid-cube-lemma-rev
ifthenelse_functionality_wrt_rev_implies
ifthenelse_functionality_wrt_rev_implies2
ifthenelse_functionality_wrt_rev_implies3
length-rev-append
lifting-gen-list-rev
lifting-gen-list-rev_wf
lifting-gen-rev
lifting-gen-rev_wf
lifting-loc-gen-rev
lifting-loc-gen-rev_wf
list-if-has-value-rev-append
list_decomp_rev
list_decomp_rev_wf
map-rev-append-top
predicate_rev_implies
predicate_rev_implies_weakening
predicate_rev_implies_wf
rel_rev_implies
rel_rev_implies_weakening
rel_rev_implies_wf
rev-append
rev-append-append
rev-append-axiom
rev-append-pair
rev-append-property
rev-append-property-top
rev-append-property-top-sqle
rev-append-rev-append
rev-append_wf
rev-zip
rev-zip_wf
rev_app_cons_lemma
rev_app_nil_lemma
rev_bimplies
rev_bimplies_wf
rev_implies
rev_implies_weakening_rev_uimplies
rev_implies_wf
rev_mdivides
rev_mdivides_wf
rev_perm
rev_perm_wf
rev_permf
rev_permf_order_2
rev_permf_wf
rev_subtype_rel
rev_subtype_rel_weakening
rev_subtype_rel_wf
rev_uimplies
rev_uimplies_wf
select-rev-append
temp-lifting-gen-list-rev_wf
uncurry-rev
uncurry-rev_wf

REVERSE

prev top next

adjacent-reverse
before-reverse
filter-reverse
fseg-iseg-reverse
hd-reverse
last-reverse
length-reverse
list_decomp_reverse
list_ind_reverse
list_ind_reverse_unfold
list_ind_reverse_unfold1
list_ind_reverse_wf
list_ind_reverse_wf_dependent
map-reverse
map-reverse-top
mapfilter-reverse
member-reverse
no_repeats_reverse
permutation-reverse
reverse
reverse-append
reverse-bag
reverse-cons
reverse-reverse
reverse_append
reverse_append_sq
reverse_nil_lemma
reverse_select
reverse_select_wf
reverse_singleton
reverse_wf
select-reverse
sorted-by-reverse
sublist-reverse

REVERSES

prev top next

rminus-reverses-rleq
rminus-reverses-rless
rmul_reverses_rleq
rmul_reverses_rleq_iff
rmul_reverses_rless
rmul_reverses_rless_iff

REWRITE

prev top next

Q-R-pre-preserving-rewrite-test
rsum-rewrite-test
test-rewrite-dcdr

REXP

prev top next

rexp
rexp_wf

RFUN

prev top next

continuous_functionality_wrt_rfun-eq
rfun
rfun-eq
rfun-eq_inversion
rfun-eq_transitivity
rfun-eq_weakening
rfun-eq_wf
rfun_subtype
rfun_wf

RGE

prev top next

rge
rge_wf

RGT

prev top next

rgt
rgt_wf

RICE

prev top next

Rice-theorem-for-Type_1
Rice-theorem-for-Type_2
Rice-theorem-for-Type_3

RICINT

prev top next

member_ricint_lemma
ricint
ricint_wf

RIEMANN

prev top next

Riemann-sum
Riemann-sum-alt
Riemann-sum-alt-req
Riemann-sum-alt_wf
Riemann-sum-constant
Riemann-sum-refinement
Riemann-sum-rleq
Riemann-sum-rsub
Riemann-sum_wf
Riemann-sums-cauchy
Riemann-sums-converge
Riemann-sums-converge-ext
Riemann-sums-near
alt-Riemann-sums-cauchy
alt-Riemann-sums-converge
alt-Riemann-sums-converge-ext
rabs-Riemann-sum

RIGHT

prev top next

append-cancellation-right
atom-implies-ispair-right
bag-bind-empty-right
bag-combine-append-right
bag-combine-empty-right
bag-combine-eq-right
bag-combine-single-right
bag-combine-single-right-as-map
bag-combine-unit-right
bag-summation-linear-right
bag-summation-linear1-right
bind-return-right
bind-zero-right
bm_T-right
bm_T-right_wf
btr_Node-right
btr_Node-right_wf
callbyvalueall-reduce-repeat-right-branch
classfun-res-disjoint-union-comb-right
classfun-res-parallel-class-right
combine-combine-list-right
equipollent-identity-right
equipollent_functionality_wrt_ext-eq-right
es-interface-or-right
es-interface-or-right-property
es-interface-or-right_wf
es-interface-right
es-interface-right-as-image
es-interface-right_wf
es-interface-union-right
eu-add-length-cancel-right
eu-between-eq-trivial-right
eu-congruent-right-comm
fpf-empty-compatible-right
fpf-join-compatible-right
fpf-sub-compatible-right
fpf-sub-join-right
function_functionality_wrt_equipollent_right
groupoid-right-cancellation
groupoid-right-cancellation
grp_eq_shift_right
grp_leq_shift_right
grp_lt_shift_right
hdf-parallel-halt-right
hdf-until-halt-right
ifthenelse-false-right
imax-right
is-interface-right
l_subset_right_cons_trivial
l_tree_node-right_subtree
l_tree_node-right_subtree_wf
lower-right-endpoint
lower-right-endpoint-rless
lower-right-endpoint_wf
mFOconnect-right
mFOconnect-right_wf
member-per-or-right
member-per-union-right
member-tagged+-right
mul-distributes-right
name-comp-id-right
normalize-decide-right
oal_merge_right_nil_lemma
oal_neg_right_inv
oob-left-or-right
pand-right
pand-right_wf
parallel-class-bind-right
parallel-eclass2-right
pimp-right
pimp-right_wf
pioption-right
pioption-right_wf
pipar-right
pipar-right_wf
por-right
por-right_wf
product_functionality_wrt_equipollent_right
pv11_p1_upd_right
rel_implies_or_right
right-endpoint
right-endpoint_wf
right_endpoint_rccint_lemma
right_mul_preserves_le
sdata-right
sdata-right_wf
sdata_right_pair_lemma
strictness-add-right
strictness-atom1_eq-right
strictness-atom2_eq-right
strictness-atom_eq-right
strictness-divide-right
strictness-int_eq-right
strictness-less-right
strictness-multiply-right
strictness-remainder-right
strictness-subtract-right
sub-bag-cancel-right
subtype_rel_b-union-right
subtype_rel_union_right
tree_node-right
tree_node-right_wf

RIGHT2

prev top next

fpf-contains-union-join-right2
fpf-sub-join-right2

RIGHTUNIT

prev top next

A-rightunit
A-rightunit'
M-rightunit

RIIINT

prev top next

member_riiint_lemma
riiint
riiint_wf

RING

prev top next

bag-summation-ring-linear1
gen-divisors-sum-int-ring
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_ring
int_ring_wf
prime_ideals_in_int_ring
quot_ring
quot_ring_car
quot_ring_car_elim
quot_ring_car_elim_a
quot_ring_car_elim_b
quot_ring_car_qinc
quot_ring_car_subtype
quot_ring_car_wf
quot_ring_sig
quot_ring_wf
ring-as-list
ring-as-list_wf
ring_divs
ring_divs_wf
ring_hom
ring_hom_wf
ring_non_triv
ring_non_triv_wf
ring_p
ring_p_wf
ring_quot_hom
ring_triv

RINV

prev top next

continuous-rinv
derivative-rinv
rabs-rinv
rinv
rinv-functionality-lemma
rinv-limit
rinv-negative
rinv-neq-zero
rinv-of-rinv
rinv-of-rmul
rinv-positive
rinv-rminus
rinv_functionality
rinv_functionality2
rinv_preserves_rless
rinv_preserves_rneq
rinv_wf
rinv_wf2
rmul-inverse-is-rinv
rmul-rinv

RINV1

prev top next

rmul-rinv1

RINV2

prev top next

rmul-rinv2

RINVERSE

prev top next

rinverse-nonzero

RIOINT

prev top next

member_rioint_lemma
rioint
rioint_wf

RLEQ2

prev top next

rleq-iff-rleq2
rleq2
rleq2-iff-rnonneg2
rleq2_functionality
rleq2_wf
rmul_functionality_wrt_rleq2
rmul_preserves_rleq2
rsum_functionality_wrt_rleq2

RLEQ3

prev top next

rsum_functionality_wrt_rleq3

RLESS

prev top next

cantor-interval-rless
decidable__rless-int-fractions
lower-right-endpoint-rless
not-rless
radd-preserves-rless
raise-left-endpoint-rless
raise-lower-endpoints-rless
rinv_preserves_rless
rleq-iff-not-rless
rleq_weakening_rless
rless
rless-case
rless-cases
rless-cases-proof
rless-cases1
rless-content
rless-iff
rless-iff-large-diff
rless-iff-rleq
rless-iff-rpositive
rless-iff2
rless-iff2-ext
rless-iff4
rless-iff8
rless-implies
rless-implies-rleq
rless-int
rless-int-fractions
rless-int-fractions2
rless-property
rless-witness
rless-witness-property
rless-witness_wf
rless_functionality
rless_functionality_wrt_implies
rless_irreflexivity
rless_transitivity
rless_transitivity1
rless_transitivity2
rless_wf
rminus-reverses-rless
rmul_functionality_wrt_rless
rmul_preserves_rless
rmul_reverses_rless
rmul_reverses_rless_iff
rnexp-rless
rnexp-rless-odd
rpositive-rless
rsub_functionality_wrt_rless
sq_stable__rless

RLESS1

prev top next

radd_functionality_wrt_rless1

RLESS2

prev top next

radd_functionality_wrt_rless2
rmul_functionality_wrt_rless2
rnexp-rless2

RLESSW

prev top next

rlessw
rlessw_wf

RMAX

prev top next

rabs-as-rmax
rabs-difference-rmax
radd-rmax
rleq-rmax
rmax
rmax-assoc
rmax-com
rmax-i-member
rmax-idempotent
rmax-int
rmax-limit
rmax-minus-rmin
rmax-nonneg
rmax-positive
rmax-req
rmax-req2
rmax-rnexp
rmax_functionality
rmax_functionality_wrt_bdd-diff
rmax_functionality_wrt_rleq
rmax_lb
rmax_strict_lb
rmax_strict_ub
rmax_ub
rmax_wf
rmin-req-rminus-rmax
rmin-rleq-rmax
rminus-rmax
rmul-rmax
rpositive-rmax

RMAXIMUM

prev top next

rmaximum
rmaximum-constant
rmaximum-lub
rmaximum-select
rmaximum-split
rmaximum_functionality
rmaximum_functionality_wrt_rleq
rmaximum_ub
rmaximum_wf

RMIN

prev top next

radd-rmin
rmax-minus-rmin
rmin
rmin-assoc
rmin-com
rmin-i-member
rmin-idempotent
rmin-idempotent-eq
rmin-int
rmin-max-cases
rmin-nonneg
rmin-positive
rmin-req
rmin-req-rminus-rmax
rmin-req2
rmin-rleq
rmin-rleq-rmax
rmin-rnexp
rmin_functionality
rmin_functionality_wrt_bdd-diff
rmin_lb
rmin_strict_lb
rmin_strict_ub
rmin_ub
rmin_wf
rminus-rmin
rmul-rmin

RMINUS

prev top next

rabs-rminus
radd-rminus
radd-rminus-assoc
radd-rminus-both
rinv-rminus
rmin-req-rminus-rmax
rminus
rminus-as-rmul
rminus-int
rminus-limit
rminus-nonneg
rminus-radd
rminus-rdiv
rminus-rdiv2
rminus-reverses-rleq
rminus-reverses-rless
rminus-rmax
rminus-rmin
rminus-rminus
rminus-rminus-eq
rminus-rneq-zero
rminus-zero
rminus_functionality
rminus_functionality_wrt_bdd-diff
rminus_functionality_wrt_rleq
rminus_wf
rmul_over_rminus
rnexp-rminus

RMUL

prev top next

fun-converges-rmul
int-rdiv-int-rmul
int-rmul
int-rmul-one
int-rmul-req
int-rmul_wf
rabs-rmul
rabs-rmul-rleq
rabs-rmul-rleq-rabs
rinv-of-rmul
rminus-as-rmul
rmul
rmul-ac
rmul-assoc
rmul-bdd-diff-reg-seq-mul
rmul-distrib
rmul-distrib1
rmul-distrib2
rmul-ident-div
rmul-identity1
rmul-int
rmul-int-fractions
rmul-int-rdiv
rmul-int-rdiv2
rmul-inverse-is-rinv
rmul-is-negative
rmul-is-negative1
rmul-is-positive
rmul-limit
rmul-minus
rmul-neq-zero
rmul-nonneg
rmul-nonzero
rmul-nonzero-on
rmul-one
rmul-one-both
rmul-rdiv
rmul-rdiv-cancel
rmul-rdiv-cancel2
rmul-rdiv-cancel3
rmul-rdiv-cancel4
rmul-rdiv-cancel5
rmul-rdiv-cancel6
rmul-rdiv-cancel7
rmul-rdiv-cancel8
rmul-rdiv-cancel9
rmul-rdiv-one
rmul-rdiv2
rmul-rinv
rmul-rinv1
rmul-rinv2
rmul-rmax
rmul-rmin
rmul-rsub-distrib
rmul-zero
rmul-zero-both
rmul-zero-div
rmul_assoc
rmul_comm
rmul_functionality
rmul_functionality_wrt_rleq
rmul_functionality_wrt_rleq2
rmul_functionality_wrt_rless
rmul_functionality_wrt_rless2
rmul_over_rminus
rmul_preserves_req
rmul_preserves_rleq
rmul_preserves_rleq2
rmul_preserves_rless
rmul_preserves_rneq
rmul_reverses_rleq
rmul_reverses_rleq_iff
rmul_reverses_rless
rmul_reverses_rless_iff
rmul_wf
rnexp-rmul
rnonneg-rmul
rpositive-rmul
series-converges-rmul
series-converges-rmul-ext

RNDV1

prev top next

pDVselex-rndv1
pDVselex-rndv1_wf

RNDV2

prev top next

pDVrequest-rndv2
pDVrequest-rndv2_wf

RNEQ

prev top next

absval-implies-rneq
continuous-rneq
not-rneq
req-iff-not-rneq
rinv_preserves_rneq
rminus-rneq-zero
rmul_preserves_rneq
rneq
rneq-iff-rabs
rneq-int
rneq-zero
rneq_functionality
rneq_irreflexivity
rneq_wf
small-reciprocal-rneq-zero

RNEXP

prev top next

continuous-rnexp
derivative-rnexp
rabs-rnexp
rmax-rnexp
rmin-rnexp
rnexp
rnexp-add
rnexp-converges
rnexp-converges-ext
rnexp-convex
rnexp-convex2
rnexp-convex3
rnexp-even-nonneg
rnexp-int
rnexp-is-positive
rnexp-minus-one
rnexp-mul
rnexp-nonneg
rnexp-one
rnexp-positive
rnexp-rdiv
rnexp-req
rnexp-req-iff
rnexp-req-iff-even
rnexp-req-iff-odd
rnexp-rleq
rnexp-rleq-iff
rnexp-rless
rnexp-rless-odd
rnexp-rless2
rnexp-rminus
rnexp-rmul
rnexp_functionality
rnexp_step
rnexp_unroll
rnexp_wf
rnexp_zero_lemma
rsqrt-rnexp-2

RNEXP1

prev top next

rnexp1

RNEXP2

prev top next

continuous-rnexp2
rnexp2

RNG

prev top next

add_grp_of_rng
add_grp_of_rng_wf
add_grp_of_rng_wf_a
add_grp_of_rng_wf_b
alg_act_is_rng_chom
alg_from_rng
alg_from_rng_wf
all_rng_quot_elim
all_rng_quot_elim_a
assert_of_rng_eq
comb_for_rng_mssum_wf
comb_for_rng_nat_op_wf
comb_for_rng_nexp_wf
comb_for_rng_sum_wf
comb_for_rng_when_wf
crng_subtype_rng
decidable__rng_eq
drng_subtype_rng
fps-rng
fps-rng_wf
fps-scalar-mul-rng-add
module_over_triv_rng
mul_mon_of_rng
mul_mon_of_rng_wf
mul_mon_of_rng_wf_a
mul_mon_of_rng_wf_b
mul_mon_of_rng_wf_c
rng
rng_abmon
rng_abmon_wf
rng_all_properties
rng_before_all_imp_before
rng_before_imp_before_all
rng_car
rng_car_qinc
rng_car_wf
rng_chom_p
rng_chom_p_wf
rng_div
rng_div_wf
rng_eq
rng_eq_wf
rng_from_grp
rng_from_grp_wf
rng_fset_for_when_eq
rng_hom_minus
rng_hom_p
rng_hom_p_wf
rng_hom_zero
rng_le
rng_le_wf
rng_lookup_before_start
rng_lsum
rng_lsum_wf
rng_lsum_when_swap
rng_minus
rng_minus_minus
rng_minus_over_plus
rng_minus_wf
rng_minus_zero
rng_mssum
rng_mssum_dom_shift
rng_mssum_functionality_wrt_bsubmset
rng_mssum_functionality_wrt_equal
rng_mssum_of_plus
rng_mssum_swap
rng_mssum_wf
rng_mssum_when_swap
rng_nat_op
rng_nat_op-int
rng_nat_op_add
rng_nat_op_one
rng_nat_op_wf
rng_nexp
rng_nexp-int
rng_nexp_unroll
rng_nexp_wf
rng_nexp_zero
rng_of_alg
rng_of_alg_wf
rng_of_alg_wf2
rng_one
rng_one_wf
rng_p
rng_p_wf
rng_plus
rng_plus_ac_1
rng_plus_assoc
rng_plus_cancel_l
rng_plus_comm
rng_plus_comm2
rng_plus_inv
rng_plus_inv_assoc
rng_plus_wf
rng_plus_zero
rng_prod
rng_prod_wf
rng_properties
rng_sig
rng_sig_inc
rng_sig_wf
rng_subtype_rng_sig
rng_sum
rng_sum-int
rng_sum_plus
rng_sum_shift
rng_sum_split
rng_sum_unroll_base
rng_sum_unroll_hi
rng_sum_unroll_lo
rng_sum_unroll_unit
rng_sum_wf
rng_times
rng_times_assoc
rng_times_lsum_l
rng_times_lsum_r
rng_times_mssum_l
rng_times_mssum_r
rng_times_nat_op
rng_times_nat_op_r
rng_times_one
rng_times_over_minus
rng_times_over_plus
rng_times_sum_l
rng_times_sum_r
rng_times_wf
rng_times_when_l
rng_times_when_r
rng_times_zero
rng_to_alg
rng_to_alg_wf
rng_wf
rng_when
rng_when_of_zero
rng_when_swap
rng_when_thru_plus
rng_when_wf
rng_when_when
rng_zero
rng_zero_wf
subtype_rel_rng_sig

RNONNEG

prev top next

rnonneg
rnonneg-iff
rnonneg-int
rnonneg-radd
rnonneg-rmul
rnonneg_functionality
rnonneg_wf
rpositive-implies-rnonneg
sq_stable__rnonneg

RNONNEG2

prev top next

rleq2-iff-rnonneg2
rnonneg2
rnonneg2_functionality
rnonneg2_wf

RNONZERO

prev top next

rnonzero
rnonzero-iff
rnonzero-lemma1
rnonzero_functionality
rnonzero_wf

ROBIN

prev top next

round-robin
round-robin-equal
round-robin-list-index
round-robin-member
round-robin-onto
round-robin_wf

ROCINT

prev top next

member_rocint_lemma
rocint
rocint_wf

ROIINT

prev top next

member_roiint_lemma
roiint
roiint_wf

ROLL

prev top next

mk_applies_roll

ROLLES

prev top next

Rolles-theorem

ROOINT

prev top next

member_rooint_lemma
rooint
rooint_wf

ROOT

prev top next

int-sq-root
integer-nth-root
integer-nth-root-ext
near-root
near-root-rational
near-root-rational-ext
near-root_wf

ROOT2

prev top next

integer-nth-root2

ROTATE

prev top next

compose-rotate-by
flip-conjugate-rotate
iterate-rotate
iterate-rotate-by
iterate-rotate-rotate-by
iterated-rotate
permutation-rotate
permutation-rotate-cons
rotate
rotate-by
rotate-by-cyclic-map
rotate-by-id
rotate-by-injection
rotate-by-is-id
rotate-by-rotate-by
rotate-by-transitive
rotate-by-trivial
rotate-by-trivial-test
rotate-by-zero
rotate-by_wf
rotate-injection
rotate-inverse
rotate-inverse1
rotate-order
rotate_wf

ROUND

prev top next

new_23_sig_Round
new_23_sig_Round-program
new_23_sig_Round-program_wf
new_23_sig_Round_wf
new_23_sig_round_info_classrel2
new_23_sig_update_round
new_23_sig_update_round_wf
new_23_sig_when_new_round
new_23_sig_when_new_round_wf
proportional-round
proportional-round_wf
round-robin
round-robin-equal
round-robin-list-index
round-robin-member
round-robin-onto
round-robin_wf

ROUNDED

prev top next

rounded-numerator
rounded-numerator_wf

ROUNDINFO

prev top next

new_23_sig_RoundInfo
new_23_sig_RoundInfo-program
new_23_sig_RoundInfo-program_wf
new_23_sig_RoundInfo-single-val
new_23_sig_RoundInfo_wf

ROUNDOUT

prev top next

new_23_sig_roundout
new_23_sig_roundout_wf

ROUNDS

prev top next

new_23_sig_Rounds
new_23_sig_Rounds-program
new_23_sig_Rounds-program_wf
new_23_sig_Rounds_wf
new_23_sig_rounds_inc
new_23_sig_rounds_mem
new_23_sig_rounds_mem_fun
new_23_sig_rounds_pos
new_23_sig_rounds_pos_fun
new_23_sig_rounds_strict_inc

RPOLY

prev top next

rpoly-deriv
rpoly-deriv_wf
rpoly-nth-deriv
rpoly-nth-deriv-linear
rpoly-nth-deriv_functionality
rpoly-nth-deriv_wf

RPOLYNOMIAL

prev top next

continuous-rpolynomial
derivative-rpolynomial
intermediate-value-theorem-rpolynomial
rpolynomial
rpolynomial-composition1
rpolynomial-locally-non-zero
rpolynomial-locally-non-zero-1
rpolynomial_unroll
rpolynomial_wf

RPOLYNOMIAL1

prev top next

IVT-rpolynomial1

RPOLYNOMIAL2

prev top next

IVT-rpolynomial2

RPOSITIVE

prev top next

not-rpositive
rless-iff-rpositive
rpositive
rpositive-iff
rpositive-implies-rnonneg
rpositive-int
rpositive-radd
rpositive-radd2
rpositive-rless
rpositive-rmax
rpositive-rmul
rpositive_functionality
rpositive_wf

RPOSITIVE2

prev top next

rpositive2
rpositive2_functionality
rpositive2_wf

RPOWER

prev top next

inverse-rpower
rpower-greater-one
rpower-nonzero
rpower-one
rpower-two

RPOWERS

prev top next

rpowers-converge
rpowers-converge-ext

RPRIME

prev top next

rprime
rprime_wf

RRANGE

prev top next

rrange
rrange_wf
rset-member-rrange

RROOT

prev top next

constructing rroot
extracted-rroot
extracted-rroot_wf
rroot
rroot-abs
rroot-abs-non-neg
rroot-abs-property
rroot-abs_wf
rroot-exists
rroot-exists-ext
rroot-exists-part1
rroot-exists-part2
rroot-exists1
rroot-exists1-ext
rroot-odd
rroot-odd-2-regular
rroot-odd_wf
rroot-regularity-lemma
rroot_functionality
rroot_wf

RSET

prev top next

closed-rset
closed-rset_wf
member_mk_rset_lemma
member_rset_neg_lemma
mk-rset
mk-rset_wf
rset
rset-member
rset-member-rrange
rset-member_functionality
rset-member_wf
rset-neg
rset-neg_wf
rset_wf

RSETEQ

prev top next

rseteq
rseteq_weakening
rseteq_wf

RSQRT

prev top next

fast-rsqrt
rsqrt
rsqrt-irrational
rsqrt-rnexp-2
rsqrt_2-irrational
rsqrt_functionality
rsqrt_nonneg
rsqrt_squared
rsqrt_wf

RSUB

prev top next

Riemann-sum-rsub
rmul-rsub-distrib
rsub
rsub-int
rsub-limit
rsub-rdiv
rsub_functionality
rsub_functionality_wrt_rleq
rsub_functionality_wrt_rless
rsub_wf
rsum_linearity-rsub

RSUM

prev top next

derivative-rsum
rabs-rsum
rsum
rsum'
rsum'-eq-rsum
rsum'-rsum
rsum'_wf
rsum-constant
rsum-constant2
rsum-difference
rsum-difference2
rsum-empty
rsum-one
rsum-rewrite-test
rsum-shift
rsum-single
rsum-split
rsum-split-first
rsum-split-last
rsum-split-shift
rsum-telescopes
rsum-triangle-inequality1
rsum-triangle-inequality2
rsum-zero
rsum_functionality
rsum_functionality2
rsum_functionality_wrt_rleq
rsum_functionality_wrt_rleq2
rsum_functionality_wrt_rleq3
rsum_linearity-rsub
rsum_linearity1
rsum_linearity2
rsum_linearity3
rsum_nonneg
rsum_product
rsum_single
rsum_unroll
rsum_wf

RULE

prev top next

chain-rule
chain-rule_1
divisibility-by-2-rule
divisibility-by-3-rule
divisibility-by-5-rule
divisibility-by-9-rule
es-propagation-rule
es-propagation-rule-iff
es-propagation-rule-iff_wf
es-propagation-rule_wf
simple-chain-rule

RULES

prev top next

Rules of MLTT type formers
Rules of MLTT without type formers

RUN

prev top next

adjacent-run-states
decidable__run-lt
decidable__run-pred
finite-run-lt
finite-run-pred
hdf-ap-run
hdf-halted-run
hdf-out-run
hdf-run
hdf-run_wf
hdf_halted_run_red_lemma
is-run-event
is-run-event_wf
member-prior-run-events
member-run-event-interval
more-things-that-can-be-run
pi-run-example
pi-run-example_wf
prior-run-events
prior-run-events_wf
run-cause
run-cause_wf
run-command
run-command-node
run-command-node_wf
run-command_wf
run-eo
run-eo_wf
run-event-cases
run-event-history
run-event-history_wf
run-event-in-transit
run-event-in-transit_wf
run-event-interval
run-event-interval-cases
run-event-interval_wf
run-event-loc
run-event-loc_wf
run-event-local-pred
run-event-local-pred_wf
run-event-msg
run-event-msg_wf
run-event-state
run-event-state-next
run-event-state-next2
run-event-state-when
run-event-state-when_wf
run-event-state_wf
run-event-step
run-event-step-positive
run-event-step_wf
run-info
run-info_wf
run-initialization
run-initialization-property
run-initialization_wf
run-intransit
run-intransit_wf
run-local-pred
run-local-pred_wf
run-lt
run-lt-step-less
run-lt-transitive
run-lt_wf
run-msg-commands
run-msg-commands_wf
run-pred
run-pred-step-less
run-pred_wf
run-prior-state
run-prior-state-property
run-prior-state_wf
run-system
run-system_wf
run-to-n
run-to-n_wf
run_local_pred
run_local_pred_loc
run_local_pred_maximal
run_local_pred_time
run_local_pred_time_less
run_local_pred_wf
things-that-can-be-run
total-run-lt
well-founded-run-lt
well-founded-run-pred

RUNEO

prev top next

runEO
runEO_wf

RUNEVENTS

prev top next

decidable__equal_runEvents
deq-runEvents-witness
deq-runEvents-witness_wf
runEvents
runEvents_wf

RUNINFO

prev top next

norm-runinfo
norm-runinfo_wf

RUNNING

prev top next

hdf-running
hdf-running_wf

RUSSELL

prev top next

Russell
Russell-paradox
Russell-property
Russell-theorem
Russell-theorem-ext
Russell-theorem-take2
Russell_wf

RV

prev top next

expectation-rv-add
expectation-rv-add-cubed
expectation-rv-add-fourth
expectation-rv-add-squared
expectation-rv-const
expectation-rv-disjoint
expectation-rv-sample
expectation-rv-scale
rv-add
rv-add_wf
rv-compose
rv-compose_wf
rv-const
rv-const_wf
rv-disjoint
rv-disjoint-compose
rv-disjoint-const
rv-disjoint-monotone-in-first
rv-disjoint-rv-add
rv-disjoint-rv-add2
rv-disjoint-rv-mul
rv-disjoint-rv-mul2
rv-disjoint-rv-partial-sum
rv-disjoint-rv-scale
rv-disjoint-rv-shift
rv-disjoint-shift
rv-disjoint-symmetry
rv-disjoint_wf
rv-identically-distributed
rv-identically-distributed_wf
rv-iid
rv-iid-add
rv-iid-add-const
rv-iid_wf
rv-le
rv-le_wf
rv-le_witness
rv-mul
rv-mul_wf
rv-partial-sum
rv-partial-sum-monotone
rv-partial-sum-unroll
rv-partial-sum_wf
rv-qle
rv-qle_wf
rv-sample
rv-sample_wf
rv-scale
rv-scale_wf
rv-shift
rv-shift-linear
rv-shift_wf
rv-unbounded
rv-unbounded_wf

RVAL

prev top next

oobright-rval
oobright-rval_wf

RW

prev top

add_mono_wrt_eq_rw
add_mono_wrt_le_rw
add_mono_wrt_lt_rw
assert_of_eq_int_rw
bmsexists_char_a_rw
bmsexists_char_rw
free-from-atom-Id-rw
ite_rw_false
ite_rw_test
ite_rw_true
le_to_lt_rw
lt_to_le_rw
mk_perm_eta_rw
pair_eta_rw