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

(2639 entries)

Notation 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

(46 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

(1928 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

(8 entries)

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

(19 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

(200 entries)

Constructor 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

(126 entries)

Projection 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

(30 entries)

Inductive 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

(15 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

(17 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

(68 entries)

Abbreviation 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

(18 entries)

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

(154 entries)

Record 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

(10 entries)

Global Index

A

add_impl:69 [binder, in intensional.examples.iterator]
add_spec [definition, in intensional.examples.iterator]
add:12 [binder, in intensional.examples.iterator]
adequacy [library]
Alloc [abbreviation, in intensional.heap_lang.notation]
alloc_atomic [instance, in intensional.heap_lang.lifting]
alloc_hist [lemma, in intensional.heap_lang.lifting]
AlreadyKnown [constructor, in intensional.examples.tactics]
array [definition, in intensional.heap_lang.array]
array [library]
array_cons_frame [instance, in intensional.heap_lang.array]
array_cons [lemma, in intensional.heap_lang.array]
array_app [lemma, in intensional.heap_lang.array]
array_singleton [lemma, in intensional.heap_lang.array]
array_nil [lemma, in intensional.heap_lang.array]
array_as_fractional [instance, in intensional.heap_lang.array]
array_fractional [instance, in intensional.heap_lang.array]
array_timeless [instance, in intensional.heap_lang.array]
AsRecV [record, in intensional.heap_lang.lifting]
AsRecV [inductive, in intensional.heap_lang.lifting]
AsRecV_recv [definition, in intensional.heap_lang.lifting]
AsRecV0:183 [binder, in intensional.heap_lang.lifting]
as_recv [projection, in intensional.heap_lang.lifting]
as_recv [constructor, in intensional.heap_lang.lifting]
as_val_val [instance, in intensional.heap_lang.lifting]
A:1 [binder, in intensional.heap_lang.lifting]
A:1 [binder, in intensional.examples.tactics]
A:1 [binder, in intensional.examples.iris_extra]
A:1 [binder, in intensional.examples.stdpp_extra]
A:10 [binder, in intensional.heap_lang.lifting]
A:12 [binder, in intensional.examples.stdpp_extra]
A:13 [binder, in intensional.examples.tactics]
A:14 [binder, in intensional.examples.iris_extra]
a:17 [binder, in intensional.examples.tactics]
A:18 [binder, in intensional.examples.tactics]
a:2 [binder, in intensional.examples.tactics]
a:24 [binder, in intensional.examples.tactics]
A:27 [binder, in intensional.examples.tactics]
a:35 [binder, in intensional.examples.tactics]
A:5 [binder, in intensional.examples.tactics]
A:6 [binder, in intensional.heap_lang.lifting]
A:6 [binder, in intensional.examples.stdpp_extra]
A:7 [binder, in intensional.examples.iris_extra]
A:73 [binder, in intensional.heap_lang.lifting]
a:8 [binder, in intensional.examples.tactics]
A:87 [binder, in intensional.heap_lang.lifting]
a:9 [binder, in intensional.heap_lang.lifting]
A:9 [binder, in intensional.examples.tactics]

B

beta_atomic [instance, in intensional.heap_lang.lifting]
bfilelibN [definition, in intensional.examples.well_bracketed]
bfilelib_spec [definition, in intensional.examples.well_bracketed]
bfile_trace [definition, in intensional.examples.well_bracketed]
binop_atomic [instance, in intensional.heap_lang.lifting]
b1:212 [binder, in intensional.heap_lang.lang]
b2:213 [binder, in intensional.heap_lang.lang]
B:10 [binder, in intensional.examples.tactics]
B:14 [binder, in intensional.examples.tactics]
B:19 [binder, in intensional.examples.tactics]
b:25 [binder, in intensional.examples.tactics]
B:28 [binder, in intensional.examples.tactics]
b:324 [binder, in intensional.heap_lang.lang]
b:36 [binder, in intensional.examples.tactics]
b:4 [binder, in intensional.heap_lang.lang]
B:6 [binder, in intensional.examples.tactics]

C

CAS [abbreviation, in intensional.heap_lang.notation]
check_tag_iff [lemma, in intensional.examples.trace_helpers]
check_tag_in_tags [lemma, in intensional.examples.trace_helpers]
check_tag [definition, in intensional.examples.trace_helpers]
close_impl:58 [binder, in intensional.examples.file]
close_spec [definition, in intensional.examples.file]
close:10 [binder, in intensional.examples.file]
cmpxchg_atomic [instance, in intensional.heap_lang.lifting]
Coll_impl:66 [binder, in intensional.examples.iterator]
Coll:10 [binder, in intensional.examples.iterator]
Coll:18 [binder, in intensional.examples.iterator]
Coll:26 [binder, in intensional.examples.iterator]
Coll:3 [binder, in intensional.examples.iterator]
Coll:33 [binder, in intensional.examples.iterator]
Coll:42 [binder, in intensional.examples.iterator]
create_impl:68 [binder, in intensional.examples.traversable_stack]
create_spec [definition, in intensional.examples.traversable_stack]
create_impl:44 [binder, in intensional.examples.stack]
create_spec [definition, in intensional.examples.stack]
create:5 [binder, in intensional.examples.traversable_stack]
create:5 [binder, in intensional.examples.stack]
ctx:184 [binder, in intensional.heap_lang.lang]
c':15 [binder, in intensional.examples.iterator]
c':23 [binder, in intensional.examples.iterator]
c:13 [binder, in intensional.examples.iterator]
C:20 [binder, in intensional.examples.tactics]
c:21 [binder, in intensional.examples.iterator]
C:29 [binder, in intensional.examples.tactics]
c:29 [binder, in intensional.examples.iterator]
c:36 [binder, in intensional.examples.iterator]
c:37 [binder, in intensional.examples.tactics]
c:44 [binder, in intensional.examples.iterator]
c:6 [binder, in intensional.examples.iterator]

D

D:30 [binder, in intensional.examples.tactics]

E

efs':391 [binder, in intensional.heap_lang.lang]
efs:335 [binder, in intensional.heap_lang.lifting]
efs:352 [binder, in intensional.heap_lang.lang]
efs:359 [binder, in intensional.heap_lang.lang]
efs:380 [binder, in intensional.heap_lang.lang]
efs:386 [binder, in intensional.heap_lang.lang]
elts:139 [binder, in intensional.examples.linearizability]
emit_atomic [instance, in intensional.heap_lang.lifting]
empty_state [definition, in intensional.examples.linearizability]
empty_state [definition, in intensional.examples.traversable_stack]
empty_state [definition, in intensional.examples.stack]
empty_state [definition, in intensional.examples.iterator]
empty_state [definition, in intensional.examples.well_bracketed]
empty_state [definition, in intensional.examples.file]
erec:165 [binder, in intensional.heap_lang.lifting]
erec:173 [binder, in intensional.heap_lang.lifting]
erec:180 [binder, in intensional.heap_lang.lifting]
eventO [definition, in intensional.heap_lang.lifting]
excl_auth_alloc [lemma, in intensional.examples.iris_extra]
excl_auth_upd [lemma, in intensional.examples.iris_extra]
excl_auth_eq [lemma, in intensional.examples.iris_extra]
e_init:44 [binder, in intensional.heap_lang.adequacy]
e'':18 [binder, in intensional.heap_lang.proofmode]
e'':9 [binder, in intensional.heap_lang.proofmode]
e':17 [binder, in intensional.heap_lang.proofmode]
e':247 [binder, in intensional.examples.linearizability]
e':275 [binder, in intensional.heap_lang.lang]
e':49 [binder, in intensional.heap_lang.adequacy]
e':61 [binder, in intensional.examples.stack]
e':72 [binder, in intensional.examples.file]
e':73 [binder, in intensional.examples.well_bracketed]
e':8 [binder, in intensional.heap_lang.proofmode]
e':86 [binder, in intensional.examples.traversable_stack]
e':95 [binder, in intensional.examples.iterator]
e0:178 [binder, in intensional.heap_lang.lang]
e0:180 [binder, in intensional.heap_lang.lang]
e0:187 [binder, in intensional.heap_lang.lang]
e0:189 [binder, in intensional.heap_lang.lang]
e0:28 [binder, in intensional.heap_lang.lang]
e0:37 [binder, in intensional.heap_lang.lang]
e0:46 [binder, in intensional.heap_lang.lang]
e0:51 [binder, in intensional.heap_lang.lang]
e1:128 [binder, in intensional.heap_lang.lifting]
e1:160 [binder, in intensional.heap_lang.lang]
e1:165 [binder, in intensional.heap_lang.lang]
e1:166 [binder, in intensional.heap_lang.lang]
e1:169 [binder, in intensional.heap_lang.lang]
e1:170 [binder, in intensional.heap_lang.lang]
e1:173 [binder, in intensional.heap_lang.lang]
e1:175 [binder, in intensional.heap_lang.lang]
e1:181 [binder, in intensional.heap_lang.lang]
e1:183 [binder, in intensional.heap_lang.lang]
e1:190 [binder, in intensional.heap_lang.lang]
e1:193 [binder, in intensional.heap_lang.lifting]
e1:195 [binder, in intensional.heap_lang.lifting]
e1:202 [binder, in intensional.heap_lang.lifting]
e1:205 [binder, in intensional.heap_lang.lifting]
e1:21 [binder, in intensional.heap_lang.lang]
e1:26 [binder, in intensional.heap_lang.lang]
e1:26 [binder, in intensional.heap_lang.proofmode]
e1:273 [binder, in intensional.heap_lang.lang]
e1:286 [binder, in intensional.heap_lang.lang]
e1:289 [binder, in intensional.heap_lang.lang]
e1:29 [binder, in intensional.heap_lang.lang]
e1:299 [binder, in intensional.heap_lang.lang]
e1:303 [binder, in intensional.heap_lang.lang]
e1:31 [binder, in intensional.heap_lang.lang]
e1:347 [binder, in intensional.heap_lang.lang]
e1:362 [binder, in intensional.heap_lang.lang]
e1:37 [binder, in intensional.heap_lang.proofmode]
e1:38 [binder, in intensional.heap_lang.lang]
e1:381 [binder, in intensional.heap_lang.lang]
e1:41 [binder, in intensional.heap_lang.lang]
e1:44 [binder, in intensional.heap_lang.lang]
e1:47 [binder, in intensional.heap_lang.lang]
e1:49 [binder, in intensional.heap_lang.lang]
e1:52 [binder, in intensional.heap_lang.lang]
e1:81 [binder, in intensional.heap_lang.lang]
e1:91 [binder, in intensional.heap_lang.lang]
e2':389 [binder, in intensional.heap_lang.lang]
e2:126 [binder, in intensional.heap_lang.lifting]
e2:167 [binder, in intensional.heap_lang.lang]
e2:171 [binder, in intensional.heap_lang.lang]
e2:194 [binder, in intensional.heap_lang.lifting]
e2:196 [binder, in intensional.heap_lang.lifting]
e2:203 [binder, in intensional.heap_lang.lifting]
e2:206 [binder, in intensional.heap_lang.lifting]
e2:22 [binder, in intensional.heap_lang.lang]
e2:27 [binder, in intensional.heap_lang.lang]
e2:27 [binder, in intensional.heap_lang.proofmode]
e2:287 [binder, in intensional.heap_lang.lang]
e2:290 [binder, in intensional.heap_lang.lang]
e2:30 [binder, in intensional.heap_lang.lang]
e2:300 [binder, in intensional.heap_lang.lang]
e2:304 [binder, in intensional.heap_lang.lang]
e2:32 [binder, in intensional.heap_lang.lang]
e2:333 [binder, in intensional.heap_lang.lifting]
e2:350 [binder, in intensional.heap_lang.lang]
e2:357 [binder, in intensional.heap_lang.lang]
e2:363 [binder, in intensional.heap_lang.lang]
e2:38 [binder, in intensional.heap_lang.proofmode]
e2:384 [binder, in intensional.heap_lang.lang]
e2:39 [binder, in intensional.heap_lang.lang]
e2:42 [binder, in intensional.heap_lang.lang]
e2:45 [binder, in intensional.heap_lang.lang]
e2:48 [binder, in intensional.heap_lang.lang]
e2:50 [binder, in intensional.heap_lang.lang]
e2:53 [binder, in intensional.heap_lang.lang]
e2:82 [binder, in intensional.heap_lang.lang]
e2:92 [binder, in intensional.heap_lang.lang]
E:100 [binder, in intensional.heap_lang.proofmode]
e:104 [binder, in intensional.heap_lang.lifting]
E:104 [binder, in intensional.heap_lang.array]
E:109 [binder, in intensional.heap_lang.proofmode]
e:11 [binder, in intensional.heap_lang.adequacy]
E:110 [binder, in intensional.heap_lang.array]
E:116 [binder, in intensional.heap_lang.array]
E:119 [binder, in intensional.heap_lang.proofmode]
E:123 [binder, in intensional.heap_lang.array]
e:125 [binder, in intensional.heap_lang.lang]
E:128 [binder, in intensional.heap_lang.proofmode]
E:130 [binder, in intensional.heap_lang.array]
e:131 [binder, in intensional.heap_lang.lang]
e:135 [binder, in intensional.heap_lang.lifting]
e:137 [binder, in intensional.heap_lang.lang]
E:138 [binder, in intensional.heap_lang.array]
E:138 [binder, in intensional.heap_lang.proofmode]
E:14 [binder, in intensional.heap_lang.proofmode]
e:143 [binder, in intensional.heap_lang.lang]
E:146 [binder, in intensional.heap_lang.array]
E:148 [binder, in intensional.heap_lang.proofmode]
e:149 [binder, in intensional.heap_lang.lang]
e:153 [binder, in intensional.heap_lang.lang]
E:154 [binder, in intensional.heap_lang.array]
e:157 [binder, in intensional.heap_lang.lifting]
E:159 [binder, in intensional.heap_lang.proofmode]
e:16 [binder, in intensional.heap_lang.proofmode]
E:162 [binder, in intensional.heap_lang.array]
e:170 [binder, in intensional.heap_lang.lifting]
E:170 [binder, in intensional.heap_lang.proofmode]
E:171 [binder, in intensional.heap_lang.array]
E:18 [binder, in intensional.examples.linearizability]
E:180 [binder, in intensional.heap_lang.array]
E:182 [binder, in intensional.heap_lang.proofmode]
E:189 [binder, in intensional.heap_lang.array]
e:192 [binder, in intensional.heap_lang.lang]
E:192 [binder, in intensional.heap_lang.proofmode]
e:197 [binder, in intensional.heap_lang.lang]
E:198 [binder, in intensional.heap_lang.array]
e:20 [binder, in intensional.heap_lang.lang]
E:203 [binder, in intensional.heap_lang.proofmode]
E:205 [binder, in intensional.heap_lang.array]
E:210 [binder, in intensional.heap_lang.lifting]
E:212 [binder, in intensional.heap_lang.array]
E:212 [binder, in intensional.heap_lang.proofmode]
E:216 [binder, in intensional.heap_lang.lifting]
E:220 [binder, in intensional.heap_lang.array]
E:224 [binder, in intensional.heap_lang.lifting]
e:225 [binder, in intensional.heap_lang.lifting]
E:228 [binder, in intensional.heap_lang.lifting]
e:229 [binder, in intensional.heap_lang.lifting]
e:24 [binder, in intensional.heap_lang.lang]
E:24 [binder, in intensional.heap_lang.proofmode]
E:243 [binder, in intensional.heap_lang.lifting]
e:244 [binder, in intensional.examples.linearizability]
E:249 [binder, in intensional.heap_lang.lifting]
E:251 [binder, in intensional.examples.linearizability]
E:255 [binder, in intensional.heap_lang.lifting]
E:259 [binder, in intensional.heap_lang.lifting]
e:26 [binder, in intensional.heap_lang.adequacy]
e:262 [binder, in intensional.heap_lang.lang]
E:263 [binder, in intensional.heap_lang.lifting]
E:268 [binder, in intensional.heap_lang.lifting]
E:273 [binder, in intensional.heap_lang.lifting]
E:278 [binder, in intensional.heap_lang.lifting]
E:283 [binder, in intensional.heap_lang.lifting]
E:290 [binder, in intensional.heap_lang.lifting]
E:297 [binder, in intensional.heap_lang.lifting]
E:303 [binder, in intensional.heap_lang.lifting]
e:306 [binder, in intensional.heap_lang.lang]
E:309 [binder, in intensional.heap_lang.lifting]
E:314 [binder, in intensional.heap_lang.lifting]
E:319 [binder, in intensional.heap_lang.lifting]
e:322 [binder, in intensional.heap_lang.lifting]
e:328 [binder, in intensional.heap_lang.lifting]
e:33 [binder, in intensional.heap_lang.lang]
e:333 [binder, in intensional.heap_lang.lang]
E:337 [binder, in intensional.heap_lang.lifting]
e:338 [binder, in intensional.heap_lang.lifting]
e:34 [binder, in intensional.heap_lang.lang]
E:346 [binder, in intensional.heap_lang.lifting]
e:346 [binder, in intensional.heap_lang.lang]
e:35 [binder, in intensional.heap_lang.lang]
E:35 [binder, in intensional.heap_lang.proofmode]
E:352 [binder, in intensional.heap_lang.lifting]
e:354 [binder, in intensional.heap_lang.lang]
e:36 [binder, in intensional.heap_lang.lang]
E:361 [binder, in intensional.heap_lang.lifting]
e:371 [binder, in intensional.heap_lang.lang]
e:375 [binder, in intensional.heap_lang.lang]
e:392 [binder, in intensional.heap_lang.lang]
e:40 [binder, in intensional.heap_lang.lang]
e:40 [binder, in intensional.examples.file]
e:43 [binder, in intensional.heap_lang.lang]
e:43 [binder, in intensional.heap_lang.adequacy]
E:45 [binder, in intensional.examples.linearizability]
E:46 [binder, in intensional.heap_lang.proofmode]
E:5 [binder, in intensional.heap_lang.proofmode]
E:52 [binder, in intensional.heap_lang.array]
E:53 [binder, in intensional.heap_lang.proofmode]
e:54 [binder, in intensional.heap_lang.lang]
e:55 [binder, in intensional.heap_lang.lang]
E:58 [binder, in intensional.heap_lang.array]
e:58 [binder, in intensional.examples.stack]
e:59 [binder, in intensional.heap_lang.lang]
E:61 [binder, in intensional.heap_lang.proofmode]
e:63 [binder, in intensional.heap_lang.proofmode]
E:64 [binder, in intensional.heap_lang.array]
e:64 [binder, in intensional.heap_lang.lang]
e:66 [binder, in intensional.heap_lang.proofmode]
e:69 [binder, in intensional.examples.file]
e:7 [binder, in intensional.heap_lang.proofmode]
e:70 [binder, in intensional.heap_lang.lifting]
E:70 [binder, in intensional.heap_lang.array]
e:70 [binder, in intensional.examples.well_bracketed]
E:72 [binder, in intensional.heap_lang.proofmode]
e:74 [binder, in intensional.heap_lang.proofmode]
E:76 [binder, in intensional.heap_lang.array]
e:77 [binder, in intensional.heap_lang.proofmode]
e:79 [binder, in intensional.heap_lang.lang]
E:83 [binder, in intensional.heap_lang.array]
e:83 [binder, in intensional.examples.traversable_stack]
E:83 [binder, in intensional.heap_lang.proofmode]
E:90 [binder, in intensional.heap_lang.array]
E:91 [binder, in intensional.heap_lang.proofmode]
e:92 [binder, in intensional.examples.iterator]
E:97 [binder, in intensional.heap_lang.array]

F

f [projection, in intensional.examples.linearizability]
faa_atomic [instance, in intensional.heap_lang.lifting]
file [library]
filelibN [definition, in intensional.examples.file]
filelib_spec [definition, in intensional.examples.file]
file_trace_nil [lemma, in intensional.examples.file]
file_trace_read [lemma, in intensional.examples.file]
file_trace_close [lemma, in intensional.examples.file]
file_trace_open [lemma, in intensional.examples.file]
file_trace [definition, in intensional.examples.file]
filter_check_single_tag_eq [lemma, in intensional.examples.trace_helpers]
filter_check_single_tag_neq [lemma, in intensional.examples.trace_helpers]
filter_Forall_id [lemma, in intensional.examples.stdpp_extra]
filter_is_nil [lemma, in intensional.examples.stdpp_extra]
foreach_impl:69 [binder, in intensional.examples.traversable_stack]
foreach_spec [definition, in intensional.examples.traversable_stack]
foreach:25 [binder, in intensional.examples.traversable_stack]
fork_atomic [instance, in intensional.heap_lang.lifting]
fresh_atomic [instance, in intensional.heap_lang.lifting]
fresh_locs_fresh [lemma, in intensional.heap_lang.locations]
fresh_locs [definition, in intensional.heap_lang.locations]
fresh_tag_nocheck [lemma, in intensional.examples.trace_helpers]
fst_atomic [instance, in intensional.heap_lang.lifting]
f:102 [binder, in intensional.heap_lang.lifting]
f:113 [binder, in intensional.heap_lang.lifting]
f:12 [binder, in intensional.examples.tactics]
f:16 [binder, in intensional.examples.tactics]
f:163 [binder, in intensional.heap_lang.lifting]
f:168 [binder, in intensional.heap_lang.lifting]
f:171 [binder, in intensional.heap_lang.lifting]
f:178 [binder, in intensional.heap_lang.lifting]
f:18 [binder, in intensional.heap_lang.lang]
f:225 [binder, in intensional.heap_lang.lang]
f:229 [binder, in intensional.heap_lang.lang]
f:23 [binder, in intensional.examples.tactics]
f:23 [binder, in intensional.examples.stack_impl]
f:260 [binder, in intensional.heap_lang.lang]
f:271 [binder, in intensional.heap_lang.lang]
f:28 [binder, in intensional.examples.traversable_stack]
f:32 [binder, in intensional.examples.well_bracketed]
f:34 [binder, in intensional.examples.tactics]
f:36 [binder, in intensional.examples.well_bracketed]
f:38 [binder, in intensional.examples.traversable_stack]
f:39 [binder, in intensional.examples.well_bracketed]
f:43 [binder, in intensional.examples.well_bracketed]
f:52 [binder, in intensional.examples.traversable_stack]
f:54 [binder, in intensional.examples.well_bracketed]
f:56 [binder, in intensional.examples.traversable_stack]
f:56 [binder, in intensional.examples.well_bracketed]
f:57 [binder, in intensional.heap_lang.lang]
f:58 [binder, in intensional.examples.well_bracketed]
f:59 [binder, in intensional.examples.traversable_stack]
f:64 [binder, in intensional.heap_lang.proofmode]
f:7 [binder, in intensional.examples.tactics]
f:75 [binder, in intensional.heap_lang.proofmode]
f:8 [binder, in intensional.examples.well_bracketed]

G

gmap_of_trace_valid [lemma, in intensional.heap_lang.lifting]
gmap_of_trace_hist_valid_prefix [lemma, in intensional.heap_lang.lifting]
gmap_of_trace_dom [lemma, in intensional.heap_lang.lifting]
gmap_of_trace_snoc [lemma, in intensional.heap_lang.lifting]
gmap_of_trace [definition, in intensional.heap_lang.lifting]
good_trace_nil [lemma, in intensional.examples.traversable_stack]
good_trace [definition, in intensional.examples.traversable_stack]
good_trace_for_foreach [constructor, in intensional.examples.traversable_stack]
good_trace_for_pop [constructor, in intensional.examples.traversable_stack]
good_trace_for_pop_nil [constructor, in intensional.examples.traversable_stack]
good_trace_for_push [constructor, in intensional.examples.traversable_stack]
good_trace_for_nil [constructor, in intensional.examples.traversable_stack]
good_trace_for [inductive, in intensional.examples.traversable_stack]
good_stack_trace_pop [lemma, in intensional.examples.stack]
good_stack_trace_pop_nil [lemma, in intensional.examples.stack]
good_stack_trace_push [lemma, in intensional.examples.stack]
good_stack_trace_nil [lemma, in intensional.examples.stack]
good_stack_trace [definition, in intensional.examples.stack]
good_trace:46 [binder, in intensional.heap_lang.adequacy]
gs:136 [binder, in intensional.examples.linearizability]
g:157 [binder, in intensional.examples.linearizability]

H

head_step_to_val [lemma, in intensional.heap_lang.lang]
heap [section, in intensional.heap_lang.proofmode]
heapG [record, in intensional.heap_lang.lifting]
HeapG [constructor, in intensional.heap_lang.lifting]
heapG_irisG [instance, in intensional.heap_lang.lifting]
heapG_traceG [projection, in intensional.heap_lang.lifting]
heapG_proph_mapG [projection, in intensional.heap_lang.lifting]
heapG_gen_heapG [projection, in intensional.heap_lang.lifting]
heapG_invG [projection, in intensional.heap_lang.lifting]
heapG0:11 [binder, in intensional.heap_lang.proofmode]
heapG0:12 [binder, in intensional.examples.well_bracketed]
heapG0:12 [binder, in intensional.examples.file]
heapG0:15 [binder, in intensional.examples.linearizability]
heapG0:15 [binder, in intensional.examples.traversable_stack]
heapG0:15 [binder, in intensional.examples.stack]
heapG0:15 [binder, in intensional.heap_lang.adequacy]
heapG0:17 [binder, in intensional.examples.iterator]
heapG0:17 [binder, in intensional.examples.file]
heapG0:19 [binder, in intensional.examples.well_bracketed]
heapG0:2 [binder, in intensional.heap_lang.array]
heapG0:2 [binder, in intensional.examples.traversable_stack]
heapG0:2 [binder, in intensional.examples.stack]
heapG0:2 [binder, in intensional.heap_lang.proofmode]
heapG0:2 [binder, in intensional.examples.iterator]
heapG0:2 [binder, in intensional.examples.well_bracketed]
heapG0:2 [binder, in intensional.examples.file]
heapG0:20 [binder, in intensional.heap_lang.proofmode]
heapG0:208 [binder, in intensional.heap_lang.lifting]
heapG0:23 [binder, in intensional.examples.traversable_stack]
heapG0:23 [binder, in intensional.examples.stack]
heapG0:25 [binder, in intensional.examples.iterator]
heapG0:30 [binder, in intensional.heap_lang.adequacy]
heapG0:32 [binder, in intensional.heap_lang.proofmode]
heapG0:32 [binder, in intensional.examples.iterator]
heapG0:33 [binder, in intensional.examples.traversable_stack]
heapG0:39 [binder, in intensional.examples.iterator]
heapG0:43 [binder, in intensional.heap_lang.proofmode]
heapG0:47 [binder, in intensional.examples.linearizability]
heapG0:50 [binder, in intensional.heap_lang.proofmode]
heapG0:54 [binder, in intensional.examples.stack]
heapG0:57 [binder, in intensional.heap_lang.proofmode]
heapG0:65 [binder, in intensional.examples.file]
heapG0:66 [binder, in intensional.examples.well_bracketed]
heapG0:68 [binder, in intensional.heap_lang.proofmode]
heapG0:7 [binder, in intensional.examples.file]
heapG0:79 [binder, in intensional.examples.traversable_stack]
heapG0:79 [binder, in intensional.heap_lang.proofmode]
heapG0:8 [binder, in intensional.examples.traversable_stack]
heapG0:8 [binder, in intensional.examples.stack]
heapG0:88 [binder, in intensional.examples.iterator]
heapG0:9 [binder, in intensional.heap_lang.array]
heapG0:9 [binder, in intensional.examples.iterator]
heapG0:95 [binder, in intensional.heap_lang.lifting]
heapPreG [record, in intensional.heap_lang.adequacy]
HeapPreG [constructor, in intensional.heap_lang.adequacy]
heapPreG0:22 [binder, in intensional.heap_lang.adequacy]
heapPreG0:9 [binder, in intensional.heap_lang.adequacy]
heap_array_to_seq_mapsto [lemma, in intensional.heap_lang.lifting]
heap_array_to_seq_meta [lemma, in intensional.heap_lang.lifting]
heap_lang [definition, in intensional.heap_lang.lang]
heap_ectx_lang [definition, in intensional.heap_lang.lang]
heap_ectxi_lang [definition, in intensional.heap_lang.lang]
heap_lang.heap_lang_mixin [lemma, in intensional.heap_lang.lang]
heap_lang.new_proph_id_fresh [lemma, in intensional.heap_lang.lang]
heap_lang.alloc_fresh [lemma, in intensional.heap_lang.lang]
heap_lang.fill_item_no_val_inj [lemma, in intensional.heap_lang.lang]
heap_lang.head_ctx_step_val [lemma, in intensional.heap_lang.lang]
heap_lang.val_head_stuck [lemma, in intensional.heap_lang.lang]
heap_lang.fill_item_val [lemma, in intensional.heap_lang.lang]
heap_lang.fill_item_inj [instance, in intensional.heap_lang.lang]
heap_lang.FreshS [constructor, in intensional.heap_lang.lang]
heap_lang.EmitS [constructor, in intensional.heap_lang.lang]
heap_lang.ResolveS [constructor, in intensional.heap_lang.lang]
heap_lang.NewProphS [constructor, in intensional.heap_lang.lang]
heap_lang.FaaS [constructor, in intensional.heap_lang.lang]
heap_lang.CmpXchgS [constructor, in intensional.heap_lang.lang]
heap_lang.StoreS [constructor, in intensional.heap_lang.lang]
heap_lang.LoadS [constructor, in intensional.heap_lang.lang]
heap_lang.AllocNS [constructor, in intensional.heap_lang.lang]
heap_lang.ForkS [constructor, in intensional.heap_lang.lang]
heap_lang.CaseRS [constructor, in intensional.heap_lang.lang]
heap_lang.CaseLS [constructor, in intensional.heap_lang.lang]
heap_lang.SndS [constructor, in intensional.heap_lang.lang]
heap_lang.FstS [constructor, in intensional.heap_lang.lang]
heap_lang.IfFalseS [constructor, in intensional.heap_lang.lang]
heap_lang.IfTrueS [constructor, in intensional.heap_lang.lang]
heap_lang.BinOpS [constructor, in intensional.heap_lang.lang]
heap_lang.UnOpS [constructor, in intensional.heap_lang.lang]
heap_lang.BetaS [constructor, in intensional.heap_lang.lang]
heap_lang.InjRS [constructor, in intensional.heap_lang.lang]
heap_lang.InjLS [constructor, in intensional.heap_lang.lang]
heap_lang.PairS [constructor, in intensional.heap_lang.lang]
heap_lang.RecS [constructor, in intensional.heap_lang.lang]
heap_lang.head_step [inductive, in intensional.heap_lang.lang]
heap_lang.tags [definition, in intensional.heap_lang.lang]
heap_lang.state_init_heap_singleton [lemma, in intensional.heap_lang.lang]
heap_lang.state_init_heap [definition, in intensional.heap_lang.lang]
heap_lang.heap_array_map_disjoint [lemma, in intensional.heap_lang.lang]
heap_lang.heap_array_lookup [lemma, in intensional.heap_lang.lang]
heap_lang.heap_array_singleton [lemma, in intensional.heap_lang.lang]
heap_lang.heap_array [definition, in intensional.heap_lang.lang]
heap_lang.state_upd_used_proph_id [definition, in intensional.heap_lang.lang]
heap_lang.state_add_event [definition, in intensional.heap_lang.lang]
heap_lang.state_upd_heap [definition, in intensional.heap_lang.lang]
heap_lang.bin_op_eval [definition, in intensional.heap_lang.lang]
heap_lang.bin_op_eval_loc [definition, in intensional.heap_lang.lang]
heap_lang.bin_op_eval_bool [definition, in intensional.heap_lang.lang]
heap_lang.bin_op_eval_int [definition, in intensional.heap_lang.lang]
heap_lang.un_op_eval [definition, in intensional.heap_lang.lang]
heap_lang.subst' [definition, in intensional.heap_lang.lang]
heap_lang.subst [definition, in intensional.heap_lang.lang]
heap_lang.fill_item [definition, in intensional.heap_lang.lang]
heap_lang.FreshCtx [constructor, in intensional.heap_lang.lang]
heap_lang.EmitCtx [constructor, in intensional.heap_lang.lang]
heap_lang.ResolveRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.ResolveMCtx [constructor, in intensional.heap_lang.lang]
heap_lang.ResolveLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.FaaRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.FaaLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.CmpXchgRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.CmpXchgMCtx [constructor, in intensional.heap_lang.lang]
heap_lang.CmpXchgLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.StoreRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.StoreLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.LoadCtx [constructor, in intensional.heap_lang.lang]
heap_lang.AllocNRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.AllocNLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.CaseCtx [constructor, in intensional.heap_lang.lang]
heap_lang.InjRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.InjLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.SndCtx [constructor, in intensional.heap_lang.lang]
heap_lang.FstCtx [constructor, in intensional.heap_lang.lang]
heap_lang.PairRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.PairLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.IfCtx [constructor, in intensional.heap_lang.lang]
heap_lang.BinOpRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.BinOpLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.UnOpCtx [constructor, in intensional.heap_lang.lang]
heap_lang.AppRCtx [constructor, in intensional.heap_lang.lang]
heap_lang.AppLCtx [constructor, in intensional.heap_lang.lang]
heap_lang.ectx_item [inductive, in intensional.heap_lang.lang]
heap_lang.exprO [definition, in intensional.heap_lang.lang]
heap_lang.valO [definition, in intensional.heap_lang.lang]
heap_lang.locO [definition, in intensional.heap_lang.lang]
heap_lang.stateO [definition, in intensional.heap_lang.lang]
heap_lang.expr_inhabited [instance, in intensional.heap_lang.lang]
heap_lang.val_inhabited [instance, in intensional.heap_lang.lang]
heap_lang.state_inhabited [instance, in intensional.heap_lang.lang]
heap_lang.val_countable [instance, in intensional.heap_lang.lang]
heap_lang.expr_countable [instance, in intensional.heap_lang.lang]
heap_lang.bin_op_countable [instance, in intensional.heap_lang.lang]
heap_lang.un_op_finite [instance, in intensional.heap_lang.lang]
heap_lang.base_lit_countable [instance, in intensional.heap_lang.lang]
heap_lang.val_eq_dec [instance, in intensional.heap_lang.lang]
heap_lang.expr_eq_dec [instance, in intensional.heap_lang.lang]
heap_lang.bin_op_eq_dec [instance, in intensional.heap_lang.lang]
heap_lang.un_op_eq_dec [instance, in intensional.heap_lang.lang]
heap_lang.base_lit_eq_dec [instance, in intensional.heap_lang.lang]
heap_lang.of_val_inj [instance, in intensional.heap_lang.lang]
heap_lang.of_to_val [lemma, in intensional.heap_lang.lang]
heap_lang.to_of_val [lemma, in intensional.heap_lang.lang]
heap_lang.used_proph_id [projection, in intensional.heap_lang.lang]
heap_lang.trace [projection, in intensional.heap_lang.lang]
heap_lang.heap [projection, in intensional.heap_lang.lang]
heap_lang.state [record, in intensional.heap_lang.lang]
heap_lang.vals_compare_safe [definition, in intensional.heap_lang.lang]
heap_lang.val_is_unboxed_dec [instance, in intensional.heap_lang.lang]
heap_lang.lit_is_unboxed_dec [instance, in intensional.heap_lang.lang]
heap_lang.val_is_unboxed [definition, in intensional.heap_lang.lang]
heap_lang.lit_is_unboxed [definition, in intensional.heap_lang.lang]
heap_lang.to_val [definition, in intensional.heap_lang.lang]
heap_lang.of_val [abbreviation, in intensional.heap_lang.lang]
heap_lang.observation [definition, in intensional.heap_lang.lang]
heap_lang.InjRV [constructor, in intensional.heap_lang.lang]
heap_lang.InjLV [constructor, in intensional.heap_lang.lang]
heap_lang.PairV [constructor, in intensional.heap_lang.lang]
heap_lang.RecV [constructor, in intensional.heap_lang.lang]
heap_lang.LitV [constructor, in intensional.heap_lang.lang]
heap_lang.val [inductive, in intensional.heap_lang.lang]
heap_lang.Fresh [constructor, in intensional.heap_lang.lang]
heap_lang.Emit [constructor, in intensional.heap_lang.lang]
heap_lang.Resolve [constructor, in intensional.heap_lang.lang]
heap_lang.NewProph [constructor, in intensional.heap_lang.lang]
heap_lang.FAA [constructor, in intensional.heap_lang.lang]
heap_lang.CmpXchg [constructor, in intensional.heap_lang.lang]
heap_lang.Store [constructor, in intensional.heap_lang.lang]
heap_lang.Load [constructor, in intensional.heap_lang.lang]
heap_lang.AllocN [constructor, in intensional.heap_lang.lang]
heap_lang.Fork [constructor, in intensional.heap_lang.lang]
heap_lang.Case [constructor, in intensional.heap_lang.lang]
heap_lang.InjR [constructor, in intensional.heap_lang.lang]
heap_lang.InjL [constructor, in intensional.heap_lang.lang]
heap_lang.Snd [constructor, in intensional.heap_lang.lang]
heap_lang.Fst [constructor, in intensional.heap_lang.lang]
heap_lang.Pair [constructor, in intensional.heap_lang.lang]
heap_lang.If [constructor, in intensional.heap_lang.lang]
heap_lang.BinOp [constructor, in intensional.heap_lang.lang]
heap_lang.UnOp [constructor, in intensional.heap_lang.lang]
heap_lang.App [constructor, in intensional.heap_lang.lang]
heap_lang.Rec [constructor, in intensional.heap_lang.lang]
heap_lang.Var [constructor, in intensional.heap_lang.lang]
heap_lang.Val [constructor, in intensional.heap_lang.lang]
heap_lang.expr [inductive, in intensional.heap_lang.lang]
heap_lang.OffsetOp [constructor, in intensional.heap_lang.lang]
heap_lang.EqOp [constructor, in intensional.heap_lang.lang]
heap_lang.LtOp [constructor, in intensional.heap_lang.lang]
heap_lang.LeOp [constructor, in intensional.heap_lang.lang]
heap_lang.ShiftROp [constructor, in intensional.heap_lang.lang]
heap_lang.ShiftLOp [constructor, in intensional.heap_lang.lang]
heap_lang.XorOp [constructor, in intensional.heap_lang.lang]
heap_lang.OrOp [constructor, in intensional.heap_lang.lang]
heap_lang.AndOp [constructor, in intensional.heap_lang.lang]
heap_lang.RemOp [constructor, in intensional.heap_lang.lang]
heap_lang.QuotOp [constructor, in intensional.heap_lang.lang]
heap_lang.MultOp [constructor, in intensional.heap_lang.lang]
heap_lang.MinusOp [constructor, in intensional.heap_lang.lang]
heap_lang.PlusOp [constructor, in intensional.heap_lang.lang]
heap_lang.bin_op [inductive, in intensional.heap_lang.lang]
heap_lang.MinusUnOp [constructor, in intensional.heap_lang.lang]
heap_lang.NegOp [constructor, in intensional.heap_lang.lang]
heap_lang.un_op [inductive, in intensional.heap_lang.lang]
heap_lang.LitProphecy [constructor, in intensional.heap_lang.lang]
heap_lang.LitTag [constructor, in intensional.heap_lang.lang]
heap_lang.LitLoc [constructor, in intensional.heap_lang.lang]
heap_lang.LitPoison [constructor, in intensional.heap_lang.lang]
heap_lang.LitUnit [constructor, in intensional.heap_lang.lang]
heap_lang.LitBool [constructor, in intensional.heap_lang.lang]
heap_lang.LitInt [constructor, in intensional.heap_lang.lang]
heap_lang.base_lit [inductive, in intensional.heap_lang.lang]
heap_lang.proph_id [definition, in intensional.heap_lang.lang]
heap_lang [module, in intensional.heap_lang.lang]
heap_invariance [definition, in intensional.heap_lang.adequacy]
heap_adequacy [definition, in intensional.heap_lang.adequacy]
heap_preG_trace [projection, in intensional.heap_lang.adequacy]
heap_preG_proph [projection, in intensional.heap_lang.adequacy]
heap_preG_heap [projection, in intensional.heap_lang.adequacy]
heap_preG_iris [projection, in intensional.heap_lang.adequacy]
heapΣ [definition, in intensional.heap_lang.adequacy]
hist [definition, in intensional.heap_lang.lifting]
hist_trace_is_prefix [lemma, in intensional.heap_lang.lifting]
hist_persistent [instance, in intensional.heap_lang.lifting]
hI:45 [binder, in intensional.heap_lang.lifting]
HNN':128 [binder, in intensional.examples.linearizability]
hT:32 [binder, in intensional.heap_lang.lifting]
hT:35 [binder, in intensional.heap_lang.lifting]
hT:38 [binder, in intensional.heap_lang.lifting]
hT:41 [binder, in intensional.heap_lang.lifting]
hT:44 [binder, in intensional.heap_lang.lifting]
hT:91 [binder, in intensional.heap_lang.lifting]
H':39 [binder, in intensional.examples.tactics]
H0:123 [binder, in intensional.examples.linearizability]
H0:236 [binder, in intensional.examples.linearizability]
H0:249 [binder, in intensional.examples.linearizability]
H0:255 [binder, in intensional.examples.linearizability]
H0:40 [binder, in intensional.heap_lang.adequacy]
H0:50 [binder, in intensional.heap_lang.adequacy]
H0:51 [binder, in intensional.heap_lang.adequacy]
H0:52 [binder, in intensional.heap_lang.adequacy]
H0:83 [binder, in intensional.heap_lang.lifting]
H2:125 [binder, in intensional.examples.linearizability]
H2:238 [binder, in intensional.examples.linearizability]
H:102 [binder, in intensional.examples.iterator]
H:111 [binder, in intensional.examples.linearizability]
H:118 [binder, in intensional.examples.linearizability]
H:119 [binder, in intensional.examples.linearizability]
H:122 [binder, in intensional.examples.linearizability]
H:15 [binder, in intensional.examples.stdpp_extra]
H:16 [binder, in intensional.examples.linearizability]
H:16 [binder, in intensional.examples.iris_extra]
H:2 [binder, in intensional.examples.stack_impl]
H:235 [binder, in intensional.examples.linearizability]
h:242 [binder, in intensional.heap_lang.lang]
H:243 [binder, in intensional.examples.linearizability]
h:250 [binder, in intensional.heap_lang.lang]
H:26 [binder, in intensional.examples.tactics]
H:3 [binder, in intensional.examples.iris_extra]
H:38 [binder, in intensional.examples.tactics]
H:38 [binder, in intensional.heap_lang.adequacy]
H:39 [binder, in intensional.examples.stack]
H:44 [binder, in intensional.examples.linearizability]
H:47 [binder, in intensional.examples.well_bracketed]
H:50 [binder, in intensional.heap_lang.lifting]
H:53 [binder, in intensional.heap_lang.lifting]
H:53 [binder, in intensional.examples.file]
H:56 [binder, in intensional.heap_lang.lifting]
H:60 [binder, in intensional.heap_lang.lifting]
H:63 [binder, in intensional.examples.traversable_stack]
H:63 [binder, in intensional.examples.stack]
H:64 [binder, in intensional.heap_lang.lifting]
H:64 [binder, in intensional.examples.iterator]
H:65 [binder, in intensional.examples.linearizability]
H:68 [binder, in intensional.heap_lang.lifting]
H:68 [binder, in intensional.examples.stack]
H:7 [binder, in intensional.examples.linearizability]
H:72 [binder, in intensional.heap_lang.lifting]
H:74 [binder, in intensional.examples.file]
H:75 [binder, in intensional.examples.well_bracketed]
h:76 [binder, in intensional.heap_lang.lifting]
H:78 [binder, in intensional.heap_lang.lifting]
H:79 [binder, in intensional.examples.file]
h:80 [binder, in intensional.heap_lang.lifting]
H:80 [binder, in intensional.examples.well_bracketed]
H:82 [binder, in intensional.heap_lang.lifting]
H:84 [binder, in intensional.examples.linearizability]
H:88 [binder, in intensional.examples.linearizability]
H:88 [binder, in intensional.examples.traversable_stack]
H:9 [binder, in intensional.examples.iris_extra]
H:9 [binder, in intensional.examples.stdpp_extra]
H:93 [binder, in intensional.heap_lang.lifting]
H:93 [binder, in intensional.examples.traversable_stack]
H:97 [binder, in intensional.examples.iterator]

I

if_false_atomic [instance, in intensional.heap_lang.lifting]
if_true_atomic [instance, in intensional.heap_lang.lifting]
imimpl:45 [binder, in intensional.heap_lang.adequacy]
init_impl:131 [binder, in intensional.examples.linearizability]
init_spec [definition, in intensional.examples.linearizability]
init:20 [binder, in intensional.examples.linearizability]
injl_atomic [instance, in intensional.heap_lang.lifting]
injr_atomic [instance, in intensional.heap_lang.lifting]
into_val_val [instance, in intensional.heap_lang.lifting]
iris_extra [library]
irreducible_resolve [lemma, in intensional.heap_lang.lang]
isClosed_impl:56 [binder, in intensional.examples.file]
isClosed:21 [binder, in intensional.examples.file]
isClosed:3 [binder, in intensional.examples.file]
isClosed:8 [binder, in intensional.examples.file]
isopen [definition, in intensional.examples.file]
isOpen_impl:55 [binder, in intensional.examples.file]
isopen_read_last [lemma, in intensional.examples.file]
isopen_open_last [lemma, in intensional.examples.file]
isopen_open' [lemma, in intensional.examples.file]
isopen_open [lemma, in intensional.examples.file]
isOpen:13 [binder, in intensional.examples.file]
isOpen:20 [binder, in intensional.examples.file]
isOpen:4 [binder, in intensional.examples.file]
isOpen:9 [binder, in intensional.examples.file]
is_lin [definition, in intensional.examples.linearizability]
is_call_return [definition, in intensional.examples.linearizability]
is_P_persistent [projection, in intensional.examples.linearizability]
is_P [projection, in intensional.examples.linearizability]
iterator [library]
iterator_impl:71 [binder, in intensional.examples.iterator]
iterator_trace_next [lemma, in intensional.examples.iterator]
iterator_trace_iterator [lemma, in intensional.examples.iterator]
iterator_trace_remove [lemma, in intensional.examples.iterator]
iterator_trace_add [lemma, in intensional.examples.iterator]
iterator_trace_size [lemma, in intensional.examples.iterator]
iterator_trace_nil [lemma, in intensional.examples.iterator]
iterator_trace [definition, in intensional.examples.iterator]
iterator_spec [definition, in intensional.examples.iterator]
iterator:28 [binder, in intensional.examples.iterator]
iterlibN [definition, in intensional.examples.iterator]
iterlib_spec [definition, in intensional.examples.iterator]
Iter_impl:67 [binder, in intensional.examples.iterator]
Iter:11 [binder, in intensional.examples.iterator]
Iter:19 [binder, in intensional.examples.iterator]
Iter:27 [binder, in intensional.examples.iterator]
Iter:34 [binder, in intensional.examples.iterator]
Iter:4 [binder, in intensional.examples.iterator]
Iter:43 [binder, in intensional.examples.iterator]
i1:202 [binder, in intensional.heap_lang.array]
i1:209 [binder, in intensional.heap_lang.array]
i1:217 [binder, in intensional.heap_lang.array]
i1:225 [binder, in intensional.heap_lang.array]
i1:311 [binder, in intensional.heap_lang.lifting]
i1:316 [binder, in intensional.heap_lang.lifting]
i1:326 [binder, in intensional.heap_lang.lang]
i2:203 [binder, in intensional.heap_lang.array]
i2:210 [binder, in intensional.heap_lang.array]
i2:218 [binder, in intensional.heap_lang.array]
i2:226 [binder, in intensional.heap_lang.array]
i2:312 [binder, in intensional.heap_lang.lifting]
i2:317 [binder, in intensional.heap_lang.lifting]
i2:327 [binder, in intensional.heap_lang.lang]
i:10 [binder, in intensional.heap_lang.locations]
i:101 [binder, in intensional.heap_lang.proofmode]
i:110 [binder, in intensional.heap_lang.proofmode]
i:120 [binder, in intensional.heap_lang.proofmode]
i:129 [binder, in intensional.heap_lang.proofmode]
i:139 [binder, in intensional.heap_lang.proofmode]
i:149 [binder, in intensional.heap_lang.proofmode]
i:160 [binder, in intensional.heap_lang.proofmode]
i:171 [binder, in intensional.heap_lang.proofmode]
i:18 [binder, in intensional.heap_lang.locations]
i:183 [binder, in intensional.heap_lang.proofmode]
i:193 [binder, in intensional.heap_lang.proofmode]
i:204 [binder, in intensional.heap_lang.proofmode]
i:213 [binder, in intensional.heap_lang.proofmode]
I:214 [binder, in intensional.heap_lang.lifting]
I:220 [binder, in intensional.heap_lang.lifting]
i:235 [binder, in intensional.heap_lang.lifting]
I:24 [binder, in intensional.heap_lang.adequacy]
I:24 [binder, in intensional.examples.stack_impl]
i:241 [binder, in intensional.heap_lang.lifting]
i:245 [binder, in intensional.heap_lang.lang]
i:247 [binder, in intensional.heap_lang.lifting]
i:253 [binder, in intensional.heap_lang.lifting]
I:29 [binder, in intensional.examples.traversable_stack]
i:29 [binder, in intensional.examples.stack]
i:3 [binder, in intensional.heap_lang.locations]
i:312 [binder, in intensional.heap_lang.lang]
i:37 [binder, in intensional.examples.stack]
i:4 [binder, in intensional.heap_lang.locations]
I:47 [binder, in intensional.heap_lang.lifting]
i:47 [binder, in intensional.examples.iterator]
i:49 [binder, in intensional.examples.stack]
i:5 [binder, in intensional.examples.stdpp_extra]
i:50 [binder, in intensional.heap_lang.array]
i:56 [binder, in intensional.heap_lang.array]
i:6 [binder, in intensional.heap_lang.array]
i:62 [binder, in intensional.heap_lang.array]
i:68 [binder, in intensional.heap_lang.array]
i:74 [binder, in intensional.heap_lang.array]
I:86 [binder, in intensional.heap_lang.lifting]

J

j:11 [binder, in intensional.heap_lang.locations]
j:241 [binder, in intensional.heap_lang.lang]
j:31 [binder, in intensional.examples.stack]
j:49 [binder, in intensional.examples.iterator]
j:84 [binder, in intensional.heap_lang.proofmode]
j:92 [binder, in intensional.heap_lang.proofmode]

K

Ki1:360 [binder, in intensional.heap_lang.lang]
Ki2:361 [binder, in intensional.heap_lang.lang]
Ki:191 [binder, in intensional.heap_lang.lang]
Ki:344 [binder, in intensional.heap_lang.lang]
Ki:345 [binder, in intensional.heap_lang.lang]
Ki:353 [binder, in intensional.heap_lang.lang]
K:102 [binder, in intensional.heap_lang.proofmode]
K:111 [binder, in intensional.heap_lang.proofmode]
K:121 [binder, in intensional.heap_lang.proofmode]
k:13 [binder, in intensional.heap_lang.lifting]
K:130 [binder, in intensional.heap_lang.proofmode]
K:140 [binder, in intensional.heap_lang.proofmode]
k:15 [binder, in intensional.heap_lang.locations]
K:150 [binder, in intensional.heap_lang.proofmode]
K:161 [binder, in intensional.heap_lang.proofmode]
K:172 [binder, in intensional.heap_lang.proofmode]
K:184 [binder, in intensional.heap_lang.proofmode]
K:194 [binder, in intensional.heap_lang.proofmode]
K:205 [binder, in intensional.heap_lang.proofmode]
K:214 [binder, in intensional.heap_lang.proofmode]
k:240 [binder, in intensional.heap_lang.lang]
K:25 [binder, in intensional.heap_lang.proofmode]
k:26 [binder, in intensional.examples.file]
K:36 [binder, in intensional.heap_lang.proofmode]
K:370 [binder, in intensional.heap_lang.lang]
k:50 [binder, in intensional.examples.iterator]
K:58 [binder, in intensional.heap_lang.proofmode]
k:59 [binder, in intensional.examples.iterator]
k:61 [binder, in intensional.examples.iterator]
K:69 [binder, in intensional.heap_lang.proofmode]
k:77 [binder, in intensional.examples.iterator]
k:84 [binder, in intensional.examples.iterator]
K:85 [binder, in intensional.heap_lang.proofmode]
K:93 [binder, in intensional.heap_lang.proofmode]

L

Lam [abbreviation, in intensional.heap_lang.notation]
LamV [abbreviation, in intensional.heap_lang.notation]
lang [library]
Learnt [inductive, in intensional.examples.tactics]
Let [abbreviation, in intensional.heap_lang.notation]
LetCtx [abbreviation, in intensional.heap_lang.notation]
libN [definition, in intensional.examples.linearizability]
lib_impl:242 [binder, in intensional.examples.linearizability]
lib_impl:232 [binder, in intensional.examples.linearizability]
lib_spec [definition, in intensional.examples.linearizability]
lib_impl:82 [binder, in intensional.examples.traversable_stack]
lib_impl:76 [binder, in intensional.examples.traversable_stack]
lib_impl:57 [binder, in intensional.examples.stack]
lib_impl:51 [binder, in intensional.examples.stack]
lib_impl:91 [binder, in intensional.examples.iterator]
lib_impl:85 [binder, in intensional.examples.iterator]
lib_impl:69 [binder, in intensional.examples.well_bracketed]
lib_impl:63 [binder, in intensional.examples.well_bracketed]
lib_impl:68 [binder, in intensional.examples.file]
lib_impl:62 [binder, in intensional.examples.file]
lib:19 [binder, in intensional.examples.file]
lib:21 [binder, in intensional.examples.well_bracketed]
lib:245 [binder, in intensional.examples.linearizability]
lib:25 [binder, in intensional.examples.stack]
lib:252 [binder, in intensional.examples.linearizability]
lib:35 [binder, in intensional.examples.traversable_stack]
lib:41 [binder, in intensional.examples.iterator]
lib:49 [binder, in intensional.examples.linearizability]
lib:59 [binder, in intensional.examples.stack]
lib:65 [binder, in intensional.examples.stack]
lib:70 [binder, in intensional.examples.file]
lib:71 [binder, in intensional.examples.well_bracketed]
lib:76 [binder, in intensional.examples.file]
lib:77 [binder, in intensional.examples.well_bracketed]
lib:84 [binder, in intensional.examples.traversable_stack]
lib:90 [binder, in intensional.examples.traversable_stack]
lib:93 [binder, in intensional.examples.iterator]
lib:99 [binder, in intensional.examples.iterator]
lifting [section, in intensional.heap_lang.lifting]
lifting [section, in intensional.heap_lang.array]
lifting [library]
linearizability [library]
linearizable [definition, in intensional.examples.linearizability]
linearizable_nil [lemma, in intensional.examples.linearizability]
linearization_fresh_tag_call_ret [lemma, in intensional.examples.linearizability]
linearization_trace_ret [constructor, in intensional.examples.linearizability]
linearization_trace_lin [constructor, in intensional.examples.linearizability]
linearization_trace_call [constructor, in intensional.examples.linearizability]
linearization_trace_nil [constructor, in intensional.examples.linearizability]
linearization_trace [inductive, in intensional.examples.linearizability]
linearized_sound_lin [constructor, in intensional.examples.linearizability]
linearized_sound_nil [constructor, in intensional.examples.linearizability]
linearized_sound [inductive, in intensional.examples.linearizability]
load_atomic [instance, in intensional.heap_lang.lifting]
loc [record, in intensional.heap_lang.locations]
locations [library]
locked_impl:49 [binder, in intensional.examples.well_bracketed]
locked:13 [binder, in intensional.examples.well_bracketed]
locked:22 [binder, in intensional.examples.well_bracketed]
locked:3 [binder, in intensional.examples.well_bracketed]
loc_add_inj [instance, in intensional.heap_lang.locations]
loc_add_0 [lemma, in intensional.heap_lang.locations]
loc_add_assoc [lemma, in intensional.heap_lang.locations]
loc_add [definition, in intensional.heap_lang.locations]
loc_infinite [instance, in intensional.heap_lang.locations]
loc_countable [instance, in intensional.heap_lang.locations]
loc_inhabited [instance, in intensional.heap_lang.locations]
loc_eq_decision [instance, in intensional.heap_lang.locations]
loc_car [projection, in intensional.heap_lang.locations]
lookup_snoc_Some [lemma, in intensional.examples.stdpp_extra]
ls:14 [binder, in intensional.heap_lang.locations]
ls:17 [binder, in intensional.heap_lang.locations]
ls:22 [binder, in intensional.heap_lang.locations]
ls:25 [binder, in intensional.heap_lang.locations]
lv:12 [binder, in intensional.examples.stack_impl]
l':234 [binder, in intensional.heap_lang.lifting]
l':239 [binder, in intensional.heap_lang.lifting]
l':58 [binder, in intensional.examples.traversable_stack]
l':61 [binder, in intensional.examples.traversable_stack]
l1:216 [binder, in intensional.heap_lang.lang]
l:10 [binder, in intensional.heap_lang.array]
l:10 [binder, in intensional.examples.stdpp_extra]
l:101 [binder, in intensional.heap_lang.lang]
l:103 [binder, in intensional.heap_lang.lang]
l:103 [binder, in intensional.heap_lang.proofmode]
l:105 [binder, in intensional.heap_lang.array]
l:105 [binder, in intensional.heap_lang.lang]
l:107 [binder, in intensional.heap_lang.lang]
l:11 [binder, in intensional.examples.traversable_stack]
l:11 [binder, in intensional.examples.stack]
l:111 [binder, in intensional.heap_lang.array]
l:112 [binder, in intensional.heap_lang.proofmode]
l:117 [binder, in intensional.heap_lang.array]
l:12 [binder, in intensional.heap_lang.lifting]
l:12 [binder, in intensional.heap_lang.locations]
l:122 [binder, in intensional.heap_lang.proofmode]
l:124 [binder, in intensional.heap_lang.array]
l:13 [binder, in intensional.heap_lang.array]
l:13 [binder, in intensional.heap_lang.locations]
l:131 [binder, in intensional.heap_lang.array]
l:131 [binder, in intensional.heap_lang.proofmode]
l:139 [binder, in intensional.heap_lang.array]
l:141 [binder, in intensional.heap_lang.proofmode]
l:147 [binder, in intensional.heap_lang.array]
l:151 [binder, in intensional.heap_lang.proofmode]
l:155 [binder, in intensional.heap_lang.array]
l:16 [binder, in intensional.heap_lang.array]
l:16 [binder, in intensional.examples.stack_impl]
l:16 [binder, in intensional.examples.stdpp_extra]
l:162 [binder, in intensional.heap_lang.proofmode]
l:163 [binder, in intensional.heap_lang.array]
l:172 [binder, in intensional.heap_lang.array]
l:173 [binder, in intensional.heap_lang.proofmode]
l:18 [binder, in intensional.examples.traversable_stack]
l:18 [binder, in intensional.examples.stack]
l:18 [binder, in intensional.examples.stack_impl]
l:181 [binder, in intensional.heap_lang.array]
l:185 [binder, in intensional.heap_lang.proofmode]
l:19 [binder, in intensional.heap_lang.locations]
l:190 [binder, in intensional.heap_lang.array]
l:195 [binder, in intensional.heap_lang.proofmode]
l:199 [binder, in intensional.heap_lang.array]
l:2 [binder, in intensional.examples.stdpp_extra]
l:20 [binder, in intensional.heap_lang.array]
l:20 [binder, in intensional.heap_lang.locations]
l:206 [binder, in intensional.heap_lang.array]
l:206 [binder, in intensional.heap_lang.proofmode]
l:213 [binder, in intensional.heap_lang.array]
l:215 [binder, in intensional.heap_lang.proofmode]
l:22 [binder, in intensional.heap_lang.array]
l:22 [binder, in intensional.examples.stack_impl]
l:221 [binder, in intensional.heap_lang.array]
l:23 [binder, in intensional.heap_lang.locations]
l:231 [binder, in intensional.heap_lang.lifting]
l:231 [binder, in intensional.heap_lang.lang]
l:235 [binder, in intensional.heap_lang.lang]
l:236 [binder, in intensional.heap_lang.lifting]
l:237 [binder, in intensional.heap_lang.lang]
l:243 [binder, in intensional.heap_lang.lang]
l:246 [binder, in intensional.heap_lang.lifting]
l:246 [binder, in intensional.heap_lang.lang]
l:25 [binder, in intensional.heap_lang.array]
l:251 [binder, in intensional.heap_lang.lang]
l:252 [binder, in intensional.heap_lang.lifting]
l:257 [binder, in intensional.heap_lang.lifting]
l:26 [binder, in intensional.examples.traversable_stack]
l:26 [binder, in intensional.heap_lang.locations]
l:261 [binder, in intensional.heap_lang.lifting]
l:264 [binder, in intensional.heap_lang.lifting]
l:269 [binder, in intensional.heap_lang.lifting]
l:274 [binder, in intensional.heap_lang.lifting]
l:279 [binder, in intensional.heap_lang.lifting]
l:284 [binder, in intensional.heap_lang.lifting]
l:29 [binder, in intensional.heap_lang.array]
l:291 [binder, in intensional.heap_lang.lifting]
l:298 [binder, in intensional.heap_lang.lifting]
l:3 [binder, in intensional.heap_lang.lifting]
l:3 [binder, in intensional.heap_lang.array]
l:3 [binder, in intensional.examples.stack_impl]
l:304 [binder, in intensional.heap_lang.lifting]
l:310 [binder, in intensional.heap_lang.lifting]
l:311 [binder, in intensional.heap_lang.lang]
l:313 [binder, in intensional.heap_lang.lang]
l:315 [binder, in intensional.heap_lang.lifting]
l:316 [binder, in intensional.heap_lang.lang]
l:319 [binder, in intensional.heap_lang.lang]
l:325 [binder, in intensional.heap_lang.lang]
l:33 [binder, in intensional.heap_lang.array]
l:353 [binder, in intensional.heap_lang.lifting]
l:362 [binder, in intensional.heap_lang.lifting]
l:367 [binder, in intensional.heap_lang.lang]
l:39 [binder, in intensional.heap_lang.array]
l:39 [binder, in intensional.examples.traversable_stack]
l:44 [binder, in intensional.examples.traversable_stack]
l:45 [binder, in intensional.examples.stack]
l:46 [binder, in intensional.heap_lang.array]
l:48 [binder, in intensional.examples.traversable_stack]
l:48 [binder, in intensional.examples.iterator]
l:5 [binder, in intensional.heap_lang.lang]
l:5 [binder, in intensional.heap_lang.locations]
l:50 [binder, in intensional.examples.traversable_stack]
l:54 [binder, in intensional.examples.traversable_stack]
l:55 [binder, in intensional.heap_lang.array]
l:56 [binder, in intensional.heap_lang.lang]
l:57 [binder, in intensional.examples.traversable_stack]
l:60 [binder, in intensional.examples.traversable_stack]
l:61 [binder, in intensional.heap_lang.array]
l:66 [binder, in intensional.heap_lang.lang]
l:67 [binder, in intensional.heap_lang.array]
l:7 [binder, in intensional.heap_lang.locations]
l:70 [binder, in intensional.heap_lang.lang]
l:70 [binder, in intensional.examples.traversable_stack]
l:73 [binder, in intensional.heap_lang.array]
l:77 [binder, in intensional.heap_lang.array]
l:8 [binder, in intensional.heap_lang.lifting]
l:84 [binder, in intensional.heap_lang.array]
l:88 [binder, in intensional.heap_lang.lifting]
l:88 [binder, in intensional.heap_lang.proofmode]
l:9 [binder, in intensional.heap_lang.locations]
l:9 [binder, in intensional.examples.stack_impl]
l:91 [binder, in intensional.heap_lang.array]
l:96 [binder, in intensional.heap_lang.proofmode]
l:98 [binder, in intensional.heap_lang.array]

M

mapsto_seq_array [lemma, in intensional.heap_lang.array]
Match [abbreviation, in intensional.heap_lang.notation]
model [record, in intensional.examples.linearizability]
module_invariance [lemma, in intensional.heap_lang.adequacy]
mx:200 [binder, in intensional.heap_lang.lang]
m':155 [binder, in intensional.examples.linearizability]
m:134 [binder, in intensional.examples.linearizability]
m:144 [binder, in intensional.examples.linearizability]
m:150 [binder, in intensional.examples.linearizability]
m:154 [binder, in intensional.examples.linearizability]
M:165 [binder, in intensional.examples.linearizability]
M:203 [binder, in intensional.examples.linearizability]
M:215 [binder, in intensional.examples.linearizability]
M:228 [binder, in intensional.examples.linearizability]
m:24 [binder, in intensional.examples.file]
m:30 [binder, in intensional.examples.file]
m:35 [binder, in intensional.examples.file]
m:44 [binder, in intensional.examples.file]
m:54 [binder, in intensional.heap_lang.adequacy]

N

new_proph_atomic [instance, in intensional.heap_lang.lifting]
next_impl:72 [binder, in intensional.examples.iterator]
next_spec [definition, in intensional.examples.iterator]
next:35 [binder, in intensional.examples.iterator]
noclose [definition, in intensional.examples.file]
noclose_read_last [lemma, in intensional.examples.file]
noclose_open_last [lemma, in intensional.examples.file]
noclose_open [lemma, in intensional.examples.file]
NONE [abbreviation, in intensional.heap_lang.notation]
NONEV [abbreviation, in intensional.heap_lang.notation]
notation [library]
not_check_tag_iff [lemma, in intensional.examples.trace_helpers]
N':127 [binder, in intensional.examples.linearizability]
N':240 [binder, in intensional.examples.linearizability]
n0:58 [binder, in intensional.examples.iterator]
n1:208 [binder, in intensional.heap_lang.lang]
n2:209 [binder, in intensional.heap_lang.lang]
n:109 [binder, in intensional.heap_lang.lang]
n:11 [binder, in intensional.heap_lang.lifting]
n:113 [binder, in intensional.heap_lang.lang]
n:117 [binder, in intensional.heap_lang.lang]
n:121 [binder, in intensional.heap_lang.lang]
N:126 [binder, in intensional.examples.linearizability]
n:2 [binder, in intensional.heap_lang.lifting]
N:213 [binder, in intensional.heap_lang.lifting]
N:219 [binder, in intensional.heap_lang.lifting]
N:23 [binder, in intensional.heap_lang.adequacy]
n:233 [binder, in intensional.heap_lang.lifting]
n:238 [binder, in intensional.heap_lang.lifting]
N:239 [binder, in intensional.examples.linearizability]
n:245 [binder, in intensional.heap_lang.lifting]
n:247 [binder, in intensional.heap_lang.lang]
n:25 [binder, in intensional.examples.file]
n:251 [binder, in intensional.heap_lang.lifting]
n:29 [binder, in intensional.heap_lang.proofmode]
n:29 [binder, in intensional.examples.file]
n:3 [binder, in intensional.heap_lang.lang]
n:308 [binder, in intensional.heap_lang.lang]
n:32 [binder, in intensional.examples.file]
n:34 [binder, in intensional.examples.file]
n:365 [binder, in intensional.heap_lang.lang]
n:37 [binder, in intensional.examples.file]
N:39 [binder, in intensional.heap_lang.adequacy]
n:39 [binder, in intensional.examples.file]
N:40 [binder, in intensional.examples.stack]
n:40 [binder, in intensional.heap_lang.proofmode]
N:46 [binder, in intensional.heap_lang.lifting]
N:48 [binder, in intensional.examples.well_bracketed]
n:49 [binder, in intensional.heap_lang.array]
n:54 [binder, in intensional.heap_lang.array]
N:54 [binder, in intensional.examples.file]
N:55 [binder, in intensional.examples.stack]
n:60 [binder, in intensional.heap_lang.array]
N:64 [binder, in intensional.examples.traversable_stack]
N:65 [binder, in intensional.examples.iterator]
n:66 [binder, in intensional.heap_lang.array]
N:66 [binder, in intensional.examples.file]
N:67 [binder, in intensional.examples.well_bracketed]
n:7 [binder, in intensional.heap_lang.lifting]
n:72 [binder, in intensional.heap_lang.array]
n:74 [binder, in intensional.heap_lang.lifting]
n:75 [binder, in intensional.examples.iterator]
N:80 [binder, in intensional.examples.traversable_stack]
n:82 [binder, in intensional.examples.iterator]
N:85 [binder, in intensional.heap_lang.lifting]
n:89 [binder, in intensional.heap_lang.lifting]
N:89 [binder, in intensional.examples.iterator]

O

off:101 [binder, in intensional.heap_lang.array]
off:106 [binder, in intensional.heap_lang.array]
off:112 [binder, in intensional.heap_lang.array]
off:119 [binder, in intensional.heap_lang.array]
off:126 [binder, in intensional.heap_lang.array]
off:132 [binder, in intensional.heap_lang.array]
off:140 [binder, in intensional.heap_lang.array]
off:149 [binder, in intensional.heap_lang.array]
off:157 [binder, in intensional.heap_lang.array]
off:165 [binder, in intensional.heap_lang.array]
off:174 [binder, in intensional.heap_lang.array]
off:184 [binder, in intensional.heap_lang.array]
off:193 [binder, in intensional.heap_lang.array]
off:200 [binder, in intensional.heap_lang.array]
off:207 [binder, in intensional.heap_lang.array]
off:215 [binder, in intensional.heap_lang.array]
off:223 [binder, in intensional.heap_lang.array]
off:42 [binder, in intensional.heap_lang.array]
off:79 [binder, in intensional.heap_lang.array]
off:8 [binder, in intensional.heap_lang.locations]
off:86 [binder, in intensional.heap_lang.array]
off:94 [binder, in intensional.heap_lang.array]
open_impl:57 [binder, in intensional.examples.file]
open_spec [definition, in intensional.examples.file]
open:5 [binder, in intensional.examples.file]
op_impl:132 [binder, in intensional.examples.linearizability]
op_spec [definition, in intensional.examples.linearizability]
op_impl:52 [binder, in intensional.examples.well_bracketed]
op_trace_call [constructor, in intensional.examples.well_bracketed]
op_trace_nil [constructor, in intensional.examples.well_bracketed]
op_trace [inductive, in intensional.examples.well_bracketed]
op_spec [definition, in intensional.examples.well_bracketed]
op:111 [binder, in intensional.heap_lang.lang]
op:115 [binder, in intensional.heap_lang.lang]
op:118 [binder, in intensional.heap_lang.lifting]
op:119 [binder, in intensional.heap_lang.lang]
op:121 [binder, in intensional.heap_lang.lifting]
op:123 [binder, in intensional.heap_lang.lang]
op:15 [binder, in intensional.examples.well_bracketed]
op:161 [binder, in intensional.heap_lang.lang]
op:162 [binder, in intensional.heap_lang.lang]
op:164 [binder, in intensional.heap_lang.lang]
op:184 [binder, in intensional.heap_lang.lifting]
op:187 [binder, in intensional.heap_lang.lifting]
op:203 [binder, in intensional.heap_lang.lang]
op:207 [binder, in intensional.heap_lang.lang]
op:211 [binder, in intensional.heap_lang.lang]
op:215 [binder, in intensional.heap_lang.lang]
op:220 [binder, in intensional.heap_lang.lang]
op:23 [binder, in intensional.examples.linearizability]
op:23 [binder, in intensional.heap_lang.lang]
op:25 [binder, in intensional.heap_lang.lang]
op:277 [binder, in intensional.heap_lang.lang]
op:281 [binder, in intensional.heap_lang.lang]

P

pair_atomic [instance, in intensional.heap_lang.lifting]
per_tag_linearized_add_ret [lemma, in intensional.examples.linearizability]
per_tag_linearized_add_lin [lemma, in intensional.examples.linearizability]
per_tag_linearized_add_call [lemma, in intensional.examples.linearizability]
per_tag_linearized_prefix [lemma, in intensional.examples.linearizability]
per_tag_linearized [definition, in intensional.examples.linearizability]
Pinit_impl:130 [binder, in intensional.examples.linearizability]
pop_impl:67 [binder, in intensional.examples.traversable_stack]
pop_spec [definition, in intensional.examples.traversable_stack]
pop_impl:43 [binder, in intensional.examples.stack]
pop_spec [definition, in intensional.examples.stack]
pop:17 [binder, in intensional.examples.traversable_stack]
pop:17 [binder, in intensional.examples.stack]
prim_step_to_val_is_head_step [lemma, in intensional.heap_lang.lang]
proofmode [library]
pure_case_inr [instance, in intensional.heap_lang.lifting]
pure_case_inl [instance, in intensional.heap_lang.lifting]
pure_snd [instance, in intensional.heap_lang.lifting]
pure_fst [instance, in intensional.heap_lang.lifting]
pure_if_false [instance, in intensional.heap_lang.lifting]
pure_if_true [instance, in intensional.heap_lang.lifting]
pure_eqop [instance, in intensional.heap_lang.lifting]
pure_binop [instance, in intensional.heap_lang.lifting]
pure_unop [instance, in intensional.heap_lang.lifting]
pure_beta [instance, in intensional.heap_lang.lifting]
pure_injrc [instance, in intensional.heap_lang.lifting]
pure_injlc [instance, in intensional.heap_lang.lifting]
pure_pairc [instance, in intensional.heap_lang.lifting]
pure_recc [instance, in intensional.heap_lang.lifting]
push_impl:66 [binder, in intensional.examples.traversable_stack]
push_spec [definition, in intensional.examples.traversable_stack]
push_impl:42 [binder, in intensional.examples.stack]
push_spec [definition, in intensional.examples.stack]
push:10 [binder, in intensional.examples.traversable_stack]
push:10 [binder, in intensional.examples.stack]
pvs':344 [binder, in intensional.heap_lang.lifting]
pvs':350 [binder, in intensional.heap_lang.lifting]
pvs':359 [binder, in intensional.heap_lang.lifting]
pvs':370 [binder, in intensional.heap_lang.lifting]
pvs:320 [binder, in intensional.heap_lang.lifting]
pvs:342 [binder, in intensional.heap_lang.lifting]
pvs:348 [binder, in intensional.heap_lang.lifting]
pvs:355 [binder, in intensional.heap_lang.lifting]
pvs:364 [binder, in intensional.heap_lang.lifting]
P_state [projection, in intensional.examples.linearizability]
P0:18 [binder, in intensional.examples.file]
P0:19 [binder, in intensional.examples.linearizability]
P0:20 [binder, in intensional.examples.well_bracketed]
P0:24 [binder, in intensional.examples.stack]
P0:241 [binder, in intensional.examples.linearizability]
P0:3 [binder, in intensional.examples.traversable_stack]
P0:3 [binder, in intensional.examples.stack]
P0:34 [binder, in intensional.examples.traversable_stack]
P0:40 [binder, in intensional.examples.iterator]
P0:42 [binder, in intensional.heap_lang.adequacy]
P0:48 [binder, in intensional.examples.linearizability]
P0:50 [binder, in intensional.examples.stack]
P0:56 [binder, in intensional.examples.stack]
P0:67 [binder, in intensional.examples.file]
P0:68 [binder, in intensional.examples.well_bracketed]
P0:73 [binder, in intensional.examples.traversable_stack]
P0:81 [binder, in intensional.examples.traversable_stack]
P0:90 [binder, in intensional.examples.iterator]
P:13 [binder, in intensional.examples.stdpp_extra]
p:25 [binder, in intensional.examples.stack_impl]
P:250 [binder, in intensional.examples.linearizability]
p:30 [binder, in intensional.examples.traversable_stack]
p:321 [binder, in intensional.heap_lang.lifting]
p:324 [binder, in intensional.heap_lang.lifting]
p:330 [binder, in intensional.heap_lang.lang]
p:331 [binder, in intensional.heap_lang.lang]
p:340 [binder, in intensional.heap_lang.lifting]
p:347 [binder, in intensional.heap_lang.lifting]
p:354 [binder, in intensional.heap_lang.lifting]
p:363 [binder, in intensional.heap_lang.lifting]
p:369 [binder, in intensional.heap_lang.lang]
P:53 [binder, in intensional.heap_lang.adequacy]
p:6 [binder, in intensional.heap_lang.locations]
P:6 [binder, in intensional.examples.well_bracketed]
P:64 [binder, in intensional.examples.stack]
p:7 [binder, in intensional.heap_lang.lang]
P:7 [binder, in intensional.examples.stdpp_extra]
p:74 [binder, in intensional.examples.traversable_stack]
p:75 [binder, in intensional.examples.traversable_stack]
P:75 [binder, in intensional.examples.file]
P:76 [binder, in intensional.examples.well_bracketed]
P:89 [binder, in intensional.examples.traversable_stack]
P:98 [binder, in intensional.examples.iterator]

Q

q:104 [binder, in intensional.heap_lang.proofmode]
q:11 [binder, in intensional.heap_lang.array]
q:113 [binder, in intensional.heap_lang.proofmode]
q:15 [binder, in intensional.heap_lang.array]
q:163 [binder, in intensional.heap_lang.proofmode]
q:164 [binder, in intensional.heap_lang.array]
q:17 [binder, in intensional.heap_lang.array]
q:173 [binder, in intensional.heap_lang.array]
q:174 [binder, in intensional.heap_lang.proofmode]
q:182 [binder, in intensional.heap_lang.array]
q:19 [binder, in intensional.heap_lang.array]
q:191 [binder, in intensional.heap_lang.array]
q:21 [binder, in intensional.heap_lang.array]
q:23 [binder, in intensional.heap_lang.array]
q:26 [binder, in intensional.heap_lang.array]
q:265 [binder, in intensional.heap_lang.lifting]
q:270 [binder, in intensional.heap_lang.lifting]
q:285 [binder, in intensional.heap_lang.lifting]
q:292 [binder, in intensional.heap_lang.lifting]
q:30 [binder, in intensional.heap_lang.array]
q:34 [binder, in intensional.heap_lang.array]
q:365 [binder, in intensional.heap_lang.lifting]
Q:38 [binder, in intensional.heap_lang.array]
q:4 [binder, in intensional.heap_lang.array]
q:40 [binder, in intensional.heap_lang.array]
q:47 [binder, in intensional.heap_lang.array]
Q:7 [binder, in intensional.examples.well_bracketed]
q:78 [binder, in intensional.heap_lang.array]
q:85 [binder, in intensional.heap_lang.array]
q:92 [binder, in intensional.heap_lang.array]
q:99 [binder, in intensional.heap_lang.array]

R

r [projection, in intensional.examples.linearizability]
read_impl:59 [binder, in intensional.examples.file]
read_spec [definition, in intensional.examples.file]
read:14 [binder, in intensional.examples.file]
rec_atomic [instance, in intensional.heap_lang.lifting]
remove_impl:70 [binder, in intensional.examples.iterator]
remove_spec [definition, in intensional.examples.iterator]
remove:20 [binder, in intensional.examples.iterator]
repr [record, in intensional.examples.linearizability]
ResolveProph [abbreviation, in intensional.heap_lang.notation]
resolve_reducible [lemma, in intensional.heap_lang.lifting]
resolve_atomic [instance, in intensional.heap_lang.lifting]
R_impl:129 [binder, in intensional.examples.linearizability]
r:16 [binder, in intensional.heap_lang.locations]
R:17 [binder, in intensional.examples.linearizability]
r:21 [binder, in intensional.heap_lang.locations]
r:22 [binder, in intensional.examples.linearizability]
r:24 [binder, in intensional.heap_lang.locations]
r:30 [binder, in intensional.examples.iterator]
r:343 [binder, in intensional.heap_lang.lifting]
R:37 [binder, in intensional.heap_lang.array]
R:50 [binder, in intensional.examples.linearizability]
r:79 [binder, in intensional.examples.iterator]

S

S [projection, in intensional.examples.linearizability]
Seq [abbreviation, in intensional.heap_lang.notation]
SeqCtx [abbreviation, in intensional.heap_lang.notation]
size_impl:68 [binder, in intensional.examples.iterator]
size_spec [definition, in intensional.examples.iterator]
size:5 [binder, in intensional.examples.iterator]
Skip [abbreviation, in intensional.heap_lang.notation]
snd_atomic [instance, in intensional.heap_lang.lifting]
SOME [abbreviation, in intensional.heap_lang.notation]
SOMEV [abbreviation, in intensional.heap_lang.notation]
Specs [section, in intensional.examples.linearizability]
stack [library]
stacklibN [definition, in intensional.examples.traversable_stack]
stacklibN [definition, in intensional.examples.stack]
stacklib_spec [definition, in intensional.examples.traversable_stack]
stacklib_spec [definition, in intensional.examples.stack]
stack_impl:65 [binder, in intensional.examples.traversable_stack]
stack_impl:41 [binder, in intensional.examples.stack]
Stack_impl.traversable_correct [lemma, in intensional.examples.stack_impl]
Stack_impl.correct [lemma, in intensional.examples.stack_impl]
Stack_impl.foreach_correct [lemma, in intensional.examples.stack_impl]
Stack_impl.pop_correct [lemma, in intensional.examples.stack_impl]
Stack_impl.push_correct [lemma, in intensional.examples.stack_impl]
Stack_impl.create_correct [lemma, in intensional.examples.stack_impl]
Stack_impl.stack_val [definition, in intensional.examples.stack_impl]
Stack_impl.list_val [definition, in intensional.examples.stack_impl]
Stack_impl.foreach [definition, in intensional.examples.stack_impl]
Stack_impl.pop [definition, in intensional.examples.stack_impl]
Stack_impl.push [definition, in intensional.examples.stack_impl]
Stack_impl.create [definition, in intensional.examples.stack_impl]
Stack_impl.S [section, in intensional.examples.stack_impl]
Stack_impl [module, in intensional.examples.stack_impl]
stack_impl [library]
Stack:16 [binder, in intensional.examples.traversable_stack]
Stack:16 [binder, in intensional.examples.stack]
Stack:24 [binder, in intensional.examples.traversable_stack]
Stack:26 [binder, in intensional.examples.stack]
Stack:36 [binder, in intensional.examples.traversable_stack]
Stack:4 [binder, in intensional.examples.traversable_stack]
Stack:4 [binder, in intensional.examples.stack]
Stack:9 [binder, in intensional.examples.traversable_stack]
Stack:9 [binder, in intensional.examples.stack]
stdpp_extra [library]
step_resolve [lemma, in intensional.heap_lang.lifting]
store_atomic [instance, in intensional.heap_lang.lifting]
subG_tracePreG [instance, in intensional.heap_lang.lifting]
subG_heapPreG [instance, in intensional.heap_lang.adequacy]
sz:100 [binder, in intensional.heap_lang.array]
sz:118 [binder, in intensional.heap_lang.array]
sz:125 [binder, in intensional.heap_lang.array]
sz:148 [binder, in intensional.heap_lang.array]
sz:156 [binder, in intensional.heap_lang.array]
sz:183 [binder, in intensional.heap_lang.array]
sz:192 [binder, in intensional.heap_lang.array]
sz:214 [binder, in intensional.heap_lang.array]
sz:222 [binder, in intensional.heap_lang.array]
sz:93 [binder, in intensional.heap_lang.array]
s_init [projection, in intensional.examples.linearizability]
s':190 [binder, in intensional.examples.linearizability]
s':210 [binder, in intensional.examples.linearizability]
s':223 [binder, in intensional.examples.linearizability]
s':28 [binder, in intensional.examples.linearizability]
s':33 [binder, in intensional.examples.linearizability]
s':35 [binder, in intensional.examples.linearizability]
s':39 [binder, in intensional.examples.linearizability]
s':41 [binder, in intensional.examples.linearizability]
s':71 [binder, in intensional.examples.linearizability]
s':87 [binder, in intensional.examples.linearizability]
s0:69 [binder, in intensional.examples.linearizability]
s:10 [binder, in intensional.heap_lang.adequacy]
s:101 [binder, in intensional.heap_lang.lifting]
s:103 [binder, in intensional.heap_lang.array]
s:105 [binder, in intensional.heap_lang.lifting]
s:108 [binder, in intensional.heap_lang.lifting]
s:108 [binder, in intensional.heap_lang.proofmode]
s:109 [binder, in intensional.heap_lang.array]
s:110 [binder, in intensional.heap_lang.lifting]
s:112 [binder, in intensional.heap_lang.lifting]
s:115 [binder, in intensional.heap_lang.array]
s:117 [binder, in intensional.heap_lang.lifting]
s:118 [binder, in intensional.heap_lang.proofmode]
s:12 [binder, in intensional.examples.traversable_stack]
s:12 [binder, in intensional.examples.stack]
s:120 [binder, in intensional.heap_lang.lifting]
s:122 [binder, in intensional.heap_lang.array]
s:124 [binder, in intensional.heap_lang.lifting]
s:127 [binder, in intensional.heap_lang.lifting]
s:127 [binder, in intensional.heap_lang.proofmode]
s:129 [binder, in intensional.heap_lang.array]
s:13 [binder, in intensional.heap_lang.proofmode]
s:13 [binder, in intensional.examples.stack_impl]
s:130 [binder, in intensional.heap_lang.lifting]
s:132 [binder, in intensional.heap_lang.lifting]
s:134 [binder, in intensional.heap_lang.lifting]
s:136 [binder, in intensional.heap_lang.lifting]
s:137 [binder, in intensional.heap_lang.array]
s:137 [binder, in intensional.heap_lang.proofmode]
s:139 [binder, in intensional.heap_lang.lifting]
s:14 [binder, in intensional.examples.stack_impl]
s:141 [binder, in intensional.heap_lang.lifting]
s:144 [binder, in intensional.heap_lang.lifting]
s:145 [binder, in intensional.heap_lang.array]
s:147 [binder, in intensional.heap_lang.proofmode]
s:148 [binder, in intensional.heap_lang.lifting]
s:151 [binder, in intensional.heap_lang.lifting]
s:153 [binder, in intensional.heap_lang.lifting]
s:153 [binder, in intensional.heap_lang.array]
s:155 [binder, in intensional.heap_lang.lifting]
s:156 [binder, in intensional.heap_lang.lifting]
s:158 [binder, in intensional.heap_lang.proofmode]
s:161 [binder, in intensional.heap_lang.array]
s:163 [binder, in intensional.examples.linearizability]
s:169 [binder, in intensional.heap_lang.proofmode]
s:17 [binder, in intensional.examples.stack_impl]
s:170 [binder, in intensional.heap_lang.array]
s:171 [binder, in intensional.examples.linearizability]
s:173 [binder, in intensional.examples.linearizability]
s:179 [binder, in intensional.heap_lang.array]
s:181 [binder, in intensional.heap_lang.proofmode]
s:184 [binder, in intensional.examples.linearizability]
s:188 [binder, in intensional.heap_lang.array]
s:189 [binder, in intensional.examples.linearizability]
s:19 [binder, in intensional.examples.traversable_stack]
s:19 [binder, in intensional.examples.stack]
s:191 [binder, in intensional.examples.linearizability]
s:191 [binder, in intensional.heap_lang.proofmode]
s:192 [binder, in intensional.examples.linearizability]
s:197 [binder, in intensional.examples.linearizability]
s:197 [binder, in intensional.heap_lang.array]
s:202 [binder, in intensional.heap_lang.proofmode]
s:204 [binder, in intensional.heap_lang.array]
s:209 [binder, in intensional.heap_lang.lifting]
s:209 [binder, in intensional.examples.linearizability]
s:21 [binder, in intensional.examples.stack_impl]
s:211 [binder, in intensional.heap_lang.array]
s:211 [binder, in intensional.heap_lang.proofmode]
s:215 [binder, in intensional.heap_lang.lifting]
s:219 [binder, in intensional.heap_lang.array]
s:222 [binder, in intensional.examples.linearizability]
s:223 [binder, in intensional.heap_lang.lifting]
s:227 [binder, in intensional.heap_lang.lifting]
s:23 [binder, in intensional.heap_lang.proofmode]
s:242 [binder, in intensional.heap_lang.lifting]
s:248 [binder, in intensional.heap_lang.lifting]
s:25 [binder, in intensional.heap_lang.adequacy]
s:254 [binder, in intensional.heap_lang.lifting]
s:258 [binder, in intensional.heap_lang.lifting]
s:262 [binder, in intensional.heap_lang.lifting]
s:267 [binder, in intensional.heap_lang.lifting]
s:27 [binder, in intensional.examples.linearizability]
s:27 [binder, in intensional.examples.traversable_stack]
s:272 [binder, in intensional.heap_lang.lifting]
s:277 [binder, in intensional.heap_lang.lifting]
s:282 [binder, in intensional.heap_lang.lifting]
s:289 [binder, in intensional.heap_lang.lifting]
s:296 [binder, in intensional.heap_lang.lifting]
s:30 [binder, in intensional.examples.linearizability]
s:302 [binder, in intensional.heap_lang.lifting]
s:308 [binder, in intensional.heap_lang.lifting]
s:31 [binder, in intensional.examples.linearizability]
s:313 [binder, in intensional.heap_lang.lifting]
s:318 [binder, in intensional.heap_lang.lifting]
s:32 [binder, in intensional.examples.linearizability]
s:336 [binder, in intensional.heap_lang.lifting]
s:34 [binder, in intensional.heap_lang.proofmode]
s:345 [binder, in intensional.heap_lang.lifting]
s:351 [binder, in intensional.heap_lang.lifting]
s:360 [binder, in intensional.heap_lang.lifting]
s:37 [binder, in intensional.examples.linearizability]
s:38 [binder, in intensional.examples.linearizability]
s:4 [binder, in intensional.heap_lang.proofmode]
s:43 [binder, in intensional.examples.linearizability]
s:45 [binder, in intensional.heap_lang.proofmode]
s:51 [binder, in intensional.heap_lang.array]
s:52 [binder, in intensional.heap_lang.proofmode]
s:57 [binder, in intensional.heap_lang.array]
s:6 [binder, in intensional.heap_lang.lang]
s:6 [binder, in intensional.examples.traversable_stack]
s:6 [binder, in intensional.examples.stack]
s:60 [binder, in intensional.heap_lang.proofmode]
s:63 [binder, in intensional.heap_lang.array]
s:68 [binder, in intensional.examples.linearizability]
s:69 [binder, in intensional.heap_lang.array]
s:70 [binder, in intensional.examples.linearizability]
s:71 [binder, in intensional.examples.traversable_stack]
s:71 [binder, in intensional.heap_lang.proofmode]
s:75 [binder, in intensional.heap_lang.array]
s:82 [binder, in intensional.heap_lang.array]
s:82 [binder, in intensional.heap_lang.proofmode]
s:89 [binder, in intensional.heap_lang.array]
s:90 [binder, in intensional.heap_lang.proofmode]
s:96 [binder, in intensional.heap_lang.array]
s:99 [binder, in intensional.heap_lang.proofmode]

T

tactics [library]
tactics [library]
tac_twp_faa [lemma, in intensional.heap_lang.proofmode]
tac_wp_faa [lemma, in intensional.heap_lang.proofmode]
tac_twp_cmpxchg_suc [lemma, in intensional.heap_lang.proofmode]
tac_wp_cmpxchg_suc [lemma, in intensional.heap_lang.proofmode]
tac_twp_cmpxchg_fail [lemma, in intensional.heap_lang.proofmode]
tac_wp_cmpxchg_fail [lemma, in intensional.heap_lang.proofmode]
tac_twp_cmpxchg [lemma, in intensional.heap_lang.proofmode]
tac_wp_cmpxchg [lemma, in intensional.heap_lang.proofmode]
tac_twp_store [lemma, in intensional.heap_lang.proofmode]
tac_wp_store [lemma, in intensional.heap_lang.proofmode]
tac_twp_load [lemma, in intensional.heap_lang.proofmode]
tac_wp_load [lemma, in intensional.heap_lang.proofmode]
tac_twp_alloc [lemma, in intensional.heap_lang.proofmode]
tac_wp_alloc [lemma, in intensional.heap_lang.proofmode]
tac_twp_bind [lemma, in intensional.heap_lang.proofmode]
tac_wp_bind [lemma, in intensional.heap_lang.proofmode]
tac_twp_value [lemma, in intensional.heap_lang.proofmode]
tac_wp_value [lemma, in intensional.heap_lang.proofmode]
tac_twp_pure [lemma, in intensional.heap_lang.proofmode]
tac_wp_pure [lemma, in intensional.heap_lang.proofmode]
tac_twp_expr_eval [lemma, in intensional.heap_lang.proofmode]
tac_wp_expr_eval [lemma, in intensional.heap_lang.proofmode]
tagst:138 [binder, in intensional.examples.linearizability]
tags_app [lemma, in intensional.examples.trace_helpers]
tag':11 [binder, in intensional.examples.trace_helpers]
tag':14 [binder, in intensional.examples.trace_helpers]
tag':17 [binder, in intensional.examples.trace_helpers]
tag:1 [binder, in intensional.examples.trace_helpers]
tag:10 [binder, in intensional.examples.trace_helpers]
tag:102 [binder, in intensional.examples.linearizability]
tag:13 [binder, in intensional.examples.trace_helpers]
tag:135 [binder, in intensional.examples.linearizability]
tag:145 [binder, in intensional.examples.linearizability]
tag:151 [binder, in intensional.examples.linearizability]
tag:156 [binder, in intensional.examples.linearizability]
tag:16 [binder, in intensional.examples.trace_helpers]
tag:199 [binder, in intensional.examples.linearizability]
tag:20 [binder, in intensional.examples.trace_helpers]
tag:201 [binder, in intensional.examples.linearizability]
tag:214 [binder, in intensional.examples.linearizability]
tag:221 [binder, in intensional.heap_lang.lifting]
tag:222 [binder, in intensional.heap_lang.lifting]
tag:226 [binder, in intensional.examples.linearizability]
tag:343 [binder, in intensional.heap_lang.lang]
tag:4 [binder, in intensional.examples.trace_helpers]
tag:54 [binder, in intensional.examples.linearizability]
tag:57 [binder, in intensional.examples.linearizability]
tag:61 [binder, in intensional.examples.linearizability]
tag:62 [binder, in intensional.examples.iterator]
tag:72 [binder, in intensional.examples.linearizability]
tag:77 [binder, in intensional.examples.linearizability]
tag:78 [binder, in intensional.examples.iterator]
tag:8 [binder, in intensional.examples.trace_helpers]
tag:92 [binder, in intensional.examples.linearizability]
tag:94 [binder, in intensional.examples.linearizability]
tag:97 [binder, in intensional.examples.linearizability]
to_val_fill_some [lemma, in intensional.heap_lang.lang]
Trace [section, in intensional.examples.linearizability]
Trace [section, in intensional.examples.traversable_stack]
trace [abbreviation, in intensional.examples.traversable_stack]
Trace [section, in intensional.examples.stack]
Trace [section, in intensional.examples.iterator]
Trace [section, in intensional.examples.well_bracketed]
Trace [section, in intensional.examples.file]
traceG [record, in intensional.heap_lang.lifting]
TraceG [constructor, in intensional.heap_lang.lifting]
traceO [definition, in intensional.heap_lang.lifting]
TracePreG [constructor, in intensional.heap_lang.lifting]
trace_auth_init [lemma, in intensional.heap_lang.lifting]
trace_is_inv [lemma, in intensional.heap_lang.lifting]
trace_add_event [lemma, in intensional.heap_lang.lifting]
trace_half_frag_agree [lemma, in intensional.heap_lang.lifting]
trace_agree [lemma, in intensional.heap_lang.lifting]
trace_auth_half_frag_agree [lemma, in intensional.heap_lang.lifting]
trace_inv [definition, in intensional.heap_lang.lifting]
trace_is [definition, in intensional.heap_lang.lifting]
trace_half_frag [definition, in intensional.heap_lang.lifting]
trace_auth [definition, in intensional.heap_lang.lifting]
trace_preG_inG [projection, in intensional.heap_lang.lifting]
trace_hist_preG_inG [projection, in intensional.heap_lang.lifting]
trace_preG [record, in intensional.heap_lang.lifting]
trace_name [projection, in intensional.heap_lang.lifting]
trace_inG [projection, in intensional.heap_lang.lifting]
trace_hist_name [projection, in intensional.heap_lang.lifting]
trace_hist_inG [projection, in intensional.heap_lang.lifting]
trace_helpers [library]
trace1 [definition, in intensional.examples.well_bracketed]
trace2 [definition, in intensional.examples.well_bracketed]
trace3 [definition, in intensional.examples.well_bracketed]
traceΣ [definition, in intensional.heap_lang.lifting]
traversable_stack [library]
traversal_trace_prefix [lemma, in intensional.examples.traversable_stack]
traversal_trace_app [lemma, in intensional.examples.traversable_stack]
traversal_trace [definition, in intensional.examples.traversable_stack]
tr:211 [binder, in intensional.heap_lang.lifting]
tr:217 [binder, in intensional.heap_lang.lifting]
ts:338 [binder, in intensional.heap_lang.lang]
twp_faa [lemma, in intensional.heap_lang.lifting]
twp_cmpxchg_suc [lemma, in intensional.heap_lang.lifting]
twp_cmpxchg_fail [lemma, in intensional.heap_lang.lifting]
twp_store [lemma, in intensional.heap_lang.lifting]
twp_load [lemma, in intensional.heap_lang.lifting]
twp_alloc [lemma, in intensional.heap_lang.lifting]
twp_allocN_seq [lemma, in intensional.heap_lang.lifting]
twp_fork [lemma, in intensional.heap_lang.lifting]
twp_faa_offset_vec [lemma, in intensional.heap_lang.array]
twp_faa_offset [lemma, in intensional.heap_lang.array]
twp_cmpxchg_fail_offset_vec [lemma, in intensional.heap_lang.array]
twp_cmpxchg_fail_offset [lemma, in intensional.heap_lang.array]
twp_cmpxchg_suc_offset_vec [lemma, in intensional.heap_lang.array]
twp_cmpxchg_suc_offset [lemma, in intensional.heap_lang.array]
twp_store_offset_vec [lemma, in intensional.heap_lang.array]
twp_store_offset [lemma, in intensional.heap_lang.array]
twp_load_offset_vec [lemma, in intensional.heap_lang.array]
twp_load_offset [lemma, in intensional.heap_lang.array]
twp_allocN_vec [lemma, in intensional.heap_lang.array]
twp_allocN [lemma, in intensional.heap_lang.array]
t_op:45 [binder, in intensional.examples.well_bracketed]
t_op:41 [binder, in intensional.examples.well_bracketed]
t_op:31 [binder, in intensional.examples.well_bracketed]
t':34 [binder, in intensional.examples.well_bracketed]
t':37 [binder, in intensional.examples.well_bracketed]
t':40 [binder, in intensional.examples.well_bracketed]
t':44 [binder, in intensional.examples.well_bracketed]
t':55 [binder, in intensional.examples.traversable_stack]
t':57 [binder, in intensional.examples.iterator]
t':58 [binder, in intensional.heap_lang.lifting]
t':62 [binder, in intensional.heap_lang.lifting]
t':66 [binder, in intensional.heap_lang.lifting]
t':86 [binder, in intensional.examples.linearizability]
t':90 [binder, in intensional.examples.linearizability]
t:101 [binder, in intensional.examples.linearizability]
t:133 [binder, in intensional.examples.linearizability]
t:143 [binder, in intensional.examples.linearizability]
t:149 [binder, in intensional.examples.linearizability]
t:158 [binder, in intensional.examples.linearizability]
t:23 [binder, in intensional.examples.trace_helpers]
t:23 [binder, in intensional.examples.file]
t:254 [binder, in intensional.heap_lang.lang]
t:27 [binder, in intensional.examples.well_bracketed]
t:28 [binder, in intensional.examples.stack]
t:28 [binder, in intensional.examples.file]
t:29 [binder, in intensional.heap_lang.adequacy]
t:30 [binder, in intensional.examples.well_bracketed]
t:31 [binder, in intensional.heap_lang.adequacy]
t:31 [binder, in intensional.examples.file]
t:32 [binder, in intensional.examples.stack]
t:32 [binder, in intensional.heap_lang.adequacy]
t:33 [binder, in intensional.heap_lang.lifting]
t:33 [binder, in intensional.examples.well_bracketed]
t:33 [binder, in intensional.examples.file]
t:34 [binder, in intensional.examples.stack]
t:35 [binder, in intensional.examples.stack]
t:35 [binder, in intensional.examples.well_bracketed]
t:36 [binder, in intensional.heap_lang.lifting]
t:36 [binder, in intensional.examples.file]
t:38 [binder, in intensional.examples.well_bracketed]
t:38 [binder, in intensional.examples.file]
t:39 [binder, in intensional.heap_lang.lifting]
t:41 [binder, in intensional.examples.file]
t:42 [binder, in intensional.heap_lang.lifting]
t:42 [binder, in intensional.examples.well_bracketed]
t:42 [binder, in intensional.examples.file]
t:45 [binder, in intensional.examples.traversable_stack]
t:45 [binder, in intensional.examples.file]
t:46 [binder, in intensional.examples.traversable_stack]
t:46 [binder, in intensional.examples.iterator]
t:46 [binder, in intensional.examples.file]
t:47 [binder, in intensional.examples.stack]
t:48 [binder, in intensional.heap_lang.lifting]
t:48 [binder, in intensional.examples.file]
t:49 [binder, in intensional.examples.traversable_stack]
t:49 [binder, in intensional.examples.file]
t:50 [binder, in intensional.examples.file]
t:51 [binder, in intensional.heap_lang.lifting]
t:51 [binder, in intensional.examples.traversable_stack]
t:51 [binder, in intensional.examples.iterator]
t:52 [binder, in intensional.examples.iterator]
t:53 [binder, in intensional.examples.traversable_stack]
t:53 [binder, in intensional.examples.iterator]
t:53 [binder, in intensional.examples.well_bracketed]
t:54 [binder, in intensional.heap_lang.lifting]
t:54 [binder, in intensional.examples.iterator]
t:55 [binder, in intensional.examples.well_bracketed]
t:56 [binder, in intensional.examples.linearizability]
t:56 [binder, in intensional.examples.iterator]
t:57 [binder, in intensional.heap_lang.lifting]
t:57 [binder, in intensional.examples.well_bracketed]
t:59 [binder, in intensional.examples.well_bracketed]
t:6 [binder, in intensional.examples.trace_helpers]
t:60 [binder, in intensional.examples.linearizability]
t:60 [binder, in intensional.examples.file]
t:61 [binder, in intensional.heap_lang.lifting]
t:61 [binder, in intensional.examples.file]
t:64 [binder, in intensional.examples.linearizability]
t:65 [binder, in intensional.heap_lang.lifting]
t:69 [binder, in intensional.heap_lang.lifting]
t:7 [binder, in intensional.examples.trace_helpers]
t:72 [binder, in intensional.examples.traversable_stack]
t:75 [binder, in intensional.heap_lang.lifting]
t:75 [binder, in intensional.examples.linearizability]
t:76 [binder, in intensional.examples.linearizability]
t:76 [binder, in intensional.examples.iterator]
t:79 [binder, in intensional.heap_lang.lifting]
t:8 [binder, in intensional.examples.stack_impl]
t:83 [binder, in intensional.examples.iterator]
t:84 [binder, in intensional.heap_lang.lifting]
t:85 [binder, in intensional.examples.linearizability]
t:89 [binder, in intensional.examples.linearizability]
t:91 [binder, in intensional.examples.linearizability]
t:92 [binder, in intensional.heap_lang.lifting]
t:93 [binder, in intensional.examples.linearizability]
t:96 [binder, in intensional.examples.linearizability]

U

unlocked_impl:50 [binder, in intensional.examples.well_bracketed]
unlocked:14 [binder, in intensional.examples.well_bracketed]
unlocked:23 [binder, in intensional.examples.well_bracketed]
unlocked:4 [binder, in intensional.examples.well_bracketed]
Unnamed_thm [definition, in intensional.examples.tactics]
Unnamed_thm [definition, in intensional.examples.tactics]
Unnamed_thm [definition, in intensional.examples.tactics]
Unnamed_thm [definition, in intensional.examples.tactics]
Unnamed_thm [definition, in intensional.examples.tactics]
unop_atomic [instance, in intensional.heap_lang.lifting]
update_array [lemma, in intensional.heap_lang.array]
u:24 [binder, in intensional.examples.trace_helpers]

V

vl:322 [binder, in intensional.heap_lang.lang]
vl:72 [binder, in intensional.heap_lang.lang]
vp:329 [binder, in intensional.heap_lang.lifting]
vs:102 [binder, in intensional.heap_lang.array]
vs:107 [binder, in intensional.heap_lang.array]
vs:113 [binder, in intensional.heap_lang.array]
vs:12 [binder, in intensional.heap_lang.array]
vs:120 [binder, in intensional.heap_lang.array]
vs:127 [binder, in intensional.heap_lang.array]
vs:133 [binder, in intensional.heap_lang.array]
vs:14 [binder, in intensional.heap_lang.array]
vs:141 [binder, in intensional.heap_lang.array]
vs:150 [binder, in intensional.heap_lang.array]
vs:158 [binder, in intensional.heap_lang.array]
vs:166 [binder, in intensional.heap_lang.array]
vs:175 [binder, in intensional.heap_lang.array]
vs:18 [binder, in intensional.heap_lang.array]
vs:185 [binder, in intensional.heap_lang.array]
vs:194 [binder, in intensional.heap_lang.array]
vs:201 [binder, in intensional.heap_lang.array]
vs:208 [binder, in intensional.heap_lang.array]
vs:216 [binder, in intensional.heap_lang.array]
vs:224 [binder, in intensional.heap_lang.array]
vs:232 [binder, in intensional.heap_lang.lifting]
vs:232 [binder, in intensional.heap_lang.lang]
vs:238 [binder, in intensional.heap_lang.lang]
vs:244 [binder, in intensional.heap_lang.lang]
vs:27 [binder, in intensional.heap_lang.array]
vs:32 [binder, in intensional.heap_lang.array]
vs:36 [binder, in intensional.heap_lang.array]
vs:41 [binder, in intensional.heap_lang.array]
vs:5 [binder, in intensional.heap_lang.array]
vs:80 [binder, in intensional.heap_lang.array]
vs:87 [binder, in intensional.heap_lang.array]
vs:95 [binder, in intensional.heap_lang.array]
vt:330 [binder, in intensional.heap_lang.lifting]
v':104 [binder, in intensional.examples.linearizability]
v':110 [binder, in intensional.examples.linearizability]
v':124 [binder, in intensional.heap_lang.proofmode]
v':133 [binder, in intensional.heap_lang.proofmode]
v':134 [binder, in intensional.heap_lang.array]
v':142 [binder, in intensional.examples.linearizability]
v':142 [binder, in intensional.heap_lang.array]
v':148 [binder, in intensional.examples.linearizability]
v':186 [binder, in intensional.heap_lang.lifting]
v':190 [binder, in intensional.heap_lang.lifting]
v':213 [binder, in intensional.examples.linearizability]
v':225 [binder, in intensional.examples.linearizability]
v':275 [binder, in intensional.heap_lang.lifting]
v':279 [binder, in intensional.heap_lang.lang]
v':280 [binder, in intensional.heap_lang.lifting]
v':284 [binder, in intensional.heap_lang.lang]
v':286 [binder, in intensional.heap_lang.lifting]
v':293 [binder, in intensional.heap_lang.lifting]
v':301 [binder, in intensional.heap_lang.lifting]
v':307 [binder, in intensional.heap_lang.lifting]
v':366 [binder, in intensional.heap_lang.lifting]
v':44 [binder, in intensional.heap_lang.array]
v':59 [binder, in intensional.examples.linearizability]
v':63 [binder, in intensional.examples.linearizability]
v':74 [binder, in intensional.examples.linearizability]
v':79 [binder, in intensional.examples.linearizability]
v':99 [binder, in intensional.examples.linearizability]
v0:145 [binder, in intensional.heap_lang.lifting]
v0:167 [binder, in intensional.heap_lang.array]
v0:176 [binder, in intensional.heap_lang.array]
v1:106 [binder, in intensional.heap_lang.lifting]
v1:115 [binder, in intensional.heap_lang.lifting]
v1:122 [binder, in intensional.heap_lang.lifting]
v1:125 [binder, in intensional.heap_lang.lifting]
v1:135 [binder, in intensional.heap_lang.array]
v1:142 [binder, in intensional.heap_lang.lifting]
v1:143 [binder, in intensional.heap_lang.array]
v1:143 [binder, in intensional.heap_lang.proofmode]
v1:146 [binder, in intensional.heap_lang.lifting]
v1:149 [binder, in intensional.heap_lang.lifting]
v1:151 [binder, in intensional.heap_lang.array]
v1:153 [binder, in intensional.heap_lang.proofmode]
v1:158 [binder, in intensional.heap_lang.lifting]
v1:159 [binder, in intensional.heap_lang.array]
v1:165 [binder, in intensional.heap_lang.proofmode]
v1:168 [binder, in intensional.heap_lang.array]
v1:174 [binder, in intensional.heap_lang.lifting]
v1:176 [binder, in intensional.heap_lang.lang]
v1:176 [binder, in intensional.heap_lang.proofmode]
v1:177 [binder, in intensional.heap_lang.array]
v1:181 [binder, in intensional.heap_lang.lifting]
v1:185 [binder, in intensional.heap_lang.lang]
v1:186 [binder, in intensional.heap_lang.array]
v1:187 [binder, in intensional.heap_lang.proofmode]
v1:188 [binder, in intensional.heap_lang.lifting]
v1:191 [binder, in intensional.heap_lang.lifting]
v1:195 [binder, in intensional.heap_lang.array]
v1:197 [binder, in intensional.heap_lang.lifting]
v1:197 [binder, in intensional.heap_lang.proofmode]
v1:199 [binder, in intensional.heap_lang.lifting]
v1:221 [binder, in intensional.heap_lang.lang]
v1:264 [binder, in intensional.heap_lang.lang]
v1:282 [binder, in intensional.heap_lang.lang]
v1:287 [binder, in intensional.heap_lang.lifting]
v1:292 [binder, in intensional.heap_lang.lang]
v1:294 [binder, in intensional.heap_lang.lifting]
v1:295 [binder, in intensional.heap_lang.lang]
v1:299 [binder, in intensional.heap_lang.lifting]
v1:305 [binder, in intensional.heap_lang.lifting]
v1:320 [binder, in intensional.heap_lang.lang]
v1:356 [binder, in intensional.heap_lang.lifting]
v1:367 [binder, in intensional.heap_lang.lifting]
v1:393 [binder, in intensional.heap_lang.lang]
v1:60 [binder, in intensional.heap_lang.lang]
v1:73 [binder, in intensional.heap_lang.lang]
v1:83 [binder, in intensional.heap_lang.lang]
v1:93 [binder, in intensional.heap_lang.lang]
v2:107 [binder, in intensional.heap_lang.lifting]
v2:116 [binder, in intensional.heap_lang.lifting]
v2:123 [binder, in intensional.heap_lang.lifting]
v2:129 [binder, in intensional.heap_lang.lifting]
v2:136 [binder, in intensional.heap_lang.array]
v2:143 [binder, in intensional.heap_lang.lifting]
v2:144 [binder, in intensional.heap_lang.array]
v2:144 [binder, in intensional.heap_lang.proofmode]
v2:147 [binder, in intensional.heap_lang.lifting]
v2:150 [binder, in intensional.heap_lang.lifting]
v2:152 [binder, in intensional.heap_lang.array]
v2:154 [binder, in intensional.heap_lang.proofmode]
v2:159 [binder, in intensional.heap_lang.lifting]
v2:159 [binder, in intensional.heap_lang.lang]
v2:160 [binder, in intensional.heap_lang.array]
v2:163 [binder, in intensional.heap_lang.lang]
v2:166 [binder, in intensional.heap_lang.proofmode]
v2:168 [binder, in intensional.heap_lang.lang]
v2:169 [binder, in intensional.heap_lang.array]
v2:172 [binder, in intensional.heap_lang.lang]
v2:174 [binder, in intensional.heap_lang.lang]
v2:175 [binder, in intensional.heap_lang.lifting]
v2:177 [binder, in intensional.heap_lang.lang]
v2:177 [binder, in intensional.heap_lang.proofmode]
v2:178 [binder, in intensional.heap_lang.array]
v2:179 [binder, in intensional.heap_lang.lang]
v2:182 [binder, in intensional.heap_lang.lifting]
v2:182 [binder, in intensional.heap_lang.lang]
v2:186 [binder, in intensional.heap_lang.lang]
v2:187 [binder, in intensional.heap_lang.array]
v2:188 [binder, in intensional.heap_lang.lang]
v2:188 [binder, in intensional.heap_lang.proofmode]
v2:189 [binder, in intensional.heap_lang.lifting]
v2:192 [binder, in intensional.heap_lang.lifting]
v2:196 [binder, in intensional.heap_lang.array]
v2:198 [binder, in intensional.heap_lang.lifting]
v2:198 [binder, in intensional.heap_lang.proofmode]
v2:200 [binder, in intensional.heap_lang.lifting]
v2:217 [binder, in intensional.heap_lang.lang]
v2:222 [binder, in intensional.heap_lang.lang]
v2:265 [binder, in intensional.heap_lang.lang]
v2:274 [binder, in intensional.heap_lang.lang]
v2:283 [binder, in intensional.heap_lang.lang]
v2:288 [binder, in intensional.heap_lang.lifting]
v2:293 [binder, in intensional.heap_lang.lang]
v2:295 [binder, in intensional.heap_lang.lifting]
v2:296 [binder, in intensional.heap_lang.lang]
v2:300 [binder, in intensional.heap_lang.lifting]
v2:306 [binder, in intensional.heap_lang.lifting]
v2:321 [binder, in intensional.heap_lang.lang]
v2:357 [binder, in intensional.heap_lang.lifting]
v2:368 [binder, in intensional.heap_lang.lifting]
v2:394 [binder, in intensional.heap_lang.lang]
v2:61 [binder, in intensional.heap_lang.lang]
v2:84 [binder, in intensional.heap_lang.lang]
v2:94 [binder, in intensional.heap_lang.lang]
v:10 [binder, in intensional.examples.stack_impl]
v:100 [binder, in intensional.heap_lang.lifting]
v:100 [binder, in intensional.examples.linearizability]
v:100 [binder, in intensional.examples.iterator]
v:103 [binder, in intensional.examples.linearizability]
v:105 [binder, in intensional.examples.linearizability]
v:105 [binder, in intensional.heap_lang.proofmode]
v:108 [binder, in intensional.examples.linearizability]
v:108 [binder, in intensional.heap_lang.array]
v:109 [binder, in intensional.heap_lang.lifting]
v:109 [binder, in intensional.examples.linearizability]
v:111 [binder, in intensional.heap_lang.lifting]
v:114 [binder, in intensional.heap_lang.array]
v:114 [binder, in intensional.heap_lang.proofmode]
v:119 [binder, in intensional.heap_lang.lifting]
v:12 [binder, in intensional.examples.trace_helpers]
v:121 [binder, in intensional.heap_lang.array]
v:123 [binder, in intensional.heap_lang.proofmode]
v:126 [binder, in intensional.heap_lang.lang]
v:128 [binder, in intensional.heap_lang.array]
v:131 [binder, in intensional.heap_lang.lifting]
v:132 [binder, in intensional.heap_lang.lang]
v:132 [binder, in intensional.heap_lang.proofmode]
v:133 [binder, in intensional.heap_lang.lifting]
v:137 [binder, in intensional.heap_lang.lifting]
v:138 [binder, in intensional.heap_lang.lang]
v:14 [binder, in intensional.heap_lang.adequacy]
v:140 [binder, in intensional.heap_lang.lifting]
v:141 [binder, in intensional.examples.linearizability]
v:142 [binder, in intensional.heap_lang.proofmode]
v:144 [binder, in intensional.heap_lang.lang]
v:147 [binder, in intensional.examples.linearizability]
v:15 [binder, in intensional.examples.trace_helpers]
v:15 [binder, in intensional.examples.file]
v:150 [binder, in intensional.heap_lang.lang]
v:152 [binder, in intensional.heap_lang.lifting]
v:152 [binder, in intensional.heap_lang.proofmode]
v:154 [binder, in intensional.heap_lang.lifting]
v:154 [binder, in intensional.heap_lang.lang]
v:16 [binder, in intensional.heap_lang.lang]
v:16 [binder, in intensional.heap_lang.adequacy]
v:160 [binder, in intensional.heap_lang.lifting]
v:161 [binder, in intensional.heap_lang.lifting]
v:162 [binder, in intensional.heap_lang.lifting]
v:164 [binder, in intensional.heap_lang.proofmode]
v:175 [binder, in intensional.heap_lang.proofmode]
v:176 [binder, in intensional.heap_lang.lifting]
v:177 [binder, in intensional.heap_lang.lifting]
v:18 [binder, in intensional.examples.trace_helpers]
v:185 [binder, in intensional.heap_lang.lifting]
v:186 [binder, in intensional.heap_lang.proofmode]
v:19 [binder, in intensional.examples.trace_helpers]
v:19 [binder, in intensional.examples.stack_impl]
v:196 [binder, in intensional.heap_lang.lang]
v:196 [binder, in intensional.heap_lang.proofmode]
v:2 [binder, in intensional.examples.trace_helpers]
v:20 [binder, in intensional.examples.traversable_stack]
v:20 [binder, in intensional.examples.stack]
v:200 [binder, in intensional.examples.linearizability]
v:201 [binder, in intensional.heap_lang.lifting]
v:201 [binder, in intensional.heap_lang.lang]
v:202 [binder, in intensional.examples.linearizability]
v:204 [binder, in intensional.heap_lang.lifting]
v:204 [binder, in intensional.heap_lang.lang]
v:21 [binder, in intensional.examples.trace_helpers]
v:212 [binder, in intensional.heap_lang.lifting]
v:212 [binder, in intensional.examples.linearizability]
v:216 [binder, in intensional.examples.linearizability]
v:217 [binder, in intensional.examples.linearizability]
v:218 [binder, in intensional.heap_lang.lifting]
v:22 [binder, in intensional.examples.trace_helpers]
v:224 [binder, in intensional.examples.linearizability]
v:227 [binder, in intensional.heap_lang.lang]
v:230 [binder, in intensional.examples.linearizability]
v:231 [binder, in intensional.examples.linearizability]
v:236 [binder, in intensional.heap_lang.lang]
v:237 [binder, in intensional.heap_lang.lifting]
v:24 [binder, in intensional.heap_lang.array]
v:240 [binder, in intensional.heap_lang.lifting]
v:244 [binder, in intensional.heap_lang.lifting]
v:248 [binder, in intensional.heap_lang.lang]
v:250 [binder, in intensional.heap_lang.lifting]
v:252 [binder, in intensional.heap_lang.lang]
v:253 [binder, in intensional.examples.linearizability]
v:256 [binder, in intensional.heap_lang.lifting]
v:260 [binder, in intensional.heap_lang.lifting]
v:266 [binder, in intensional.heap_lang.lifting]
v:267 [binder, in intensional.heap_lang.lang]
v:269 [binder, in intensional.heap_lang.lang]
v:27 [binder, in intensional.examples.file]
v:271 [binder, in intensional.heap_lang.lifting]
v:276 [binder, in intensional.heap_lang.lifting]
v:278 [binder, in intensional.heap_lang.lang]
v:281 [binder, in intensional.heap_lang.lifting]
v:298 [binder, in intensional.heap_lang.lang]
v:30 [binder, in intensional.examples.stack]
v:302 [binder, in intensional.heap_lang.lang]
v:309 [binder, in intensional.heap_lang.lang]
v:31 [binder, in intensional.heap_lang.array]
v:314 [binder, in intensional.heap_lang.lang]
v:317 [binder, in intensional.heap_lang.lang]
v:325 [binder, in intensional.heap_lang.lifting]
v:33 [binder, in intensional.examples.stack]
v:332 [binder, in intensional.heap_lang.lang]
v:339 [binder, in intensional.heap_lang.lang]
v:341 [binder, in intensional.heap_lang.lifting]
v:341 [binder, in intensional.heap_lang.lang]
v:349 [binder, in intensional.heap_lang.lifting]
v:35 [binder, in intensional.heap_lang.array]
v:358 [binder, in intensional.heap_lang.lifting]
v:36 [binder, in intensional.examples.stack]
v:364 [binder, in intensional.heap_lang.lang]
v:369 [binder, in intensional.heap_lang.lifting]
v:372 [binder, in intensional.heap_lang.lang]
v:4 [binder, in intensional.examples.stack_impl]
v:43 [binder, in intensional.heap_lang.array]
v:43 [binder, in intensional.examples.file]
v:46 [binder, in intensional.examples.stack]
v:47 [binder, in intensional.examples.file]
v:48 [binder, in intensional.heap_lang.array]
v:48 [binder, in intensional.heap_lang.proofmode]
v:5 [binder, in intensional.examples.trace_helpers]
v:51 [binder, in intensional.examples.file]
v:53 [binder, in intensional.heap_lang.array]
v:55 [binder, in intensional.examples.linearizability]
v:55 [binder, in intensional.heap_lang.proofmode]
v:55 [binder, in intensional.heap_lang.adequacy]
v:58 [binder, in intensional.examples.linearizability]
v:59 [binder, in intensional.heap_lang.array]
v:62 [binder, in intensional.examples.linearizability]
v:62 [binder, in intensional.heap_lang.lang]
v:63 [binder, in intensional.heap_lang.lang]
v:65 [binder, in intensional.heap_lang.array]
v:65 [binder, in intensional.heap_lang.proofmode]
v:66 [binder, in intensional.examples.stack]
v:68 [binder, in intensional.heap_lang.lang]
v:7 [binder, in intensional.heap_lang.array]
v:71 [binder, in intensional.heap_lang.array]
v:71 [binder, in intensional.heap_lang.lang]
v:73 [binder, in intensional.examples.linearizability]
v:76 [binder, in intensional.heap_lang.proofmode]
v:77 [binder, in intensional.examples.file]
v:78 [binder, in intensional.examples.linearizability]
v:78 [binder, in intensional.heap_lang.lang]
v:78 [binder, in intensional.examples.well_bracketed]
v:80 [binder, in intensional.examples.linearizability]
v:80 [binder, in intensional.heap_lang.lang]
v:81 [binder, in intensional.heap_lang.array]
v:82 [binder, in intensional.examples.linearizability]
v:86 [binder, in intensional.heap_lang.proofmode]
v:88 [binder, in intensional.heap_lang.array]
v:9 [binder, in intensional.examples.trace_helpers]
v:91 [binder, in intensional.examples.traversable_stack]
v:94 [binder, in intensional.heap_lang.proofmode]
v:95 [binder, in intensional.examples.linearizability]
v:98 [binder, in intensional.heap_lang.lifting]
v:98 [binder, in intensional.examples.linearizability]
v:99 [binder, in intensional.heap_lang.lifting]

W

well_bracketed [library]
withRes_impl:51 [binder, in intensional.examples.well_bracketed]
withRes_trace_call [constructor, in intensional.examples.well_bracketed]
withRes_trace_nil [constructor, in intensional.examples.well_bracketed]
withRes_trace [inductive, in intensional.examples.well_bracketed]
withRes_spec [definition, in intensional.examples.well_bracketed]
withRes:5 [binder, in intensional.examples.well_bracketed]
wp_resolve_cmpxchg_fail [lemma, in intensional.heap_lang.lifting]
wp_resolve_cmpxchg_suc [lemma, in intensional.heap_lang.lifting]
wp_resolve_proph [lemma, in intensional.heap_lang.lifting]
wp_resolve [lemma, in intensional.heap_lang.lifting]
wp_new_proph [lemma, in intensional.heap_lang.lifting]
wp_faa [lemma, in intensional.heap_lang.lifting]
wp_cmpxchg_suc [lemma, in intensional.heap_lang.lifting]
wp_cmpxchg_fail [lemma, in intensional.heap_lang.lifting]
wp_store [lemma, in intensional.heap_lang.lifting]
wp_load [lemma, in intensional.heap_lang.lifting]
wp_alloc [lemma, in intensional.heap_lang.lifting]
wp_allocN_seq [lemma, in intensional.heap_lang.lifting]
wp_fork [lemma, in intensional.heap_lang.lifting]
wp_fresh [lemma, in intensional.heap_lang.lifting]
wp_emit [lemma, in intensional.heap_lang.lifting]
wp_faa_offset_vec [lemma, in intensional.heap_lang.array]
wp_faa_offset [lemma, in intensional.heap_lang.array]
wp_cmpxchg_fail_offset_vec [lemma, in intensional.heap_lang.array]
wp_cmpxchg_fail_offset [lemma, in intensional.heap_lang.array]
wp_cmpxchg_suc_offset_vec [lemma, in intensional.heap_lang.array]
wp_cmpxchg_suc_offset [lemma, in intensional.heap_lang.array]
wp_store_offset_vec [lemma, in intensional.heap_lang.array]
wp_store_offset [lemma, in intensional.heap_lang.array]
wp_load_offset_vec [lemma, in intensional.heap_lang.array]
wp_load_offset [lemma, in intensional.heap_lang.array]
wp_allocN_vec [lemma, in intensional.heap_lang.array]
wp_allocN [lemma, in intensional.heap_lang.array]
Wrap [module, in intensional.examples.linearizability]
Wrap [module, in intensional.examples.traversable_stack]
Wrap [module, in intensional.examples.stack]
Wrap [module, in intensional.examples.iterator]
Wrap [module, in intensional.examples.well_bracketed]
Wrap [module, in intensional.examples.file]
wrapN [definition, in intensional.examples.linearizability]
wrap_lib_correct [lemma, in intensional.examples.linearizability]
wrap_stacklib_correct [lemma, in intensional.examples.traversable_stack]
wrap_stacklib_correct [lemma, in intensional.examples.stack]
wrap_iterlib_correct [lemma, in intensional.examples.iterator]
wrap_bfilelib_correct [lemma, in intensional.examples.well_bracketed]
wrap_filelib_correct [lemma, in intensional.examples.file]
Wrap.add [definition, in intensional.examples.iterator]
Wrap.add_correct [lemma, in intensional.examples.iterator]
Wrap.AfterCall [constructor, in intensional.examples.linearizability]
Wrap.AfterLin [constructor, in intensional.examples.linearizability]
Wrap.close [definition, in intensional.examples.file]
Wrap.close_correct [lemma, in intensional.examples.file]
Wrap.Coll [definition, in intensional.examples.iterator]
Wrap.correct [lemma, in intensional.examples.linearizability]
Wrap.correct [lemma, in intensional.examples.traversable_stack]
Wrap.correct [lemma, in intensional.examples.stack]
Wrap.correct [lemma, in intensional.examples.iterator]
Wrap.correct [lemma, in intensional.examples.well_bracketed]
Wrap.correct [lemma, in intensional.examples.file]
Wrap.create [definition, in intensional.examples.traversable_stack]
Wrap.create [definition, in intensional.examples.stack]
Wrap.create_correct [lemma, in intensional.examples.traversable_stack]
Wrap.create_correct [lemma, in intensional.examples.stack]
Wrap.Done [constructor, in intensional.examples.linearizability]
Wrap.foreach [definition, in intensional.examples.traversable_stack]
Wrap.foreach_correct [lemma, in intensional.examples.traversable_stack]
Wrap.init [definition, in intensional.examples.linearizability]
Wrap.init_correct [lemma, in intensional.examples.linearizability]
Wrap.isClosed [definition, in intensional.examples.file]
Wrap.isOpen [definition, in intensional.examples.file]
Wrap.is_P_wrap [definition, in intensional.examples.linearizability]
Wrap.Iter [definition, in intensional.examples.iterator]
Wrap.iterator [definition, in intensional.examples.iterator]
Wrap.iterator_correct [lemma, in intensional.examples.iterator]
Wrap.lib [definition, in intensional.examples.linearizability]
Wrap.lib [definition, in intensional.examples.traversable_stack]
Wrap.lib [definition, in intensional.examples.stack]
Wrap.lib [definition, in intensional.examples.iterator]
Wrap.lib [definition, in intensional.examples.well_bracketed]
Wrap.lib [definition, in intensional.examples.file]
Wrap.linG [record, in intensional.examples.linearizability]
Wrap.lin_tag_res_inG [projection, in intensional.examples.linearizability]
Wrap.lin_tag_state_inG [projection, in intensional.examples.linearizability]
Wrap.lin_gnames_inG [projection, in intensional.examples.linearizability]
Wrap.lin_model_inG [projection, in intensional.examples.linearizability]
Wrap.linΣ [definition, in intensional.examples.linearizability]
Wrap.locked [definition, in intensional.examples.well_bracketed]
Wrap.mainN [definition, in intensional.examples.linearizability]
Wrap.main_inv_state_eq [lemma, in intensional.examples.linearizability]
Wrap.main_inv_gnames_eq [lemma, in intensional.examples.linearizability]
Wrap.main_inv [definition, in intensional.examples.linearizability]
Wrap.next [definition, in intensional.examples.iterator]
Wrap.next_correct [lemma, in intensional.examples.iterator]
Wrap.op [definition, in intensional.examples.linearizability]
Wrap.op [definition, in intensional.examples.well_bracketed]
Wrap.open [definition, in intensional.examples.file]
Wrap.open_correct [lemma, in intensional.examples.file]
Wrap.op_correct [lemma, in intensional.examples.linearizability]
Wrap.op_correct_ret [lemma, in intensional.examples.linearizability]
Wrap.op_correct_lin [lemma, in intensional.examples.linearizability]
Wrap.op_correct_call [lemma, in intensional.examples.linearizability]
Wrap.op_correct [lemma, in intensional.examples.well_bracketed]
Wrap.Pinit [definition, in intensional.examples.linearizability]
Wrap.pop [definition, in intensional.examples.traversable_stack]
Wrap.pop [definition, in intensional.examples.stack]
Wrap.pop_correct [lemma, in intensional.examples.traversable_stack]
Wrap.pop_correct [lemma, in intensional.examples.stack]
Wrap.push [definition, in intensional.examples.traversable_stack]
Wrap.push [definition, in intensional.examples.stack]
Wrap.push_correct [lemma, in intensional.examples.traversable_stack]
Wrap.push_correct [lemma, in intensional.examples.stack]
Wrap.P_state_wrap [definition, in intensional.examples.linearizability]
Wrap.R [definition, in intensional.examples.linearizability]
Wrap.read [definition, in intensional.examples.file]
Wrap.read_correct [lemma, in intensional.examples.file]
Wrap.remove [definition, in intensional.examples.iterator]
Wrap.remove_correct [lemma, in intensional.examples.iterator]
Wrap.S [section, in intensional.examples.linearizability]
Wrap.S [section, in intensional.examples.traversable_stack]
Wrap.S [section, in intensional.examples.stack]
Wrap.S [section, in intensional.examples.iterator]
Wrap.S [section, in intensional.examples.well_bracketed]
Wrap.S [section, in intensional.examples.file]
Wrap.size [definition, in intensional.examples.iterator]
Wrap.size_correct [lemma, in intensional.examples.iterator]
Wrap.SO [abbreviation, in intensional.examples.linearizability]
Wrap.stack_val [definition, in intensional.examples.traversable_stack]
Wrap.stack_val [definition, in intensional.examples.stack]
Wrap.subG_linG [instance, in intensional.examples.linearizability]
Wrap.tags_state_lookup_sub [lemma, in intensional.examples.linearizability]
Wrap.tags_state_lin_to_ret [lemma, in intensional.examples.linearizability]
Wrap.tags_state_call_to_lin [lemma, in intensional.examples.linearizability]
Wrap.tags_state [definition, in intensional.examples.linearizability]
Wrap.tag_state [inductive, in intensional.examples.linearizability]
Wrap.traceN [definition, in intensional.examples.linearizability]
Wrap.T0 [definition, in intensional.examples.well_bracketed]
Wrap.T1 [definition, in intensional.examples.well_bracketed]
Wrap.T2 [definition, in intensional.examples.well_bracketed]
Wrap.T3 [definition, in intensional.examples.well_bracketed]
Wrap.unlocked [definition, in intensional.examples.well_bracketed]
Wrap.withRes [definition, in intensional.examples.well_bracketed]
Wrap.withRes_correct [lemma, in intensional.examples.well_bracketed]
ws:28 [binder, in intensional.heap_lang.array]
w:138 [binder, in intensional.heap_lang.lifting]
w:239 [binder, in intensional.heap_lang.lang]
w:326 [binder, in intensional.heap_lang.lifting]
w:327 [binder, in intensional.heap_lang.lifting]
w:335 [binder, in intensional.heap_lang.lang]
w:373 [binder, in intensional.heap_lang.lang]
w:374 [binder, in intensional.heap_lang.lang]
w:378 [binder, in intensional.heap_lang.lang]

X

x:10 [binder, in intensional.examples.well_bracketed]
x:103 [binder, in intensional.heap_lang.lifting]
x:11 [binder, in intensional.examples.tactics]
x:11 [binder, in intensional.examples.iris_extra]
x:11 [binder, in intensional.examples.stdpp_extra]
x:114 [binder, in intensional.heap_lang.lifting]
x:12 [binder, in intensional.examples.linearizability]
x:13 [binder, in intensional.examples.traversable_stack]
x:13 [binder, in intensional.examples.stack]
x:14 [binder, in intensional.examples.iterator]
x:14 [binder, in intensional.examples.stdpp_extra]
x:15 [binder, in intensional.examples.tactics]
x:15 [binder, in intensional.examples.stack_impl]
x:16 [binder, in intensional.examples.well_bracketed]
x:164 [binder, in intensional.heap_lang.lifting]
x:167 [binder, in intensional.examples.linearizability]
x:169 [binder, in intensional.heap_lang.lifting]
x:17 [binder, in intensional.examples.iris_extra]
x:17 [binder, in intensional.heap_lang.lang]
x:172 [binder, in intensional.heap_lang.lifting]
x:179 [binder, in intensional.heap_lang.lifting]
x:19 [binder, in intensional.heap_lang.lang]
x:195 [binder, in intensional.heap_lang.lang]
x:21 [binder, in intensional.examples.tactics]
x:22 [binder, in intensional.examples.iterator]
x:25 [binder, in intensional.examples.linearizability]
x:26 [binder, in intensional.examples.stack_impl]
x:261 [binder, in intensional.heap_lang.lang]
x:272 [binder, in intensional.heap_lang.lang]
x:3 [binder, in intensional.examples.stdpp_extra]
x:31 [binder, in intensional.examples.tactics]
x:31 [binder, in intensional.examples.traversable_stack]
x:37 [binder, in intensional.examples.iterator]
x:40 [binder, in intensional.examples.traversable_stack]
x:43 [binder, in intensional.examples.traversable_stack]
x:47 [binder, in intensional.examples.traversable_stack]
x:48 [binder, in intensional.examples.stack]
x:5 [binder, in intensional.examples.iris_extra]
x:55 [binder, in intensional.examples.iterator]
x:58 [binder, in intensional.heap_lang.lang]
x:60 [binder, in intensional.examples.iterator]
x:60 [binder, in intensional.examples.well_bracketed]
x:7 [binder, in intensional.examples.iterator]
x:73 [binder, in intensional.examples.iterator]
x:8 [binder, in intensional.examples.stdpp_extra]
x:80 [binder, in intensional.examples.iterator]

Y

y':29 [binder, in intensional.examples.linearizability]
y':34 [binder, in intensional.examples.linearizability]
y':36 [binder, in intensional.examples.linearizability]
y':40 [binder, in intensional.examples.linearizability]
y':42 [binder, in intensional.examples.linearizability]
y:12 [binder, in intensional.examples.iris_extra]
y:17 [binder, in intensional.examples.well_bracketed]
y:22 [binder, in intensional.examples.tactics]
y:26 [binder, in intensional.examples.linearizability]
y:32 [binder, in intensional.examples.tactics]
y:4 [binder, in intensional.examples.stdpp_extra]
y:6 [binder, in intensional.examples.iris_extra]
y:61 [binder, in intensional.examples.well_bracketed]
y:74 [binder, in intensional.examples.iterator]
y:81 [binder, in intensional.examples.iterator]
y:9 [binder, in intensional.examples.well_bracketed]

Z

z1:207 [binder, in intensional.heap_lang.proofmode]
z1:216 [binder, in intensional.heap_lang.proofmode]
z2:208 [binder, in intensional.heap_lang.proofmode]
z2:217 [binder, in intensional.heap_lang.proofmode]
z:13 [binder, in intensional.examples.iris_extra]
z:33 [binder, in intensional.examples.tactics]
z:62 [binder, in intensional.examples.well_bracketed]

other

_ ↦ - (bi_scope) [notation, in intensional.heap_lang.lifting]
_ ↦{ _ } - (bi_scope) [notation, in intensional.heap_lang.lifting]
_ ↦ _ (bi_scope) [notation, in intensional.heap_lang.lifting]
_ ↦{ _ } _ (bi_scope) [notation, in intensional.heap_lang.lifting]
_ ↦∗ _ (bi_scope) [notation, in intensional.heap_lang.array]
_ ↦∗{ _ } _ (bi_scope) [notation, in intensional.heap_lang.array]
resolve_proph: _ to: _ (expr_scope) [notation, in intensional.heap_lang.notation]
match: _ with SOME _ => _ | NONE => _ end (expr_scope) [notation, in intensional.heap_lang.notation]
match: _ with NONE => _ | SOME _ => _ end (expr_scope) [notation, in intensional.heap_lang.notation]
_ || _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ && _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ ;; _ (expr_scope) [notation, in intensional.heap_lang.notation]
let: _ := _ in _ (expr_scope) [notation, in intensional.heap_lang.notation]
λ: _ _ .. _ , _ (expr_scope) [notation, in intensional.heap_lang.notation]
λ: _ , _ (expr_scope) [notation, in intensional.heap_lang.notation]
rec: _ _ _ .. _ := _ (expr_scope) [notation, in intensional.heap_lang.notation]
if: _ then _ else _ (expr_scope) [notation, in intensional.heap_lang.notation]
rec: _ _ := _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ <- _ (expr_scope) [notation, in intensional.heap_lang.notation]
~ _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ ≠ _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ = _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ < _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ ≤ _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ ≫ _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ ≪ _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ `rem` _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ `quot` _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ * _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ - _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ +ₗ _ (expr_scope) [notation, in intensional.heap_lang.notation]
_ + _ (expr_scope) [notation, in intensional.heap_lang.notation]
- _ (expr_scope) [notation, in intensional.heap_lang.notation]
ref _ (expr_scope) [notation, in intensional.heap_lang.notation]
! _ (expr_scope) [notation, in intensional.heap_lang.notation]
match: _ with InjR _ => _ | InjL _ => _ end (expr_scope) [notation, in intensional.heap_lang.notation]
match: _ with InjL _ => _ | InjR _ => _ end (expr_scope) [notation, in intensional.heap_lang.notation]
( _ , _ , .. , _ ) (expr_scope) [notation, in intensional.heap_lang.notation]
_ +ₗ _ (stdpp_scope) [notation, in intensional.heap_lang.locations]
λ: _ _ .. _ , _ (val_scope) [notation, in intensional.heap_lang.notation]
λ: _ , _ (val_scope) [notation, in intensional.heap_lang.notation]
rec: _ _ _ .. _ := _ (val_scope) [notation, in intensional.heap_lang.notation]
rec: _ _ := _ (val_scope) [notation, in intensional.heap_lang.notation]
() (val_scope) [notation, in intensional.heap_lang.notation]
( _ , _ , .. , _ ) (val_scope) [notation, in intensional.heap_lang.notation]
# _ [notation, in intensional.heap_lang.notation]
Δ':117 [binder, in intensional.heap_lang.proofmode]
Δ':136 [binder, in intensional.heap_lang.proofmode]
Δ':157 [binder, in intensional.heap_lang.proofmode]
Δ':180 [binder, in intensional.heap_lang.proofmode]
Δ':201 [binder, in intensional.heap_lang.proofmode]
Δ':22 [binder, in intensional.heap_lang.proofmode]
Δ':81 [binder, in intensional.heap_lang.proofmode]
Δ':98 [binder, in intensional.heap_lang.proofmode]
Δ:107 [binder, in intensional.heap_lang.proofmode]
Δ:116 [binder, in intensional.heap_lang.proofmode]
Δ:12 [binder, in intensional.heap_lang.proofmode]
Δ:126 [binder, in intensional.heap_lang.proofmode]
Δ:135 [binder, in intensional.heap_lang.proofmode]
Δ:146 [binder, in intensional.heap_lang.proofmode]
Δ:156 [binder, in intensional.heap_lang.proofmode]
Δ:168 [binder, in intensional.heap_lang.proofmode]
Δ:179 [binder, in intensional.heap_lang.proofmode]
Δ:190 [binder, in intensional.heap_lang.proofmode]
Δ:200 [binder, in intensional.heap_lang.proofmode]
Δ:21 [binder, in intensional.heap_lang.proofmode]
Δ:210 [binder, in intensional.heap_lang.proofmode]
Δ:3 [binder, in intensional.heap_lang.proofmode]
Δ:33 [binder, in intensional.heap_lang.proofmode]
Δ:44 [binder, in intensional.heap_lang.proofmode]
Δ:51 [binder, in intensional.heap_lang.proofmode]
Δ:59 [binder, in intensional.heap_lang.proofmode]
Δ:70 [binder, in intensional.heap_lang.proofmode]
Δ:80 [binder, in intensional.heap_lang.proofmode]
Δ:89 [binder, in intensional.heap_lang.proofmode]
Δ:97 [binder, in intensional.heap_lang.proofmode]
Σ:1 [binder, in intensional.heap_lang.array]
Σ:1 [binder, in intensional.examples.traversable_stack]
Σ:1 [binder, in intensional.examples.stack]
Σ:1 [binder, in intensional.heap_lang.proofmode]
Σ:1 [binder, in intensional.heap_lang.adequacy]
Σ:1 [binder, in intensional.examples.iterator]
Σ:1 [binder, in intensional.examples.well_bracketed]
Σ:1 [binder, in intensional.examples.stack_impl]
Σ:1 [binder, in intensional.examples.file]
Σ:10 [binder, in intensional.heap_lang.proofmode]
Σ:101 [binder, in intensional.examples.iterator]
Σ:11 [binder, in intensional.examples.well_bracketed]
Σ:11 [binder, in intensional.examples.file]
Σ:112 [binder, in intensional.examples.linearizability]
Σ:121 [binder, in intensional.examples.linearizability]
Σ:14 [binder, in intensional.heap_lang.lifting]
Σ:14 [binder, in intensional.examples.linearizability]
Σ:14 [binder, in intensional.examples.traversable_stack]
Σ:14 [binder, in intensional.examples.stack]
Σ:15 [binder, in intensional.examples.iris_extra]
Σ:16 [binder, in intensional.examples.iterator]
Σ:16 [binder, in intensional.examples.file]
Σ:18 [binder, in intensional.examples.well_bracketed]
Σ:19 [binder, in intensional.heap_lang.proofmode]
Σ:2 [binder, in intensional.examples.iris_extra]
Σ:20 [binder, in intensional.heap_lang.lifting]
Σ:207 [binder, in intensional.heap_lang.lifting]
Σ:21 [binder, in intensional.heap_lang.adequacy]
Σ:22 [binder, in intensional.examples.traversable_stack]
Σ:22 [binder, in intensional.examples.stack]
Σ:234 [binder, in intensional.examples.linearizability]
Σ:24 [binder, in intensional.examples.iterator]
Σ:248 [binder, in intensional.examples.linearizability]
Σ:25 [binder, in intensional.heap_lang.lifting]
Σ:254 [binder, in intensional.examples.linearizability]
Σ:31 [binder, in intensional.heap_lang.lifting]
Σ:31 [binder, in intensional.heap_lang.proofmode]
Σ:31 [binder, in intensional.examples.iterator]
Σ:32 [binder, in intensional.examples.traversable_stack]
Σ:34 [binder, in intensional.heap_lang.lifting]
Σ:37 [binder, in intensional.heap_lang.adequacy]
Σ:38 [binder, in intensional.examples.stack]
Σ:38 [binder, in intensional.examples.iterator]
Σ:40 [binder, in intensional.heap_lang.lifting]
Σ:42 [binder, in intensional.heap_lang.proofmode]
Σ:43 [binder, in intensional.heap_lang.lifting]
Σ:46 [binder, in intensional.examples.linearizability]
Σ:46 [binder, in intensional.examples.well_bracketed]
Σ:49 [binder, in intensional.heap_lang.lifting]
Σ:49 [binder, in intensional.heap_lang.proofmode]
Σ:52 [binder, in intensional.heap_lang.lifting]
Σ:52 [binder, in intensional.examples.file]
Σ:53 [binder, in intensional.examples.stack]
Σ:55 [binder, in intensional.heap_lang.lifting]
Σ:56 [binder, in intensional.heap_lang.proofmode]
Σ:59 [binder, in intensional.heap_lang.lifting]
Σ:6 [binder, in intensional.examples.linearizability]
Σ:6 [binder, in intensional.examples.file]
Σ:62 [binder, in intensional.examples.traversable_stack]
Σ:62 [binder, in intensional.examples.stack]
Σ:63 [binder, in intensional.heap_lang.lifting]
Σ:63 [binder, in intensional.examples.iterator]
Σ:64 [binder, in intensional.examples.file]
Σ:65 [binder, in intensional.examples.well_bracketed]
Σ:67 [binder, in intensional.heap_lang.lifting]
Σ:67 [binder, in intensional.examples.stack]
Σ:67 [binder, in intensional.heap_lang.proofmode]
Σ:7 [binder, in intensional.examples.traversable_stack]
Σ:7 [binder, in intensional.examples.stack]
Σ:7 [binder, in intensional.heap_lang.adequacy]
Σ:71 [binder, in intensional.heap_lang.lifting]
Σ:73 [binder, in intensional.examples.file]
Σ:74 [binder, in intensional.examples.well_bracketed]
Σ:77 [binder, in intensional.heap_lang.lifting]
Σ:78 [binder, in intensional.examples.traversable_stack]
Σ:78 [binder, in intensional.heap_lang.proofmode]
Σ:78 [binder, in intensional.examples.file]
Σ:79 [binder, in intensional.examples.well_bracketed]
Σ:8 [binder, in intensional.examples.iris_extra]
Σ:8 [binder, in intensional.heap_lang.array]
Σ:8 [binder, in intensional.heap_lang.adequacy]
Σ:8 [binder, in intensional.examples.iterator]
Σ:81 [binder, in intensional.heap_lang.lifting]
Σ:87 [binder, in intensional.examples.traversable_stack]
Σ:87 [binder, in intensional.examples.iterator]
Σ:90 [binder, in intensional.heap_lang.lifting]
Σ:92 [binder, in intensional.examples.traversable_stack]
Σ:94 [binder, in intensional.heap_lang.lifting]
Σ:96 [binder, in intensional.examples.iterator]
Φ:106 [binder, in intensional.heap_lang.proofmode]
Φ:115 [binder, in intensional.heap_lang.proofmode]
Φ:125 [binder, in intensional.heap_lang.proofmode]
Φ:134 [binder, in intensional.heap_lang.proofmode]
Φ:145 [binder, in intensional.heap_lang.proofmode]
Φ:15 [binder, in intensional.heap_lang.proofmode]
Φ:155 [binder, in intensional.heap_lang.proofmode]
Φ:167 [binder, in intensional.heap_lang.proofmode]
Φ:178 [binder, in intensional.heap_lang.proofmode]
Φ:189 [binder, in intensional.heap_lang.proofmode]
Φ:199 [binder, in intensional.heap_lang.proofmode]
Φ:209 [binder, in intensional.heap_lang.proofmode]
Φ:218 [binder, in intensional.heap_lang.proofmode]
Φ:226 [binder, in intensional.heap_lang.lifting]
Φ:230 [binder, in intensional.heap_lang.lifting]
Φ:30 [binder, in intensional.heap_lang.proofmode]
Φ:339 [binder, in intensional.heap_lang.lifting]
Φ:41 [binder, in intensional.heap_lang.proofmode]
Φ:41 [binder, in intensional.heap_lang.adequacy]
Φ:47 [binder, in intensional.heap_lang.proofmode]
Φ:54 [binder, in intensional.heap_lang.proofmode]
Φ:6 [binder, in intensional.heap_lang.proofmode]
Φ:62 [binder, in intensional.heap_lang.proofmode]
Φ:73 [binder, in intensional.heap_lang.proofmode]
Φ:87 [binder, in intensional.heap_lang.proofmode]
Φ:95 [binder, in intensional.heap_lang.proofmode]
α:198 [binder, in intensional.examples.linearizability]
α:229 [binder, in intensional.examples.linearizability]
β:164 [binder, in intensional.examples.linearizability]
γe':183 [binder, in intensional.examples.linearizability]
γe:162 [binder, in intensional.examples.linearizability]
γe:170 [binder, in intensional.examples.linearizability]
γe:176 [binder, in intensional.examples.linearizability]
γe:180 [binder, in intensional.examples.linearizability]
γe:188 [binder, in intensional.examples.linearizability]
γe:196 [binder, in intensional.examples.linearizability]
γe:208 [binder, in intensional.examples.linearizability]
γe:221 [binder, in intensional.examples.linearizability]
γi':181 [binder, in intensional.examples.linearizability]
γi:160 [binder, in intensional.examples.linearizability]
γi:168 [binder, in intensional.examples.linearizability]
γi:174 [binder, in intensional.examples.linearizability]
γi:178 [binder, in intensional.examples.linearizability]
γi:186 [binder, in intensional.examples.linearizability]
γi:194 [binder, in intensional.examples.linearizability]
γi:206 [binder, in intensional.examples.linearizability]
γi:219 [binder, in intensional.examples.linearizability]
γs':182 [binder, in intensional.examples.linearizability]
γs:137 [binder, in intensional.examples.linearizability]
γs:146 [binder, in intensional.examples.linearizability]
γs:152 [binder, in intensional.examples.linearizability]
γs:161 [binder, in intensional.examples.linearizability]
γs:169 [binder, in intensional.examples.linearizability]
γs:175 [binder, in intensional.examples.linearizability]
γs:179 [binder, in intensional.examples.linearizability]
γs:187 [binder, in intensional.examples.linearizability]
γs:195 [binder, in intensional.examples.linearizability]
γs:207 [binder, in intensional.examples.linearizability]
γs:220 [binder, in intensional.examples.linearizability]
γtag:204 [binder, in intensional.examples.linearizability]
γtag:211 [binder, in intensional.examples.linearizability]
γtag:227 [binder, in intensional.examples.linearizability]
γ:10 [binder, in intensional.examples.iris_extra]
γ:11 [binder, in intensional.examples.linearizability]
γ:153 [binder, in intensional.examples.linearizability]
γ:159 [binder, in intensional.examples.linearizability]
γ:166 [binder, in intensional.examples.linearizability]
γ:172 [binder, in intensional.examples.linearizability]
γ:177 [binder, in intensional.examples.linearizability]
γ:18 [binder, in intensional.examples.iris_extra]
γ:185 [binder, in intensional.examples.linearizability]
γ:193 [binder, in intensional.examples.linearizability]
γ:205 [binder, in intensional.examples.linearizability]
γ:21 [binder, in intensional.examples.linearizability]
γ:218 [binder, in intensional.examples.linearizability]
γ:24 [binder, in intensional.examples.linearizability]
γ:4 [binder, in intensional.examples.iris_extra]
κs:18 [binder, in intensional.heap_lang.adequacy]
κs:20 [binder, in intensional.heap_lang.adequacy]
κs:337 [binder, in intensional.heap_lang.lang]
κs:34 [binder, in intensional.heap_lang.adequacy]
κs:36 [binder, in intensional.heap_lang.adequacy]
κs:377 [binder, in intensional.heap_lang.lang]
κs:97 [binder, in intensional.heap_lang.lifting]
κ':388 [binder, in intensional.heap_lang.lang]
κ:332 [binder, in intensional.heap_lang.lifting]
κ:349 [binder, in intensional.heap_lang.lang]
κ:356 [binder, in intensional.heap_lang.lang]
κ:383 [binder, in intensional.heap_lang.lang]
σ':246 [binder, in intensional.examples.linearizability]
σ':28 [binder, in intensional.heap_lang.adequacy]
σ':336 [binder, in intensional.heap_lang.lang]
σ':48 [binder, in intensional.heap_lang.adequacy]
σ':60 [binder, in intensional.examples.stack]
σ':71 [binder, in intensional.examples.file]
σ':72 [binder, in intensional.examples.well_bracketed]
σ':85 [binder, in intensional.examples.traversable_stack]
σ':94 [binder, in intensional.examples.iterator]
σ1':387 [binder, in intensional.heap_lang.lang]
σ1:331 [binder, in intensional.heap_lang.lifting]
σ1:348 [binder, in intensional.heap_lang.lang]
σ1:355 [binder, in intensional.heap_lang.lang]
σ1:376 [binder, in intensional.heap_lang.lang]
σ1:382 [binder, in intensional.heap_lang.lang]
σ2':390 [binder, in intensional.heap_lang.lang]
σ2:334 [binder, in intensional.heap_lang.lifting]
σ2:351 [binder, in intensional.heap_lang.lang]
σ2:358 [binder, in intensional.heap_lang.lang]
σ2:379 [binder, in intensional.heap_lang.lang]
σ2:385 [binder, in intensional.heap_lang.lang]
σ:12 [binder, in intensional.heap_lang.adequacy]
σ:17 [binder, in intensional.heap_lang.adequacy]
σ:19 [binder, in intensional.heap_lang.adequacy]
σ:226 [binder, in intensional.heap_lang.lang]
σ:228 [binder, in intensional.heap_lang.lang]
σ:230 [binder, in intensional.heap_lang.lang]
σ:249 [binder, in intensional.heap_lang.lang]
σ:253 [binder, in intensional.heap_lang.lang]
σ:263 [binder, in intensional.heap_lang.lang]
σ:266 [binder, in intensional.heap_lang.lang]
σ:268 [binder, in intensional.heap_lang.lang]
σ:27 [binder, in intensional.heap_lang.adequacy]
σ:270 [binder, in intensional.heap_lang.lang]
σ:276 [binder, in intensional.heap_lang.lang]
σ:280 [binder, in intensional.heap_lang.lang]
σ:285 [binder, in intensional.heap_lang.lang]
σ:288 [binder, in intensional.heap_lang.lang]
σ:291 [binder, in intensional.heap_lang.lang]
σ:294 [binder, in intensional.heap_lang.lang]
σ:297 [binder, in intensional.heap_lang.lang]
σ:301 [binder, in intensional.heap_lang.lang]
σ:305 [binder, in intensional.heap_lang.lang]
σ:307 [binder, in intensional.heap_lang.lang]
σ:310 [binder, in intensional.heap_lang.lang]
σ:315 [binder, in intensional.heap_lang.lang]
σ:318 [binder, in intensional.heap_lang.lang]
σ:323 [binder, in intensional.heap_lang.lifting]
σ:323 [binder, in intensional.heap_lang.lang]
σ:328 [binder, in intensional.heap_lang.lang]
σ:329 [binder, in intensional.heap_lang.lang]
σ:33 [binder, in intensional.heap_lang.adequacy]
σ:334 [binder, in intensional.heap_lang.lang]
σ:340 [binder, in intensional.heap_lang.lang]
σ:342 [binder, in intensional.heap_lang.lang]
σ:35 [binder, in intensional.heap_lang.adequacy]
σ:366 [binder, in intensional.heap_lang.lang]
σ:368 [binder, in intensional.heap_lang.lang]
σ:395 [binder, in intensional.heap_lang.lang]
σ:47 [binder, in intensional.heap_lang.adequacy]
σ:96 [binder, in intensional.heap_lang.lifting]
φ:13 [binder, in intensional.heap_lang.adequacy]
φ:28 [binder, in intensional.heap_lang.proofmode]
φ:39 [binder, in intensional.heap_lang.proofmode]
ℓ:11 [binder, in intensional.examples.stack_impl]
ℓ:7 [binder, in intensional.examples.stack_impl]

Notation Index

other

_ ↦ - (bi_scope) [in intensional.heap_lang.lifting]
_ ↦{ _ } - (bi_scope) [in intensional.heap_lang.lifting]
_ ↦ _ (bi_scope) [in intensional.heap_lang.lifting]
_ ↦{ _ } _ (bi_scope) [in intensional.heap_lang.lifting]
_ ↦∗ _ (bi_scope) [in intensional.heap_lang.array]
_ ↦∗{ _ } _ (bi_scope) [in intensional.heap_lang.array]
resolve_proph: _ to: _ (expr_scope) [in intensional.heap_lang.notation]
match: _ with SOME _ => _ | NONE => _ end (expr_scope) [in intensional.heap_lang.notation]
match: _ with NONE => _ | SOME _ => _ end (expr_scope) [in intensional.heap_lang.notation]
_ || _ (expr_scope) [in intensional.heap_lang.notation]
_ && _ (expr_scope) [in intensional.heap_lang.notation]
_ ;; _ (expr_scope) [in intensional.heap_lang.notation]
let: _ := _ in _ (expr_scope) [in intensional.heap_lang.notation]
λ: _ _ .. _ , _ (expr_scope) [in intensional.heap_lang.notation]
λ: _ , _ (expr_scope) [in intensional.heap_lang.notation]
rec: _ _ _ .. _ := _ (expr_scope) [in intensional.heap_lang.notation]
if: _ then _ else _ (expr_scope) [in intensional.heap_lang.notation]
rec: _ _ := _ (expr_scope) [in intensional.heap_lang.notation]
_ <- _ (expr_scope) [in intensional.heap_lang.notation]
~ _ (expr_scope) [in intensional.heap_lang.notation]
_ ≠ _ (expr_scope) [in intensional.heap_lang.notation]
_ = _ (expr_scope) [in intensional.heap_lang.notation]
_ < _ (expr_scope) [in intensional.heap_lang.notation]
_ ≤ _ (expr_scope) [in intensional.heap_lang.notation]
_ ≫ _ (expr_scope) [in intensional.heap_lang.notation]
_ ≪ _ (expr_scope) [in intensional.heap_lang.notation]
_ `rem` _ (expr_scope) [in intensional.heap_lang.notation]
_ `quot` _ (expr_scope) [in intensional.heap_lang.notation]
_ * _ (expr_scope) [in intensional.heap_lang.notation]
_ - _ (expr_scope) [in intensional.heap_lang.notation]
_ +ₗ _ (expr_scope) [in intensional.heap_lang.notation]
_ + _ (expr_scope) [in intensional.heap_lang.notation]
- _ (expr_scope) [in intensional.heap_lang.notation]
ref _ (expr_scope) [in intensional.heap_lang.notation]
! _ (expr_scope) [in intensional.heap_lang.notation]
match: _ with InjR _ => _ | InjL _ => _ end (expr_scope) [in intensional.heap_lang.notation]
match: _ with InjL _ => _ | InjR _ => _ end (expr_scope) [in intensional.heap_lang.notation]
( _ , _ , .. , _ ) (expr_scope) [in intensional.heap_lang.notation]
_ +ₗ _ (stdpp_scope) [in intensional.heap_lang.locations]
λ: _ _ .. _ , _ (val_scope) [in intensional.heap_lang.notation]
λ: _ , _ (val_scope) [in intensional.heap_lang.notation]
rec: _ _ _ .. _ := _ (val_scope) [in intensional.heap_lang.notation]
rec: _ _ := _ (val_scope) [in intensional.heap_lang.notation]
() (val_scope) [in intensional.heap_lang.notation]
( _ , _ , .. , _ ) (val_scope) [in intensional.heap_lang.notation]
# _ [in intensional.heap_lang.notation]

Binder Index

A

add_impl:69 [in intensional.examples.iterator]
add:12 [in intensional.examples.iterator]
AsRecV0:183 [in intensional.heap_lang.lifting]
A:1 [in intensional.heap_lang.lifting]
A:1 [in intensional.examples.tactics]
A:1 [in intensional.examples.iris_extra]
A:1 [in intensional.examples.stdpp_extra]
A:10 [in intensional.heap_lang.lifting]
A:12 [in intensional.examples.stdpp_extra]
A:13 [in intensional.examples.tactics]
A:14 [in intensional.examples.iris_extra]
a:17 [in intensional.examples.tactics]
A:18 [in intensional.examples.tactics]
a:2 [in intensional.examples.tactics]
a:24 [in intensional.examples.tactics]
A:27 [in intensional.examples.tactics]
a:35 [in intensional.examples.tactics]
A:5 [in intensional.examples.tactics]
A:6 [in intensional.heap_lang.lifting]
A:6 [in intensional.examples.stdpp_extra]
A:7 [in intensional.examples.iris_extra]
A:73 [in intensional.heap_lang.lifting]
a:8 [in intensional.examples.tactics]
A:87 [in intensional.heap_lang.lifting]
a:9 [in intensional.heap_lang.lifting]
A:9 [in intensional.examples.tactics]

B

b1:212 [in intensional.heap_lang.lang]
b2:213 [in intensional.heap_lang.lang]
B:10 [in intensional.examples.tactics]
B:14 [in intensional.examples.tactics]
B:19 [in intensional.examples.tactics]
b:25 [in intensional.examples.tactics]
B:28 [in intensional.examples.tactics]
b:324 [in intensional.heap_lang.lang]
b:36 [in intensional.examples.tactics]
b:4 [in intensional.heap_lang.lang]
B:6 [in intensional.examples.tactics]

C

close_impl:58 [in intensional.examples.file]
close:10 [in intensional.examples.file]
Coll_impl:66 [in intensional.examples.iterator]
Coll:10 [in intensional.examples.iterator]
Coll:18 [in intensional.examples.iterator]
Coll:26 [in intensional.examples.iterator]
Coll:3 [in intensional.examples.iterator]
Coll:33 [in intensional.examples.iterator]
Coll:42 [in intensional.examples.iterator]
create_impl:68 [in intensional.examples.traversable_stack]
create_impl:44 [in intensional.examples.stack]
create:5 [in intensional.examples.traversable_stack]
create:5 [in intensional.examples.stack]
ctx:184 [in intensional.heap_lang.lang]
c':15 [in intensional.examples.iterator]
c':23 [in intensional.examples.iterator]
c:13 [in intensional.examples.iterator]
C:20 [in intensional.examples.tactics]
c:21 [in intensional.examples.iterator]
C:29 [in intensional.examples.tactics]
c:29 [in intensional.examples.iterator]
c:36 [in intensional.examples.iterator]
c:37 [in intensional.examples.tactics]
c:44 [in intensional.examples.iterator]
c:6 [in intensional.examples.iterator]

D

D:30 [in intensional.examples.tactics]

E

efs':391 [in intensional.heap_lang.lang]
efs:335 [in intensional.heap_lang.lifting]
efs:352 [in intensional.heap_lang.lang]
efs:359 [in intensional.heap_lang.lang]
efs:380 [in intensional.heap_lang.lang]
efs:386 [in intensional.heap_lang.lang]
elts:139 [in intensional.examples.linearizability]
erec:165 [in intensional.heap_lang.lifting]
erec:173 [in intensional.heap_lang.lifting]
erec:180 [in intensional.heap_lang.lifting]
e_init:44 [in intensional.heap_lang.adequacy]
e'':18 [in intensional.heap_lang.proofmode]
e'':9 [in intensional.heap_lang.proofmode]
e':17 [in intensional.heap_lang.proofmode]
e':247 [in intensional.examples.linearizability]
e':275 [in intensional.heap_lang.lang]
e':49 [in intensional.heap_lang.adequacy]
e':61 [in intensional.examples.stack]
e':72 [in intensional.examples.file]
e':73 [in intensional.examples.well_bracketed]
e':8 [in intensional.heap_lang.proofmode]
e':86 [in intensional.examples.traversable_stack]
e':95 [in intensional.examples.iterator]
e0:178 [in intensional.heap_lang.lang]
e0:180 [in intensional.heap_lang.lang]
e0:187 [in intensional.heap_lang.lang]
e0:189 [in intensional.heap_lang.lang]
e0:28 [in intensional.heap_lang.lang]
e0:37 [in intensional.heap_lang.lang]
e0:46 [in intensional.heap_lang.lang]
e0:51 [in intensional.heap_lang.lang]
e1:128 [in intensional.heap_lang.lifting]
e1:160 [in intensional.heap_lang.lang]
e1:165 [in intensional.heap_lang.lang]
e1:166 [in intensional.heap_lang.lang]
e1:169 [in intensional.heap_lang.lang]
e1:170 [in intensional.heap_lang.lang]
e1:173 [in intensional.heap_lang.lang]
e1:175 [in intensional.heap_lang.lang]
e1:181 [in intensional.heap_lang.lang]
e1:183 [in intensional.heap_lang.lang]
e1:190 [in intensional.heap_lang.lang]
e1:193 [in intensional.heap_lang.lifting]
e1:195 [in intensional.heap_lang.lifting]
e1:202 [in intensional.heap_lang.lifting]
e1:205 [in intensional.heap_lang.lifting]
e1:21 [in intensional.heap_lang.lang]
e1:26 [in intensional.heap_lang.lang]
e1:26 [in intensional.heap_lang.proofmode]
e1:273 [in intensional.heap_lang.lang]
e1:286 [in intensional.heap_lang.lang]
e1:289 [in intensional.heap_lang.lang]
e1:29 [in intensional.heap_lang.lang]
e1:299 [in intensional.heap_lang.lang]
e1:303 [in intensional.heap_lang.lang]
e1:31 [in intensional.heap_lang.lang]
e1:347 [in intensional.heap_lang.lang]
e1:362 [in intensional.heap_lang.lang]
e1:37 [in intensional.heap_lang.proofmode]
e1:38 [in intensional.heap_lang.lang]
e1:381 [in intensional.heap_lang.lang]
e1:41 [in intensional.heap_lang.lang]
e1:44 [in intensional.heap_lang.lang]
e1:47 [in intensional.heap_lang.lang]
e1:49 [in intensional.heap_lang.lang]
e1:52 [in intensional.heap_lang.lang]
e1:81 [in intensional.heap_lang.lang]
e1:91 [in intensional.heap_lang.lang]
e2':389 [in intensional.heap_lang.lang]
e2:126 [in intensional.heap_lang.lifting]
e2:167 [in intensional.heap_lang.lang]
e2:171 [in intensional.heap_lang.lang]
e2:194 [in intensional.heap_lang.lifting]
e2:196 [in intensional.heap_lang.lifting]
e2:203 [in intensional.heap_lang.lifting]
e2:206 [in intensional.heap_lang.lifting]
e2:22 [in intensional.heap_lang.lang]
e2:27 [in intensional.heap_lang.lang]
e2:27 [in intensional.heap_lang.proofmode]
e2:287 [in intensional.heap_lang.lang]
e2:290 [in intensional.heap_lang.lang]
e2:30 [in intensional.heap_lang.lang]
e2:300 [in intensional.heap_lang.lang]
e2:304 [in intensional.heap_lang.lang]
e2:32 [in intensional.heap_lang.lang]
e2:333 [in intensional.heap_lang.lifting]
e2:350 [in intensional.heap_lang.lang]
e2:357 [in intensional.heap_lang.lang]
e2:363 [in intensional.heap_lang.lang]
e2:38 [in intensional.heap_lang.proofmode]
e2:384 [in intensional.heap_lang.lang]
e2:39 [in intensional.heap_lang.lang]
e2:42 [in intensional.heap_lang.lang]
e2:45 [in intensional.heap_lang.lang]
e2:48 [in intensional.heap_lang.lang]
e2:50 [in intensional.heap_lang.lang]
e2:53 [in intensional.heap_lang.lang]
e2:82 [in intensional.heap_lang.lang]
e2:92 [in intensional.heap_lang.lang]
E:100 [in intensional.heap_lang.proofmode]
e:104 [in intensional.heap_lang.lifting]
E:104 [in intensional.heap_lang.array]
E:109 [in intensional.heap_lang.proofmode]
e:11 [in intensional.heap_lang.adequacy]
E:110 [in intensional.heap_lang.array]
E:116 [in intensional.heap_lang.array]
E:119 [in intensional.heap_lang.proofmode]
E:123 [in intensional.heap_lang.array]
e:125 [in intensional.heap_lang.lang]
E:128 [in intensional.heap_lang.proofmode]
E:130 [in intensional.heap_lang.array]
e:131 [in intensional.heap_lang.lang]
e:135 [in intensional.heap_lang.lifting]
e:137 [in intensional.heap_lang.lang]
E:138 [in intensional.heap_lang.array]
E:138 [in intensional.heap_lang.proofmode]
E:14 [in intensional.heap_lang.proofmode]
e:143 [in intensional.heap_lang.lang]
E:146 [in intensional.heap_lang.array]
E:148 [in intensional.heap_lang.proofmode]
e:149 [in intensional.heap_lang.lang]
e:153 [in intensional.heap_lang.lang]
E:154 [in intensional.heap_lang.array]
e:157 [in intensional.heap_lang.lifting]
E:159 [in intensional.heap_lang.proofmode]
e:16 [in intensional.heap_lang.proofmode]
E:162 [in intensional.heap_lang.array]
e:170 [in intensional.heap_lang.lifting]
E:170 [in intensional.heap_lang.proofmode]
E:171 [in intensional.heap_lang.array]
E:18 [in intensional.examples.linearizability]
E:180 [in intensional.heap_lang.array]
E:182 [in intensional.heap_lang.proofmode]
E:189 [in intensional.heap_lang.array]
e:192 [in intensional.heap_lang.lang]
E:192 [in intensional.heap_lang.proofmode]
e:197 [in intensional.heap_lang.lang]
E:198 [in intensional.heap_lang.array]
e:20 [in intensional.heap_lang.lang]
E:203 [in intensional.heap_lang.proofmode]
E:205 [in intensional.heap_lang.array]
E:210 [in intensional.heap_lang.lifting]
E:212 [in intensional.heap_lang.array]
E:212 [in intensional.heap_lang.proofmode]
E:216 [in intensional.heap_lang.lifting]
E:220 [in intensional.heap_lang.array]
E:224 [in intensional.heap_lang.lifting]
e:225 [in intensional.heap_lang.lifting]
E:228 [in intensional.heap_lang.lifting]
e:229 [in intensional.heap_lang.lifting]
e:24 [in intensional.heap_lang.lang]
E:24 [in intensional.heap_lang.proofmode]
E:243 [in intensional.heap_lang.lifting]
e:244 [in intensional.examples.linearizability]
E:249 [in intensional.heap_lang.lifting]
E:251 [in intensional.examples.linearizability]
E:255 [in intensional.heap_lang.lifting]
E:259 [in intensional.heap_lang.lifting]
e:26 [in intensional.heap_lang.adequacy]
e:262 [in intensional.heap_lang.lang]
E:263 [in intensional.heap_lang.lifting]
E:268 [in intensional.heap_lang.lifting]
E:273 [in intensional.heap_lang.lifting]
E:278 [in intensional.heap_lang.lifting]
E:283 [in intensional.heap_lang.lifting]
E:290 [in intensional.heap_lang.lifting]
E:297 [in intensional.heap_lang.lifting]
E:303 [in intensional.heap_lang.lifting]
e:306 [in intensional.heap_lang.lang]
E:309 [in intensional.heap_lang.lifting]
E:314 [in intensional.heap_lang.lifting]
E:319 [in intensional.heap_lang.lifting]
e:322 [in intensional.heap_lang.lifting]
e:328 [in intensional.heap_lang.lifting]
e:33 [in intensional.heap_lang.lang]
e:333 [in intensional.heap_lang.lang]
E:337 [in intensional.heap_lang.lifting]
e:338 [in intensional.heap_lang.lifting]
e:34 [in intensional.heap_lang.lang]
E:346 [in intensional.heap_lang.lifting]
e:346 [in intensional.heap_lang.lang]
e:35 [in intensional.heap_lang.lang]
E:35 [in intensional.heap_lang.proofmode]
E:352 [in intensional.heap_lang.lifting]
e:354 [in intensional.heap_lang.lang]
e:36 [in intensional.heap_lang.lang]
E:361 [in intensional.heap_lang.lifting]
e:371 [in intensional.heap_lang.lang]
e:375 [in intensional.heap_lang.lang]
e:392 [in intensional.heap_lang.lang]
e:40 [in intensional.heap_lang.lang]
e:40 [in intensional.examples.file]
e:43 [in intensional.heap_lang.lang]
e:43 [in intensional.heap_lang.adequacy]
E:45 [in intensional.examples.linearizability]
E:46 [in intensional.heap_lang.proofmode]
E:5 [in intensional.heap_lang.proofmode]
E:52 [in intensional.heap_lang.array]
E:53 [in intensional.heap_lang.proofmode]
e:54 [in intensional.heap_lang.lang]
e:55 [in intensional.heap_lang.lang]
E:58 [in intensional.heap_lang.array]
e:58 [in intensional.examples.stack]
e:59 [in intensional.heap_lang.lang]
E:61 [in intensional.heap_lang.proofmode]
e:63 [in intensional.heap_lang.proofmode]
E:64 [in intensional.heap_lang.array]
e:64 [in intensional.heap_lang.lang]
e:66 [in intensional.heap_lang.proofmode]
e:69 [in intensional.examples.file]
e:7 [in intensional.heap_lang.proofmode]
e:70 [in intensional.heap_lang.lifting]
E:70 [in intensional.heap_lang.array]
e:70 [in intensional.examples.well_bracketed]
E:72 [in intensional.heap_lang.proofmode]
e:74 [in intensional.heap_lang.proofmode]
E:76 [in intensional.heap_lang.array]
e:77 [in intensional.heap_lang.proofmode]
e:79 [in intensional.heap_lang.lang]
E:83 [in intensional.heap_lang.array]
e:83 [in intensional.examples.traversable_stack]
E:83 [in intensional.heap_lang.proofmode]
E:90 [in intensional.heap_lang.array]
E:91 [in intensional.heap_lang.proofmode]
e:92 [in intensional.examples.iterator]
E:97 [in intensional.heap_lang.array]

F

foreach_impl:69 [in intensional.examples.traversable_stack]
foreach:25 [in intensional.examples.traversable_stack]
f:102 [in intensional.heap_lang.lifting]
f:113 [in intensional.heap_lang.lifting]
f:12 [in intensional.examples.tactics]
f:16 [in intensional.examples.tactics]
f:163 [in intensional.heap_lang.lifting]
f:168 [in intensional.heap_lang.lifting]
f:171 [in intensional.heap_lang.lifting]
f:178 [in intensional.heap_lang.lifting]
f:18 [in intensional.heap_lang.lang]
f:225 [in intensional.heap_lang.lang]
f:229 [in intensional.heap_lang.lang]
f:23 [in intensional.examples.tactics]
f:23 [in intensional.examples.stack_impl]
f:260 [in intensional.heap_lang.lang]
f:271 [in intensional.heap_lang.lang]
f:28 [in intensional.examples.traversable_stack]
f:32 [in intensional.examples.well_bracketed]
f:34 [in intensional.examples.tactics]
f:36 [in intensional.examples.well_bracketed]
f:38 [in intensional.examples.traversable_stack]
f:39 [in intensional.examples.well_bracketed]
f:43 [in intensional.examples.well_bracketed]
f:52 [in intensional.examples.traversable_stack]
f:54 [in intensional.examples.well_bracketed]
f:56 [in intensional.examples.traversable_stack]
f:56 [in intensional.examples.well_bracketed]
f:57 [in intensional.heap_lang.lang]
f:58 [in intensional.examples.well_bracketed]
f:59 [in intensional.examples.traversable_stack]
f:64 [in intensional.heap_lang.proofmode]
f:7 [in intensional.examples.tactics]
f:75 [in intensional.heap_lang.proofmode]
f:8 [in intensional.examples.well_bracketed]

G

good_trace:46 [in intensional.heap_lang.adequacy]
gs:136 [in intensional.examples.linearizability]
g:157 [in intensional.examples.linearizability]

H

heapG0:11 [in intensional.heap_lang.proofmode]
heapG0:12 [in intensional.examples.well_bracketed]
heapG0:12 [in intensional.examples.file]
heapG0:15 [in intensional.examples.linearizability]
heapG0:15 [in intensional.examples.traversable_stack]
heapG0:15 [in intensional.examples.stack]
heapG0:15 [in intensional.heap_lang.adequacy]
heapG0:17 [in intensional.examples.iterator]
heapG0:17 [in intensional.examples.file]
heapG0:19 [in intensional.examples.well_bracketed]
heapG0:2 [in intensional.heap_lang.array]
heapG0:2 [in intensional.examples.traversable_stack]
heapG0:2 [in intensional.examples.stack]
heapG0:2 [in intensional.heap_lang.proofmode]
heapG0:2 [in intensional.examples.iterator]
heapG0:2 [in intensional.examples.well_bracketed]
heapG0:2 [in intensional.examples.file]
heapG0:20 [in intensional.heap_lang.proofmode]
heapG0:208 [in intensional.heap_lang.lifting]
heapG0:23 [in intensional.examples.traversable_stack]
heapG0:23 [in intensional.examples.stack]
heapG0:25 [in intensional.examples.iterator]
heapG0:30 [in intensional.heap_lang.adequacy]
heapG0:32 [in intensional.heap_lang.proofmode]
heapG0:32 [in intensional.examples.iterator]
heapG0:33 [in intensional.examples.traversable_stack]
heapG0:39 [in intensional.examples.iterator]
heapG0:43 [in intensional.heap_lang.proofmode]
heapG0:47 [in intensional.examples.linearizability]
heapG0:50 [in intensional.heap_lang.proofmode]
heapG0:54 [in intensional.examples.stack]
heapG0:57 [in intensional.heap_lang.proofmode]
heapG0:65 [in intensional.examples.file]
heapG0:66 [in intensional.examples.well_bracketed]
heapG0:68 [in intensional.heap_lang.proofmode]
heapG0:7 [in intensional.examples.file]
heapG0:79 [in intensional.examples.traversable_stack]
heapG0:79 [in intensional.heap_lang.proofmode]
heapG0:8 [in intensional.examples.traversable_stack]
heapG0:8 [in intensional.examples.stack]
heapG0:88 [in intensional.examples.iterator]
heapG0:9 [in intensional.heap_lang.array]
heapG0:9 [in intensional.examples.iterator]
heapG0:95 [in intensional.heap_lang.lifting]
heapPreG0:22 [in intensional.heap_lang.adequacy]
heapPreG0:9 [in intensional.heap_lang.adequacy]
hI:45 [in intensional.heap_lang.lifting]
HNN':128 [in intensional.examples.linearizability]
hT:32 [in intensional.heap_lang.lifting]
hT:35 [in intensional.heap_lang.lifting]
hT:38 [in intensional.heap_lang.lifting]
hT:41 [in intensional.heap_lang.lifting]
hT:44 [in intensional.heap_lang.lifting]
hT:91 [in intensional.heap_lang.lifting]
H':39 [in intensional.examples.tactics]
H0:123 [in intensional.examples.linearizability]
H0:236 [in intensional.examples.linearizability]
H0:249 [in intensional.examples.linearizability]
H0:255 [in intensional.examples.linearizability]
H0:40 [in intensional.heap_lang.adequacy]
H0:50 [in intensional.heap_lang.adequacy]
H0:51 [in intensional.heap_lang.adequacy]
H0:52 [in intensional.heap_lang.adequacy]
H0:83 [in intensional.heap_lang.lifting]
H2:125 [in intensional.examples.linearizability]
H2:238 [in intensional.examples.linearizability]
H:102 [in intensional.examples.iterator]
H:111 [in intensional.examples.linearizability]
H:118 [in intensional.examples.linearizability]
H:119 [in intensional.examples.linearizability]
H:122 [in intensional.examples.linearizability]
H:15 [in intensional.examples.stdpp_extra]
H:16 [in intensional.examples.linearizability]
H:16 [in intensional.examples.iris_extra]
H:2 [in intensional.examples.stack_impl]
H:235 [in intensional.examples.linearizability]
h:242 [in intensional.heap_lang.lang]
H:243 [in intensional.examples.linearizability]
h:250 [in intensional.heap_lang.lang]
H:26 [in intensional.examples.tactics]
H:3 [in intensional.examples.iris_extra]
H:38 [in intensional.examples.tactics]
H:38 [in intensional.heap_lang.adequacy]
H:39 [in intensional.examples.stack]
H:44 [in intensional.examples.linearizability]
H:47 [in intensional.examples.well_bracketed]
H:50 [in intensional.heap_lang.lifting]
H:53 [in intensional.heap_lang.lifting]
H:53 [in intensional.examples.file]
H:56 [in intensional.heap_lang.lifting]
H:60 [in intensional.heap_lang.lifting]
H:63 [in intensional.examples.traversable_stack]
H:63 [in intensional.examples.stack]
H:64 [in intensional.heap_lang.lifting]
H:64 [in intensional.examples.iterator]
H:65 [in intensional.examples.linearizability]
H:68 [in intensional.heap_lang.lifting]
H:68 [in intensional.examples.stack]
H:7 [in intensional.examples.linearizability]
H:72 [in intensional.heap_lang.lifting]
H:74 [in intensional.examples.file]
H:75 [in intensional.examples.well_bracketed]
h:76 [in intensional.heap_lang.lifting]
H:78 [in intensional.heap_lang.lifting]
H:79 [in intensional.examples.file]
h:80 [in intensional.heap_lang.lifting]
H:80 [in intensional.examples.well_bracketed]
H:82 [in intensional.heap_lang.lifting]
H:84 [in intensional.examples.linearizability]
H:88 [in intensional.examples.linearizability]
H:88 [in intensional.examples.traversable_stack]
H:9 [in intensional.examples.iris_extra]
H:9 [in intensional.examples.stdpp_extra]
H:93 [in intensional.heap_lang.lifting]
H:93 [in intensional.examples.traversable_stack]
H:97 [in intensional.examples.iterator]

I

imimpl:45 [in intensional.heap_lang.adequacy]
init_impl:131 [in intensional.examples.linearizability]
init:20 [in intensional.examples.linearizability]
isClosed_impl:56 [in intensional.examples.file]
isClosed:21 [in intensional.examples.file]
isClosed:3 [in intensional.examples.file]
isClosed:8 [in intensional.examples.file]
isOpen_impl:55 [in intensional.examples.file]
isOpen:13 [in intensional.examples.file]
isOpen:20 [in intensional.examples.file]
isOpen:4 [in intensional.examples.file]
isOpen:9 [in intensional.examples.file]
iterator_impl:71 [in intensional.examples.iterator]
iterator:28 [in intensional.examples.iterator]
Iter_impl:67 [in intensional.examples.iterator]
Iter:11 [in intensional.examples.iterator]
Iter:19 [in intensional.examples.iterator]
Iter:27 [in intensional.examples.iterator]
Iter:34 [in intensional.examples.iterator]
Iter:4 [in intensional.examples.iterator]
Iter:43 [in intensional.examples.iterator]
i1:202 [in intensional.heap_lang.array]
i1:209 [in intensional.heap_lang.array]
i1:217 [in intensional.heap_lang.array]
i1:225 [in intensional.heap_lang.array]
i1:311 [in intensional.heap_lang.lifting]
i1:316 [in intensional.heap_lang.lifting]
i1:326 [in intensional.heap_lang.lang]
i2:203 [in intensional.heap_lang.array]
i2:210 [in intensional.heap_lang.array]
i2:218 [in intensional.heap_lang.array]
i2:226 [in intensional.heap_lang.array]
i2:312 [in intensional.heap_lang.lifting]
i2:317 [in intensional.heap_lang.lifting]
i2:327 [in intensional.heap_lang.lang]
i:10 [in intensional.heap_lang.locations]
i:101 [in intensional.heap_lang.proofmode]
i:110 [in intensional.heap_lang.proofmode]
i:120 [in intensional.heap_lang.proofmode]
i:129 [in intensional.heap_lang.proofmode]
i:139 [in intensional.heap_lang.proofmode]
i:149 [in intensional.heap_lang.proofmode]
i:160 [in intensional.heap_lang.proofmode]
i:171 [in intensional.heap_lang.proofmode]
i:18 [in intensional.heap_lang.locations]
i:183 [in intensional.heap_lang.proofmode]
i:193 [in intensional.heap_lang.proofmode]
i:204 [in intensional.heap_lang.proofmode]
i:213 [in intensional.heap_lang.proofmode]
I:214 [in intensional.heap_lang.lifting]
I:220 [in intensional.heap_lang.lifting]
i:235 [in intensional.heap_lang.lifting]
I:24 [in intensional.heap_lang.adequacy]
I:24 [in intensional.examples.stack_impl]
i:241 [in intensional.heap_lang.lifting]
i:245 [in intensional.heap_lang.lang]
i:247 [in intensional.heap_lang.lifting]
i:253 [in intensional.heap_lang.lifting]
I:29 [in intensional.examples.traversable_stack]
i:29 [in intensional.examples.stack]
i:3 [in intensional.heap_lang.locations]
i:312 [in intensional.heap_lang.lang]
i:37 [in intensional.examples.stack]
i:4 [in intensional.heap_lang.locations]
I:47 [in intensional.heap_lang.lifting]
i:47 [in intensional.examples.iterator]
i:49 [in intensional.examples.stack]
i:5 [in intensional.examples.stdpp_extra]
i:50 [in intensional.heap_lang.array]
i:56 [in intensional.heap_lang.array]
i:6 [in intensional.heap_lang.array]
i:62 [in intensional.heap_lang.array]
i:68 [in intensional.heap_lang.array]
i:74 [in intensional.heap_lang.array]
I:86 [in intensional.heap_lang.lifting]

J

j:11 [in intensional.heap_lang.locations]
j:241 [in intensional.heap_lang.lang]
j:31 [in intensional.examples.stack]
j:49 [in intensional.examples.iterator]
j:84 [in intensional.heap_lang.proofmode]
j:92 [in intensional.heap_lang.proofmode]

K

Ki1:360 [in intensional.heap_lang.lang]
Ki2:361 [in intensional.heap_lang.lang]
Ki:191 [in intensional.heap_lang.lang]
Ki:344 [in intensional.heap_lang.lang]
Ki:345 [in intensional.heap_lang.lang]
Ki:353 [in intensional.heap_lang.lang]
K:102 [in intensional.heap_lang.proofmode]
K:111 [in intensional.heap_lang.proofmode]
K:121 [in intensional.heap_lang.proofmode]
k:13 [in intensional.heap_lang.lifting]
K:130 [in intensional.heap_lang.proofmode]
K:140 [in intensional.heap_lang.proofmode]
k:15 [in intensional.heap_lang.locations]
K:150 [in intensional.heap_lang.proofmode]
K:161 [in intensional.heap_lang.proofmode]
K:172 [in intensional.heap_lang.proofmode]
K:184 [in intensional.heap_lang.proofmode]
K:194 [in intensional.heap_lang.proofmode]
K:205 [in intensional.heap_lang.proofmode]
K:214 [in intensional.heap_lang.proofmode]
k:240 [in intensional.heap_lang.lang]
K:25 [in intensional.heap_lang.proofmode]
k:26 [in intensional.examples.file]
K:36 [in intensional.heap_lang.proofmode]
K:370 [in intensional.heap_lang.lang]
k:50 [in intensional.examples.iterator]
K:58 [in intensional.heap_lang.proofmode]
k:59 [in intensional.examples.iterator]
k:61 [in intensional.examples.iterator]
K:69 [in intensional.heap_lang.proofmode]
k:77 [in intensional.examples.iterator]
k:84 [in intensional.examples.iterator]
K:85 [in intensional.heap_lang.proofmode]
K:93 [in intensional.heap_lang.proofmode]

L

lib_impl:242 [in intensional.examples.linearizability]
lib_impl:232 [in intensional.examples.linearizability]
lib_impl:82 [in intensional.examples.traversable_stack]
lib_impl:76 [in intensional.examples.traversable_stack]
lib_impl:57 [in intensional.examples.stack]
lib_impl:51 [in intensional.examples.stack]
lib_impl:91 [in intensional.examples.iterator]
lib_impl:85 [in intensional.examples.iterator]
lib_impl:69 [in intensional.examples.well_bracketed]
lib_impl:63 [in intensional.examples.well_bracketed]
lib_impl:68 [in intensional.examples.file]
lib_impl:62 [in intensional.examples.file]
lib:19 [in intensional.examples.file]
lib:21 [in intensional.examples.well_bracketed]
lib:245 [in intensional.examples.linearizability]
lib:25 [in intensional.examples.stack]
lib:252 [in intensional.examples.linearizability]
lib:35 [in intensional.examples.traversable_stack]
lib:41 [in intensional.examples.iterator]
lib:49 [in intensional.examples.linearizability]
lib:59 [in intensional.examples.stack]
lib:65 [in intensional.examples.stack]
lib:70 [in intensional.examples.file]
lib:71 [in intensional.examples.well_bracketed]
lib:76 [in intensional.examples.file]
lib:77 [in intensional.examples.well_bracketed]
lib:84 [in intensional.examples.traversable_stack]
lib:90 [in intensional.examples.traversable_stack]
lib:93 [in intensional.examples.iterator]
lib:99 [in intensional.examples.iterator]
locked_impl:49 [in intensional.examples.well_bracketed]
locked:13 [in intensional.examples.well_bracketed]
locked:22 [in intensional.examples.well_bracketed]
locked:3 [in intensional.examples.well_bracketed]
ls:14 [in intensional.heap_lang.locations]
ls:17 [in intensional.heap_lang.locations]
ls:22 [in intensional.heap_lang.locations]
ls:25 [in intensional.heap_lang.locations]
lv:12 [in intensional.examples.stack_impl]
l':234 [in intensional.heap_lang.lifting]
l':239 [in intensional.heap_lang.lifting]
l':58 [in intensional.examples.traversable_stack]
l':61 [in intensional.examples.traversable_stack]
l1:216 [in intensional.heap_lang.lang]
l:10 [in intensional.heap_lang.array]
l:10 [in intensional.examples.stdpp_extra]
l:101 [in intensional.heap_lang.lang]
l:103 [in intensional.heap_lang.lang]
l:103 [in intensional.heap_lang.proofmode]
l:105 [in intensional.heap_lang.array]
l:105 [in intensional.heap_lang.lang]
l:107 [in intensional.heap_lang.lang]
l:11 [in intensional.examples.traversable_stack]
l:11 [in intensional.examples.stack]
l:111 [in intensional.heap_lang.array]
l:112 [in intensional.heap_lang.proofmode]
l:117 [in intensional.heap_lang.array]
l:12 [in intensional.heap_lang.lifting]
l:12 [in intensional.heap_lang.locations]
l:122 [in intensional.heap_lang.proofmode]
l:124 [in intensional.heap_lang.array]
l:13 [in intensional.heap_lang.array]
l:13 [in intensional.heap_lang.locations]
l:131 [in intensional.heap_lang.array]
l:131 [in intensional.heap_lang.proofmode]
l:139 [in intensional.heap_lang.array]
l:141 [in intensional.heap_lang.proofmode]
l:147 [in intensional.heap_lang.array]
l:151 [in intensional.heap_lang.proofmode]
l:155 [in intensional.heap_lang.array]
l:16 [in intensional.heap_lang.array]
l:16 [in intensional.examples.stack_impl]
l:16 [in intensional.examples.stdpp_extra]
l:162 [in intensional.heap_lang.proofmode]
l:163 [in intensional.heap_lang.array]
l:172 [in intensional.heap_lang.array]
l:173 [in intensional.heap_lang.proofmode]
l:18 [in intensional.examples.traversable_stack]
l:18 [in intensional.examples.stack]
l:18 [in intensional.examples.stack_impl]
l:181 [in intensional.heap_lang.array]
l:185 [in intensional.heap_lang.proofmode]
l:19 [in intensional.heap_lang.locations]
l:190 [in intensional.heap_lang.array]
l:195 [in intensional.heap_lang.proofmode]
l:199 [in intensional.heap_lang.array]
l:2 [in intensional.examples.stdpp_extra]
l:20 [in intensional.heap_lang.array]
l:20 [in intensional.heap_lang.locations]
l:206 [in intensional.heap_lang.array]
l:206 [in intensional.heap_lang.proofmode]
l:213 [in intensional.heap_lang.array]
l:215 [in intensional.heap_lang.proofmode]
l:22 [in intensional.heap_lang.array]
l:22 [in intensional.examples.stack_impl]
l:221 [in intensional.heap_lang.array]
l:23 [in intensional.heap_lang.locations]
l:231 [in intensional.heap_lang.lifting]
l:231 [in intensional.heap_lang.lang]
l:235 [in intensional.heap_lang.lang]
l:236 [in intensional.heap_lang.lifting]
l:237 [in intensional.heap_lang.lang]
l:243 [in intensional.heap_lang.lang]
l:246 [in intensional.heap_lang.lifting]
l:246 [in intensional.heap_lang.lang]
l:25 [in intensional.heap_lang.array]
l:251 [in intensional.heap_lang.lang]
l:252 [in intensional.heap_lang.lifting]
l:257 [in intensional.heap_lang.lifting]
l:26 [in intensional.examples.traversable_stack]
l:26 [in intensional.heap_lang.locations]
l:261 [in intensional.heap_lang.lifting]
l:264 [in intensional.heap_lang.lifting]
l:269 [in intensional.heap_lang.lifting]
l:274 [in intensional.heap_lang.lifting]
l:279 [in intensional.heap_lang.lifting]
l:284 [in intensional.heap_lang.lifting]
l:29 [in intensional.heap_lang.array]
l:291 [in intensional.heap_lang.lifting]
l:298 [in intensional.heap_lang.lifting]
l:3 [in intensional.heap_lang.lifting]
l:3 [in intensional.heap_lang.array]
l:3 [in intensional.examples.stack_impl]
l:304 [in intensional.heap_lang.lifting]
l:310 [in intensional.heap_lang.lifting]
l:311 [in intensional.heap_lang.lang]
l:313 [in intensional.heap_lang.lang]
l:315 [in intensional.heap_lang.lifting]
l:316 [in intensional.heap_lang.lang]
l:319 [in intensional.heap_lang.lang]
l:325 [in intensional.heap_lang.lang]
l:33 [in intensional.heap_lang.array]
l:353 [in intensional.heap_lang.lifting]
l:362 [in intensional.heap_lang.lifting]
l:367 [in intensional.heap_lang.lang]
l:39 [in intensional.heap_lang.array]
l:39 [in intensional.examples.traversable_stack]
l:44 [in intensional.examples.traversable_stack]
l:45 [in intensional.examples.stack]
l:46 [in intensional.heap_lang.array]
l:48 [in intensional.examples.traversable_stack]
l:48 [in intensional.examples.iterator]
l:5 [in intensional.heap_lang.lang]
l:5 [in intensional.heap_lang.locations]
l:50 [in intensional.examples.traversable_stack]
l:54 [in intensional.examples.traversable_stack]
l:55 [in intensional.heap_lang.array]
l:56 [in intensional.heap_lang.lang]
l:57 [in intensional.examples.traversable_stack]
l:60 [in intensional.examples.traversable_stack]
l:61 [in intensional.heap_lang.array]
l:66 [in intensional.heap_lang.lang]
l:67 [in intensional.heap_lang.array]
l:7 [in intensional.heap_lang.locations]
l:70 [in intensional.heap_lang.lang]
l:70 [in intensional.examples.traversable_stack]
l:73 [in intensional.heap_lang.array]
l:77 [in intensional.heap_lang.array]
l:8 [in intensional.heap_lang.lifting]
l:84 [in intensional.heap_lang.array]
l:88 [in intensional.heap_lang.lifting]
l:88 [in intensional.heap_lang.proofmode]
l:9 [in intensional.heap_lang.locations]
l:9 [in intensional.examples.stack_impl]
l:91 [in intensional.heap_lang.array]
l:96 [in intensional.heap_lang.proofmode]
l:98 [in intensional.heap_lang.array]

M

mx:200 [in intensional.heap_lang.lang]
m':155 [in intensional.examples.linearizability]
m:134 [in intensional.examples.linearizability]
m:144 [in intensional.examples.linearizability]
m:150 [in intensional.examples.linearizability]
m:154 [in intensional.examples.linearizability]
M:165 [in intensional.examples.linearizability]
M:203 [in intensional.examples.linearizability]
M:215 [in intensional.examples.linearizability]
M:228 [in intensional.examples.linearizability]
m:24 [in intensional.examples.file]
m:30 [in intensional.examples.file]
m:35 [in intensional.examples.file]
m:44 [in intensional.examples.file]
m:54 [in intensional.heap_lang.adequacy]

N

next_impl:72 [in intensional.examples.iterator]
next:35 [in intensional.examples.iterator]
N':127 [in intensional.examples.linearizability]
N':240 [in intensional.examples.linearizability]
n0:58 [in intensional.examples.iterator]
n1:208 [in intensional.heap_lang.lang]
n2:209 [in intensional.heap_lang.lang]
n:109 [in intensional.heap_lang.lang]
n:11 [in intensional.heap_lang.lifting]
n:113 [in intensional.heap_lang.lang]
n:117 [in intensional.heap_lang.lang]
n:121 [in intensional.heap_lang.lang]
N:126 [in intensional.examples.linearizability]
n:2 [in intensional.heap_lang.lifting]
N:213 [in intensional.heap_lang.lifting]
N:219 [in intensional.heap_lang.lifting]
N:23 [in intensional.heap_lang.adequacy]
n:233 [in intensional.heap_lang.lifting]
n:238 [in intensional.heap_lang.lifting]
N:239 [in intensional.examples.linearizability]
n:245 [in intensional.heap_lang.lifting]
n:247 [in intensional.heap_lang.lang]
n:25 [in intensional.examples.file]
n:251 [in intensional.heap_lang.lifting]
n:29 [in intensional.heap_lang.proofmode]
n:29 [in intensional.examples.file]
n:3 [in intensional.heap_lang.lang]
n:308 [in intensional.heap_lang.lang]
n:32 [in intensional.examples.file]
n:34 [in intensional.examples.file]
n:365 [in intensional.heap_lang.lang]
n:37 [in intensional.examples.file]
N:39 [in intensional.heap_lang.adequacy]
n:39 [in intensional.examples.file]
N:40 [in intensional.examples.stack]
n:40 [in intensional.heap_lang.proofmode]
N:46 [in intensional.heap_lang.lifting]
N:48 [in intensional.examples.well_bracketed]
n:49 [in intensional.heap_lang.array]
n:54 [in intensional.heap_lang.array]
N:54 [in intensional.examples.file]
N:55 [in intensional.examples.stack]
n:60 [in intensional.heap_lang.array]
N:64 [in intensional.examples.traversable_stack]
N:65 [in intensional.examples.iterator]
n:66 [in intensional.heap_lang.array]
N:66 [in intensional.examples.file]
N:67 [in intensional.examples.well_bracketed]
n:7 [in intensional.heap_lang.lifting]
n:72 [in intensional.heap_lang.array]
n:74 [in intensional.heap_lang.lifting]
n:75 [in intensional.examples.iterator]
N:80 [in intensional.examples.traversable_stack]
n:82 [in intensional.examples.iterator]
N:85 [in intensional.heap_lang.lifting]
n:89 [in intensional.heap_lang.lifting]
N:89 [in intensional.examples.iterator]

O

off:101 [in intensional.heap_lang.array]
off:106 [in intensional.heap_lang.array]
off:112 [in intensional.heap_lang.array]
off:119 [in intensional.heap_lang.array]
off:126 [in intensional.heap_lang.array]
off:132 [in intensional.heap_lang.array]
off:140 [in intensional.heap_lang.array]
off:149 [in intensional.heap_lang.array]
off:157 [in intensional.heap_lang.array]
off:165 [in intensional.heap_lang.array]
off:174 [in intensional.heap_lang.array]
off:184 [in intensional.heap_lang.array]
off:193 [in intensional.heap_lang.array]
off:200 [in intensional.heap_lang.array]
off:207 [in intensional.heap_lang.array]
off:215 [in intensional.heap_lang.array]
off:223 [in intensional.heap_lang.array]
off:42 [in intensional.heap_lang.array]
off:79 [in intensional.heap_lang.array]
off:8 [in intensional.heap_lang.locations]
off:86 [in intensional.heap_lang.array]
off:94 [in intensional.heap_lang.array]
open_impl:57 [in intensional.examples.file]
open:5 [in intensional.examples.file]
op_impl:132 [in intensional.examples.linearizability]
op_impl:52 [in intensional.examples.well_bracketed]
op:111 [in intensional.heap_lang.lang]
op:115 [in intensional.heap_lang.lang]
op:118 [in intensional.heap_lang.lifting]
op:119 [in intensional.heap_lang.lang]
op:121 [in intensional.heap_lang.lifting]
op:123 [in intensional.heap_lang.lang]
op:15 [in intensional.examples.well_bracketed]
op:161 [in intensional.heap_lang.lang]
op:162 [in intensional.heap_lang.lang]
op:164 [in intensional.heap_lang.lang]
op:184 [in intensional.heap_lang.lifting]
op:187 [in intensional.heap_lang.lifting]
op:203 [in intensional.heap_lang.lang]
op:207 [in intensional.heap_lang.lang]
op:211 [in intensional.heap_lang.lang]
op:215 [in intensional.heap_lang.lang]
op:220 [in intensional.heap_lang.lang]
op:23 [in intensional.examples.linearizability]
op:23 [in intensional.heap_lang.lang]
op:25 [in intensional.heap_lang.lang]
op:277 [in intensional.heap_lang.lang]
op:281 [in intensional.heap_lang.lang]

P

Pinit_impl:130 [in intensional.examples.linearizability]
pop_impl:67 [in intensional.examples.traversable_stack]
pop_impl:43 [in intensional.examples.stack]
pop:17 [in intensional.examples.traversable_stack]
pop:17 [in intensional.examples.stack]
push_impl:66 [in intensional.examples.traversable_stack]
push_impl:42 [in intensional.examples.stack]
push:10 [in intensional.examples.traversable_stack]
push:10 [in intensional.examples.stack]
pvs':344 [in intensional.heap_lang.lifting]
pvs':350 [in intensional.heap_lang.lifting]
pvs':359 [in intensional.heap_lang.lifting]
pvs':370 [in intensional.heap_lang.lifting]
pvs:320 [in intensional.heap_lang.lifting]
pvs:342 [in intensional.heap_lang.lifting]
pvs:348 [in intensional.heap_lang.lifting]
pvs:355 [in intensional.heap_lang.lifting]
pvs:364 [in intensional.heap_lang.lifting]
P0:18 [in intensional.examples.file]
P0:19 [in intensional.examples.linearizability]
P0:20 [in intensional.examples.well_bracketed]
P0:24 [in intensional.examples.stack]
P0:241 [in intensional.examples.linearizability]
P0:3 [in intensional.examples.traversable_stack]
P0:3 [in intensional.examples.stack]
P0:34 [in intensional.examples.traversable_stack]
P0:40 [in intensional.examples.iterator]
P0:42 [in intensional.heap_lang.adequacy]
P0:48 [in intensional.examples.linearizability]
P0:50 [in intensional.examples.stack]
P0:56 [in intensional.examples.stack]
P0:67 [in intensional.examples.file]
P0:68 [in intensional.examples.well_bracketed]
P0:73 [in intensional.examples.traversable_stack]
P0:81 [in intensional.examples.traversable_stack]
P0:90 [in intensional.examples.iterator]
P:13 [in intensional.examples.stdpp_extra]
p:25 [in intensional.examples.stack_impl]
P:250 [in intensional.examples.linearizability]
p:30 [in intensional.examples.traversable_stack]
p:321 [in intensional.heap_lang.lifting]
p:324 [in intensional.heap_lang.lifting]
p:330 [in intensional.heap_lang.lang]
p:331 [in intensional.heap_lang.lang]
p:340 [in intensional.heap_lang.lifting]
p:347 [in intensional.heap_lang.lifting]
p:354 [in intensional.heap_lang.lifting]
p:363 [in intensional.heap_lang.lifting]
p:369 [in intensional.heap_lang.lang]
P:53 [in intensional.heap_lang.adequacy]
p:6 [in intensional.heap_lang.locations]
P:6 [in intensional.examples.well_bracketed]
P:64 [in intensional.examples.stack]
p:7 [in intensional.heap_lang.lang]
P:7 [in intensional.examples.stdpp_extra]
p:74 [in intensional.examples.traversable_stack]
p:75 [in intensional.examples.traversable_stack]
P:75 [in intensional.examples.file]
P:76 [in intensional.examples.well_bracketed]
P:89 [in intensional.examples.traversable_stack]
P:98 [in intensional.examples.iterator]

Q

q:104 [in intensional.heap_lang.proofmode]
q:11 [in intensional.heap_lang.array]
q:113 [in intensional.heap_lang.proofmode]
q:15 [in intensional.heap_lang.array]
q:163 [in intensional.heap_lang.proofmode]
q:164 [in intensional.heap_lang.array]
q:17 [in intensional.heap_lang.array]
q:173 [in intensional.heap_lang.array]
q:174 [in intensional.heap_lang.proofmode]
q:182 [in intensional.heap_lang.array]
q:19 [in intensional.heap_lang.array]
q:191 [in intensional.heap_lang.array]
q:21 [in intensional.heap_lang.array]
q:23 [in intensional.heap_lang.array]
q:26 [in intensional.heap_lang.array]
q:265 [in intensional.heap_lang.lifting]
q:270 [in intensional.heap_lang.lifting]
q:285 [in intensional.heap_lang.lifting]
q:292 [in intensional.heap_lang.lifting]
q:30 [in intensional.heap_lang.array]
q:34 [in intensional.heap_lang.array]
q:365 [in intensional.heap_lang.lifting]
Q:38 [in intensional.heap_lang.array]
q:4 [in intensional.heap_lang.array]
q:40 [in intensional.heap_lang.array]
q:47 [in intensional.heap_lang.array]
Q:7 [in intensional.examples.well_bracketed]
q:78 [in intensional.heap_lang.array]
q:85 [in intensional.heap_lang.array]
q:92 [in intensional.heap_lang.array]
q:99 [in intensional.heap_lang.array]

R

read_impl:59 [in intensional.examples.file]
read:14 [in intensional.examples.file]
remove_impl:70 [in intensional.examples.iterator]
remove:20 [in intensional.examples.iterator]
R_impl:129 [in intensional.examples.linearizability]
r:16 [in intensional.heap_lang.locations]
R:17 [in intensional.examples.linearizability]
r:21 [in intensional.heap_lang.locations]
r:22 [in intensional.examples.linearizability]
r:24 [in intensional.heap_lang.locations]
r:30 [in intensional.examples.iterator]
r:343 [in intensional.heap_lang.lifting]
R:37 [in intensional.heap_lang.array]
R:50 [in intensional.examples.linearizability]
r:79 [in intensional.examples.iterator]

S

size_impl:68 [in intensional.examples.iterator]
size:5 [in intensional.examples.iterator]
stack_impl:65 [in intensional.examples.traversable_stack]
stack_impl:41 [in intensional.examples.stack]
Stack:16 [in intensional.examples.traversable_stack]
Stack:16 [in intensional.examples.stack]
Stack:24 [in intensional.examples.traversable_stack]
Stack:26 [in intensional.examples.stack]
Stack:36 [in intensional.examples.traversable_stack]
Stack:4 [in intensional.examples.traversable_stack]
Stack:4 [in intensional.examples.stack]
Stack:9 [in intensional.examples.traversable_stack]
Stack:9 [in intensional.examples.stack]
sz:100 [in intensional.heap_lang.array]
sz:118 [in intensional.heap_lang.array]
sz:125 [in intensional.heap_lang.array]
sz:148 [in intensional.heap_lang.array]
sz:156 [in intensional.heap_lang.array]
sz:183 [in intensional.heap_lang.array]
sz:192 [in intensional.heap_lang.array]
sz:214 [in intensional.heap_lang.array]
sz:222 [in intensional.heap_lang.array]
sz:93 [in intensional.heap_lang.array]
s':190 [in intensional.examples.linearizability]
s':210 [in intensional.examples.linearizability]
s':223 [in intensional.examples.linearizability]
s':28 [in intensional.examples.linearizability]
s':33 [in intensional.examples.linearizability]
s':35 [in intensional.examples.linearizability]
s':39 [in intensional.examples.linearizability]
s':41 [in intensional.examples.linearizability]
s':71 [in intensional.examples.linearizability]
s':87 [in intensional.examples.linearizability]
s0:69 [in intensional.examples.linearizability]
s:10 [in intensional.heap_lang.adequacy]
s:101 [in intensional.heap_lang.lifting]
s:103 [in intensional.heap_lang.array]
s:105 [in intensional.heap_lang.lifting]
s:108 [in intensional.heap_lang.lifting]
s:108 [in intensional.heap_lang.proofmode]
s:109 [in intensional.heap_lang.array]
s:110 [in intensional.heap_lang.lifting]
s:112 [in intensional.heap_lang.lifting]
s:115 [in intensional.heap_lang.array]
s:117 [in intensional.heap_lang.lifting]
s:118 [in intensional.heap_lang.proofmode]
s:12 [in intensional.examples.traversable_stack]
s:12 [in intensional.examples.stack]
s:120 [in intensional.heap_lang.lifting]
s:122 [in intensional.heap_lang.array]
s:124 [in intensional.heap_lang.lifting]
s:127 [in intensional.heap_lang.lifting]
s:127 [in intensional.heap_lang.proofmode]
s:129 [in intensional.heap_lang.array]
s:13 [in intensional.heap_lang.proofmode]
s:13 [in intensional.examples.stack_impl]
s:130 [in intensional.heap_lang.lifting]
s:132 [in intensional.heap_lang.lifting]
s:134 [in intensional.heap_lang.lifting]
s:136 [in intensional.heap_lang.lifting]
s:137 [in intensional.heap_lang.array]
s:137 [in intensional.heap_lang.proofmode]
s:139 [in intensional.heap_lang.lifting]
s:14 [in intensional.examples.stack_impl]
s:141 [in intensional.heap_lang.lifting]
s:144 [in intensional.heap_lang.lifting]
s:145 [in intensional.heap_lang.array]
s:147 [in intensional.heap_lang.proofmode]
s:148 [in intensional.heap_lang.lifting]
s:151 [in intensional.heap_lang.lifting]
s:153 [in intensional.heap_lang.lifting]
s:153 [in intensional.heap_lang.array]
s:155 [in intensional.heap_lang.lifting]
s:156 [in intensional.heap_lang.lifting]
s:158 [in intensional.heap_lang.proofmode]
s:161 [in intensional.heap_lang.array]
s:163 [in intensional.examples.linearizability]
s:169 [in intensional.heap_lang.proofmode]
s:17 [in intensional.examples.stack_impl]
s:170 [in intensional.heap_lang.array]
s:171 [in intensional.examples.linearizability]
s:173 [in intensional.examples.linearizability]
s:179 [in intensional.heap_lang.array]
s:181 [in intensional.heap_lang.proofmode]
s:184 [in intensional.examples.linearizability]
s:188 [in intensional.heap_lang.array]
s:189 [in intensional.examples.linearizability]
s:19 [in intensional.examples.traversable_stack]
s:19 [in intensional.examples.stack]
s:191 [in intensional.examples.linearizability]
s:191 [in intensional.heap_lang.proofmode]
s:192 [in intensional.examples.linearizability]
s:197 [in intensional.examples.linearizability]
s:197 [in intensional.heap_lang.array]
s:202 [in intensional.heap_lang.proofmode]
s:204 [in intensional.heap_lang.array]
s:209 [in intensional.heap_lang.lifting]
s:209 [in intensional.examples.linearizability]
s:21 [in intensional.examples.stack_impl]
s:211 [in intensional.heap_lang.array]
s:211 [in intensional.heap_lang.proofmode]
s:215 [in intensional.heap_lang.lifting]
s:219 [in intensional.heap_lang.array]
s:222 [in intensional.examples.linearizability]
s:223 [in intensional.heap_lang.lifting]
s:227 [in intensional.heap_lang.lifting]
s:23 [in intensional.heap_lang.proofmode]
s:242 [in intensional.heap_lang.lifting]
s:248 [in intensional.heap_lang.lifting]
s:25 [in intensional.heap_lang.adequacy]
s:254 [in intensional.heap_lang.lifting]
s:258 [in intensional.heap_lang.lifting]
s:262 [in intensional.heap_lang.lifting]
s:267 [in intensional.heap_lang.lifting]
s:27 [in intensional.examples.linearizability]
s:27 [in intensional.examples.traversable_stack]
s:272 [in intensional.heap_lang.lifting]
s:277 [in intensional.heap_lang.lifting]
s:282 [in intensional.heap_lang.lifting]
s:289 [in intensional.heap_lang.lifting]
s:296 [in intensional.heap_lang.lifting]
s:30 [in intensional.examples.linearizability]
s:302 [in intensional.heap_lang.lifting]
s:308 [in intensional.heap_lang.lifting]
s:31 [in intensional.examples.linearizability]
s:313 [in intensional.heap_lang.lifting]
s:318 [in intensional.heap_lang.lifting]
s:32 [in intensional.examples.linearizability]
s:336 [in intensional.heap_lang.lifting]
s:34 [in intensional.heap_lang.proofmode]
s:345 [in intensional.heap_lang.lifting]
s:351 [in intensional.heap_lang.lifting]
s:360 [in intensional.heap_lang.lifting]
s:37 [in intensional.examples.linearizability]
s:38 [in intensional.examples.linearizability]
s:4 [in intensional.heap_lang.proofmode]
s:43 [in intensional.examples.linearizability]
s:45 [in intensional.heap_lang.proofmode]
s:51 [in intensional.heap_lang.array]
s:52 [in intensional.heap_lang.proofmode]
s:57 [in intensional.heap_lang.array]
s:6 [in intensional.heap_lang.lang]
s:6 [in intensional.examples.traversable_stack]
s:6 [in intensional.examples.stack]
s:60 [in intensional.heap_lang.proofmode]
s:63 [in intensional.heap_lang.array]
s:68 [in intensional.examples.linearizability]
s:69 [in intensional.heap_lang.array]
s:70 [in intensional.examples.linearizability]
s:71 [in intensional.examples.traversable_stack]
s:71 [in intensional.heap_lang.proofmode]
s:75 [in intensional.heap_lang.array]
s:82 [in intensional.heap_lang.array]
s:82 [in intensional.heap_lang.proofmode]
s:89 [in intensional.heap_lang.array]
s:90 [in intensional.heap_lang.proofmode]
s:96 [in intensional.heap_lang.array]
s:99 [in intensional.heap_lang.proofmode]

T

tagst:138 [in intensional.examples.linearizability]
tag':11 [in intensional.examples.trace_helpers]
tag':14 [in intensional.examples.trace_helpers]
tag':17 [in intensional.examples.trace_helpers]
tag:1 [in intensional.examples.trace_helpers]
tag:10 [in intensional.examples.trace_helpers]
tag:102 [in intensional.examples.linearizability]
tag:13 [in intensional.examples.trace_helpers]
tag:135 [in intensional.examples.linearizability]
tag:145 [in intensional.examples.linearizability]
tag:151 [in intensional.examples.linearizability]
tag:156 [in intensional.examples.linearizability]
tag:16 [in intensional.examples.trace_helpers]
tag:199 [in intensional.examples.linearizability]
tag:20 [in intensional.examples.trace_helpers]
tag:201 [in intensional.examples.linearizability]
tag:214 [in intensional.examples.linearizability]
tag:221 [in intensional.heap_lang.lifting]
tag:222 [in intensional.heap_lang.lifting]
tag:226 [in intensional.examples.linearizability]
tag:343 [in intensional.heap_lang.lang]
tag:4 [in intensional.examples.trace_helpers]
tag:54 [in intensional.examples.linearizability]
tag:57 [in intensional.examples.linearizability]
tag:61 [in intensional.examples.linearizability]
tag:62 [in intensional.examples.iterator]
tag:72 [in intensional.examples.linearizability]
tag:77 [in intensional.examples.linearizability]
tag:78 [in intensional.examples.iterator]
tag:8 [in intensional.examples.trace_helpers]
tag:92 [in intensional.examples.linearizability]
tag:94 [in intensional.examples.linearizability]
tag:97 [in intensional.examples.linearizability]
tr:211 [in intensional.heap_lang.lifting]
tr:217 [in intensional.heap_lang.lifting]
ts:338 [in intensional.heap_lang.lang]
t_op:45 [in intensional.examples.well_bracketed]
t_op:41 [in intensional.examples.well_bracketed]
t_op:31 [in intensional.examples.well_bracketed]
t':34 [in intensional.examples.well_bracketed]
t':37 [in intensional.examples.well_bracketed]
t':40 [in intensional.examples.well_bracketed]
t':44 [in intensional.examples.well_bracketed]
t':55 [in intensional.examples.traversable_stack]
t':57 [in intensional.examples.iterator]
t':58 [in intensional.heap_lang.lifting]
t':62 [in intensional.heap_lang.lifting]
t':66 [in intensional.heap_lang.lifting]
t':86 [in intensional.examples.linearizability]
t':90 [in intensional.examples.linearizability]
t:101 [in intensional.examples.linearizability]
t:133 [in intensional.examples.linearizability]
t:143 [in intensional.examples.linearizability]
t:149 [in intensional.examples.linearizability]
t:158 [in intensional.examples.linearizability]
t:23 [in intensional.examples.trace_helpers]
t:23 [in intensional.examples.file]
t:254 [in intensional.heap_lang.lang]
t:27 [in intensional.examples.well_bracketed]
t:28 [in intensional.examples.stack]
t:28 [in intensional.examples.file]
t:29 [in intensional.heap_lang.adequacy]
t:30 [in intensional.examples.well_bracketed]
t:31 [in intensional.heap_lang.adequacy]
t:31 [in intensional.examples.file]
t:32 [in intensional.examples.stack]
t:32 [in intensional.heap_lang.adequacy]
t:33 [in intensional.heap_lang.lifting]
t:33 [in intensional.examples.well_bracketed]
t:33 [in intensional.examples.file]
t:34 [in intensional.examples.stack]
t:35 [in intensional.examples.stack]
t:35 [in intensional.examples.well_bracketed]
t:36 [in intensional.heap_lang.lifting]
t:36 [in intensional.examples.file]
t:38 [in intensional.examples.well_bracketed]
t:38 [in intensional.examples.file]
t:39 [in intensional.heap_lang.lifting]
t:41 [in intensional.examples.file]
t:42 [in intensional.heap_lang.lifting]
t:42 [in intensional.examples.well_bracketed]
t:42 [in intensional.examples.file]
t:45 [in intensional.examples.traversable_stack]
t:45 [in intensional.examples.file]
t:46 [in intensional.examples.traversable_stack]
t:46 [in intensional.examples.iterator]
t:46 [in intensional.examples.file]
t:47 [in intensional.examples.stack]
t:48 [in intensional.heap_lang.lifting]
t:48 [in intensional.examples.file]
t:49 [in intensional.examples.traversable_stack]
t:49 [in intensional.examples.file]
t:50 [in intensional.examples.file]
t:51 [in intensional.heap_lang.lifting]
t:51 [in intensional.examples.traversable_stack]
t:51 [in intensional.examples.iterator]
t:52 [in intensional.examples.iterator]
t:53 [in intensional.examples.traversable_stack]
t:53 [in intensional.examples.iterator]
t:53 [in intensional.examples.well_bracketed]
t:54 [in intensional.heap_lang.lifting]
t:54 [in intensional.examples.iterator]
t:55 [in intensional.examples.well_bracketed]
t:56 [in intensional.examples.linearizability]
t:56 [in intensional.examples.iterator]
t:57 [in intensional.heap_lang.lifting]
t:57 [in intensional.examples.well_bracketed]
t:59 [in intensional.examples.well_bracketed]
t:6 [in intensional.examples.trace_helpers]
t:60 [in intensional.examples.linearizability]
t:60 [in intensional.examples.file]
t:61 [in intensional.heap_lang.lifting]
t:61 [in intensional.examples.file]
t:64 [in intensional.examples.linearizability]
t:65 [in intensional.heap_lang.lifting]
t:69 [in intensional.heap_lang.lifting]
t:7 [in intensional.examples.trace_helpers]
t:72 [in intensional.examples.traversable_stack]
t:75 [in intensional.heap_lang.lifting]
t:75 [in intensional.examples.linearizability]
t:76 [in intensional.examples.linearizability]
t:76 [in intensional.examples.iterator]
t:79 [in intensional.heap_lang.lifting]
t:8 [in intensional.examples.stack_impl]
t:83 [in intensional.examples.iterator]
t:84 [in intensional.heap_lang.lifting]
t:85 [in intensional.examples.linearizability]
t:89 [in intensional.examples.linearizability]
t:91 [in intensional.examples.linearizability]
t:92 [in intensional.heap_lang.lifting]
t:93 [in intensional.examples.linearizability]
t:96 [in intensional.examples.linearizability]

U

unlocked_impl:50 [in intensional.examples.well_bracketed]
unlocked:14 [in intensional.examples.well_bracketed]
unlocked:23 [in intensional.examples.well_bracketed]
unlocked:4 [in intensional.examples.well_bracketed]
u:24 [in intensional.examples.trace_helpers]

V

vl:322 [in intensional.heap_lang.lang]
vl:72 [in intensional.heap_lang.lang]
vp:329 [in intensional.heap_lang.lifting]
vs:102 [in intensional.heap_lang.array]
vs:107 [in intensional.heap_lang.array]
vs:113 [in intensional.heap_lang.array]
vs:12 [in intensional.heap_lang.array]
vs:120 [in intensional.heap_lang.array]
vs:127 [in intensional.heap_lang.array]
vs:133 [in intensional.heap_lang.array]
vs:14 [in intensional.heap_lang.array]
vs:141 [in intensional.heap_lang.array]
vs:150 [in intensional.heap_lang.array]
vs:158 [in intensional.heap_lang.array]
vs:166 [in intensional.heap_lang.array]
vs:175 [in intensional.heap_lang.array]
vs:18 [in intensional.heap_lang.array]
vs:185 [in intensional.heap_lang.array]
vs:194 [in intensional.heap_lang.array]
vs:201 [in intensional.heap_lang.array]
vs:208 [in intensional.heap_lang.array]
vs:216 [in intensional.heap_lang.array]
vs:224 [in intensional.heap_lang.array]
vs:232 [in intensional.heap_lang.lifting]
vs:232 [in intensional.heap_lang.lang]
vs:238 [in intensional.heap_lang.lang]
vs:244 [in intensional.heap_lang.lang]
vs:27 [in intensional.heap_lang.array]
vs:32 [in intensional.heap_lang.array]
vs:36 [in intensional.heap_lang.array]
vs:41 [in intensional.heap_lang.array]
vs:5 [in intensional.heap_lang.array]
vs:80 [in intensional.heap_lang.array]
vs:87 [in intensional.heap_lang.array]
vs:95 [in intensional.heap_lang.array]
vt:330 [in intensional.heap_lang.lifting]
v':104 [in intensional.examples.linearizability]
v':110 [in intensional.examples.linearizability]
v':124 [in intensional.heap_lang.proofmode]
v':133 [in intensional.heap_lang.proofmode]
v':134 [in intensional.heap_lang.array]
v':142 [in intensional.examples.linearizability]
v':142 [in intensional.heap_lang.array]
v':148 [in intensional.examples.linearizability]
v':186 [in intensional.heap_lang.lifting]
v':190 [in intensional.heap_lang.lifting]
v':213 [in intensional.examples.linearizability]
v':225 [in intensional.examples.linearizability]
v':275 [in intensional.heap_lang.lifting]
v':279 [in intensional.heap_lang.lang]
v':280 [in intensional.heap_lang.lifting]
v':284 [in intensional.heap_lang.lang]
v':286 [in intensional.heap_lang.lifting]
v':293 [in intensional.heap_lang.lifting]
v':301 [in intensional.heap_lang.lifting]
v':307 [in intensional.heap_lang.lifting]
v':366 [in intensional.heap_lang.lifting]
v':44 [in intensional.heap_lang.array]
v':59 [in intensional.examples.linearizability]
v':63 [in intensional.examples.linearizability]
v':74 [in intensional.examples.linearizability]
v':79 [in intensional.examples.linearizability]
v':99 [in intensional.examples.linearizability]
v0:145 [in intensional.heap_lang.lifting]
v0:167 [in intensional.heap_lang.array]
v0:176 [in intensional.heap_lang.array]
v1:106 [in intensional.heap_lang.lifting]
v1:115 [in intensional.heap_lang.lifting]
v1:122 [in intensional.heap_lang.lifting]
v1:125 [in intensional.heap_lang.lifting]
v1:135 [in intensional.heap_lang.array]
v1:142 [in intensional.heap_lang.lifting]
v1:143 [in intensional.heap_lang.array]
v1:143 [in intensional.heap_lang.proofmode]
v1:146 [in intensional.heap_lang.lifting]
v1:149 [in intensional.heap_lang.lifting]
v1:151 [in intensional.heap_lang.array]
v1:153 [in intensional.heap_lang.proofmode]
v1:158 [in intensional.heap_lang.lifting]
v1:159 [in intensional.heap_lang.array]
v1:165 [in intensional.heap_lang.proofmode]
v1:168 [in intensional.heap_lang.array]
v1:174 [in intensional.heap_lang.lifting]
v1:176 [in intensional.heap_lang.lang]
v1:176 [in intensional.heap_lang.proofmode]
v1:177 [in intensional.heap_lang.array]
v1:181 [in intensional.heap_lang.lifting]
v1:185 [in intensional.heap_lang.lang]
v1:186 [in intensional.heap_lang.array]
v1:187 [in intensional.heap_lang.proofmode]
v1:188 [in intensional.heap_lang.lifting]
v1:191 [in intensional.heap_lang.lifting]
v1:195 [in intensional.heap_lang.array]
v1:197 [in intensional.heap_lang.lifting]
v1:197 [in intensional.heap_lang.proofmode]
v1:199 [in intensional.heap_lang.lifting]
v1:221 [in intensional.heap_lang.lang]
v1:264 [in intensional.heap_lang.lang]
v1:282 [in intensional.heap_lang.lang]
v1:287 [in intensional.heap_lang.lifting]
v1:292 [in intensional.heap_lang.lang]
v1:294 [in intensional.heap_lang.lifting]
v1:295 [in intensional.heap_lang.lang]
v1:299 [in intensional.heap_lang.lifting]
v1:305 [in intensional.heap_lang.lifting]
v1:320 [in intensional.heap_lang.lang]
v1:356 [in intensional.heap_lang.lifting]
v1:367 [in intensional.heap_lang.lifting]
v1:393 [in intensional.heap_lang.lang]
v1:60 [in intensional.heap_lang.lang]
v1:73 [in intensional.heap_lang.lang]
v1:83 [in intensional.heap_lang.lang]
v1:93 [in intensional.heap_lang.lang]
v2:107 [in intensional.heap_lang.lifting]
v2:116 [in intensional.heap_lang.lifting]
v2:123 [in intensional.heap_lang.lifting]
v2:129 [in intensional.heap_lang.lifting]
v2:136 [in intensional.heap_lang.array]
v2:143 [in intensional.heap_lang.lifting]
v2:144 [in intensional.heap_lang.array]
v2:144 [in intensional.heap_lang.proofmode]
v2:147 [in intensional.heap_lang.lifting]
v2:150 [in intensional.heap_lang.lifting]
v2:152 [in intensional.heap_lang.array]
v2:154 [in intensional.heap_lang.proofmode]
v2:159 [in intensional.heap_lang.lifting]
v2:159 [in intensional.heap_lang.lang]
v2:160 [in intensional.heap_lang.array]
v2:163 [in intensional.heap_lang.lang]
v2:166 [in intensional.heap_lang.proofmode]
v2:168 [in intensional.heap_lang.lang]
v2:169 [in intensional.heap_lang.array]
v2:172 [in intensional.heap_lang.lang]
v2:174 [in intensional.heap_lang.lang]
v2:175 [in intensional.heap_lang.lifting]
v2:177 [in intensional.heap_lang.lang]
v2:177 [in intensional.heap_lang.proofmode]
v2:178 [in intensional.heap_lang.array]
v2:179 [in intensional.heap_lang.lang]
v2:182 [in intensional.heap_lang.lifting]
v2:182 [in intensional.heap_lang.lang]
v2:186 [in intensional.heap_lang.lang]
v2:187 [in intensional.heap_lang.array]
v2:188 [in intensional.heap_lang.lang]
v2:188 [in intensional.heap_lang.proofmode]
v2:189 [in intensional.heap_lang.lifting]
v2:192 [in intensional.heap_lang.lifting]
v2:196 [in intensional.heap_lang.array]
v2:198 [in intensional.heap_lang.lifting]
v2:198 [in intensional.heap_lang.proofmode]
v2:200 [in intensional.heap_lang.lifting]
v2:217 [in intensional.heap_lang.lang]
v2:222 [in intensional.heap_lang.lang]
v2:265 [in intensional.heap_lang.lang]
v2:274 [in intensional.heap_lang.lang]
v2:283 [in intensional.heap_lang.lang]
v2:288 [in intensional.heap_lang.lifting]
v2:293 [in intensional.heap_lang.lang]
v2:295 [in intensional.heap_lang.lifting]
v2:296 [in intensional.heap_lang.lang]
v2:300 [in intensional.heap_lang.lifting]
v2:306 [in intensional.heap_lang.lifting]
v2:321 [in intensional.heap_lang.lang]
v2:357 [in intensional.heap_lang.lifting]
v2:368 [in intensional.heap_lang.lifting]
v2:394 [in intensional.heap_lang.lang]
v2:61 [in intensional.heap_lang.lang]
v2:84 [in intensional.heap_lang.lang]
v2:94 [in intensional.heap_lang.lang]
v:10 [in intensional.examples.stack_impl]
v:100 [in intensional.heap_lang.lifting]
v:100 [in intensional.examples.linearizability]
v:100 [in intensional.examples.iterator]
v:103 [in intensional.examples.linearizability]
v:105 [in intensional.examples.linearizability]
v:105 [in intensional.heap_lang.proofmode]
v:108 [in intensional.examples.linearizability]
v:108 [in intensional.heap_lang.array]
v:109 [in intensional.heap_lang.lifting]
v:109 [in intensional.examples.linearizability]
v:111 [in intensional.heap_lang.lifting]
v:114 [in intensional.heap_lang.array]
v:114 [in intensional.heap_lang.proofmode]
v:119 [in intensional.heap_lang.lifting]
v:12 [in intensional.examples.trace_helpers]
v:121 [in intensional.heap_lang.array]
v:123 [in intensional.heap_lang.proofmode]
v:126 [in intensional.heap_lang.lang]
v:128 [in intensional.heap_lang.array]
v:131 [in intensional.heap_lang.lifting]
v:132 [in intensional.heap_lang.lang]
v:132 [in intensional.heap_lang.proofmode]
v:133 [in intensional.heap_lang.lifting]
v:137 [in intensional.heap_lang.lifting]
v:138 [in intensional.heap_lang.lang]
v:14 [in intensional.heap_lang.adequacy]
v:140 [in intensional.heap_lang.lifting]
v:141 [in intensional.examples.linearizability]
v:142 [in intensional.heap_lang.proofmode]
v:144 [in intensional.heap_lang.lang]
v:147 [in intensional.examples.linearizability]
v:15 [in intensional.examples.trace_helpers]
v:15 [in intensional.examples.file]
v:150 [in intensional.heap_lang.lang]
v:152 [in intensional.heap_lang.lifting]
v:152 [in intensional.heap_lang.proofmode]
v:154 [in intensional.heap_lang.lifting]
v:154 [in intensional.heap_lang.lang]
v:16 [in intensional.heap_lang.lang]
v:16 [in intensional.heap_lang.adequacy]
v:160 [in intensional.heap_lang.lifting]
v:161 [in intensional.heap_lang.lifting]
v:162 [in intensional.heap_lang.lifting]
v:164 [in intensional.heap_lang.proofmode]
v:175 [in intensional.heap_lang.proofmode]
v:176 [in intensional.heap_lang.lifting]
v:177 [in intensional.heap_lang.lifting]
v:18 [in intensional.examples.trace_helpers]
v:185 [in intensional.heap_lang.lifting]
v:186 [in intensional.heap_lang.proofmode]
v:19 [in intensional.examples.trace_helpers]
v:19 [in intensional.examples.stack_impl]
v:196 [in intensional.heap_lang.lang]
v:196 [in intensional.heap_lang.proofmode]
v:2 [in intensional.examples.trace_helpers]
v:20 [in intensional.examples.traversable_stack]
v:20 [in intensional.examples.stack]
v:200 [in intensional.examples.linearizability]
v:201 [in intensional.heap_lang.lifting]
v:201 [in intensional.heap_lang.lang]
v:202 [in intensional.examples.linearizability]
v:204 [in intensional.heap_lang.lifting]
v:204 [in intensional.heap_lang.lang]
v:21 [in intensional.examples.trace_helpers]
v:212 [in intensional.heap_lang.lifting]
v:212 [in intensional.examples.linearizability]
v:216 [in intensional.examples.linearizability]
v:217 [in intensional.examples.linearizability]
v:218 [in intensional.heap_lang.lifting]
v:22 [in intensional.examples.trace_helpers]
v:224 [in intensional.examples.linearizability]
v:227 [in intensional.heap_lang.lang]
v:230 [in intensional.examples.linearizability]
v:231 [in intensional.examples.linearizability]
v:236 [in intensional.heap_lang.lang]
v:237 [in intensional.heap_lang.lifting]
v:24 [in intensional.heap_lang.array]
v:240 [in intensional.heap_lang.lifting]
v:244 [in intensional.heap_lang.lifting]
v:248 [in intensional.heap_lang.lang]
v:250 [in intensional.heap_lang.lifting]
v:252 [in intensional.heap_lang.lang]
v:253 [in intensional.examples.linearizability]
v:256 [in intensional.heap_lang.lifting]
v:260 [in intensional.heap_lang.lifting]
v:266 [in intensional.heap_lang.lifting]
v:267 [in intensional.heap_lang.lang]
v:269 [in intensional.heap_lang.lang]
v:27 [in intensional.examples.file]
v:271 [in intensional.heap_lang.lifting]
v:276 [in intensional.heap_lang.lifting]
v:278 [in intensional.heap_lang.lang]
v:281 [in intensional.heap_lang.lifting]
v:298 [in intensional.heap_lang.lang]
v:30 [in intensional.examples.stack]
v:302 [in intensional.heap_lang.lang]
v:309 [in intensional.heap_lang.lang]
v:31 [in intensional.heap_lang.array]
v:314 [in intensional.heap_lang.lang]
v:317 [in intensional.heap_lang.lang]
v:325 [in intensional.heap_lang.lifting]
v:33 [in intensional.examples.stack]
v:332 [in intensional.heap_lang.lang]
v:339 [in intensional.heap_lang.lang]
v:341 [in intensional.heap_lang.lifting]
v:341 [in intensional.heap_lang.lang]
v:349 [in intensional.heap_lang.lifting]
v:35 [in intensional.heap_lang.array]
v:358 [in intensional.heap_lang.lifting]
v:36 [in intensional.examples.stack]
v:364 [in intensional.heap_lang.lang]
v:369 [in intensional.heap_lang.lifting]
v:372 [in intensional.heap_lang.lang]
v:4 [in intensional.examples.stack_impl]
v:43 [in intensional.heap_lang.array]
v:43 [in intensional.examples.file]
v:46 [in intensional.examples.stack]
v:47 [in intensional.examples.file]
v:48 [in intensional.heap_lang.array]
v:48 [in intensional.heap_lang.proofmode]
v:5 [in intensional.examples.trace_helpers]
v:51 [in intensional.examples.file]
v:53 [in intensional.heap_lang.array]
v:55 [in intensional.examples.linearizability]
v:55 [in intensional.heap_lang.proofmode]
v:55 [in intensional.heap_lang.adequacy]
v:58 [in intensional.examples.linearizability]
v:59 [in intensional.heap_lang.array]
v:62 [in intensional.examples.linearizability]
v:62 [in intensional.heap_lang.lang]
v:63 [in intensional.heap_lang.lang]
v:65 [in intensional.heap_lang.array]
v:65 [in intensional.heap_lang.proofmode]
v:66 [in intensional.examples.stack]
v:68 [in intensional.heap_lang.lang]
v:7 [in intensional.heap_lang.array]
v:71 [in intensional.heap_lang.array]
v:71 [in intensional.heap_lang.lang]
v:73 [in intensional.examples.linearizability]
v:76 [in intensional.heap_lang.proofmode]
v:77 [in intensional.examples.file]
v:78 [in intensional.examples.linearizability]
v:78 [in intensional.heap_lang.lang]
v:78 [in intensional.examples.well_bracketed]
v:80 [in intensional.examples.linearizability]
v:80 [in intensional.heap_lang.lang]
v:81 [in intensional.heap_lang.array]
v:82 [in intensional.examples.linearizability]
v:86 [in intensional.heap_lang.proofmode]
v:88 [in intensional.heap_lang.array]
v:9 [in intensional.examples.trace_helpers]
v:91 [in intensional.examples.traversable_stack]
v:94 [in intensional.heap_lang.proofmode]
v:95 [in intensional.examples.linearizability]
v:98 [in intensional.heap_lang.lifting]
v:98 [in intensional.examples.linearizability]
v:99 [in intensional.heap_lang.lifting]

W

withRes_impl:51 [in intensional.examples.well_bracketed]
withRes:5 [in intensional.examples.well_bracketed]
ws:28 [in intensional.heap_lang.array]
w:138 [in intensional.heap_lang.lifting]
w:239 [in intensional.heap_lang.lang]
w:326 [in intensional.heap_lang.lifting]
w:327 [in intensional.heap_lang.lifting]
w:335 [in intensional.heap_lang.lang]
w:373 [in intensional.heap_lang.lang]
w:374 [in intensional.heap_lang.lang]
w:378 [in intensional.heap_lang.lang]

X

x:10 [in intensional.examples.well_bracketed]
x:103 [in intensional.heap_lang.lifting]
x:11 [in intensional.examples.tactics]
x:11 [in intensional.examples.iris_extra]
x:11 [in intensional.examples.stdpp_extra]
x:114 [in intensional.heap_lang.lifting]
x:12 [in intensional.examples.linearizability]
x:13 [in intensional.examples.traversable_stack]
x:13 [in intensional.examples.stack]
x:14 [in intensional.examples.iterator]
x:14 [in intensional.examples.stdpp_extra]
x:15 [in intensional.examples.tactics]
x:15 [in intensional.examples.stack_impl]
x:16 [in intensional.examples.well_bracketed]
x:164 [in intensional.heap_lang.lifting]
x:167 [in intensional.examples.linearizability]
x:169 [in intensional.heap_lang.lifting]
x:17 [in intensional.examples.iris_extra]
x:17 [in intensional.heap_lang.lang]
x:172 [in intensional.heap_lang.lifting]
x:179 [in intensional.heap_lang.lifting]
x:19 [in intensional.heap_lang.lang]
x:195 [in intensional.heap_lang.lang]
x:21 [in intensional.examples.tactics]
x:22 [in intensional.examples.iterator]
x:25 [in intensional.examples.linearizability]
x:26 [in intensional.examples.stack_impl]
x:261 [in intensional.heap_lang.lang]
x:272 [in intensional.heap_lang.lang]
x:3 [in intensional.examples.stdpp_extra]
x:31 [in intensional.examples.tactics]
x:31 [in intensional.examples.traversable_stack]
x:37 [in intensional.examples.iterator]
x:40 [in intensional.examples.traversable_stack]
x:43 [in intensional.examples.traversable_stack]
x:47 [in intensional.examples.traversable_stack]
x:48 [in intensional.examples.stack]
x:5 [in intensional.examples.iris_extra]
x:55 [in intensional.examples.iterator]
x:58 [in intensional.heap_lang.lang]
x:60 [in intensional.examples.iterator]
x:60 [in intensional.examples.well_bracketed]
x:7 [in intensional.examples.iterator]
x:73 [in intensional.examples.iterator]
x:8 [in intensional.examples.stdpp_extra]
x:80 [in intensional.examples.iterator]

Y

y':29 [in intensional.examples.linearizability]
y':34 [in intensional.examples.linearizability]
y':36 [in intensional.examples.linearizability]
y':40 [in intensional.examples.linearizability]
y':42 [in intensional.examples.linearizability]
y:12 [in intensional.examples.iris_extra]
y:17 [in intensional.examples.well_bracketed]
y:22 [in intensional.examples.tactics]
y:26 [in intensional.examples.linearizability]
y:32 [in intensional.examples.tactics]
y:4 [in intensional.examples.stdpp_extra]
y:6 [in intensional.examples.iris_extra]
y:61 [in intensional.examples.well_bracketed]
y:74 [in intensional.examples.iterator]
y:81 [in intensional.examples.iterator]
y:9 [in intensional.examples.well_bracketed]

Z

z1:207 [in intensional.heap_lang.proofmode]
z1:216 [in intensional.heap_lang.proofmode]
z2:208 [in intensional.heap_lang.proofmode]
z2:217 [in intensional.heap_lang.proofmode]
z:13 [in intensional.examples.iris_extra]
z:33 [in intensional.examples.tactics]
z:62 [in intensional.examples.well_bracketed]

other

Δ':117 [in intensional.heap_lang.proofmode]
Δ':136 [in intensional.heap_lang.proofmode]
Δ':157 [in intensional.heap_lang.proofmode]
Δ':180 [in intensional.heap_lang.proofmode]
Δ':201 [in intensional.heap_lang.proofmode]
Δ':22 [in intensional.heap_lang.proofmode]
Δ':81 [in intensional.heap_lang.proofmode]
Δ':98 [in intensional.heap_lang.proofmode]
Δ:107 [in intensional.heap_lang.proofmode]
Δ:116 [in intensional.heap_lang.proofmode]
Δ:12 [in intensional.heap_lang.proofmode]
Δ:126 [in intensional.heap_lang.proofmode]
Δ:135 [in intensional.heap_lang.proofmode]
Δ:146 [in intensional.heap_lang.proofmode]
Δ:156 [in intensional.heap_lang.proofmode]
Δ:168 [in intensional.heap_lang.proofmode]
Δ:179 [in intensional.heap_lang.proofmode]
Δ:190 [in intensional.heap_lang.proofmode]
Δ:200 [in intensional.heap_lang.proofmode]
Δ:21 [in intensional.heap_lang.proofmode]
Δ:210 [in intensional.heap_lang.proofmode]
Δ:3 [in intensional.heap_lang.proofmode]
Δ:33 [in intensional.heap_lang.proofmode]
Δ:44 [in intensional.heap_lang.proofmode]
Δ:51 [in intensional.heap_lang.proofmode]
Δ:59 [in intensional.heap_lang.proofmode]
Δ:70 [in intensional.heap_lang.proofmode]
Δ:80 [in intensional.heap_lang.proofmode]
Δ:89 [in intensional.heap_lang.proofmode]
Δ:97 [in intensional.heap_lang.proofmode]
Σ:1 [in intensional.heap_lang.array]
Σ:1 [in intensional.examples.traversable_stack]
Σ:1 [in intensional.examples.stack]
Σ:1 [in intensional.heap_lang.proofmode]
Σ:1 [in intensional.heap_lang.adequacy]
Σ:1 [in intensional.examples.iterator]
Σ:1 [in intensional.examples.well_bracketed]
Σ:1 [in intensional.examples.stack_impl]
Σ:1 [in intensional.examples.file]
Σ:10 [in intensional.heap_lang.proofmode]
Σ:101 [in intensional.examples.iterator]
Σ:11 [in intensional.examples.well_bracketed]
Σ:11 [in intensional.examples.file]
Σ:112 [in intensional.examples.linearizability]
Σ:121 [in intensional.examples.linearizability]
Σ:14 [in intensional.heap_lang.lifting]
Σ:14 [in intensional.examples.linearizability]
Σ:14 [in intensional.examples.traversable_stack]
Σ:14 [in intensional.examples.stack]
Σ:15 [in intensional.examples.iris_extra]
Σ:16 [in intensional.examples.iterator]
Σ:16 [in intensional.examples.file]
Σ:18 [in intensional.examples.well_bracketed]
Σ:19 [in intensional.heap_lang.proofmode]
Σ:2 [in intensional.examples.iris_extra]
Σ:20 [in intensional.heap_lang.lifting]
Σ:207 [in intensional.heap_lang.lifting]
Σ:21 [in intensional.heap_lang.adequacy]
Σ:22 [in intensional.examples.traversable_stack]
Σ:22 [in intensional.examples.stack]
Σ:234 [in intensional.examples.linearizability]
Σ:24 [in intensional.examples.iterator]
Σ:248 [in intensional.examples.linearizability]
Σ:25 [in intensional.heap_lang.lifting]
Σ:254 [in intensional.examples.linearizability]
Σ:31 [in intensional.heap_lang.lifting]
Σ:31 [in intensional.heap_lang.proofmode]
Σ:31 [in intensional.examples.iterator]
Σ:32 [in intensional.examples.traversable_stack]
Σ:34 [in intensional.heap_lang.lifting]
Σ:37 [in intensional.heap_lang.adequacy]
Σ:38 [in intensional.examples.stack]
Σ:38 [in intensional.examples.iterator]
Σ:40 [in intensional.heap_lang.lifting]
Σ:42 [in intensional.heap_lang.proofmode]
Σ:43 [in intensional.heap_lang.lifting]
Σ:46 [in intensional.examples.linearizability]
Σ:46 [in intensional.examples.well_bracketed]
Σ:49 [in intensional.heap_lang.lifting]
Σ:49 [in intensional.heap_lang.proofmode]
Σ:52 [in intensional.heap_lang.lifting]
Σ:52 [in intensional.examples.file]
Σ:53 [in intensional.examples.stack]
Σ:55 [in intensional.heap_lang.lifting]
Σ:56 [in intensional.heap_lang.proofmode]
Σ:59 [in intensional.heap_lang.lifting]
Σ:6 [in intensional.examples.linearizability]
Σ:6 [in intensional.examples.file]
Σ:62 [in intensional.examples.traversable_stack]
Σ:62 [in intensional.examples.stack]
Σ:63 [in intensional.heap_lang.lifting]
Σ:63 [in intensional.examples.iterator]
Σ:64 [in intensional.examples.file]
Σ:65 [in intensional.examples.well_bracketed]
Σ:67 [in intensional.heap_lang.lifting]
Σ:67 [in intensional.examples.stack]
Σ:67 [in intensional.heap_lang.proofmode]
Σ:7 [in intensional.examples.traversable_stack]
Σ:7 [in intensional.examples.stack]
Σ:7 [in intensional.heap_lang.adequacy]
Σ:71 [in intensional.heap_lang.lifting]
Σ:73 [in intensional.examples.file]
Σ:74 [in intensional.examples.well_bracketed]
Σ:77 [in intensional.heap_lang.lifting]
Σ:78 [in intensional.examples.traversable_stack]
Σ:78 [in intensional.heap_lang.proofmode]
Σ:78 [in intensional.examples.file]
Σ:79 [in intensional.examples.well_bracketed]
Σ:8 [in intensional.examples.iris_extra]
Σ:8 [in intensional.heap_lang.array]
Σ:8 [in intensional.heap_lang.adequacy]
Σ:8 [in intensional.examples.iterator]
Σ:81 [in intensional.heap_lang.lifting]
Σ:87 [in intensional.examples.traversable_stack]
Σ:87 [in intensional.examples.iterator]
Σ:90 [in intensional.heap_lang.lifting]
Σ:92 [in intensional.examples.traversable_stack]
Σ:94 [in intensional.heap_lang.lifting]
Σ:96 [in intensional.examples.iterator]
Φ:106 [in intensional.heap_lang.proofmode]
Φ:115 [in intensional.heap_lang.proofmode]
Φ:125 [in intensional.heap_lang.proofmode]
Φ:134 [in intensional.heap_lang.proofmode]
Φ:145 [in intensional.heap_lang.proofmode]
Φ:15 [in intensional.heap_lang.proofmode]
Φ:155 [in intensional.heap_lang.proofmode]
Φ:167 [in intensional.heap_lang.proofmode]
Φ:178 [in intensional.heap_lang.proofmode]
Φ:189 [in intensional.heap_lang.proofmode]
Φ:199 [in intensional.heap_lang.proofmode]
Φ:209 [in intensional.heap_lang.proofmode]
Φ:218 [in intensional.heap_lang.proofmode]
Φ:226 [in intensional.heap_lang.lifting]
Φ:230 [in intensional.heap_lang.lifting]
Φ:30 [in intensional.heap_lang.proofmode]
Φ:339 [in intensional.heap_lang.lifting]
Φ:41 [in intensional.heap_lang.proofmode]
Φ:41 [in intensional.heap_lang.adequacy]
Φ:47 [in intensional.heap_lang.proofmode]
Φ:54 [in intensional.heap_lang.proofmode]
Φ:6 [in intensional.heap_lang.proofmode]
Φ:62 [in intensional.heap_lang.proofmode]
Φ:73 [in intensional.heap_lang.proofmode]
Φ:87 [in intensional.heap_lang.proofmode]
Φ:95 [in intensional.heap_lang.proofmode]
α:198 [in intensional.examples.linearizability]
α:229 [in intensional.examples.linearizability]
β:164 [in intensional.examples.linearizability]
γe':183 [in intensional.examples.linearizability]
γe:162 [in intensional.examples.linearizability]
γe:170 [in intensional.examples.linearizability]
γe:176 [in intensional.examples.linearizability]
γe:180 [in intensional.examples.linearizability]
γe:188 [in intensional.examples.linearizability]
γe:196 [in intensional.examples.linearizability]
γe:208 [in intensional.examples.linearizability]
γe:221 [in intensional.examples.linearizability]
γi':181 [in intensional.examples.linearizability]
γi:160 [in intensional.examples.linearizability]
γi:168 [in intensional.examples.linearizability]
γi:174 [in intensional.examples.linearizability]
γi:178 [in intensional.examples.linearizability]
γi:186 [in intensional.examples.linearizability]
γi:194 [in intensional.examples.linearizability]
γi:206 [in intensional.examples.linearizability]
γi:219 [in intensional.examples.linearizability]
γs':182 [in intensional.examples.linearizability]
γs:137 [in intensional.examples.linearizability]
γs:146 [in intensional.examples.linearizability]
γs:152 [in intensional.examples.linearizability]
γs:161 [in intensional.examples.linearizability]
γs:169 [in intensional.examples.linearizability]
γs:175 [in intensional.examples.linearizability]
γs:179 [in intensional.examples.linearizability]
γs:187 [in intensional.examples.linearizability]
γs:195 [in intensional.examples.linearizability]
γs:207 [in intensional.examples.linearizability]
γs:220 [in intensional.examples.linearizability]
γtag:204 [in intensional.examples.linearizability]
γtag:211 [in intensional.examples.linearizability]
γtag:227 [in intensional.examples.linearizability]
γ:10 [in intensional.examples.iris_extra]
γ:11 [in intensional.examples.linearizability]
γ:153 [in intensional.examples.linearizability]
γ:159 [in intensional.examples.linearizability]
γ:166 [in intensional.examples.linearizability]
γ:172 [in intensional.examples.linearizability]
γ:177 [in intensional.examples.linearizability]
γ:18 [in intensional.examples.iris_extra]
γ:185 [in intensional.examples.linearizability]
γ:193 [in intensional.examples.linearizability]
γ:205 [in intensional.examples.linearizability]
γ:21 [in intensional.examples.linearizability]
γ:218 [in intensional.examples.linearizability]
γ:24 [in intensional.examples.linearizability]
γ:4 [in intensional.examples.iris_extra]
κs:18 [in intensional.heap_lang.adequacy]
κs:20 [in intensional.heap_lang.adequacy]
κs:337 [in intensional.heap_lang.lang]
κs:34 [in intensional.heap_lang.adequacy]
κs:36 [in intensional.heap_lang.adequacy]
κs:377 [in intensional.heap_lang.lang]
κs:97 [in intensional.heap_lang.lifting]
κ':388 [in intensional.heap_lang.lang]
κ:332 [in intensional.heap_lang.lifting]
κ:349 [in intensional.heap_lang.lang]
κ:356 [in intensional.heap_lang.lang]
κ:383 [in intensional.heap_lang.lang]
σ':246 [in intensional.examples.linearizability]
σ':28 [in intensional.heap_lang.adequacy]
σ':336 [in intensional.heap_lang.lang]
σ':48 [in intensional.heap_lang.adequacy]
σ':60 [in intensional.examples.stack]
σ':71 [in intensional.examples.file]
σ':72 [in intensional.examples.well_bracketed]
σ':85 [in intensional.examples.traversable_stack]
σ':94 [in intensional.examples.iterator]
σ1':387 [in intensional.heap_lang.lang]
σ1:331 [in intensional.heap_lang.lifting]
σ1:348 [in intensional.heap_lang.lang]
σ1:355 [in intensional.heap_lang.lang]
σ1:376 [in intensional.heap_lang.lang]
σ1:382 [in intensional.heap_lang.lang]
σ2':390 [in intensional.heap_lang.lang]
σ2:334 [in intensional.heap_lang.lifting]
σ2:351 [in intensional.heap_lang.lang]
σ2:358 [in intensional.heap_lang.lang]
σ2:379 [in intensional.heap_lang.lang]
σ2:385 [in intensional.heap_lang.lang]
σ:12 [in intensional.heap_lang.adequacy]
σ:17 [in intensional.heap_lang.adequacy]
σ:19 [in intensional.heap_lang.adequacy]
σ:226 [in intensional.heap_lang.lang]
σ:228 [in intensional.heap_lang.lang]
σ:230 [in intensional.heap_lang.lang]
σ:249 [in intensional.heap_lang.lang]
σ:253 [in intensional.heap_lang.lang]
σ:263 [in intensional.heap_lang.lang]
σ:266 [in intensional.heap_lang.lang]
σ:268 [in intensional.heap_lang.lang]
σ:27 [in intensional.heap_lang.adequacy]
σ:270 [in intensional.heap_lang.lang]
σ:276 [in intensional.heap_lang.lang]
σ:280 [in intensional.heap_lang.lang]
σ:285 [in intensional.heap_lang.lang]
σ:288 [in intensional.heap_lang.lang]
σ:291 [in intensional.heap_lang.lang]
σ:294 [in intensional.heap_lang.lang]
σ:297 [in intensional.heap_lang.lang]
σ:301 [in intensional.heap_lang.lang]
σ:305 [in intensional.heap_lang.lang]
σ:307 [in intensional.heap_lang.lang]
σ:310 [in intensional.heap_lang.lang]
σ:315 [in intensional.heap_lang.lang]
σ:318 [in intensional.heap_lang.lang]
σ:323 [in intensional.heap_lang.lifting]
σ:323 [in intensional.heap_lang.lang]
σ:328 [in intensional.heap_lang.lang]
σ:329 [in intensional.heap_lang.lang]
σ:33 [in intensional.heap_lang.adequacy]
σ:334 [in intensional.heap_lang.lang]
σ:340 [in intensional.heap_lang.lang]
σ:342 [in intensional.heap_lang.lang]
σ:35 [in intensional.heap_lang.adequacy]
σ:366 [in intensional.heap_lang.lang]
σ:368 [in intensional.heap_lang.lang]
σ:395 [in intensional.heap_lang.lang]
σ:47 [in intensional.heap_lang.adequacy]
σ:96 [in intensional.heap_lang.lifting]
φ:13 [in intensional.heap_lang.adequacy]
φ:28 [in intensional.heap_lang.proofmode]
φ:39 [in intensional.heap_lang.proofmode]
ℓ:11 [in intensional.examples.stack_impl]
ℓ:7 [in intensional.examples.stack_impl]

Module Index

H

heap_lang [in intensional.heap_lang.lang]

S

Stack_impl [in intensional.examples.stack_impl]

W

Wrap [in intensional.examples.linearizability]
Wrap [in intensional.examples.traversable_stack]
Wrap [in intensional.examples.stack]
Wrap [in intensional.examples.iterator]
Wrap [in intensional.examples.well_bracketed]
Wrap [in intensional.examples.file]

Library Index

A

adequacy
array

F

file

I

iris_extra
iterator

L

lang
lifting
linearizability
locations

N

notation

P

proofmode

S

stack
stack_impl
stdpp_extra

T

tactics
tactics
trace_helpers
traversable_stack

W

well_bracketed

Lemma Index

A

alloc_hist [in intensional.heap_lang.lifting]
array_cons [in intensional.heap_lang.array]
array_app [in intensional.heap_lang.array]
array_singleton [in intensional.heap_lang.array]
array_nil [in intensional.heap_lang.array]

C

check_tag_iff [in intensional.examples.trace_helpers]
check_tag_in_tags [in intensional.examples.trace_helpers]

E

excl_auth_alloc [in intensional.examples.iris_extra]
excl_auth_upd [in intensional.examples.iris_extra]
excl_auth_eq [in intensional.examples.iris_extra]

F

file_trace_nil [in intensional.examples.file]
file_trace_read [in intensional.examples.file]
file_trace_close [in intensional.examples.file]
file_trace_open [in intensional.examples.file]
filter_check_single_tag_eq [in intensional.examples.trace_helpers]
filter_check_single_tag_neq [in intensional.examples.trace_helpers]
filter_Forall_id [in intensional.examples.stdpp_extra]
filter_is_nil [in intensional.examples.stdpp_extra]
fresh_locs_fresh [in intensional.heap_lang.locations]
fresh_tag_nocheck [in intensional.examples.trace_helpers]

G

gmap_of_trace_valid [in intensional.heap_lang.lifting]
gmap_of_trace_hist_valid_prefix [in intensional.heap_lang.lifting]
gmap_of_trace_dom [in intensional.heap_lang.lifting]
gmap_of_trace_snoc [in intensional.heap_lang.lifting]
good_trace_nil [in intensional.examples.traversable_stack]
good_stack_trace_pop [in intensional.examples.stack]
good_stack_trace_pop_nil [in intensional.examples.stack]
good_stack_trace_push [in intensional.examples.stack]
good_stack_trace_nil [in intensional.examples.stack]

H

head_step_to_val [in intensional.heap_lang.lang]
heap_array_to_seq_mapsto [in intensional.heap_lang.lifting]
heap_array_to_seq_meta [in intensional.heap_lang.lifting]
heap_lang.heap_lang_mixin [in intensional.heap_lang.lang]
heap_lang.new_proph_id_fresh [in intensional.heap_lang.lang]
heap_lang.alloc_fresh [in intensional.heap_lang.lang]
heap_lang.fill_item_no_val_inj [in intensional.heap_lang.lang]
heap_lang.head_ctx_step_val [in intensional.heap_lang.lang]
heap_lang.val_head_stuck [in intensional.heap_lang.lang]
heap_lang.fill_item_val [in intensional.heap_lang.lang]
heap_lang.state_init_heap_singleton [in intensional.heap_lang.lang]
heap_lang.heap_array_map_disjoint [in intensional.heap_lang.lang]
heap_lang.heap_array_lookup [in intensional.heap_lang.lang]
heap_lang.heap_array_singleton [in intensional.heap_lang.lang]
heap_lang.of_to_val [in intensional.heap_lang.lang]
heap_lang.to_of_val [in intensional.heap_lang.lang]
hist_trace_is_prefix [in intensional.heap_lang.lifting]

I

irreducible_resolve [in intensional.heap_lang.lang]
isopen_read_last [in intensional.examples.file]
isopen_open_last [in intensional.examples.file]
isopen_open' [in intensional.examples.file]
isopen_open [in intensional.examples.file]
iterator_trace_next [in intensional.examples.iterator]
iterator_trace_iterator [in intensional.examples.iterator]
iterator_trace_remove [in intensional.examples.iterator]
iterator_trace_add [in intensional.examples.iterator]
iterator_trace_size [in intensional.examples.iterator]
iterator_trace_nil [in intensional.examples.iterator]

L

linearizable_nil [in intensional.examples.linearizability]
linearization_fresh_tag_call_ret [in intensional.examples.linearizability]
loc_add_0 [in intensional.heap_lang.locations]
loc_add_assoc [in intensional.heap_lang.locations]
lookup_snoc_Some [in intensional.examples.stdpp_extra]

M

mapsto_seq_array [in intensional.heap_lang.array]
module_invariance [in intensional.heap_lang.adequacy]

N

noclose_read_last [in intensional.examples.file]
noclose_open_last [in intensional.examples.file]
noclose_open [in intensional.examples.file]
not_check_tag_iff [in intensional.examples.trace_helpers]

P

per_tag_linearized_add_ret [in intensional.examples.linearizability]
per_tag_linearized_add_lin [in intensional.examples.linearizability]
per_tag_linearized_add_call [in intensional.examples.linearizability]
per_tag_linearized_prefix [in intensional.examples.linearizability]
prim_step_to_val_is_head_step [in intensional.heap_lang.lang]

R

resolve_reducible [in intensional.heap_lang.lifting]

S

Stack_impl.traversable_correct [in intensional.examples.stack_impl]
Stack_impl.correct [in intensional.examples.stack_impl]
Stack_impl.foreach_correct [in intensional.examples.stack_impl]
Stack_impl.pop_correct [in intensional.examples.stack_impl]
Stack_impl.push_correct [in intensional.examples.stack_impl]
Stack_impl.create_correct [in intensional.examples.stack_impl]
step_resolve [in intensional.heap_lang.lifting]

T

tac_twp_faa [in intensional.heap_lang.proofmode]
tac_wp_faa [in intensional.heap_lang.proofmode]
tac_twp_cmpxchg_suc [in intensional.heap_lang.proofmode]
tac_wp_cmpxchg_suc [in intensional.heap_lang.proofmode]
tac_twp_cmpxchg_fail [in intensional.heap_lang.proofmode]
tac_wp_cmpxchg_fail [in intensional.heap_lang.proofmode]
tac_twp_cmpxchg [in intensional.heap_lang.proofmode]
tac_wp_cmpxchg [in intensional.heap_lang.proofmode]
tac_twp_store [in intensional.heap_lang.proofmode]
tac_wp_store [in intensional.heap_lang.proofmode]
tac_twp_load [in intensional.heap_lang.proofmode]
tac_wp_load [in intensional.heap_lang.proofmode]
tac_twp_alloc [in intensional.heap_lang.proofmode]
tac_wp_alloc [in intensional.heap_lang.proofmode]
tac_twp_bind [in intensional.heap_lang.proofmode]
tac_wp_bind [in intensional.heap_lang.proofmode]
tac_twp_value [in intensional.heap_lang.proofmode]
tac_wp_value [in intensional.heap_lang.proofmode]
tac_twp_pure [in intensional.heap_lang.proofmode]
tac_wp_pure [in intensional.heap_lang.proofmode]
tac_twp_expr_eval [in intensional.heap_lang.proofmode]
tac_wp_expr_eval [in intensional.heap_lang.proofmode]
tags_app [in intensional.examples.trace_helpers]
to_val_fill_some [in intensional.heap_lang.lang]
trace_auth_init [in intensional.heap_lang.lifting]
trace_is_inv [in intensional.heap_lang.lifting]
trace_add_event [in intensional.heap_lang.lifting]
trace_half_frag_agree [in intensional.heap_lang.lifting]
trace_agree [in intensional.heap_lang.lifting]
trace_auth_half_frag_agree [in intensional.heap_lang.lifting]
traversal_trace_prefix [in intensional.examples.traversable_stack]
traversal_trace_app [in intensional.examples.traversable_stack]
twp_faa [in intensional.heap_lang.lifting]
twp_cmpxchg_suc [in intensional.heap_lang.lifting]
twp_cmpxchg_fail [in intensional.heap_lang.lifting]
twp_store [in intensional.heap_lang.lifting]
twp_load [in intensional.heap_lang.lifting]
twp_alloc [in intensional.heap_lang.lifting]
twp_allocN_seq [in intensional.heap_lang.lifting]
twp_fork [in intensional.heap_lang.lifting]
twp_faa_offset_vec [in intensional.heap_lang.array]
twp_faa_offset [in intensional.heap_lang.array]
twp_cmpxchg_fail_offset_vec [in intensional.heap_lang.array]
twp_cmpxchg_fail_offset [in intensional.heap_lang.array]
twp_cmpxchg_suc_offset_vec [in intensional.heap_lang.array]
twp_cmpxchg_suc_offset [in intensional.heap_lang.array]
twp_store_offset_vec [in intensional.heap_lang.array]
twp_store_offset [in intensional.heap_lang.array]
twp_load_offset_vec [in intensional.heap_lang.array]
twp_load_offset [in intensional.heap_lang.array]
twp_allocN_vec [in intensional.heap_lang.array]
twp_allocN [in intensional.heap_lang.array]

U

update_array [in intensional.heap_lang.array]

W

wp_resolve_cmpxchg_fail [in intensional.heap_lang.lifting]
wp_resolve_cmpxchg_suc [in intensional.heap_lang.lifting]
wp_resolve_proph [in intensional.heap_lang.lifting]
wp_resolve [in intensional.heap_lang.lifting]
wp_new_proph [in intensional.heap_lang.lifting]
wp_faa [in intensional.heap_lang.lifting]
wp_cmpxchg_suc [in intensional.heap_lang.lifting]
wp_cmpxchg_fail [in intensional.heap_lang.lifting]
wp_store [in intensional.heap_lang.lifting]
wp_load [in intensional.heap_lang.lifting]
wp_alloc [in intensional.heap_lang.lifting]
wp_allocN_seq [in intensional.heap_lang.lifting]
wp_fork [in intensional.heap_lang.lifting]
wp_fresh [in intensional.heap_lang.lifting]
wp_emit [in intensional.heap_lang.lifting]
wp_faa_offset_vec [in intensional.heap_lang.array]
wp_faa_offset [in intensional.heap_lang.array]
wp_cmpxchg_fail_offset_vec [in intensional.heap_lang.array]
wp_cmpxchg_fail_offset [in intensional.heap_lang.array]
wp_cmpxchg_suc_offset_vec [in intensional.heap_lang.array]
wp_cmpxchg_suc_offset [in intensional.heap_lang.array]
wp_store_offset_vec [in intensional.heap_lang.array]
wp_store_offset [in intensional.heap_lang.array]
wp_load_offset_vec [in intensional.heap_lang.array]
wp_load_offset [in intensional.heap_lang.array]
wp_allocN_vec [in intensional.heap_lang.array]
wp_allocN [in intensional.heap_lang.array]
wrap_lib_correct [in intensional.examples.linearizability]
wrap_stacklib_correct [in intensional.examples.traversable_stack]
wrap_stacklib_correct [in intensional.examples.stack]
wrap_iterlib_correct [in intensional.examples.iterator]
wrap_bfilelib_correct [in intensional.examples.well_bracketed]
wrap_filelib_correct [in intensional.examples.file]
Wrap.add_correct [in intensional.examples.iterator]
Wrap.close_correct [in intensional.examples.file]
Wrap.correct [in intensional.examples.linearizability]
Wrap.correct [in intensional.examples.traversable_stack]
Wrap.correct [in intensional.examples.stack]
Wrap.correct [in intensional.examples.iterator]
Wrap.correct [in intensional.examples.well_bracketed]
Wrap.correct [in intensional.examples.file]
Wrap.create_correct [in intensional.examples.traversable_stack]
Wrap.create_correct [in intensional.examples.stack]
Wrap.foreach_correct [in intensional.examples.traversable_stack]
Wrap.init_correct [in intensional.examples.linearizability]
Wrap.iterator_correct [in intensional.examples.iterator]
Wrap.main_inv_state_eq [in intensional.examples.linearizability]
Wrap.main_inv_gnames_eq [in intensional.examples.linearizability]
Wrap.next_correct [in intensional.examples.iterator]
Wrap.open_correct [in intensional.examples.file]
Wrap.op_correct [in intensional.examples.linearizability]
Wrap.op_correct_ret [in intensional.examples.linearizability]
Wrap.op_correct_lin [in intensional.examples.linearizability]
Wrap.op_correct_call [in intensional.examples.linearizability]
Wrap.op_correct [in intensional.examples.well_bracketed]
Wrap.pop_correct [in intensional.examples.traversable_stack]
Wrap.pop_correct [in intensional.examples.stack]
Wrap.push_correct [in intensional.examples.traversable_stack]
Wrap.push_correct [in intensional.examples.stack]
Wrap.read_correct [in intensional.examples.file]
Wrap.remove_correct [in intensional.examples.iterator]
Wrap.size_correct [in intensional.examples.iterator]
Wrap.tags_state_lookup_sub [in intensional.examples.linearizability]
Wrap.tags_state_lin_to_ret [in intensional.examples.linearizability]
Wrap.tags_state_call_to_lin [in intensional.examples.linearizability]
Wrap.withRes_correct [in intensional.examples.well_bracketed]

Constructor Index

A

AlreadyKnown [in intensional.examples.tactics]
as_recv [in intensional.heap_lang.lifting]

G

good_trace_for_foreach [in intensional.examples.traversable_stack]
good_trace_for_pop [in intensional.examples.traversable_stack]
good_trace_for_pop_nil [in intensional.examples.traversable_stack]
good_trace_for_push [in intensional.examples.traversable_stack]
good_trace_for_nil [in intensional.examples.traversable_stack]

H

HeapG [in intensional.heap_lang.lifting]
HeapPreG [in intensional.heap_lang.adequacy]
heap_lang.FreshS [in intensional.heap_lang.lang]
heap_lang.EmitS [in intensional.heap_lang.lang]
heap_lang.ResolveS [in intensional.heap_lang.lang]
heap_lang.NewProphS [in intensional.heap_lang.lang]
heap_lang.FaaS [in intensional.heap_lang.lang]
heap_lang.CmpXchgS [in intensional.heap_lang.lang]
heap_lang.StoreS [in intensional.heap_lang.lang]
heap_lang.LoadS [in intensional.heap_lang.lang]
heap_lang.AllocNS [in intensional.heap_lang.lang]
heap_lang.ForkS [in intensional.heap_lang.lang]
heap_lang.CaseRS [in intensional.heap_lang.lang]
heap_lang.CaseLS [in intensional.heap_lang.lang]
heap_lang.SndS [in intensional.heap_lang.lang]
heap_lang.FstS [in intensional.heap_lang.lang]
heap_lang.IfFalseS [in intensional.heap_lang.lang]
heap_lang.IfTrueS [in intensional.heap_lang.lang]
heap_lang.BinOpS [in intensional.heap_lang.lang]
heap_lang.UnOpS [in intensional.heap_lang.lang]
heap_lang.BetaS [in intensional.heap_lang.lang]
heap_lang.InjRS [in intensional.heap_lang.lang]
heap_lang.InjLS [in intensional.heap_lang.lang]
heap_lang.PairS [in intensional.heap_lang.lang]
heap_lang.RecS [in intensional.heap_lang.lang]
heap_lang.FreshCtx [in intensional.heap_lang.lang]
heap_lang.EmitCtx [in intensional.heap_lang.lang]
heap_lang.ResolveRCtx [in intensional.heap_lang.lang]
heap_lang.ResolveMCtx [in intensional.heap_lang.lang]
heap_lang.ResolveLCtx [in intensional.heap_lang.lang]
heap_lang.FaaRCtx [in intensional.heap_lang.lang]
heap_lang.FaaLCtx [in intensional.heap_lang.lang]
heap_lang.CmpXchgRCtx [in intensional.heap_lang.lang]
heap_lang.CmpXchgMCtx [in intensional.heap_lang.lang]
heap_lang.CmpXchgLCtx [in intensional.heap_lang.lang]
heap_lang.StoreRCtx [in intensional.heap_lang.lang]
heap_lang.StoreLCtx [in intensional.heap_lang.lang]
heap_lang.LoadCtx [in intensional.heap_lang.lang]
heap_lang.AllocNRCtx [in intensional.heap_lang.lang]
heap_lang.AllocNLCtx [in intensional.heap_lang.lang]
heap_lang.CaseCtx [in intensional.heap_lang.lang]
heap_lang.InjRCtx [in intensional.heap_lang.lang]
heap_lang.InjLCtx [in intensional.heap_lang.lang]
heap_lang.SndCtx [in intensional.heap_lang.lang]
heap_lang.FstCtx [in intensional.heap_lang.lang]
heap_lang.PairRCtx [in intensional.heap_lang.lang]
heap_lang.PairLCtx [in intensional.heap_lang.lang]
heap_lang.IfCtx [in intensional.heap_lang.lang]
heap_lang.BinOpRCtx [in intensional.heap_lang.lang]
heap_lang.BinOpLCtx [in intensional.heap_lang.lang]
heap_lang.UnOpCtx [in intensional.heap_lang.lang]
heap_lang.AppRCtx [in intensional.heap_lang.lang]
heap_lang.AppLCtx [in intensional.heap_lang.lang]
heap_lang.InjRV [in intensional.heap_lang.lang]
heap_lang.InjLV [in intensional.heap_lang.lang]
heap_lang.PairV [in intensional.heap_lang.lang]
heap_lang.RecV [in intensional.heap_lang.lang]
heap_lang.LitV [in intensional.heap_lang.lang]
heap_lang.Fresh [in intensional.heap_lang.lang]
heap_lang.Emit [in intensional.heap_lang.lang]
heap_lang.Resolve [in intensional.heap_lang.lang]
heap_lang.NewProph [in intensional.heap_lang.lang]
heap_lang.FAA [in intensional.heap_lang.lang]
heap_lang.CmpXchg [in intensional.heap_lang.lang]
heap_lang.Store [in intensional.heap_lang.lang]
heap_lang.Load [in intensional.heap_lang.lang]
heap_lang.AllocN [in intensional.heap_lang.lang]
heap_lang.Fork [in intensional.heap_lang.lang]
heap_lang.Case [in intensional.heap_lang.lang]
heap_lang.InjR [in intensional.heap_lang.lang]
heap_lang.InjL [in intensional.heap_lang.lang]
heap_lang.Snd [in intensional.heap_lang.lang]
heap_lang.Fst [in intensional.heap_lang.lang]
heap_lang.Pair [in intensional.heap_lang.lang]
heap_lang.If [in intensional.heap_lang.lang]
heap_lang.BinOp [in intensional.heap_lang.lang]
heap_lang.UnOp [in intensional.heap_lang.lang]
heap_lang.App [in intensional.heap_lang.lang]
heap_lang.Rec [in intensional.heap_lang.lang]
heap_lang.Var [in intensional.heap_lang.lang]
heap_lang.Val [in intensional.heap_lang.lang]
heap_lang.OffsetOp [in intensional.heap_lang.lang]
heap_lang.EqOp [in intensional.heap_lang.lang]
heap_lang.LtOp [in intensional.heap_lang.lang]
heap_lang.LeOp [in intensional.heap_lang.lang]
heap_lang.ShiftROp [in intensional.heap_lang.lang]
heap_lang.ShiftLOp [in intensional.heap_lang.lang]
heap_lang.XorOp [in intensional.heap_lang.lang]
heap_lang.OrOp [in intensional.heap_lang.lang]
heap_lang.AndOp [in intensional.heap_lang.lang]
heap_lang.RemOp [in intensional.heap_lang.lang]
heap_lang.QuotOp [in intensional.heap_lang.lang]
heap_lang.MultOp [in intensional.heap_lang.lang]
heap_lang.MinusOp [in intensional.heap_lang.lang]
heap_lang.PlusOp [in intensional.heap_lang.lang]
heap_lang.MinusUnOp [in intensional.heap_lang.lang]
heap_lang.NegOp [in intensional.heap_lang.lang]
heap_lang.LitProphecy [in intensional.heap_lang.lang]
heap_lang.LitTag [in intensional.heap_lang.lang]
heap_lang.LitLoc [in intensional.heap_lang.lang]
heap_lang.LitPoison [in intensional.heap_lang.lang]
heap_lang.LitUnit [in intensional.heap_lang.lang]
heap_lang.LitBool [in intensional.heap_lang.lang]
heap_lang.LitInt [in intensional.heap_lang.lang]

L

linearization_trace_ret [in intensional.examples.linearizability]
linearization_trace_lin [in intensional.examples.linearizability]
linearization_trace_call [in intensional.examples.linearizability]
linearization_trace_nil [in intensional.examples.linearizability]
linearized_sound_lin [in intensional.examples.linearizability]
linearized_sound_nil [in intensional.examples.linearizability]

O

op_trace_call [in intensional.examples.well_bracketed]
op_trace_nil [in intensional.examples.well_bracketed]

T

TraceG [in intensional.heap_lang.lifting]
TracePreG [in intensional.heap_lang.lifting]

W

withRes_trace_call [in intensional.examples.well_bracketed]
withRes_trace_nil [in intensional.examples.well_bracketed]
Wrap.AfterCall [in intensional.examples.linearizability]
Wrap.AfterLin [in intensional.examples.linearizability]
Wrap.Done [in intensional.examples.linearizability]

Projection Index

A

as_recv [in intensional.heap_lang.lifting]

F

f [in intensional.examples.linearizability]

H

heapG_traceG [in intensional.heap_lang.lifting]
heapG_proph_mapG [in intensional.heap_lang.lifting]
heapG_gen_heapG [in intensional.heap_lang.lifting]
heapG_invG [in intensional.heap_lang.lifting]
heap_lang.used_proph_id [in intensional.heap_lang.lang]
heap_lang.trace [in intensional.heap_lang.lang]
heap_lang.heap [in intensional.heap_lang.lang]
heap_preG_trace [in intensional.heap_lang.adequacy]
heap_preG_proph [in intensional.heap_lang.adequacy]
heap_preG_heap [in intensional.heap_lang.adequacy]
heap_preG_iris [in intensional.heap_lang.adequacy]

I

is_P_persistent [in intensional.examples.linearizability]
is_P [in intensional.examples.linearizability]

L

loc_car [in intensional.heap_lang.locations]

P

P_state [in intensional.examples.linearizability]

R

r [in intensional.examples.linearizability]

S

S [in intensional.examples.linearizability]
s_init [in intensional.examples.linearizability]

T

trace_preG_inG [in intensional.heap_lang.lifting]
trace_hist_preG_inG [in intensional.heap_lang.lifting]
trace_name [in intensional.heap_lang.lifting]
trace_inG [in intensional.heap_lang.lifting]
trace_hist_name [in intensional.heap_lang.lifting]
trace_hist_inG [in intensional.heap_lang.lifting]

W

Wrap.lin_tag_res_inG [in intensional.examples.linearizability]
Wrap.lin_tag_state_inG [in intensional.examples.linearizability]
Wrap.lin_gnames_inG [in intensional.examples.linearizability]
Wrap.lin_model_inG [in intensional.examples.linearizability]

Inductive Index

A

AsRecV [in intensional.heap_lang.lifting]

G

good_trace_for [in intensional.examples.traversable_stack]

H

heap_lang.head_step [in intensional.heap_lang.lang]
heap_lang.ectx_item [in intensional.heap_lang.lang]
heap_lang.val [in intensional.heap_lang.lang]
heap_lang.expr [in intensional.heap_lang.lang]
heap_lang.bin_op [in intensional.heap_lang.lang]
heap_lang.un_op [in intensional.heap_lang.lang]
heap_lang.base_lit [in intensional.heap_lang.lang]

L

Learnt [in intensional.examples.tactics]
linearization_trace [in intensional.examples.linearizability]
linearized_sound [in intensional.examples.linearizability]

O

op_trace [in intensional.examples.well_bracketed]

W

withRes_trace [in intensional.examples.well_bracketed]
Wrap.tag_state [in intensional.examples.linearizability]

Section Index

H

heap [in intensional.heap_lang.proofmode]

L

lifting [in intensional.heap_lang.lifting]
lifting [in intensional.heap_lang.array]

S

Specs [in intensional.examples.linearizability]
Stack_impl.S [in intensional.examples.stack_impl]

T

Trace [in intensional.examples.linearizability]
Trace [in intensional.examples.traversable_stack]
Trace [in intensional.examples.stack]
Trace [in intensional.examples.iterator]
Trace [in intensional.examples.well_bracketed]
Trace [in intensional.examples.file]

W

Wrap.S [in intensional.examples.linearizability]
Wrap.S [in intensional.examples.traversable_stack]
Wrap.S [in intensional.examples.stack]
Wrap.S [in intensional.examples.iterator]
Wrap.S [in intensional.examples.well_bracketed]
Wrap.S [in intensional.examples.file]

Instance Index

A

alloc_atomic [in intensional.heap_lang.lifting]
array_cons_frame [in intensional.heap_lang.array]
array_as_fractional [in intensional.heap_lang.array]
array_fractional [in intensional.heap_lang.array]
array_timeless [in intensional.heap_lang.array]
as_val_val [in intensional.heap_lang.lifting]

B

beta_atomic [in intensional.heap_lang.lifting]
binop_atomic [in intensional.heap_lang.lifting]

C

cmpxchg_atomic [in intensional.heap_lang.lifting]

E

emit_atomic [in intensional.heap_lang.lifting]

F

faa_atomic [in intensional.heap_lang.lifting]
fork_atomic [in intensional.heap_lang.lifting]
fresh_atomic [in intensional.heap_lang.lifting]
fst_atomic [in intensional.heap_lang.lifting]

H

heapG_irisG [in intensional.heap_lang.lifting]
heap_lang.fill_item_inj [in intensional.heap_lang.lang]
heap_lang.expr_inhabited [in intensional.heap_lang.lang]
heap_lang.val_inhabited [in intensional.heap_lang.lang]
heap_lang.state_inhabited [in intensional.heap_lang.lang]
heap_lang.val_countable [in intensional.heap_lang.lang]
heap_lang.expr_countable [in intensional.heap_lang.lang]
heap_lang.bin_op_countable [in intensional.heap_lang.lang]
heap_lang.un_op_finite [in intensional.heap_lang.lang]
heap_lang.base_lit_countable [in intensional.heap_lang.lang]
heap_lang.val_eq_dec [in intensional.heap_lang.lang]
heap_lang.expr_eq_dec [in intensional.heap_lang.lang]
heap_lang.bin_op_eq_dec [in intensional.heap_lang.lang]
heap_lang.un_op_eq_dec [in intensional.heap_lang.lang]
heap_lang.base_lit_eq_dec [in intensional.heap_lang.lang]
heap_lang.of_val_inj [in intensional.heap_lang.lang]
heap_lang.val_is_unboxed_dec [in intensional.heap_lang.lang]
heap_lang.lit_is_unboxed_dec [in intensional.heap_lang.lang]
hist_persistent [in intensional.heap_lang.lifting]

I

if_false_atomic [in intensional.heap_lang.lifting]
if_true_atomic [in intensional.heap_lang.lifting]
injl_atomic [in intensional.heap_lang.lifting]
injr_atomic [in intensional.heap_lang.lifting]
into_val_val [in intensional.heap_lang.lifting]

L

load_atomic [in intensional.heap_lang.lifting]
loc_add_inj [in intensional.heap_lang.locations]
loc_infinite [in intensional.heap_lang.locations]
loc_countable [in intensional.heap_lang.locations]
loc_inhabited [in intensional.heap_lang.locations]
loc_eq_decision [in intensional.heap_lang.locations]

N

new_proph_atomic [in intensional.heap_lang.lifting]

P

pair_atomic [in intensional.heap_lang.lifting]
pure_case_inr [in intensional.heap_lang.lifting]
pure_case_inl [in intensional.heap_lang.lifting]
pure_snd [in intensional.heap_lang.lifting]
pure_fst [in intensional.heap_lang.lifting]
pure_if_false [in intensional.heap_lang.lifting]
pure_if_true [in intensional.heap_lang.lifting]
pure_eqop [in intensional.heap_lang.lifting]
pure_binop [in intensional.heap_lang.lifting]
pure_unop [in intensional.heap_lang.lifting]
pure_beta [in intensional.heap_lang.lifting]
pure_injrc [in intensional.heap_lang.lifting]
pure_injlc [in intensional.heap_lang.lifting]
pure_pairc [in intensional.heap_lang.lifting]
pure_recc [in intensional.heap_lang.lifting]

R

rec_atomic [in intensional.heap_lang.lifting]
resolve_atomic [in intensional.heap_lang.lifting]

S

snd_atomic [in intensional.heap_lang.lifting]
store_atomic [in intensional.heap_lang.lifting]
subG_tracePreG [in intensional.heap_lang.lifting]
subG_heapPreG [in intensional.heap_lang.adequacy]

U

unop_atomic [in intensional.heap_lang.lifting]

W

Wrap.subG_linG [in intensional.examples.linearizability]

Abbreviation Index

A

Alloc [in intensional.heap_lang.notation]

C

CAS [in intensional.heap_lang.notation]

H

heap_lang.of_val [in intensional.heap_lang.lang]

L

Lam [in intensional.heap_lang.notation]
LamV [in intensional.heap_lang.notation]
Let [in intensional.heap_lang.notation]
LetCtx [in intensional.heap_lang.notation]

M

Match [in intensional.heap_lang.notation]

N

NONE [in intensional.heap_lang.notation]
NONEV [in intensional.heap_lang.notation]

R

ResolveProph [in intensional.heap_lang.notation]

S

Seq [in intensional.heap_lang.notation]
SeqCtx [in intensional.heap_lang.notation]
Skip [in intensional.heap_lang.notation]
SOME [in intensional.heap_lang.notation]
SOMEV [in intensional.heap_lang.notation]

T

trace [in intensional.examples.traversable_stack]

W

Wrap.SO [in intensional.examples.linearizability]

Definition Index

A

add_spec [in intensional.examples.iterator]
array [in intensional.heap_lang.array]
AsRecV_recv [in intensional.heap_lang.lifting]

B

bfilelibN [in intensional.examples.well_bracketed]
bfilelib_spec [in intensional.examples.well_bracketed]
bfile_trace [in intensional.examples.well_bracketed]

C

check_tag [in intensional.examples.trace_helpers]
close_spec [in intensional.examples.file]
create_spec [in intensional.examples.traversable_stack]
create_spec [in intensional.examples.stack]

E

empty_state [in intensional.examples.linearizability]
empty_state [in intensional.examples.traversable_stack]
empty_state [in intensional.examples.stack]
empty_state [in intensional.examples.iterator]
empty_state [in intensional.examples.well_bracketed]
empty_state [in intensional.examples.file]
eventO [in intensional.heap_lang.lifting]

F

filelibN [in intensional.examples.file]
filelib_spec [in intensional.examples.file]
file_trace [in intensional.examples.file]
foreach_spec [in intensional.examples.traversable_stack]
fresh_locs [in intensional.heap_lang.locations]

G

gmap_of_trace [in intensional.heap_lang.lifting]
good_trace [in intensional.examples.traversable_stack]
good_stack_trace [in intensional.examples.stack]

H

heap_lang [in intensional.heap_lang.lang]
heap_ectx_lang [in intensional.heap_lang.lang]
heap_ectxi_lang [in intensional.heap_lang.lang]
heap_lang.tags [in intensional.heap_lang.lang]
heap_lang.state_init_heap [in intensional.heap_lang.lang]
heap_lang.heap_array [in intensional.heap_lang.lang]
heap_lang.state_upd_used_proph_id [in intensional.heap_lang.lang]
heap_lang.state_add_event [in intensional.heap_lang.lang]
heap_lang.state_upd_heap [in intensional.heap_lang.lang]
heap_lang.bin_op_eval [in intensional.heap_lang.lang]
heap_lang.bin_op_eval_loc [in intensional.heap_lang.lang]
heap_lang.bin_op_eval_bool [in intensional.heap_lang.lang]
heap_lang.bin_op_eval_int [in intensional.heap_lang.lang]
heap_lang.un_op_eval [in intensional.heap_lang.lang]
heap_lang.subst' [in intensional.heap_lang.lang]
heap_lang.subst [in intensional.heap_lang.lang]
heap_lang.fill_item [in intensional.heap_lang.lang]
heap_lang.exprO [in intensional.heap_lang.lang]
heap_lang.valO [in intensional.heap_lang.lang]
heap_lang.locO [in intensional.heap_lang.lang]
heap_lang.stateO [in intensional.heap_lang.lang]
heap_lang.vals_compare_safe [in intensional.heap_lang.lang]
heap_lang.val_is_unboxed [in intensional.heap_lang.lang]
heap_lang.lit_is_unboxed [in intensional.heap_lang.lang]
heap_lang.to_val [in intensional.heap_lang.lang]
heap_lang.observation [in intensional.heap_lang.lang]
heap_lang.proph_id [in intensional.heap_lang.lang]
heap_invariance [in intensional.heap_lang.adequacy]
heap_adequacy [in intensional.heap_lang.adequacy]
heapΣ [in intensional.heap_lang.adequacy]
hist [in intensional.heap_lang.lifting]

I

init_spec [in intensional.examples.linearizability]
isopen [in intensional.examples.file]
is_lin [in intensional.examples.linearizability]
is_call_return [in intensional.examples.linearizability]
iterator_trace [in intensional.examples.iterator]
iterator_spec [in intensional.examples.iterator]
iterlibN [in intensional.examples.iterator]
iterlib_spec [in intensional.examples.iterator]

L

libN [in intensional.examples.linearizability]
lib_spec [in intensional.examples.linearizability]
linearizable [in intensional.examples.linearizability]
loc_add [in intensional.heap_lang.locations]

N

next_spec [in intensional.examples.iterator]
noclose [in intensional.examples.file]

O

open_spec [in intensional.examples.file]
op_spec [in intensional.examples.linearizability]
op_spec [in intensional.examples.well_bracketed]

P

per_tag_linearized [in intensional.examples.linearizability]
pop_spec [in intensional.examples.traversable_stack]
pop_spec [in intensional.examples.stack]
push_spec [in intensional.examples.traversable_stack]
push_spec [in intensional.examples.stack]

R

read_spec [in intensional.examples.file]
remove_spec [in intensional.examples.iterator]

S

size_spec [in intensional.examples.iterator]
stacklibN [in intensional.examples.traversable_stack]
stacklibN [in intensional.examples.stack]
stacklib_spec [in intensional.examples.traversable_stack]
stacklib_spec [in intensional.examples.stack]
Stack_impl.stack_val [in intensional.examples.stack_impl]
Stack_impl.list_val [in intensional.examples.stack_impl]
Stack_impl.foreach [in intensional.examples.stack_impl]
Stack_impl.pop [in intensional.examples.stack_impl]
Stack_impl.push [in intensional.examples.stack_impl]
Stack_impl.create [in intensional.examples.stack_impl]

T

traceO [in intensional.heap_lang.lifting]
trace_inv [in intensional.heap_lang.lifting]
trace_is [in intensional.heap_lang.lifting]
trace_half_frag [in intensional.heap_lang.lifting]
trace_auth [in intensional.heap_lang.lifting]
trace1 [in intensional.examples.well_bracketed]
trace2 [in intensional.examples.well_bracketed]
trace3 [in intensional.examples.well_bracketed]
traceΣ [in intensional.heap_lang.lifting]
traversal_trace [in intensional.examples.traversable_stack]

U

Unnamed_thm [in intensional.examples.tactics]
Unnamed_thm [in intensional.examples.tactics]
Unnamed_thm [in intensional.examples.tactics]
Unnamed_thm [in intensional.examples.tactics]
Unnamed_thm [in intensional.examples.tactics]

W

withRes_spec [in intensional.examples.well_bracketed]
wrapN [in intensional.examples.linearizability]
Wrap.add [in intensional.examples.iterator]
Wrap.close [in intensional.examples.file]
Wrap.Coll [in intensional.examples.iterator]
Wrap.create [in intensional.examples.traversable_stack]
Wrap.create [in intensional.examples.stack]
Wrap.foreach [in intensional.examples.traversable_stack]
Wrap.init [in intensional.examples.linearizability]
Wrap.isClosed [in intensional.examples.file]
Wrap.isOpen [in intensional.examples.file]
Wrap.is_P_wrap [in intensional.examples.linearizability]
Wrap.Iter [in intensional.examples.iterator]
Wrap.iterator [in intensional.examples.iterator]
Wrap.lib [in intensional.examples.linearizability]
Wrap.lib [in intensional.examples.traversable_stack]
Wrap.lib [in intensional.examples.stack]
Wrap.lib [in intensional.examples.iterator]
Wrap.lib [in intensional.examples.well_bracketed]
Wrap.lib [in intensional.examples.file]
Wrap.linΣ [in intensional.examples.linearizability]
Wrap.locked [in intensional.examples.well_bracketed]
Wrap.mainN [in intensional.examples.linearizability]
Wrap.main_inv [in intensional.examples.linearizability]
Wrap.next [in intensional.examples.iterator]
Wrap.op [in intensional.examples.linearizability]
Wrap.op [in intensional.examples.well_bracketed]
Wrap.open [in intensional.examples.file]
Wrap.Pinit [in intensional.examples.linearizability]
Wrap.pop [in intensional.examples.traversable_stack]
Wrap.pop [in intensional.examples.stack]
Wrap.push [in intensional.examples.traversable_stack]
Wrap.push [in intensional.examples.stack]
Wrap.P_state_wrap [in intensional.examples.linearizability]
Wrap.R [in intensional.examples.linearizability]
Wrap.read [in intensional.examples.file]
Wrap.remove [in intensional.examples.iterator]
Wrap.size [in intensional.examples.iterator]
Wrap.stack_val [in intensional.examples.traversable_stack]
Wrap.stack_val [in intensional.examples.stack]
Wrap.tags_state [in intensional.examples.linearizability]
Wrap.traceN [in intensional.examples.linearizability]
Wrap.T0 [in intensional.examples.well_bracketed]
Wrap.T1 [in intensional.examples.well_bracketed]
Wrap.T2 [in intensional.examples.well_bracketed]
Wrap.T3 [in intensional.examples.well_bracketed]
Wrap.unlocked [in intensional.examples.well_bracketed]
Wrap.withRes [in intensional.examples.well_bracketed]

Record Index

A

AsRecV [in intensional.heap_lang.lifting]

H

heapG [in intensional.heap_lang.lifting]
heapPreG [in intensional.heap_lang.adequacy]
heap_lang.state [in intensional.heap_lang.lang]

L

loc [in intensional.heap_lang.locations]

M

model [in intensional.examples.linearizability]

R

repr [in intensional.examples.linearizability]

T

traceG [in intensional.heap_lang.lifting]
trace_preG [in intensional.heap_lang.lifting]

W

Wrap.linG [in intensional.examples.linearizability]

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

(2639 entries)

Notation 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

(46 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

(1928 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

(8 entries)

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

(19 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

(200 entries)

Constructor 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

(126 entries)

Projection 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

(30 entries)

Inductive 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

(15 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

(17 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

(68 entries)

Abbreviation 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

(18 entries)

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

(154 entries)

Record 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

(10 entries)