[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]
HALT
top next
hdf-bind-gen-halt-left
hdf-bind-gen-left-halt
hdf-halt
hdf-halt-compose2
hdf-halt_wf
hdf-halted-halt
hdf-halted-is-halt
hdf-out-halt
hdf-parallel-bind-halt-eq
hdf-parallel-bind-halt-eq-gen
hdf-parallel-halt
hdf-parallel-halt-left
hdf-parallel-halt-right
hdf-union-halt
hdf-until-halt-left
hdf-until-halt-right
hdf_ap_halt_lemma
hdf_halted_halt_red_lemma
hdf_out_halt_red_lemma
iterate-hdf-halt
no-halt-decider
HALTED
prev top next
hdf-bind-gen-halted
hdf-halted
hdf-halted-compose2
hdf-halted-compose2-iterate
hdf-halted-halt
hdf-halted-inl
hdf-halted-is-halt
hdf-halted-is-inr
hdf-halted-run
hdf-halted_wf
hdf-parallel-halted
hdf_halted_halt_red_lemma
hdf_halted_inl_red_lemma
hdf_halted_run_red_lemma
HAPPENED
prev top next
es-happened-before
es-happened-before_wf
HARMONIC
prev top next
harmonic-series-diverges
HAS
prev top next
Id-has-value
Id-has-valueall
assert-bag-has-no-repeats
assert-has-header-and-in-locs
assert-has-src
atom-sdata-has-atom
bag-has-no-repeats
bag-has-no-repeats_wf
class-value-has
class-value-has_wf
co-list-has-value
component-has-value
decide-atom-if-has-value
decide-atom2-if-has-value
decide-axiom-if-has-value
decide-inl-if-has-value
decide-inr-if-has-value
decide-int-if-has-value
decide-isatom-if-has-value
decide-isatom2-if-has-value
decide-isaxiom-if-has-value
decide-isinl-if-has-value
decide-isinr-if-has-value
decide-isint-if-has-value
decide-islambda-if-has-value
decide-ispair-if-has-value
decide-lambda-if-has-value
decide-pair-if-has-value
decomp-map-if-has-value
eo-forward-has-es-info-type
event-has
event-has*
event-has*-iff
event-has*-transitive-encrypt
event-has*_wf
event-has_functionality
event-has_wf
has-es-info-type
has-es-info-type-is-msg-has-type
has-es-info-type-subtype
has-es-info-type_wf
has-header-and-in-locs
has-header-and-in-locs_wf
has-latest-val
has-no-path
has-no-path_wf
has-src
has-src_wf
has-value
has-value-append
has-value-append-nil
has-value-band
has-value-band-type
has-value-bnot
has-value-bnot-type
has-value-bor
has-value-bor-type
has-value-equality-fix
has-value-equality-fix-bar
has-value-extensionality
has-value-if-has-value-map
has-value-ifthenelse
has-value-ifthenelse-type
has-value-implies-dec-isatom
has-value-implies-dec-isatom-2
has-value-implies-dec-isatom2
has-value-implies-dec-isatom2-2
has-value-implies-dec-isaxiom
has-value-implies-dec-isaxiom-2
has-value-implies-dec-isinl
has-value-implies-dec-isinl-2
has-value-implies-dec-isinr
has-value-implies-dec-isinr-2
has-value-implies-dec-isint
has-value-implies-dec-isint-2
has-value-implies-dec-islambda
has-value-implies-dec-islambda-2
has-value-implies-dec-ispair
has-value-implies-dec-ispair-2
has-value-is-list-approx-is-type
has-value-is-list-map-if-has-value-is-list
has-value-is-list-map-iff-has-value-is-list
has-value-is-list-of-co-list
has-value-l-last
has-value-l-last-default-list
has-value-l-last-list
has-value-last
has-value-last-list
has-value-length-member-int
has-value-length-member-list
has-value-mklist
has-value-monotonic
has-value-wf-base
has-value-wf-value-type
has-value_wf-bar
has-value_wf-partial
has-value_wf_base
has-valueall
has-valueall-append-nil
has-valueall-apply
has-valueall-cons
has-valueall-has-value
has-valueall-if-has-value-callbyvalueall
has-valueall-inl
has-valueall-inr
has-valueall-lambda
has-valueall-pair
has-valueall-single
has-valueall_wf_base
id-sdata-has-atom
is-list-if-has-value
is-list-if-has-value-decomp
is-list-if-has-value-ext
is-list-if-has-value-fun
is-list-if-has-value-fun-ax-mem
is-list-if-has-value-fun_wf
is-list-if-has-value-hv-prp
is-list-if-has-value-rec
is-list-if-has-value-rec-decomp
is-list-if-has-value-rec-map
is-list-if-has-value-rec-pair-bot
is-list-if-has-value-rec-snd
is-list-if-has-value-rec-subtype-unit
is-list-if-has-value-rec_wf
is-list-if-has-value_wf
isatom-bool-if-has-value
isatom1-bool-if-has-value
isatom2-bool-if-has-value
isaxiom-bool-if-has-value
isinl-bool-if-has-value
isinr-bool-if-has-value
isint-bool-if-has-value
islambda-bool-if-has-value
islist-iff-length-has-value
ispair-bool-if-has-value
length-nat-if-has-value
length-wf-has-value
lg-acyclic-has-source
list-if-has-value-length
list-if-has-value-length2
list-if-has-value-list_ind
list-if-has-value-rev-append
member-has-value
member-has-valueall
msg-has-type
msg-has-type-encodes
msg-has-type_wf
new_23_sig_proposal_has_header
not-exception-has-value
not-has-value-bottom
not-has-value-decidable-quot
not_has-value_decidable_on_base
process-has-value
rational-form-has-value
rational-has-value
rational-has-value2
real-has-value
real-has-valueall
real-list-has-valueall
sdata-has-atom
sdata-pair-has-atom
ses-act-has-atom
ses-flow-has
ses-flow-has*
ses-legal-thread-has*-nonce
ses-legal-thread-has*-signature
ses-legal-thread-has-atom
ses-sign-has-atom
sq_stable__has-es-info-type
sq_stable__has-value
sq_stable__has-value
sq_stable__has-valueall
sq_stable__is-list-if-has-value-fun
sqle-append-nil-if-has-value4
sum-has-value
sum-partial-has-value
sum-partial-list-has-value
value-type-has-value
valueall-type-has-value
valueall-type-has-valueall
HASLEFT
prev top next
es-interface-or-hasleft
oob-hasleft
oob-hasleft_wf
HASLINK
prev top next
haslink
haslink_wf
HASLOC
prev top next
assert-hasloc
hasloc
hasloc_wf
lnk-decl_wf-hasloc
subtype-set-hasloc
HASRIGHT
prev top next
es-interface-or-hasright
oob-hasright
oob-hasright_wf
HAVE
prev top next
separated-partitions-have-common-refinement
HD
prev top next
bag-member-iff-hd
bag-member-implies-hd-append
before-hd
comb_for_hd_wf_listp
find-hd-filter
hd
hd-append
hd-append-sq
hd-as-reduce
hd-before
hd-es-interval
hd-es-le-before
hd-es-le-before-is-first
hd-filter
hd-map
hd-map-spread
hd-nil
hd-reverse
hd-stream-zip
hd-wf-not-null
hd?
hd?_wf
hd_l_interval
hd_map
hd_member
hd_two_swap_permr
hd_wf
hd_wf_listp
l_index_hd
permr_hd_cancel
pred-hd-es-open-interval
reduce_hd_cons_lemma
reject_cons_hd
reject_cons_hd_sq
s-hd
s-hd_wf
s_hd_cons_lemma
select-as-hd
select-cons-hd
select_cons_hd
single-valued-bag-hd
HDATAFLOW
prev top next
class-of-hdataflow
hdataflow
hdataflow-class
hdataflow-class_wf
hdataflow-equal
hdataflow-ext
hdataflow-value-type
hdataflow-valueall-type
hdataflow_subtype
hdataflow_wf
iterate-hdataflow
iterate-hdataflow_wf
HDF
prev top next
base-class-program-wf-hdf
bind-class-program-eq-hdf
bind-class-program-wf-hdf
class-at-program-eq-hdf
class-at-program-wf-hdf
eclass1-program-wf-hdf
eclass2-program-eq-hdf
eclass2-program-wf-hdf
hdf-ap
hdf-ap-inl
hdf-ap-invariant
hdf-ap-invariant2
hdf-ap-only-headers
hdf-ap-only-headers2
hdf-ap-run
hdf-ap-single-valued-except
hdf-ap-single-valued-except2
hdf-ap_wf
hdf-at-locs
hdf-at-locs_wf
hdf-base
hdf-base-ap
hdf-base-ap-fst
hdf-base-transformation1
hdf-base-transformation1-base
hdf-base-transformation2
hdf-base_wf
hdf-bind
hdf-bind-ap
hdf-bind-as-gen
hdf-bind-compose1-left
hdf-bind-gen
hdf-bind-gen-ap
hdf-bind-gen-ap-eq
hdf-bind-gen-compose1-left
hdf-bind-gen-halt-left
hdf-bind-gen-halted
hdf-bind-gen-left-halt
hdf-bind-gen_wf
hdf-bind_wf
hdf-buffer
hdf-buffer-transformation2
hdf-buffer-transformation3
hdf-buffer2
hdf-buffer2_wf
hdf-buffer_wf
hdf-cbva-simple
hdf-cbva-simple_wf
hdf-comb2
hdf-comb2_wf
hdf-comb3
hdf-comb3_wf
hdf-compose0
hdf-compose0-bag
hdf-compose0-bag_wf
hdf-compose0-transformation1
hdf-compose0-transformation2
hdf-compose0_wf
hdf-compose1
hdf-compose1-ap
hdf-compose1-transformation0
hdf-compose1-transformation0-2
hdf-compose1-transformation1
hdf-compose1-transformation1-2
hdf-compose1-transformation2
hdf-compose1-transformation3
hdf-compose1_wf
hdf-compose2
hdf-compose2'
hdf-compose2-ap
hdf-compose2-transformation1
hdf-compose2-transformation1-2-0
hdf-compose2-transformation1-2-1
hdf-compose2-transformation1-2-2
hdf-compose2-transformation1-2-3
hdf-compose2-transformation2
hdf-compose2_wf
hdf-compose3
hdf-compose3_wf
hdf-halt
hdf-halt-compose2
hdf-halt_wf
hdf-halted
hdf-halted-compose2
hdf-halted-compose2-iterate
hdf-halted-halt
hdf-halted-inl
hdf-halted-is-halt
hdf-halted-is-inr
hdf-halted-run
hdf-halted_wf
hdf-invariant
hdf-invariant_wf
hdf-memory
hdf-memory-base
hdf-memory-base2-2
hdf-memory-base2-3
hdf-memory-base3-2
hdf-memory-base3-3
hdf-memory-base4-2
hdf-memory-base4-3
hdf-memory-transformation2
hdf-memory_wf
hdf-once
hdf-once-transformation1
hdf-once-transformation2
hdf-once-transformation3
hdf-once_wf
hdf-only-headers
hdf-only-headers_wf
hdf-out
hdf-out-halt
hdf-out-inl
hdf-out-run
hdf-out_wf
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
hdf-prior
hdf-prior_wf
hdf-rec-bind
hdf-rec-bind_wf
hdf-return
hdf-return-transformation1
hdf-return-transformation2
hdf-return_wf
hdf-run
hdf-run_wf
hdf-running
hdf-running_wf
hdf-sequence
hdf-sequence_wf
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-sqequal1
hdf-sqequal2
hdf-sqequal2-cbva
hdf-sqequal2-weak
hdf-sqequal3
hdf-sqequal3-cbva
hdf-sqequal4
hdf-sqequal6
hdf-sqequal6-1
hdf-sqequal6-2
hdf-sqequal7
hdf-sqequal8
hdf-sqequal8-2
hdf-sqequal8-3
hdf-sqequal8-4
hdf-sqequal9
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-state1-single-val
hdf-state1-single-val_wf
hdf-state_wf
hdf-transformation-test1
hdf-union
hdf-union-ap
hdf-union-eq-disju
hdf-union-halt
hdf-union_wf
hdf-until
hdf-until-ap
hdf-until-ap-fst
hdf-until-ap-snd
hdf-until-halt-left
hdf-until-halt-right
hdf-until_wf
hdf-with-state-pair-left-axiom
hdf_ap_halt_lemma
hdf_halted_halt_red_lemma
hdf_halted_inl_red_lemma
hdf_halted_run_red_lemma
hdf_out_halt_red_lemma
iter_hdf_cons_lemma
iter_hdf_nil_lemma
iterate-hdf-append
iterate-hdf-bind-simple
iterate-hdf-buffer-simple
iterate-hdf-buffer2-simple
iterate-hdf-halt
loop-class-state-program-wf-hdf
mk-hdf
mk-hdf_wf
msg-interface-hdf
msg-interface-hdf_wf
on-loc-class-program-eq-hdf
on-loc-class-program-wf-hdf
once-class-program-eq-hdf
once-class-program-wf-hdf
parallel-class-program-eq-hdf
parallel-class-program-wf-hdf
return-loc-bag-class-program-wf-hdf
simple-hdf-bind
simple-hdf-bind_wf
simple-hdf-buffer
simple-hdf-buffer2
simple-hdf-buffer2_wf
simple-hdf-buffer_wf
single-valued-class-implies-hdf
state-class1-program-wf-hdf
verify-class-program-wf-hdf
HDP
prev top next
hdp
hdp_wf
HDR
prev top next
message-constraint-swap-hdr
message-constraint-swap-hdr_wf
HDRMAKEMSG
prev top next
hdrmakeMsg_lemma
HDRMKMSG
prev top next
hdrmkmsg_lemma
HDS
prev top next
eq_cons_imp_eq_hds
HDTL
prev top next
for_hdtl
for_hdtl_cons_lemma
for_hdtl_nil_lemma
for_hdtl_wf
HEAD
prev top next
bag-drop-head
pcw-pp-head
pcw-pp-head_wf
HEADER
prev top next
----- header property --------------------
assert-has-header-and-in-locs
assert-test-msg-header-and-loc
eo-forward-header
es-header
es-header_wf
has-header-and-in-locs
has-header-and-in-locs_wf
header-type-spec
header-type-spec_wf
msg-header
msg-header_wf
new_23_sig_proposal_has_header
new_23_sig_vote_with_ballot-header
single-valued-on-header
single-valued-on-header_wf
subtype_rel_header-type-spec
test-msg-header-and-loc
test-msg-header-and-loc_wf
HEADERS
prev top next
------ CLK - headers ------
------ OARcast - headers ------
------ new_23_sig - headers ------
------ nysiad - headers ------
------ pv11_p1 - headers ------
CLK_headers
CLK_headers_fun
CLK_headers_fun_wf
CLK_headers_internal
CLK_headers_internal_wf
CLK_headers_no_inputs
CLK_headers_no_inputs_types
CLK_headers_no_inputs_types_wf
CLK_headers_no_inputs_wf
CLK_headers_no_rep
CLK_headers_no_rep_wf
CLK_headers_type
CLK_headers_type_wf
CLK_headers_wf
OARcast_headers
OARcast_headers_fun
OARcast_headers_fun_wf
OARcast_headers_internal
OARcast_headers_internal_wf
OARcast_headers_no_inputs
OARcast_headers_no_inputs_types
OARcast_headers_no_inputs_types_wf
OARcast_headers_no_inputs_wf
OARcast_headers_no_rep
OARcast_headers_no_rep_wf
OARcast_headers_type
OARcast_headers_type_wf
OARcast_headers_wf
base-headers-msg-val
base-headers-msg-val-es-sv
base-headers-msg-val-loc
base-headers-msg-val-loc_wf
base-headers-msg-val-single-val
base-headers-msg-val_wf
class-only-headers
class-only-headers_wf
delivered-with-headers
delivered-with-headers-no_repeats
delivered-with-headers_wf
hdf-ap-only-headers
hdf-only-headers
hdf-only-headers_wf
local-class-only-headers
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
nysiad_headers
nysiad_headers_fun
nysiad_headers_fun_wf
nysiad_headers_internal
nysiad_headers_internal_wf
nysiad_headers_no_inputs
nysiad_headers_no_inputs_types
nysiad_headers_no_inputs_types_wf
nysiad_headers_no_inputs_wf
nysiad_headers_no_rep
nysiad_headers_no_rep_wf
nysiad_headers_type
nysiad_headers_type_wf
nysiad_headers_wf
pv11_p1_headers
pv11_p1_headers-property
pv11_p1_headers_fun
pv11_p1_headers_fun_wf
pv11_p1_headers_internal
pv11_p1_headers_internal_wf
pv11_p1_headers_no_inputs
pv11_p1_headers_no_inputs_types
pv11_p1_headers_no_inputs_types_wf
pv11_p1_headers_no_inputs_wf
pv11_p1_headers_no_rep
pv11_p1_headers_no_rep_wf
pv11_p1_headers_type
pv11_p1_headers_type_wf
pv11_p1_headers_wf
HEADERS2
prev top next
hdf-ap-only-headers2
HEIGHT
prev top next
co-value-height
co-value-height_wf
rec-value-height
rec-value-height_wf
HGP
prev top next
oal_hgp
oal_hgp_subtype_oal_grp
oal_hgp_wf
oal_hgp_wf2
HGRP
prev top next
hgrp_car
hgrp_car_properties
hgrp_car_wf
hgrp_of_ocgrp
hgrp_of_ocgrp_wf
hgrp_of_ocgrp_wf2
int_hgrp_el
int_hgrp_el_wf
int_hgrp_to_nat
int_hgrp_to_nat_wf
oalist_hgrp_eqs
HI
prev top next
itop_unroll_hi
mon_itop_unroll_hi
rng_sum_unroll_hi
HIDDEN
prev top next
test-hidden-ap
HIDDENFIX
prev top next
hiddenfix
HIDE
prev top next
!hyp_hide
hide
hide_wf
HINT
prev top next
hint
hint_wf
HIST
prev top next
es-hist
es-hist-is-append
es-hist-is-concat
es-hist-iseg
es-hist-last
es-hist-one-one
es-hist-partition
es-hist_wf
iseg-es-hist
last-es-hist
member-es-hist
null-es-hist
HISTORY
prev top next
es-history-accum
es-interface-history
es-interface-history-first
es-interface-history-iseg
es-interface-history-pred
es-interface-history-prior
es-interface-history_wf
iseg-global-order-history
member-es-interface-history
nonempty-es-interface-history
run-event-history
run-event-history_wf
stdEO-event-history
HOLE
prev top next
general-pigeon-hole
pigeon-hole
pigeon-hole-implies
pigeon-hole-implies-ext
HOM
prev top next
alg_hom_p
alg_hom_p_wf
algebra_hom
algebra_hom_properties
algebra_hom_wf
bag-summation-hom
comb_for_compose_wf_for_mon_hom
compose_wf_for_mon_hom
dist_hom_over_mon_for
dist_hom_over_mset_for
fps-elim-hom
grp_hom_formation
grp_hom_inv
ident_mon_hom_shift
inj_mon_hom
inj_mon_hom_properties
inj_mon_hom_wf
int-to-ring-hom
inverse_grp_sig_hom_shift
mcopower_inj_is_hom
mcopower_umap_is_hom
module_act_grp_hom_l
module_act_is_grp_hom
module_hom
module_hom_action
module_hom_is_grp_hom
module_hom_p
module_hom_p_wf
module_hom_plus
module_hom_properties
module_hom_wf
mon_hom_inj_p
mon_hom_inj_p_wf
mon_hom_p_comp
mon_hom_p_id
mon_nat_op_hom_swap
mon_when_hom_swap
mon_when_is_hom
monoid_hom
monoid_hom_id
monoid_hom_op
monoid_hom_p
monoid_hom_p_wf
monoid_hom_properties
monoid_hom_wf
mset_sum_bor_mon_hom
mset_union_bor_mon_hom
nat_int_grp_sig_hom
nat_op_mon_hom_1
nat_op_mon_hom_2
oal_inj_mon_hom
omral_alg_umap_is_hom
ring_hom
ring_hom_wf
ring_quot_hom
rng_hom_minus
rng_hom_p
rng_hom_p_wf
rng_hom_zero
sq_stable__alg_hom_p
sq_stable__module_hom_p
sq_stable__monoid_hom_p
tidentity_wf_for_mon_hom
zhgrp_op_mon_hom_1
zhgrp_to_nat_is_hom
HOMOGENEOUS
prev top next
homogeneous
homogeneous_wf
le2-homogeneous
non-homogeneous-add
HONEST
prev top next
ses-honest
ses-honest_wf
ses-honest_witness
HTFOR
prev top next
mon_htfor
mon_htfor_cons_lemma
mon_htfor_nil_lemma
mon_htfor_wf
HUBER
prev top next
Theorem 6.2 in Bezem,Coquand,Huber
HV
prev top next
is-list-if-has-value-hv-prp
HYP
prev top next
!hyp_hide
double-negation-hyp-elim
gen_hyp_tp
minimal-double-negation-hyp-elim
HYPNUM
prev top
mRuleallE-hypnum
mRuleallE-hypnum_wf
mRuleandE-hypnum
mRuleandE-hypnum_wf
mRuleexistsE-hypnum
mRuleexistsE-hypnum_wf
mRuleimpE-hypnum
mRuleimpE-hypnum_wf
mRuleorE-hypnum
mRuleorE-hypnum_wf