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

P

top next

C_the_value_p
action_p
action_p_wf
alg_hom_p
alg_hom_p_wf
alg_p
alg_p_wf
bilinear_p
bilinear_p_wf
can-apply-p-co-filter
can-apply-p-co-restrict
can-apply-p-filter
can-apply-p-first
can-apply-p-lift
can-apply-p-restrict
comb_for_gcd_p_wf
countable-p-union
countable-p-union_wf
decidable__es-p-le-pred
decidable__es-p-local-pred
decidable__exists-es-p-le-pred
decidable__exists-es-p-local-pred
decidable__p-outcome
do-apply-p-co-filter
do-apply-p-co-restrict
do-apply-p-filter
do-apply-p-first
do-apply-p-first-disjoint
do-apply-p-lift
do-apply-p-restrict
eqfun_p
eqfun_p_shift
eqfun_p_subtyping
eqfun_p_wf
es-causl-p-locl-test
es-causl_weakening_p-locl
es-causle_weakening_p-le
es-is-interface-p-first
es-local-pred-iff-es-p-local-pred
es-p-le
es-p-le-pred
es-p-le-pred_wf
es-p-le_transitivity
es-p-le_weakening
es-p-le_weakening_eq
es-p-le_wf
es-p-local-pred
es-p-local-pred_wf
es-p-locl
es-p-locl-test
es-p-locl_transitivity
es-p-locl_transitivity1
es-p-locl_transitivity2
es-p-locl_wf
field_p
field_p_wf
gcd_p
gcd_p_eq_args
gcd_p_functionality_wrt_assoced
gcd_p_mul
gcd_p_neg_arg
gcd_p_neg_arg_2
gcd_p_neg_arg_a
gcd_p_one
gcd_p_shift
gcd_p_sym
gcd_p_sym_a
gcd_p_wf
gcd_p_zero
gcd_p_zero_rel
gcd_sat_gcd_p
group_p
group_p_wf
grp_p
grp_p_wf
ideal_p
ideal_p_wf
integ_dom_p
integ_dom_p_wf
max_ideal_p
max_ideal_p_wf
member-countable-p-union
member-p-union
module_action_p
module_eqfun_p
module_hom_p
module_hom_p_wf
mon_hom_inj_p
mon_hom_inj_p_wf
mon_hom_p_comp
mon_hom_p_id
mon_p
mon_p_wf
monoid_hom_p
monoid_hom_p_wf
monoid_p
monoid_p_wf
natural_number_wf_p-outcome
norm_subset_p
norm_subset_p_wf
normal-p-outcome
p-co-filter
p-co-filter_wf
p-co-restrict
p-co-restrict_wf
p-compose
p-compose'
p-compose'_wf
p-compose-associative
p-compose-causal-predecessor1
p-compose-id
p-compose-inject
p-compose_wf
p-conditional
p-conditional-domain
p-conditional-to-p-first
p-conditional_wf
p-disjoint
p-disjoint_wf
p-filter
p-filter_wf
p-first
p-first-append
p-first-cons
p-first-singleton
p-first_wf
p-fun-exp
p-fun-exp-add
p-fun-exp-add-sq
p-fun-exp-add1-sq
p-fun-exp-compose
p-fun-exp-injection
p-fun-exp-one
p-fun-exp_wf
p-graph
p-graph_wf
p-graph_wf2
p-id
p-id-compose
p-id_wf
p-inject
p-inject_wf
p-lift
p-lift_wf
p-measure-le
p-measure-le_wf
p-mu
p-mu-decider
p-mu-exists
p-mu_wf
p-open
p-open-measure-one
p-open-measure-one_wf
p-open-member
p-open-member_wf
p-open_wf
p-outcome
p-outcome_wf
p-restrict
p-restrict_wf
p-selector
p-selector_wf
p-union
p-union_wf
p_equiv
p_equiv_wf
p_first_nil_lemma
p_subset
p_subset_wf
prime_ideal_p
prime_ideal_p_wf
prior-classrel-p-local-pred
ring_p
ring_p_wf
rng_chom_p
rng_chom_p_wf
rng_hom_p
rng_hom_p_wf
rng_p
rng_p_wf
sq_stable__action_p
sq_stable__alg_hom_p
sq_stable__bilinear_p
sq_stable__eqfun_p
sq_stable__group_p
sq_stable__ideal_p
sq_stable__integ_dom_p
sq_stable__module_hom_p
sq_stable__monoid_hom_p
sq_stable__monoid_p
subgrp_p
subgrp_p_wf
thread-p-ordered

P1A

prev top next

pv11_p1-p1a
pv11_p1_on_p1a
pv11_p1_on_p1a_wf
pv11_p1_p1a'base
pv11_p1_p1a'base-program
pv11_p1_p1a'base-program_wf
pv11_p1_p1a'base_wf
pv11_p1_p1a'broadcast
pv11_p1_p1a'broadcast_wf

P1B

prev top next

pv11_p1-p1b
pv11_p1_on_p1b
pv11_p1_on_p1b_wf
pv11_p1_p1b'base
pv11_p1_p1b'base-program
pv11_p1_p1b'base-program_wf
pv11_p1_p1b'base_wf
pv11_p1_p1b'send
pv11_p1_p1b'send_wf
pv11_p1_valid-p1b-message
pv11_p1_valid-p1b-message_wf

P1BS

prev top next

pv11_p1_scout_state_from_p1bs

P2

prev top next

euclid-P2

P2A

prev top next

pv11_p1-p2a
pv11_p1_acc_fun_p2a
pv11_p1_acc_fun_p2a_pv
pv11_p1_acc_p2a
pv11_p1_acc_rcv_p2a
pv11_p1_acc_state_from_p2a
pv11_p1_acc_state_from_p2a_fun
pv11_p1_bnum_p2a
pv11_p1_bnum_p2a_loc
pv11_p1_decision_from_p2a
pv11_p1_decision_from_p2a_acc
pv11_p1_from-p2a
pv11_p1_from-p2a_wf
pv11_p1_on_p2a
pv11_p1_on_p2a_wf
pv11_p1_p2a'base
pv11_p1_p2a'base-program
pv11_p1_p2a'base-program_wf
pv11_p1_p2a'base_wf
pv11_p1_p2a'broadcast
pv11_p1_p2a'broadcast_wf
pv11_p1_p2a'send
pv11_p1_p2a'send_wf
pv11_p1_pvalue_from_p2a
pv11_p1_valid-p2a-message
pv11_p1_valid-p2a-message_wf

P2A2

prev top next

pv11_p1_acc_rcv_p2a2

P2B

prev top next

pv11_p1-p2b
pv11_p1_on_p2b
pv11_p1_on_p2b_wf
pv11_p1_p2b'base
pv11_p1_p2b'base-program
pv11_p1_p2b'base-program_wf
pv11_p1_p2b'base_wf
pv11_p1_p2b'send
pv11_p1_p2b'send_wf

P2BS

prev top next

pv11_p1_commander_state_from_p2bs

P3

prev top next

euclid-P3

PA

prev top next

decidable__pa-is-new-and
decidable__pa-is-sign-implies
mk-pa
mk-pa_wf
pa-is-new-and
pa-is-new-and_wf
pa-is-sign-implies
pa-is-sign-implies_wf
pa-useable
pa-useable_wf
pa-used
pa-used_wf

PAASCHE

prev top next

Paasche-alg-1
Paasche-alg-1_wf
Paasche-alg-2
Paasche-alg-2_wf
Paasche-theorem
Paasche-theorem2

PAGE55

prev top next

page55
page55'
page55-again
page55_witness

PAIR

prev top next

E-interface-pair
assert-pair-blex
assert_of_eq_pair
atom-sdata-not-pair
case_pair
church-pair
church-pair_wf
church_null_pair_lemma
code-coded-pair
code-pair
code-pair-bijection
code-pair_wf
coded-code-pair
coded-pair
coded-pair_wf
coprime-equiv-unique-pair
csm-ap-cubical-pair
cubical-fst-pair
cubical-pair
cubical-pair-eta
cubical-pair_wf
cubical-snd-pair
decide-pair-if-has-value
eq_pair
eq_pair_wf
equipollent-type-unit-pair
es-interface-pair
es-interface-pair-prior
es-interface-pair-prior-programmable
es-interface-pair-prior_wf
es-interface-pair_wf
evalall-pair
exists-pair
fpf_ap_pair_lemma
free-from-atom-pair
free-from-atom-pair-components
free-from-atom-pair-iff
has-valueall-pair
hdf-with-state-pair-left-axiom
id-sdata-not-pair
interface-pair-val
is-above-pair
is-interface-pair
is-latest-pair
is-list-if-has-value-rec-pair-bot
is-pair-prior
is_list_fun_pair_lemma
is_list_pair_lemma
ispair-pair
latest-pair
latest-pair_wf
lifting-callbyvalueall-pair
list_accum_pair
list_accum_pair-sq
list_accum_pair_wf
map-pair
map-pair-prior
non-pair-list
non-pair-listunion
norm-pair
norm-pair_wf
norm-pair_wf_sq
not-pair-member-int
pair def
pair-blex
pair-blex_wf
pair-coding-exists
pair-eta
pair-lex
pair-lex_well_fnd
pair-lex_wf
pair-list
pair-list-set-type
pair-listunion
pair-mono
pair-prior-val
pair-sq-axiom-wf
pair_eta_rw
pair_support
pair_support_double_sum
pair_wf_l_member
rev-append-pair
sdata-pair
sdata-pair-free-from-atom
sdata-pair-has-atom
sdata-pair-one-one
sdata-pair?
sdata-pair?_wf
sdata-pair_wf
sdata_atoms_pair_lemma
sdata_left_pair_lemma
sdata_pair_atom_lemma
sdata_pair_id_lemma
sdata_pair_rec_lemma
sdata_right_pair_lemma
sublist_pair

PAIR2

prev top next

atom-sdata-not-pair2
id-sdata-not-pair2

PAIRS

prev top next

count_index_pairs
count_index_pairs_wf
count_pairs
count_pairs_wf
no_repeats-pairs-fpf
pairs-fpf
pairs-fpf_property
pairs-fpf_wf

PAIRWISE

prev top next

global-order-pairwise-compat-invariant
global-order-pairwise-compat-msg-and-classrel
global-order-pairwise-compat-msg-interface-constraint
global-order-pairwise-compat-squash-invariant
no-repeats-pairwise
pairwise
pairwise-append
pairwise-cons
pairwise-filter
pairwise-implies
pairwise-map
pairwise-map1
pairwise-map2
pairwise-mapl
pairwise-mapl-no-repeats
pairwise-nil
pairwise-singleton
pairwise-sublist
pairwise_wf
pairwise_wf2
sq_stable__pairwise

PALINDROME

prev top next

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

PAND

prev top next

pand
pand-left
pand-left_wf
pand-right
pand-right_wf
pand?
pand?_wf
pand_wf

PAR

prev top next

pi-par-decompose
rank-par
rank-par-decompose

PARADOX

prev top next

Russell-paradox

PARALLEL

prev top next

classfun-res-disjoint-union-comb-as-parallel-eclass1
classfun-res-parallel-class-left
classfun-res-parallel-class-right
hdf-parallel
hdf-parallel-ap
hdf-parallel-bag
hdf-parallel-bag-iterate
hdf-parallel-bag_wf
hdf-parallel-bind-eq
hdf-parallel-bind-eq-gen
hdf-parallel-bind-halt-eq
hdf-parallel-bind-halt-eq-gen
hdf-parallel-compose-eq
hdf-parallel-halt
hdf-parallel-halt-left
hdf-parallel-halt-right
hdf-parallel-halted
hdf-parallel-transformation1
hdf-parallel-transformation1-2-0
hdf-parallel-transformation1-2-1
hdf-parallel-transformation2
hdf-parallel-transformation2-0
hdf-parallel-transformation2-1
hdf-parallel-transformation2-2
hdf-parallel-transformation2-3
hdf-parallel_wf
member-parallel-class
member-parallel-class-bool
parallel composition of base-process-class
parallel-bag-class
parallel-bag-class_wf
parallel-bag-classrel
parallel-bind-program-eq
parallel-bind-program-eq-gen
parallel-class
parallel-class-assoc
parallel-class-bind-left
parallel-class-bind-right
parallel-class-com
parallel-class-disjoint-classrel
parallel-class-es-sv
parallel-class-loc-bounded
parallel-class-program
parallel-class-program-compose2-eq
parallel-class-program-eq
parallel-class-program-eq-hdf
parallel-class-program-wf-hdf
parallel-class-program_wf
parallel-class-single-val
parallel-class-zero
parallel-class_wf
parallel-classrel
parallel-classrel-weak
parallel-compose2-program-eq
parallel-eclass2-left
parallel-eclass2-right

PARAM

prev top next

equal-implies-member-param-W
param-W
param-W-ext
param-W-induction
param-W-rel
param-W-rel_wf
param-W_wf
param-co-W
param-co-W-ext
param-co-W_wf
test-nat-param

PARAMETER

prev top next

es-parameter-class
es-parameter-class_wf
fix_wf_corec_parameter
is-parameter-class
parameter
parameter-class-val

PARAMETER2

prev top next

fix_wf_corec_parameter2

PARAMETER3

prev top next

fix_wf_corec_parameter3

PARAMETERIZED

prev top next

parameterized-rec

PARITY

prev top next

not-same-parity-implies
not-same-parity-implies-even-odd
same-parity
same-parity-implies
same-parity-implies-even-odd
same-parity_wf

PART

prev top next

es-interface-part
es-interface-part_wf
interface-part-subtype
interface-part-val
is-interface-part
member-interface-part
s_part
s_part_char
s_part_functionality_wrt_breqv
s_part_wf
strict_part
strict_part_irrefl
strict_part_wf

PART1

prev top next

rroot-exists-part1

PART2

prev top next

rroot-exists-part2

PARTIAL

prev top next

add-wf-partial
add-wf-partial-nat
apply-partial
apply-partial-indep
band-wf-partial
base-equal-partial
base-member-partial
base-partial
base-partial-not-exception
base-partial-partial
base-partial_wf
bnot-wf-partial
bottom_wf-partial
callbyvalueall_seq-partial-ap-all
callbyvalueall_seq-partial-ap-all0
colist-fix-ap-partial
colist-fix-partial
eq_int-wf-partial
fix_wf_corec_partial_nat
has-value_wf-partial
ifthenelse_wf-partial
ifthenelse_wf-partial-base
inclusion-partial
le_int-wf-partial
partial
partial-base
partial-not-exception
partial-partial
partial-type-continuous
partial-void
partial_ap
partial_ap_compose
partial_ap_gen
partial_ap_gen_wf
partial_ap_is_gen
partial_ap_of_partial_ap_gen
partial_ap_of_partial_ap_gen1
partial_ap_wf
partial_wf
pcw-partial
pcw-partial_wf
per-partial
per-partial-equiv_rel
per-partial-reflex
per-partial-subtype
per-partial_wf
rv-disjoint-rv-partial-sum
rv-partial-sum
rv-partial-sum-monotone
rv-partial-sum-unroll
rv-partial-sum_wf
select_fun_last_partial_ap1
select_fun_last_partial_ap_gen1
subtract-wf-partial
subtype_partial_sqtype_base
subtype_rel_partial
sum-partial-has-value
sum-partial-list-has-value
sum-partial-nat

PARTIAL1

prev top next

fix-corec-partial1
fix_wf_corec-partial1

PARTIAL2

prev top next

eq_int-wf-partial2
inclusion-partial2
le_int-wf-partial2

PARTITION

prev top next

adjacent-full-partition-points
adjacent-partition-points
bag-size-partition
bag-summation-partition
constant-partition-sum
default-partition-choice
default-partition-choice_wf
equipollent-partition
es-before-partition
es-hist-partition
es-interval-partition
es-le-before-partition
es-pplus-partition
es-pstar-q-partition
finite-partition
finite-partition-property
firstn-partition
full-partition
full-partition-non-dec
full-partition-point-member
full-partition_wf
implies-is-partition-choice
is-partition-choice
is-partition-choice_wf
list-partition
list-partition-permutation
list-partition_wf
mesh-trivial-partition
mesh-uniform-partition
nth_tl-partition
partition
partition-choice
partition-choice-member
partition-choice-subtype
partition-choice_wf
partition-endpoints
partition-exists
partition-lemma
partition-mesh
partition-mesh-nil
partition-mesh-nonneg
partition-mesh_wf
partition-point-member
partition-refinement-sum
partition-refines
partition-refines-cons
partition-refines_transitivity
partition-refines_weakening
partition-refines_wf
partition-split-cons
partition-split-cons-mesh
partition-sum
partition-sum_functionality
partition-sum_wf
partition_wf
simple-partition-exists
sq_stable__is-partition-choice
trivial-partition
trivial-partition_wf
uniform-partition
uniform-partition-increasing
uniform-partition-point
uniform-partition-refines
uniform-partition_wf

PARTITION2

prev top next

es-le-before-partition2

PARTITIONS

prev top next

bag-member-partitions
bag-partitions
bag-partitions-assoc
bag-partitions-symmetry
bag-partitions-with-one-given
bag-partitions_wf
bag-summation-partitions-primes
bag-summation-partitions-primes-general
no-repeats-bag-partitions
partitions
partitions_wf
separated-partitions
separated-partitions-have-common-refinement
separated-partitions_wf
sq_stable__partitions

PARTS

prev top next

bag-member-parts
bag-member-parts'
bag-parts
bag-parts'
bag-parts'-no-repeats
bag-parts'_wf
bag-parts'_wf2
bag-parts-no-repeats
bag-parts_wf

PASCAL

prev top next

Pascal-completion
Pascal-completion-property
Pascal-completion_wf
fps-Pascal
fps-Pascal-iff
fps-Pascal_wf
fps-pascal
fps-pascal-elim
fps-pascal-slice
fps-pascal-symmetry
fps-pascal_wf

PASCH

prev top next

eu-inner-pasch
eu-inner-pasch-property
eu-inner-pasch_wf
not-not-inner-pasch

PASSED

prev top next

consensus-ts4-passed-stable
cs-passed
cs-passed_wf
decidable__cs-passed

PATH

prev top next

AF-path-barred
I-path
I-path-morph
I-path-morph-comp
I-path-morph-id
I-path-morph_functionality
I-path-morph_wf
I-path-morph_wf2
I-path_wf
W-path-lemma
W-path-lemma2
cWO-rel-path-barred
csm-I-path
cubical-path
cubical-path-same-name
cubical-path_wf
decidable__path-goes-thru
eff-unique-path
eff-unique-path_wf
fun-path
fun-path-append
fun-path-append1
fun-path-before
fun-path-cons
fun-path-fixedpoint
fun-path-induction
fun-path-member
fun-path-member-connected
fun-path-no_repeats
fun-path_wf
has-no-path
has-no-path_wf
is-path
is-path_wf
loc-on-path
loc-on-path-append
loc-on-path-cons
loc-on-path-decomp
loc-on-path-nil
loc-on-path-singleton
loc-on-path_wf
name-path-endpoints
name-path-endpoints_wf
named-path
named-path-equal-implies
named-path-morph
named-path-morph_wf
named-path-subtype
named-path_wf
path-eq
path-eq-equiv
path-eq-same-name
path-eq_weakening
path-eq_wf
path-goes-thru
path-goes-thru-last
path-goes-thru-last_wf
path-goes-thru_wf
pcw-path
pcw-path-rel
pcw-path-rel_wf
pcw-path-shift
pcw-path_wf
refl-path
refl-path_wf
rel-path
rel-path-between
rel-path-between-append
rel-path-between-cons
rel-path-between_wf
rel-path_wf
rel_exp-iff-path
rel_path
rel_path_wf
rel_plus-iff-path
rel_star-iff-path
retraction-fun-path
retraction-fun-path-before
retraction-fun-path-squash
set-path-name
set-path-name_wf
sq_stable__rel_path

PATHS

prev top next

equal-I-paths
equal-named-paths
pcw-consistent-paths
pcw-consistent-paths_wf

PAXOS

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

PCOM

prev top next

mk-tagged_wf_pCom_choose
mk-tagged_wf_pCom_create
mk-tagged_wf_pCom_msg
mk-tagged_wf_pCom_new
pCom
pCom_wf

PCW

prev top next

decidable__pcw-pp-barred
pcw-consistent-paths
pcw-consistent-paths_wf
pcw-consistent-steps
pcw-consistent-steps_wf
pcw-final-step
pcw-final-step_wf
pcw-partial
pcw-partial_wf
pcw-path
pcw-path-rel
pcw-path-rel_wf
pcw-path-shift
pcw-path_wf
pcw-pp
pcw-pp-barred
pcw-pp-barred-W
pcw-pp-barred-W-decidable
pcw-pp-barred_wf
pcw-pp-barred_wf0
pcw-pp-head
pcw-pp-head_wf
pcw-pp-lemma
pcw-pp-null
pcw-pp-null_wf
pcw-pp-tail
pcw-pp-tail_wf
pcw-pp_wf
pcw-step
pcw-step-agree
pcw-step-agree_wf
pcw-step_wf
pcw-steprel
pcw-steprel_wf

PDIVISOR

prev top next

pdivisor_bound

PDVCONTINUE

prev top next

PiDataVal_ind_pDVcontinue_lemma
pDVcontinue
pDVcontinue?
pDVcontinue?_wf
pDVcontinue_wf

PDVFIRE

prev top next

PiDataVal_ind_pDVfire_lemma
pDVfire
pDVfire?
pDVfire?_wf
pDVfire_wf

PDVGUARDS

prev top next

PiDataVal_ind_pDVguards_lemma
pDVguards
pDVguards-from
pDVguards-from_wf
pDVguards-preList
pDVguards-preList_wf
pDVguards?
pDVguards?_wf
pDVguards_wf

PDVLOC

prev top next

PiDataVal_ind_pDVloc_lemma
PiDataVal_ind_pDVloc_tag_lemma
pDVloc
pDVloc-id
pDVloc-id_wf
pDVloc?
pDVloc?_wf
pDVloc_tag
pDVloc_tag-id
pDVloc_tag-id_wf
pDVloc_tag-name
pDVloc_tag-name_wf
pDVloc_tag?
pDVloc_tag?_wf
pDVloc_tag_wf
pDVloc_wf

PDVMSG

prev top next

PiDataVal_ind_pDVmsg_lemma
pDVmsg
pDVmsg-index
pDVmsg-index_wf
pDVmsg-val
pDVmsg-val_wf
pDVmsg?
pDVmsg?_wf
pDVmsg_wf

PDVREQUEST

prev top next

PiDataVal_ind_pDVrequest_lemma
pDVrequest
pDVrequest-counter
pDVrequest-counter_wf
pDVrequest-rndv2
pDVrequest-rndv2_wf
pDVrequest?
pDVrequest?_wf
pDVrequest_wf

PDVSELEX

prev top next

PiDataVal_ind_pDVselex_lemma
pDVselex
pDVselex-rndv1
pDVselex-rndv1_wf
pDVselex?
pDVselex?_wf
pDVselex_wf

PE

prev top next

pe-e
pe-e_wf
pe-es
pe-es_wf
pe-loc
pe-loc_wf

PEIRCE

prev top next

Peirce's-law-iff-xmiddle
no-uniform-Peirce's-law

PENVTYPE

prev top next

pEnvType
pEnvType_wf

PER

prev top next

apply-wf-per
base-member-per-function
if-per-void
member-per-and
member-per-or-left
member-per-or-right
member-per-product
member-per-union-left
member-per-union-right
member-per-value
per-all
per-all_wf
per-and
per-and_wf
per-apply
per-apply_wf
per-class
per-class-base
per-class-base-singleton
per-class-subtype-singleton
per-class_wf
per-close
per-close_wf
per-computes-to
per-computes-to_wf
per-eq-def
per-eq-def_wf
per-exists
per-exists_wf
per-function
per-function-ext
per-function-type-apply
per-function_wf
per-function_wf_base_family
per-function_wf_type
per-int
per-int_wf
per-or
per-or-equal
per-or_wf
per-partial
per-partial-equiv_rel
per-partial-reflex
per-partial-subtype
per-partial_wf
per-product
per-product-elim
per-product_wf
per-set
per-set_wf
per-union
per-union-elim
per-union-elim1
per-union-implies-wf1
per-union-implies-wf2
per-union_wf
per-univi
per-value
per-value-property
per-value_subtype_base
per-value_wf
per-void
per-void_wf
squash-per-class
subtype_rel-per-set
subtype_rel_per-class
trivial-per-class

PERM

prev top next

app_perm
app_perm_wf
comb_for_comp_perm_wf
comb_for_extend_perm_wf
comb_for_mk_perm_wf
comb_for_mk_perm_wf_a
comb_for_perm_igrp_wf
comb_for_perm_sig_wf
comb_for_perm_wf
comb_for_txpose_perm_wf
comp_perm
comp_perm_wf
conj_perm
conj_perm_wf
extend_perm
extend_perm_over_comp
extend_perm_over_id
extend_perm_over_itcomp
extend_perm_over_txpose
extend_perm_wf
extend_restrict_perm_cancel
id_perm
id_perm_wf
inv_perm
inv_perm_wf
mk_perm
mk_perm_eta_rw
mk_perm_wf
mk_perm_wf_a
mon_itop_perm_invar
perm
perm_assoc
perm_b
perm_b_f_cancel
perm_b_inj
perm_b_to_f
perm_b_wf
perm_f
perm_f_b_cancel
perm_f_inj
perm_f_wf
perm_grp_inv_assoc
perm_grp_inv_id
perm_grp_inv_inv
perm_grp_inv_thru_op
perm_grp_inverse
perm_ident
perm_igrp
perm_igrp_wf
perm_induction
perm_induction_a
perm_induction_b
perm_inverse
perm_mon_assoc
perm_mon_ident
perm_morph
perm_morph_wf
perm_properties
perm_sig
perm_sig_wf
perm_wf
restrict_perm
restrict_perm_using_txpose
restrict_perm_wf
rev_perm
rev_perm_wf
tl_perm
tl_perm_wf
triple_txpose_perm
txpose_perm
txpose_perm_id
txpose_perm_inv
txpose_perm_order_2
txpose_perm_sym
txpose_perm_wf

PERMF

prev top next

app_permf
app_permf_comp
app_permf_id
app_permf_wf
comb_for_app_permf_wf
comb_for_extend_permf_wf
extend_permf
extend_permf_over_comp
extend_permf_over_id
extend_permf_over_swap
extend_permf_wf
rev_permf
rev_permf_order_2
rev_permf_wf

PERMUTATION1

prev top next

bag-splits-permutation1

PERMUTE

prev top next

l_member-permute
l_mul_permute
l_sum_permute
list_accum_permute
map-permute_list
map_permute_list
no_repeats-permute
permute-to-front
permute-to-front-permutation
permute-to-front_wf
permute_list
permute_list-compose
permute_list-identity
permute_list_length
permute_list_select
permute_list_wf
permute_permute_list
residues-permute
set-equal-permute

PERMUTE1

prev top next

list_accum_permute1

PERTYPE

prev top next

pertype
pertype_wf

PES

prev top next

pes-axioms

PEVAL

prev top next

peval
peval-pnegate
peval-unroll
peval_wf

PEXT

prev top next

pExt
pExt_wf

PFAN

prev top next

PFan
PFan_wf
fan-implies-PFan
fan-implies-nwkl!-using-PFan

PI1

prev top next

apply-ifthenelse-pi1
apply-ifthenelse-pi1-eq
comb_for_pi1_wf
pi1
pi1-axiom
pi1-if-ispair-append-nil
pi1_cons_lemma
pi1_wf
pi1_wf_top

PI12

prev top next

pi12-sqle-spread
spread-sq-pi12
spread-sqle-pi12
spread_to_pi12

PI2

prev top next

apply-ifthenelse-pi2
apply-ifthenelse-pi2-eq
pi2
pi2-consensus-rcvs-to-consensus-events
pi2-if-ispair-append-nil
pi2_wf
uniform-continuity-pi2
uniform-continuity-pi2-dec
uniform-continuity-pi2-dec-ext
uniform-continuity-pi2_wf

PICOMM

prev top next

picomm
picomm-body
picomm-body_wf
picomm-pre
picomm-pre_wf
picomm?
picomm?_wf
picomm_wf

PIDATA

prev top next

PiData-comment

PIDATAVAL

prev top next

PiDataVal
PiDataVal-induction
PiDataVal_ind
PiDataVal_ind_pDVcontinue_lemma
PiDataVal_ind_pDVfire_lemma
PiDataVal_ind_pDVguards_lemma
PiDataVal_ind_pDVloc_lemma
PiDataVal_ind_pDVloc_tag_lemma
PiDataVal_ind_pDVmsg_lemma
PiDataVal_ind_pDVrequest_lemma
PiDataVal_ind_pDVselex_lemma
PiDataVal_ind_wf
PiDataVal_wf

PIGEON

prev top next

general-pigeon-hole
pigeon-hole
pigeon-hole-implies
pigeon-hole-implies-ext

PIM

prev top next

piM
piM-continuous
piM_wf

PIMP

prev top next

pimp
pimp-left
pimp-left_wf
pimp-right
pimp-right_wf
pimp?
pimp?_wf
pimp_wf

PINEW

prev top next

pinew
pinew-body
pinew-body_wf
pinew-name
pinew-name_wf
pinew?
pinew?_wf
pinew_wf

PINTRANSIT

prev top next

pInTransit
pInTransit_wf

PIOPTION

prev top next

pioption
pioption-left
pioption-left_wf
pioption-right
pioption-right_wf
pioption?
pioption?_wf
pioption_wf

PIPAR

prev top next

pipar
pipar-left
pipar-left_wf
pipar-right
pipar-right_wf
pipar?
pipar?_wf
pipar_wf

PIRCV

prev top next

pircv
pircv-chan
pircv-chan_wf
pircv-var
pircv-var_wf
pircv?
pircv?_wf
pircv_wf

PIREP

prev top next

pirep
pirep-body
pirep-body_wf
pirep?
pirep?_wf
pirep_wf

PISEND

prev top next

pisend
pisend-chan
pisend-chan_wf
pisend-var
pisend-var_wf
pisend?
pisend?_wf
pisend_wf

PIZERO

prev top next

pizero
pizero?
pizero?_wf
pizero_wf

PLANE

prev top next

euclidean-plane
euclidean-plane_wf

PLAY

prev top next

Play
Play_wf
shift-play
shift-play_wf

PLUS

prev top next

add-plus-1-div-2-implies-lt
alg_plus
alg_plus_wf
decidable__equal_nat_plus
decidable__rel_plus
es-loc-pred-plus
exp_wf_nat_plus
lookup_omral_plus
module_act_plus
module_hom_plus
module_plus_assoc
module_plus_comm
module_plus_ident
module_plus_inv
mul_over_plus_fps
nat_plus
nat_plus_inc
nat_plus_inc_int_nzero
nat_plus_inc_nat
nat_plus_properties
nat_plus_subtype_nat
nat_plus_wf
omral_action_plus_l
omral_action_plus_r
omral_plus
omral_plus_assoc
omral_plus_comm
omral_plus_dom
omral_plus_non_zero_vals
omral_plus_sd_ordered
omral_plus_wf
omral_plus_wf2
primrec-wf-nat-plus
rel-immediate-rel-plus
rel-plus-rel-immediate
rel-plus-rel-star
rel-rel-plus
rel-star-iff-rel-plus
rel-star-iff-rel-plus-or
rel-star-rel-plus
rel_plus
rel_plus-TI
rel_plus-iff-path
rel_plus-of-restriction
rel_plus-restriction-equiv
rel_plus-uniform-TI
rel_plus-weak-TI
rel_plus_closure
rel_plus_field
rel_plus_functionality_wrt_breqv
rel_plus_functionality_wrt_brle
rel_plus_functionality_wrt_iff
rel_plus_functionality_wrt_rel_implies
rel_plus_idempotent
rel_plus_iff
rel_plus_iff2
rel_plus_implies
rel_plus_implies2
rel_plus_irreflexive
rel_plus_minimal
rel_plus_monotone
rel_plus_strongwellfounded
rel_plus_trans
rel_plus_wf
rng_minus_over_plus
rng_mssum_of_plus
rng_plus
rng_plus_ac_1
rng_plus_assoc
rng_plus_cancel_l
rng_plus_comm
rng_plus_comm2
rng_plus_inv
rng_plus_inv_assoc
rng_plus_wf
rng_plus_zero
rng_sum_plus
rng_times_over_plus
rng_when_thru_plus
str-to-nat-plus
str-to-nat-plus-property
str-to-nat-plus_wf

PLUS2

prev top next

rel-star-rel-plus2

PLUS3

prev top next

rel-star-rel-plus3

PM

prev top next

only_pm_one_divs_one
pm_equal
pm_equal_wf

PMAX

prev top next

pv11_p1_pmax
pv11_p1_pmax_desc
pv11_p1_pmax_desc_iff
pv11_p1_pmax_desc_implies
pv11_p1_pmax_wf

PMSG

prev top next

pMsg
pMsg_wf

PNEGATE

prev top next

peval-pnegate
pnegate
pnegate_wf

PNOT

prev top next

pnot
pnot-sub
pnot-sub_wf
pnot?
pnot?_wf
pnot_wf

POINT

prev top next

eu-point
eu-point_wf
euclidean-point-eq
full-partition-point-member
partition-point-member
stable_point-eq
uniform-partition-point

POINTER

prev top next

C_Pointer
C_Pointer-to
C_Pointer-to_wf
C_Pointer?
C_Pointer?_wf
C_Pointer_wf
DVp_Pointer
DVp_Pointer-ptr
DVp_Pointer-ptr_wf
DVp_Pointer?
DVp_Pointer?_wf
DVp_Pointer_wf

POINTS

prev top next

adjacent-frs-points
adjacent-full-partition-points
adjacent-partition-points

POINTWISE

prev top next

pointwise-req
pointwise-req_wf
pointwise-rleq
pointwise-rleq_wf
stream-pointwise
stream-pointwise-iff
stream-pointwise_transitivity
stream-pointwise_wf

POLARITY

prev top next

grp_op_polarity

POLY

prev top next

poly-deriv
poly-deriv-linear
poly-deriv_wf
poly-nth-deriv
poly-nth-deriv-req
poly-nth-deriv_wf
polyalg_poly
polyalg_poly_wf

POLYALG

prev top next

oal_polyalg
oal_polyalg_wf
polyalg_mo
polyalg_mo_wf
polyalg_poly
polyalg_poly_wf

POLYMORPHIC

prev top next

polymorphic-choice-1
polymorphic-constant
polymorphic-constant-base
polymorphic-constant-bool
polymorphic-id-unique
polymorphic-id-unique-sq

POLYMORPHISM

prev top next

subtype_neg_polymorphism_test
subtype_pos_polymorphism_test

POLYNOM

prev top next

polynom_alg
polynom_alg_wf

POLYNOMIAL

prev top next

mv-polynomial
mv-polynomial_wf
polynomial-deriv-seq

POR

prev top next

por
por-left
por-left_wf
por-right
por-right_wf
por?
por?_wf
por_wf

PORT

prev top next

ci-port
es-in-port-conds

POS

prev top next

absval_pos
bm_cnt_prop_pos
bm_count_prop_pos
l_contains_pos_length
l_subset_pos_length
length-filter-pos
mapfilter-pos-length
new_23_sig_rounds_pos
new_23_sig_rounds_pos_fun
pos-length
pos_length
pos_length2
pos_length3
pos_mul_arg_bounds
pv11_p1_ldr_fun_pos
pv11_p1_ldr_pos
subtype_pos_polymorphism_test
union-nat-missing-pos
union-nat-missing-pos-prop
union-nat-missing-pos_wf

POSET

prev top next

decidable__equal-poset-cat-ob
loset_subtype_poset
loset_subtype_poset_sig
member-poset-cat-arrow
poset
poset-cat
poset-cat-arrow-cases
poset-cat-arrow-equals
poset-cat-arrow-filter-nil
poset-cat-arrow-flip
poset-cat-arrow-iff
poset-cat-arrow-not-equal
poset-cat-arrow-unique
poset-cat-arrow_subtype
poset-cat-dist
poset-cat-dist-add
poset-cat-dist-flip
poset-cat-dist-non-zero
poset-cat-dist-zero
poset-cat-dist_wf
poset-cat-ob-cases
poset-cat-ob_subtype
poset-cat_wf
poset-extend-unique
poset-functor
poset-functor-comp
poset-functor-extends
poset-functor-extends-box-faces
poset-functor-extends-box-faces-1
poset-functor-extends_wf
poset-functor-id
poset-functor_wf
poset-functors-equal
poset-id-functor
poset_anti_sym
poset_functor_extend
poset_functor_extend-extends
poset_functor_extend-face-map
poset_functor_extend-face-map1
poset_functor_extend-flip
poset_functor_extend-is-functor
poset_functor_extend_id
poset_functor_extend_same
poset_functor_extend_wf
poset_properties
poset_sig
poset_sig_inc
poset_sig_wf
poset_subtype_qoset
poset_wf
subtype_rel_poset
unique-poset-functor

POSINT

prev top next

posint_atom_imp_prime
posint_cancel
posint_div_dec
posint_fact_exists
posint_is_ufm
posint_mul_mon
posint_mul_mon_wf
posint_munit_elim
posint_reduc_dec
posint_unit_dec
posint_well_fnd

POSITIVE

prev top next

absval-positive
add-positive
add-positive-nonneg
colength-positive
combinations-positive
div-positive-1
exp-positive
exp-positive-stronger
fact-positive
first_index-positive
gcd-positive
int-bag-product-positive
iroot-positive
iseg_product-positive
lcm-positive
less-iff-positive
positive-prime-divides-prime
positive-prime-divides-product
rabs-positive
rabs-positive-iff
radd-positive-implies
rinv-positive
rmax-positive
rmin-positive
rmul-is-positive
rnexp-is-positive
rnexp-positive
run-event-step-positive

POSITIVE2

prev top next

colength-positive2

POSS

prev top next

poss-le
poss-le_wf
poss-maj
poss-maj-invariant
poss-maj-length
poss-maj-length2
poss-maj-member
poss-maj-property
poss-maj-unanimous
poss-maj_wf

POSSIBLE

prev top next

cs-possible-state-reachable
possible-event
possible-event_wf
possible-majority
possible-majority_wf

POST

prev top next

A-post-val
A-post-val_wf

POWER

prev top next

cantor-theorem-on-power-set
cantor-theorem-on-power-set-prop
list-subtype-power-type
power-series
power-series-converges
power-series_wf
power-set
power-set-lift
power-set-lift-well-founded-implies
power-set-lift_wf
power-set_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
power-type
power-type-length
power-type-subtype-list
power-type_wf

POWERED

prev top next

equipollent-nat-powered

POWERED2

prev top next

equipollent-nat-powered2

POWERED3

prev top next

equipollent-nat-powered3

POWERSET

prev top next

equipollent-powerset
powerset
powerset_wf

PP

prev top next

cw-pp-lemma
decidable__pcw-pp-barred
pcw-pp
pcw-pp-barred
pcw-pp-barred-W
pcw-pp-barred-W-decidable
pcw-pp-barred_wf
pcw-pp-barred_wf0
pcw-pp-head
pcw-pp-head_wf
pcw-pp-lemma
pcw-pp-null
pcw-pp-null_wf
pcw-pp-tail
pcw-pp-tail_wf
pcw-pp_wf

PPCC

prev top next

ppcc-problem
ppcc-problem2
ppcc-problem3
ppcc-test
ppcc-test2
ppcc-test3
ppcc-test4
ppcc-test6

PPLUS

prev top next

es-pplus
es-pplus-alle-between2
es-pplus-first-since
es-pplus-first-since-exit
es-pplus-le
es-pplus-partition
es-pplus-trivial
es-pplus_functionality_wrt_iff
es-pplus_functionality_wrt_implies
es-pplus_functionality_wrt_rev_implies
es-pplus_wf

PR

prev top next

cons_pr_in_oalist
list_pr_length_ind
lookup_cons_pr_lemma
oal_cons_pr
oal_cons_pr_wf
oalist_pr_length_ind

PRANK

prev top next

prank
prank-psub
prank-pvar
prank_functionality
prank_wf

PRC

prev top next

Memory4-prc
State3-prc

PRE

prev top next

A-pre-val
A-pre-val_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
locl-pre-preserving
locl-pre-preserving-1-1
locl-pre-preserving-compose
locl-pre-preserving_wf
picomm-pre
picomm-pre_wf
rel-pre-preserving
rel-pre-preserving-compose
rel-pre-preserving_wf
rep-pre-sheaf
rep-pre-sheaf
rep-pre-sheaf_wf
rep-pre-sheaf_wf

PRECONDITION

prev top next

cs-knowledge-precondition
cs-knowledge-precondition_wf
cs-precondition
cs-precondition_wf
decidable__cs-precondition

PRED

prev top next

causal-pred-wellfounded
class-pred
class-pred-cases
class-pred_wf
decidable__es-p-le-pred
decidable__es-p-local-pred
decidable__exists-es-p-le-pred
decidable__exists-es-p-local-pred
decidable__exists-pred-iterated-classrel-between3-sv
decidable__run-pred
eo-forward-base-pred
eo-forward-pred
eo-forward-pred?
eo-strict-forward-pred
eo-strict-forward-pred?
es-base-pred
es-base-pred-le
es-base-pred-less
es-base-pred-properties
es-base-pred_wf
es-before-pred-length
es-causl-if-pred
es-interface-history-pred
es-interface-le-pred
es-interface-le-pred-bool
es-interface-local-pred
es-interface-local-pred-bool
es-interface-pred
es-interface-pred_wf
es-interface-pred_wf2
es-is-prior-interface-pred
es-le-before-pred
es-le-pred
es-loc-pred
es-loc-pred-plus
es-local-le-pred
es-local-le-pred-property
es-local-le-pred_wf
es-local-pred
es-local-pred-cases
es-local-pred-cases-sq
es-local-pred-iff-es-p-local-pred
es-local-pred-property
es-local-pred-property2
es-local-pred_wf
es-local-pred_wf2
es-locl-pred
es-p-le-pred
es-p-le-pred_wf
es-p-local-pred
es-p-local-pred_wf
es-pred
es-pred-causl
es-pred-cle
es-pred-eq
es-pred-eq_wf
es-pred-exists-between
es-pred-exists-between2
es-pred-le
es-pred-less-base
es-pred-loc-base
es-pred-locl
es-pred-locl-implies-le
es-pred-maximal-base
es-pred-one-one
es-pred-wf-base
es-pred?
es-pred?_property
es-pred?_wf
es-pred_property
es-pred_property_base
es-pred_wf
es-prior-interface-val-pred
finite-run-pred
gcd_sat_pred
implies-es-le-pred
implies-es-pred
list-eo-pred
local-pred-class
local-pred-class_wf
oal_merge_dom_pred
omral_scale_dom_pred
pred-hd-es-open-interval
pred-member-es-open-interval
primed-class-pred
prior-classrel-p-local-pred
prior-val-pred
pv11_p1_ldr_fun_state_adopted_pred
pv11_p1_ldr_fun_state_propose_pred
pv11_p1_ldr_state_adopted_pred
pv11_p1_ldr_state_propose_pred
ranked-eo-pred
run-event-local-pred
run-event-local-pred_wf
run-local-pred
run-local-pred_wf
run-pred
run-pred-step-less
run-pred_wf
run_local_pred
run_local_pred_loc
run_local_pred_maximal
run_local_pred_time
run_local_pred_time_less
run_local_pred_wf
sub-es-pred
sub-es-pred_wf
weak-antecedent-function_functionality_wrt_pred_equiv
weak-antecedent-surjection_functionality_wrt_pred_equiv
well-founded-run-pred

PRED2

prev top next

implies-es-pred2

PREDECESSOR

prev top next

causal-predecessor
causal-predecessor_wf
causal-weak-predecessor
causal-weak-predecessor_wf

PREDECESSOR1

prev top next

p-compose-causal-predecessor1

PREDECESSORS1

prev top next

first-at-filter-interface-predecessors1

PREDECESSORS2

prev top next

member-interface-predecessors2

PREDECIDED

prev top next

cs-predecided
cs-predecided_wf
cs-ref-map3-predecided

PREDICATE

prev top next

dec-predicate
dec-predicate_wf
decidable-predicate-and
decidable-predicate-not
decidable-predicate-or
es-E-interface-predicate
es-interface-conditional-predicate-equivalent
es-interface-predicate
es-interface-predicate_wf
interface_predicate_set_lemma
lift-predicate
lift-predicate_wf
local-class-predicate
local-class-predicate-property
local-class-predicate-property2
local-class-predicate_wf
nary-rel-predicate
nary-rel-predicate_wf
predicate-and
predicate-and_wf
predicate-not
predicate-not_wf
predicate-or
predicate-or-shift
predicate-or-shift_wf
predicate-or_wf
predicate-shift
predicate-shift_wf
predicate_equivalent
predicate_equivalent_implies
predicate_equivalent_inversion
predicate_equivalent_transitivity
predicate_equivalent_weakening
predicate_equivalent_wf
predicate_implies
predicate_implies_reflexivity
predicate_implies_transitivity
predicate_implies_weakening
predicate_implies_wf
predicate_or
predicate_or_idempotent
predicate_or_wf
predicate_rev_implies
predicate_rev_implies_weakening
predicate_rev_implies_wf
unbounded-list-predicate
unbounded-list-predicate_wf

PREEMPTED

prev top next

pv11_p1-preempted
pv11_p1_adopted_from_init_or_preempted
pv11_p1_ldr_mem_preempted
pv11_p1_leader_preempted
pv11_p1_leader_preempted_wf
pv11_p1_preempted'base
pv11_p1_preempted'base-program
pv11_p1_preempted'base-program_wf
pv11_p1_preempted'base_wf
pv11_p1_preempted'send
pv11_p1_preempted'send_wf
pv11_p1_when_preempted
pv11_p1_when_preempted_wf

PREFIX

prev top next

accum_split_prefix
bound_in_prefix
bound_in_prefix_wf
free_in_prefix
free_in_prefix_wf
list_split_prefix
longest-prefix
longest-prefix-decomp
longest-prefix-is-nil
longest-prefix-list_accum
longest-prefix-singleton
longest-prefix_property
longest-prefix_property'
longest-prefix_property2
longest-prefix_wf
pi-prefix-names
pi-prefix-names_wf
pi_prefix
pi_prefix-definition
pi_prefix-ext
pi_prefix-induction
pi_prefix_ind
pi_prefix_ind_wf
pi_prefix_ind_wf_simple
pi_prefix_wf
prefix-match
prefix-match_wf
prefix-replace
prefix-replace_wf

PREFIX2

prev top next

accum_split_prefix2

PRELIST

prev top next

pDVguards-preList
pDVguards-preList_wf

PREORDER

prev top next

divides_preorder
mdivides_preorder
preorder
preorder_wf
symmetrized_preorder

PREPEND1

prev top next

mklist-prepend1

PRESERVED

prev top next

and_preserved_by
and_preserved_by2
preserved_by
preserved_by2
preserved_by2_wf
preserved_by_monotone
preserved_by_or
preserved_by_star
preserved_by_symmetric
preserved_by_wf

PRESERVES

prev top next

div_preserves_le
embedding-preserves-local-class
embedding-preserves-local-property
embedding-preserves-local-relation
eu-congruent-preserves-between
exp_preserves_le
exp_preserves_lt
grp_op_preserves_le
grp_op_preserves_lt
iff_preserves_decidability
joint-embedding-preserves-causal-invariant
mul_preserves_eq
mul_preserves_le
mul_preserves_lt
oal_merge_preserves_le
oal_merge_preserves_lt
radd-preserves-req
radd-preserves-rleq
radd-preserves-rless
rel-immediate-preserves-order
right_mul_preserves_le
rinv_preserves_rless
rinv_preserves_rneq
rmul_preserves_req
rmul_preserves_rleq
rmul_preserves_rleq2
rmul_preserves_rless
rmul_preserves_rneq
strong-subtype-iff-preserves-singleton
weak-joint-embedding-preserves-causal-invariant
weak-joint-embedding-preserves-squash-causal-invariant

PRESERVING

prev top next

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
causal-order-preserving
causal-order-preserving_wf
causale-order-preserving
causale-order-preserving_wf
convergent-flow-order-preserving
es-fix-order-preserving
global-order-preserving
global-order-preserving_wf
interface-order-preserving
interface-order-preserving_wf
locl-pre-preserving
locl-pre-preserving-1-1
locl-pre-preserving-compose
locl-pre-preserving_wf
order-preserving
order-preserving_wf
rel-pre-preserving
rel-pre-preserving-compose
rel-pre-preserving_wf
rel-preserving
rel-preserving-composes
rel-preserving-star
rel-preserving-star-reachable
rel-preserving_wf
strong-interface-fifo-order-preserving
tree-flow-order-preserving

PREVIOUS

prev top next

previous-event-exists

PRIMALITY

prev top next

primality-test

PRIME

prev top next

Prime
Prime_wf
assert-is_prime
atomic_imp_prime
decidable__prime
divides-prime
eqmod-prime-order-fixedpoints
factors-prime-product
gcd-prime
ideal_of_prime
is_prime
is_prime_wf
posint_atom_imp_prime
positive-prime-divides-prime
positive-prime-divides-product
prime
prime-divides-prime
prime-factors
prime-factors-unique
prime-factors2
prime-factors3
prime-product-injection
prime_divs_prod
prime_elim
prime_ideal_p
prime_ideal_p_wf
prime_ideals_in_int_ring
prime_imp_atomic
prime_wf
quot_by_prime_ideal
sq_stable__prime_ideal

PRIMED

prev top next

primed-class
primed-class-cases
primed-class-equal
primed-class-opt
primed-class-opt-cases
primed-class-opt-cases2
primed-class-opt-classrel
primed-class-opt-es-sv
primed-class-opt-es-sv0
primed-class-opt-exists
primed-class-opt-single-val
primed-class-opt-single-val0
primed-class-opt_eq_class-opt-class-primed
primed-class-opt_eq_class-opt-primed
primed-class-opt_functionality
primed-class-opt_functionality-locl
primed-class-opt_wf
primed-class-pred
primed-class-prior-val
primed-class_wf
primed-classrel
primed-classrel-opt

PRIMEFACTORS

prev top next

primefactors
primefactors_wf

PRIMES

prev top next

bag-product-primes
bag-summation-partitions-primes
bag-summation-partitions-primes-general
equipollent-primes

PRIMITIVE

prev top next

mutual-primitive-recursion

PRIMREC

prev top next

primrec
primrec-induction
primrec-induction-factorial
primrec-unroll
primrec-unroll-1
primrec-wf
primrec-wf-int_seg
primrec-wf-nat-plus
primrec-wf-nsub
primrec-wf-upper
primrec-wf2
primrec_add
primrec_wf
simple-primrec-add
sum-as-primrec
sum_aux-as-primrec

PRIMREC0

prev top next

primrec0_lemma

PRIMREC1

prev top next

primrec1_lemma

PRINC

prev top next

princ_ideal
princ_ideal_mem_cond
princ_ideal_wf

PRINCIPLE

prev top next

coinduction-principle
generalized-markov-principle
generalized-markov-principle_wf
indexed-coinduction-principle
real-continuity-principle
real-continuity-principle_wf

PRINT

prev top next

find-xover-print
mu-ge-print

PRIORITY

prev top next

not-isl-priority-select
priority-select
priority-select-ff
priority-select-inr
priority-select-property
priority-select-tt
priority-select_wf

PRIVATE

prev top next

ses-D-private
ses-D-private_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-public-not-private

PROB

prev top next

finite-prob-space
finite-prob-space_wf

PROB2

prev top next

prob2.1
prob2.2
prob2.3
prob2.4

PROBLEM

prev top next

ppcc-problem

PROBLEM2

prev top next

ppcc-problem2

PROBLEM3

prev top next

ppcc-problem3

PROCESS

prev top next

Comm-process-q
Comm-process-q_aux
Comm-process-q_aux_wf
Comm-process-q_wf
Process
Process-apply
Process-apply_wf
Process-stream
Process-stream_wf
Process-value-type
Process_wf
base-process-class
base-process-class-program
base-process-class-program-ap
base-process-class-program_wf
base-process-class-program_wf1
base-process-class_wf
base-process-inputs
base-process-inputs-non-null
base-process-inputs_wf
boot-process
boot-process_wf
component-process
component-process_wf
dataflow-to-Process
dataflow-to-Process_functionality
dataflow-to-Process_wf
datastream-dataflow-to-Process
forkable-process
forkable-process_wf
iterate-Process
iterate-Process_wf
iterate-base-process-class-program
iterate-null-process
iterate-process
iterate-process_wf
null-process
null-process_wf
parallel composition of base-process-class
pi-process
pi-process_wf
process
process model notes
process-equiv
process-equiv-is-equiv
process-equiv_wf
process-has-value
process-ordered-message
process-ordered-message_wf
process-ordered-message_wf_simple
process-subtype
process-value-type
process-valueall-type
process_wf
rec-process
rec-process_wf
rec-process_wf_Process
rec-process_wf_pi
rec-process_wf_pi_simple_state
virus-process
virus-process_wf

PROCESSCHOOSE

prev top next

processChoose
processChoose-comment
processChoose_wf
processChoose_wf2

PROCESSCOMM

prev top next

processComm
processComm_wf
processComm_wf2

PROD

prev top next

RankEx1_Prod
RankEx1_Prod-prod
RankEx1_Prod-prod_wf
RankEx1_Prod?
RankEx1_Prod?_wf
RankEx1_Prod_wf
RankEx2_Prod
RankEx2_Prod-prod
RankEx2_Prod-prod_wf
RankEx2_Prod?
RankEx2_Prod?_wf
RankEx2_Prod_wf
coprime_divides_prod
coprime_divisors_prod
coprime_prod
equipollent-nat-prod-nsub
int-prod
int-prod-factor
int-prod-split
int-prod_wf
int-prod_wf_nat
isaxiom-bool-if-bunion-unit-prod
isect_prod_lemma
ispair-bool-if-bunion-unit-prod
list-prod-set-type
mset_prod
mset_prod_mem
mset_prod_wf
mset_prod_wf2
prime_divs_prod
prod-if-ispair-append-nil
prod-image-is-image
prod_in_mset_prod
rng_prod
rng_prod_wf
set_prod
set_prod_wf
super-fact-int-prod-exp

PROD0

prev top next

int_prod0_lemma

PRODDEQ

prev top next

proddeq
proddeq_reduce_lemma
proddeq_wf

PRODL

prev top next

RankEx1_ProdL
RankEx1_ProdL-prodl
RankEx1_ProdL-prodl_wf
RankEx1_ProdL?
RankEx1_ProdL?_wf
RankEx1_ProdL_wf

PRODR

prev top next

RankEx1_ProdR
RankEx1_ProdR-prodr
RankEx1_ProdR-prodr_wf
RankEx1_ProdR?
RankEx1_ProdR?_wf
RankEx1_ProdR_wf

PRODUCT

prev top next

absval-diff-product-bound
assert-product-deq
atom-product-disjoint
bag-member-product
bag-product
bag-product-append
bag-product-empty
bag-product-no-repeats
bag-product-primes
bag-product-single
bag-product_wf
bag-summation-product
canonicalizable-product
compact-product
continuous'-monotone-product
continuous-monotone-product
decidable__equal_product
destructor-product
divides_product
dot-product
dot-product-comm
dot-product-linearity1
dot-product-linearity2
dot-product-nonneg
dot-product_functionality
dot-product_wf
equipollent-function-product
equipollent-list-as-product
equipollent-nat-list-as-product
equipollent-product
equipollent-product-assoc
equipollent-product-com
equipollent-product-one
equipollent-product-product
equipollent-product-sum
equipollent-product-zero
equipollent-union-product
factors-prime-product
finite-type-product
fps-compose-fps-product
fps-product
fps-product-append
fps-product-reindex
fps-product-single
fps-product-upto
fps-product_wf
int-bag-product
int-bag-product-append
int-bag-product-positive
int-bag-product_wf
int-product-disjoint
int-product-union-atom-disjoint
iseg_product
iseg_product-positive
iseg_product-property
iseg_product-split
iseg_product_rem
iseg_product_rem_property
iseg_product_rem_wf
iseg_product_wf
markov-streamless-product
member-per-product
member-product-map
mul-list-bag-product
per-product
per-product-elim
per-product_wf
positive-prime-divides-product
power-sum-product
prime-product-injection
product def
product-deq
product-deq_wf
product-equipollent-tuple
product-equipollent-tuple2
product-equipollent-tuple3
product-factors
product-map
product-map_wf
product-subtype-co-list
product-union-atom-disjoint
product-unit-disjoint
product-value-type
product-valueall-type
product-wf
product_functionality_wrt_equipollent
product_functionality_wrt_equipollent_dependent
product_functionality_wrt_equipollent_left
product_functionality_wrt_equipollent_right
product_subtype_base
product_subtype_list
product_well_fnd
rsum_product
simple-product_subtype_base
singleton-type-product
squash-product
strong-continuous-product
strong-subtype-dep-product
strong-subtype-product
subtype_rel_dep_product_iff
subtype_rel_product
subtype_rel_simple_product
test-eq-product
type-functor-product
type-functor-product_wf
union-product-disjoint
unit-product-disjoint
void-dep-product
void-product

PRODUCT1

prev top next

equal-product1
exists-product1

PRODUCT2

prev top next

exists-product2

PRODUCT3

prev top next

exists-product3

PRODUCT4

prev top next

exists-product4

PRODUCT5

prev top next

exists-product5

PRODUCTDEQ

prev top next

productdeq_reduce_lemma

PROG

prev top next

sum_of_geometric_prog

PROGRAMMABLE

prev top next

accum-class-programmable
es-interface-accum-programmable
es-interface-pair-prior-programmable
es-prior-class-when-programmable
es-prior-match-programmable

PROGRESS1

prev top next

new_23_sig_progress1

PROGRESS2

prev top next

new_23_sig_progress2-step1
new_23_sig_progress2-step2

PROJN

prev top next

projn

PROOF

prev top next

correct_proof
correct_proof-wf
correct_proof_wf
decidable__l_all-proof
decidable__l_exists-proof
ex-evd-proof
ex-evd-proof-check
ex-evd-proof-step
fix_wf_corec-alt-proof
full-evd-proof-step
proof-by-cont-implies-LEM
proof-tree
proof-tree-ext
proof-tree_wf
rless-cases-proof
sq_stable__correct_proof
sv-bag-is-bag-rep-lousy-proof
uniform-evd-proof
uniform-evd-proof-check
uniform-evd-proof-checks
uniform-evd-to-proof

PROOF2

prev top next

map-filter-proof2
stream-lex_transitivity-proof2

PROP

prev top next

CLK-prop
add-nat-missing-prop
base-member-prop
bm_cnt_prop
bm_cnt_prop_E
bm_cnt_prop_E_reduce_lemma
bm_cnt_prop_T
bm_cnt_prop_pos
bm_cnt_prop_wf
bm_count_prop
bm_count_prop_pos
bottom-member-prop
cantor-theorem-on-power-set-prop
empty-nat-missing-prop
extract-decider-of-decidable-prop
ifthenelse-prop
implies-prop-truncation
int-decr-map-add-prop
int-decr-map-empty-prop
int-decr-map-find-prop
int-decr-map-inDom-prop
int-decr-map-isEmpty-prop
int-decr-map-remove-prop
int-decr-map-update-prop
isEmpty-nat-missing-prop
length-in-prop-if-co-list
lookup-list-map-add-prop
lookup-list-map-empty-prop
lookup-list-map-inDom-prop
lookup-list-map-isEmpty-prop
lookup-list-map-remove-prop
lookup-list-map-type-prop
lookup-list-map-update-prop
map-sig-inDom-prop
prop
prop-truncation-implies
prop-truncation-quot
prop_and
prop_and_wf
remove-nat-missing-prop
set-sig-add-prop
set-sig-empty-prop
singleton-nat-missing-prop
uniform-continuity-pi-pi-prop
union-nat-missing-pos-prop
union-nat-missing-prop

PROP0

prev top next

bm_cnt_prop0
bm_cnt_prop0_E
bm_cnt_prop0_E_reduce_lemma
bm_cnt_prop0_T
bm_cnt_prop0_wf
bm_numItems_is_cnt_prop0

PROP1

prev top next

int-decr-map-inDom-prop1
is-list-prop1
quicksort-int-prop1
strong-continuity-test-prop1
uniform-continuity-pi-search-prop1

PROP2

prev top next

CLK-prop2
int-decr-map-find-prop2
int-decr-map-inDom-prop2
is-list-prop2
set-sig-empty-prop2
strong-continuity-test-prop2
uniform-continuity-pi-pi-prop2
uniform-continuity-pi-search-prop2

PROP3

prev top next

strong-continuity-test-prop3

PROPAGATE

prev top next

es-propagate-iff1
es-propagate-iff1_wf
es-propagate-iff2
es-propagate-iff2_wf

PROPAGATION

prev top next

es-fwd-propagation
es-fwd-propagation-via
es-fwd-propagation-via-unique
es-fwd-propagation-via_wf
es-fwd-propagation_wf
es-propagation-rule
es-propagation-rule-iff
es-propagation-rule-iff_wf
es-propagation-rule_wf

PROPER

prev top next

C_LVALUE-proper
C_LVALUE-proper-Ground
C_LVALUE-proper-Index
C_LVALUE-proper-Indexed
C_LVALUE-proper-Scomp
C_LVALUE-proper-Scomped
C_LVALUE-proper_wf
cantor-to-interval-onto-proper
compact-proper-interval-near-member
cons-proper-iseg
decidable__proper_divisor
eu-proper-extend-exists
eu-proper-segment
eu-proper-segment_wf
eu-seg-congruent-equiv-proper
eu-seg-proper
eu-seg-proper_wf
i-member-proper-iff
list_accum_proper_iseg_inv
proper-divisor
proper-divisor-aux
proper-divisor-aux_wf
proper-divisor_wf
proper-iseg
proper-iseg-append
proper-iseg-append-one
proper-iseg-length
proper-iseg_wf
proper-real-continuity
proper-real-continuity_wf
proper_sublist_length

PROPERTIES

prev top next

EventML spec properties
EventML spec properties
EventML spec properties
EventML spec properties
Wmul-add-properties
abdgrp_properties
abdmonoid_properties
abgrp_properties
abmonoid_properties
algebra_hom_properties
algebra_properties
bagp_properties
calgebra_properties
cdrng_properties
crng_all_properties
crng_properties
detach_fun_properties
dislist_properties
dmon_properties
drng_all_properties
drng_properties
dset_properties
es-base-pred-properties
event_ordering_properties
fin_type_properties
fmonalg_properties
free_abmon_umap_properties
free_abmon_umap_properties_1
fset_properties
ftype_properties
gcd_properties
gcopower_properties
grp_properties
hgrp_car_properties
iabgrp_properties
iabmonoid_properties
igrp_properties
imon_all_properties
imon_properties
inj_mon_hom_properties
int_iseg_properties
int_lower_properties
int_nzero_properties
int_seg_properties
int_upper_properties
list_n_properties
listp_properties
loset_properties
matom_ty_properties
mcopower_properties
module_hom_properties
module_properties
mon_properties
monoid_hom_properties
nat_plus_properties
nat_properties
oalist_car_properties
ocgrp_properties
ocmon_properties
omon_properties
omralist_car_properties
perm_properties
poset_properties
qoset_properties
rng_all_properties
rng_properties
singleton_properties

PROPERTY

prev top next

----- header property --------------------
A-null-property
CV_property
NSL-authentication-property
NSL-authentication-property_wf
Pascal-completion-property
Q-R-glues-property
Russell-property
bag-co-restrict-property
bag-diff-property
bag-drop-property
bag-lub-property
bag-moebius-property
bag-remove1-property
bag_remove1_aux_property
bigger-int-property
cnv-taba-property
combinations_aux_rem_property
cut-of-property
deq_property
ds_property
embedding-preserves-local-property
eo-restrict_property
es-E-interface-property
es-cut-at-property
es-empty-interface-property
es-fix_property
es-fset-at-property
es-interface-or-left-property
es-interface-or-right-property
es-local-le-pred-property
es-local-pred-property
es-local-property
es-local-property_wf
es-locless-property
es-pred?_property
es-pred_property
es-pred_property_base
es-prior-interface-vals-property
es-rank_property
es-rank_property-base
eu-extend-property
eu-inner-pasch-property
exp-ratio-property
exp-rem-property
expfact-property
face-map-property
face-maps-comp-property
final-iterate-property
find_property
finite-partition-property
first-choosable-property
first-event-property
first_index_property
fix_property
fpf-join-single-property
fpf-union-compatible-property
fps-div-coeff-property
fps-div-property
fps-scalar-mul-property
fresh-sig-protocol1_property
fset-max_property
funinv-property
gcd-property
gcd_reduce_property
general-iroot-property
glues-property
i-witness-property
index-split_property
insert_property
int-list-index-property
iroot-property
iseg-local-property
iseg_product-property
iseg_product_rem_property
isqrt-property
l-all-and-property
l-all-property
last_index_property
last_with_property
lcm-property
lg-search-property
list-diff-property
list-eo-property
list-index-property
list-max-aux-property
list-max-property
list-set-type-property
list-to-set-property
local-class-predicate-property
log-property
longest-prefix_property
longest-prefix_property'
max-fst-property
mesh-property
mu-bound-property
mu-bound-property+
mu-dec-property
mu-ge-bound-property
mu-ge-property
mu-property
mul-initial-seg-property
nat-to-incomparable-property
new_23_sig_decided_property
new_23_sig_retry_property
ni-selector-property
null-class-property
num-antecedents-property
pairs-fpf_property
per-value-property
poss-maj-property
prior-as-rec-bind-class-in-property
prior-as-rec-bind-class-in2-property
priority-select-property
property-from-l_member
pv11_p1_headers-property
r-bound-property
r-strict-bound-property
range-inf-property
range-sup-property
ranked-eo-property
rational-approx-property
rational-approx-property-ext
reg-seq-adjust-property
rel-immediate-property
reliable-env-property
remove-repeats_property
remove_leading_property
rev-append-property
rev-append-property-top
rev-append-property-top-sqle
rless-property
rless-witness-property
rroot-abs-property
run-initialization-property
run-prior-state-property
search_property
skip-first-class-property
skip-first-class-property-iff
sp-lub-property
st-lookup-property
std-component-property
std-components-property
std-initial-property
stdEO-E-property
str-to-nat-plus-property
strict-majority-or-max-property
strict-majority-property
stump'_property
taba-property
tagged-true-property
trans-id-property
trans-id-property
tsqrt-property
urec-level-property
values-for-distinct-property
weak-antecedent-function-property
weak-antecedent-surjection-property

PROPERTY1

prev top next

bag-moebius-property1
bag-remove1-property1
consensus-accum-num-property1
es-cut-at-property1
rational-approx-property1
reliable-env-property1

PROPERTY2

prev top next

bag-drop-property2
bigger-int-property2
consensus-accum-num-property2
deq_property2
es-fix_property2
es-local-pred-property2
first-choosable-property2
glues-property2
list-max-property2
local-class-predicate-property2
longest-prefix_property2
mu-ge-property2
mu-property2
mul-initial-seg-property2
rational-approx-property2
reliable-env-property2
remove_leading_property2

PROPERTY3

prev top next

consensus-accum-num-property3

PROPORTIONAL

prev top next

proportional-round
proportional-round_wf

PROPOSAL

prev top next

new_23_sig_Proposal
new_23_sig_Proposal-program
new_23_sig_Proposal-program_wf
new_23_sig_Proposal_wf
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_replica_state_from_proposal
new_23_sig_replica_state_from_proposal_fun
new_23_sig_when_new_proposal
new_23_sig_when_new_proposal_wf
pv11_p1_same_proposal
pv11_p1_same_proposal_wf
pv11_p1_valid-proposal
pv11_p1_valid-proposal-forward
pv11_p1_valid-proposal-transitivity
pv11_p1_valid-proposal-transitivity-forward
pv11_p1_valid-proposal_wf

PROPOSAL3

prev top next

pv11_p1_ldr_fun_proposal3
pv11_p1_ldr_proposal3

PROPOSALS

prev top next

pv11_p1_init_proposals
pv11_p1_init_proposals_wf
pv11_p1_update_proposals
pv11_p1_update_proposals_wf
pv11_p1_valid-proposals
pv11_p1_valid-proposals_wf

PROPOSE

prev top next

new_23_sig_propose'base
new_23_sig_propose'base-program
new_23_sig_propose'base-program_wf
new_23_sig_propose'base_wf
pv11_p1_ldr_fun_mem_propose
pv11_p1_ldr_fun_state_propose_pred
pv11_p1_ldr_mem_propose
pv11_p1_ldr_state_propose_pred
pv11_p1_leader_propose
pv11_p1_leader_propose_wf
pv11_p1_on_propose
pv11_p1_on_propose_wf
pv11_p1_propose'base
pv11_p1_propose'base-program
pv11_p1_propose'base-program_wf
pv11_p1_propose'base_wf

PROPOSE2

prev top next

pv11_p1_ldr_fun_mem_propose2
pv11_p1_ldr_mem_propose2

PROPOSITION

prev top next

proposition 3

PROTOCOL1

prev top next

fresh-sig-protocol1
fresh-sig-protocol1_property
fresh-sig-protocol1_wf
ses-protocol1
ses-protocol1-legal
ses-protocol1-legal_wf
ses-protocol1-thread
ses-protocol1-thread_wf
ses-protocol1_wf

PROVEABLE

prev top next

mFOL-proveable
mFOL-proveable-evidence
mFOL-proveable-formula
mFOL-proveable-formula-evidence
mFOL-proveable-formula-evidence-ext
mFOL-proveable-formula-evidence-ext2
mFOL-proveable-formula_wf
mFOL-proveable_wf
proveable
proveable_wf

PRP

prev top next

is-list-if-has-value-hv-prp

PRUN

prev top next

pRun
pRun-System-invariant
pRun-intransit-invariant
pRun-invariant1
pRun-invariant2
pRun-invariant3
pRun_functionality
pRun_wf
pRun_wf2

PRUN2

prev top next

pRun2
pRun2_wf

PRUNINFO

prev top next

pRunInfo
pRunInfo_wf

PRUNTYPE

prev top next

pRunType
pRunType_wf

PSTAR

prev top next

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

PSUB

prev top next

prank-psub
psub
psub-same
psub_antisymmetry
psub_transitivity
psub_weakening
psub_wf

PTR

prev top next

DVp_Pointer-ptr
DVp_Pointer-ptr_wf
st-ptr
st-ptr-wf2
st-ptr_wf

PUBLIC

prev top next

public-decls
ses-D-public
ses-D-public_wf
ses-private-not-public
ses-public-key
ses-public-key-atoms
ses-public-key_wf
ses-public-not-private
ses-public-one-one

PULLBACK

prev top next

chain-pullback

PUSH

prev top next

push-spread-into-ifthenelse

PUSHDOWN

prev top next

assert-pushdown-test

PUSHDOWNC

prev top next

assert-pushdownC-test

PUSHUP

prev top next

assert_pushup_example

PV

prev top next

pv11_p1_acc_fun_p2a_pv

PVALS

prev top next

pv11_p1_inc_acc_pvals_fun
pv11_p1_scout_state_subset_pvals

PVALUE

prev top next

pv11_p1_pvalue
pv11_p1_pvalue_from_p2a
pv11_p1_pvalue_wf
pv11_p1_same_pvalue
pv11_p1_same_pvalue_wf

PVALUES

prev top next

pv11_p1_consistent-pvalues
pv11_p1_consistent-pvalues_wf
pv11_p1_init_pvalues
pv11_p1_init_pvalues_wf

PVAR

prev top next

prank-pvar
pvar
pvar-name
pvar-name_wf
pvar?
pvar?_wf
pvar_wf

PW

prev top

pW-rec
pW-rec_wf
pW-sup
pW-sup_wf
pw-evenodd
pw-evenodd_wf