[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]
Q
top next
Comm-process-q
Comm-process-q_aux
Comm-process-q_aux_wf
Comm-process-q_wf
Comm-q
Comm-q_wf
Q-Q-glued-self-image
Q-Q-glued-to-self
Q-Q-glues-to-self
Q-Q-glues-to-self-image
Q-R-glued
Q-R-glued-composes
Q-R-glued-conditional
Q-R-glued-empty
Q-R-glued-first
Q-R-glued_wf
Q-R-glues
Q-R-glues-composes
Q-R-glues-composes2
Q-R-glues-conditional
Q-R-glues-conditional2
Q-R-glues-empty
Q-R-glues-property
Q-R-glues-split
Q-R-glues-trivial-restrict
Q-R-glues-trivial-split
Q-R-glues_functionality
Q-R-glues_wf
Q-R-pre-preserving
Q-R-pre-preserving-1-1
Q-R-pre-preserving-compose
Q-R-pre-preserving-conditional
Q-R-pre-preserving-rewrite-test
Q-R-pre-preserving_functionality_wrt_implies
Q-R-pre-preserving_wf
better-q-elim
es-pstar-q
es-pstar-q-le
es-pstar-q-partition
es-pstar-q-trivial
es-pstar-q_functionality_wrt_iff
es-pstar-q_functionality_wrt_implies
es-pstar-q_functionality_wrt_rev_implies
es-pstar-q_wf
glued-Q-R-glued
q-elim
q_le
q_le-elim
q_le_wf
QADD
prev top next
qadd
qadd-add
qadd-elim
qadd_wf
QDIV
prev top next
mk-rational-qdiv
qdiv
qdiv-int-elim
qdiv_wf
QEQ
prev top next
assert-qeq
qeq
qeq-elim
qeq-equiv
qeq-functionality
qeq-qrep
qeq-refl
qeq-sym
qeq-trans
qeq-wf
qeq_refl
qeq_wf
qeq_wf2
QINC
prev top next
bag_qinc
mset_qinc
quot_ring_car_qinc
quotient_qinc
rng_car_qinc
QINV
prev top next
qinv
qinv-elim
qinv-wf
qinv_wf
QLE
prev top next
rv-qle
rv-qle_wf
QMINUS
prev top next
qminus-minus
QMUL
prev top next
qmul
qmul-elim
qmul-mul
qmul_assoc
qmul_com
qmul_ident
qmul_wf
QOSET
prev top next
poset_subtype_qoset
qoset
qoset_lt_irrefl
qoset_lt_trans
qoset_properties
qoset_refl
qoset_subtype_dset
qoset_trans
qoset_wf
QPOSITIVE
prev top next
qpositive
qpositive-elim
qpositive_wf
QREP
prev top next
assert-is-qrep
equals-qrep
is-qrep
is-qrep_wf
qeq-qrep
qrep
qrep-coprime
qrep-denom
qrep_wf
QRNG
prev top next
type_inj_wf_for_qrng
QROUND
prev top next
qround
qround-eq
qround_wf
QSQUASH
prev top next
qsquash
qsquash_wf
QSUB
prev top next
qsub
qsub_wf
QSUM
prev top next
expectation-qsum
QUADRATIC
prev top next
quadratic-residue
quadratic-residue_functionality
quadratic-residue_wf
QUANTIFIER
prev top next
mFO-dest-quantifier
mFO-dest-quantifier_wf
QUERY
prev top next
nysiad_query
nysiad_query_wf
QUEUE
prev top next
nysiad_Queue
nysiad_Queue-program
nysiad_Queue-program_wf
nysiad_Queue_wf
nysiad_on_input_queue
nysiad_on_input_queue_wf
QUEUESTATE
prev top next
nysiad_QueueState
nysiad_QueueState-classrel
nysiad_QueueState-functional
nysiad_QueueState-program
nysiad_QueueState-program_wf
nysiad_QueueState_wf
QUEUESTATEFUN
prev top next
nysiad_QueueStateFun
nysiad_QueueStateFun_wf
QUICK
prev top next
quick-find
quick-find_wf
QUICKSORT
prev top next
cpsquicksort-quicksort
quicksort
quicksort-int
quicksort-int-iseg
quicksort-int-last
quicksort-int-length
quicksort-int-member
quicksort-int-nil
quicksort-int-null
quicksort-int-prop1
quicksort-int-single
quicksort-int_wf
quicksort_wf
QUIET
prev top next
es-quiet-until
es-quiet-until_wf
QUORUM
prev top next
new_23_sig_Quorum
new_23_sig_Quorum-program
new_23_sig_Quorum-program_wf
new_23_sig_Quorum_wf
new_23_sig_add_to_quorum
new_23_sig_add_to_quorum_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_when_quorum
new_23_sig_when_quorum_wf
QUORUMSTATE
prev top next
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_QuorumState_wf
QUORUMSTATEFUN
prev top next
new_23_sig_QuorumStateFun
new_23_sig_QuorumStateFun_wf
QUOT
prev top next
all_quot_elim
all_rng_quot_elim
all_rng_quot_elim_a
axiom-choice-00-quot
axiom-choice-0X-quot
axiom-choice-1X-quot
axiom-choice-quot
no-excluded-middle-quot-true
no-excluded-middle-quot-true1
no-excluded-middle-quot-true2
not-has-value-decidable-quot
prop-truncation-quot
quot_by_prime_ideal
quot_elim
quot_grp_car
quot_grp_car_wf
quot_grp_inv_wf
quot_rem_exists
quot_rem_exists_n
quot_ring
quot_ring_car
quot_ring_car_elim
quot_ring_car_elim_a
quot_ring_car_elim_b
quot_ring_car_qinc
quot_ring_car_subtype
quot_ring_car_wf
quot_ring_sig
quot_ring_wf
ring_quot_hom
type_inj_wf_for_quot
QUOTIENT
prev top
count-quotient
decidable__quotient_equal
disjoint-quotient_subtype
equipollent-quotient
equiv_rel-wf-quotient
equiv_rel_quotient
isect2_quotient
not-quotient-function-subtype
or-quotient-true
or-quotient-true-subtype
quotient
quotient-dep-function-subtype
quotient-function-subtype
quotient-isect-base
quotient-isect-base2
quotient-member-eq
quotient-squash
quotient-value-type
quotient-valueall-type
quotient_qinc
quotient_wf
subtype_quotient
subtype_rel_quotient
subtype_rel_quotient_trivial