| Global Index | 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 | _ | other | (956 entries) |
| Binder Index | 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 | _ | other | (678 entries) |
| Module Index | 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 | _ | other | (3 entries) |
| Variable Index | 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 | _ | other | (1 entry) |
| Library Index | 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 | _ | other | (12 entries) |
| Lemma Index | 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 | _ | other | (136 entries) |
| Axiom Index | 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 | _ | other | (8 entries) |
| Instance Index | 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 | _ | other | (8 entries) |
| Section Index | 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 | _ | other | (1 entry) |
| Definition Index | 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 | _ | other | (109 entries) |
Global Index
A
add_another [lemma, in Verif_triang]add_list_sublist_bounds [lemma, in Verif_triang]
add_list_nonneg [lemma, in Verif_triang]
add_list_app [lemma, in Verif_triang]
add_list_decreasing_eq [lemma, in Verif_triang]
add_list_decreasing_eq_alt [lemma, in Verif_triang]
add_list [definition, in Verif_triang]
al:103 [binder, in Verif_hash]
al:108 [binder, in Verif_hash]
al:11 [binder, in Hashfun]
al:126 [binder, in Verif_hash]
al:129 [binder, in Verif_hash]
al:130 [binder, in Verif_hash]
al:138 [binder, in Verif_hash]
al:143 [binder, in Verif_hash]
al:19 [binder, in Hashfun]
al:64 [binder, in Verif_hash]
al:65 [binder, in Verif_hash]
al:7 [binder, in Hashfun]
al:87 [binder, in Verif_triang]
append_spec [definition, in Verif_append1]
a:1 [binder, in Verif_sumarray]
a:1 [binder, in Verif_triang]
A:123 [binder, in Verif_hash]
a:21 [binder, in Verif_append1]
a:24 [binder, in Verif_append1]
a:25 [binder, in Verif_append2]
a:25 [binder, in Hashfun]
a:28 [binder, in Verif_append1]
a:3 [binder, in Verif_sumarray]
a:3 [binder, in Verif_triang]
a:38 [binder, in Verif_reverse]
A:42 [binder, in Verif_append2]
a:44 [binder, in Verif_reverse]
a:45 [binder, in Verif_append2]
A:47 [binder, in Verif_append2]
A:68 [binder, in Verif_hash]
a:8 [binder, in Verif_sumarray]
a:80 [binder, in Verif_append2]
a:86 [binder, in Verif_append1]
a:89 [binder, in Verif_append1]
a:96 [binder, in Verif_append1]
B
Bib [library]bl:122 [binder, in Verif_hash]
bl:75 [binder, in Verif_hash]
bl:88 [binder, in Verif_triang]
body_incr [lemma, in Verif_hash]
body_incr_field_address_lemma [lemma, in Verif_hash]
body_incr_list [lemma, in Verif_hash]
body_get [lemma, in Verif_hash]
body_new_table [lemma, in Verif_hash]
body_new_table_helper [lemma, in Verif_hash]
body_new_cell [lemma, in Verif_hash]
body_copy_string [lemma, in Verif_hash]
body_hash [lemma, in Verif_hash]
body_append_alter2 [lemma, in Verif_append2]
body_append_alter1 [lemma, in Verif_append1]
body_append [lemma, in Verif_append1]
body_main [lemma, in Verif_sumarray]
body_sumarray [lemma, in Verif_sumarray]
body_reverse_step [lemma, in Verif_reverse]
body_reverse [lemma, in Verif_reverse]
body_strcmp [lemma, in Verif_strlib]
body_example_call_strcpy [lemma, in Verif_strlib]
body_strcpy [lemma, in Verif_strlib]
body_strlen [lemma, in Verif_strlib]
body_main [lemma, in Verif_triang]
body_pop_and_add [lemma, in Verif_triang]
body_pop_and_add [lemma, in Verif_triang]
body_push_increasing [lemma, in Verif_triang]
body_newstack [lemma, in Verif_stack]
body_push [lemma, in Verif_stack]
body_pop [lemma, in Verif_stack]
b0:141 [binder, in Verif_hash]
b:147 [binder, in Verif_hash]
b:149 [binder, in Verif_hash]
b:2 [binder, in Verif_sumarray]
b:2 [binder, in Verif_triang]
b:25 [binder, in Verif_append1]
b:29 [binder, in Verif_append1]
b:33 [binder, in Verif_append2]
b:38 [binder, in Verif_append2]
b:39 [binder, in Verif_reverse]
b:4 [binder, in Verif_triang]
b:45 [binder, in Verif_reverse]
b:54 [binder, in Verif_append1]
b:59 [binder, in Verif_append1]
B:69 [binder, in Verif_hash]
b:90 [binder, in Verif_append1]
C
cancel_example [lemma, in Verif_strlib]CompSpecs [instance, in Verif_hash]
CompSpecs [instance, in Verif_append1]
CompSpecs [instance, in Verif_sumarray]
CompSpecs [instance, in Verif_reverse]
CompSpecs [instance, in Verif_strlib]
CompSpecs [instance, in Verif_triang]
CompSpecs [instance, in Verif_stack]
contents:10 [binder, in Verif_sumarray]
contents:11 [binder, in Verif_strlib]
contents:113 [binder, in Verif_hash]
contents:118 [binder, in Verif_hash]
contents:15 [binder, in Verif_append2]
contents:15 [binder, in Verif_append1]
contents:15 [binder, in Hashfun]
contents:17 [binder, in Hashfun]
contents:30 [binder, in Verif_hash]
contents:32 [binder, in Verif_hash]
contents:46 [binder, in Verif_append1]
contents:48 [binder, in Verif_append1]
contents:5 [binder, in Verif_sumarray]
contents:54 [binder, in Verif_append2]
contents:57 [binder, in Verif_append2]
contents:6 [binder, in Verif_strlib]
contents:73 [binder, in Verif_hash]
contents:76 [binder, in Verif_hash]
contents:78 [binder, in Verif_hash]
contents:79 [binder, in Verif_append1]
contents:85 [binder, in Verif_append1]
contents:95 [binder, in Verif_hash]
contents:99 [binder, in Verif_hash]
copy_string_spec [definition, in Verif_hash]
COUNT_TABLE.gso [axiom, in Hashfun]
COUNT_TABLE.gss [axiom, in Hashfun]
COUNT_TABLE.gempty [axiom, in Hashfun]
COUNT_TABLE.incr [axiom, in Hashfun]
COUNT_TABLE.get [axiom, in Hashfun]
COUNT_TABLE.empty [axiom, in Hashfun]
COUNT_TABLE.key [axiom, in Hashfun]
COUNT_TABLE.table [axiom, in Hashfun]
COUNT_TABLE [module, in Hashfun]
count:132 [binder, in Verif_hash]
count:137 [binder, in Verif_hash]
count:154 [binder, in Verif_hash]
count:160 [binder, in Verif_hash]
count:34 [binder, in Verif_hash]
count:39 [binder, in Verif_hash]
count:43 [binder, in Verif_hash]
count:48 [binder, in Verif_hash]
count:61 [binder, in Verif_hash]
count:85 [binder, in Verif_hash]
count:90 [binder, in Verif_hash]
cts:145 [binder, in Verif_hash]
cts:146 [binder, in Verif_hash]
cts:177 [binder, in Verif_hash]
cts:178 [binder, in Verif_hash]
cts:22 [binder, in Hashfun]
cts:24 [binder, in Hashfun]
cts:58 [binder, in Hashfun]
cts:62 [binder, in Hashfun]
c:30 [binder, in Verif_append1]
C:70 [binder, in Verif_hash]
D
data_at_isptr_example2 [lemma, in Verif_reverse]data_at_isptr_example1 [lemma, in Verif_reverse]
data_at_Vundef_example [lemma, in Verif_strlib]
data_at_Vundef_example [lemma, in Verif_strlib]
decreasing_Z1 [definition, in Verif_triang]
decreasing_Z1_aux [definition, in Verif_triang]
decreasing_Z [definition, in Verif_triang]
decreasing_nat [definition, in Verif_triang]
demonstrate_cstring2 [lemma, in Verif_strlib]
demonstrate_cstring1 [lemma, in Verif_strlib]
dest:10 [binder, in Verif_hash]
dest:14 [binder, in Verif_hash]
dest:23 [binder, in Verif_strlib]
dest:29 [binder, in Verif_strlib]
dest:51 [binder, in Verif_strlib]
dest:55 [binder, in Verif_strlib]
dl:156 [binder, in Verif_hash]
dl:162 [binder, in Verif_hash]
d:124 [binder, in Verif_hash]
E
empty_table [definition, in Hashfun]emp_lbseg [lemma, in Verif_append2]
emp_wlseg [lemma, in Verif_append2]
emp_wand_emp_left [lemma, in Verif_append2]
emp_wand_emp_right [lemma, in Verif_append2]
EqDec_string [instance, in Hashfun]
Espec:50 [binder, in Verif_reverse]
example_field_at_data_at''' [lemma, in Verif_hash]
example_field_at_data_at'' [lemma, in Verif_hash]
example_field_at_data_at' [lemma, in Verif_hash]
example_field_at_data_at [lemma, in Verif_hash]
example_split_struct [lemma, in Verif_hash]
example_call_strcpy_spec [definition, in Verif_strlib]
F
four_contents [definition, in Verif_sumarray]free_spec_example [definition, in Verif_stack]
FunTable [module, in Hashfun]
FunTable.empty [definition, in Hashfun]
FunTable.gempty [lemma, in Hashfun]
FunTable.get [definition, in Hashfun]
FunTable.gso [lemma, in Hashfun]
FunTable.gss [lemma, in Hashfun]
FunTable.incr [definition, in Hashfun]
FunTable.key [definition, in Hashfun]
FunTable.table [definition, in Hashfun]
f:127 [binder, in Verif_hash]
f:16 [binder, in Verif_sumarray]
f:71 [binder, in Verif_hash]
G
get_spec [definition, in Verif_hash]Gprog [definition, in Verif_hash]
Gprog [definition, in Verif_append1]
Gprog [definition, in Verif_sumarray]
Gprog [definition, in Verif_reverse]
Gprog [definition, in Verif_strlib]
Gprog [definition, in Verif_triang]
Gprog [definition, in Verif_stack]
gv:106 [binder, in Verif_hash]
gv:111 [binder, in Verif_hash]
gv:116 [binder, in Verif_hash]
gv:12 [binder, in Verif_sumarray]
gv:121 [binder, in Verif_hash]
gv:13 [binder, in Verif_sumarray]
gv:24 [binder, in Verif_hash]
gv:24 [binder, in Verif_stack]
gv:25 [binder, in Verif_stack]
gv:27 [binder, in Verif_hash]
gv:30 [binder, in Verif_stack]
gv:34 [binder, in Verif_stack]
gv:38 [binder, in Verif_stack]
gv:42 [binder, in Verif_stack]
gv:54 [binder, in Verif_triang]
gv:55 [binder, in Verif_triang]
gv:60 [binder, in Verif_triang]
gv:64 [binder, in Verif_triang]
gv:68 [binder, in Verif_triang]
gv:72 [binder, in Verif_triang]
gv:74 [binder, in Verif_strlib]
gv:75 [binder, in Verif_strlib]
gv:75 [binder, in Verif_triang]
gv:78 [binder, in Verif_triang]
gv:80 [binder, in Verif_hash]
gv:81 [binder, in Verif_hash]
gv:81 [binder, in Verif_triang]
gv:84 [binder, in Verif_triang]
gv:85 [binder, in Verif_triang]
gv:86 [binder, in Verif_triang]
gv:87 [binder, in Verif_hash]
gv:92 [binder, in Verif_hash]
H
hashfun [definition, in Hashfun]Hashfun [library]
hashfun_snoc [lemma, in Hashfun]
hashfun_aux_snoc [lemma, in Hashfun]
hashfun_inrange [lemma, in Hashfun]
hashfun_aux [definition, in Hashfun]
hashtable_rep_valid_pointer [lemma, in Verif_hash]
hashtable_rep_local_facts [lemma, in Verif_hash]
hashtable_rep [definition, in Verif_hash]
hashtable_get_unfold [lemma, in Hashfun]
hashtable_incr [definition, in Hashfun]
hashtable_get [definition, in Hashfun]
hashtable_contents [definition, in Hashfun]
hash_spec [definition, in Verif_hash]
Hello [definition, in Verif_strlib]
Hello' [definition, in Verif_strlib]
hi:91 [binder, in Verif_triang]
HRE:57 [binder, in Verif_reverse]
hs:51 [binder, in Verif_append1]
H0:13 [binder, in Verif_strlib]
H0:8 [binder, in Verif_strlib]
H1:14 [binder, in Verif_strlib]
H1:9 [binder, in Verif_strlib]
h:1 [binder, in Hashfun]
H:12 [binder, in Verif_strlib]
h:176 [binder, in Verif_hash]
h:18 [binder, in Verif_reverse]
h:18 [binder, in Hashfun]
h:27 [binder, in Hashfun]
h:50 [binder, in Verif_append1]
h:53 [binder, in Verif_reverse]
H:58 [binder, in Verif_reverse]
h:6 [binder, in Verif_reverse]
H:7 [binder, in Verif_strlib]
h:9 [binder, in Verif_reverse]
I
il:13 [binder, in Verif_stack]il:15 [binder, in Verif_stack]
il:17 [binder, in Verif_stack]
il:20 [binder, in Verif_stack]
il:22 [binder, in Verif_stack]
il:29 [binder, in Verif_stack]
il:33 [binder, in Verif_stack]
il:37 [binder, in Verif_stack]
il:38 [binder, in Verif_triang]
il:41 [binder, in Verif_stack]
il:43 [binder, in Verif_triang]
il:45 [binder, in Verif_triang]
il:47 [binder, in Verif_triang]
il:50 [binder, in Verif_triang]
il:52 [binder, in Verif_triang]
il:59 [binder, in Verif_triang]
il:63 [binder, in Verif_triang]
il:67 [binder, in Verif_triang]
il:71 [binder, in Verif_triang]
il:8 [binder, in Verif_stack]
il:80 [binder, in Verif_triang]
il:83 [binder, in Verif_triang]
il:89 [binder, in Verif_triang]
il:93 [binder, in Verif_triang]
il:94 [binder, in Verif_triang]
implies_and_adjoint [lemma, in Verif_append2]
incr_spec [definition, in Verif_hash]
incr_list_spec [definition, in Verif_hash]
IntHashTable [module, in Hashfun]
IntHashTable.empty [definition, in Hashfun]
IntHashTable.empty_invariant [lemma, in Hashfun]
IntHashTable.gempty [lemma, in Hashfun]
IntHashTable.get [definition, in Hashfun]
IntHashTable.gso [lemma, in Hashfun]
IntHashTable.gss [lemma, in Hashfun]
IntHashTable.hashtable_invariant [definition, in Hashfun]
IntHashTable.incr [definition, in Hashfun]
IntHashTable.incr_invariant [lemma, in Hashfun]
IntHashTable.key [definition, in Hashfun]
IntHashTable.table [definition, in Hashfun]
Int_repr_eq_mod [lemma, in Hashfun]
iter_sepcon_split3 [lemma, in Verif_hash]
iter_sepcon_listrep_local_facts [lemma, in Verif_hash]
i:10 [binder, in Verif_strlib]
i:125 [binder, in Verif_hash]
i:14 [binder, in Verif_sumarray]
i:15 [binder, in Verif_sumarray]
i:18 [binder, in Verif_sumarray]
i:28 [binder, in Verif_stack]
i:29 [binder, in Hashfun]
i:31 [binder, in Hashfun]
i:32 [binder, in Verif_stack]
i:34 [binder, in Verif_triang]
i:36 [binder, in Verif_stack]
i:40 [binder, in Verif_stack]
i:45 [binder, in Verif_strlib]
i:46 [binder, in Verif_strlib]
i:47 [binder, in Verif_strlib]
i:5 [binder, in Verif_strlib]
i:58 [binder, in Verif_strlib]
i:58 [binder, in Verif_triang]
i:59 [binder, in Verif_strlib]
i:59 [binder, in Hashfun]
i:62 [binder, in Verif_triang]
i:63 [binder, in Verif_strlib]
i:66 [binder, in Verif_triang]
i:68 [binder, in Verif_strlib]
i:70 [binder, in Verif_triang]
i:72 [binder, in Verif_strlib]
i:73 [binder, in Verif_strlib]
i:9 [binder, in Verif_hash]
i:95 [binder, in Verif_triang]
i:96 [binder, in Verif_triang]
i:97 [binder, in Verif_triang]
J
j:42 [binder, in Hashfun]j:55 [binder, in Hashfun]
j:69 [binder, in Verif_strlib]
j:70 [binder, in Hashfun]
K
key:131 [binder, in Verif_hash]key:136 [binder, in Verif_hash]
key:153 [binder, in Verif_hash]
key:159 [binder, in Verif_hash]
key:33 [binder, in Verif_hash]
key:38 [binder, in Verif_hash]
key:42 [binder, in Verif_hash]
key:46 [binder, in Verif_hash]
key:60 [binder, in Verif_hash]
key:84 [binder, in Verif_hash]
key:89 [binder, in Verif_hash]
kp:135 [binder, in Verif_hash]
kp:152 [binder, in Verif_hash]
kp:158 [binder, in Verif_hash]
kp:37 [binder, in Verif_hash]
kp:47 [binder, in Verif_hash]
k':51 [binder, in Hashfun]
k:37 [binder, in Hashfun]
k:39 [binder, in Hashfun]
k:43 [binder, in Hashfun]
k:46 [binder, in Hashfun]
k:47 [binder, in Hashfun]
k:49 [binder, in Hashfun]
k:52 [binder, in Hashfun]
k:53 [binder, in Hashfun]
k:56 [binder, in Hashfun]
k:61 [binder, in Hashfun]
k:63 [binder, in Hashfun]
k:65 [binder, in Hashfun]
k:67 [binder, in Hashfun]
k:68 [binder, in Hashfun]
k:71 [binder, in Hashfun]
K:92 [binder, in Verif_triang]
L
lbseg [definition, in Verif_append2]lbseg_lbseg [lemma, in Verif_append2]
listboxrep [definition, in Verif_hash]
listboxrep [definition, in Verif_append2]
listboxrep_traverse32 [lemma, in Verif_hash]
listboxrep_traverse [lemma, in Verif_hash]
listbox_lbseg [lemma, in Verif_append2]
listcell_fold [lemma, in Verif_hash]
listrep [definition, in Verif_hash]
listrep [definition, in Verif_append1]
listrep [definition, in Verif_reverse]
listrep [definition, in Verif_triang]
listrep [definition, in Verif_stack]
listrep_traverse_finish [lemma, in Verif_hash]
listrep_traverse_step_example [lemma, in Verif_hash]
listrep_traverse_step [lemma, in Verif_hash]
listrep_traverse_start [lemma, in Verif_hash]
listrep_fold [lemma, in Verif_hash]
listrep_valid_pointer [lemma, in Verif_hash]
listrep_local_prop [lemma, in Verif_hash]
listrep_nonnull [lemma, in Verif_append1]
listrep_null [lemma, in Verif_append1]
listrep_valid_pointer [lemma, in Verif_append1]
listrep_local_facts [lemma, in Verif_append1]
listrep_len_ge2_address_different [lemma, in Verif_reverse]
listrep_len_ge2_fact [lemma, in Verif_reverse]
listrep_valid_pointer [lemma, in Verif_reverse]
listrep_valid_pointer_example [lemma, in Verif_reverse]
listrep_local_facts [lemma, in Verif_reverse]
listrep_facts_example [lemma, in Verif_reverse]
listrep_facts_example [lemma, in Verif_reverse]
listrep_valid_pointer [lemma, in Verif_triang]
listrep_local_prop [lemma, in Verif_triang]
listrep_valid_pointer [lemma, in Verif_stack]
listrep_local_prop [lemma, in Verif_stack]
listrep2lseg [lemma, in Verif_append1]
list_cell_valid_pointer [definition, in Verif_hash]
list_cell_local_facts [definition, in Verif_hash]
list_cell [definition, in Verif_hash]
list_incr [definition, in Hashfun]
list_get [definition, in Hashfun]
loopy_lseg_no_connection [lemma, in Verif_append1]
loopy_lseg_not_bad [lemma, in Verif_append1]
lo:28 [binder, in Hashfun]
lo:90 [binder, in Verif_triang]
lseg [definition, in Verif_append1]
lseg_lseg_inv [lemma, in Verif_append1]
lseg_listrep_equiv [lemma, in Verif_append1]
lseg_list [lemma, in Verif_append1]
lseg_lseg [lemma, in Verif_append1]
lseg_maybe_loop [lemma, in Verif_append1]
lseg2listrep [lemma, in Verif_append1]
lseg2wlseg [lemma, in Verif_append2]
l:41 [binder, in Verif_reverse]
l:49 [binder, in Verif_reverse]
M
main_spec [definition, in Verif_sumarray]main_spec [definition, in Verif_triang]
malloc_spec_example [definition, in Verif_stack]
modus_ponens_wand_from_adjoint [lemma, in Verif_append2]
N
N [definition, in Hashfun]nat_sub_add_yuck [lemma, in Verif_triang]
newstack_spec [definition, in Verif_triang]
newstack_spec [definition, in Verif_stack]
new_cell_spec [definition, in Verif_hash]
new_table_spec [definition, in Verif_hash]
next:35 [binder, in Verif_hash]
next:40 [binder, in Verif_hash]
next:44 [binder, in Verif_hash]
next:86 [binder, in Verif_hash]
next:91 [binder, in Verif_hash]
nt_lseg_list [lemma, in Verif_append1]
nt_lseg_nt_lseg [lemma, in Verif_append1]
nt_lseg [definition, in Verif_append1]
N_eq [lemma, in Hashfun]
n:11 [binder, in Verif_hash]
n:11 [binder, in Verif_triang]
n:14 [binder, in Verif_triang]
n:15 [binder, in Verif_hash]
n:15 [binder, in Verif_triang]
n:17 [binder, in Verif_triang]
n:18 [binder, in Verif_triang]
n:20 [binder, in Verif_triang]
n:21 [binder, in Verif_triang]
n:22 [binder, in Verif_triang]
n:24 [binder, in Verif_strlib]
n:30 [binder, in Verif_strlib]
n:35 [binder, in Verif_triang]
n:36 [binder, in Verif_triang]
n:37 [binder, in Verif_triang]
n:48 [binder, in Verif_strlib]
n:49 [binder, in Verif_strlib]
n:5 [binder, in Verif_triang]
n:52 [binder, in Verif_strlib]
n:56 [binder, in Verif_strlib]
n:60 [binder, in Verif_strlib]
n:64 [binder, in Verif_strlib]
n:74 [binder, in Verif_triang]
n:77 [binder, in Verif_triang]
n:8 [binder, in Verif_triang]
P
pop_and_add_spec [definition, in Verif_triang]pop_spec [definition, in Verif_triang]
pop_spec [definition, in Verif_stack]
Postscript [library]
Preface [library]
prog_correct [lemma, in Verif_sumarray]
push_increasing_spec [definition, in Verif_triang]
push_spec [definition, in Verif_triang]
push_spec [definition, in Verif_stack]
p':133 [binder, in Verif_hash]
p':49 [binder, in Verif_hash]
p':62 [binder, in Verif_hash]
P':9 [binder, in Verif_append2]
p0:142 [binder, in Verif_hash]
P:1 [binder, in Verif_append2]
p:11 [binder, in Verif_reverse]
p:112 [binder, in Verif_hash]
p:117 [binder, in Verif_hash]
P:12 [binder, in Verif_append2]
p:128 [binder, in Verif_hash]
p:13 [binder, in Verif_reverse]
p:134 [binder, in Verif_hash]
p:14 [binder, in Verif_stack]
p:140 [binder, in Verif_hash]
p:144 [binder, in Verif_hash]
p:148 [binder, in Verif_hash]
p:15 [binder, in Verif_reverse]
p:150 [binder, in Verif_hash]
p:151 [binder, in Verif_hash]
p:157 [binder, in Verif_hash]
p:16 [binder, in Verif_stack]
p:163 [binder, in Verif_hash]
p:167 [binder, in Verif_hash]
p:169 [binder, in Verif_hash]
p:17 [binder, in Verif_reverse]
p:171 [binder, in Verif_hash]
p:173 [binder, in Verif_hash]
p:18 [binder, in Verif_stack]
p:2 [binder, in Verif_append1]
p:2 [binder, in Verif_reverse]
p:20 [binder, in Verif_reverse]
p:21 [binder, in Verif_stack]
p:22 [binder, in Verif_reverse]
p:23 [binder, in Verif_stack]
p:24 [binder, in Verif_reverse]
p:26 [binder, in Verif_reverse]
p:26 [binder, in Verif_stack]
p:27 [binder, in Verif_stack]
p:28 [binder, in Verif_hash]
p:28 [binder, in Verif_reverse]
p:3 [binder, in Verif_stack]
p:31 [binder, in Verif_stack]
P:33 [binder, in Verif_triang]
p:35 [binder, in Verif_stack]
p:36 [binder, in Verif_hash]
p:39 [binder, in Verif_triang]
p:39 [binder, in Verif_stack]
P:4 [binder, in Verif_append2]
p:41 [binder, in Verif_hash]
P:43 [binder, in Verif_append2]
p:43 [binder, in Verif_append1]
p:44 [binder, in Verif_triang]
p:45 [binder, in Verif_hash]
p:45 [binder, in Verif_append1]
p:46 [binder, in Verif_triang]
P:48 [binder, in Verif_append2]
p:48 [binder, in Verif_triang]
p:5 [binder, in Verif_stack]
p:50 [binder, in Verif_hash]
p:51 [binder, in Verif_triang]
p:53 [binder, in Verif_triang]
p:56 [binder, in Verif_triang]
p:57 [binder, in Verif_hash]
p:57 [binder, in Verif_triang]
p:59 [binder, in Verif_hash]
P:6 [binder, in Verif_append2]
p:61 [binder, in Verif_triang]
p:62 [binder, in Verif_strlib]
p:63 [binder, in Verif_hash]
p:65 [binder, in Verif_triang]
p:66 [binder, in Verif_strlib]
p:67 [binder, in Verif_hash]
p:69 [binder, in Verif_triang]
p:7 [binder, in Verif_stack]
p:70 [binder, in Verif_strlib]
p:74 [binder, in Verif_hash]
p:77 [binder, in Verif_hash]
p:79 [binder, in Verif_hash]
P:8 [binder, in Verif_append2]
p:8 [binder, in Verif_reverse]
p:82 [binder, in Verif_hash]
p:9 [binder, in Verif_stack]
p:93 [binder, in Verif_hash]
p:94 [binder, in Verif_hash]
p:98 [binder, in Verif_hash]
Q
Q':11 [binder, in Verif_append2]Q:10 [binder, in Verif_append2]
Q:13 [binder, in Verif_append2]
q:139 [binder, in Verif_hash]
q:19 [binder, in Verif_stack]
Q:2 [binder, in Verif_append2]
q:29 [binder, in Verif_reverse]
Q:44 [binder, in Verif_append2]
Q:49 [binder, in Verif_append2]
q:49 [binder, in Verif_triang]
Q:5 [binder, in Verif_append2]
Q:7 [binder, in Verif_append2]
q:71 [binder, in Verif_strlib]
R
reverse_spec [definition, in Verif_reverse]rsh:22 [binder, in Verif_strlib]
rsh:28 [binder, in Verif_strlib]
r0:102 [binder, in Verif_hash]
r0:107 [binder, in Verif_hash]
R:14 [binder, in Verif_append2]
r:14 [binder, in Verif_append1]
r:155 [binder, in Verif_hash]
r:161 [binder, in Verif_hash]
R:3 [binder, in Verif_append2]
R:50 [binder, in Verif_append2]
r:54 [binder, in Verif_reverse]
r:66 [binder, in Verif_hash]
S
sh1:33 [binder, in Verif_strlib]sh1:39 [binder, in Verif_strlib]
sh2:34 [binder, in Verif_strlib]
sh2:40 [binder, in Verif_strlib]
sh:15 [binder, in Verif_strlib]
sh:18 [binder, in Verif_strlib]
sh:4 [binder, in Verif_sumarray]
sh:61 [binder, in Verif_strlib]
sh:65 [binder, in Verif_strlib]
sh:67 [binder, in Verif_strlib]
sh:9 [binder, in Verif_sumarray]
sigma:1 [binder, in Verif_append1]
sigma:1 [binder, in Verif_reverse]
sigma:101 [binder, in Verif_hash]
sigma:105 [binder, in Verif_hash]
sigma:110 [binder, in Verif_hash]
sigma:115 [binder, in Verif_hash]
sigma:12 [binder, in Verif_reverse]
sigma:120 [binder, in Verif_hash]
sigma:14 [binder, in Verif_reverse]
sigma:16 [binder, in Verif_reverse]
sigma:21 [binder, in Verif_reverse]
sigma:21 [binder, in Hashfun]
sigma:23 [binder, in Verif_hash]
sigma:23 [binder, in Verif_reverse]
sigma:23 [binder, in Hashfun]
sigma:25 [binder, in Verif_reverse]
sigma:26 [binder, in Verif_hash]
sigma:26 [binder, in Hashfun]
sigma:27 [binder, in Verif_reverse]
sigma:30 [binder, in Hashfun]
sigma:42 [binder, in Verif_append1]
sigma:44 [binder, in Verif_append1]
sigma:51 [binder, in Verif_hash]
sigma:51 [binder, in Verif_reverse]
sigma:56 [binder, in Verif_hash]
sigma:58 [binder, in Verif_hash]
sigma:97 [binder, in Verif_hash]
singleton_wlseg [lemma, in Verif_append2]
singleton_nt_lseg' [lemma, in Verif_append1]
singleton_nt_lseg [lemma, in Verif_append1]
singleton_lseg [lemma, in Verif_append1]
size:11 [binder, in Verif_sumarray]
size:6 [binder, in Verif_sumarray]
src:12 [binder, in Verif_hash]
src:16 [binder, in Verif_hash]
src:25 [binder, in Verif_strlib]
src:31 [binder, in Verif_strlib]
stack [definition, in Verif_triang]
stack [definition, in Verif_stack]
stack_valid_pointer [lemma, in Verif_triang]
stack_local_prop [lemma, in Verif_triang]
stack_valid_pointer [lemma, in Verif_stack]
stack_local_prop [lemma, in Verif_stack]
strcmp_spec [definition, in Verif_hash]
strcmp_spec [definition, in Verif_strlib]
strcpy_spec [definition, in Verif_hash]
strcpy_else_clause [lemma, in Verif_strlib]
strcpy_then_clause [lemma, in Verif_strlib]
strcpy_spec [definition, in Verif_strlib]
StringDemo [section, in Verif_strlib]
StringDemo.p [variable, in Verif_strlib]
stringlit_1_contents [definition, in Verif_strlib]
string_to_list_byte [definition, in Verif_strlib]
strlen_spec [definition, in Verif_hash]
strlen_spec [definition, in Verif_strlib]
struct_list_valid_pointer_example [lemma, in Verif_reverse]
str1:1 [binder, in Verif_hash]
str1:35 [binder, in Verif_strlib]
str1:41 [binder, in Verif_strlib]
str1:5 [binder, in Verif_hash]
str2:3 [binder, in Verif_hash]
str2:37 [binder, in Verif_strlib]
str2:43 [binder, in Verif_strlib]
str2:7 [binder, in Verif_hash]
str:17 [binder, in Verif_strlib]
str:19 [binder, in Verif_hash]
str:20 [binder, in Verif_strlib]
str:21 [binder, in Verif_hash]
st:73 [binder, in Verif_triang]
st:76 [binder, in Verif_triang]
st:79 [binder, in Verif_triang]
st:82 [binder, in Verif_triang]
sumarray_spec [definition, in Verif_sumarray]
sum_Z_app [lemma, in Verif_sumarray]
sum_Z [definition, in Verif_sumarray]
s1a:32 [binder, in Verif_append2]
s1a:37 [binder, in Verif_append2]
s1a:53 [binder, in Verif_append1]
s1a:58 [binder, in Verif_append1]
s1c:34 [binder, in Verif_append2]
s1c:39 [binder, in Verif_append2]
s1c:55 [binder, in Verif_append1]
s1c:60 [binder, in Verif_append1]
s1:101 [binder, in Verif_append1]
s1:12 [binder, in Verif_append1]
s1:2 [binder, in Verif_hash]
s1:20 [binder, in Verif_append2]
s1:28 [binder, in Verif_append2]
s1:30 [binder, in Verif_reverse]
s1:33 [binder, in Verif_append1]
s1:34 [binder, in Verif_reverse]
s1:36 [binder, in Verif_strlib]
s1:38 [binder, in Verif_append1]
s1:42 [binder, in Verif_strlib]
s1:52 [binder, in Verif_reverse]
s1:6 [binder, in Verif_hash]
s1:62 [binder, in Verif_append2]
s1:67 [binder, in Verif_append2]
s1:69 [binder, in Verif_append1]
s1:74 [binder, in Verif_append1]
s1:8 [binder, in Verif_append1]
s1:94 [binder, in Verif_append1]
s2:102 [binder, in Verif_append1]
s2:13 [binder, in Verif_append1]
s2:21 [binder, in Verif_append2]
s2:29 [binder, in Verif_append2]
s2:31 [binder, in Verif_reverse]
s2:34 [binder, in Verif_append1]
s2:35 [binder, in Verif_reverse]
s2:38 [binder, in Verif_strlib]
s2:39 [binder, in Verif_append1]
s2:4 [binder, in Verif_hash]
s2:44 [binder, in Verif_strlib]
s2:63 [binder, in Verif_append2]
s2:68 [binder, in Verif_append2]
s2:70 [binder, in Verif_append1]
s2:75 [binder, in Verif_append1]
s2:8 [binder, in Verif_hash]
s2:9 [binder, in Verif_append1]
s2:95 [binder, in Verif_append1]
s:1 [binder, in Verif_strlib]
s:10 [binder, in Hashfun]
s:100 [binder, in Verif_hash]
s:104 [binder, in Verif_hash]
s:109 [binder, in Verif_hash]
s:114 [binder, in Verif_hash]
s:119 [binder, in Verif_hash]
s:13 [binder, in Verif_hash]
s:14 [binder, in Hashfun]
s:16 [binder, in Verif_strlib]
s:16 [binder, in Hashfun]
s:17 [binder, in Verif_hash]
s:18 [binder, in Verif_hash]
s:19 [binder, in Verif_strlib]
s:2 [binder, in Hashfun]
s:20 [binder, in Verif_hash]
s:20 [binder, in Hashfun]
s:22 [binder, in Verif_hash]
s:25 [binder, in Verif_hash]
s:26 [binder, in Verif_strlib]
s:29 [binder, in Verif_hash]
s:31 [binder, in Verif_hash]
s:32 [binder, in Verif_strlib]
s:5 [binder, in Hashfun]
s:53 [binder, in Verif_strlib]
s:57 [binder, in Verif_strlib]
s:6 [binder, in Hashfun]
s:60 [binder, in Hashfun]
s:63 [binder, in Verif_append1]
s:65 [binder, in Verif_append1]
s:67 [binder, in Verif_append1]
s:71 [binder, in Verif_append2]
s:74 [binder, in Verif_append2]
s:76 [binder, in Verif_append2]
s:78 [binder, in Verif_append2]
s:83 [binder, in Verif_hash]
s:88 [binder, in Verif_hash]
s:96 [binder, in Verif_hash]
T
table:175 [binder, in Verif_hash]tail:18 [binder, in Verif_append2]
tail:60 [binder, in Verif_append2]
tbl:64 [binder, in Hashfun]
tbl:66 [binder, in Hashfun]
tcell [definition, in Verif_hash]
thashtable [definition, in Verif_hash]
t_list_box [definition, in Verif_append2]
t_list [definition, in Verif_append1]
t_list [definition, in Verif_reverse]
t:1 [binder, in Verif_stack]
t:2 [binder, in Verif_stack]
t:35 [binder, in Verif_append2]
t:4 [binder, in Verif_stack]
t:40 [binder, in Verif_append2]
t:40 [binder, in Hashfun]
t:44 [binder, in Hashfun]
t:48 [binder, in Hashfun]
t:50 [binder, in Hashfun]
t:54 [binder, in Hashfun]
t:56 [binder, in Verif_append1]
t:57 [binder, in Hashfun]
t:6 [binder, in Verif_stack]
t:61 [binder, in Verif_append1]
t:69 [binder, in Hashfun]
t:72 [binder, in Hashfun]
U
uncurry [definition, in Verif_hash]Unnamed_thm6 [definition, in Verif_hash]
Unnamed_thm5 [definition, in Verif_hash]
Unnamed_thm4 [definition, in Verif_hash]
Unnamed_thm3 [definition, in Verif_hash]
Unnamed_thm2 [definition, in Verif_hash]
Unnamed_thm1 [definition, in Verif_hash]
Unnamed_thm0 [definition, in Verif_hash]
Unnamed_thm [definition, in Verif_hash]
Unnamed_thm [definition, in Verif_sumarray]
Unnamed_thm0 [definition, in Verif_strlib]
Unnamed_thm [definition, in Verif_strlib]
Unnamed_thm [definition, in Preface]
u:100 [binder, in Verif_append1]
u:36 [binder, in Verif_append2]
u:41 [binder, in Verif_append2]
u:57 [binder, in Verif_append1]
u:62 [binder, in Verif_append1]
V
Verif_append1 [library]Verif_triang [library]
Verif_sumarray [library]
Verif_stack [library]
Verif_hash [library]
Verif_append2 [library]
Verif_reverse [library]
Verif_strlib [library]
Vprog [definition, in Verif_hash]
Vprog [definition, in Verif_append1]
Vprog [definition, in Verif_sumarray]
Vprog [definition, in Verif_reverse]
Vprog [definition, in Verif_strlib]
Vprog [definition, in Verif_triang]
Vprog [definition, in Verif_stack]
v:33 [binder, in Verif_reverse]
v:37 [binder, in Verif_reverse]
v:56 [binder, in Verif_reverse]
W
wandQ_frame_ver_mpred [lemma, in Verif_append2]wandQ_frame_elim_mpred [lemma, in Verif_append2]
wand_frame_ver_from_adjoint_and_modus_ponens [lemma, in Verif_append2]
wand_derives_from_adjoint_and_modus_ponens [lemma, in Verif_append2]
wand_trivial [lemma, in Verif_append2]
wlseg [definition, in Verif_append2]
wlseg_weird [lemma, in Verif_append2]
wlseg_listrep_equiv [lemma, in Verif_append2]
wlseg_nullval [lemma, in Verif_append2]
wlseg_list [lemma, in Verif_append2]
wlseg_wlseg [lemma, in Verif_append2]
wlseg2lseg_nullval [lemma, in Verif_append2]
wsh:21 [binder, in Verif_strlib]
wsh:27 [binder, in Verif_strlib]
wsh:50 [binder, in Verif_strlib]
wsh:54 [binder, in Verif_strlib]
w:32 [binder, in Verif_reverse]
w:36 [binder, in Verif_reverse]
w:55 [binder, in Verif_reverse]
X
xy:72 [binder, in Verif_hash]x:10 [binder, in Verif_append1]
x:103 [binder, in Verif_append1]
x:16 [binder, in Verif_append2]
x:16 [binder, in Verif_append1]
x:164 [binder, in Verif_hash]
x:17 [binder, in Verif_sumarray]
x:19 [binder, in Verif_append2]
x:22 [binder, in Verif_append2]
x:22 [binder, in Verif_append1]
x:26 [binder, in Verif_append2]
x:26 [binder, in Verif_append1]
x:30 [binder, in Verif_append2]
x:31 [binder, in Verif_append1]
x:35 [binder, in Verif_append1]
x:40 [binder, in Verif_append1]
x:40 [binder, in Verif_reverse]
x:46 [binder, in Verif_append2]
x:46 [binder, in Verif_reverse]
x:47 [binder, in Verif_append1]
x:49 [binder, in Verif_append1]
x:51 [binder, in Verif_append2]
x:52 [binder, in Verif_hash]
x:52 [binder, in Verif_append2]
x:53 [binder, in Verif_append2]
x:55 [binder, in Verif_append2]
x:58 [binder, in Verif_append2]
x:6 [binder, in Verif_append1]
x:61 [binder, in Verif_append2]
x:64 [binder, in Verif_append2]
x:64 [binder, in Verif_append1]
x:66 [binder, in Verif_append1]
x:68 [binder, in Verif_append1]
x:69 [binder, in Verif_append2]
x:7 [binder, in Verif_sumarray]
x:71 [binder, in Verif_append1]
x:72 [binder, in Verif_append2]
x:75 [binder, in Verif_append2]
x:76 [binder, in Verif_append1]
x:77 [binder, in Verif_append2]
x:79 [binder, in Verif_append2]
x:80 [binder, in Verif_append1]
x:81 [binder, in Verif_append2]
x:87 [binder, in Verif_append1]
x:91 [binder, in Verif_append1]
x:97 [binder, in Verif_append1]
Y
y:10 [binder, in Verif_reverse]y:104 [binder, in Verif_append1]
y:11 [binder, in Verif_append1]
y:12 [binder, in Verif_stack]
y:165 [binder, in Verif_hash]
y:17 [binder, in Verif_append2]
y:19 [binder, in Verif_reverse]
y:20 [binder, in Verif_append1]
y:23 [binder, in Verif_append2]
y:23 [binder, in Verif_append1]
y:27 [binder, in Verif_append2]
y:27 [binder, in Verif_append1]
y:31 [binder, in Verif_append2]
y:32 [binder, in Verif_append1]
y:36 [binder, in Verif_append1]
y:41 [binder, in Verif_append1]
y:42 [binder, in Verif_reverse]
y:42 [binder, in Verif_triang]
y:47 [binder, in Verif_reverse]
y:5 [binder, in Verif_append1]
y:5 [binder, in Verif_reverse]
y:52 [binder, in Verif_append1]
y:55 [binder, in Verif_hash]
y:56 [binder, in Verif_append2]
y:59 [binder, in Verif_append2]
y:59 [binder, in Verif_reverse]
y:65 [binder, in Verif_append2]
y:7 [binder, in Verif_append1]
y:7 [binder, in Verif_reverse]
y:70 [binder, in Verif_append2]
y:73 [binder, in Verif_append2]
y:73 [binder, in Verif_append1]
y:77 [binder, in Verif_append1]
y:82 [binder, in Verif_append2]
y:84 [binder, in Verif_append1]
y:88 [binder, in Verif_append1]
y:92 [binder, in Verif_append1]
y:98 [binder, in Verif_append1]
Z
Zinduction [lemma, in Verif_triang]Zlength_hashtable_incr [lemma, in Hashfun]
Z_sub_add_ok [lemma, in Verif_triang]
z:166 [binder, in Verif_hash]
z:168 [binder, in Verif_hash]
z:17 [binder, in Verif_append1]
z:170 [binder, in Verif_hash]
z:172 [binder, in Verif_hash]
z:174 [binder, in Verif_hash]
z:24 [binder, in Verif_append2]
z:37 [binder, in Verif_append1]
z:43 [binder, in Verif_reverse]
z:48 [binder, in Verif_reverse]
z:66 [binder, in Verif_append2]
z:72 [binder, in Verif_append1]
z:78 [binder, in Verif_append1]
z:81 [binder, in Verif_append1]
z:93 [binder, in Verif_append1]
z:99 [binder, in Verif_append1]
Binder Index
A
al:103 [in Verif_hash]al:108 [in Verif_hash]
al:11 [in Hashfun]
al:126 [in Verif_hash]
al:129 [in Verif_hash]
al:130 [in Verif_hash]
al:138 [in Verif_hash]
al:143 [in Verif_hash]
al:19 [in Hashfun]
al:64 [in Verif_hash]
al:65 [in Verif_hash]
al:7 [in Hashfun]
al:87 [in Verif_triang]
a:1 [in Verif_sumarray]
a:1 [in Verif_triang]
A:123 [in Verif_hash]
a:21 [in Verif_append1]
a:24 [in Verif_append1]
a:25 [in Verif_append2]
a:25 [in Hashfun]
a:28 [in Verif_append1]
a:3 [in Verif_sumarray]
a:3 [in Verif_triang]
a:38 [in Verif_reverse]
A:42 [in Verif_append2]
a:44 [in Verif_reverse]
a:45 [in Verif_append2]
A:47 [in Verif_append2]
A:68 [in Verif_hash]
a:8 [in Verif_sumarray]
a:80 [in Verif_append2]
a:86 [in Verif_append1]
a:89 [in Verif_append1]
a:96 [in Verif_append1]
B
bl:122 [in Verif_hash]bl:75 [in Verif_hash]
bl:88 [in Verif_triang]
b0:141 [in Verif_hash]
b:147 [in Verif_hash]
b:149 [in Verif_hash]
b:2 [in Verif_sumarray]
b:2 [in Verif_triang]
b:25 [in Verif_append1]
b:29 [in Verif_append1]
b:33 [in Verif_append2]
b:38 [in Verif_append2]
b:39 [in Verif_reverse]
b:4 [in Verif_triang]
b:45 [in Verif_reverse]
b:54 [in Verif_append1]
b:59 [in Verif_append1]
B:69 [in Verif_hash]
b:90 [in Verif_append1]
C
contents:10 [in Verif_sumarray]contents:11 [in Verif_strlib]
contents:113 [in Verif_hash]
contents:118 [in Verif_hash]
contents:15 [in Verif_append2]
contents:15 [in Verif_append1]
contents:15 [in Hashfun]
contents:17 [in Hashfun]
contents:30 [in Verif_hash]
contents:32 [in Verif_hash]
contents:46 [in Verif_append1]
contents:48 [in Verif_append1]
contents:5 [in Verif_sumarray]
contents:54 [in Verif_append2]
contents:57 [in Verif_append2]
contents:6 [in Verif_strlib]
contents:73 [in Verif_hash]
contents:76 [in Verif_hash]
contents:78 [in Verif_hash]
contents:79 [in Verif_append1]
contents:85 [in Verif_append1]
contents:95 [in Verif_hash]
contents:99 [in Verif_hash]
count:132 [in Verif_hash]
count:137 [in Verif_hash]
count:154 [in Verif_hash]
count:160 [in Verif_hash]
count:34 [in Verif_hash]
count:39 [in Verif_hash]
count:43 [in Verif_hash]
count:48 [in Verif_hash]
count:61 [in Verif_hash]
count:85 [in Verif_hash]
count:90 [in Verif_hash]
cts:145 [in Verif_hash]
cts:146 [in Verif_hash]
cts:177 [in Verif_hash]
cts:178 [in Verif_hash]
cts:22 [in Hashfun]
cts:24 [in Hashfun]
cts:58 [in Hashfun]
cts:62 [in Hashfun]
c:30 [in Verif_append1]
C:70 [in Verif_hash]
D
dest:10 [in Verif_hash]dest:14 [in Verif_hash]
dest:23 [in Verif_strlib]
dest:29 [in Verif_strlib]
dest:51 [in Verif_strlib]
dest:55 [in Verif_strlib]
dl:156 [in Verif_hash]
dl:162 [in Verif_hash]
d:124 [in Verif_hash]
E
Espec:50 [in Verif_reverse]F
f:127 [in Verif_hash]f:16 [in Verif_sumarray]
f:71 [in Verif_hash]
G
gv:106 [in Verif_hash]gv:111 [in Verif_hash]
gv:116 [in Verif_hash]
gv:12 [in Verif_sumarray]
gv:121 [in Verif_hash]
gv:13 [in Verif_sumarray]
gv:24 [in Verif_hash]
gv:24 [in Verif_stack]
gv:25 [in Verif_stack]
gv:27 [in Verif_hash]
gv:30 [in Verif_stack]
gv:34 [in Verif_stack]
gv:38 [in Verif_stack]
gv:42 [in Verif_stack]
gv:54 [in Verif_triang]
gv:55 [in Verif_triang]
gv:60 [in Verif_triang]
gv:64 [in Verif_triang]
gv:68 [in Verif_triang]
gv:72 [in Verif_triang]
gv:74 [in Verif_strlib]
gv:75 [in Verif_strlib]
gv:75 [in Verif_triang]
gv:78 [in Verif_triang]
gv:80 [in Verif_hash]
gv:81 [in Verif_hash]
gv:81 [in Verif_triang]
gv:84 [in Verif_triang]
gv:85 [in Verif_triang]
gv:86 [in Verif_triang]
gv:87 [in Verif_hash]
gv:92 [in Verif_hash]
H
hi:91 [in Verif_triang]HRE:57 [in Verif_reverse]
hs:51 [in Verif_append1]
H0:13 [in Verif_strlib]
H0:8 [in Verif_strlib]
H1:14 [in Verif_strlib]
H1:9 [in Verif_strlib]
h:1 [in Hashfun]
H:12 [in Verif_strlib]
h:176 [in Verif_hash]
h:18 [in Verif_reverse]
h:18 [in Hashfun]
h:27 [in Hashfun]
h:50 [in Verif_append1]
h:53 [in Verif_reverse]
H:58 [in Verif_reverse]
h:6 [in Verif_reverse]
H:7 [in Verif_strlib]
h:9 [in Verif_reverse]
I
il:13 [in Verif_stack]il:15 [in Verif_stack]
il:17 [in Verif_stack]
il:20 [in Verif_stack]
il:22 [in Verif_stack]
il:29 [in Verif_stack]
il:33 [in Verif_stack]
il:37 [in Verif_stack]
il:38 [in Verif_triang]
il:41 [in Verif_stack]
il:43 [in Verif_triang]
il:45 [in Verif_triang]
il:47 [in Verif_triang]
il:50 [in Verif_triang]
il:52 [in Verif_triang]
il:59 [in Verif_triang]
il:63 [in Verif_triang]
il:67 [in Verif_triang]
il:71 [in Verif_triang]
il:8 [in Verif_stack]
il:80 [in Verif_triang]
il:83 [in Verif_triang]
il:89 [in Verif_triang]
il:93 [in Verif_triang]
il:94 [in Verif_triang]
i:10 [in Verif_strlib]
i:125 [in Verif_hash]
i:14 [in Verif_sumarray]
i:15 [in Verif_sumarray]
i:18 [in Verif_sumarray]
i:28 [in Verif_stack]
i:29 [in Hashfun]
i:31 [in Hashfun]
i:32 [in Verif_stack]
i:34 [in Verif_triang]
i:36 [in Verif_stack]
i:40 [in Verif_stack]
i:45 [in Verif_strlib]
i:46 [in Verif_strlib]
i:47 [in Verif_strlib]
i:5 [in Verif_strlib]
i:58 [in Verif_strlib]
i:58 [in Verif_triang]
i:59 [in Verif_strlib]
i:59 [in Hashfun]
i:62 [in Verif_triang]
i:63 [in Verif_strlib]
i:66 [in Verif_triang]
i:68 [in Verif_strlib]
i:70 [in Verif_triang]
i:72 [in Verif_strlib]
i:73 [in Verif_strlib]
i:9 [in Verif_hash]
i:95 [in Verif_triang]
i:96 [in Verif_triang]
i:97 [in Verif_triang]
J
j:42 [in Hashfun]j:55 [in Hashfun]
j:69 [in Verif_strlib]
j:70 [in Hashfun]
K
key:131 [in Verif_hash]key:136 [in Verif_hash]
key:153 [in Verif_hash]
key:159 [in Verif_hash]
key:33 [in Verif_hash]
key:38 [in Verif_hash]
key:42 [in Verif_hash]
key:46 [in Verif_hash]
key:60 [in Verif_hash]
key:84 [in Verif_hash]
key:89 [in Verif_hash]
kp:135 [in Verif_hash]
kp:152 [in Verif_hash]
kp:158 [in Verif_hash]
kp:37 [in Verif_hash]
kp:47 [in Verif_hash]
k':51 [in Hashfun]
k:37 [in Hashfun]
k:39 [in Hashfun]
k:43 [in Hashfun]
k:46 [in Hashfun]
k:47 [in Hashfun]
k:49 [in Hashfun]
k:52 [in Hashfun]
k:53 [in Hashfun]
k:56 [in Hashfun]
k:61 [in Hashfun]
k:63 [in Hashfun]
k:65 [in Hashfun]
k:67 [in Hashfun]
k:68 [in Hashfun]
k:71 [in Hashfun]
K:92 [in Verif_triang]
L
lo:28 [in Hashfun]lo:90 [in Verif_triang]
l:41 [in Verif_reverse]
l:49 [in Verif_reverse]
N
next:35 [in Verif_hash]next:40 [in Verif_hash]
next:44 [in Verif_hash]
next:86 [in Verif_hash]
next:91 [in Verif_hash]
n:11 [in Verif_hash]
n:11 [in Verif_triang]
n:14 [in Verif_triang]
n:15 [in Verif_hash]
n:15 [in Verif_triang]
n:17 [in Verif_triang]
n:18 [in Verif_triang]
n:20 [in Verif_triang]
n:21 [in Verif_triang]
n:22 [in Verif_triang]
n:24 [in Verif_strlib]
n:30 [in Verif_strlib]
n:35 [in Verif_triang]
n:36 [in Verif_triang]
n:37 [in Verif_triang]
n:48 [in Verif_strlib]
n:49 [in Verif_strlib]
n:5 [in Verif_triang]
n:52 [in Verif_strlib]
n:56 [in Verif_strlib]
n:60 [in Verif_strlib]
n:64 [in Verif_strlib]
n:74 [in Verif_triang]
n:77 [in Verif_triang]
n:8 [in Verif_triang]
P
p':133 [in Verif_hash]p':49 [in Verif_hash]
p':62 [in Verif_hash]
P':9 [in Verif_append2]
p0:142 [in Verif_hash]
P:1 [in Verif_append2]
p:11 [in Verif_reverse]
p:112 [in Verif_hash]
p:117 [in Verif_hash]
P:12 [in Verif_append2]
p:128 [in Verif_hash]
p:13 [in Verif_reverse]
p:134 [in Verif_hash]
p:14 [in Verif_stack]
p:140 [in Verif_hash]
p:144 [in Verif_hash]
p:148 [in Verif_hash]
p:15 [in Verif_reverse]
p:150 [in Verif_hash]
p:151 [in Verif_hash]
p:157 [in Verif_hash]
p:16 [in Verif_stack]
p:163 [in Verif_hash]
p:167 [in Verif_hash]
p:169 [in Verif_hash]
p:17 [in Verif_reverse]
p:171 [in Verif_hash]
p:173 [in Verif_hash]
p:18 [in Verif_stack]
p:2 [in Verif_append1]
p:2 [in Verif_reverse]
p:20 [in Verif_reverse]
p:21 [in Verif_stack]
p:22 [in Verif_reverse]
p:23 [in Verif_stack]
p:24 [in Verif_reverse]
p:26 [in Verif_reverse]
p:26 [in Verif_stack]
p:27 [in Verif_stack]
p:28 [in Verif_hash]
p:28 [in Verif_reverse]
p:3 [in Verif_stack]
p:31 [in Verif_stack]
P:33 [in Verif_triang]
p:35 [in Verif_stack]
p:36 [in Verif_hash]
p:39 [in Verif_triang]
p:39 [in Verif_stack]
P:4 [in Verif_append2]
p:41 [in Verif_hash]
P:43 [in Verif_append2]
p:43 [in Verif_append1]
p:44 [in Verif_triang]
p:45 [in Verif_hash]
p:45 [in Verif_append1]
p:46 [in Verif_triang]
P:48 [in Verif_append2]
p:48 [in Verif_triang]
p:5 [in Verif_stack]
p:50 [in Verif_hash]
p:51 [in Verif_triang]
p:53 [in Verif_triang]
p:56 [in Verif_triang]
p:57 [in Verif_hash]
p:57 [in Verif_triang]
p:59 [in Verif_hash]
P:6 [in Verif_append2]
p:61 [in Verif_triang]
p:62 [in Verif_strlib]
p:63 [in Verif_hash]
p:65 [in Verif_triang]
p:66 [in Verif_strlib]
p:67 [in Verif_hash]
p:69 [in Verif_triang]
p:7 [in Verif_stack]
p:70 [in Verif_strlib]
p:74 [in Verif_hash]
p:77 [in Verif_hash]
p:79 [in Verif_hash]
P:8 [in Verif_append2]
p:8 [in Verif_reverse]
p:82 [in Verif_hash]
p:9 [in Verif_stack]
p:93 [in Verif_hash]
p:94 [in Verif_hash]
p:98 [in Verif_hash]
Q
Q':11 [in Verif_append2]Q:10 [in Verif_append2]
Q:13 [in Verif_append2]
q:139 [in Verif_hash]
q:19 [in Verif_stack]
Q:2 [in Verif_append2]
q:29 [in Verif_reverse]
Q:44 [in Verif_append2]
Q:49 [in Verif_append2]
q:49 [in Verif_triang]
Q:5 [in Verif_append2]
Q:7 [in Verif_append2]
q:71 [in Verif_strlib]
R
rsh:22 [in Verif_strlib]rsh:28 [in Verif_strlib]
r0:102 [in Verif_hash]
r0:107 [in Verif_hash]
R:14 [in Verif_append2]
r:14 [in Verif_append1]
r:155 [in Verif_hash]
r:161 [in Verif_hash]
R:3 [in Verif_append2]
R:50 [in Verif_append2]
r:54 [in Verif_reverse]
r:66 [in Verif_hash]
S
sh1:33 [in Verif_strlib]sh1:39 [in Verif_strlib]
sh2:34 [in Verif_strlib]
sh2:40 [in Verif_strlib]
sh:15 [in Verif_strlib]
sh:18 [in Verif_strlib]
sh:4 [in Verif_sumarray]
sh:61 [in Verif_strlib]
sh:65 [in Verif_strlib]
sh:67 [in Verif_strlib]
sh:9 [in Verif_sumarray]
sigma:1 [in Verif_append1]
sigma:1 [in Verif_reverse]
sigma:101 [in Verif_hash]
sigma:105 [in Verif_hash]
sigma:110 [in Verif_hash]
sigma:115 [in Verif_hash]
sigma:12 [in Verif_reverse]
sigma:120 [in Verif_hash]
sigma:14 [in Verif_reverse]
sigma:16 [in Verif_reverse]
sigma:21 [in Verif_reverse]
sigma:21 [in Hashfun]
sigma:23 [in Verif_hash]
sigma:23 [in Verif_reverse]
sigma:23 [in Hashfun]
sigma:25 [in Verif_reverse]
sigma:26 [in Verif_hash]
sigma:26 [in Hashfun]
sigma:27 [in Verif_reverse]
sigma:30 [in Hashfun]
sigma:42 [in Verif_append1]
sigma:44 [in Verif_append1]
sigma:51 [in Verif_hash]
sigma:51 [in Verif_reverse]
sigma:56 [in Verif_hash]
sigma:58 [in Verif_hash]
sigma:97 [in Verif_hash]
size:11 [in Verif_sumarray]
size:6 [in Verif_sumarray]
src:12 [in Verif_hash]
src:16 [in Verif_hash]
src:25 [in Verif_strlib]
src:31 [in Verif_strlib]
str1:1 [in Verif_hash]
str1:35 [in Verif_strlib]
str1:41 [in Verif_strlib]
str1:5 [in Verif_hash]
str2:3 [in Verif_hash]
str2:37 [in Verif_strlib]
str2:43 [in Verif_strlib]
str2:7 [in Verif_hash]
str:17 [in Verif_strlib]
str:19 [in Verif_hash]
str:20 [in Verif_strlib]
str:21 [in Verif_hash]
st:73 [in Verif_triang]
st:76 [in Verif_triang]
st:79 [in Verif_triang]
st:82 [in Verif_triang]
s1a:32 [in Verif_append2]
s1a:37 [in Verif_append2]
s1a:53 [in Verif_append1]
s1a:58 [in Verif_append1]
s1c:34 [in Verif_append2]
s1c:39 [in Verif_append2]
s1c:55 [in Verif_append1]
s1c:60 [in Verif_append1]
s1:101 [in Verif_append1]
s1:12 [in Verif_append1]
s1:2 [in Verif_hash]
s1:20 [in Verif_append2]
s1:28 [in Verif_append2]
s1:30 [in Verif_reverse]
s1:33 [in Verif_append1]
s1:34 [in Verif_reverse]
s1:36 [in Verif_strlib]
s1:38 [in Verif_append1]
s1:42 [in Verif_strlib]
s1:52 [in Verif_reverse]
s1:6 [in Verif_hash]
s1:62 [in Verif_append2]
s1:67 [in Verif_append2]
s1:69 [in Verif_append1]
s1:74 [in Verif_append1]
s1:8 [in Verif_append1]
s1:94 [in Verif_append1]
s2:102 [in Verif_append1]
s2:13 [in Verif_append1]
s2:21 [in Verif_append2]
s2:29 [in Verif_append2]
s2:31 [in Verif_reverse]
s2:34 [in Verif_append1]
s2:35 [in Verif_reverse]
s2:38 [in Verif_strlib]
s2:39 [in Verif_append1]
s2:4 [in Verif_hash]
s2:44 [in Verif_strlib]
s2:63 [in Verif_append2]
s2:68 [in Verif_append2]
s2:70 [in Verif_append1]
s2:75 [in Verif_append1]
s2:8 [in Verif_hash]
s2:9 [in Verif_append1]
s2:95 [in Verif_append1]
s:1 [in Verif_strlib]
s:10 [in Hashfun]
s:100 [in Verif_hash]
s:104 [in Verif_hash]
s:109 [in Verif_hash]
s:114 [in Verif_hash]
s:119 [in Verif_hash]
s:13 [in Verif_hash]
s:14 [in Hashfun]
s:16 [in Verif_strlib]
s:16 [in Hashfun]
s:17 [in Verif_hash]
s:18 [in Verif_hash]
s:19 [in Verif_strlib]
s:2 [in Hashfun]
s:20 [in Verif_hash]
s:20 [in Hashfun]
s:22 [in Verif_hash]
s:25 [in Verif_hash]
s:26 [in Verif_strlib]
s:29 [in Verif_hash]
s:31 [in Verif_hash]
s:32 [in Verif_strlib]
s:5 [in Hashfun]
s:53 [in Verif_strlib]
s:57 [in Verif_strlib]
s:6 [in Hashfun]
s:60 [in Hashfun]
s:63 [in Verif_append1]
s:65 [in Verif_append1]
s:67 [in Verif_append1]
s:71 [in Verif_append2]
s:74 [in Verif_append2]
s:76 [in Verif_append2]
s:78 [in Verif_append2]
s:83 [in Verif_hash]
s:88 [in Verif_hash]
s:96 [in Verif_hash]
T
table:175 [in Verif_hash]tail:18 [in Verif_append2]
tail:60 [in Verif_append2]
tbl:64 [in Hashfun]
tbl:66 [in Hashfun]
t:1 [in Verif_stack]
t:2 [in Verif_stack]
t:35 [in Verif_append2]
t:4 [in Verif_stack]
t:40 [in Verif_append2]
t:40 [in Hashfun]
t:44 [in Hashfun]
t:48 [in Hashfun]
t:50 [in Hashfun]
t:54 [in Hashfun]
t:56 [in Verif_append1]
t:57 [in Hashfun]
t:6 [in Verif_stack]
t:61 [in Verif_append1]
t:69 [in Hashfun]
t:72 [in Hashfun]
U
u:100 [in Verif_append1]u:36 [in Verif_append2]
u:41 [in Verif_append2]
u:57 [in Verif_append1]
u:62 [in Verif_append1]
V
v:33 [in Verif_reverse]v:37 [in Verif_reverse]
v:56 [in Verif_reverse]
W
wsh:21 [in Verif_strlib]wsh:27 [in Verif_strlib]
wsh:50 [in Verif_strlib]
wsh:54 [in Verif_strlib]
w:32 [in Verif_reverse]
w:36 [in Verif_reverse]
w:55 [in Verif_reverse]
X
xy:72 [in Verif_hash]x:10 [in Verif_append1]
x:103 [in Verif_append1]
x:16 [in Verif_append2]
x:16 [in Verif_append1]
x:164 [in Verif_hash]
x:17 [in Verif_sumarray]
x:19 [in Verif_append2]
x:22 [in Verif_append2]
x:22 [in Verif_append1]
x:26 [in Verif_append2]
x:26 [in Verif_append1]
x:30 [in Verif_append2]
x:31 [in Verif_append1]
x:35 [in Verif_append1]
x:40 [in Verif_append1]
x:40 [in Verif_reverse]
x:46 [in Verif_append2]
x:46 [in Verif_reverse]
x:47 [in Verif_append1]
x:49 [in Verif_append1]
x:51 [in Verif_append2]
x:52 [in Verif_hash]
x:52 [in Verif_append2]
x:53 [in Verif_append2]
x:55 [in Verif_append2]
x:58 [in Verif_append2]
x:6 [in Verif_append1]
x:61 [in Verif_append2]
x:64 [in Verif_append2]
x:64 [in Verif_append1]
x:66 [in Verif_append1]
x:68 [in Verif_append1]
x:69 [in Verif_append2]
x:7 [in Verif_sumarray]
x:71 [in Verif_append1]
x:72 [in Verif_append2]
x:75 [in Verif_append2]
x:76 [in Verif_append1]
x:77 [in Verif_append2]
x:79 [in Verif_append2]
x:80 [in Verif_append1]
x:81 [in Verif_append2]
x:87 [in Verif_append1]
x:91 [in Verif_append1]
x:97 [in Verif_append1]
Y
y:10 [in Verif_reverse]y:104 [in Verif_append1]
y:11 [in Verif_append1]
y:12 [in Verif_stack]
y:165 [in Verif_hash]
y:17 [in Verif_append2]
y:19 [in Verif_reverse]
y:20 [in Verif_append1]
y:23 [in Verif_append2]
y:23 [in Verif_append1]
y:27 [in Verif_append2]
y:27 [in Verif_append1]
y:31 [in Verif_append2]
y:32 [in Verif_append1]
y:36 [in Verif_append1]
y:41 [in Verif_append1]
y:42 [in Verif_reverse]
y:42 [in Verif_triang]
y:47 [in Verif_reverse]
y:5 [in Verif_append1]
y:5 [in Verif_reverse]
y:52 [in Verif_append1]
y:55 [in Verif_hash]
y:56 [in Verif_append2]
y:59 [in Verif_append2]
y:59 [in Verif_reverse]
y:65 [in Verif_append2]
y:7 [in Verif_append1]
y:7 [in Verif_reverse]
y:70 [in Verif_append2]
y:73 [in Verif_append2]
y:73 [in Verif_append1]
y:77 [in Verif_append1]
y:82 [in Verif_append2]
y:84 [in Verif_append1]
y:88 [in Verif_append1]
y:92 [in Verif_append1]
y:98 [in Verif_append1]
Z
z:166 [in Verif_hash]z:168 [in Verif_hash]
z:17 [in Verif_append1]
z:170 [in Verif_hash]
z:172 [in Verif_hash]
z:174 [in Verif_hash]
z:24 [in Verif_append2]
z:37 [in Verif_append1]
z:43 [in Verif_reverse]
z:48 [in Verif_reverse]
z:66 [in Verif_append2]
z:72 [in Verif_append1]
z:78 [in Verif_append1]
z:81 [in Verif_append1]
z:93 [in Verif_append1]
z:99 [in Verif_append1]
Module Index
C
COUNT_TABLE [in Hashfun]F
FunTable [in Hashfun]I
IntHashTable [in Hashfun]Variable Index
S
StringDemo.p [in Verif_strlib]Library Index
B
BibH
HashfunP
PostscriptPreface
V
Verif_append1Verif_triang
Verif_sumarray
Verif_stack
Verif_hash
Verif_append2
Verif_reverse
Verif_strlib
Lemma Index
A
add_another [in Verif_triang]add_list_sublist_bounds [in Verif_triang]
add_list_nonneg [in Verif_triang]
add_list_app [in Verif_triang]
add_list_decreasing_eq [in Verif_triang]
add_list_decreasing_eq_alt [in Verif_triang]
B
body_incr [in Verif_hash]body_incr_field_address_lemma [in Verif_hash]
body_incr_list [in Verif_hash]
body_get [in Verif_hash]
body_new_table [in Verif_hash]
body_new_table_helper [in Verif_hash]
body_new_cell [in Verif_hash]
body_copy_string [in Verif_hash]
body_hash [in Verif_hash]
body_append_alter2 [in Verif_append2]
body_append_alter1 [in Verif_append1]
body_append [in Verif_append1]
body_main [in Verif_sumarray]
body_sumarray [in Verif_sumarray]
body_reverse_step [in Verif_reverse]
body_reverse [in Verif_reverse]
body_strcmp [in Verif_strlib]
body_example_call_strcpy [in Verif_strlib]
body_strcpy [in Verif_strlib]
body_strlen [in Verif_strlib]
body_main [in Verif_triang]
body_pop_and_add [in Verif_triang]
body_pop_and_add [in Verif_triang]
body_push_increasing [in Verif_triang]
body_newstack [in Verif_stack]
body_push [in Verif_stack]
body_pop [in Verif_stack]
C
cancel_example [in Verif_strlib]D
data_at_isptr_example2 [in Verif_reverse]data_at_isptr_example1 [in Verif_reverse]
data_at_Vundef_example [in Verif_strlib]
data_at_Vundef_example [in Verif_strlib]
demonstrate_cstring2 [in Verif_strlib]
demonstrate_cstring1 [in Verif_strlib]
E
emp_lbseg [in Verif_append2]emp_wlseg [in Verif_append2]
emp_wand_emp_left [in Verif_append2]
emp_wand_emp_right [in Verif_append2]
example_field_at_data_at''' [in Verif_hash]
example_field_at_data_at'' [in Verif_hash]
example_field_at_data_at' [in Verif_hash]
example_field_at_data_at [in Verif_hash]
example_split_struct [in Verif_hash]
F
FunTable.gempty [in Hashfun]FunTable.gso [in Hashfun]
FunTable.gss [in Hashfun]
H
hashfun_snoc [in Hashfun]hashfun_aux_snoc [in Hashfun]
hashfun_inrange [in Hashfun]
hashtable_rep_valid_pointer [in Verif_hash]
hashtable_rep_local_facts [in Verif_hash]
hashtable_get_unfold [in Hashfun]
I
implies_and_adjoint [in Verif_append2]IntHashTable.empty_invariant [in Hashfun]
IntHashTable.gempty [in Hashfun]
IntHashTable.gso [in Hashfun]
IntHashTable.gss [in Hashfun]
IntHashTable.incr_invariant [in Hashfun]
Int_repr_eq_mod [in Hashfun]
iter_sepcon_split3 [in Verif_hash]
iter_sepcon_listrep_local_facts [in Verif_hash]
L
lbseg_lbseg [in Verif_append2]listboxrep_traverse32 [in Verif_hash]
listboxrep_traverse [in Verif_hash]
listbox_lbseg [in Verif_append2]
listcell_fold [in Verif_hash]
listrep_traverse_finish [in Verif_hash]
listrep_traverse_step_example [in Verif_hash]
listrep_traverse_step [in Verif_hash]
listrep_traverse_start [in Verif_hash]
listrep_fold [in Verif_hash]
listrep_valid_pointer [in Verif_hash]
listrep_local_prop [in Verif_hash]
listrep_nonnull [in Verif_append1]
listrep_null [in Verif_append1]
listrep_valid_pointer [in Verif_append1]
listrep_local_facts [in Verif_append1]
listrep_len_ge2_address_different [in Verif_reverse]
listrep_len_ge2_fact [in Verif_reverse]
listrep_valid_pointer [in Verif_reverse]
listrep_valid_pointer_example [in Verif_reverse]
listrep_local_facts [in Verif_reverse]
listrep_facts_example [in Verif_reverse]
listrep_facts_example [in Verif_reverse]
listrep_valid_pointer [in Verif_triang]
listrep_local_prop [in Verif_triang]
listrep_valid_pointer [in Verif_stack]
listrep_local_prop [in Verif_stack]
listrep2lseg [in Verif_append1]
loopy_lseg_no_connection [in Verif_append1]
loopy_lseg_not_bad [in Verif_append1]
lseg_lseg_inv [in Verif_append1]
lseg_listrep_equiv [in Verif_append1]
lseg_list [in Verif_append1]
lseg_lseg [in Verif_append1]
lseg_maybe_loop [in Verif_append1]
lseg2listrep [in Verif_append1]
lseg2wlseg [in Verif_append2]
M
modus_ponens_wand_from_adjoint [in Verif_append2]N
nat_sub_add_yuck [in Verif_triang]nt_lseg_list [in Verif_append1]
nt_lseg_nt_lseg [in Verif_append1]
N_eq [in Hashfun]
P
prog_correct [in Verif_sumarray]S
singleton_wlseg [in Verif_append2]singleton_nt_lseg' [in Verif_append1]
singleton_nt_lseg [in Verif_append1]
singleton_lseg [in Verif_append1]
stack_valid_pointer [in Verif_triang]
stack_local_prop [in Verif_triang]
stack_valid_pointer [in Verif_stack]
stack_local_prop [in Verif_stack]
strcpy_else_clause [in Verif_strlib]
strcpy_then_clause [in Verif_strlib]
struct_list_valid_pointer_example [in Verif_reverse]
sum_Z_app [in Verif_sumarray]
W
wandQ_frame_ver_mpred [in Verif_append2]wandQ_frame_elim_mpred [in Verif_append2]
wand_frame_ver_from_adjoint_and_modus_ponens [in Verif_append2]
wand_derives_from_adjoint_and_modus_ponens [in Verif_append2]
wand_trivial [in Verif_append2]
wlseg_weird [in Verif_append2]
wlseg_listrep_equiv [in Verif_append2]
wlseg_nullval [in Verif_append2]
wlseg_list [in Verif_append2]
wlseg_wlseg [in Verif_append2]
wlseg2lseg_nullval [in Verif_append2]
Z
Zinduction [in Verif_triang]Zlength_hashtable_incr [in Hashfun]
Z_sub_add_ok [in Verif_triang]
Axiom Index
C
COUNT_TABLE.gso [in Hashfun]COUNT_TABLE.gss [in Hashfun]
COUNT_TABLE.gempty [in Hashfun]
COUNT_TABLE.incr [in Hashfun]
COUNT_TABLE.get [in Hashfun]
COUNT_TABLE.empty [in Hashfun]
COUNT_TABLE.key [in Hashfun]
COUNT_TABLE.table [in Hashfun]
Instance Index
C
CompSpecs [in Verif_hash]CompSpecs [in Verif_append1]
CompSpecs [in Verif_sumarray]
CompSpecs [in Verif_reverse]
CompSpecs [in Verif_strlib]
CompSpecs [in Verif_triang]
CompSpecs [in Verif_stack]
E
EqDec_string [in Hashfun]Section Index
S
StringDemo [in Verif_strlib]Definition Index
A
add_list [in Verif_triang]append_spec [in Verif_append1]
C
copy_string_spec [in Verif_hash]D
decreasing_Z1 [in Verif_triang]decreasing_Z1_aux [in Verif_triang]
decreasing_Z [in Verif_triang]
decreasing_nat [in Verif_triang]
E
empty_table [in Hashfun]example_call_strcpy_spec [in Verif_strlib]
F
four_contents [in Verif_sumarray]free_spec_example [in Verif_stack]
FunTable.empty [in Hashfun]
FunTable.get [in Hashfun]
FunTable.incr [in Hashfun]
FunTable.key [in Hashfun]
FunTable.table [in Hashfun]
G
get_spec [in Verif_hash]Gprog [in Verif_hash]
Gprog [in Verif_append1]
Gprog [in Verif_sumarray]
Gprog [in Verif_reverse]
Gprog [in Verif_strlib]
Gprog [in Verif_triang]
Gprog [in Verif_stack]
H
hashfun [in Hashfun]hashfun_aux [in Hashfun]
hashtable_rep [in Verif_hash]
hashtable_incr [in Hashfun]
hashtable_get [in Hashfun]
hashtable_contents [in Hashfun]
hash_spec [in Verif_hash]
Hello [in Verif_strlib]
Hello' [in Verif_strlib]
I
incr_spec [in Verif_hash]incr_list_spec [in Verif_hash]
IntHashTable.empty [in Hashfun]
IntHashTable.get [in Hashfun]
IntHashTable.hashtable_invariant [in Hashfun]
IntHashTable.incr [in Hashfun]
IntHashTable.key [in Hashfun]
IntHashTable.table [in Hashfun]
L
lbseg [in Verif_append2]listboxrep [in Verif_hash]
listboxrep [in Verif_append2]
listrep [in Verif_hash]
listrep [in Verif_append1]
listrep [in Verif_reverse]
listrep [in Verif_triang]
listrep [in Verif_stack]
list_cell_valid_pointer [in Verif_hash]
list_cell_local_facts [in Verif_hash]
list_cell [in Verif_hash]
list_incr [in Hashfun]
list_get [in Hashfun]
lseg [in Verif_append1]
M
main_spec [in Verif_sumarray]main_spec [in Verif_triang]
malloc_spec_example [in Verif_stack]
N
N [in Hashfun]newstack_spec [in Verif_triang]
newstack_spec [in Verif_stack]
new_cell_spec [in Verif_hash]
new_table_spec [in Verif_hash]
nt_lseg [in Verif_append1]
P
pop_and_add_spec [in Verif_triang]pop_spec [in Verif_triang]
pop_spec [in Verif_stack]
push_increasing_spec [in Verif_triang]
push_spec [in Verif_triang]
push_spec [in Verif_stack]
R
reverse_spec [in Verif_reverse]S
stack [in Verif_triang]stack [in Verif_stack]
strcmp_spec [in Verif_hash]
strcmp_spec [in Verif_strlib]
strcpy_spec [in Verif_hash]
strcpy_spec [in Verif_strlib]
stringlit_1_contents [in Verif_strlib]
string_to_list_byte [in Verif_strlib]
strlen_spec [in Verif_hash]
strlen_spec [in Verif_strlib]
sumarray_spec [in Verif_sumarray]
sum_Z [in Verif_sumarray]
T
tcell [in Verif_hash]thashtable [in Verif_hash]
t_list_box [in Verif_append2]
t_list [in Verif_append1]
t_list [in Verif_reverse]
U
uncurry [in Verif_hash]Unnamed_thm6 [in Verif_hash]
Unnamed_thm5 [in Verif_hash]
Unnamed_thm4 [in Verif_hash]
Unnamed_thm3 [in Verif_hash]
Unnamed_thm2 [in Verif_hash]
Unnamed_thm1 [in Verif_hash]
Unnamed_thm0 [in Verif_hash]
Unnamed_thm [in Verif_hash]
Unnamed_thm [in Verif_sumarray]
Unnamed_thm0 [in Verif_strlib]
Unnamed_thm [in Verif_strlib]
Unnamed_thm [in Preface]
V
Vprog [in Verif_hash]Vprog [in Verif_append1]
Vprog [in Verif_sumarray]
Vprog [in Verif_reverse]
Vprog [in Verif_strlib]
Vprog [in Verif_triang]
Vprog [in Verif_stack]
W
wlseg [in Verif_append2]| Global Index | 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 | _ | other | (956 entries) |
| Binder Index | 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 | _ | other | (678 entries) |
| Module Index | 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 | _ | other | (3 entries) |
| Variable Index | 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 | _ | other | (1 entry) |
| Library Index | 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 | _ | other | (12 entries) |
| Lemma Index | 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 | _ | other | (136 entries) |
| Axiom Index | 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 | _ | other | (8 entries) |
| Instance Index | 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 | _ | other | (8 entries) |
| Section Index | 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 | _ | other | (1 entry) |
| Definition Index | 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 | _ | other | (109 entries) |
This page has been generated by coqdoc