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

---

S

top next

Beeson's Constructive Tarski Geometry
Dickson's lemma
Peirce's-law-iff-xmiddle
member-s-insert
no-uniform-Peirce's-law
s-cons
s-cons_wf
s-filter
s-filter_wf
s-hd
s-hd_wf
s-insert
s-insert-no-repeats
s-insert-sorted
s-insert_wf
s-nth
s-nth_wf
s-tl
s-tl_wf
s_hd_cons_lemma
s_part
s_part_char
s_part_functionality_wrt_breqv
s_part_wf
s_tl_cons_lemma
ses-S
ses-S_wf

---

SAFE

prev top next

no-weakly-safe-extensions
safe-assert-deq
weakly-safe-extension
weakly-safe-seq
weakly-safe-seq_wf

---

SAFETY

prev top next

all_safety
cond_safety_and
consensus-safety
filter_safety
filter_strong_safety
no_repeats_safety
safety
safety_and
safety_induced
safety_nil
safety_wf
strong_safety
strong_safety_safety
strong_safety_wf
three-cs-int-safety
three-cs-safety

---

SAFETY1

prev top next

consensus-safety1
three-cs-safety1

---

SAFETY2

prev top next

three-cs-safety2

---

SAME

prev top next

adjacent-to-same
adjacent-to-same-sublist
adjacent-to-same-sublist2
bag-filter-same
cubical-path-same-name
decidable__es-causl-same-loc
decidable__same-thread
es-prior-interface-same
eu-between-eq-same
eu-between-eq-same-side
eu-between-eq-same-side2
eu-between-same
extend-face-map-same
fun-connected-to-same
iseg_same_length
ite-same
l-union-same
l_subset_cons_same
lookups_same
lookups_same_a
nerve_box_edge_same
nerve_box_label_same
not-same-parity-implies
not-same-parity-implies-even-odd
omral_lookups_same_a
path-eq-same-name
poset_functor_extend_same
psub-same
pv11_p1_same_proposal
pv11_p1_same_proposal_wf
pv11_p1_same_pvalue
pv11_p1_same_pvalue_wf
rename-one-same
same-action
same-action_wf
same-face-edge-arrows-commute
same-face-edge-arrows-commute0
same-face-edge-arrows-commute1
same-face-edge-arrows-commute2
same-face-edge-arrows-commute3
same-face-edge-arrows-commute4
same-face-square-commutes
same-face-square-commutes2
same-final-iterate-one-one
same-loc-total
same-loc-total2
same-parity
same-parity-implies
same-parity-implies-even-odd
same-parity_wf
same-thread
same-thread-do-apply
same-thread_inversion
same-thread_transitivity
same-thread_weakening
same-thread_wf
same_order
same_order_wf
sublist-same-last

---

SAME1

prev top next

nerve_box_edge_same1

---

SAME2

prev top next

adjacent-to-same2
eu-between-eq-same2
eu-between-same2

---

SAMPLE

prev top next

expectation-rv-sample
rv-sample
rv-sample_wf
sample reals lemmas

---

SASYM

prev top next

irrefl_trans_imp_sasym

---

SAT

prev top next

div_fun_sat_div_nrel
gcd_sat_gcd_p
gcd_sat_pred
rem_fun_sat_rem_nrel
sq_stable__uni_sat
uni_sat
uni_sat_imp_in_uni_set
uni_sat_upto
uni_sat_upto_wf
uni_sat_wf

---

SB

prev top next

sb-equipollent

---

SBCODE

prev top next

sbcode
sbcode-decode
sbcode-mul
sbcode_aux
sbcode_wf

---

SBDECODE

prev top next

sbdecode
sbdecode-code
sbdecode_wf
sbdecode_wf_gcd

---

SBHOMOUT

prev top next

sbhomout
sbhomout-correct
sbhomout_wf

---

SCALAR

prev top next

fps-compose-scalar-mul
fps-scalar-mul
fps-scalar-mul-one
fps-scalar-mul-property
fps-scalar-mul-rng-add
fps-scalar-mul-slice
fps-scalar-mul-zero
fps-scalar-mul_wf
fps-set-to-one-scalar-mul
sum_scalar_mult

---

SCALE

prev top next

expectation-rv-scale
lookup_omral_scale_a
lookup_omral_scale_b
lookup_omral_scale_c
lookup_omral_scale_d
omral_dom_scale
omral_scale
omral_scale_dom_bound
omral_scale_dom_pred
omral_scale_non_zero_vals
omral_scale_sd_ordered
omral_scale_wf
omral_scale_wf2
rv-disjoint-rv-scale
rv-scale
rv-scale_wf

---

SCHWARZ

prev top next

Cauchy-Schwarz

---

SCHWARZ1

prev top next

Cauchy-Schwarz1

---

SCHWARZ2

prev top next

Cauchy-Schwarz2

---

SCHWARZ3

prev top next

Cauchy-Schwarz3

---

SCOMB

prev top next

scomb
scomb_wf

---

SCOMP

prev top next

C_LVALUE-proper-Scomp
LV_Scomp
LV_Scomp-comp
LV_Scomp-comp_wf
LV_Scomp-lval
LV_Scomp-lval_wf
LV_Scomp?
LV_Scomp?_wf
LV_Scomp_wf

---

SCOMPED

prev top next

C_LVALUE-proper-Scomped

---

SCOUT

prev top next

pv11_p1_Scout
pv11_p1_Scout-program
pv11_p1_Scout-program_wf
pv11_p1_Scout_wf
pv11_p1_init_scout
pv11_p1_init_scout_wf
pv11_p1_inv_scout
pv11_p1_ord_scout
pv11_p1_scout_from_acc
pv11_p1_scout_fun_from_acc
pv11_p1_scout_fun_from_acc2
pv11_p1_scout_output
pv11_p1_scout_output_wf
pv11_p1_scout_state_from_p1bs
pv11_p1_scout_state_fun_eq
pv11_p1_scout_state_subset_pvals

---

SCOUTNOTIFY

prev top next

pv11_p1_ScoutNotify
pv11_p1_ScoutNotify-program
pv11_p1_ScoutNotify-program_wf
pv11_p1_ScoutNotify_wf

---

SCOUTOUTPUT

prev top next

pv11_p1_ScoutOutput
pv11_p1_ScoutOutput-program
pv11_p1_ScoutOutput-program_wf
pv11_p1_ScoutOutput_wf

---

SCOUTSTATE

prev top next

pv11_p1_ScoutState
pv11_p1_ScoutState-classrel
pv11_p1_ScoutState-functional
pv11_p1_ScoutState-program
pv11_p1_ScoutState-program_wf
pv11_p1_ScoutState_wf
pv11_p1_valid-ScoutState
pv11_p1_valid-ScoutState_wf

---

SCOUTSTATEFUN

prev top next

pv11_p1_ScoutStateFun
pv11_p1_ScoutStateFun_wf

---

SD

prev top next

comb_for_sd_ordered_wf
oal_merge_sd_ordered
oal_neg_sd_ordered
omral_plus_sd_ordered
omral_scale_sd_ordered
omral_times_sd_ordered
sd_ordered
sd_ordered_char
sd_ordered_cons_lemma
sd_ordered_count
sd_ordered_nil_lemma
sd_ordered_wf

---

SDATA

prev top next

atom-sdata
atom-sdata-has-atom
atom-sdata-not-pair
atom-sdata-not-pair2
atom-sdata-one-one
atom-sdata_wf
id-sdata
id-sdata-has-atom
id-sdata-not-pair
id-sdata-not-pair2
id-sdata-one-one
id-sdata_wf
sdata
sdata-atoms
sdata-atoms_wf
sdata-free-from-atom
sdata-has-atom
sdata-left
sdata-left_wf
sdata-pair
sdata-pair-free-from-atom
sdata-pair-has-atom
sdata-pair-one-one
sdata-pair?
sdata-pair?_wf
sdata-pair_wf
sdata-right
sdata-right_wf
sdata-test
sdata_atoms_atom_lemma
sdata_atoms_id_lemma
sdata_atoms_pair_lemma
sdata_left_pair_lemma
sdata_pair_atom_lemma
sdata_pair_id_lemma
sdata_pair_rec_lemma
sdata_right_pair_lemma
sdata_sq
sdata_subtype_base
sdata_wf

---

SEARCH

prev top next

binary-search
binary-search_wf
can-apply-es-search-back
div-search-lemma
div-search-lemma-ext
es-search-back
es-search-back-cases
es-search-back_wf
integer-sqrt-bin-search
isl-es-search-back
lg-search
lg-search-minimal
lg-search-property
lg-search_wf
search
search_property
search_succ
search_wf
uniform-continuity-pi-search
uniform-continuity-pi-search-prop1
uniform-continuity-pi-search-prop2
uniform-continuity-pi-search_wf

---

SECOND

prev top next

second-countable-choice

---

SECRECY

prev top next

ses-secrecy
ses-secrecy_wf

---

SECRET

prev top next

secret-table
secret-table_wf

---

SECURES

prev top next

tree-secures
tree-secures_functionality
tree-secures_wf
trivial-tree-secures

---

SECURITY

prev top next

security-event-structure
security-event-structure_wf
security-theory
security-theory_wf

---

SEG

prev top next

cardinality-le-int_seg
comb_for_int_seg_wf
decidable-exists-int_seg-subtype
decidable__all_int_seg
decidable__equal_int_seg
decidable__exists_int_seg
equipollent-int_seg
eu-congruent-flip-seg
eu-mk-seg
eu-mk-seg_wf
eu-seg-congruent
eu-seg-congruent-equiv
eu-seg-congruent-equiv-proper
eu-seg-congruent-iff-length
eu-seg-congruent_symmetry
eu-seg-congruent_transitivity
eu-seg-congruent_weakening
eu-seg-congruent_wf
eu-seg-extend
eu-seg-extend_functionality
eu-seg-extend_wf
eu-seg-length-extend
eu-seg-length-test
eu-seg-length-test-ext
eu-seg-length-test2
eu-seg-proper
eu-seg-proper_wf
eu_seg1_mk_seg_lemma
eu_seg2_mk_seg_lemma
finite-type-int_seg
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
mul-initial-seg
mul-initial-seg-property
mul-initial-seg-property2
mul-initial-seg-step
mul-initial-seg_wf
not-all-int_seg
primrec-wf-int_seg
sq_stable__ex_int_seg_ap
sq_stable_eu-seg-congruent
subtype_rel-int_seg

---

SEG1

prev top next

eu-seg1
eu-seg1_wf
eu_seg1_mk_seg_lemma

---

SEG2

prev top next

eu-seg2
eu-seg2_wf
eu_seg2_mk_seg_lemma

---

SEGMENT

prev top next

append_segment
comb_for_segment_wf
eu-colinear-five-segment
eu-five-segment
eu-inner-five-segment
eu-inner-three-segment
eu-le-null-segment
eu-length-null-segment
eu-lt-null-segment
eu-proper-segment
eu-proper-segment_wf
eu-segment
eu-segment_wf
eu-three-segment
length_segment
segment
segment_factor
segment_wf
whole_segment

---

SEGMENT2

prev top next

eu-lt-null-segment2

---

SEGMENTS

prev top next

eu-segments-cross

---

SEL

prev top next

W_sel
W_sel_wf

---

SELECT

prev top next

W-select
W-select_wf
W_select_nil_lemma
bag-member-select
co-w-select
co-w-select-wfd
co-w-select_wf
co_w_select_nil_lemma
es-interval-select
fseg_select
iseg_select
l_before_select
list_update_select
listify_select_id
map_select
mklist_select
not-isl-priority-select
permute_list_select
priority-select
priority-select-ff
priority-select-inr
priority-select-property
priority-select-tt
priority-select_wf
rec_select_update_lemma
record-select
record-select-update
record-select_wf
record-select_wf2
reverse_select
reverse_select_wf
rmaximum-select
select
select-add-indices
select-append
select-as-hd
select-as-reduce
select-bag-rep
select-cons
select-cons-hd
select-cons-tl
select-data-stream
select-firstn
select-from-upto
select-front-as-reduce
select-indices
select-indices-aux
select-indices-aux_wf
select-indices_wf
select-is-bottom
select-last-in-nat-missing
select-last-in-nat-missing_wf
select-map
select-map-index
select-map-index_aux
select-mklist
select-nil
select-nth_tl
select-nthtl
select-nthtl0
select-remove-first
select-repn
select-rev-append
select-reverse
select-shorten-tuple
select-shuffle
select-shuffle2
select-tagged-indices
select-tagged-indices-aux
select-tagged-indices-aux_wf
select-tagged-indices_wf
select-tuple
select-tuple-tuple
select-tuple_wf
select-unshuffle
select-update-tuple
select-upto
select-zip
select_append
select_append_back
select_append_front
select_concat
select_concat_sum
select_cons_hd
select_cons_tl
select_cons_tl_sq
select_cons_tl_sq2
select_equal
select_firstn
select_fun_ap
select_fun_ap_is_last1
select_fun_ap_wf
select_fun_last
select_fun_last_partial_ap1
select_fun_last_partial_ap_gen1
select_fun_last_wf
select_l_index
select_l_interval
select_listify_id
select_member
select_nth_tl
select_reject_permr
select_tl
select_upto
select_wf
select_zip
swap_select
swapped_select
test-select-nil

---

SELECT0

prev top next

select0

---

SELECT2

prev top next

iseg_select2

---

SELECTOR

prev top next

ni-selector
ni-selector-property
ni-selector_wf
p-selector
p-selector_wf

---

SELEX

prev top next

Comm-next-selex
Comm-next-selex_wf

---

SELF

prev top next

Q-Q-glued-self-image
Q-Q-glued-to-self
Q-Q-glues-to-self
Q-Q-glues-to-self-image
div-self
eq_atom1_self
eq_atom2_self
eq_id_self
eq_knd_self
eq_lnk_self
equiv_rel_self_functionality
es-le-self
fpf-compatible-self
fpf-contains_self
fpf-union-compatible-self
glued-to-self
not-self-starting
not-self-starting_wf
rdiv-self
self_divisor_mul
strong-subtype-self
subtype_rel_self
trans_rel_func_wrt_sym_self
trans_rel_self_functionality
uequiv_rel_self_functionality
utrans_rel_self_functionality

---

SEND

prev top next

CLK_msg'send
CLK_msg'send_wf
OARcast_deliver'send
OARcast_deliver'send_wf
new_23_sig_retry'send
new_23_sig_retry'send_wf
nysiad_add2bag'send
nysiad_add2bag'send_wf
nysiad_addwaiting'send
nysiad_addwaiting'send_wf
nysiad_adeliver'send
nysiad_adeliver'send_wf
nysiad_ready'send
nysiad_ready'send_wf
pv11_p1_adopted'send
pv11_p1_adopted'send_wf
pv11_p1_decision'send
pv11_p1_decision'send_wf
pv11_p1_p1b'send
pv11_p1_p1b'send_wf
pv11_p1_p2a'send
pv11_p1_p2a'send_wf
pv11_p1_p2b'send
pv11_p1_p2b'send_wf
pv11_p1_preempted'send
pv11_p1_preempted'send_wf
send-class
send-class_wf
send-first-class
send-first-class_wf
send-on-class
send-on-class_wf
send-once-class
send-once-class_wf
send-once-classrel
send-once-loc-class
send-once-loc-class-eq-once-simple-loc-comb-0
send-once-loc-class_wf
send-once-loc-classrel
send-once-no-prior-classrel
send-rcv-match
send-rcv-match_wf
ses-send
ses-send_wf

---

SENDER

prev top next

OARcast_Sender
OARcast_Sender-program
OARcast_Sender-program_wf
OARcast_Sender_wf
OARcast_deliverer_for_sender_output
OARcast_deliverer_for_sender_output_wf
OARcast_deliverer_for_sender_seq_output
OARcast_deliverer_for_sender_seq_output_wf
OARcast_deliverer_for_sender_seq_update
OARcast_deliverer_for_sender_seq_update_wf
OARcast_deliverer_for_sender_update
OARcast_deliverer_for_sender_update_wf
OARcast_orderer_for_sender
OARcast_orderer_for_sender_outputs
OARcast_orderer_for_sender_outputs_wf
OARcast_orderer_for_sender_wf

---

SENDERSTATE

prev top next

OARcast_SenderState
OARcast_SenderState-classrel
OARcast_SenderState-functional
OARcast_SenderState-program
OARcast_SenderState-program_wf
OARcast_SenderState_wf

---

SENDERSTATEFUN

prev top next

OARcast_SenderStateFun
OARcast_SenderStateFun_wf

---

SENDS

prev top next

csm-sends
csm-sends_wf

---

SEP

prev top next

fan-implies-bar-sep

---

SEPARATE

prev top next

bag-separate
bag-separate-merge
bag-separate_wf

---

SEPARATED

prev top next

frs-increasing-separated-common-refinement
frs-separated
frs-separated_wf
separated-partitions
separated-partitions-have-common-refinement
separated-partitions_wf

---

SEPARATION

prev top next

bar-separation
bar-separation_wf
type-separation

---

SEQ

prev top next

IVT-deriv-seq-test
OARcast_deliverer_for_sender_seq_output
OARcast_deliverer_for_sender_seq_output_wf
OARcast_deliverer_for_sender_seq_update
OARcast_deliverer_for_sender_seq_update_wf
basic-seq-1-1
basic-seq-1-1_wf
basic-seq-1-2
basic-seq-1-2_wf
basic-seq-1-3
basic-seq-1-3_wf
basic-seq-1-4
basic-seq-1-4_wf
basic-seq-1-5
basic-seq-1-5_wf
bdd-diff-regular-int-seq
callbyvalueall-seq
callbyvalueall-seq-extend
callbyvalueall-seq-extend-2
callbyvalueall-seq-extend0
callbyvalueall-seq-extend0-2
callbyvalueall-seq-fun
callbyvalueall-seq-fun1
callbyvalueall-seq-fun2
callbyvalueall-seq-spread
callbyvalueall-seq-spread0
callbyvalueall-seq_wf
callbyvalueall_seq
callbyvalueall_seq-combine
callbyvalueall_seq-combine0
callbyvalueall_seq-combine2
callbyvalueall_seq-combine2-0
callbyvalueall_seq-combine3
callbyvalueall_seq-combine3-0
callbyvalueall_seq-decomp-last
callbyvalueall_seq-eta
callbyvalueall_seq-extend
callbyvalueall_seq-fun1
callbyvalueall_seq-fun2
callbyvalueall_seq-fun3
callbyvalueall_seq-fun4
callbyvalueall_seq-lambdas-all
callbyvalueall_seq-lambdas-all0
callbyvalueall_seq-partial-ap-all
callbyvalueall_seq-partial-ap-all0
callbyvalueall_seq-seq
callbyvalueall_seq-shift
callbyvalueall_seq-shift-init
callbyvalueall_seq-shift-init0
callbyvalueall_seq-spread
callbyvalueall_seq-spread0
callbyvalueall_seq_wf
cbva-seq
cbva-seq_seq
cbva-seq_wf
cbva_seq
cbva_seq-combine
cbva_seq-combine2
cbva_seq-list-case1
cbva_seq-list-case2
cbva_seq-spread
cbva_seq-sqequal-n
cbva_seq_extend
cbva_seq_wf
code-coded-seq
code-seq
code-seq-bijection
code-seq_wf
coded-code-seq
coded-seq
coded-seq_wf
comparison-seq
comparison-seq-simple-wf
comparison-seq-zero
comparison-seq-zero-simple
comparison-seq_wf
cons-seq
cons-seq_wf
consistent-seq
consistent-seq_wf
derived-seq
derived-seq_wf
eq_seq
eq_seq_wf
es-seq
es-seq_wf
finite-deriv-seq
finite-deriv-seq_wf
implies-strictly-increasing-seq
infinite-deriv-seq
infinite-deriv-seq_wf
is-basic-seq
is-basic-seq_wf
locally-non-constant-deriv-seq-test
locally-non-zero-finite-deriv-seq
null-seq
null-seq_wf
polynomial-deriv-seq
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
regular-int-seq
regular-int-seq_wf
rmul-bdd-diff-reg-seq-mul
seq-add
seq-add_wf
seq-add_wf_consistent
seq-adjoin
seq-adjoin_wf
seq-append
seq-append-assoc
seq-append-normalize
seq-append0
seq-append1
seq-append1-assoc
seq-append_wf
seq-append_wf_consistent
seq-count
seq-count_wf
seq-normalize
seq-normalize-append
seq-normalize-equal
seq-normalize-normalize
seq-normalize0
seq-normalize_wf
seq-single
seq-single_wf
simple-cbva-seq
simple-cbva-seq-combine
simple-cbva-seq-extend
simple-cbva-seq-extend-2
simple-cbva-seq-list
simple-cbva-seq-list-case1
simple-cbva-seq-list-case2
simple-cbva-seq-spread
simple-cbva-seq-spread0
simple-cbva-seq-sqequal-n
simple-cbva-seq_wf
sq_stable__regular-int-seq
strictly-increasing-seq
strictly-increasing-seq-add
strictly-increasing-seq_wf
weakly-safe-seq
weakly-safe-seq_wf

---

SEQ1

prev top next

code-coded-seq1
code-seq1
code-seq1_wf
coded-code-seq1
coded-seq1
coded-seq1_wf

---

SEQUENCE

prev top next

bounded-sequence
bounded-sequence_wf
decidable-ses-fresh-sequence
decidable__ses-legal-sequence
es-increasing-sequence
finite-sequence-coding-exists
hdf-sequence
hdf-sequence_wf
sequence-class
sequence-class-program
sequence-class-program_wf
sequence-class_wf
sequence-classrel
ses-fresh-sequence
ses-fresh-sequence_wf
ses-legal-sequence
ses-legal-sequence_wf

---

SEQUENCE1

prev top next

ses-basic-sequence1
ses-basic-sequence1_wf

---

SEQUENCE2

prev top next

es-increasing-sequence2

---

SEQUENCES

prev top next

equipollent-nat-sequences

---

SEQUENT

prev top next

mFOL-sequent
mFOL-sequent-abstract
mFOL-sequent-abstract_wf
mFOL-sequent-evidence
mFOL-sequent-evidence-trivial
mFOL-sequent-evidence_and
mFOL-sequent-evidence_transitivity1
mFOL-sequent-evidence_transitivity2
mFOL-sequent-evidence_wf
mFOL-sequent_wf

---

SEQUENTIAL

prev top next

sequential-composition-class
sequential-composition-inputs
sequential-composition-inputs_wf

---

SERIES

prev top next

Taylor-series-converges
alternating-series-converges
continuous-series-sum
exp-series-converges
fun-series-converges
fun-series-converges-absolutely
fun-series-converges-absolutely-converges
fun-series-converges-absolutely_wf
fun-series-converges-on-compact
fun-series-converges-tail
fun-series-converges_wf
fun-series-sum
fun-series-sum_wf
geometric-series-converges
geometric-series-converges-ext
harmonic-series-diverges
power-series
power-series-converges
power-series_wf
series-converges
series-converges-limit-zero
series-converges-rmul
series-converges-rmul-ext
series-converges-tail
series-converges-tail2
series-converges-tail2-ext
series-converges_wf
series-diverges
series-diverges-trivially
series-diverges_wf
series-sum
series-sum-linear1
series-sum-linear2
series-sum-linear3
series-sum_wf
triangular-reciprocal-series-sum

---

SERVER

prev top next

loc-Server
loc-Server_wf
loc-Server_wf2
loc-server-comment

---

SES

prev top next

assert-ses-is-fresh
assert-ses-is-legal
decidable-ses-fresh-sequence
decidable__ses-action
decidable__ses-legal-sequence
ses-D
ses-D-implies
ses-D-private
ses-D-private_wf
ses-D-public
ses-D-public_wf
ses-D_wf
ses-K
ses-K_wf
ses-NR
ses-NR_wf
ses-NU
ses-NU_wf
ses-R
ses-R_wf
ses-S
ses-S_wf
ses-V
ses-V_wf
ses-act
ses-act-has-atom
ses-act_wf
ses-action
ses-action_wf
ses-axioms
ses-axioms-imply
ses-axioms_wf
ses-basic-sequence1
ses-basic-sequence1_wf
ses-cabal
ses-cabal_wf
ses-cipher
ses-cipher-unique
ses-cipher-unique2
ses-cipher_wf
ses-crypt
ses-crypt_wf
ses-decrypt
ses-decrypt_wf
ses-decrypted
ses-decrypted_wf
ses-decryption-key
ses-decryption-key_wf
ses-disjoint
ses-disjoint-old
ses-disjoint_wf
ses-encrypt
ses-encrypt_wf
ses-encrypted
ses-encrypted_wf
ses-encryption-key
ses-encryption-key_wf
ses-flow
ses-flow-axiom
ses-flow-axiom-ordering
ses-flow-axiom_wf
ses-flow-causle
ses-flow-has
ses-flow-has*
ses-flow-implies
ses-flow-implies'
ses-flow-induction
ses-flow_wf
ses-fresh-sequence
ses-fresh-sequence_wf
ses-fresh-thread
ses-fresh-thread_wf
ses-honest
ses-honest_wf
ses-honest_witness
ses-info
ses-info-flow
ses-info-flow-exp_functionality
ses-info-flow_functionality
ses-info-flow_wf
ses-info_wf
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-key-rel
ses-key-rel_wf
ses-key-rel_witness
ses-legal-sequence
ses-legal-sequence_wf
ses-legal-thread
ses-legal-thread-decrypt
ses-legal-thread-has*-nonce
ses-legal-thread-has*-signature
ses-legal-thread-has-atom
ses-legal-thread_wf
ses-msg
ses-msg-cases
ses-msg_wf
ses-new
ses-new_wf
ses-nonce
ses-nonce-disjoint
ses-nonce-disjoint_wf
ses-nonce-from-ordering
ses-nonce-release
ses-nonce-unique
ses-nonce_wf
ses-ordering
ses-ordering'
ses-ordering'_wf
ses-ordering-implies
ses-ordering-ordering'
ses-ordering_wf
ses-private
ses-private-key
ses-private-key-atoms
ses-private-key_wf
ses-private-not-public
ses-private-one-one
ses-private_wf
ses-protocol1
ses-protocol1-legal
ses-protocol1-legal_wf
ses-protocol1-thread
ses-protocol1-thread_wf
ses-protocol1_wf
ses-public-key
ses-public-key-atoms
ses-public-key_wf
ses-public-not-private
ses-public-one-one
ses-rcv
ses-rcv_wf
ses-secrecy
ses-secrecy_wf
ses-send
ses-send_wf
ses-sig
ses-sig_wf
ses-sign
ses-sign-has-atom
ses-sign-is-protocol-action
ses-sign_wf
ses-signature-unique
ses-signature-unique2
ses-signed
ses-signed_wf
ses-signer
ses-signer_wf
ses-thread
ses-thread-loc
ses-thread-loc_wf
ses-thread-member
ses-thread-member_wf
ses-thread-no_repeats
ses-thread-order
ses-thread-subtype
ses-thread-weak-order
ses-thread_wf
ses-useable-atoms
ses-useable-atoms_wf
ses-used-atoms
ses-used-atoms_wf
ses-verify
ses-verify-sig
ses-verify-sig_wf
ses-verify-signed
ses-verify-signed_wf
ses-verify-signer
ses-verify-signer_wf
ses-verify_wf

---

SESSION

prev top next

thread-session
thread-session_wf

---

SET

prev top next

Kan-cubical-set
Kan-cubical-set_wf
assert_of_set_leq
assert_of_set_lt
bag-member-filter-set
bag-to-set
bag-to-set_wf
cantor-theorem-on-power-set
cantor-theorem-on-power-set-prop
cardinality-le-list-set
comb_for_set_blt_wf
continuous-monotone-set
count-bag-to-set
cube-set-map
cube-set-map-is
cube-set-map-subtype
cube-set-map_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
cubical-set
cubical-set-is-functor
cubical-set_wf
decidable__equal_set
decidable__set_leq
decidable__set_lt
decl-set-read-allowed
dset_set
dset_set_wf
equal-count-bag-to-set
equipollent-set
es-decl-set
es-decl-set-avoids
es-decl-set-avoids-tag
es-decl-set-avoids-tag_wf
es-decl-set-avoids_wf
es-decl-set-da
es-decl-set-da_wf
es-decl-set-declares-tag
es-decl-set-declares-tag_wf
es-decl-set-domain
es-decl-set-domain_wf
es-decl-set-ds
es-decl-set-ds_wf
es-decl-set-join
es-decl-set-join-domain
es-decl-set-join_wf
es-decl-set-single
es-decl-set-single_wf
es-decl-set_wf
es-interface-set-subtype
finite-decidable-set
finite-set-type
finite-set-type-cases
finite_set
finite_set_wf
fpf-sub-set
fpf-trivial-subtype-set
fps-set-to-one
fps-set-to-one-add
fps-set-to-one-neg
fps-set-to-one-one
fps-set-to-one-scalar-mul
fps-set-to-one-single
fps-set-to-one-slice
fps-set-to-one-sub
fps-set-to-one-ucont
fps-set-to-one-zero
fps-set-to-one_wf
id-fun-set
interface_predicate_set_lemma
l_all-set
l_before_filter_set_type
l_contains-eq_set-no_repeats
l_member-set
l_member_set
last-event-of-set
list-eq-set-type
list-equal-set
list-prod-set-type
list-set-type
list-set-type-member
list-set-type-property
list-set-type2
list-set-type3
list-to-set
list-to-set-cons
list-to-set-filter
list-to-set-is-remove-repeats
list-to-set-property
list-to-set_functionality_wrt_permutation
list-to-set_wf
list_accum-set-equal-idemp
list_accum_set-equal
list_set_type
list_to_set_nil_lemma
member-bag-to-set
member-list-to-set
mk-set
mk-set-nat-missing
mk-set-nat-missing_wf
mk-set_wf
no-repeats-bag-to-set
no-repeats-list-to-set
normal-decl-set
normal-decl-set_wf
pair-list-set-type
per-set
per-set_wf
power-set
power-set-lift
power-set-lift-well-founded-implies
power-set-lift_wf
power-set_wf
remove-repeats-set-equal
set def
set-elim
set-equal
set-equal-cons
set-equal-equiv
set-equal-l_contains
set-equal-nil
set-equal-nil2
set-equal-no_repeats-length
set-equal-permute
set-equal-reflex
set-equal-remove-repeats
set-equal_wf
set-is-image
set-member
set-member_wf
set-mono
set-path-name
set-path-name_wf
set-sig
set-sig-add
set-sig-add-prop
set-sig-add_wf
set-sig-empty
set-sig-empty-prop
set-sig-empty-prop2
set-sig-empty_wf
set-sig-isEmpty
set-sig-isEmpty_wf
set-sig-member
set-sig-member_wf
set-sig-remove
set-sig-remove_wf
set-sig-set
set-sig-set-squash
set-sig-set-vatype
set-sig-set_wf
set-sig-singleton
set-sig-singleton_wf
set-sig-union
set-sig-union_wf
set-sig_wf
set-value-type
set-valueall-type
set-wf
set_blt
set_blt_functionality_wrt_set_lt_r
set_blt_wf
set_car
set_car_inc
set_car_wf
set_eq
set_eq_wf
set_le
set_le_wf
set_leq
set_leq_antisymmetry
set_leq_complement
set_leq_iff_lt_or_eq
set_leq_trans
set_leq_transitivity
set_leq_weakening_eq
set_leq_weakening_lt
set_leq_wf
set_lt
set_lt_complement
set_lt_irreflexivity
set_lt_is_sp_of_leq
set_lt_is_sp_of_leq_a
set_lt_transitivity_1
set_lt_transitivity_2
set_lt_wf
set_prod
set_prod_wf
set_subtype_base
set_wf
strong-continuous-set
strong-subtype-set
sublist_filter_set_type
subtype-set-hasloc
subtype_rel-per-set
subtype_rel_list_set
subtype_rel_nested_set
subtype_rel_set
subtype_rel_set_simple
three-intersecting-wait-set
three-intersecting-wait-set-exists
trivial-cube-set
trivial-cube-set_wf
two-intersecting-wait-set
two-intersecting-wait-set-exists
two-intersecting-wait-set-exists'
uni_sat_imp_in_uni_set
union-set-is-set-exists
unique_set
unique_set_wf

---

SET1

prev top next

strong-subtype-set1

---

SET2

prev top next

l_member-set2
l_member_set2
list-equal-set2
strong-subtype-set2
subtype_rel_nested_set2

---

SET3

prev top next

strong-subtype-set3

---

SETS

prev top next

es-decl-sets-compatible
es-decl-sets-compatible_wf
es-decl-sets-sub
es-decl-sets-sub_wf
subtype_rel_sets

---

SETTYPE

prev top next

bag-no-repeats-settype
bag-settype
l_member-settype
l_member_settype
no_repeats-settype

---

SHEAF

prev top next

rep-pre-sheaf
rep-pre-sheaf
rep-pre-sheaf_wf
rep-pre-sheaf_wf

---

SHIFT

prev top next

A-shift-spec
A-shift-spec_wf
A-shift-upto
A-shift-upto-spec
A-shift-upto-spec_wf
A-shift-upto_wf
anti_sym_shift
assoc_shift
callbyvalueall_seq-shift
callbyvalueall_seq-shift-init
callbyvalueall_seq-shift-init0
cancel_shift
comm_shift
connex_shift
double-negation-shift
double-negation-shift_wf
eqfun_p_shift
finite-double-negation-shift
finite-double-negation-shift-extract
from-upto-shift
gcd_p_shift
grp_eq_shift_right
grp_leq_shift_right
grp_lt_shift_right
ident_mon_hom_shift
inverse_grp_sig_hom_shift
itop_shift
le-add-shift
limit-shift
mk_lambdas-fun-shift-init
mon_itop_shift
monot_shift
mset_for_dom_shift
mset_for_when_dom_shift
pcw-path-shift
predicate-or-shift
predicate-or-shift_wf
predicate-shift
predicate-shift_wf
reduce2_shift
refl_shift
rng_mssum_dom_shift
rng_sum_shift
rsum-shift
rsum-split-shift
rv-disjoint-rv-shift
rv-disjoint-shift
rv-shift
rv-shift-linear
rv-shift_wf
shift-play
shift-play_wf
sym_shift
trans_shift
uanti_sym_shift
urefl_shift
usym_shift
utrans_shift

---

SHORTEN

prev top next

append-tuple-shorten-tuple
select-shorten-tuple
shorten-tuple
shorten-tuple-append-tuple
shorten-tuple-simplify
shorten-tuple-simplify2
shorten-tuple-split-tuple
shorten-tuple_wf
shorten-tuple_wf2

---

SHOW

prev top next

show

---

SHUFFLE

prev top next

length-shuffle
select-shuffle
shuffle
shuffle_wf
unshuffle-shuffle

---

SHUFFLE2

prev top next

select-shuffle2

---

SIDE

prev top next

eu-between-eq-same-side

---

SIDE2

prev top next

eu-between-eq-same-side2

---

SIERPINSKI

prev top next

Sierpinski
Sierpinski-bottom
Sierpinski-bottom_wf
Sierpinski-cases
Sierpinski-cases2
Sierpinski-equal
Sierpinski-equal-bottom
Sierpinski-equal2
Sierpinski-top
Sierpinski-top_wf
Sierpinski-unequal
Sierpinski-unequal-1
Sierpinski_wf
equal-Sierpinski-bottom
not-Sierpinski-bottom
not-Sierpinski-top
subtype-Sierpinski

---

SIG

prev top next

------ new_23_sig - extra ------
------ new_23_sig - headers ------
------ new_23_sig - specification ------
W-to-not-not-sig
algebra_sig
algebra_sig_inc
algebra_sig_wf
algebra_subtype_algebra_sig
comb_for_perm_sig_wf
fabgrp_sig
fabgrp_sig_wf
fma_sig
fma_sig_wf
fresh-sig-protocol1
fresh-sig-protocol1_property
fresh-sig-protocol1_wf
gcopower_sig
gcopower_sig_wf
grp_sig
grp_sig_inc
grp_sig_wf
grp_subtype_grp_sig
imon_subtype_grp_sig
inverse_grp_sig_hom_shift
loset_subtype_poset_sig
map-sig
map-sig-add
map-sig-add_wf
map-sig-empty
map-sig-empty_wf
map-sig-eqKey
map-sig-eqKey_wf
map-sig-find
map-sig-find_wf
map-sig-inDom
map-sig-inDom-prop
map-sig-inDom_wf
map-sig-isEmpty
map-sig-isEmpty_wf
map-sig-map
map-sig-map-squash
map-sig-map-vatype
map-sig-map_wf
map-sig-remove
map-sig-remove_wf
map-sig-update
map-sig-update_wf
map-sig_wf
mcopower_sig
mcopower_sig_wf
mon_subtype_grp_sig
nat_int_grp_sig_hom
new_23_sig-decided
new_23_sig-ilf
new_23_sig-notify
new_23_sig-retry
new_23_sig-vote
new_23_sig_NewRounds
new_23_sig_NewRounds-program
new_23_sig_NewRounds-program_wf
new_23_sig_NewRoundsState
new_23_sig_NewRoundsState-classrel
new_23_sig_NewRoundsState-functional
new_23_sig_NewRoundsState-program
new_23_sig_NewRoundsState-program_wf
new_23_sig_NewRoundsStateFun
new_23_sig_NewRoundsStateFun_wf
new_23_sig_NewRoundsState_wf
new_23_sig_NewRounds_wf
new_23_sig_NewVoters
new_23_sig_NewVoters-program
new_23_sig_NewVoters-program_wf
new_23_sig_NewVoters_wf
new_23_sig_Notify
new_23_sig_Notify-program
new_23_sig_Notify-program_wf
new_23_sig_Notify_wf
new_23_sig_Proposal
new_23_sig_Proposal-program
new_23_sig_Proposal-program_wf
new_23_sig_Proposal_wf
new_23_sig_Quorum
new_23_sig_Quorum-program
new_23_sig_Quorum-program_wf
new_23_sig_QuorumState
new_23_sig_QuorumState-classrel
new_23_sig_QuorumState-functional
new_23_sig_QuorumState-program
new_23_sig_QuorumState-program_wf
new_23_sig_QuorumStateFun
new_23_sig_QuorumStateFun_wf
new_23_sig_QuorumState_wf
new_23_sig_Quorum_wf
new_23_sig_Replica
new_23_sig_Replica-program
new_23_sig_Replica-program_wf
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_ReplicaStateFun
new_23_sig_ReplicaStateFun_wf
new_23_sig_ReplicaState_wf
new_23_sig_Replica_wf
new_23_sig_Round
new_23_sig_Round-program
new_23_sig_Round-program_wf
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
new_23_sig_Round_wf
new_23_sig_Rounds
new_23_sig_Rounds-program
new_23_sig_Rounds-program_wf
new_23_sig_Rounds_wf
new_23_sig_Voter
new_23_sig_Voter-program
new_23_sig_Voter-program_wf
new_23_sig_Voter_wf
new_23_sig_add_to_quorum
new_23_sig_add_to_quorum_wf
new_23_sig_addvote
new_23_sig_addvote_wf
new_23_sig_agreement
new_23_sig_assert_newvote
new_23_sig_commands_from_votes
new_23_sig_commands_from_votes_wf
new_23_sig_decided'base
new_23_sig_decided'base-program
new_23_sig_decided'base-program_wf
new_23_sig_decided'base_wf
new_23_sig_decided'broadcast
new_23_sig_decided'broadcast_wf
new_23_sig_decided_property
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_decision
new_23_sig_decision_wf
new_23_sig_headers
new_23_sig_headers_fun
new_23_sig_headers_fun_wf
new_23_sig_headers_internal
new_23_sig_headers_internal_wf
new_23_sig_headers_no_inputs
new_23_sig_headers_no_inputs_types
new_23_sig_headers_no_inputs_types_wf
new_23_sig_headers_no_inputs_wf
new_23_sig_headers_no_rep
new_23_sig_headers_no_rep_wf
new_23_sig_headers_type
new_23_sig_headers_type_wf
new_23_sig_headers_wf
new_23_sig_increasing_max
new_23_sig_main
new_23_sig_main-program
new_23_sig_main-program_wf
new_23_sig_main_wf
new_23_sig_message-constraint
new_23_sig_message-constraint_wf
new_23_sig_messages-delivered
new_23_sig_messages-delivered_wf
new_23_sig_newvote
new_23_sig_newvote_wf
new_23_sig_notify'broadcast
new_23_sig_notify'broadcast_wf
new_23_sig_progress-step1
new_23_sig_progress-step10
new_23_sig_progress-step2
new_23_sig_progress-step3
new_23_sig_progress-step4
new_23_sig_progress-step5
new_23_sig_progress-step6
new_23_sig_progress-step7
new_23_sig_progress-step8
new_23_sig_progress-step8-v2
new_23_sig_progress-step8-v3
new_23_sig_progress-step9
new_23_sig_progress-step9-v2
new_23_sig_progress-step9-v3
new_23_sig_progress1
new_23_sig_progress2-step1
new_23_sig_progress2-step2
new_23_sig_proposal_classrel
new_23_sig_proposal_classrel2
new_23_sig_proposal_has_header
new_23_sig_proposal_if_vote
new_23_sig_propose'base
new_23_sig_propose'base-program
new_23_sig_propose'base-program_wf
new_23_sig_propose'base_wf
new_23_sig_quorum_fseg
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
new_23_sig_quorum_invariant
new_23_sig_quorum_invariant_fun
new_23_sig_quorum_mem
new_23_sig_quorum_state_eq1
new_23_sig_quorum_state_eq1-forward
new_23_sig_quorum_state_fun_eq
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_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
new_23_sig_round_info_classrel2
new_23_sig_roundout
new_23_sig_roundout_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
new_23_sig_update_replica
new_23_sig_update_replica_wf
new_23_sig_update_round
new_23_sig_update_round_wf
new_23_sig_validity
new_23_sig_vote'base
new_23_sig_vote'base-program
new_23_sig_vote'base-program_wf
new_23_sig_vote'base_wf
new_23_sig_vote'broadcast
new_23_sig_vote'broadcast_wf
new_23_sig_vote2prop
new_23_sig_vote2prop_wf
new_23_sig_vote2retry
new_23_sig_vote2retry_wf
new_23_sig_vote_with_ballot
new_23_sig_vote_with_ballot-assert-classrel
new_23_sig_vote_with_ballot-assert-type
new_23_sig_vote_with_ballot-forward
new_23_sig_vote_with_ballot-header
new_23_sig_vote_with_ballot-if-classrel
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
new_23_sig_vote_with_ballot_first
new_23_sig_vote_with_ballot_first-assert
new_23_sig_vote_with_ballot_first-assert-forward
new_23_sig_vote_with_ballot_first-assert-forward2
new_23_sig_vote_with_ballot_first-assert-type
new_23_sig_vote_with_ballot_first-forward
new_23_sig_vote_with_ballot_first-not
new_23_sig_vote_with_ballot_first-not2
new_23_sig_vote_with_ballot_first_alt
new_23_sig_vote_with_ballot_first_alt_wf
new_23_sig_vote_with_ballot_first_wf
new_23_sig_vote_with_ballot_wf
new_23_sig_voter_start
new_23_sig_voter_start_unique
new_23_sig_votes_consistent
new_23_sig_when_new_proposal
new_23_sig_when_new_proposal_wf
new_23_sig_when_new_round
new_23_sig_when_new_round_wf
new_23_sig_when_quorum
new_23_sig_when_quorum_wf
not-not-sig-to-W
not-not-sig-to-W-implies-stable
perm_sig
perm_sig_wf
poset_sig
poset_sig_inc
poset_sig_wf
quot_ring_sig
rng_sig
rng_sig_inc
rng_sig_wf
rng_subtype_rng_sig
ses-sig
ses-sig_wf
ses-verify-sig
ses-verify-sig_wf
set-sig
set-sig-add
set-sig-add-prop
set-sig-add_wf
set-sig-empty
set-sig-empty-prop
set-sig-empty-prop2
set-sig-empty_wf
set-sig-isEmpty
set-sig-isEmpty_wf
set-sig-member
set-sig-member_wf
set-sig-remove
set-sig-remove_wf
set-sig-set
set-sig-set-squash
set-sig-set-vatype
set-sig-set_wf
set-sig-singleton
set-sig-singleton_wf
set-sig-union
set-sig-union_wf
set-sig_wf
sig-release-thread
sig-release-thread_wf
sig-to-W
subtype_rel_rng_sig
unique-sig-protocol
unique-sig-protocol_wf

---

SIG2

prev top next

W-to-not-not-sig2

---

SIGMA

prev top next

Kan-cubical-sigma
Kan-cubical-sigma_wf
Kan_sigma_filler
Kan_sigma_filler_uniform
Kan_sigma_filler_wf
causal_order_sigma
csm-Kan-cubical-sigma
csm-cubical-sigma
cubical-sigma
cubical-sigma-at
cubical-sigma_wf
sigma-box-fst
sigma-box-fst_wf
sigma-box-snd
sigma-box-snd_wf

---

SIGN

prev top next

decidable__pa-is-sign-implies
pa-is-sign-implies
pa-is-sign-implies_wf
rem-sign
ses-sign
ses-sign-has-atom
ses-sign-is-protocol-action
ses-sign_wf
sign
sign-absval
sign-squared
sign_wf

---

SIGNATURE

prev top next

ses-legal-thread-has*-signature
ses-signature-unique
ses-signature-unique2
signature-release-lemma
signature-release-lemma2

---

SIGNATURES

prev top next

noncelike-signatures
noncelike-signatures_wf

---

SIGNED

prev top next

ses-signed
ses-signed_wf
ses-verify-signed
ses-verify-signed_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

---

SIGNER

prev top next

ses-signer
ses-signer_wf
ses-verify-signer
ses-verify-signer_wf

---

SIM

prev top next

bool_sim_false
bool_sim_true

---

SIMILAR

prev top next

similar-bags
similar-bags_wf

---

SIMP

prev top next

band_ff_simp
band_tt_simp
bor_ff_simp
bor_tt_simp
exists-simp
exists-simp-test
simp_lemma1
sq_or_simp
test-squash-simp

---

SIMPLE

prev top next

C_DVALUEp_ind_wf_simple
C_LVALUE_ind_wf_simple
C_TYPE_ind_wf_simple
MultiTree_ind_wf_simple
RankEx1_ind_wf_simple
RankEx2_ind_wf_simple
RankEx4_ind_wf_simple
band-simple-decide
band-simple-int_eq
binary-tree_ind_wf_simple
binary_map_ind_wf_simple
comparison-seq-simple-wf
comparison-seq-zero-simple
decide-simple-int_eq
decide-simple-less
formula_ind_wf_simple
fps-mul-coeff-bag-rep-simple
glued-composes-simple
hdf-cbva-simple
hdf-cbva-simple_wf
in-simple-loc-comb-1-concat
iterate-hdf-bind-simple
iterate-hdf-buffer-simple
iterate-hdf-buffer2-simple
l_tree_ind_wf_simple
lift-simple-decide-decide1
lift-simple-decide-decide2
lifting-loc-member-simple
lifting-member-simple
mFOLRule_ind_wf_simple
mFOL_ind_wf_simple
map-simple-reduce
member-eclass-simple-comb-1
member-eclass-simple-comb-1-iff
member-eclass-simple-comb-2-iff
member-eclass-simple-loc-comb-1
member-eclass-simple-loc-comb-1-iff
member-eclass-simple-loc-comb-2-iff
pi-rank-pi-simple-subst
pi-rank-pi-simple-subst-aux
pi-simple-subst
pi-simple-subst-aux
pi-simple-subst-aux_wf
pi-simple-subst_wf
pi_prefix_ind_wf_simple
pi_term_ind_wf_simple
process-ordered-message_wf_simple
reals-uncountable-simple
rec-process_wf_pi_simple_state
send-once-loc-class-eq-once-simple-loc-comb-0
simple-bind-nxt
simple-bind-nxt_wf
simple-cbva-seq
simple-cbva-seq-combine
simple-cbva-seq-extend
simple-cbva-seq-extend-2
simple-cbva-seq-list
simple-cbva-seq-list-case1
simple-cbva-seq-list-case2
simple-cbva-seq-spread
simple-cbva-seq-spread0
simple-cbva-seq-sqequal-n
simple-cbva-seq_wf
simple-chain-rule
simple-comb
simple-comb-0
simple-comb-0_wf
simple-comb-1
simple-comb-1-classrel
simple-comb-1-classrel-weak
simple-comb-1-concat-classrel
simple-comb-1-concat-classrel-weak
simple-comb-1-disjoint-classrel
simple-comb-1-es-sv
simple-comb-1-single-val
simple-comb-1_wf
simple-comb-2
simple-comb-2-classrel
simple-comb-2-classrel-weak
simple-comb-2-concat-classrel
simple-comb-2-concat-classrel-weak
simple-comb-2-es-sv
simple-comb-2_wf
simple-comb-3
simple-comb-3_wf
simple-comb-4
simple-comb-4_wf
simple-comb-classrel
simple-comb-concat-classrel
simple-comb-es-sv
simple-comb0
simple-comb0_wf
simple-comb1
simple-comb1-classrel
simple-comb1-concat-classrel
simple-comb1_wf
simple-comb2
simple-comb2-classrel
simple-comb2-concat-classrel
simple-comb2_wf
simple-comb3
simple-comb3_wf
simple-comb_wf
simple-decidable-finite-cantor
simple-decidable-finite-cantor-ext
simple-fan-theorem
simple-finite-cantor-decider
simple-finite-cantor-decider_wf
simple-hdf-bind
simple-hdf-bind_wf
simple-hdf-buffer
simple-hdf-buffer2
simple-hdf-buffer2_wf
simple-hdf-buffer_wf
simple-loc-comb
simple-loc-comb-0
simple-loc-comb-0_wf
simple-loc-comb-1
simple-loc-comb-1-classrel
simple-loc-comb-1-classrel-weak
simple-loc-comb-1-concat-classrel
simple-loc-comb-1-concat-classrel-weak
simple-loc-comb-1-concat-es-sv
simple-loc-comb-1-concat-single-val
simple-loc-comb-1_wf
simple-loc-comb-2
simple-loc-comb-2-classrel
simple-loc-comb-2-classrel-weak
simple-loc-comb-2-concat-classrel
simple-loc-comb-2-concat-classrel-weak
simple-loc-comb-2-concat-es-sv
simple-loc-comb-2-concat-loc-bounded
simple-loc-comb-2-concat-loc-bounded2
simple-loc-comb-2-concat-loc-bounded3
simple-loc-comb-2-concat-single-val
simple-loc-comb-2-loc-bounded
simple-loc-comb-2-loc-bounded2
simple-loc-comb-2-loc-bounded3
simple-loc-comb-2_wf
simple-loc-comb-3
simple-loc-comb-3-concat-es-sv
simple-loc-comb-3-concat-single-val
simple-loc-comb-3_wf
simple-loc-comb-4
simple-loc-comb-4_wf
simple-loc-comb-classrel
simple-loc-comb-concat-classrel
simple-loc-comb0
simple-loc-comb0_wf2
simple-loc-comb1
simple-loc-comb1-classrel
simple-loc-comb1-concat-classrel
simple-loc-comb1_wf
simple-loc-comb2
simple-loc-comb2-classrel
simple-loc-comb2-concat-classrel
simple-loc-comb2_wf
simple-loc-comb_wf
simple-partition-exists
simple-primrec-add
simple-product_subtype_base
simple-swap
simple-swap-correct
simple-swap-specification
simple-swap-specification_wf
simple-swap-test
simple-swap-test2
simple-swap-test2_wf
simple-swap-test_wf
simple-swap2
simple-swap2_wf
simple-swap3
simple-swap3_wf
simple-swap_wf
simple_fan_theorem
simple_fan_theorem-ext
subtype_rel_set_simple
subtype_rel_simple_product
tree_ind_wf_simple
until-class-simple-comb

---

SIMPLIFY

prev top next

append-tuple-simplify
band-simplify
bor-simplify
map-simplify-test
shorten-tuple-simplify
simplify-equal-imp

---

SIMPLIFY0

prev top next

ifthenelse-simplify0

---

SIMPLIFY1

prev top next

ifthenelse-simplify1
union-list2-simplify1

---

SIMPLIFY2

prev top next

append-tuple-simplify2
ifthenelse-simplify2
shorten-tuple-simplify2

---

SIMPLIFY3

prev top next

ifthenelse-simplify3

---

SIMULATION

prev top next

consistent-local-simulation
iseg-local-simulation-inputs
local-simulation-E-subtype
local-simulation-agreement
local-simulation-class
local-simulation-class_wf
local-simulation-classrel
local-simulation-embedding
local-simulation-eo
local-simulation-eo-loc
local-simulation-eo_wf
local-simulation-event
local-simulation-event-info
local-simulation-event-loc
local-simulation-event_wf
local-simulation-input-consistency
local-simulation-input-consistency_wf
local-simulation-input-validity
local-simulation-input-validity_wf
local-simulation-inputs
local-simulation-inputs_wf
local-simulation-msg-constraint
local-simulation-validity
local-simulation-validity2
member-local-simulation-inputs

---

SINCE

prev top next

alle-between1-not-first-since
alle-between2-not-first-since
es-first-at-since
es-first-at-since'
es-first-at-since'_wf
es-first-at-since-iff
es-first-at-since_wf
es-first-since
es-first-since_functionality_wrt_iff
es-first-since_wf
es-interface-vals-since
es-interface-vals-since_wf
es-pplus-first-since
es-pplus-first-since-exit
l_all_since
l_all_since_wf

---

SINGLE

prev top next

Accum-class-single-val
Accum-class-single-val0
Memory-class-single-val
Memory-class-single-val2
Memory-classrel-single-val
Memory-loc-class-single-val
Memory-loc-classrel-single-val
Prior-Accum-class-single-val0
State-class-single-val
State-class-single-val0
State-comb-classrel-single-val
State-comb-single-val
State-comb-single-val0
State-loc-comb-classrel-single-val
State-loc-comb-single-val
State-loc-comb-single-val0
archive-condition-single
bag-accum-single
bag-append-is-single
bag-append-is-single-iff
bag-append-is-single-iff2
bag-combine-is-single-if
bag-combine-single-left
bag-combine-single-right
bag-combine-single-right-as-map
bag-count-single
bag-map-single
bag-maximal?-single
bag-member-single
bag-member-single-weak
bag-no-repeats-single
bag-product-single
bag-rep-is-single-valued
bag-single-no-repeats
bag-summation-single
bag-summation-single-non-zero
bag-summation-single-non-zero-no-repeats
bag-union-is-single
bag-union-is-single-if
bag-union-single
bag_map_single_lemma
bag_only_single_lemma
bag_size_single_lemma
base-headers-msg-val-single-val
bm_single_L
bm_single_L_wf
bm_single_R
bm_single_R_wf
callbyvalueall-single
callbyvalueall-single-append-nil
callbyvalueall-single-bag-combine1
callbyvalueall-single-bag-combine2
callbyvalueall-single-bag-combine3
callbyvalueall-single-bag-combine4
callbyvalueall-single-repeat
callbyvalueall-single-sqle
callbyvalueall-single-sqle2
class-at-single-val
combine_list_single_lemma
concat-map-single
concat-single
concat_conv_single_nil_lemma
cond-msg-body-single-valued
count-single
cs-inning-committed-single
cs-inning-committed-single-stable
decidable__exists-single-valued-bag
decidable__exists-single-valued-classrel
disjoint-union-class-single-val
disjoint-union-comb-single-val
eclass0-single-val
eclass1-single-val
eclass2-single-val
eclass3-single-val
es-decl-set-single
es-decl-set-single_wf
es-sv-class-implies-single-valued-classrel
fpf-add-single
fpf-add-single_wf
fpf-all-single
fpf-all-single-decl
fpf-ap-single
fpf-cap-single
fpf-cap-single-join
fpf-compatible-single
fpf-compatible-single-iff
fpf-join-single-property
fpf-single
fpf-single-dom
fpf-single-dom-sq
fpf-single-sub-reflexive
fpf-single-valued
fpf-single-valued_wf
fpf-single_wf
fpf-single_wf2
fpf-single_wf3
fpf_ap_single_lemma
fps-compose-single
fps-compose-single-disjoint
fps-mul-single
fps-mul-single-general
fps-product-single
fps-set-to-one-single
fps-single
fps-single-slice
fps-single_wf
from-upto-single
has-valueall-single
hdf-ap-single-valued-except
hdf-ap-single-valued-except2
hdf-single-val-step
hdf-single-val-step_wf
hdf-single-valued
hdf-single-valued-except
hdf-single-valued-except_wf
hdf-single-valued_wf
hdf-state-single-val
hdf-state-single-val_wf
hdf-state1-single-val
hdf-state1-single-val_wf
iseg_append_single
iseg_single
iterated-classrel-single-val
iterated_classrel-single-val
l-ordered-single
l_all_single
l_exists_single
length-concat-map-single
list-diff-cons-single
lnk-decl-compatible-single
lnk-decl-dom-single
local-class-single-valued-class-except
loop-class-memory-single-val
loop-class-state-single-val
mklist-single
new_23_sig_RoundInfo-single-val
no_repeats-single
non-void-decl-single
normal-da-single
normal-ds-single
on-loc-class-single-val
parallel-class-single-val
primed-class-opt-single-val
primed-class-opt-single-val0
quicksort-int-single
rec-combined-class-opt-1-single-val
rec-combined-class-opt-1-single-val0
rec-combined-loc-class-opt-1-single-val
rec-combined-loc-class-opt-1-single-val0
rsum-single
rsum_single
seq-single
seq-single_wf
simple-comb-1-single-val
simple-loc-comb-1-concat-single-val
simple-loc-comb-2-concat-single-val
simple-loc-comb-3-concat-single-val
single-bag
single-bag-append-nil
single-bag-not-null
single-bag_wf
single-bags-equal
single-eclass-val
single-valued-bag
single-valued-bag-append
single-valued-bag-combine
single-valued-bag-empty
single-valued-bag-filter
single-valued-bag-hd
single-valued-bag-if-le1
single-valued-bag-is-list
single-valued-bag-is-rep
single-valued-bag-list
single-valued-bag-map
single-valued-bag-single
single-valued-bag-sv-list
single-valued-bag_wf
single-valued-base-classrel
single-valued-base-loc-classrel
single-valued-class-except
single-valued-class-except_wf
single-valued-class-implies-hdf
single-valued-classrel
single-valued-classrel-all
single-valued-classrel-all-implies-bag
single-valued-classrel-all_wf
single-valued-classrel-implies-bag
single-valued-classrel_wf
single-valued-list
single-valued-list-sv-bag
single-valued-list_wf
single-valued-on-header
single-valued-on-header_wf
single-valued-sub-bag
single_iseg
sorted-by-single
sq_stable__single-valued-iterated-classrel
sq_stable__single-valued-prior-iterated-classrel
sv-bag-only-single
sv-bag-tail-single-valued
sv_bag_only_single_lemma
ws_single_lemma

---

SINGLE1

prev top next

fpf-cap-single1
fpf-val-single1

---

SINGLE2

prev top next

fpf-compatible-single2
lnk-decl-compatible-single2

---

SINGLES

prev top next

fpf-compatible-singles
fpf-compatible-singles-iff
fpf-compatible-singles-trivial

---

SINGLETON

prev top next

adjacent-singleton
bag-filter-singleton
bl-exists-singleton
bl-exists-singleton-top
bm_singleton
bm_singleton_wf
cut-of-singleton
es-interface-vals-singleton
f-singleton-subset
filter-singleton
filter_is_singleton
firstn_append_front_singleton
fpf-vals-singleton
from-upto-is-singleton
from-upto-singleton
fset-singleton
fset-singleton_wf
interleaving_singleton
l_contains_singleton
l_disjoint_singleton
last_append_singleton
last_append_singleton_sq
last_singleton
last_singleton_append
length-singleton
list_append_singleton_ind
loc-on-path-singleton
longest-prefix-singleton
mapfilter-singleton
member-fset-singleton
member_singleton
no_repeats_singleton
no_repeats_singleton_uiff
p-first-singleton
pairwise-singleton
per-class-base-singleton
per-class-subtype-singleton
permutation-singleton
reverse_singleton
set-sig-singleton
set-sig-singleton_wf
singleton
singleton-nat-missing
singleton-nat-missing-prop
singleton-nat-missing_wf
singleton-orbit
singleton-subtype
singleton-type
singleton-type-function
singleton-type-one
singleton-type-product
singleton-type-top
singleton-type-void-domain
singleton-type_wf
singleton_before
singleton_properties
singleton_support_sum
singleton_wf
strong-subtype-iff-preserves-singleton
sub-bag-singleton-left

---

SINGLETON2

prev top next

filter_is_singleton2
l_disjoint_singleton2
last_singleton2

---

SINGLETONS

prev top next

equipollent-singletons

---

SIZE

prev top next

C_DVALUEp_size
C_DVALUEp_size_wf
C_DVALUEpco_size
C_DVALUEpco_size_wf
C_LVALUE_size
C_LVALUE_size_wf
C_LVALUEco_size
C_LVALUEco_size_wf
C_TYPE_size
C_TYPE_size_wf
C_TYPEco_size
C_TYPEco_size_wf
MMTree_size
MMTree_size_wf
MMTreeco_size
MMTreeco_size_wf
MultiTree_size
MultiTree_size_wf
MultiTreeco_size
MultiTreeco_size_wf
RankEx1_size
RankEx1_size_wf
RankEx1co_size
RankEx1co_size_wf
RankEx2_size
RankEx2_size_wf
RankEx2co_size
RankEx2co_size_wf
RankEx4_size
RankEx4_size_wf
RankEx4co_size
RankEx4co_size_wf
Sudoku-size
Sudoku-size_wf
bag-combine-size
bag-combine-size-bound
bag-combine-size-bound2
bag-member-iff-size
bag-member-size
bag-no-repeats-le-bag-size
bag-remove-size
bag-remove-size-member-no-repeats
bag-rep-size-restrict
bag-restrict-size-bound
bag-size
bag-size-append
bag-size-as-summation
bag-size-bag-member
bag-size-bound
bag-size-cons
bag-size-filter-member-bound
bag-size-is-zero
bag-size-map
bag-size-one
bag-size-partition
bag-size-rep
bag-size-restrict
bag-size-zero
bag-size_wf
bag-subtract-size
bag_size_cons_lemma
bag_size_empty_lemma
bag_size_single_lemma
binary-tree_size
binary-tree_size_wf
binary-treeco_size
binary-treeco_size_wf
binary_map_size
binary_map_size_wf
binary_mapco_size
binary_mapco_size_wf
bool-size
bool-size_wf
consensus-rcv-crosses-size
empty-bag-iff-size
equal-bag-size-le1
formula_size
formula_size_wf
formulaco_size
formulaco_size_wf
fset-size
fset-size-add
fset-size-empty
fset-size-one
fset-size-remove
fset-size-union
fset-size_wf
l_intersection-size
l_tree_size
l_tree_size_wf
l_treeco_size
l_treeco_size_wf
lg-size
lg-size-add
lg-size-append
lg-size-deliver-msg
lg-size-deliver-msg-general
lg-size-map
lg-size-nil
lg-size-remove
lg-size-wf_dag
lg-size_wf
loop-class-memory-size
loop-class-memory-size-prior
loop-class-memory-size-zero
mFOL_size
mFOL_size_wf
mFOLco_size
mFOLco_size_wf
member-eclass-iff-size
mset_size
mset_size_wf
non_neg_mset_size
null-bag-size
orbit-size-divides-order
pi_term_size
pi_term_size_wf
pi_termco_size
pi_termco_size_wf
sub-bag-size
tree_size
tree_size_wf
treeco_size
treeco_size_wf

---

SIZE1

prev top next

member-eclass-iff-size1

---

SKIP

prev top next

skip-first-class
skip-first-class-is-empty-if-first
skip-first-class-property
skip-first-class-property-iff
skip-first-class_wf

---

SKOLEM

prev top next

strong-continuity2-implies-weak-skolem
strong-continuity2-implies-weak-skolem-cantor
strong-continuity2-implies-weak-skolem-cantor-nat

---

SLICE

prev top next

fps-add-slice
fps-geometric-slice
fps-geometric-slice_lemma
fps-geometric-slice_lemma2
fps-mul-slice
fps-neg-slice
fps-one-slice
fps-pascal-slice
fps-scalar-mul-slice
fps-set-to-one-slice
fps-single-slice
fps-slice
fps-slice-slice
fps-slice-ucont
fps-slice_wf
fps-sub-slice
fps-zero-slice

---

SLICE1

prev top next

fps-geometric-slice1

---

SLLN

prev top next

slln-lemma1
slln-lemma2
slln-lemma3
slln-lemma4

---

SLOT

prev top next

pv11_p1_init_slot_num
pv11_p1_init_slot_num_wf

---

SLOW

prev top next

assert-slow-int-palindrome-test
slow-int-palindrome-test
slow-int-palindrome-test_wf

---

SLOWFIB

prev top next

slowfib

---

SMALL

prev top next

small-category
small-category
small-category-subtype
small-category-subtype
small-category_wf
small-category_wf
small-ctrex1
small-ctrex1-bounds
small-ctrex1_wf
small-reciprocal-real
small-reciprocal-real-ext
small-reciprocal-rneq-zero
small-sparse-rep
small-sparse-rep-ext

---

SMALLBAG

prev top next

smallbag-subtype-list

---

SND

prev top next

cc-snd
cc-snd-csm-adjoin
cc-snd_wf
church-snd
church-snd_wf
church_snd_lemma
csm-adjoin-fst-snd
csm-ap-cubical-snd
cubical-snd
cubical-snd-pair
cubical-snd_wf
hdf-until-ap-snd
is-list-if-has-value-rec-snd
new_23_sig_vote_with_ballot_and_id-if-snd
new_23_sig_vote_with_ballot_and_id-snd
norm-snd
norm-snd_wf
sigma-box-snd
sigma-box-snd_wf

---

SO

prev top next

so_apply1
so_apply2
so_apply3
so_apply4
so_apply5
so_apply6
so_apply7
so_apply8
so_lambda1
so_lambda2
so_lambda3
so_lambda4
so_lambda5
so_lambda6
so_lambda7
so_lambda8
so_lambda9

---

SOLUTION

prev top next

awf-solution
awf-solution_wf
last-solution
last-solution_wf
unique-corec-solution

---

SOLVES

prev top next

solves-information-flow
solves-information-flow_wf

---

SOME

prev top next

class-caused-by-some
class-caused-by-some_wf
decidable__cs-inning-committable-some
decidable__cs-inning-committed-some
fset-some
fset-some-iff
fset-some-iff2
fset-some_wf

---

SOME1

prev top next

cs-inning-committable-some1
cs-inning-committed-some1

---

SOME2

prev top next

cs-inning-committable-some2

---

SORT

prev top next

comparison-sort
comparison-sort-permutation
comparison-sort_wf

---

SORTED

prev top next

es-closed-open-interval-sorted-by
es-interface-predecessors-sorted-by-le
es-interface-predecessors-sorted-by-locl
es-interval-sorted-by
from-upto-sorted
frs-increasing-sorted-by
frs-non-dec-sorted-by
insert-by-sorted-by
insert-combine-sorted-by
insert-no-combine-sorted-by
iseg-sorted-by
l-ordered-is-sorted-by
l_before-sorted-by
member-iseg-sorted-by
permutation-sorted-by-unique
s-insert-sorted
sorted
sorted-by
sorted-by-append
sorted-by-append1
sorted-by-cons
sorted-by-eq-rels
sorted-by-exists
sorted-by-exists2
sorted-by-filter
sorted-by-nil
sorted-by-no_repeats
sorted-by-reverse
sorted-by-single
sorted-by-strict-no_repeats
sorted-by-strict-unique
sorted-by-unique
sorted-by_wf
sorted-by_wf_nil
sorted-cons
sorted-filter
sorted-merge
sorted_wf
sq_stable__sorted-by
strict-sorted
sublist-sorted-by

---

SOURCE

prev top next

assert-lg-is-source
lg-acyclic-has-source
lg-is-source
lg-is-source-wf_dag
lg-is-source_wf
message-class-source
message-class-source_wf

---

SP

prev top next

grp_lt_is_sp_of_leq_a
refl_cl_sp_cancel
refl_cl_sp_le_rel
rel_le_refl_cl_sp
rel_le_sp_refl_cl
set_lt_is_sp_of_leq
set_lt_is_sp_of_leq_a
sp-join
sp-join-assoc
sp-join-bottom
sp-join-com
sp-join-idemp
sp-join-is-bottom
sp-join-meet-distrib
sp-join-top
sp-join_wf
sp-le
sp-le-bottom
sp-le-top
sp-le_transitivity
sp-le_weakening
sp-le_wf
sp-lub
sp-lub-is-bottom
sp-lub-is-top
sp-lub-is-top1
sp-lub-property
sp-lub_wf
sp-lub_wf1
sp-meet
sp-meet-assoc
sp-meet-bottom
sp-meet-com
sp-meet-idemp
sp-meet-is-top
sp-meet-join-distrib
sp-meet-top
sp-meet_wf
sp_refl_cl_cancel
sp_refl_cl_le_rel
strong-continuity-implies1-sp
strong-continuity-test-sp
strong-continuity-test-sp_wf
trans_imp_sp_trans
trans_imp_sp_trans_a
trans_imp_sp_trans_b
utrans_imp_sp_utrans
utrans_imp_sp_utrans_a
utrans_imp_sp_utrans_b
xxtrans_imp_sp_trans

---

SPACE

prev top next

finite-prob-space
finite-prob-space_wf

---

SPARSE

prev top next

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

---

SPAWNFIRSTSCOUT

prev top next

pv11_p1_SpawnFirstScout
pv11_p1_SpawnFirstScout-program
pv11_p1_SpawnFirstScout-program_wf
pv11_p1_SpawnFirstScout_wf

---

SPEC

prev top next

A-shift-spec
A-shift-spec_wf
A-shift-upto-spec
A-shift-upto-spec_wf
EventML spec properties
EventML spec properties
EventML spec properties
EventML spec properties
alt-swap-spec
alt-swap-spec_wf2
header-type-spec
header-type-spec_wf
state-machine-spec
state-machine-spec_wf
subtype_rel_header-type-spec

---

SPEC71

prev top next

Paxos-spec8-spec71

---

SPEC710

prev top next

Paxos-spec8-spec710

---

SPEC711

prev top next

Paxos-spec8-spec711

---

SPEC712

prev top next

Paxos-spec8-spec712

---

SPEC713

prev top next

Paxos-spec8-spec713

---

SPEC714

prev top next

Paxos-spec8-spec714

---

SPEC715

prev top next

Paxos-spec8-spec715

---

SPEC716

prev top next

Paxos-spec8-spec716

---

SPEC717

prev top next

Paxos-spec8-spec717

---

SPEC72

prev top next

Paxos-spec8-spec72

---

SPEC73

prev top next

Paxos-spec8-spec73

---

SPEC74

prev top next

Paxos-spec8-spec74

---

SPEC75

prev top next

Paxos-spec8-spec75

---

SPEC76

prev top next

Paxos-spec8-spec76

---

SPEC77

prev top next

Paxos-spec8-spec77

---

SPEC78

prev top next

Paxos-spec8-spec78

---

SPEC79

prev top next

Paxos-spec8-spec79

---

SPEC8

prev top next

Paxos-spec8-spec71
Paxos-spec8-spec710
Paxos-spec8-spec711
Paxos-spec8-spec712
Paxos-spec8-spec713
Paxos-spec8-spec714
Paxos-spec8-spec715
Paxos-spec8-spec716
Paxos-spec8-spec717
Paxos-spec8-spec72
Paxos-spec8-spec73
Paxos-spec8-spec74
Paxos-spec8-spec75
Paxos-spec8-spec76
Paxos-spec8-spec77
Paxos-spec8-spec78
Paxos-spec8-spec79

---

SPECIAL

prev top next

add-mul-special
special-fix
special-mod4-decomp
special-mod4-decomp-unique
special-mod4-decomp_wf

---

SPECIFICATION

prev top next

------ CLK - specification ------
------ OARcast - specification ------
------ new_23_sig - specification ------
------ nysiad - specification ------
------ pv11_p1 - specification ------
simple-swap-specification
simple-swap-specification_wf

---

SPLIT

prev top next

Q-R-glues-split
Q-R-glues-trivial-split
accum_split
accum_split_inverse
accum_split_iseg
accum_split_iseg2
accum_split_one_one
accum_split_prefix
accum_split_prefix2
accum_split_wf
append-tuple-split-tuple
append_split
bag-filter-split
bag-restrict-split
bag-split
bag-summation-split
combinations-split
eo-forward-split-before
equipollent-split
es-before-split-last
es-le-before-split-last
filter-split-length
fpf-split
from-upto-split
funtype-split
increasing_split
index-split
index-split-permutation
index-split_property
index-split_wf
int-prod-split
interface-predecessors-split
interleaved_split
interleaving_split
iseg_product-split
itop_split
list_accum_split
list_split
list_split_inverse
list_split_iseg
list_split_iseg2
list_split_one_one
list_split_prefix
list_split_wf
mk_applies_split
mon_itop_split
mon_itop_split_el
order_split
partition-split-cons
partition-split-cons-mesh
permr_upto_split
permutation-split
power-sum-split
rmaximum-split
rng_sum_split
rsum-split
rsum-split-first
rsum-split-last
rsum-split-shift
shorten-tuple-split-tuple
split-at-first
split-at-first-gap
split-at-first-gap-ext
split-at-first-rel
split-by-indices
split-gap
split-gap_wf
split-maximal-consecutive
split-maximal-consecutive_wf
split-tuple
split-tuple-append-tuple
split-tuple_wf
split_rel_last
split_tail
split_tail_correct
split_tail_lemma
split_tail_max
split_tail_rel
split_tail_trivial
split_tail_wf
sum_split
sum_split_first
uorder_split
weighted-sum-split
xxorder_split

---

SPLIT1

prev top next

sum_split1

---

SPLIT2

prev top next

append_split2
permutation-split2

---

SPLITS

prev top next

bag-member-splits
bag-splits
bag-splits-permutation
bag-splits-permutation1
bag-splits_wf
bag-splits_wf_list

---

SPLITTING

prev top next

is_accum_splitting
is_accum_splitting_wf
is_list_splitting
is_list_splitting_wf
sq_stable__is_accum_splitting
sq_stable__is_list_splitting

---

SPREAD

prev top next

AF-spread-law
AF-spread-law_wf
Spread
Spread-family
Spread-family-ext
Spread-family_wf
Spread_wf
apply-spread
bag-member-spread
bag-member-spread-to-pi
band_spread_left
callbyvalueall-seq-spread
callbyvalueall_seq-spread
cbva_seq-spread
decide-spread
decide-spread-sq1
decide-spread-sq2
fun_thru_spread
hd-map-spread
lifting-add-spread-1
lifting-add-spread-2
lifting-apply-spread
lifting-callbyvalue-spread
lifting-callbyvalueall-spread
lifting-decide-spread
lifting-isaxiom-spread
lifting-ispair-spread
lifting-null-spread
lifting-spread-callbyvalue
lifting-spread-callbyvalueall
lifting-spread-concat
lifting-spread-decide
lifting-spread-isaxiom
lifting-spread-ispair
lifting-spread-less
lifting-spread-spread
lifting-strict-spread
locknd-spread
locknd-spread_wf
locknd-spread_wf2
map-spread
name_eq_spread
normalization-spread
pi12-sqle-spread
push-spread-into-ifthenelse
simple-cbva-seq-spread
spread def
spread-append
spread-axiom-sqequal-bottom
spread-bag-append
spread-decide
spread-ext
spread-ifthenelse
spread-ispair-spread
spread-spread
spread-sq-pi12
spread-sqle-pi12
spread-trivial
spread-wf
spread_cons_lemma
spread_to_pi12
spread_wf
sqequal-spread-cbva-weak
strict4-spread
strictness-spread
stuck-spread
sub-spread
sub-spread-transitive
sub-spread_wf
test-spread-normalize

---

SPREAD0

prev top next

callbyvalueall-seq-spread0
callbyvalueall_seq-spread0
simple-cbva-seq-spread0

---

SPREAD1

prev top next

normalization-callbyvalueall-spread1

---

SPREAD2

prev top next

map_reduce_spread2_to_reduce
normalization-callbyvalueall-spread2
normalization-spread2

---

SPREAD3

prev top next

normalization-spread3
spread3

---

SPREAD4

prev top next

normalization-spread4
spread4

---

SPREAD5

prev top next

spread5

---

SPREAD6

prev top next

spread6

---

SPREAD7

prev top next

spread7

---

SPREAD8

prev top next

spread8

---

SPSR

prev top next

spsr

---

SQ

prev top next

Accum-classrel-Memory-sq
Accum-loc-classrel-Memory-sq
IdLnk_sq
Id_sq
Kind_sq
Knd_sq
add-remove-fresh-sq
append_assoc_sq
append_firstn_lastn_sq
append_nil_sq
assert-bag-null-sq
atom1_sq
atom2_sq
atom_eq_sq_normalize
atom_sq
bag-member-iff-sq-list-member
bag-member-sq-list-member
base_sq
baseof_sq
bl-rev-exists-sq
bool_sq
can-apply-compose-sq
cbv-concat-sq
encryption-key_sq
eo-forward-base-classfun-res-sq
eo-forward-base-classfun-sq
equal-nil-sq-nil
es-cut-induction-sq-stable
es-interface-predecessors-step-sq
es-interface-val-restrict-sq
es-interval-less-sq
es-local-pred-cases-sq
es-prior-interface-cases-sq
eval-list-sq
eval_list_sq
filter-sq
filter_append_sq
firstn_last_mklist_sq
firstn_last_sq
fpf-join-ap-sq
fpf-join-cap-sq
fpf-join-dom-sq
fpf-join-empty-sq
fpf-single-dom-sq
fun_exp_add-sq
fun_exp_add1-sq
fun_exp_add_sq
fun_exp_add_sq_again
global-eo-E-sq
hd-append-sq
iflift_sq_1
int-decr-map-type-member-sq-stable
int-palindrome-test-sq
int-sq-root
int_sq
is-filter-image-sq
isaxiom-implies-sq
ispair-implies-sq
last-lemma-sq
last_append_singleton_sq
length-if-co-list-sq
length-map-sq
length-zero-implies-sq-nil
list-eo-E-sq
list_accum_pair-sq
listid-sq
map_append_sq
map_functionality_wrt_sq
nameset_sq
nameset_sq
nat_sq
no-member-sq-nil
norm-list_wf_sq
norm-pair_wf_sq
not-name_eq-implies-sq-bfalse
p-fun-exp-add-sq
p-fun-exp-add1-sq
pair-sq-axiom-wf
polymorphic-id-unique-sq
ranked-eo-E-sq
rec-case-map-sq
reject_cons_hd_sq
reject_cons_tl_sq
remove-repeats-append-sq
reverse_append_sq
sdata_sq
select_cons_tl_sq
spread-sq-pi12
sq-all-large
sq-all-large-and
sq-all-large_wf
sq-decider
sq-decider-atom-deq
sq-decider-list-deq
sq-decider-name-deq
sq-decider_wf
sq-id-fun
sq-id-fun_wf
sq_exists
sq_exists_subtype_rel
sq_exists_wf
sq_or
sq_or_functionality_wrt_iff
sq_or_simp
sq_or_sq_or
sq_or_squash
sq_or_squash2
sq_or_squash3
sq_or_wf
sq_stable
sq_stable_Kan-A-filler
sq_stable__W-bars
sq_stable__action_p
sq_stable__alg_hom_p
sq_stable__all
sq_stable__and
sq_stable__anti_sym
sq_stable__assert
sq_stable__assoc
sq_stable__bag-member
sq_stable__bag-no-repeats
sq_stable__bilinear
sq_stable__bilinear_p
sq_stable__cancel
sq_stable__classrel
sq_stable__colinear
sq_stable__comm
sq_stable__connex
sq_stable__coprime
sq_stable__correct_proof
sq_stable__dist_1op_2op_lr
sq_stable__encodes-msg-type
sq_stable__eo_axioms
sq_stable__eqfun_p
sq_stable__eqmod
sq_stable__equal
sq_stable__equal-info-body
sq_stable__es-causl
sq_stable__es-causle
sq_stable__eu-between
sq_stable__eu-between-eq
sq_stable__eu-congruent
sq_stable__ex_int_seg_ap
sq_stable__ex_int_upper
sq_stable__ex_int_upper_ap
sq_stable__ex_nat
sq_stable__fpf-sub
sq_stable__from_stable
sq_stable__frs-non-dec
sq_stable__fseg
sq_stable__fun_thru_1op
sq_stable__fun_thru_2op
sq_stable__group_p
sq_stable__grp_leq
sq_stable__has-es-info-type
sq_stable__has-value
sq_stable__has-value
sq_stable__has-valueall
sq_stable__i-member
sq_stable__icompact
sq_stable__ideal_p
sq_stable__ident
sq_stable__iff
sq_stable__implies
sq_stable__inject
sq_stable__integ_dom_p
sq_stable__inv_funs
sq_stable__inverse
sq_stable__is-list-if-has-value-fun
sq_stable__is-partition-choice
sq_stable__is_accum_splitting
sq_stable__is_list_splitting
sq_stable__iseg
sq_stable__iterated_classrel
sq_stable__l-ordered
sq_stable__l_all
sq_stable__l_member
sq_stable__l_subset
sq_stable__le
sq_stable__less_than
sq_stable__module_hom_p
sq_stable__monoid_hom_p
sq_stable__monoid_p
sq_stable__monot
sq_stable__mprime
sq_stable__no-classrel-in-interval
sq_stable__no-prior-classrel
sq_stable__no_repeats
sq_stable__not
sq_stable__pairwise
sq_stable__partitions
sq_stable__prime_ideal
sq_stable__refl
sq_stable__regular-int-seq
sq_stable__rel_path
sq_stable__req
sq_stable__rleq
sq_stable__rless
sq_stable__rnonneg
sq_stable__single-valued-iterated-classrel
sq_stable__single-valued-prior-iterated-classrel
sq_stable__sorted-by
sq_stable__sq_or
sq_stable__sqequal
sq_stable__sqle
sq_stable__squash
sq_stable__strong-subtype
sq_stable__sublist
sq_stable__sublist-rec
sq_stable__subtype_rel
sq_stable__sym
sq_stable__t-sqle
sq_stable__trans
sq_stable__uall
sq_stable__uanti_sym
sq_stable__uconnex
sq_stable__uiff
sq_stable__uimplies
sq_stable__uni_sat
sq_stable__urefl
sq_stable__usym
sq_stable__utrans
sq_stable__value-type
sq_stable__valueall-type
sq_stable_and_decidable
sq_stable_and_left_false
sq_stable_eu-seg-congruent
sq_stable_euclidean-axioms
sq_stable_fills-A-open-box
sq_stable_from_decidable
sq_stable_iff_stable
sq_stable_iff_uimplies
sq_stable_sqle
sq_stable_uniform-Kan-A-filler
sq_stable_wf
sq_type
squash_sq_or
sub-bag-list-if-bag-no-repeats-sq
subtype_base_sq
test-sq-lift3
test-sq-stuff

---

SQ1

prev top next

decide-spread-sq1

---

SQ2

prev top next

decide-spread-sq2
fun_exp_add1-sq2
select_cons_tl_sq2

---

SQEQ

prev top next

list_eq_imp_sqeq
not-btrue-sqeq-bfalse
not-btrue-sqeq-bottom
not-inl-sqeq-inr
not_id_sqeq_bottom

---

SQEQFF

prev top next

sqeqff_to_assert

---

SQEQTT

prev top next

sqeqtt_to_assert

---

SQEQUAL

prev top next

absval-sqequal-imax
bag-count-sqequal
band-sqequal-inl
bool_cases_sqequal
bottom-sqequal-fix-id
cWO-induction-extract-sqequal
cbv_sqequal
cbva_seq-sqequal-n
eq_atom_eq_false_elim_sqequal
eq_atom_eq_true_elim_sqequal
eq_int_eq_false_elim_sqequal
eq_int_eq_true_elim_sqequal
es-fix-sqequal
es-interface-predecessors-sqequal
evalall-sqequal
ifthenelse_sqequal
isaxiom-sqequal
islist-append-nil-sqequal-islist
ispair-sqequal
l-ind-sqequal-list_ind
less_sqequal
lt_int_eq_false_elim_sqequal
lt_int_eq_true_elim_sqequal
mk_lambdas-sqequal-n
mk_lambdas-sqequal-n2
not_all_sqequal
not_zero_sqequal_one
simple-cbva-seq-sqequal-n
spread-axiom-sqequal-bottom
sq_stable__sqequal
sqequal def
sqequal-append-cbva-weak2
sqequal-append-cbva-weak3
sqequal-ff-to-assert
sqequal-fix-lemma1
sqequal-induction-test1
sqequal-list_accum
sqequal-list_accum-list_ind
sqequal-list_ind
sqequal-nil
sqequal-spread-cbva-weak
sqequal-tt-to-assert
sqequal-wf-base
sqequal_n def
sqequal_n-wf
sqequal_n_add
sqequal_n_wf
sqequal_zero
sum_functionality_wrt_sqequal

---

SQEQUAL0

prev top next

cbv-sqequal0
cbva-sqequal0

---

SQEQUAL1

prev top next

hdf-sqequal1

---

SQEQUAL2

prev top next

evalall-sqequal2
hdf-sqequal2
hdf-sqequal2-cbva
hdf-sqequal2-weak

---

SQEQUAL3

prev top next

hdf-sqequal3
hdf-sqequal3-cbva

---

SQEQUAL4

prev top next

hdf-sqequal4

---

SQEQUAL6

prev top next

hdf-sqequal6
hdf-sqequal6-1
hdf-sqequal6-2

---

SQEQUAL7

prev top next

hdf-sqequal7

---

SQEQUAL8

prev top next

hdf-sqequal8
hdf-sqequal8-2
hdf-sqequal8-3
hdf-sqequal8-4

---

SQEQUAL9

prev top next

hdf-sqequal9

---

SQEQUALIFFSQLE

prev top next

sqequalIffSqle

---

SQEQUALN

prev top next

sqequaln_sqlen
sqequaln_symm
sqlen_sqequaln

---

SQLE

prev top next

append-nil-sqle
bottom-sqle
callbyvalueall-single-sqle
cbv_sqle
cbv_sqle_2
eval_list-sqle-append-nil
evalall-append-sqle
evalall-sqle
exception-sqle-is-exception
ifthenelse_sqle
int_eq-sqle-lemma1
int_eq-sqle-lemma2
less_sqle
not-bfalse-sqle-btrue
not-btrue-sqle-bfalse
not-btrue-sqle-bottom
not-id-sqle-bottom
pi12-sqle-spread
rev-append-property-top-sqle
spread-sqle-pi12
sq_stable__sqle
sq_stable__t-sqle
sq_stable_sqle
sqle def
sqle-append-nil-if-has-value4
sqle-list_accum
sqle-list_accum-list_ind
sqle-list_ind
sqle-list_ind-list_accum
sqle-wf
sqle_n def
sqle_n-wf
sqle_n_subtype_rel
sqle_n_wf
sqle_trans
sqle_wf_base
t-sqle
t-sqle-apply
t-sqle-apply-dependent
t-sqle-base
t-sqle-subtype
t-sqle_reflexive
t-sqle_wf
zero-add-sqle

---

SQLE2

prev top next

callbyvalueall-single-sqle2

---

SQLEN

prev top next

sqequaln_sqlen
sqlen_sqequaln

---

SQNTYPE

prev top next

sqntype def
sqntype_wf

---

SQNTYPE0

prev top next

sqntype0

---

SQRT

prev top next

int-sqrt-ext
integer-sqrt
integer-sqrt-bin-search
integer-sqrt-ext
integer-sqrt-newton
integer-sqrt-newton-ext
integer-sqrt-xover

---

SQTYPE

prev top next

subtype_partial_sqtype_base

---

SQTYPE1

prev top next

test_sqtype1

---

SQUARE

prev top next

absval_square
cat-square-commutes
cat-square-commutes
cat-square-commutes-sym
cat-square-commutes-sym
cat-square-commutes_wf
cat-square-commutes_wf
groupoid-square-commutes-iff
groupoid-square-commutes-iff
groupoid-square-commutes-iff2
groupoid-square-commutes-iff2
map-square-board
map-square-board-cell
map-square-board_wf
same-face-square-commutes
same-face-square-commutes2
square-board
square-board-subtype
square-board_wf
square-iff-isqrt
square-nonneg
square_non_neg

---

SQUARE1

prev top next

groupoid-square1
groupoid-square1
groupoid-square1_wf
groupoid-square1_wf

---

SQUARE2

prev top next

groupoid-square2
groupoid-square2
groupoid-square2_wf
groupoid-square2_wf

---

SQUARED

prev top next

absval_squared
equipollent-nat-squared
expectation-rv-add-squared
real-vec-norm-squared
rsqrt_squared
sign-squared

---

SQUASH

prev top next

b_all-squash-exists-bag
b_all-squash-exists-bag2
b_all-squash-exists-list
bag_to_squash_list
decidable__squash
equiv_rel_squash
es-causle-retraction-squash
global-order-compat-squash-invariant
global-order-pairwise-compat-squash-invariant
l_all-squash-exists-list
map-sig-map-squash
no-excluded-middle-squash
not_squash
quotient-squash
retraction-fun-path-squash
set-sig-set-squash
sq_or_squash
sq_stable__squash
squash
squash-assert
squash-bag-member
squash-causal-invariant
squash-causal-invariant_wf
squash-classrel
squash-exists-is-union-squash
squash-iterated_classrel
squash-list-exists
squash-per-class
squash-product
squash-test
squash-union-is-union-squash
squash_and
squash_elim
squash_equal
squash_false
squash_functionality_wrt_iff
squash_functionality_wrt_implies
squash_functionality_wrt_uiff
squash_not
squash_sq_or
squash_squash
squash_thru_equiv_rel
squash_thru_implies_dec
squash_thru_uequiv_rel
squash_true
squash_wf
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
test-squash-simp
uimplies-iff-squash-implies
weak-joint-embedding-preserves-squash-causal-invariant

---

SQUASH2

prev top next

sq_or_squash2

---

SQUASH3

prev top next

sq_or_squash3

---

SQUEEZE

prev top next

absval-squeeze
common-limit-squeeze
common-limit-squeeze-ext

---

SRC

prev top next

assert-has-src
has-src
has-src_wf
src_vlnk_lemma

---

ST

prev top next

Comm-st
Comm-st_wf
st-atom
st-atom-encrypt
st-atom_wf
st-atoms-distinct
st-atoms-distinct_wf
st-data
st-data_wf
st-decrypt
st-decrypt_wf
st-encrypt
st-encrypt_wf
st-key
st-key-match
st-key-match_wf
st-key_wf
st-length
st-length-encrypt
st-length_wf
st-lookup
st-lookup-distinct
st-lookup-outl
st-lookup-property
st-lookup_wf
st-next
st-next_wf
st-ptr
st-ptr-wf2
st-ptr_wf
st_anti_sym
st_anti_sym_wf

---

STABLE

prev top next

bar-val-stable
consensus-ts4-archived-stable
consensus-ts4-inning-committed-stable
consensus-ts4-passed-stable
cs-inning-committed-single-stable
es-cut-induction-sq-stable
es-knows-stable
int-decr-map-type-member-sq-stable
not-not-sig-to-W-implies-stable
sq_stable
sq_stable_Kan-A-filler
sq_stable__W-bars
sq_stable__action_p
sq_stable__alg_hom_p
sq_stable__all
sq_stable__and
sq_stable__anti_sym
sq_stable__assert
sq_stable__assoc
sq_stable__bag-member
sq_stable__bag-no-repeats
sq_stable__bilinear
sq_stable__bilinear_p
sq_stable__cancel
sq_stable__classrel
sq_stable__colinear
sq_stable__comm
sq_stable__connex
sq_stable__coprime
sq_stable__correct_proof
sq_stable__dist_1op_2op_lr
sq_stable__encodes-msg-type
sq_stable__eo_axioms
sq_stable__eqfun_p
sq_stable__eqmod
sq_stable__equal
sq_stable__equal-info-body
sq_stable__es-causl
sq_stable__es-causle
sq_stable__eu-between
sq_stable__eu-between-eq
sq_stable__eu-congruent
sq_stable__ex_int_seg_ap
sq_stable__ex_int_upper
sq_stable__ex_int_upper_ap
sq_stable__ex_nat
sq_stable__fpf-sub
sq_stable__from_stable
sq_stable__frs-non-dec
sq_stable__fseg
sq_stable__fun_thru_1op
sq_stable__fun_thru_2op
sq_stable__group_p
sq_stable__grp_leq
sq_stable__has-es-info-type
sq_stable__has-value
sq_stable__has-value
sq_stable__has-valueall
sq_stable__i-member
sq_stable__icompact
sq_stable__ideal_p
sq_stable__ident
sq_stable__iff
sq_stable__implies
sq_stable__inject
sq_stable__integ_dom_p
sq_stable__inv_funs
sq_stable__inverse
sq_stable__is-list-if-has-value-fun
sq_stable__is-partition-choice
sq_stable__is_accum_splitting
sq_stable__is_list_splitting
sq_stable__iseg
sq_stable__iterated_classrel
sq_stable__l-ordered
sq_stable__l_all
sq_stable__l_member
sq_stable__l_subset
sq_stable__le
sq_stable__less_than
sq_stable__module_hom_p
sq_stable__monoid_hom_p
sq_stable__monoid_p
sq_stable__monot
sq_stable__mprime
sq_stable__no-classrel-in-interval
sq_stable__no-prior-classrel
sq_stable__no_repeats
sq_stable__not
sq_stable__pairwise
sq_stable__partitions
sq_stable__prime_ideal
sq_stable__refl
sq_stable__regular-int-seq
sq_stable__rel_path
sq_stable__req
sq_stable__rleq
sq_stable__rless
sq_stable__rnonneg
sq_stable__single-valued-iterated-classrel
sq_stable__single-valued-prior-iterated-classrel
sq_stable__sorted-by
sq_stable__sq_or
sq_stable__sqequal
sq_stable__sqle
sq_stable__squash
sq_stable__strong-subtype
sq_stable__sublist
sq_stable__sublist-rec
sq_stable__subtype_rel
sq_stable__sym
sq_stable__t-sqle
sq_stable__trans
sq_stable__uall
sq_stable__uanti_sym
sq_stable__uconnex
sq_stable__uiff
sq_stable__uimplies
sq_stable__uni_sat
sq_stable__urefl
sq_stable__usym
sq_stable__utrans
sq_stable__value-type
sq_stable__valueall-type
sq_stable_and_decidable
sq_stable_and_left_false
sq_stable_eu-seg-congruent
sq_stable_euclidean-axioms
sq_stable_fills-A-open-box
sq_stable_from_decidable
sq_stable_iff_stable
sq_stable_iff_uimplies
sq_stable_sqle
sq_stable_uniform-Kan-A-filler
sq_stable_wf
stable
stable__colinear
stable__eu-between
stable__eu-between-eq
stable__eu-congruent
stable__from_decidable
stable__function_equal
stable__not
stable_eu-between-eq
stable_point-eq
stable_wf
ts-stable
ts-stable-rel
ts-stable-rel_wf
ts-stable-star
ts-stable_wf
ts-transitive-stable
xmiddle-implies-stable

---

STAMPS

prev top next

stamps-example
stamps-example-ext

---

STAMPS35

prev top next

stamps35
stamps35_wf

---

STANDARD

prev top next

standard-ds
standard-ds_wf

---

STAR

prev top next

cond_rel_star_equiv
cond_rel_star_monotone
cond_rel_star_monotonic
preserved_by_star
rel-plus-rel-star
rel-preserving-star
rel-preserving-star-reachable
rel-star-iff-rel-plus
rel-star-iff-rel-plus-or
rel-star-rel-plus
rel-star-rel-plus2
rel-star-rel-plus3
rel_inverse_star
rel_rel_star
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
star-append
star-append-iff
star-append_wf
ts-stable-star

---

START

prev top next

lookup_before_start
lookup_before_start_a
new_23_sig_voter_start
new_23_sig_voter_start_unique
rng_lookup_before_start

---

STARTING

prev top next

not-self-starting
not-self-starting_wf

---

STATE

prev top next

Comm-state
Comm-state_wf
Memory-loc-class-is-prior-State-loc-comb
State-class
State-class-es-sv
State-class-es-sv1
State-class-single-val
State-class-single-val0
State-class-top
State-class_wf
State-classrel
State-classrel2
State-comb
State-comb-classrel
State-comb-classrel-class
State-comb-classrel-mem
State-comb-classrel-mem2
State-comb-classrel-mem3
State-comb-classrel-single-val
State-comb-classrel2
State-comb-es-sv
State-comb-es-sv1
State-comb-exists
State-comb-exists-iff
State-comb-fun-eq
State-comb-fun-eq2
State-comb-functional
State-comb-invariant
State-comb-invariant-or
State-comb-invariant-sv
State-comb-mem
State-comb-mem2
State-comb-progress
State-comb-single-val
State-comb-single-val0
State-comb-top
State-comb-total
State-comb-trans-refl
State-comb-trans1
State-comb-trans2
State-comb_wf
State-loc-comb
State-loc-comb-classrel
State-loc-comb-classrel-mem
State-loc-comb-classrel-mem2
State-loc-comb-classrel-mem3
State-loc-comb-classrel-non-loc
State-loc-comb-classrel-single-val
State-loc-comb-classrel2
State-loc-comb-exists
State-loc-comb-fun-eq
State-loc-comb-fun-eq-non-loc
State-loc-comb-fun-eq2
State-loc-comb-functional
State-loc-comb-invariant
State-loc-comb-invariant-or
State-loc-comb-invariant-sv
State-loc-comb-invariant-sv1
State-loc-comb-invariant-sv2
State-loc-comb-is-loop-class-state
State-loc-comb-non-empty
State-loc-comb-non-empty-iff
State-loc-comb-progress
State-loc-comb-single-val
State-loc-comb-single-val0
State-loc-comb-total
State-loc-comb-trans-refl
State-loc-comb-trans1
State-loc-comb_wf
State1-state-class1
State2-state-class2
State3-state-class3
consensus-accum-num-state
consensus-accum-num-state_wf
consensus-accum-state
consensus-accum-state_wf
cp-state-type
cp-state-type_wf
cs-events-to-state
cs-events-to-state_wf
cs-possible-state-reachable
csm-state
csm-state_wf
eclass-state
eclass-state-classrel
eclass-state-program
eclass-state-program_wf
eclass-state_wf
es-interface-local-state
es-interface-local-state-cases
es-interface-local-state-prior
es-interface-local-state_wf
es-interface-state
es-interface-state_wf
es-local-prior-state
es-local-prior-state-induction
es-local-prior-state_wf
fix_wf_dataflow_w_state
flow-state-compression
flow-state-compression_wf
hdf-state
hdf-state-base
hdf-state-base2-2
hdf-state-base2-3
hdf-state-base3-2
hdf-state-base3-3
hdf-state-base4-2
hdf-state-base4-3
hdf-state-single-val
hdf-state-single-val_wf
hdf-state-transformation2
hdf-state_wf
hdf-with-state-pair-left-axiom
local-prior-state-accumulate
loop-class-memory-is-prior-loop-class-state
loop-class-state
loop-class-state-classrel
loop-class-state-exists
loop-class-state-fun-eq
loop-class-state-functional
loop-class-state-prior
loop-class-state-program
loop-class-state-program-wf-hdf
loop-class-state-program_wf
loop-class-state-single-val
loop-class-state-total
loop-class-state_wf
ma-state
ma-state-subtype
ma-state-subtype2
ma-state_wf
new_23_sig_quorum_state_eq1
new_23_sig_quorum_state_eq1-forward
new_23_sig_quorum_state_fun_eq
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
pv11_p1_acc_state_from_p2a
pv11_p1_acc_state_from_p2a_fun
pv11_p1_acc_state_fun_eq
pv11_p1_acc_state_fun_eq2
pv11_p1_commander_state_from_p2bs
pv11_p1_commander_state_fun_eq
pv11_p1_ldr_fun_state_adopted_pred
pv11_p1_ldr_fun_state_propose_pred
pv11_p1_ldr_state_adopted_pred
pv11_p1_ldr_state_eq
pv11_p1_ldr_state_eq2
pv11_p1_ldr_state_fun_eq
pv11_p1_ldr_state_propose_pred
pv11_p1_scout_state_from_p1bs
pv11_p1_scout_state_fun_eq
pv11_p1_scout_state_subset_pvals
rec-dataflow-state
rec-dataflow-state_wf
rec-process_wf_pi_simple_state
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-prior-state
run-prior-state-property
run-prior-state_wf
state-class1
state-class1-exists
state-class1-fun-eq
state-class1-prior
state-class1-program
state-class1-program-wf-hdf
state-class1-program_wf
state-class1-state1-classrel
state-class1-state1-eq
state-class1_wf
state-class2
state-class2-fun-eq
state-class2-inv
state-class2-program
state-class2-program_wf
state-class2_wf
state-class3
state-class3-fun-eq
state-class3-program
state-class3-program_wf
state-class3_wf
state-class4
state-class4-program
state-class4-program_wf
state-class4_wf
state-class5
state-class5-program
state-class5-program_wf
state-class5_wf
state-machine-spec
state-machine-spec_wf
state-var-allowed
state-var-read-allowed

---

STATE1

prev top next

State1
State1-exists
State1-functional
State1-loc-exists
State1-prior
State1-state-class1
State1_wf
consensus-state1
consensus-state1_wf
hdf-state1-single-val
hdf-state1-single-val_wf
state-class1-state1-classrel
state-class1-state1-eq

---

STATE2

prev top next

State2
State2-exists
State2-functional
State2-loc-exists
State2-state-class2
State2_wf
consensus-state2
consensus-state2-cases
consensus-state2_wf

---

STATE3

prev top next

State3
State3-exists
State3-loc-exists
State3-prc
State3-state-class3
State3_wf
consensus-state3
consensus-state3-cases
consensus-state3-unequal
consensus-state3_wf

---

STATE4

prev top next

consensus-state4
consensus-state4-cases
consensus-state4-exclusive-cases
consensus-state4-subtype
consensus-state4_wf

---

STATE5

prev top next

consensus-state5
consensus-state5_wf

---

STATE6

prev top next

consensus-state6
consensus-state6_wf

---

STATELESS

prev top next

iterate-stateless-dataflow
stateless-dataflow
stateless-dataflow_wf
stateless_dataflow_ap_lemma

---

STATES

prev top next

adjacent-run-states

---

STD

prev top next

std-component-property
std-components-property
std-env
std-env-reliable
std-env_wf
std-initial
std-initial-property
std-initial_wf
std-ma
std-ma-with-omissions
std-ma-with-omissions_wf
std-ma_wf

---

STDEO

prev top next

stdEO
stdEO-E-property
stdEO-causal
stdEO-eq-E
stdEO-event-history
stdEO-le
stdEO-locl
stdEO_wf

---

STEP

prev top next

aa_step_3n
combinations-step
consensus-rel-add-knowledge-step
consensus-rel-add-knowledge-step_wf
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
cs-inning-committable-step
cs-ref-map-step
cut-order-step
cw-step
cw-step_wf
do-elimination-step
elimination-step
es-fix-step
es-interface-predecessors-general-step
es-interface-predecessors-step
es-interface-predecessors-step-sq
ex-evd-proof-step
exp_step
fix-step
full-evd-proof-step
fun-connected-step
fun-connected-step-back
hdf-single-val-step
hdf-single-val-step_wf
is-list-approx-step
mul-initial-seg-step
pcw-final-step
pcw-final-step_wf
pcw-step
pcw-step-agree
pcw-step-agree_wf
pcw-step_wf
rnexp_step
run-event-step
run-event-step-positive
run-event-step_wf
run-lt-step-less
run-pred-step-less
step-function
step-function-example
step-function-example-member
step-function-example-monotone
step-function-example_wf
step-function_wf
strict-fun-connected-step

---

STEP1

prev top next

new_23_sig_progress-step1
new_23_sig_progress2-step1

---

STEP10

prev top next

new_23_sig_progress-step10

---

STEP2

prev top next

new_23_sig_progress-step2
new_23_sig_progress2-step2

---

STEP3

prev top next

new_23_sig_progress-step3

---

STEP4

prev top next

new_23_sig_progress-step4

---

STEP5

prev top next

new_23_sig_progress-step5

---

STEP6

prev top next

new_23_sig_progress-step6

---

STEP7

prev top next

new_23_sig_progress-step7

---

STEP8

prev top next

new_23_sig_progress-step8
new_23_sig_progress-step8-v2
new_23_sig_progress-step8-v3

---

STEP9

prev top next

new_23_sig_progress-step9
new_23_sig_progress-step9-v2
new_23_sig_progress-step9-v3

---

STEPREL

prev top next

pcw-steprel
pcw-steprel_wf

---

STEPS

prev top next

pcw-consistent-steps
pcw-consistent-steps_wf

---

STH

prev top next

sth-axioms
sth-es
sth-es_wf

---

STOREP

prev top next

C_STOREp
C_STOREp-welltyped
C_STOREp-welltyped_wf
C_STOREp_wf

---

STR

prev top next

member-nat-to-str
nat-to-str
nat-to-str_wf
str-to-nat
str-to-nat-plus
str-to-nat-plus-property
str-to-nat-plus_wf
str-to-nat-to-str
str-to-nat_wf

---

STR1

prev top next

str1-to-nat
str1-to-nat_wf

---

STREAM

prev top next

Process-stream
Process-stream_wf
const-stream
const-stream_wf
constant-data-stream
data-stream
data-stream-append
data-stream-cons
data-stream_wf
data_stream_nil_lemma
firstn-data-stream
hd-stream-zip
iterate-fun-stream
iterate-fun-stream_wf
last-data-stream
length-data-stream
map-iterate-fun-stream
mk-stream
mk-stream_wf
nth-stream-map
nth-stream-zip
null-data-stream
select-data-stream
stream
stream-bijection
stream-coinduction
stream-decomp
stream-ext
stream-extensionality
stream-lex
stream-lex-iff
stream-lex-monotonic
stream-lex_transitivity
stream-lex_transitivity-proof2
stream-lex_wf
stream-map
stream-map_wf
stream-pointwise
stream-pointwise-iff
stream-pointwise_transitivity
stream-pointwise_wf
stream-subtype
stream-zip
stream-zip_wf
stream-zip_wf2
stream_subtype_base
stream_wf
tl-stream-zip

---

STREAMLESS

prev top next

markov-streamless-function
markov-streamless-iff
markov-streamless-iff-not-not-enum
markov-streamless-product
streamless
streamless-dec-equal
streamless-implies-not-not-enum
streamless_wf

---

STRIC

prev top next

CLK_stric_inc

---

STRICT

prev top next

CLK_strict_inc2
append-strict-1
apply-strict-fun
bounded-above-strict
cbv-reduce-strict
concat-lifting-1-strict
concat-lifting-2-strict
concat-lifting-3-strict
concat-lifting-loc-1-strict
concat-lifting-loc-2-strict
concat-lifting-loc-3-strict
concat-lifting-strict
concat-strict
eo-strict-forward
eo-strict-forward-E
eo-strict-forward-E-member
eo-strict-forward-E-subtype
eo-strict-forward-E-subtype2
eo-strict-forward-base-E
eo-strict-forward-before
eo-strict-forward-ble
eo-strict-forward-bless
eo-strict-forward-eq
eo-strict-forward-first
eo-strict-forward-info
eo-strict-forward-le
eo-strict-forward-less
eo-strict-forward-loc
eo-strict-forward-locl
eo-strict-forward-pred
eo-strict-forward-pred?
eo-strict-forward_wf
equal-eo-strict-forward-E
fix-strict
fix_strict_diverge
imax-list-strict-lb
imax_strict_lb
imax_strict_ub
is-strict-fun
l-strict
l-strict_wf
lifting-1-strict
lifting-2-strict
lifting-3-strict
lifting-gen-strict
lifting-strict-atom_eq
lifting-strict-atom_eq1
lifting-strict-atom_eq2
lifting-strict-callbyvalue
lifting-strict-callbyvalueall
lifting-strict-decide
lifting-strict-ifthenelse
lifting-strict-int_eq
lifting-strict-isatom
lifting-strict-isatom2
lifting-strict-isaxiom
lifting-strict-isint
lifting-strict-islambda
lifting-strict-ispair
lifting-strict-less
lifting-strict-spread
list-strict
list-strict_wf
member-eo-strict-forward-E
merge-strict-exists
new_23_sig_rounds_strict_inc
null-strict
r-strict-bound-property
rmax_strict_lb
rmax_strict_ub
rmin_strict_lb
rmin_strict_ub
sorted-by-strict-no_repeats
sorted-by-strict-unique
strict
strict-bag-function
strict-bag-function_wf
strict-fun
strict-fun
strict-fun-connected
strict-fun-connected-induction
strict-fun-connected-step
strict-fun-connected_irreflexivity
strict-fun-connected_transitivity1
strict-fun-connected_transitivity2
strict-fun-connected_transitivity3
strict-fun-connected_wf
strict-fun_wf
strict-majority
strict-majority-or-first
strict-majority-or-first_wf
strict-majority-or-max
strict-majority-or-max-property
strict-majority-or-max_wf
strict-majority-property
strict-majority_functionality
strict-majority_wf
strict-sorted
strict-strict1
strict-strict4
strict-upper-bound
strict-upper-bound_functionality
strict-upper-bound_wf
strict-upper-bounds
strict-upper-bounds_wf
strict_part
strict_part_irrefl
strict_part_wf
strict_wf

---

STRICT1

prev top next

strict-strict1
strict1
strict1-strict4
strict1_wf

---

STRICT2

prev top next

strict2
strict2_wf

---

STRICT4

prev top next

strict-strict4
strict1-strict4
strict4
strict4-append
strict4-bag-combine
strict4-callbyvalueall
strict4-concat
strict4-concat-map
strict4-evalall
strict4-ispair
strict4-map
strict4-spread
strict4_wf

---

STRICT5

prev top next

strict5

---

STRICTLY

prev top next

implies-strictly-increasing-seq
strictly-decreasing-on-interval
strictly-decreasing-on-interval_wf
strictly-increasing-on-interval
strictly-increasing-on-interval_wf
strictly-increasing-seq
strictly-increasing-seq-add
strictly-increasing-seq_wf

---

STRICTNESS

prev top next

strictness-add-left
strictness-add-right
strictness-apply
strictness-atom1_eq-left
strictness-atom1_eq-right
strictness-atom2_eq-left
strictness-atom2_eq-right
strictness-atom_eq-left
strictness-atom_eq-right
strictness-band-left
strictness-callbyvalue
strictness-callbyvalueall
strictness-concat
strictness-decide
strictness-divide-left
strictness-divide-right
strictness-fix
strictness-ifthenelse
strictness-int_eq-left
strictness-int_eq-right
strictness-isatom
strictness-isatom1
strictness-isatom2
strictness-isaxiom
strictness-isinl
strictness-isinr
strictness-islambda
strictness-ispair
strictness-isr
strictness-less-left
strictness-less-right
strictness-minus
strictness-multiply-left
strictness-multiply-right
strictness-remainder-left
strictness-remainder-right
strictness-spread
strictness-subtract-left
strictness-subtract-right

---

STRONG

prev top next

as_strong
as_strong_transitivity
as_strong_wf
bag-member-strong-subtype
bar_recursion_wf_strong
basic_strong_bar_induction
es-E-interface-strong-subtype
es-E-interfaces-strong-subtype
filter_strong_safety
nat-strong-overt-implies-Markov
no_repeats-strong-subtype
oalist_strong-subtype
permutation-strong-subtype
sq_stable__strong-subtype
strong-continuity-implies1
strong-continuity-implies1-sp
strong-continuity-implies2
strong-continuity-implies3
strong-continuity-implies4
strong-continuity-test
strong-continuity-test-prop1
strong-continuity-test-prop2
strong-continuity-test-prop3
strong-continuity-test-sp
strong-continuity-test-sp_wf
strong-continuity-test-unroll
strong-continuity-test_wf
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-continuity2-no-inner-squash
strong-continuity2-no-inner-squash-cantor
strong-continuity2-no-inner-squash-cantor2
strong-continuity2-no-inner-squash-cantor3
strong-continuity2-no-inner-squash-cantor4
strong-continuity2-no-inner-squash-cantor5
strong-continuity2-no-inner-squash-unique
strong-continuous-b-union
strong-continuous-dep-isect
strong-continuous-depproduct
strong-continuous-function
strong-continuous-isect2
strong-continuous-list
strong-continuous-product
strong-continuous-set
strong-continuous-tag-case
strong-continuous-union
strong-fun-connected-induction
strong-interface-fifo
strong-interface-fifo-order-preserving
strong-interface-fifo_wf
strong-law-of-large-numbers
strong-message-constraint
strong-message-constraint-bag
strong-message-constraint-bag_wf
strong-message-constraint-implies-message-constraint
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
strong-message-constraint_wf
strong-overt
strong-overt_wf
strong-subtype
strong-subtype-b-union
strong-subtype-b-union-better
strong-subtype-bag
strong-subtype-bar
strong-subtype-dep-product
strong-subtype-deq
strong-subtype-deq-subtype
strong-subtype-eo-forward-E
strong-subtype-eq1
strong-subtype-eq2
strong-subtype-eq3
strong-subtype-eq4
strong-subtype-equal
strong-subtype-equal-lists
strong-subtype-ext-equal
strong-subtype-fset-member-type
strong-subtype-iff-preserves-singleton
strong-subtype-implies
strong-subtype-isect-base
strong-subtype-l_member
strong-subtype-l_member-type
strong-subtype-list
strong-subtype-member
strong-subtype-product
strong-subtype-self
strong-subtype-set
strong-subtype-set1
strong-subtype-set2
strong-subtype-set3
strong-subtype-union
strong-subtype-union-base
strong-subtype-void
strong-subtype_functionality
strong-subtype_transitivity
strong-subtype_wf
strong-subtype_witness
strong-type-continuous
strong-type-continuous_wf
strong_before
strong_before_wf
strong_safety
strong_safety_safety
strong_safety_wf

---

STRONG1

prev top next

weak-continuity-implies-strong1

---

STRONGER

prev top next

exp-positive-stronger

---

STRONGLY

prev top next

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

---

STRONGWELLFOUNDED

prev top next

rel_plus_strongwellfounded
strongwellfounded
strongwellfounded_rel_exp
strongwellfounded_wf

---

STRONGWF

prev top next

strongwf-implies
strongwf-monotone

---

STRUCT

prev top next

C_Struct
C_Struct-fields
C_Struct-fields_wf
C_Struct?
C_Struct?_wf
C_Struct_vs_DVALp
C_Struct_wf
DVp_Struct
DVp_Struct-lbls
DVp_Struct-lbls_wf
DVp_Struct-struct
DVp_Struct-struct_wf
DVp_Struct?
DVp_Struct?_wf
DVp_Struct_wf
discrete_struct
discrete_struct_wf

---

STRUCTURE

prev top next

Kan structure on Id_A a b
defining the Kan structure
euclidean-structure
euclidean-structure_wf
security-event-structure
security-event-structure_wf
theorems about Kan structure

---

STUCK

prev top next

stuck-decide
stuck-spread
test_stuck_apply

---

STUFF

prev top next

test-sq-stuff

---

STUMP

prev top next

stump
stump'
stump'-inductive
stump'_property
stump'_wf
stump-bars
stump-monotone
stump-nil
stump_wf

---

SUB

prev top next

Msg_sub
Msg_sub_wf
assert-deq-sub-bag
bag-filter-is-sub-bag
base-class-program-wf-sub
continuous-sub
corec-sub-family
decidable__sub-bag
deq-sub-bag
deq-sub-bag_wf
derivative-sub
empty-sub-bag
es-decl-sets-sub
es-decl-sets-sub_wf
fpf-cap-subtype_functionality_wrt_sub
fpf-cap_functionality_wrt_sub
fpf-empty-sub
fpf-join-sub
fpf-single-sub-reflexive
fpf-sub
fpf-sub-compatible-left
fpf-sub-compatible-right
fpf-sub-functionality
fpf-sub-functionality2
fpf-sub-join
fpf-sub-join-left
fpf-sub-join-left2
fpf-sub-join-right
fpf-sub-join-right2
fpf-sub-join-symmetry
fpf-sub-reflexive
fpf-sub-set
fpf-sub-val
fpf-sub-val2
fpf-sub-val3
fpf-sub_functionality
fpf-sub_functionality2
fpf-sub_transitivity
fpf-sub_weakening
fpf-sub_wf
fpf-sub_witness
fps-compose-sub
fps-elim-x-sub
fps-set-to-one-sub
fps-sub
fps-sub-slice
fps-sub_wf
fun_exp_add1_sub
member-sub-bags
member-sub-mset
messages-delivered-with-omissions-sub
messages-delivered-with-omissions-sub_wf
msgs-interface-with-omissions-sub
msgs-interface-with-omissions-sub_wf
pnot-sub
pnot-sub_wf
real-vec-sub
real-vec-sub_wf
single-valued-sub-bag
sq_stable__fpf-sub
sub-bag
sub-bag-admissable
sub-bag-append-left
sub-bag-append-left2
sub-bag-cancel-right
sub-bag-combine
sub-bag-empty
sub-bag-equal
sub-bag-filter
sub-bag-filter2
sub-bag-filter3
sub-bag-iff
sub-bag-list-if-bag-no-repeats-sq
sub-bag-lub
sub-bag-map-equal
sub-bag-mapfilter-implies
sub-bag-member
sub-bag-no-repeats-iff
sub-bag-of-bag-rep
sub-bag-remove-if
sub-bag-remove-repeats-if-no-repeats
sub-bag-rep
sub-bag-singleton-left
sub-bag-size
sub-bag-union-of-list
sub-bag_antisymmetry
sub-bag_transitivity
sub-bag_weakening
sub-bag_wf
sub-bags
sub-bags-no-repeats
sub-bags_wf
sub-corec-family
sub-equality
sub-es-pred
sub-es-pred_wf
sub-family
sub-family_transitivity
sub-family_wf
sub-isect-family
sub-mset
sub-mset-contains
sub-mset-map
sub-mset_transitivity
sub-mset_weakening
sub-mset_wf
sub-spread
sub-spread-transitive
sub-spread_wf
sub-system
sub-system-append
sub-system_transitivity
sub-system_weakening
sub-system_wf
sub_functionality_wrt_le
verify-class-program-wf-sub

---

SUB2

prev top next

fpf-cap-subtype_functionality_wrt_sub2
fpf-join-sub2

---

SUBBAG

prev top next

mapfilter-subbag

---

SUBGAME

prev top next

subgame
subgame_wf

---

SUBGRP

prev top next

norm_subgrp
norm_subgrp_wf
subgrp_p
subgrp_p_wf

---

SUBINTERVAL

prev top next

compact-subinterval
continuous_functionality_wrt_subinterval
derivative_functionality_wrt_subinterval
es-subinterval
i-approx-is-subinterval
rcc-subinterval
subinterval
subinterval_transitivity
subinterval_wf

---

SUBLEVELSET

prev top next

sublevelset
sublevelset-closed
sublevelset_wf

---

SUBLIST

prev top next

adjacent-sublist
adjacent-to-same-sublist
comb_for_sublist_wf
cons_sublist_cons
cons_sublist_nil
decidable__sublist-rec
disjoint_sublists_sublist
es-interface-sublist
es-interface-sublist_wf
filter_is_sublist
filter_sublist
interleaving_sublist
iseg_is_sublist
l-ordered-sublist
l_all_sublist
l_before_sublist
length_sublist
member_iff_sublist
member_sublist
nil-sublist
nil_sublist
no_repeats-sublist
pairwise-sublist
proper_sublist_length
range_sublist
remove-repeats-fun-sublist
sq_stable__sublist
sq_stable__sublist-rec
sublist
sublist*
sublist*_filter
sublist*_wf
sublist-if-no_repeats
sublist-rec
sublist-rec-iff-sublist
sublist-rec-nil
sublist-rec-nil-iff
sublist-rec_wf
sublist-reverse
sublist-same-last
sublist-sorted-by
sublist_accum
sublist_antisymmetry
sublist_append
sublist_append1
sublist_append2
sublist_append_front
sublist_filter
sublist_filter_2
sublist_filter_set_type
sublist_interleaved
sublist_iseg
sublist_map
sublist_map_inj
sublist_nil
sublist_occurence
sublist_occurence_wf
sublist_pair
sublist_tl
sublist_tl2
sublist_transitivity
sublist_weakening
sublist_wf
tl_sublist

---

SUBLIST2

prev top next

adjacent-to-same-sublist2

---

SUBLISTS

prev top next

append_overlapping_sublists
disjoint_sublists
disjoint_sublists_sublist
disjoint_sublists_wf
disjoint_sublists_witness
length_disjoint_sublists

---

SUBSEQUENCE

prev top next

subsequence-converges

---

SUBSET

prev top next

cut-subset-cut
decidable__f-subset
equipollent-nat-decidable-subset
equipollent-nat-subset
eqv_mod_subset
eqv_mod_subset_is_eqv
eqv_mod_subset_wf
f-singleton-subset
f-subset
f-subset-union
f-subset_antisymmetry
f-subset_transitivity
f-subset_weakening
f-subset_wf
f-union-subset
imax-list-subset
l-union-subset
l_subset
l_subset-l_contains
l_subset_append
l_subset_cons
l_subset_cons_same
l_subset_nil_left
l_subset_nil_left_true
l_subset_pos_length
l_subset_refl
l_subset_right_cons_trivial
l_subset_transitivity
l_subset_wf
list-diff-subset
member_list_accum_l_subset
norm_subset_p
norm_subset_p_wf
p_subset
p_subset_wf
pv11_p1_scout_state_subset_pvals
sq_stable__l_subset
subset-map

---

SUBSET2

prev top next

member_list_accum_l_subset2

---

SUBST

prev top next

mFOL-subst
mFOL-subst-abstract
mFOL-subst_wf
name-subst
name-subst_wf
pi-rank-pi-simple-subst
pi-rank-pi-simple-subst-aux
pi-simple-subst
pi-simple-subst-aux
pi-simple-subst-aux_wf
pi-simple-subst_wf
pi-subst
pi-subst-aux
pi-subst-aux_wf
pi-subst_wf

---

SUBSUME

prev top next

list-equal-subsume

---

SUBTRACT

prev top next

bag-subtract
bag-subtract-append
bag-subtract-member-if-no-repeats
bag-subtract-no-repeats
bag-subtract-size
bag-subtract_wf
divides_subtract
equipollent-general-subtract-one
equipollent-subtract
equipollent-subtract-one
gcd_subtract
left_mul_subtract_distrib
strictness-subtract-left
strictness-subtract-right
subtract
subtract-elim
subtract-is-less
subtract-wf-bar
subtract-wf-bar-int
subtract-wf-partial
subtract_functionality_wrt_eqmod
subtract_wf

---

SUBTRACT2

prev top next

equipollent-subtract2

---

SUBTREE

prev top next

l_tree_node-left_subtree
l_tree_node-left_subtree_wf
l_tree_node-right_subtree
l_tree_node-right_subtree_wf

---

SUBTREES

prev top next

wfd-subtrees
wfd-subtrees_wf

---

SUBTYPE

prev top next

C_TYPE_subtype_base
Com-subtype
W_subtype
abdgrp_subtype_abgrp
abgrp_subtype_grp
abmonoid_subtype_iabmonoid
abmonoid_subtype_mon
algebra_subtype_algebra_sig
algebra_subtype_module
array_subtype
atom1_subtype_base
atom2_subtype_base
atom_subtype_base
atomic-values_subtype_base
awf-subtype
awf-system-subtype
bag-eq-subtype
bag-member-strong-subtype
bag-member-subtype
bag-member-subtype-2
bag-no-repeats-subtype
bag-subtype
bag-subtype-list
bar-base-subtype
bar-base_subtype
baseof_subtype
baseof_subtype_base
bool_subtype_base
cdrng_subtype_crng
co-list-subtype
consensus-state4-subtype
continuous-abs-subtype
corec-subtype
corec-subtype-corec
corec-subtype-corec2
corec_subtype
corec_subtype_base
crng_subtype_rng
cube-set-map-subtype
dataflow_subtype
decidable-exists-int_seg-subtype
decidable-subtype
dep-eclass_subtype_rel
dep-eclass_subtype_rel2
dep-isect-subtype
deq_subtype
disjoint-quotient_subtype
dmon_subtype_mon
double_isect_subtype_rel
drng_subtype_rng
eclass_subtype_rel
eo-forward-E-subtype
eo-forward-le-subtype
eo-strict-forward-E-subtype
equal-in-subtype-implies
equal_functionality_wrt_subtype_rel
equal_functionality_wrt_subtype_rel2
equal_subtype
equipollent-subtype
equiv_rel_subtype
es-E-interface-conditional-subtype
es-E-interface-conditional-subtype_rel
es-E-interface-strong-subtype
es-E-interface-subtype
es-E-interface-subtype_rel
es-E-interface-subtype_rel-implies
es-E-interfaces-strong-subtype
es-E-subtype
es-interface-predecessors-equal-subtype
es-interface-set-subtype
es-interface-subtype_rel
es-interface-subtype_rel2
event-ordering+-subtype
event-ordering+_subtype
event-ordering+_subtype_mem
event_system-level-subtype
extd-nameset_subtype
extd-nameset_subtype_base
extd-nameset_subtype_int
finite-subtype
fpf-cap-join-subtype
fpf-cap-subtype_functionality
fpf-cap-subtype_functionality_wrt_sub
fpf-cap-subtype_functionality_wrt_sub2
fpf-cap-void-subtype
fpf-trivial-subtype-set
fpf-trivial-subtype-top
fpf-union-compatible-subtype
free-from-atom-bool-subtype
free-from-atom-subtype
fset-subtype
fulpRunType-subtype
function-subtype-top
grp_car_subtype
grp_subtype_grp_sig
grp_subtype_igrp
grp_subtype_mon
has-es-info-type-subtype
hdataflow_subtype
iabmonoid_subtype_imon
id-fun-subtype
imon_subtype_grp_sig
int-subtype-rationals
int_seg_subtype
int_seg_subtype-nat
int_subtype_base
int_upper_subtype_int_upper
int_upper_subtype_nat
interface-at-subtype
interface-part-subtype
is-above-subtype
is-list-if-has-value-rec-subtype-unit
isect-subtype-1
isect-subtype-2
isect2-b-union-subtype
isect2_functionality_wrt_subtype_rel
isect2_subtype_rel
isect2_subtype_rel2
isect2_subtype_rel3
isect_subtype
isect_subtype_base
isect_subtype_rel
isect_subtype_rel_trivial
iseg-subtype
l_all_subtype
l_before_filter_subtype
l_member_in_subtype
l_member_subtype
list-eq-subtype
list-subtype
list-subtype-bag
list-subtype-power-type
list_subtype_base
local-simulation-E-subtype
loset_subtype_dset
loset_subtype_poset
loset_subtype_poset_sig
ma-state-subtype
ma-valtype-subtype
member-interface-predecessors-subtype
mk_deq-subtype
mon_subtype_grp_sig
name-morph-domain_subtype
name-morph_subtype
name-morph_subtype_domain
name-morph_subtype_remove1
named-path-subtype
nameset_subtype
nameset_subtype
nameset_subtype_base
nameset_subtype_base
nameset_subtype_cons_diff
nameset_subtype_cons_diff
nameset_subtype_extd-nameset
nat_plus_subtype_nat
nat_subtype
no_repeats-strong-subtype
no_repeats-subtype
not-quotient-function-subtype
not_subtype_rel
nsub2_subtype_extd-nameset
oal_hgp_subtype_oal_grp
oalist_strong-subtype
oalist_subtype
oalist_subtype_oal_mon
ocgrp_subtype_abdgrp
ocgrp_subtype_abgrp
ocgrp_subtype_ocmon
ocmon_subtype_abdmonoid
omon_subtype
oob-subtype
or-quotient-true-subtype
partition-choice-subtype
per-class-subtype-singleton
per-partial-subtype
per-value_subtype_base
permutation-strong-subtype
permutation-subtype
poset-cat-arrow_subtype
poset-cat-ob_subtype
poset_subtype_qoset
power-type-subtype-list
process-subtype
product-subtype-co-list
product_subtype_base
product_subtype_list
qoset_subtype_dset
quot_ring_car_subtype
quotient-dep-function-subtype
quotient-function-subtype
record+_subtype_rel
rev_subtype_rel
rev_subtype_rel_weakening
rev_subtype_rel_wf
rfun_subtype
rng_subtype_rng_sig
sdata_subtype_base
ses-thread-subtype
set_subtype_base
simple-product_subtype_base
singleton-subtype
small-category-subtype
small-category-subtype
smallbag-subtype-list
sq_exists_subtype_rel
sq_stable__strong-subtype
sq_stable__subtype_rel
sqle_n_subtype_rel
square-board-subtype
stream-subtype
stream_subtype_base
strong-subtype
strong-subtype-b-union
strong-subtype-b-union-better
strong-subtype-bag
strong-subtype-bar
strong-subtype-dep-product
strong-subtype-deq
strong-subtype-deq-subtype
strong-subtype-eo-forward-E
strong-subtype-eq1
strong-subtype-eq2
strong-subtype-eq3
strong-subtype-eq4
strong-subtype-equal
strong-subtype-equal-lists
strong-subtype-ext-equal
strong-subtype-fset-member-type
strong-subtype-iff-preserves-singleton
strong-subtype-implies
strong-subtype-isect-base
strong-subtype-l_member
strong-subtype-l_member-type
strong-subtype-list
strong-subtype-member
strong-subtype-product
strong-subtype-self
strong-subtype-set
strong-subtype-set1
strong-subtype-set2
strong-subtype-set3
strong-subtype-union
strong-subtype-union-base
strong-subtype-void
strong-subtype_functionality
strong-subtype_transitivity
strong-subtype_wf
strong-subtype_witness
subtype
subtype-Sierpinski
subtype-add-fresh-cname
subtype-bag-empty
subtype-bag-only
subtype-corec1
subtype-corec2
subtype-deq
subtype-fpf
subtype-fpf-cap
subtype-fpf-cap-top
subtype-fpf-cap-top2
subtype-fpf-cap-void
subtype-fpf-cap-void-list
subtype-fpf-cap-void2
subtype-fpf-cap5
subtype-fpf-general
subtype-fpf-variant
subtype-fpf-void
subtype-fpf2
subtype-fpf3
subtype-iff-id-mem-fun
subtype-l_all
subtype-mono
subtype-set-hasloc
subtype-top
subtype-value-type
subtype-valueall-type
subtype_bar
subtype_bar2
subtype_barSqtype_base
subtype_base_sq
subtype_by_equality
subtype_corec
subtype_neg_polymorphism_test
subtype_partial_sqtype_base
subtype_pos_polymorphism_test
subtype_quotient
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
subtype_top
subtype_urec
t-sqle-subtype
tag-by-subtype-tag-case
tagged+_subtype_rel
tagged-true-subtype
top-subtype-function
tree_subtype
tree_subtype_base
tunion_subtype_base
tuple-type-subtype-n-tuple
type-incr-chain-subtype
uall_subtype
uimplies_subtype
union_subtype_base
unit-subtype-co-list
unit_subtype_base
unit_subtype_list
urec_subtype
urec_subtype_base

---

SUBTYPE1

prev top next

bag-eq-subtype1
cond-class-subtype1
es-E-interface-conditional-subtype1
list-eq-subtype1
uand-subtype1

---

SUBTYPE2

prev top next

bag-subtype2
co-list-subtype2
cond-class-subtype2
dep-isect-subtype2
eo-forward-E-subtype2
eo-strict-forward-E-subtype2
es-E-interface-conditional-subtype2
fpf-cap-join-subtype2
l_member_in_subtype2
l_member_subtype2
list-eq-subtype2
ma-state-subtype2
uand-subtype2

---

SUBTYPING

prev top next

eqfun_p_subtyping
equiv_rel_subtyping
subtype_rel_isect_as_subtyping_lemma
uequiv_rel_subtyping

---

SUBYPE

prev top next

rec-value_subype_base

---

SUCC

prev top next

comb_for_l_succ_wf
cons_succ
even-succ-implies-not-even
evodd-succ
evodd-succ_wf
l_succ
l_succ_wf
not-even-succ-implies-even
odd-implies-succ-two-times
search_succ

---

SUDOKU

prev top next

Sudoku
Sudoku-induction
Sudoku-size
Sudoku-size_wf
Sudoku_wf
sudoku-allowed
sudoku-allowed_wf
sudoku-cell
sudoku-cell_wf

---

SUDOKUPUZZLE

prev top next

SudokuPuzzle
SudokuPuzzle_wf

---

SUDOKUSOLUTION

prev top next

SudokuSolution
SudokuSolution_wf

---

SUM

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
absval_sum
awf_sum
awf_sum_wf
bag-sum
bag-sum-count
bag-sum-nonneg
bag-sum_wf
bag-sum_wf_nat
comb_for_mset_sum_wf
comb_for_rng_sum_wf
constant-partition-sum
continuous'-monotone-sum
continuous-series-sum
continuous-sum
destructor-sum
div_floor_mod_sum
div_rem_sum
divisor_of_sum
divisors-sum
divisors-sum_wf
double_sum
double_sum_difference
double_sum_functionality
double_sum_wf
equipollent-product-sum
equipollent-sum
equipollent-sum-zero
equipollent-union-sum
es-interface-sum
es-interface-sum-cases
es-interface-sum-le-interface
es-interface-sum-non-neg
es-interface-sum_wf
fun-series-sum
fun-series-sum_wf
gen-divisors-sum
gen-divisors-sum-int-ring
gen-divisors-sum_wf
int-bag-sum
int-bag-sum-append
int-bag-sum_wf
l_sum
l_sum-append
l_sum-lower-bound
l_sum-mapfilter
l_sum-mapfilter-upto
l_sum-mul-left
l_sum-sum
l_sum-triangle-inequality
l_sum-triangle-inequality-general
l_sum-upper-bound
l_sum-upper-bound-map
l_sum_as_accum
l_sum_as_reduce
l_sum_as_reduce_general
l_sum_cons_lemma
l_sum_filter0
l_sum_functionality_wrt_permutation
l_sum_nil_lemma
l_sum_permute
l_sum_wf
mset_count_sum
mset_for_mset_sum
mset_mem_inj_sum_lemma
mset_mem_sum
mset_sum
mset_sum_assoc
mset_sum_bor_mon_hom
mset_sum_comm
mset_sum_ident_r
mset_sum_wf
non_neg_sum
non_neg_sum-map
pair_support_double_sum
partition-refinement-sum
partition-sum
partition-sum_functionality
partition-sum_wf
power-sum
power-sum-linear
power-sum-product
power-sum-split
power-sum_functionality_wrt_eqmod
power-sum_functionality_wrt_le
power-sum_wf
rabs-Riemann-sum
reg-seq-list-add-as-l_sum
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_sum_l
rng_times_sum_r
rv-disjoint-rv-partial-sum
rv-partial-sum
rv-partial-sum-monotone
rv-partial-sum-unroll
rv-partial-sum_wf
select_concat_sum
series-sum
series-sum-linear1
series-sum-linear2
series-sum-linear3
series-sum_wf
singleton_support_sum
subtype_rel_sum
sum
sum-as-accum
sum-as-accum-filter
sum-as-accum2
sum-as-bag-accum
sum-as-primrec
sum-count-repeats
sum-equal-terms
sum-has-value
sum-ite
sum-l_sum
sum-map
sum-map-append
sum-map-append1
sum-map-cons
sum-map_wf
sum-nat
sum-nat-le
sum-nat-less
sum-partial-has-value
sum-partial-list-has-value
sum-partial-nat
sum-reindex
sum-reindex2
sum-unroll
sum-unroll-1
sum_arith
sum_arith1
sum_aux
sum_aux-as-primrec
sum_aux_wf
sum_bound
sum_constant
sum_difference
sum_functionality
sum_functionality_wrt_sqequal
sum_le
sum_linear
sum_lower_bound
sum_map_nil_lemma
sum_of_geometric_prog
sum_of_torder
sum_of_torder_wf
sum_scalar_mult
sum_split
sum_split1
sum_split_first
sum_switch
sum_wf
triangular-reciprocal-series-sum
type-functor-sum
type-functor-sum_wf
weighted-sum
weighted-sum-linear
weighted-sum-nil
weighted-sum-split
weighted-sum_wf
weighted-sum_wf2

---

SUM1

prev top next

sum1

---

SUM2

prev top next

div_rem_sum2

---

SUMDEQ

prev top next

sumdeq
sumdeq_wf

---

SUMMAND

prev top next

isolate_summand

---

SUMMARY

prev top next

summary of definitions

---

SUMMATION

prev top next

bag-double-summation
bag-size-as-summation
bag-summation
bag-summation-add
bag-summation-append
bag-summation-cons
bag-summation-constant
bag-summation-constant-int
bag-summation-empty
bag-summation-equal
bag-summation-equal-implies-all-equal
bag-summation-equal-implies-all-equal-1
bag-summation-equal2
bag-summation-filter
bag-summation-from-upto
bag-summation-hom
bag-summation-is-zero
bag-summation-linear
bag-summation-linear-right
bag-summation-linear1
bag-summation-linear1-right
bag-summation-map
bag-summation-minus
bag-summation-partition
bag-summation-partitions-primes
bag-summation-partitions-primes-general
bag-summation-product
bag-summation-reindex
bag-summation-ring-linear1
bag-summation-single
bag-summation-single-non-zero
bag-summation-single-non-zero-no-repeats
bag-summation-split
bag-summation-zero
bag-summation_functionality_wrt_le
bag-summation_functionality_wrt_le_1
bag-summation_wf
fps-restrict-summation
fps-summation
fps-summation-coeff
fps-summation_wf

---

SUMMATION2

prev top next

bag-double-summation2

---

SUMS

prev top next

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

---

SUP

prev top next

W-sup
W-sup_wf
inf-as-sup
pW-sup
pW-sup_wf
range-sup
range-sup-property
range-sup_wf
sup
sup-iff-closure
sup-range
sup-unique
sup_wf
totally-bounded-sup

---

SUPER

prev top next

super-fact
super-fact-int-prod-exp
super-fact-unroll
super-fact_wf

---

SUPERLEVELSET

prev top next

superlevelset
superlevelset-closed
superlevelset_wf

---

SUPERTYPE

prev top next

bag-no-repeats-supertype

---

SUPPORT

prev top next

class-output-member-support
class-output-support
class-output-support-no-repeats
class-output-support-no_repeats
class-output-support_wf
empty_support
fps-support
fps-support-degree-bound
fps-support_wf
pair_support
pair_support_double_sum
singleton_support_sum

---

SUPTYPE

prev top next

suptype

---

SUPTYPING

prev top next

permr_suptyping

---

SURJECT

prev top next

compact_functionality_wrt_surject
surject
surject-inverse
surject_wf

---

SURJECTION

prev top next

antecedent-surjection
antecedent-surjection_functionality_wrt_iff
antecedent-surjection_wf
evodd-enum-surjection
injection-is-surjection
surjection-cantor-finite-branching
weak-antecedent-surjection
weak-antecedent-surjection-conditional
weak-antecedent-surjection-conditional2
weak-antecedent-surjection-property
weak-antecedent-surjection_functionality_wrt_pred_equiv
weak-antecedent-surjection_wf

---

SURJECTIONS

prev top next

combine-antecedent-surjections
weak-antecedent-surjections-compose

---

SV

prev top next

Accum-class-es-sv
Accum-loc-class-es-sv
Memory-class-es-sv
Memory-class-invariant-sv
Memory-loc-class-invariant-sv
State-class-es-sv
State-comb-es-sv
State-comb-invariant-sv
State-loc-comb-invariant-sv
bag-member-sv-bag-only
bag-member-sv-list
base-headers-msg-val-es-sv
class-at-es-sv
cond-msg-body-sv-bag-only
decidable__exists-classrel-between1-sv
decidable__exists-classrel-between3-sv
decidable__exists-iterated-classrel-between3-sv
decidable__exists-last-classrel-between3-sv
decidable__exists-pred-iterated-classrel-between3-sv
disjoint-union-comb-es-sv
es-sv-class
es-sv-class-implies-single-valued-classrel
es-sv-class_wf
event_in_sv_classrel_is_in_class
memory-classrel1-sv
memory-classrel2-sv
memory-classrel3-sv
on-loc-class-es-sv
only_value_of_sv_class_in_classrel
parallel-class-es-sv
permutation-sv-list
primed-class-opt-es-sv
rec-comb-es-sv
rec-combined-class-opt-1-es-sv
rec-combined-loc-class-opt-1-es-sv
simple-comb-1-es-sv
simple-comb-2-es-sv
simple-comb-es-sv
simple-loc-comb-1-concat-es-sv
simple-loc-comb-2-concat-es-sv
simple-loc-comb-3-concat-es-sv
single-valued-bag-sv-list
single-valued-list-sv-bag
sv-bag-equals-list
sv-bag-is-bag-rep
sv-bag-is-bag-rep-lousy-proof
sv-bag-only
sv-bag-only-append
sv-bag-only-combine
sv-bag-only-filter
sv-bag-only-map
sv-bag-only-map2
sv-bag-only-single
sv-bag-only_wf
sv-bag-tail
sv-bag-tail-single-valued
sv-bag-tail_wf
sv-class
sv-class-iff
sv-class_wf
sv-classrel
sv-list-equal
sv-list-tail
sv_bag_only_single_lemma

---

SV0

prev top next

primed-class-opt-es-sv0
rec-combined-class-opt-1-es-sv0
rec-combined-loc-class-opt-1-es-sv0

---

SV1

prev top next

Accum-class-es-sv1
Accum-loc-class-es-sv1
Memory-class-es-sv1
Memory-class-invariant-sv1
Memory-loc-class-invariant-sv1
State-class-es-sv1
State-comb-es-sv1
State-loc-comb-invariant-sv1

---

SV2

prev top next

State-loc-comb-invariant-sv2

---

SWAP

prev top next

add-swap
alt-swap-spec
alt-swap-spec_wf2
comb_for_swap_wf
extend_permf_over_swap
hd_two_swap_permr
l_before_swap
map_swap
message-constraint-swap-hdr
message-constraint-swap-hdr_wf
mod_mssum_swap
mon_for_swap
mon_for_when_swap
mon_nat_op_hom_swap
mon_when_hom_swap
mon_when_swap
mset_for_swap
mul-swap
permutation-swap-first2
rng_lsum_when_swap
rng_mssum_swap
rng_mssum_when_swap
rng_when_swap
simple-swap
simple-swap-correct
simple-swap-specification
simple-swap-specification_wf
simple-swap-test
simple-swap-test2
simple-swap-test2_wf
simple-swap-test_wf
simple-swap_wf
swap
swap
swap-exists
swap-filter-filter
swap-names
swap-names_wf
swap_adjacent_decomp
swap_cons
swap_eval_1
swap_eval_2
swap_eval_3
swap_id
swap_length
swap_order_2
swap_select
swap_swap
swap_sym
swap_wf
swap_wf
triple_swap

---

SWAP2

prev top next

simple-swap2
simple-swap2_wf

---

SWAP3

prev top next

simple-swap3
simple-swap3_wf

---

SWAPPED

prev top next

swapped_select

---

SWAPS

prev top next

sym_grp_is_swaps
sym_grp_is_swaps_a

---

SWELLFND

prev top next

es-causl-swellfnd
es-causl-swellfnd-base
es-locl-swellfnd

---

SWITCH

prev top next

sum_switch
switch
switch_case
switch_default
switch_done

---

SYM

prev top next

absval_sym
anti_sym
anti_sym_functionality_wrt_iff
anti_sym_shift
anti_sym_wf
bm_compare_sym_eq
cat-square-commutes-sym
cat-square-commutes-sym
divides_anti_sym
divides_anti_sym_n
eu-between-sym
eu-congruence-identity-sym
gcd_p_sym
gcd_p_sym_a
gcd_sym
gcd_sym_nat
grp_eq_sym
inv_funs_sym
list-diff2-sym
ocmon_anti_sym
poset_anti_sym
qeq-sym
rem_sym
rem_sym_1
rem_sym_1a
rem_sym_2
sq_stable__anti_sym
sq_stable__sym
sq_stable__uanti_sym
st_anti_sym
st_anti_sym_wf
swap_sym
sym
sym_cl
sym_cl_wf
sym_functionality_wrt_iff
sym_grp
sym_grp_is_swaps
sym_grp_is_swaps_a
sym_shift
sym_wf
trans_rel_func_wrt_sym_self
trivial_sym_grp
txpose_perm_sym
uanti_sym
uanti_sym_functionality_wrt_iff
uanti_sym_shift
uanti_sym_wf
xxanti_sym
xxanti_sym_functionality_wrt_breqv
xxanti_sym_wf
xxst_anti_sym
xxst_anti_sym_wf
zero_sym_grp

---

SYMM

prev top next

disjoint-classrel-symm
sqequaln_symm

---

SYMMETRIC

prev top next

preserved_by_symmetric
rel_star_symmetric
rel_star_symmetric_2
symmetric-key
symmetric-key-atoms
symmetric-key_wf
symmetric_rel_or

---

SYMMETRIZE

prev top next

symmetrize
symmetrize_wf

---

SYMMETRIZED

prev top next

symmetrized_preorder

---

SYMMETRY

prev top next

absval-diff-symmetry
agree_on_common_symmetry
bag-partitions-symmetry
compat_symmetry
coprime_symmetry
equal_symmetry
eu-between-eq-symmetry
eu-congruent-symmetry
eu-seg-congruent_symmetry
face-compatible-symmetry
flip_symmetry
fpf-compatible-symmetry
fpf-sub-join-symmetry
fpf-union-compatible_symmetry
fps-pascal-symmetry
function-eq-symmetry
function-eq-symmetry-type-function
iff_symmetry
interleaving_symmetry
l_disjoint-symmetry
manames-overlap-case-symmetry
name_eq_symmetry
rabs-difference-symmetry
rv-disjoint-symmetry

---

SYS

prev top next

sys-antecedent
sys-antecedent-closure
sys-antecedent-filter-image
sys-antecedent-fixedpoint
sys-antecedent-retraction
sys-antecedent_wf

---

SYSTEM

prev top

System
System_wf
awf-system
awf-system-subtype
awf-system_wf
candidate-type-system
candidate-type-system_wf
event_system-level-subtype
event_system_typename
event_system_typename_wf
fix_wf_corec_system
norm-system
norm-system_wf
pRun-System-invariant
pi-system
pi-system-example
pi-system-example_wf
pi-system_wf
run-system
run-system_wf
sub-system
sub-system-append
sub-system_transitivity
sub-system_weakening
sub-system_wf
system-append
system-append_wf
system-equiv
system-equiv-implies-equal
system-equiv-is-equiv
system-equiv_wf
system-fpf
system-fpf_wf
system-function
system-function_wf
system-realizes
system-realizes_wf
system-strongly-realizes
system-strongly-realizes-and
system-strongly-realizes-and1
system-strongly-realizes_functionality
system-strongly-realizes_wf
transition-system
transition-system_wf

---