| 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 | (2452 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 | (81 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 | (1680 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (13 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 | (366 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 | (41 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 | (18 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 | (14 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 | (115 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) |
| 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 | (19 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 | (76 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 | (8 entries) |
Global Index
A
acc:332 [binder, in Obs.list_tools]acc:362 [binder, in Obs.list_tools]
acc:44 [binder, in Obs.list_dec]
all_subsets_nodup [lemma, in Obs.list_tools]
an [projection, in Obs.fan]
andb_prop_iff [lemma, in Obs.decidable_prop]
and_Join [lemma, in Obs.laws]
anticlique [library]
anticlique_choose_clique [lemma, in Obs.anticlique]
anticlique_inf_or_cntrex [lemma, in Obs.anticlique]
anticlique_dec_inf [instance, in Obs.anticlique]
an_spec [projection, in Obs.fan]
app_comm [lemma, in Obs.list_tools]
app_idem [lemma, in Obs.list_tools]
app_eq_app_length [lemma, in Obs.list_tools]
atTop [definition, in Obs.product]
auxiliary [lemma, in Obs.product]
Ax_impl_eq [instance, in Obs.equiv_obs]
Ax:118 [binder, in Obs.laws]
Ax:127 [binder, in Obs.laws]
axΩ [abbreviation, in Obs.anticlique]
axΩ_sound [lemma, in Obs.anticlique]
a__o:6 [binder, in Obs.anticlique]
A:1 [binder, in Obs.list_tools]
A:1 [binder, in Obs.list_dec]
A:1 [binder, in Obs.notations]
a:10 [binder, in Obs.laws]
A:10 [binder, in Obs.notations]
A:100 [binder, in Obs.list_tools]
a:100 [binder, in Obs.coherence_graph]
a:101 [binder, in Obs.laws]
a:101 [binder, in Obs.list_dec]
a:102 [binder, in Obs.coherence_graph]
a:102 [binder, in Obs.list_dec]
a:103 [binder, in Obs.laws]
a:105 [binder, in Obs.coherence_graph]
a:105 [binder, in Obs.laws]
A:106 [binder, in Obs.list_tools]
a:107 [binder, in Obs.coherence_graph]
a:108 [binder, in Obs.laws]
A:11 [binder, in Obs.list_tools]
a:11 [binder, in Obs.laws]
a:11 [binder, in Obs.equiv_obs]
a:110 [binder, in Obs.coherence_graph]
a:111 [binder, in Obs.list_tools]
a:113 [binder, in Obs.coherence_graph]
a:119 [binder, in Obs.list_tools]
a:12 [binder, in Obs.coherence_graph]
a:12 [binder, in Obs.product]
a:12 [binder, in Obs.anticlique]
A:120 [binder, in Obs.list_tools]
a:120 [binder, in Obs.coherence_graph]
a:123 [binder, in Obs.list_tools]
a:123 [binder, in Obs.list_dec]
A:124 [binder, in Obs.list_tools]
a:125 [binder, in Obs.coherence_graph]
A:128 [binder, in Obs.list_tools]
a:13 [binder, in Obs.fan]
a:131 [binder, in Obs.coherence_graph]
A:136 [binder, in Obs.list_tools]
a:137 [binder, in Obs.coherence_graph]
a:139 [binder, in Obs.coherence_graph]
a:14 [binder, in Obs.laws]
A:14 [binder, in Obs.notations]
a:140 [binder, in Obs.list_tools]
a:140 [binder, in Obs.laws]
A:141 [binder, in Obs.list_tools]
a:142 [binder, in Obs.list_dec]
a:145 [binder, in Obs.list_dec]
a:146 [binder, in Obs.list_tools]
a:146 [binder, in Obs.laws]
A:148 [binder, in Obs.list_tools]
a:148 [binder, in Obs.laws]
a:148 [binder, in Obs.list_dec]
A:15 [binder, in Obs.list_tools]
a:15 [binder, in Obs.coherence_graph]
a:15 [binder, in Obs.equiv_obs]
a:15 [binder, in Obs.fan]
a:15 [binder, in Obs.anticlique]
A:154 [binder, in Obs.list_tools]
A:159 [binder, in Obs.list_tools]
a:159 [binder, in Obs.coherence_graph]
a:16 [binder, in Obs.laws]
a:16 [binder, in Obs.anticlique]
a:160 [binder, in Obs.coherence_graph]
A:167 [binder, in Obs.list_tools]
a:167 [binder, in Obs.list_dec]
a:169 [binder, in Obs.coherence_graph]
a:17 [binder, in Obs.list_tools]
a:17 [binder, in Obs.laws]
a:17 [binder, in Obs.product]
a:17 [binder, in Obs.anticlique]
a:17 [binder, in Obs.notations]
a:170 [binder, in Obs.list_dec]
A:176 [binder, in Obs.list_tools]
a:18 [binder, in Obs.coherence_graph]
a:18 [binder, in Obs.fan]
a:18 [binder, in Obs.list_dec]
A:180 [binder, in Obs.list_tools]
a:182 [binder, in Obs.coherence_graph]
a:183 [binder, in Obs.list_tools]
a:183 [binder, in Obs.coherence_graph]
a:184 [binder, in Obs.coherence_graph]
a:184 [binder, in Obs.product]
A:185 [binder, in Obs.list_tools]
a:185 [binder, in Obs.coherence_graph]
a:186 [binder, in Obs.coherence_graph]
a:188 [binder, in Obs.coherence_graph]
a:189 [binder, in Obs.coherence_graph]
a:19 [binder, in Obs.laws]
a:19 [binder, in Obs.equiv_obs]
a:19 [binder, in Obs.anticlique]
A:191 [binder, in Obs.list_dec]
a:193 [binder, in Obs.list_dec]
a:195 [binder, in Obs.list_tools]
A:195 [binder, in Obs.list_dec]
a:197 [binder, in Obs.list_tools]
A:198 [binder, in Obs.list_tools]
A:2 [binder, in Obs.list_tools]
A:2 [binder, in Obs.laws]
A:2 [binder, in Obs.equiv_obs]
A:20 [binder, in Obs.list_tools]
A:20 [binder, in Obs.decidable_prop]
a:20 [binder, in Obs.product]
a:20 [binder, in Obs.fan]
a:20 [binder, in Obs.notations]
A:201 [binder, in Obs.list_tools]
A:204 [binder, in Obs.list_tools]
A:204 [binder, in Obs.list_dec]
A:206 [binder, in Obs.list_tools]
A:208 [binder, in Obs.list_tools]
a:209 [binder, in Obs.list_dec]
a:21 [binder, in Obs.laws]
a:21 [binder, in Obs.list_dec]
A:210 [binder, in Obs.list_tools]
A:211 [binder, in Obs.list_dec]
A:212 [binder, in Obs.list_tools]
A:216 [binder, in Obs.list_tools]
a:217 [binder, in Obs.list_dec]
A:218 [binder, in Obs.list_dec]
A:219 [binder, in Obs.list_tools]
a:22 [binder, in Obs.list_tools]
a:22 [binder, in Obs.laws]
A:222 [binder, in Obs.list_tools]
A:224 [binder, in Obs.list_tools]
A:224 [binder, in Obs.list_dec]
A:227 [binder, in Obs.list_tools]
A:227 [binder, in Obs.list_dec]
A:229 [binder, in Obs.list_tools]
a:23 [binder, in Obs.equiv_obs]
A:23 [binder, in Obs.sem_obs]
a:23 [binder, in Obs.anticlique]
a:230 [binder, in Obs.product]
A:230 [binder, in Obs.list_dec]
A:232 [binder, in Obs.list_tools]
a:232 [binder, in Obs.product]
a:234 [binder, in Obs.product]
A:236 [binder, in Obs.list_tools]
a:236 [binder, in Obs.product]
A:238 [binder, in Obs.list_tools]
a:238 [binder, in Obs.product]
a:24 [binder, in Obs.coherence_graph]
a:24 [binder, in Obs.laws]
a:24 [binder, in Obs.sem_obs]
a:240 [binder, in Obs.product]
A:241 [binder, in Obs.list_tools]
A:247 [binder, in Obs.list_tools]
A:25 [binder, in Obs.equiv_obs]
a:25 [binder, in Obs.product]
A:252 [binder, in Obs.list_tools]
a:256 [binder, in Obs.list_tools]
A:257 [binder, in Obs.list_tools]
A:26 [binder, in Obs.list_tools]
a:26 [binder, in Obs.laws]
a:26 [binder, in Obs.equiv_obs]
A:26 [binder, in Obs.sem_obs]
a:26 [binder, in Obs.anticlique]
a:261 [binder, in Obs.list_tools]
A:262 [binder, in Obs.list_tools]
A:266 [binder, in Obs.list_tools]
a:27 [binder, in Obs.coherence_graph]
a:27 [binder, in Obs.sem_obs]
a:27 [binder, in Obs.list_dec]
a:271 [binder, in Obs.list_tools]
A:272 [binder, in Obs.list_tools]
a:277 [binder, in Obs.list_tools]
A:278 [binder, in Obs.list_tools]
a:28 [binder, in Obs.list_tools]
A:28 [binder, in Obs.equiv_obs]
A:284 [binder, in Obs.list_tools]
a:286 [binder, in Obs.list_tools]
a:29 [binder, in Obs.laws]
A:29 [binder, in Obs.equiv_obs]
a:29 [binder, in Obs.product]
A:293 [binder, in Obs.list_tools]
a:295 [binder, in Obs.list_tools]
a:30 [binder, in Obs.coherence_graph]
a:30 [binder, in Obs.laws]
A:30 [binder, in Obs.decidable_prop]
A:30 [binder, in Obs.equiv_obs]
A:302 [binder, in Obs.list_tools]
A:308 [binder, in Obs.list_tools]
a:31 [binder, in Obs.laws]
A:31 [binder, in Obs.equiv_obs]
a:31 [binder, in Obs.list_dec]
A:312 [binder, in Obs.list_tools]
A:315 [binder, in Obs.list_tools]
a:316 [binder, in Obs.list_tools]
A:32 [binder, in Obs.list_tools]
a:32 [binder, in Obs.coherence_graph]
a:32 [binder, in Obs.laws]
A:32 [binder, in Obs.equiv_obs]
A:320 [binder, in Obs.list_tools]
A:324 [binder, in Obs.list_tools]
A:327 [binder, in Obs.list_tools]
a:33 [binder, in Obs.laws]
A:33 [binder, in Obs.equiv_obs]
a:331 [binder, in Obs.list_tools]
A:334 [binder, in Obs.list_tools]
a:338 [binder, in Obs.list_tools]
a:34 [binder, in Obs.coherence_graph]
A:34 [binder, in Obs.equiv_obs]
a:34 [binder, in Obs.product]
A:340 [binder, in Obs.list_tools]
A:347 [binder, in Obs.list_tools]
A:35 [binder, in Obs.equiv_obs]
A:351 [binder, in Obs.list_tools]
a:354 [binder, in Obs.list_tools]
A:355 [binder, in Obs.list_tools]
A:358 [binder, in Obs.list_tools]
A:36 [binder, in Obs.list_tools]
a:36 [binder, in Obs.laws]
A:36 [binder, in Obs.equiv_obs]
a:36 [binder, in Obs.fan]
a:361 [binder, in Obs.list_tools]
A:363 [binder, in Obs.list_tools]
A:367 [binder, in Obs.list_tools]
A:37 [binder, in Obs.equiv_obs]
a:37 [binder, in Obs.fan]
A:371 [binder, in Obs.list_tools]
A:375 [binder, in Obs.list_tools]
a:38 [binder, in Obs.list_tools]
a:38 [binder, in Obs.coherence_graph]
a:38 [binder, in Obs.laws]
A:38 [binder, in Obs.equiv_obs]
a:38 [binder, in Obs.anticlique]
A:380 [binder, in Obs.list_tools]
A:385 [binder, in Obs.list_tools]
a:39 [binder, in Obs.product]
A:390 [binder, in Obs.list_tools]
A:396 [binder, in Obs.list_tools]
A:4 [binder, in Obs.list_tools]
a:4 [binder, in Obs.fan]
a:4 [binder, in Obs.anticlique]
A:40 [binder, in Obs.list_tools]
A:40 [binder, in Obs.decidable_prop]
a:40 [binder, in Obs.list_dec]
A:401 [binder, in Obs.list_tools]
A:405 [binder, in Obs.list_tools]
a:409 [binder, in Obs.list_tools]
a:41 [binder, in Obs.coherence_graph]
a:41 [binder, in Obs.laws]
a:41 [binder, in Obs.anticlique]
A:410 [binder, in Obs.list_tools]
a:414 [binder, in Obs.list_tools]
A:416 [binder, in Obs.list_tools]
A:420 [binder, in Obs.list_tools]
a:421 [binder, in Obs.list_tools]
a:428 [binder, in Obs.list_tools]
a:43 [binder, in Obs.list_tools]
a:43 [binder, in Obs.laws]
a:43 [binder, in Obs.product]
a:43 [binder, in Obs.list_dec]
A:44 [binder, in Obs.list_tools]
a:45 [binder, in Obs.coherence_graph]
a:45 [binder, in Obs.laws]
A:450 [binder, in Obs.list_tools]
a:451 [binder, in Obs.list_tools]
A:455 [binder, in Obs.list_tools]
a:46 [binder, in Obs.coherence_graph]
A:46 [binder, in Obs.equiv_obs]
a:46 [binder, in Obs.product]
a:46 [binder, in Obs.list_dec]
a:46 [binder, in Obs.anticlique]
a:47 [binder, in Obs.laws]
A:48 [binder, in Obs.list_tools]
A:48 [binder, in Obs.decidable_prop]
a:49 [binder, in Obs.laws]
a:49 [binder, in Obs.anticlique]
a:5 [binder, in Obs.list_tools]
a:5 [binder, in Obs.laws]
a:5 [binder, in Obs.equiv_obs]
A:51 [binder, in Obs.list_tools]
a:51 [binder, in Obs.coherence_graph]
A:51 [binder, in Obs.equiv_obs]
a:52 [binder, in Obs.laws]
a:53 [binder, in Obs.coherence_graph]
a:54 [binder, in Obs.product]
A:55 [binder, in Obs.list_tools]
a:55 [binder, in Obs.laws]
a:55 [binder, in Obs.sem_obs]
a:55 [binder, in Obs.fan]
a:57 [binder, in Obs.anticlique]
a:58 [binder, in Obs.list_tools]
a:58 [binder, in Obs.laws]
a:58 [binder, in Obs.equiv_obs]
a:58 [binder, in Obs.product]
a:58 [binder, in Obs.fan]
A:59 [binder, in Obs.list_tools]
a:6 [binder, in Obs.equiv_obs]
a:6 [binder, in Obs.fin_sem_obs]
a:60 [binder, in Obs.fan]
a:61 [binder, in Obs.laws]
a:61 [binder, in Obs.equiv_obs]
a:61 [binder, in Obs.product]
a:63 [binder, in Obs.equiv_obs]
a:63 [binder, in Obs.fan]
a:64 [binder, in Obs.laws]
a:64 [binder, in Obs.equiv_obs]
a:64 [binder, in Obs.product]
A:65 [binder, in Obs.list_tools]
a:65 [binder, in Obs.product]
a:65 [binder, in Obs.fan]
a:65 [binder, in Obs.list_dec]
a:66 [binder, in Obs.laws]
a:67 [binder, in Obs.equiv_obs]
a:67 [binder, in Obs.product]
a:67 [binder, in Obs.fan]
a:68 [binder, in Obs.coherence_graph]
a:68 [binder, in Obs.laws]
a:68 [binder, in Obs.fan]
a:69 [binder, in Obs.coherence_graph]
a:69 [binder, in Obs.equiv_obs]
a:69 [binder, in Obs.fan]
a:69 [binder, in Obs.list_dec]
A:7 [binder, in Obs.list_tools]
a:7 [binder, in Obs.coherence_graph]
A:70 [binder, in Obs.list_tools]
a:70 [binder, in Obs.coherence_graph]
a:70 [binder, in Obs.laws]
a:70 [binder, in Obs.equiv_obs]
a:71 [binder, in Obs.coherence_graph]
A:71 [binder, in Obs.decidable_prop]
a:71 [binder, in Obs.list_dec]
a:72 [binder, in Obs.coherence_graph]
a:72 [binder, in Obs.equiv_obs]
a:73 [binder, in Obs.laws]
a:73 [binder, in Obs.list_dec]
a:74 [binder, in Obs.coherence_graph]
a:74 [binder, in Obs.decidable_prop]
a:74 [binder, in Obs.equiv_obs]
a:74 [binder, in Obs.list_dec]
A:75 [binder, in Obs.list_tools]
a:75 [binder, in Obs.decidable_prop]
a:75 [binder, in Obs.equiv_obs]
a:75 [binder, in Obs.list_dec]
a:76 [binder, in Obs.coherence_graph]
a:76 [binder, in Obs.laws]
a:76 [binder, in Obs.decidable_prop]
a:76 [binder, in Obs.anticlique]
A:77 [binder, in Obs.list_tools]
a:77 [binder, in Obs.decidable_prop]
a:77 [binder, in Obs.equiv_obs]
a:77 [binder, in Obs.list_dec]
a:77 [binder, in Obs.anticlique]
a:78 [binder, in Obs.coherence_graph]
A:78 [binder, in Obs.decidable_prop]
a:79 [binder, in Obs.laws]
a:79 [binder, in Obs.equiv_obs]
A:8 [binder, in Obs.list_tools]
a:8 [binder, in Obs.laws]
a:8 [binder, in Obs.equiv_obs]
A:80 [binder, in Obs.list_tools]
a:80 [binder, in Obs.coherence_graph]
a:81 [binder, in Obs.decidable_prop]
a:81 [binder, in Obs.list_dec]
a:82 [binder, in Obs.coherence_graph]
a:82 [binder, in Obs.laws]
a:82 [binder, in Obs.decidable_prop]
a:83 [binder, in Obs.list_tools]
a:83 [binder, in Obs.decidable_prop]
a:83 [binder, in Obs.list_dec]
A:84 [binder, in Obs.list_tools]
a:84 [binder, in Obs.decidable_prop]
a:84 [binder, in Obs.equiv_obs]
a:85 [binder, in Obs.laws]
a:86 [binder, in Obs.laws]
a:86 [binder, in Obs.list_dec]
a:87 [binder, in Obs.laws]
a:88 [binder, in Obs.laws]
A:89 [binder, in Obs.list_tools]
a:89 [binder, in Obs.list_dec]
a:9 [binder, in Obs.anticlique]
a:91 [binder, in Obs.coherence_graph]
a:91 [binder, in Obs.laws]
a:93 [binder, in Obs.equiv_obs]
a:93 [binder, in Obs.list_dec]
A:94 [binder, in Obs.list_tools]
a:94 [binder, in Obs.coherence_graph]
a:94 [binder, in Obs.laws]
a:94 [binder, in Obs.anticlique]
a:95 [binder, in Obs.anticlique]
a:96 [binder, in Obs.coherence_graph]
a:96 [binder, in Obs.anticlique]
a:97 [binder, in Obs.anticlique]
a:98 [binder, in Obs.anticlique]
a:99 [binder, in Obs.anticlique]
B
Boolean [instance, in Obs.decidable_prop]b0:115 [binder, in Obs.coherence_graph]
b0:116 [binder, in Obs.coherence_graph]
b0:117 [binder, in Obs.coherence_graph]
b0:118 [binder, in Obs.coherence_graph]
b0:122 [binder, in Obs.coherence_graph]
b0:123 [binder, in Obs.coherence_graph]
b:10 [binder, in Obs.anticlique]
b:101 [binder, in Obs.coherence_graph]
b:103 [binder, in Obs.coherence_graph]
b:107 [binder, in Obs.laws]
b:108 [binder, in Obs.coherence_graph]
B:11 [binder, in Obs.notations]
b:110 [binder, in Obs.laws]
b:111 [binder, in Obs.coherence_graph]
b:114 [binder, in Obs.coherence_graph]
B:12 [binder, in Obs.list_tools]
b:12 [binder, in Obs.laws]
b:12 [binder, in Obs.equiv_obs]
b:121 [binder, in Obs.coherence_graph]
b:124 [binder, in Obs.list_dec]
b:125 [binder, in Obs.list_dec]
b:126 [binder, in Obs.list_dec]
b:127 [binder, in Obs.list_dec]
b:128 [binder, in Obs.list_dec]
B:129 [binder, in Obs.list_tools]
b:129 [binder, in Obs.list_dec]
b:13 [binder, in Obs.coherence_graph]
b:13 [binder, in Obs.anticlique]
b:130 [binder, in Obs.list_dec]
b:131 [binder, in Obs.list_dec]
b:132 [binder, in Obs.coherence_graph]
b:138 [binder, in Obs.coherence_graph]
b:140 [binder, in Obs.coherence_graph]
b:147 [binder, in Obs.list_tools]
B:149 [binder, in Obs.list_tools]
b:15 [binder, in Obs.laws]
B:15 [binder, in Obs.notations]
B:155 [binder, in Obs.list_tools]
b:16 [binder, in Obs.coherence_graph]
b:16 [binder, in Obs.equiv_obs]
B:160 [binder, in Obs.list_tools]
B:168 [binder, in Obs.list_tools]
B:177 [binder, in Obs.list_tools]
b:18 [binder, in Obs.laws]
b:18 [binder, in Obs.product]
b:18 [binder, in Obs.anticlique]
b:18 [binder, in Obs.notations]
B:181 [binder, in Obs.list_tools]
b:184 [binder, in Obs.list_tools]
b:187 [binder, in Obs.coherence_graph]
b:19 [binder, in Obs.coherence_graph]
b:19 [binder, in Obs.fan]
b:19 [binder, in Obs.list_dec]
b:190 [binder, in Obs.coherence_graph]
b:194 [binder, in Obs.list_dec]
B:196 [binder, in Obs.list_dec]
B:199 [binder, in Obs.list_tools]
b:20 [binder, in Obs.laws]
b:20 [binder, in Obs.equiv_obs]
B:202 [binder, in Obs.list_tools]
B:205 [binder, in Obs.list_dec]
b:21 [binder, in Obs.coherence_graph]
B:21 [binder, in Obs.decidable_prop]
b:21 [binder, in Obs.product]
b:21 [binder, in Obs.fan]
b:21 [binder, in Obs.notations]
b:210 [binder, in Obs.list_dec]
B:212 [binder, in Obs.list_dec]
B:217 [binder, in Obs.list_tools]
B:219 [binder, in Obs.list_dec]
b:22 [binder, in Obs.list_dec]
B:220 [binder, in Obs.list_tools]
b:23 [binder, in Obs.laws]
b:23 [binder, in Obs.notations]
B:230 [binder, in Obs.list_tools]
b:231 [binder, in Obs.product]
b:233 [binder, in Obs.product]
b:235 [binder, in Obs.product]
b:237 [binder, in Obs.product]
b:239 [binder, in Obs.product]
b:24 [binder, in Obs.equiv_obs]
b:24 [binder, in Obs.notations]
b:241 [binder, in Obs.product]
b:25 [binder, in Obs.laws]
b:26 [binder, in Obs.coherence_graph]
b:26 [binder, in Obs.product]
B:267 [binder, in Obs.list_tools]
b:27 [binder, in Obs.laws]
b:27 [binder, in Obs.equiv_obs]
B:273 [binder, in Obs.list_tools]
B:279 [binder, in Obs.list_tools]
B:285 [binder, in Obs.list_tools]
b:29 [binder, in Obs.coherence_graph]
B:294 [binder, in Obs.list_tools]
b:30 [binder, in Obs.product]
B:31 [binder, in Obs.decidable_prop]
B:328 [binder, in Obs.list_tools]
b:33 [binder, in Obs.fan]
b:333 [binder, in Obs.list_tools]
B:335 [binder, in Obs.list_tools]
b:339 [binder, in Obs.list_tools]
b:34 [binder, in Obs.laws]
b:35 [binder, in Obs.coherence_graph]
b:35 [binder, in Obs.product]
b:37 [binder, in Obs.laws]
b:39 [binder, in Obs.laws]
B:39 [binder, in Obs.equiv_obs]
b:39 [binder, in Obs.anticlique]
b:41 [binder, in Obs.list_dec]
b:415 [binder, in Obs.list_tools]
b:42 [binder, in Obs.coherence_graph]
b:42 [binder, in Obs.laws]
b:44 [binder, in Obs.laws]
b:46 [binder, in Obs.laws]
B:47 [binder, in Obs.equiv_obs]
b:48 [binder, in Obs.laws]
b:5 [binder, in Obs.fan]
b:51 [binder, in Obs.laws]
b:52 [binder, in Obs.coherence_graph]
B:52 [binder, in Obs.equiv_obs]
b:53 [binder, in Obs.laws]
b:54 [binder, in Obs.coherence_graph]
b:56 [binder, in Obs.laws]
b:56 [binder, in Obs.sem_obs]
b:56 [binder, in Obs.fan]
b:57 [binder, in Obs.decidable_prop]
b:58 [binder, in Obs.decidable_prop]
b:59 [binder, in Obs.laws]
b:59 [binder, in Obs.equiv_obs]
b:6 [binder, in Obs.laws]
B:60 [binder, in Obs.list_tools]
b:61 [binder, in Obs.fan]
b:62 [binder, in Obs.laws]
b:62 [binder, in Obs.equiv_obs]
b:65 [binder, in Obs.laws]
b:65 [binder, in Obs.equiv_obs]
b:67 [binder, in Obs.laws]
b:68 [binder, in Obs.equiv_obs]
b:68 [binder, in Obs.list_dec]
b:69 [binder, in Obs.laws]
b:7 [binder, in Obs.equiv_obs]
b:71 [binder, in Obs.laws]
b:71 [binder, in Obs.equiv_obs]
b:73 [binder, in Obs.coherence_graph]
b:73 [binder, in Obs.equiv_obs]
b:74 [binder, in Obs.laws]
b:75 [binder, in Obs.coherence_graph]
b:76 [binder, in Obs.equiv_obs]
b:77 [binder, in Obs.coherence_graph]
b:77 [binder, in Obs.laws]
b:78 [binder, in Obs.equiv_obs]
b:79 [binder, in Obs.coherence_graph]
b:8 [binder, in Obs.coherence_graph]
b:80 [binder, in Obs.laws]
b:80 [binder, in Obs.equiv_obs]
b:81 [binder, in Obs.coherence_graph]
b:83 [binder, in Obs.coherence_graph]
b:83 [binder, in Obs.laws]
b:85 [binder, in Obs.equiv_obs]
b:9 [binder, in Obs.laws]
b:9 [binder, in Obs.equiv_obs]
b:9 [binder, in Obs.fin_sem_obs]
b:90 [binder, in Obs.list_dec]
b:92 [binder, in Obs.coherence_graph]
b:93 [binder, in Obs.laws]
b:95 [binder, in Obs.coherence_graph]
b:96 [binder, in Obs.laws]
b:97 [binder, in Obs.coherence_graph]
C
choose_clique_aux [lemma, in Obs.product]choose_clique_𝖦:7 [binder, in Obs.product]
choose_clique_sat_dec [lemma, in Obs.sem_obs]
choose_clique [definition, in Obs.sem_obs]
clique [record, in Obs.coherence_graph]
cliques_at_most_one_elt [lemma, in Obs.anticlique]
clique_sat_iff_fsat_proj [lemma, in Obs.fin_sem_obs]
cnf_support_incl [lemma, in Obs.product]
cnf_support_proper [instance, in Obs.product]
cnf_support_proper_incl [instance, in Obs.product]
cnf_to_dnf_equiv [lemma, in Obs.product]
cnf_to_dnf_support [lemma, in Obs.product]
cnf_to_dnf [definition, in Obs.product]
cnf_support [definition, in Obs.product]
cnf:147 [binder, in Obs.product]
cnf:159 [binder, in Obs.product]
cnf:179 [binder, in Obs.product]
coh [projection, in Obs.coherence_graph]
coherence_graph [library]
coh_sym [projection, in Obs.coherence_graph]
coh_refl [projection, in Obs.coherence_graph]
coh_ij [constructor, in Obs.product]
coh_i [constructor, in Obs.product]
coh𝒢 [inductive, in Obs.product]
coh𝒢_sym [lemma, in Obs.product]
coh𝒢_refl [lemma, in Obs.product]
combine [section, in Obs.list_tools]
combine_split [lemma, in Obs.list_tools]
combine_app [lemma, in Obs.list_tools]
combine_snd [lemma, in Obs.list_tools]
combine_fst [lemma, in Obs.list_tools]
combine.same_length [variable, in Obs.list_tools]
_ ⊗ _ [notation, in Obs.list_tools]
compat_dec [instance, in Obs.coherence_graph]
compat_are_coh [lemma, in Obs.coherence_graph]
completeness_anticlique_eq [lemma, in Obs.anticlique]
completeness_anticlique [lemma, in Obs.anticlique]
complete_inf__Ω [lemma, in Obs.anticlique]
Conj [definition, in Obs.fan]
conj_interp [definition, in Obs.product]
Conj_spec [lemma, in Obs.fan]
c':57 [binder, in Obs.fan]
c':62 [binder, in Obs.fan]
c':64 [binder, in Obs.fan]
c':66 [binder, in Obs.fan]
c:10 [binder, in Obs.equiv_obs]
c:13 [binder, in Obs.laws]
c:13 [binder, in Obs.equiv_obs]
c:145 [binder, in Obs.list_tools]
C:156 [binder, in Obs.list_tools]
c:166 [binder, in Obs.product]
c:17 [binder, in Obs.equiv_obs]
c:170 [binder, in Obs.product]
c:173 [binder, in Obs.product]
c:175 [binder, in Obs.product]
c:19 [binder, in Obs.notations]
c:21 [binder, in Obs.equiv_obs]
c:22 [binder, in Obs.notations]
C:231 [binder, in Obs.list_tools]
c:28 [binder, in Obs.laws]
c:35 [binder, in Obs.laws]
c:40 [binder, in Obs.laws]
c:50 [binder, in Obs.laws]
c:54 [binder, in Obs.laws]
c:54 [binder, in Obs.fan]
c:57 [binder, in Obs.laws]
c:59 [binder, in Obs.fan]
c:60 [binder, in Obs.laws]
c:60 [binder, in Obs.equiv_obs]
c:63 [binder, in Obs.laws]
c:66 [binder, in Obs.equiv_obs]
c:7 [binder, in Obs.laws]
c:72 [binder, in Obs.laws]
c:75 [binder, in Obs.laws]
c:78 [binder, in Obs.laws]
c:81 [binder, in Obs.laws]
c:81 [binder, in Obs.equiv_obs]
c:84 [binder, in Obs.laws]
c:92 [binder, in Obs.product]
D
decG:147 [binder, in Obs.laws]decG:2 [binder, in Obs.fin_sem_obs]
decG:2 [binder, in Obs.sem_obs]
decG:61 [binder, in Obs.sem_obs]
decG:62 [binder, in Obs.coherence_graph]
decG:7 [binder, in Obs.syntax_obs]
decG:8 [binder, in Obs.fan]
decG:86 [binder, in Obs.equiv_obs]
decG:89 [binder, in Obs.coherence_graph]
decidable [section, in Obs.decidable_prop]
DecidableGraph [record, in Obs.coherence_graph]
DecidableProp [record, in Obs.decidable_prop]
DecidableProp [inductive, in Obs.decidable_prop]
DecidableProp_equiv_prop [instance, in Obs.decidable_prop]
DecidableProp_exists_bnd [instance, in Obs.decidable_prop]
DecidableProp_forall_bnd [instance, in Obs.decidable_prop]
DecidableProp_iff [instance, in Obs.decidable_prop]
DecidableProp_impl [instance, in Obs.decidable_prop]
DecidableProp_disj [instance, in Obs.decidable_prop]
DecidableProp_conj [instance, in Obs.decidable_prop]
DecidableProp_neg [instance, in Obs.decidable_prop]
DecidableProp_Eq [instance, in Obs.decidable_prop]
DecidableProp_Equiv [instance, in Obs.list_dec]
DecidableProp_Incl [instance, in Obs.list_dec]
DecidableProp_In [instance, in Obs.list_dec]
decidable_incompatible_with_fcliques [lemma, in Obs.coherence_graph]
decidable_incompatible_f [instance, in Obs.coherence_graph]
decidable_is_coherent [instance, in Obs.coherence_graph]
decidable_incoh [instance, in Obs.coherence_graph]
decidable_graph [section, in Obs.coherence_graph]
decidable_vertex [projection, in Obs.coherence_graph]
decidable_set [record, in Obs.decidable_prop]
decidable_prop [library]
decidale_coh [projection, in Obs.coherence_graph]
decIdx:2 [binder, in Obs.product]
decomposition [lemma, in Obs.list_dec]
decomp_unambiguous [lemma, in Obs.list_dec]
decomp_unique [lemma, in Obs.list_dec]
decV:2 [binder, in Obs.anticlique]
dec_prop [projection, in Obs.decidable_prop]
dec_prop [constructor, in Obs.decidable_prop]
dec_option [instance, in Obs.decidable_prop]
dec_sum [instance, in Obs.decidable_prop]
dec_prod [instance, in Obs.decidable_prop]
dec_compat_proj [lemma, in Obs.product]
dec_in_proj [lemma, in Obs.product]
dec_ssmaller_impl_dec_sequiv [lemma, in Obs.sem_obs]
dec_sequiv_impl_dec_ssmaller [lemma, in Obs.sem_obs]
dec_ssmaller_impl_dec_fsat [lemma, in Obs.sem_obs]
dec_fsat_impl_dec_ssmaller [lemma, in Obs.sem_obs]
_ − _ [notation, in Obs.list_dec]
_ ∩ _ [notation, in Obs.list_dec]
_ ⊖ _ [notation, in Obs.list_dec]
_ ∖ _ [notation, in Obs.list_dec]
{{ _ }} [notation, in Obs.list_dec]
dec_list [instance, in Obs.list_dec]
dec_A:2 [binder, in Obs.list_dec]
dec_list [section, in Obs.list_dec]
dec_sat [instance, in Obs.anticlique]
dec_inf__Ω [instance, in Obs.anticlique]
decΩ [instance, in Obs.anticlique]
dec𝒢 [instance, in Obs.product]
dec𝖦:5 [binder, in Obs.product]
difference [definition, in Obs.list_dec]
difference_intersect [lemma, in Obs.list_dec]
difference_incl [lemma, in Obs.list_dec]
difference_nil [lemma, in Obs.list_dec]
difference_inter_l [lemma, in Obs.list_dec]
difference_inter_r [lemma, in Obs.list_dec]
difference_app_r [lemma, in Obs.list_dec]
difference_app_l [lemma, in Obs.list_dec]
difference_right_subs [lemma, in Obs.list_dec]
difference_proper_inf [instance, in Obs.list_dec]
difference_proper [instance, in Obs.list_dec]
difference_spec [lemma, in Obs.list_dec]
disj_interp [definition, in Obs.product]
dnf_support_incl [lemma, in Obs.product]
dnf_support_proper [instance, in Obs.product]
dnf_support_proper_incl [instance, in Obs.product]
dnf_to_cnf_equiv [lemma, in Obs.product]
dnf_to_cnf_support [lemma, in Obs.product]
dnf_to_cnf [definition, in Obs.product]
dnf_support [definition, in Obs.product]
dnf:143 [binder, in Obs.product]
dnf:152 [binder, in Obs.product]
dnf:172 [binder, in Obs.product]
dnf:182 [binder, in Obs.product]
d:14 [binder, in Obs.equiv_obs]
d:168 [binder, in Obs.product]
d:174 [binder, in Obs.product]
d:176 [binder, in Obs.product]
d:18 [binder, in Obs.equiv_obs]
d:22 [binder, in Obs.equiv_obs]
d:52 [binder, in Obs.decidable_prop]
D:8 [binder, in Obs.decidable_prop]
d:93 [binder, in Obs.product]
E
elts:341 [binder, in Obs.list_tools]elts:348 [binder, in Obs.list_tools]
empt [definition, in Obs.coherence_graph]
empt_max [lemma, in Obs.coherence_graph]
empt_spec [lemma, in Obs.coherence_graph]
eo_Meet_impl [lemma, in Obs.laws]
eo_impl_Join [lemma, in Obs.laws]
eo_inf_in_Meet [lemma, in Obs.laws]
eo_inf_in_Join [lemma, in Obs.laws]
eo_top_impl [lemma, in Obs.laws]
eo_contradict [lemma, in Obs.laws]
eo_eq_bot_iff_inf_bot [lemma, in Obs.laws]
eo_eq_top_iff_top_inf [lemma, in Obs.laws]
eo_inf_bot [lemma, in Obs.laws]
eo_inf_top [lemma, in Obs.laws]
eo_impl_distr_left [lemma, in Obs.laws]
eo_distr2 [lemma, in Obs.laws]
eo_distr1 [lemma, in Obs.laws]
eo_curry [lemma, in Obs.laws]
eo_heyting [lemma, in Obs.laws]
eo_inf_o_impl [lemma, in Obs.laws]
eo_impl_mp [lemma, in Obs.laws]
eo_inf_impl_concl [lemma, in Obs.laws]
eo_inf_impl_right_mon [lemma, in Obs.laws]
eo_inf_and_right [lemma, in Obs.laws]
eo_inf_and_left [lemma, in Obs.laws]
eo_inf_or_right [lemma, in Obs.laws]
eo_inf_or_left [lemma, in Obs.laws]
eo_inf_and_r [lemma, in Obs.laws]
eo_inf_and_l [lemma, in Obs.laws]
eo_inf_or_r [lemma, in Obs.laws]
eo_inf_or_l [lemma, in Obs.laws]
eo_inf_o_and [lemma, in Obs.laws]
eo_or_idem [lemma, in Obs.laws]
eo_and_idem [lemma, in Obs.laws]
eo_or_top [lemma, in Obs.laws]
eo_and_bot [lemma, in Obs.laws]
eo_impl_distr [lemma, in Obs.laws]
eo_impl_concl [lemma, in Obs.laws]
eo_impl_premise [lemma, in Obs.laws]
eo_tauto [lemma, in Obs.laws]
eo_abs2 [lemma, in Obs.laws]
eo_abs1 [lemma, in Obs.laws]
eo_or_bot [lemma, in Obs.laws]
eo_or_comm [lemma, in Obs.laws]
eo_or_ass [lemma, in Obs.laws]
eo_and_top [lemma, in Obs.laws]
eo_and_comm [lemma, in Obs.laws]
eo_and_ass [lemma, in Obs.laws]
eo_ax [constructor, in Obs.equiv_obs]
eo_impl [constructor, in Obs.equiv_obs]
eo_and [constructor, in Obs.equiv_obs]
eo_or [constructor, in Obs.equiv_obs]
eo_trans [constructor, in Obs.equiv_obs]
eo_sym [constructor, in Obs.equiv_obs]
eo_re [constructor, in Obs.equiv_obs]
eo_prod_impl [lemma, in Obs.product]
eo_sound [lemma, in Obs.sem_obs]
eo_ax_complete [lemma, in Obs.fan]
eo_inf_dec [lemma, in Obs.fan]
eo_inf_complete [lemma, in Obs.fan]
eo_fan_clique_neg [lemma, in Obs.fan]
eo_Ω_neg [lemma, in Obs.anticlique]
eo_Ω_top' [lemma, in Obs.anticlique]
equal_list_spec [lemma, in Obs.list_dec]
equal_list [definition, in Obs.list_dec]
equivalent [definition, in Obs.list_tools]
equivalentb [definition, in Obs.list_dec]
equivalentb_spec [lemma, in Obs.list_dec]
equivalent_lift_prod_Proper [instance, in Obs.list_tools]
equivalent_flat_map_Proper [instance, in Obs.list_tools]
equivalent_rev_Proper [instance, in Obs.list_tools]
equivalent_cons_Proper [instance, in Obs.list_tools]
equivalent_app_Proper [instance, in Obs.list_tools]
equivalent_Equivalence [instance, in Obs.list_tools]
equiv_obs_equiv [instance, in Obs.equiv_obs]
equiv_Obs [inductive, in Obs.equiv_obs]
equiv_obs [library]
eqX [projection, in Obs.decidable_prop]
eqX_refl [lemma, in Obs.decidable_prop]
eqX_false [lemma, in Obs.decidable_prop]
eqX_correct [lemma, in Obs.decidable_prop]
eqX_eq [projection, in Obs.decidable_prop]
eq_shuffles [lemma, in Obs.list_tools]
eq_fcliques [abbreviation, in Obs.coherence_graph]
eq_obs_inf_obs [lemma, in Obs.laws]
eq_axΩ_sound [lemma, in Obs.anticlique]
eq𝒱 [definition, in Obs.product]
eq𝒱_proj2 [lemma, in Obs.product]
eq𝒱_proj1 [lemma, in Obs.product]
e:346 [binder, in Obs.list_tools]
e:352 [binder, in Obs.list_tools]
e:356 [binder, in Obs.list_tools]
e:5 [binder, in Obs.notations]
F
FAN [abbreviation, in Obs.fan]fan [library]
FanGraph [record, in Obs.fan]
fanG:3 [binder, in Obs.fin_sem_obs]
FanG:9 [binder, in Obs.fan]
fan_choose_clique [lemma, in Obs.fan]
FAN_sound [lemma, in Obs.fan]
FAN_Obs [instance, in Obs.fan]
fan_clique_neg [constructor, in Obs.fan]
fan_ax [inductive, in Obs.fan]
fcic [definition, in Obs.coherence_graph]
fcic_None [lemma, in Obs.coherence_graph]
fcic_Some [lemma, in Obs.coherence_graph]
fcliques [definition, in Obs.coherence_graph]
fcliques_coherent [lemma, in Obs.coherence_graph]
fcliques_sat_iff_fsat [lemma, in Obs.fin_sem_obs]
fcmem [definition, in Obs.coherence_graph]
fcmem_coh [lemma, in Obs.coherence_graph]
fc_to_clique_iff [lemma, in Obs.coherence_graph]
fc_to_clique_proper_eq [instance, in Obs.coherence_graph]
fc_to_clique_proper [instance, in Obs.coherence_graph]
fc_to_clique_spec [lemma, in Obs.coherence_graph]
fc_to_clique [definition, in Obs.coherence_graph]
filter_equivalent_Proper [instance, in Obs.list_tools]
filter_incl_Proper [instance, in Obs.list_tools]
filter_nil [lemma, in Obs.list_tools]
filter_NoDup [lemma, in Obs.list_tools]
filter_true [lemma, in Obs.list_tools]
filter_ext [lemma, in Obs.list_tools]
filter_ext_In [lemma, in Obs.list_tools]
filter_map [lemma, in Obs.list_tools]
filter_length_lt [lemma, in Obs.list_tools]
filter_length_eq [lemma, in Obs.list_tools]
filter_length [lemma, in Obs.list_tools]
filter_app [lemma, in Obs.list_tools]
fincompatible [definition, in Obs.coherence_graph]
fincompatible_eq [instance, in Obs.coherence_graph]
fincompatible_inf [instance, in Obs.coherence_graph]
fincompatible_incompatible [lemma, in Obs.coherence_graph]
_ @@ _ [notation, in Obs.coherence_graph]
_ ↯↯ _ [notation, in Obs.coherence_graph]
! [notation, in Obs.coherence_graph]
_ ⊃f _ [notation, in Obs.coherence_graph]
finite_cliques [section, in Obs.coherence_graph]
finSat [instance, in Obs.fin_sem_obs]
finsat [definition, in Obs.fan]
finsat_spec [lemma, in Obs.fan]
fin_sem_obs [library]
fjoins [definition, in Obs.coherence_graph]
fjoins_iff_joins [lemma, in Obs.coherence_graph]
fjoins_proper [instance, in Obs.coherence_graph]
flat_map_Join [lemma, in Obs.laws]
flat_map_Meet [lemma, in Obs.laws]
flip [definition, in Obs.list_tools]
flip [section, in Obs.list_tools]
flip_proj2 [lemma, in Obs.list_tools]
flip_proj1 [lemma, in Obs.list_tools]
flip_app [lemma, in Obs.list_tools]
flip_involutive [lemma, in Obs.list_tools]
_ ` [notation, in Obs.list_tools]
forallb_ext [lemma, in Obs.list_tools]
forallb_ext_In [lemma, in Obs.list_tools]
forallb_false_exists [lemma, in Obs.list_tools]
forall_existsb [lemma, in Obs.list_tools]
fsat_impl [lemma, in Obs.fin_sem_obs]
fsat_conj [lemma, in Obs.fin_sem_obs]
fsat_disj [lemma, in Obs.fin_sem_obs]
fsat_at [lemma, in Obs.fin_sem_obs]
fsat_bot [lemma, in Obs.fin_sem_obs]
fsat_top [lemma, in Obs.fin_sem_obs]
f:119 [binder, in Obs.laws]
f:121 [binder, in Obs.list_tools]
f:124 [binder, in Obs.laws]
f:128 [binder, in Obs.laws]
f:130 [binder, in Obs.list_tools]
f:132 [binder, in Obs.list_dec]
f:133 [binder, in Obs.laws]
f:136 [binder, in Obs.list_dec]
f:137 [binder, in Obs.list_tools]
f:14 [binder, in Obs.list_tools]
f:142 [binder, in Obs.list_tools]
f:150 [binder, in Obs.list_tools]
f:199 [binder, in Obs.list_dec]
f:200 [binder, in Obs.list_tools]
f:203 [binder, in Obs.list_tools]
f:205 [binder, in Obs.list_tools]
f:207 [binder, in Obs.list_tools]
f:215 [binder, in Obs.list_dec]
f:218 [binder, in Obs.list_tools]
f:221 [binder, in Obs.list_tools]
f:222 [binder, in Obs.list_dec]
f:223 [binder, in Obs.list_tools]
f:225 [binder, in Obs.list_tools]
f:248 [binder, in Obs.list_tools]
f:253 [binder, in Obs.list_tools]
f:258 [binder, in Obs.list_tools]
f:264 [binder, in Obs.list_tools]
f:268 [binder, in Obs.list_tools]
f:274 [binder, in Obs.list_tools]
f:280 [binder, in Obs.list_tools]
f:359 [binder, in Obs.list_tools]
f:364 [binder, in Obs.list_tools]
f:368 [binder, in Obs.list_tools]
f:372 [binder, in Obs.list_tools]
f:376 [binder, in Obs.list_tools]
f:381 [binder, in Obs.list_tools]
f:386 [binder, in Obs.list_tools]
f:391 [binder, in Obs.list_tools]
f:397 [binder, in Obs.list_tools]
f:402 [binder, in Obs.list_tools]
f:406 [binder, in Obs.list_tools]
f:411 [binder, in Obs.list_tools]
f:418 [binder, in Obs.list_tools]
f:45 [binder, in Obs.list_tools]
f:49 [binder, in Obs.list_tools]
f:52 [binder, in Obs.list_tools]
f:56 [binder, in Obs.list_tools]
f:58 [binder, in Obs.list_dec]
f:60 [binder, in Obs.list_dec]
f:61 [binder, in Obs.list_tools]
f:66 [binder, in Obs.list_tools]
f:71 [binder, in Obs.list_tools]
f:78 [binder, in Obs.list_tools]
G
Graph [record, in Obs.coherence_graph]G:1 [binder, in Obs.laws]
G:1 [binder, in Obs.equiv_obs]
G:1 [binder, in Obs.fin_sem_obs]
G:1 [binder, in Obs.sem_obs]
G:1 [binder, in Obs.fan]
G:1 [binder, in Obs.syntax_obs]
g:120 [binder, in Obs.laws]
g:129 [binder, in Obs.laws]
g:254 [binder, in Obs.list_tools]
g:259 [binder, in Obs.list_tools]
g:269 [binder, in Obs.list_tools]
g:275 [binder, in Obs.list_tools]
g:281 [binder, in Obs.list_tools]
g:377 [binder, in Obs.list_tools]
g:382 [binder, in Obs.list_tools]
g:387 [binder, in Obs.list_tools]
g:392 [binder, in Obs.list_tools]
g:398 [binder, in Obs.list_tools]
G:4 [binder, in Obs.syntax_obs]
g:407 [binder, in Obs.list_tools]
g:412 [binder, in Obs.list_tools]
G:5 [binder, in Obs.syntax_obs]
G:55 [binder, in Obs.coherence_graph]
G:6 [binder, in Obs.coherence_graph]
G:6 [binder, in Obs.syntax_obs]
G:60 [binder, in Obs.sem_obs]
G:61 [binder, in Obs.coherence_graph]
g:62 [binder, in Obs.list_tools]
g:67 [binder, in Obs.list_tools]
G:7 [binder, in Obs.fan]
g:72 [binder, in Obs.list_tools]
G:88 [binder, in Obs.coherence_graph]
H
HA_A [lemma, in Obs.laws]ha_impl_distr [constructor, in Obs.equiv_obs]
ha_impl_concl [constructor, in Obs.equiv_obs]
ha_impl_premise [constructor, in Obs.equiv_obs]
ha_tauto [constructor, in Obs.equiv_obs]
ha_abs2 [constructor, in Obs.equiv_obs]
ha_abs1 [constructor, in Obs.equiv_obs]
ha_or_bot [constructor, in Obs.equiv_obs]
ha_or_comm [constructor, in Obs.equiv_obs]
ha_or_ass [constructor, in Obs.equiv_obs]
ha_and_top [constructor, in Obs.equiv_obs]
ha_and_comm [constructor, in Obs.equiv_obs]
ha_and_ass [constructor, in Obs.equiv_obs]
ha_ax [inductive, in Obs.equiv_obs]
ha_sound [lemma, in Obs.sem_obs]
H0:198 [binder, in Obs.list_dec]
H0:207 [binder, in Obs.list_dec]
H0:214 [binder, in Obs.list_dec]
H0:221 [binder, in Obs.list_dec]
H:197 [binder, in Obs.list_dec]
H:206 [binder, in Obs.list_dec]
H:213 [binder, in Obs.list_dec]
H:220 [binder, in Obs.list_dec]
h:393 [binder, in Obs.list_tools]
H:53 [binder, in Obs.sem_obs]
H:54 [binder, in Obs.decidable_prop]
H:56 [binder, in Obs.decidable_prop]
H:57 [binder, in Obs.sem_obs]
H:59 [binder, in Obs.sem_obs]
H:61 [binder, in Obs.decidable_prop]
H:9 [binder, in Obs.notations]
I
Idx:1 [binder, in Obs.product]idx:133 [binder, in Obs.product]
idx:137 [binder, in Obs.product]
impl_Join [lemma, in Obs.laws]
impl_lst_spec [lemma, in Obs.fin_sem_obs]
impl_lst [definition, in Obs.fin_sem_obs]
impl_disj_cliques [lemma, in Obs.fan]
impl_disj [lemma, in Obs.fan]
impl_cliques [lemma, in Obs.fan]
inb [definition, in Obs.list_dec]
inb_dec [lemma, in Obs.list_dec]
inb_false [lemma, in Obs.list_dec]
inb_spec [lemma, in Obs.list_dec]
inclb [definition, in Obs.list_dec]
inclb_correct [lemma, in Obs.list_dec]
incl_cons_disj' [lemma, in Obs.list_tools]
incl_cons_disj [lemma, in Obs.list_tools]
incl_split [lemma, in Obs.list_tools]
incl_app_split [lemma, in Obs.list_tools]
incl_app_or [lemma, in Obs.list_tools]
incl_nil [lemma, in Obs.list_tools]
incl_lift_prod_Proper [instance, in Obs.list_tools]
incl_flat_map_Proper [instance, in Obs.list_tools]
incl_rev_Proper [instance, in Obs.list_tools]
incl_cons_Proper [instance, in Obs.list_tools]
incl_app_Proper [instance, in Obs.list_tools]
incl_PartialOrder [instance, in Obs.list_tools]
incl_PreOrder [instance, in Obs.list_tools]
incl_map [lemma, in Obs.list_tools]
incl_sem_iff_incl_fin_sem [lemma, in Obs.fin_sem_obs]
incoh [definition, in Obs.coherence_graph]
incoh_sym [instance, in Obs.coherence_graph]
incoh_irrefl [instance, in Obs.coherence_graph]
incoh_iff_same_component_and_incoh [lemma, in Obs.product]
incompat [projection, in Obs.coherence_graph]
incompatible [definition, in Obs.coherence_graph]
incompatible_or_joins_f [lemma, in Obs.coherence_graph]
incompatible_eq [instance, in Obs.coherence_graph]
incompatible_inf [instance, in Obs.coherence_graph]
incompatible_incompat [lemma, in Obs.coherence_graph]
incompat_dec [instance, in Obs.coherence_graph]
incompat_are_incoh [lemma, in Obs.coherence_graph]
incompat_None [projection, in Obs.coherence_graph]
incompat_Some [projection, in Obs.coherence_graph]
incompat_project [definition, in Obs.product]
incompat_inject [definition, in Obs.product]
inf_fcliques [abbreviation, in Obs.coherence_graph]
inf_fcliques [abbreviation, in Obs.coherence_graph]
inf_cliques [abbreviation, in Obs.coherence_graph]
inf_clique_compat [lemma, in Obs.coherence_graph]
inf_cliques [abbreviation, in Obs.coherence_graph]
inf_obs_partialorder [instance, in Obs.laws]
inf_obs_preorder [instance, in Obs.laws]
inf_obs [definition, in Obs.equiv_obs]
inf_axΩ_sound [lemma, in Obs.anticlique]
inf__Ω [definition, in Obs.anticlique]
inject [definition, in Obs.product]
inject_i_incompat [lemma, in Obs.product]
inject_i_member [lemma, in Obs.product]
insert [definition, in Obs.list_tools]
insert_spec [lemma, in Obs.list_tools]
insert_map [lemma, in Obs.list_dec]
interect_nil [lemma, in Obs.list_dec]
intersect [definition, in Obs.list_dec]
intersect_incl [lemma, in Obs.list_dec]
intersect_meet_l [lemma, in Obs.list_dec]
intersect_comm [lemma, in Obs.list_dec]
intersect_ass [lemma, in Obs.list_dec]
intersect_app_r [lemma, in Obs.list_dec]
intersect_app_l [lemma, in Obs.list_dec]
intersect_proper [instance, in Obs.list_dec]
intersect_proper_incl [instance, in Obs.list_dec]
intersect_spec [lemma, in Obs.list_dec]
In_shuffles [lemma, in Obs.list_tools]
In_equivalent_Proper [instance, in Obs.list_tools]
In_incl_Proper [instance, in Obs.list_tools]
In_flip [lemma, in Obs.list_tools]
in_concat [lemma, in Obs.list_tools]
in_cons_iff [lemma, in Obs.list_dec]
In_undup [lemma, in Obs.list_dec]
In_dec [lemma, in Obs.list_dec]
irrefl_fincompatible [instance, in Obs.coherence_graph]
irrefl_incompatible [instance, in Obs.coherence_graph]
is_coherent_project_list [lemma, in Obs.coherence_graph]
is_coherent [definition, in Obs.coherence_graph]
Is_true_iff_eq_true [lemma, in Obs.decidable_prop]
Is_true_dec [instance, in Obs.decidable_prop]
Is_true_test [lemma, in Obs.decidable_prop]
i:102 [binder, in Obs.product]
i:103 [binder, in Obs.product]
i:104 [binder, in Obs.product]
i:107 [binder, in Obs.product]
i:108 [binder, in Obs.product]
i:109 [binder, in Obs.product]
i:11 [binder, in Obs.product]
i:112 [binder, in Obs.product]
i:119 [binder, in Obs.product]
i:121 [binder, in Obs.product]
i:125 [binder, in Obs.product]
i:130 [binder, in Obs.product]
i:136 [binder, in Obs.product]
i:140 [binder, in Obs.product]
i:141 [binder, in Obs.product]
i:142 [binder, in Obs.product]
I:144 [binder, in Obs.product]
i:146 [binder, in Obs.product]
I:148 [binder, in Obs.product]
i:15 [binder, in Obs.product]
i:150 [binder, in Obs.product]
I:151 [binder, in Obs.product]
i:156 [binder, in Obs.product]
I:158 [binder, in Obs.product]
i:163 [binder, in Obs.product]
I:165 [binder, in Obs.product]
I:167 [binder, in Obs.product]
I:169 [binder, in Obs.product]
I:171 [binder, in Obs.product]
I:177 [binder, in Obs.product]
I:180 [binder, in Obs.product]
i:183 [binder, in Obs.product]
i:19 [binder, in Obs.product]
i:192 [binder, in Obs.product]
i:201 [binder, in Obs.product]
i:202 [binder, in Obs.product]
i:205 [binder, in Obs.product]
i:208 [binder, in Obs.product]
i:212 [binder, in Obs.product]
i:214 [binder, in Obs.product]
i:215 [binder, in Obs.product]
I:216 [binder, in Obs.product]
i:24 [binder, in Obs.product]
i:27 [binder, in Obs.product]
i:33 [binder, in Obs.product]
i:36 [binder, in Obs.product]
i:4 [binder, in Obs.product]
i:40 [binder, in Obs.product]
i:44 [binder, in Obs.product]
i:47 [binder, in Obs.product]
i:51 [binder, in Obs.product]
i:55 [binder, in Obs.product]
i:59 [binder, in Obs.product]
i:6 [binder, in Obs.product]
i:62 [binder, in Obs.product]
i:66 [binder, in Obs.product]
i:69 [binder, in Obs.product]
i:71 [binder, in Obs.product]
i:78 [binder, in Obs.product]
i:8 [binder, in Obs.product]
i:82 [binder, in Obs.product]
i:83 [binder, in Obs.product]
i:87 [binder, in Obs.product]
I:90 [binder, in Obs.product]
i:91 [binder, in Obs.product]
i:95 [binder, in Obs.product]
i:98 [binder, in Obs.product]
i:99 [binder, in Obs.product]
J
jleft [constructor, in Obs.equiv_obs]join [inductive, in Obs.equiv_obs]
Join [definition, in Obs.syntax_obs]
joins [definition, in Obs.coherence_graph]
joins_is_meet_f [lemma, in Obs.coherence_graph]
joins_is_meet [lemma, in Obs.coherence_graph]
joins_proper [instance, in Obs.coherence_graph]
Join_map_equiv_pointwise [lemma, in Obs.laws]
Join_equiv [instance, in Obs.laws]
Join_monotone [instance, in Obs.laws]
Join_and_Join [lemma, in Obs.laws]
Join_app [lemma, in Obs.laws]
join_proper_right [instance, in Obs.equiv_obs]
join_proper_left [instance, in Obs.equiv_obs]
join_project' [lemma, in Obs.product]
join_project [lemma, in Obs.product]
join__f [definition, in Obs.fan]
jright [constructor, in Obs.equiv_obs]
j:157 [binder, in Obs.product]
j:16 [binder, in Obs.product]
j:164 [binder, in Obs.product]
J:178 [binder, in Obs.product]
J:181 [binder, in Obs.product]
j:221 [binder, in Obs.product]
j:28 [binder, in Obs.product]
j:75 [binder, in Obs.product]
K
k:290 [binder, in Obs.list_tools]k:299 [binder, in Obs.list_tools]
k:325 [binder, in Obs.list_tools]
L
laws [library]length_app_tail [lemma, in Obs.list_tools]
length_app [lemma, in Obs.list_tools]
length_sum_filter [lemma, in Obs.list_dec]
len_rev_induction [lemma, in Obs.list_tools]
len_induction [lemma, in Obs.list_tools]
Levi [lemma, in Obs.list_tools]
Levi_strict [lemma, in Obs.list_tools]
le_plus_Proper [instance, in Obs.list_tools]
lift_prod_spec [lemma, in Obs.list_tools]
lift_prod [definition, in Obs.list_tools]
lists_of_length_spec [lemma, in Obs.list_tools]
lists_of_length [definition, in Obs.list_tools]
list_tools [library]
list_dec [library]
lt_plus_Proper [instance, in Obs.list_tools]
l':42 [binder, in Obs.list_tools]
l1:132 [binder, in Obs.list_tools]
l1:161 [binder, in Obs.list_tools]
l1:23 [binder, in Obs.list_dec]
l1:245 [binder, in Obs.list_tools]
l1:25 [binder, in Obs.list_dec]
l1:29 [binder, in Obs.list_dec]
l1:41 [binder, in Obs.decidable_prop]
l1:43 [binder, in Obs.decidable_prop]
l1:431 [binder, in Obs.list_tools]
l1:441 [binder, in Obs.list_tools]
l1:443 [binder, in Obs.list_tools]
l1:445 [binder, in Obs.list_tools]
l1:84 [binder, in Obs.list_dec]
l1:85 [binder, in Obs.list_tools]
l1:90 [binder, in Obs.list_tools]
l1:94 [binder, in Obs.list_dec]
l1:98 [binder, in Obs.list_dec]
l2:133 [binder, in Obs.list_tools]
l2:163 [binder, in Obs.list_tools]
l2:24 [binder, in Obs.list_dec]
l2:246 [binder, in Obs.list_tools]
l2:26 [binder, in Obs.list_dec]
l2:30 [binder, in Obs.list_dec]
l2:42 [binder, in Obs.decidable_prop]
l2:432 [binder, in Obs.list_tools]
l2:44 [binder, in Obs.decidable_prop]
l2:442 [binder, in Obs.list_tools]
l2:444 [binder, in Obs.list_tools]
l2:446 [binder, in Obs.list_tools]
l2:85 [binder, in Obs.list_dec]
l2:86 [binder, in Obs.list_tools]
l2:91 [binder, in Obs.list_tools]
l2:95 [binder, in Obs.list_dec]
l2:99 [binder, in Obs.list_dec]
l3:162 [binder, in Obs.list_tools]
l4:164 [binder, in Obs.list_tools]
l:103 [binder, in Obs.list_dec]
l:105 [binder, in Obs.list_dec]
l:107 [binder, in Obs.list_dec]
l:109 [binder, in Obs.list_dec]
l:11 [binder, in Obs.list_dec]
l:110 [binder, in Obs.product]
l:111 [binder, in Obs.list_dec]
l:113 [binder, in Obs.product]
l:113 [binder, in Obs.list_dec]
l:114 [binder, in Obs.list_tools]
l:116 [binder, in Obs.product]
l:116 [binder, in Obs.list_dec]
l:117 [binder, in Obs.list_tools]
l:119 [binder, in Obs.list_dec]
l:121 [binder, in Obs.laws]
l:121 [binder, in Obs.list_dec]
l:122 [binder, in Obs.list_tools]
l:125 [binder, in Obs.list_tools]
l:125 [binder, in Obs.laws]
L:127 [binder, in Obs.list_tools]
l:13 [binder, in Obs.list_tools]
l:13 [binder, in Obs.list_dec]
l:130 [binder, in Obs.laws]
l:133 [binder, in Obs.list_dec]
l:134 [binder, in Obs.laws]
l:137 [binder, in Obs.list_dec]
l:138 [binder, in Obs.list_tools]
l:141 [binder, in Obs.list_dec]
l:143 [binder, in Obs.list_tools]
l:15 [binder, in Obs.list_dec]
l:151 [binder, in Obs.list_tools]
l:157 [binder, in Obs.list_tools]
l:161 [binder, in Obs.coherence_graph]
l:163 [binder, in Obs.coherence_graph]
l:165 [binder, in Obs.list_tools]
l:165 [binder, in Obs.coherence_graph]
l:167 [binder, in Obs.coherence_graph]
l:17 [binder, in Obs.fan]
l:17 [binder, in Obs.list_dec]
l:170 [binder, in Obs.coherence_graph]
l:172 [binder, in Obs.coherence_graph]
l:174 [binder, in Obs.coherence_graph]
l:176 [binder, in Obs.coherence_graph]
l:178 [binder, in Obs.list_tools]
l:179 [binder, in Obs.coherence_graph]
l:18 [binder, in Obs.list_tools]
l:186 [binder, in Obs.list_tools]
l:19 [binder, in Obs.list_tools]
l:192 [binder, in Obs.list_dec]
l:203 [binder, in Obs.list_dec]
l:213 [binder, in Obs.list_tools]
l:216 [binder, in Obs.list_dec]
L:22 [binder, in Obs.fan]
l:223 [binder, in Obs.list_dec]
l:226 [binder, in Obs.list_dec]
l:228 [binder, in Obs.list_dec]
l:23 [binder, in Obs.list_tools]
l:231 [binder, in Obs.list_dec]
l:233 [binder, in Obs.list_tools]
l:237 [binder, in Obs.list_tools]
l:239 [binder, in Obs.list_tools]
l:242 [binder, in Obs.list_tools]
l:249 [binder, in Obs.list_tools]
l:25 [binder, in Obs.list_tools]
l:255 [binder, in Obs.list_tools]
L:26 [binder, in Obs.fan]
l:260 [binder, in Obs.list_tools]
l:263 [binder, in Obs.list_tools]
l:27 [binder, in Obs.fan]
l:270 [binder, in Obs.list_tools]
l:276 [binder, in Obs.list_tools]
l:28 [binder, in Obs.list_dec]
l:282 [binder, in Obs.list_tools]
l:29 [binder, in Obs.list_tools]
l:3 [binder, in Obs.list_tools]
l:3 [binder, in Obs.list_dec]
l:3 [binder, in Obs.anticlique]
l:309 [binder, in Obs.list_tools]
l:31 [binder, in Obs.list_tools]
l:313 [binder, in Obs.list_tools]
l:318 [binder, in Obs.list_tools]
l:321 [binder, in Obs.list_tools]
l:326 [binder, in Obs.list_tools]
l:329 [binder, in Obs.list_tools]
l:336 [binder, in Obs.list_tools]
l:345 [binder, in Obs.list_tools]
l:35 [binder, in Obs.list_tools]
l:350 [binder, in Obs.list_tools]
l:353 [binder, in Obs.list_tools]
l:357 [binder, in Obs.list_tools]
l:360 [binder, in Obs.list_tools]
l:365 [binder, in Obs.list_tools]
l:369 [binder, in Obs.list_tools]
l:373 [binder, in Obs.list_tools]
l:378 [binder, in Obs.list_tools]
l:383 [binder, in Obs.list_tools]
l:388 [binder, in Obs.list_tools]
l:39 [binder, in Obs.fan]
l:394 [binder, in Obs.list_tools]
l:399 [binder, in Obs.list_tools]
l:403 [binder, in Obs.list_tools]
l:408 [binder, in Obs.list_tools]
l:41 [binder, in Obs.list_tools]
l:41 [binder, in Obs.fan]
l:413 [binder, in Obs.list_tools]
l:419 [binder, in Obs.list_tools]
l:42 [binder, in Obs.list_dec]
l:422 [binder, in Obs.list_tools]
l:425 [binder, in Obs.list_tools]
l:429 [binder, in Obs.list_tools]
l:433 [binder, in Obs.list_tools]
l:435 [binder, in Obs.list_tools]
l:437 [binder, in Obs.list_tools]
l:439 [binder, in Obs.list_tools]
l:447 [binder, in Obs.list_tools]
l:45 [binder, in Obs.list_dec]
l:453 [binder, in Obs.list_tools]
l:456 [binder, in Obs.list_tools]
l:46 [binder, in Obs.list_tools]
l:47 [binder, in Obs.list_dec]
l:48 [binder, in Obs.list_dec]
l:49 [binder, in Obs.list_dec]
l:50 [binder, in Obs.list_tools]
l:50 [binder, in Obs.list_dec]
l:52 [binder, in Obs.list_dec]
l:53 [binder, in Obs.list_tools]
l:53 [binder, in Obs.list_dec]
l:57 [binder, in Obs.list_tools]
l:57 [binder, in Obs.list_dec]
l:59 [binder, in Obs.list_dec]
l:6 [binder, in Obs.list_tools]
l:6 [binder, in Obs.list_dec]
l:63 [binder, in Obs.list_tools]
l:63 [binder, in Obs.list_dec]
l:64 [binder, in Obs.list_dec]
l:66 [binder, in Obs.list_dec]
l:68 [binder, in Obs.list_tools]
l:70 [binder, in Obs.list_dec]
l:72 [binder, in Obs.list_dec]
l:73 [binder, in Obs.list_tools]
l:73 [binder, in Obs.decidable_prop]
l:76 [binder, in Obs.list_tools]
l:76 [binder, in Obs.list_dec]
l:78 [binder, in Obs.list_dec]
l:79 [binder, in Obs.list_tools]
l:80 [binder, in Obs.decidable_prop]
l:82 [binder, in Obs.list_tools]
l:82 [binder, in Obs.list_dec]
l:87 [binder, in Obs.list_dec]
l:88 [binder, in Obs.list_dec]
l:9 [binder, in Obs.list_tools]
l:9 [binder, in Obs.list_dec]
l:91 [binder, in Obs.list_dec]
M
mapNF [definition, in Obs.product]map_eq_equivalent [lemma, in Obs.list_tools]
map_ext_in_iff [lemma, in Obs.list_tools]
map_bij [lemma, in Obs.list_tools]
map_eq_id [lemma, in Obs.list_tools]
map_equivalent_Proper [instance, in Obs.list_tools]
map_incl_Proper [instance, in Obs.list_tools]
map_app_inverse [lemma, in Obs.list_tools]
map_undup_inj [lemma, in Obs.list_dec]
map_undup_id [lemma, in Obs.list_dec]
Meet [definition, in Obs.syntax_obs]
Meet_impl [lemma, in Obs.laws]
Meet_map_equiv_pointwise [lemma, in Obs.laws]
Meet_equiv [instance, in Obs.laws]
Meet_monotone [instance, in Obs.laws]
Meet_or_Meet [lemma, in Obs.laws]
Meet_app [lemma, in Obs.laws]
Meet_not_and_sgl_in [lemma, in Obs.anticlique]
Meet_not_and_sgl_not_in [lemma, in Obs.anticlique]
member [projection, in Obs.coherence_graph]
members_are_coh [projection, in Obs.coherence_graph]
mem_is_sgl [lemma, in Obs.anticlique]
mix [definition, in Obs.list_tools]
mix [section, in Obs.list_tools]
mix_app [lemma, in Obs.list_tools]
mix_snd [lemma, in Obs.list_tools]
mix_fst [lemma, in Obs.list_tools]
mix.same_length [variable, in Obs.list_tools]
_ ⋈ _ [notation, in Obs.list_tools]
m':319 [binder, in Obs.list_tools]
m':323 [binder, in Obs.list_tools]
m':454 [binder, in Obs.list_tools]
m1:134 [binder, in Obs.list_tools]
m1:87 [binder, in Obs.list_tools]
m1:92 [binder, in Obs.list_tools]
m1:96 [binder, in Obs.list_dec]
m2:135 [binder, in Obs.list_tools]
m2:88 [binder, in Obs.list_tools]
m2:93 [binder, in Obs.list_tools]
m2:97 [binder, in Obs.list_dec]
m:10 [binder, in Obs.list_tools]
m:100 [binder, in Obs.list_dec]
m:115 [binder, in Obs.list_tools]
m:118 [binder, in Obs.list_tools]
m:122 [binder, in Obs.list_dec]
m:126 [binder, in Obs.list_tools]
m:131 [binder, in Obs.list_tools]
m:134 [binder, in Obs.list_dec]
m:138 [binder, in Obs.list_dec]
m:139 [binder, in Obs.list_tools]
m:140 [binder, in Obs.list_dec]
m:144 [binder, in Obs.list_tools]
m:152 [binder, in Obs.list_tools]
m:158 [binder, in Obs.list_tools]
m:179 [binder, in Obs.list_tools]
m:180 [binder, in Obs.coherence_graph]
m:187 [binder, in Obs.list_tools]
m:229 [binder, in Obs.list_dec]
m:232 [binder, in Obs.list_dec]
m:234 [binder, in Obs.list_tools]
m:24 [binder, in Obs.list_tools]
m:240 [binder, in Obs.list_tools]
m:243 [binder, in Obs.list_tools]
m:283 [binder, in Obs.list_tools]
m:30 [binder, in Obs.list_tools]
m:314 [binder, in Obs.list_tools]
m:317 [binder, in Obs.list_tools]
m:322 [binder, in Obs.list_tools]
m:366 [binder, in Obs.list_tools]
m:370 [binder, in Obs.list_tools]
m:374 [binder, in Obs.list_tools]
m:4 [binder, in Obs.list_dec]
m:430 [binder, in Obs.list_tools]
m:434 [binder, in Obs.list_tools]
m:436 [binder, in Obs.list_tools]
m:438 [binder, in Obs.list_tools]
m:440 [binder, in Obs.list_tools]
m:448 [binder, in Obs.list_tools]
m:449 [binder, in Obs.list_tools]
m:452 [binder, in Obs.list_tools]
m:457 [binder, in Obs.list_tools]
m:47 [binder, in Obs.list_tools]
m:54 [binder, in Obs.list_dec]
m:7 [binder, in Obs.list_dec]
m:92 [binder, in Obs.list_dec]
N
NatNum [instance, in Obs.decidable_prop]nb [abbreviation, in Obs.list_dec]
nb [abbreviation, in Obs.list_dec]
nb_map [lemma, in Obs.list_dec]
nb_cons_eq [lemma, in Obs.list_dec]
nb_cons_neq [lemma, in Obs.list_dec]
nb_inv_nil [lemma, in Obs.list_dec]
nb_not_In [lemma, in Obs.list_dec]
nb_In [lemma, in Obs.list_dec]
nb_nil [lemma, in Obs.list_dec]
nb_count_occ [lemma, in Obs.list_dec]
nc:155 [binder, in Obs.product]
nd:162 [binder, in Obs.product]
neg_top'_is_bot [lemma, in Obs.anticlique]
neg_neg_axΩ [lemma, in Obs.anticlique]
NF [definition, in Obs.product]
nf [definition, in Obs.fan]
nf_spec [lemma, in Obs.fan]
nil_or_last [lemma, in Obs.list_tools]
node [constructor, in Obs.product]
NoDupb [definition, in Obs.list_dec]
NoDupb_NoDup [lemma, in Obs.list_dec]
NoDup_shuffles [lemma, in Obs.list_tools]
NoDup_app [lemma, in Obs.list_tools]
NoDup_app_inv [lemma, in Obs.list_tools]
NoDup_remove_3 [lemma, in Obs.list_tools]
NoDup_nb' [lemma, in Obs.list_dec]
NoDup_nb [lemma, in Obs.list_dec]
NoDup_length [lemma, in Obs.list_dec]
NoDup_rev [lemma, in Obs.list_dec]
NoDup_undup_eq [lemma, in Obs.list_dec]
NoDup_undup [lemma, in Obs.list_dec]
normal_form_eq [lemma, in Obs.product]
normal_form_sup [lemma, in Obs.product]
normal_form [definition, in Obs.product]
notations [library]
not_nil_add [lemma, in Obs.list_tools]
not_incompatible_is_joins_f [lemma, in Obs.coherence_graph]
not_incompatible_is_joins [lemma, in Obs.coherence_graph]
n:10 [binder, in Obs.list_dec]
n:12 [binder, in Obs.list_dec]
n:14 [binder, in Obs.list_dec]
n:145 [binder, in Obs.product]
n:149 [binder, in Obs.product]
n:153 [binder, in Obs.list_tools]
n:16 [binder, in Obs.list_dec]
n:211 [binder, in Obs.product]
n:213 [binder, in Obs.product]
n:244 [binder, in Obs.list_tools]
n:303 [binder, in Obs.list_tools]
n:342 [binder, in Obs.list_tools]
n:349 [binder, in Obs.list_tools]
n:8 [binder, in Obs.list_dec]
n:91 [binder, in Obs.decidable_prop]
O
O [abbreviation, in Obs.equiv_obs]Obs [abbreviation, in Obs.equiv_obs]
observation [inductive, in Obs.syntax_obs]
obs_Join [lemma, in Obs.laws]
obs_Meet [lemma, in Obs.laws]
obs_meet [lemma, in Obs.laws]
obs_join [lemma, in Obs.laws]
obs_clique_obs [constructor, in Obs.equiv_obs]
obs_clique_impl [constructor, in Obs.equiv_obs]
obs_incoh [constructor, in Obs.equiv_obs]
obs_ax [inductive, in Obs.equiv_obs]
Obs_sound [lemma, in Obs.sem_obs]
Obs__Ω [definition, in Obs.anticlique]
Obs' [abbreviation, in Obs.equiv_obs]
obs'_ax [inductive, in Obs.equiv_obs]
Obs'_sound [lemma, in Obs.sem_obs]
obs𝖦_to_𝒯_proper_inf [instance, in Obs.product]
obs𝖦_to_𝒯_proper [instance, in Obs.product]
obs𝖦_to_𝒯_sat [lemma, in Obs.product]
obs𝖦_to_𝒯 [definition, in Obs.product]
orb_prop_iff [lemma, in Obs.decidable_prop]
or_Meet [lemma, in Obs.laws]
o_impl_inf [instance, in Obs.laws]
o_and_inf [instance, in Obs.laws]
o_or_inf [instance, in Obs.laws]
o_impl_equiv [instance, in Obs.equiv_obs]
o_or_equiv [instance, in Obs.equiv_obs]
o_and_equiv [instance, in Obs.equiv_obs]
o_impl [constructor, in Obs.syntax_obs]
o_and [constructor, in Obs.syntax_obs]
o_or [constructor, in Obs.syntax_obs]
o_obs [constructor, in Obs.syntax_obs]
o_false [constructor, in Obs.syntax_obs]
o_true [constructor, in Obs.syntax_obs]
o1:13 [binder, in Obs.sem_obs]
o1:16 [binder, in Obs.sem_obs]
o1:19 [binder, in Obs.sem_obs]
o1:28 [binder, in Obs.fin_sem_obs]
o1:31 [binder, in Obs.fin_sem_obs]
o1:34 [binder, in Obs.fin_sem_obs]
o2:14 [binder, in Obs.sem_obs]
o2:17 [binder, in Obs.sem_obs]
o2:20 [binder, in Obs.sem_obs]
o2:29 [binder, in Obs.fin_sem_obs]
o2:32 [binder, in Obs.fin_sem_obs]
o2:35 [binder, in Obs.fin_sem_obs]
o:18 [binder, in Obs.fin_sem_obs]
o:28 [binder, in Obs.anticlique]
o:4 [binder, in Obs.sem_obs]
o:55 [binder, in Obs.anticlique]
o:59 [binder, in Obs.anticlique]
o:6 [binder, in Obs.notations]
o:61 [binder, in Obs.anticlique]
o:63 [binder, in Obs.anticlique]
P
pad [definition, in Obs.list_tools]pad_contents [lemma, in Obs.list_tools]
pairs [definition, in Obs.list_tools]
pairs_spec [lemma, in Obs.list_tools]
PartialOrder_subrelation [instance, in Obs.notations]
prj1 [abbreviation, in Obs.list_tools]
prj2 [abbreviation, in Obs.list_tools]
product [library]
product_choose_clique [lemma, in Obs.product]
product_sat_dec [instance, in Obs.product]
prod_impl [constructor, in Obs.product]
prod_idx [constructor, in Obs.product]
prod_ax [inductive, in Obs.product]
project [definition, in Obs.coherence_graph]
project [definition, in Obs.product]
project_proper_inf [instance, in Obs.coherence_graph]
project_proper [instance, in Obs.coherence_graph]
project_project [lemma, in Obs.coherence_graph]
project_max [lemma, in Obs.coherence_graph]
project_larger [lemma, in Obs.coherence_graph]
project_incl [lemma, in Obs.coherence_graph]
project_spec [lemma, in Obs.coherence_graph]
project_proof [lemma, in Obs.coherence_graph]
project_list [definition, in Obs.coherence_graph]
project_inject [lemma, in Obs.product]
project_spec [lemma, in Obs.product]
proj_length [lemma, in Obs.list_tools]
p1:63 [binder, in Obs.decidable_prop]
p1:65 [binder, in Obs.decidable_prop]
p1:67 [binder, in Obs.decidable_prop]
p1:69 [binder, in Obs.decidable_prop]
p2:64 [binder, in Obs.decidable_prop]
p2:66 [binder, in Obs.decidable_prop]
p2:68 [binder, in Obs.decidable_prop]
p2:70 [binder, in Obs.decidable_prop]
p:113 [binder, in Obs.laws]
p:116 [binder, in Obs.laws]
P:16 [binder, in Obs.list_tools]
p:16 [binder, in Obs.fan]
p:191 [binder, in Obs.product]
P:21 [binder, in Obs.list_tools]
p:235 [binder, in Obs.list_tools]
p:25 [binder, in Obs.fan]
P:27 [binder, in Obs.list_tools]
P:417 [binder, in Obs.list_tools]
P:45 [binder, in Obs.decidable_prop]
p:50 [binder, in Obs.equiv_obs]
p:51 [binder, in Obs.decidable_prop]
p:53 [binder, in Obs.decidable_prop]
p:55 [binder, in Obs.decidable_prop]
p:55 [binder, in Obs.equiv_obs]
p:59 [binder, in Obs.decidable_prop]
p:62 [binder, in Obs.decidable_prop]
p:72 [binder, in Obs.decidable_prop]
p:79 [binder, in Obs.decidable_prop]
P:81 [binder, in Obs.list_tools]
p:85 [binder, in Obs.decidable_prop]
Q
q:86 [binder, in Obs.decidable_prop]R
rev_equivalent [lemma, in Obs.list_tools]rev_induction [lemma, in Obs.list_tools]
rm [definition, in Obs.list_dec]
rmfst [definition, in Obs.list_dec]
rmfst_flip [lemma, in Obs.list_dec]
rmfst_app_dec [lemma, in Obs.list_dec]
rmfst_comm [lemma, in Obs.list_dec]
rmfst_decr [lemma, in Obs.list_dec]
rmfst_in [lemma, in Obs.list_dec]
rmfst_notin [lemma, in Obs.list_dec]
rm_notin [lemma, in Obs.list_dec]
rm_incl_Proper [instance, in Obs.list_dec]
rm_equivalent_Proper [instance, in Obs.list_dec]
rm_equiv [lemma, in Obs.list_dec]
rm_In [lemma, in Obs.list_dec]
r:330 [binder, in Obs.list_tools]
r:337 [binder, in Obs.list_tools]
S
s [section, in Obs.coherence_graph]s [section, in Obs.laws]
s [section, in Obs.equiv_obs]
s [section, in Obs.fin_sem_obs]
s [section, in Obs.product]
s [section, in Obs.sem_obs]
s [section, in Obs.fan]
s [section, in Obs.anticlique]
satClique [instance, in Obs.coherence_graph]
Satisfaction [record, in Obs.notations]
Satisfaction [inductive, in Obs.notations]
satisfies [projection, in Obs.notations]
satisfies [constructor, in Obs.notations]
satisfies_Meet [lemma, in Obs.sem_obs]
satisfies_Join [lemma, in Obs.sem_obs]
satisfies_inf [instance, in Obs.sem_obs]
satisfies_inf [instance, in Obs.notations]
satisfies_proper [instance, in Obs.notations]
satObs [instance, in Obs.sem_obs]
satObs_proper [instance, in Obs.sem_obs]
sat_impl [lemma, in Obs.sem_obs]
sat_conj [lemma, in Obs.sem_obs]
sat_disj [lemma, in Obs.sem_obs]
sat_at [lemma, in Obs.sem_obs]
sat_bot [lemma, in Obs.sem_obs]
sat_top [lemma, in Obs.sem_obs]
sat_iff_inf_finsat [lemma, in Obs.fan]
sat__Ω [instance, in Obs.anticlique]
sat:16 [binder, in Obs.notations]
SemEquiv [section, in Obs.notations]
_ ≲ _ [notation, in Obs.notations]
_ ≃ _ [notation, in Obs.notations]
sem_bij_to_Obs__Ω [lemma, in Obs.anticlique]
sem_obs [library]
sequiv [definition, in Obs.notations]
sequiv_Equiv [instance, in Obs.notations]
sgl [abbreviation, in Obs.coherence_graph]
sgl [abbreviation, in Obs.coherence_graph]
sglf_proof [lemma, in Obs.coherence_graph]
sgl_spec [lemma, in Obs.coherence_graph]
sgl__f [definition, in Obs.coherence_graph]
shuffle [section, in Obs.list_tools]
shuffles [definition, in Obs.list_tools]
shuffles_length [lemma, in Obs.list_tools]
shuffles_nodup [lemma, in Obs.list_tools]
shuffles_equiv [lemma, in Obs.list_tools]
shuffles_map [lemma, in Obs.list_dec]
shuffles_spec [lemma, in Obs.list_dec]
singleton_is_coherent [lemma, in Obs.coherence_graph]
size [projection, in Obs.notations]
Size [record, in Obs.notations]
size [constructor, in Obs.notations]
Size [inductive, in Obs.notations]
SizeApp [lemma, in Obs.list_tools]
SizeCons [lemma, in Obs.list_tools]
SizeLength [lemma, in Obs.list_tools]
SizeList [instance, in Obs.list_tools]
SizeMap [lemma, in Obs.list_tools]
SizeNil [lemma, in Obs.list_tools]
sound_τ_sat__Ω [lemma, in Obs.anticlique]
split_word [lemma, in Obs.list_tools]
split_fst [lemma, in Obs.list_tools]
split_snd [lemma, in Obs.list_tools]
split_app_unambiguous [lemma, in Obs.list_dec]
ssmaller [definition, in Obs.notations]
ssmaller_PartialOrder [instance, in Obs.notations]
ssmaller_PreOrder [instance, in Obs.notations]
subsets [definition, in Obs.list_tools]
subsets_NoDup [lemma, in Obs.list_tools]
subsets_spec [lemma, in Obs.list_tools]
subsets_In [lemma, in Obs.list_tools]
sum [definition, in Obs.list_tools]
sum_filter [lemma, in Obs.list_tools]
sum_lt [lemma, in Obs.list_tools]
sum_le [lemma, in Obs.list_tools]
sum_zero_in [lemma, in Obs.list_tools]
sum_add_distr [lemma, in Obs.list_tools]
sum_add [lemma, in Obs.list_tools]
sum_ext_In [lemma, in Obs.list_tools]
sum_ext [lemma, in Obs.list_tools]
sum_incr [lemma, in Obs.list_tools]
sum_eq_ND [lemma, in Obs.list_tools]
sum_incl_ND [lemma, in Obs.list_tools]
sum_app [lemma, in Obs.list_tools]
sum_incr_0_right [lemma, in Obs.list_dec]
sum_incr_0_left [lemma, in Obs.list_dec]
sup [definition, in Obs.product]
support [definition, in Obs.fin_sem_obs]
support_dominates_sem [lemma, in Obs.fin_sem_obs]
sym_fincompatible [instance, in Obs.coherence_graph]
sym_incompatible [instance, in Obs.coherence_graph]
syntax_obs [library]
s.infiniteV [variable, in Obs.anticlique]
_ ↯ _ [notation, in Obs.coherence_graph]
_ ⊃ _ [notation, in Obs.coherence_graph]
_ ∝ _ [notation, in Obs.coherence_graph]
_ ⋊ _ [notation, in Obs.coherence_graph]
_ ⌣ _ [notation, in Obs.coherence_graph]
_ ⁐ _ [notation, in Obs.coherence_graph]
_ =obs' _ [notation, in Obs.equiv_obs]
_ =obs _ [notation, in Obs.equiv_obs]
_ =ha _ [notation, in Obs.equiv_obs]
_ (+) _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≦ _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≡ _ [notation, in Obs.equiv_obs]
_ =𝒜 _ [notation, in Obs.product]
_ .{ _ } [notation, in Obs.product]
_ ⇂ _ [notation, in Obs.product]
_ @ _ [notation, in Obs.product]
_ @' _ [notation, in Obs.product]
_ =fan _ [notation, in Obs.fan]
_ =Ω _ [notation, in Obs.anticlique]
A⁺ [notation, in Obs.laws]
⊤' [notation, in Obs.anticlique]
⎣ _ ⎦ [notation, in Obs.fin_sem_obs]
s.𝖠_complete [variable, in Obs.product]
s1:169 [binder, in Obs.list_tools]
s1:174 [binder, in Obs.list_tools]
s1:291 [binder, in Obs.list_tools]
s1:300 [binder, in Obs.list_tools]
s2:170 [binder, in Obs.list_tools]
s2:175 [binder, in Obs.list_tools]
s2:292 [binder, in Obs.list_tools]
s2:301 [binder, in Obs.list_tools]
s3:171 [binder, in Obs.list_tools]
s4:172 [binder, in Obs.list_tools]
s:10 [binder, in Obs.fin_sem_obs]
s:122 [binder, in Obs.product]
s:126 [binder, in Obs.product]
s:13 [binder, in Obs.fin_sem_obs]
s:131 [binder, in Obs.product]
s:136 [binder, in Obs.laws]
s:139 [binder, in Obs.laws]
s:142 [binder, in Obs.laws]
s:145 [binder, in Obs.laws]
s:185 [binder, in Obs.product]
s:188 [binder, in Obs.product]
s:193 [binder, in Obs.product]
s:194 [binder, in Obs.product]
s:195 [binder, in Obs.product]
s:197 [binder, in Obs.product]
s:199 [binder, in Obs.product]
s:204 [binder, in Obs.product]
s:207 [binder, in Obs.product]
s:208 [binder, in Obs.list_dec]
s:210 [binder, in Obs.product]
s:28 [binder, in Obs.fan]
s:3 [binder, in Obs.laws]
s:31 [binder, in Obs.sem_obs]
s:32 [binder, in Obs.sem_obs]
s:34 [binder, in Obs.sem_obs]
s:35 [binder, in Obs.anticlique]
s:37 [binder, in Obs.sem_obs]
s:38 [binder, in Obs.fin_sem_obs]
s:38 [binder, in Obs.sem_obs]
s:40 [binder, in Obs.fin_sem_obs]
s:40 [binder, in Obs.sem_obs]
s:42 [binder, in Obs.equiv_obs]
s:42 [binder, in Obs.fin_sem_obs]
s:42 [binder, in Obs.sem_obs]
s:43 [binder, in Obs.fan]
s:44 [binder, in Obs.equiv_obs]
s:44 [binder, in Obs.sem_obs]
s:44 [binder, in Obs.fan]
s:46 [binder, in Obs.fan]
s:47 [binder, in Obs.sem_obs]
s:48 [binder, in Obs.equiv_obs]
s:51 [binder, in Obs.anticlique]
s:52 [binder, in Obs.sem_obs]
s:52 [binder, in Obs.fan]
s:53 [binder, in Obs.equiv_obs]
s:53 [binder, in Obs.anticlique]
s:66 [binder, in Obs.anticlique]
s:69 [binder, in Obs.anticlique]
s:71 [binder, in Obs.fan]
s:71 [binder, in Obs.anticlique]
s:73 [binder, in Obs.anticlique]
s:74 [binder, in Obs.anticlique]
s:76 [binder, in Obs.fan]
s:78 [binder, in Obs.anticlique]
s:79 [binder, in Obs.anticlique]
s:8 [binder, in Obs.syntax_obs]
s:80 [binder, in Obs.fan]
s:81 [binder, in Obs.anticlique]
s:84 [binder, in Obs.product]
s:84 [binder, in Obs.anticlique]
s:85 [binder, in Obs.anticlique]
s:88 [binder, in Obs.product]
s:88 [binder, in Obs.anticlique]
s:89 [binder, in Obs.laws]
s:89 [binder, in Obs.anticlique]
s:90 [binder, in Obs.laws]
s:90 [binder, in Obs.equiv_obs]
s:91 [binder, in Obs.anticlique]
T
termVect [definition, in Obs.product]test [definition, in Obs.decidable_prop]
test_spec [lemma, in Obs.decidable_prop]
test_Is_true [lemma, in Obs.decidable_prop]
test_reflect [lemma, in Obs.decidable_prop]
top'_or_neg [lemma, in Obs.anticlique]
top'_not_a [lemma, in Obs.anticlique]
top'_a [lemma, in Obs.anticlique]
to_Obs__Ω [definition, in Obs.anticlique]
t1:288 [binder, in Obs.list_tools]
t1:297 [binder, in Obs.list_tools]
t2:289 [binder, in Obs.list_tools]
t2:298 [binder, in Obs.list_tools]
t:123 [binder, in Obs.product]
t:127 [binder, in Obs.product]
t:132 [binder, in Obs.product]
t:150 [binder, in Obs.coherence_graph]
T:189 [binder, in Obs.list_tools]
T:190 [binder, in Obs.list_tools]
T:191 [binder, in Obs.list_tools]
T:192 [binder, in Obs.list_tools]
T:193 [binder, in Obs.list_tools]
T:194 [binder, in Obs.list_tools]
T:196 [binder, in Obs.list_tools]
t:196 [binder, in Obs.product]
t:198 [binder, in Obs.product]
t:200 [binder, in Obs.product]
T:214 [binder, in Obs.list_tools]
T:215 [binder, in Obs.list_tools]
T:226 [binder, in Obs.list_tools]
T:228 [binder, in Obs.list_tools]
t:287 [binder, in Obs.list_tools]
t:296 [binder, in Obs.list_tools]
t:33 [binder, in Obs.sem_obs]
t:35 [binder, in Obs.sem_obs]
t:36 [binder, in Obs.anticlique]
t:39 [binder, in Obs.sem_obs]
t:4 [binder, in Obs.laws]
t:41 [binder, in Obs.sem_obs]
t:43 [binder, in Obs.equiv_obs]
t:43 [binder, in Obs.fin_sem_obs]
t:43 [binder, in Obs.sem_obs]
t:45 [binder, in Obs.equiv_obs]
t:45 [binder, in Obs.sem_obs]
t:45 [binder, in Obs.fan]
t:47 [binder, in Obs.fan]
t:48 [binder, in Obs.sem_obs]
t:49 [binder, in Obs.equiv_obs]
t:52 [binder, in Obs.anticlique]
t:53 [binder, in Obs.fan]
t:54 [binder, in Obs.equiv_obs]
t:54 [binder, in Obs.anticlique]
t:70 [binder, in Obs.anticlique]
t:72 [binder, in Obs.anticlique]
t:75 [binder, in Obs.anticlique]
t:80 [binder, in Obs.anticlique]
t:82 [binder, in Obs.anticlique]
t:86 [binder, in Obs.anticlique]
t:87 [binder, in Obs.coherence_graph]
t:90 [binder, in Obs.anticlique]
t:91 [binder, in Obs.equiv_obs]
t:92 [binder, in Obs.anticlique]
U
undup [definition, in Obs.list_dec]undup_equivalent_Proper [instance, in Obs.list_dec]
undup_incl_Proper [instance, in Obs.list_dec]
undup_equivalent [lemma, in Obs.list_dec]
undup_length [lemma, in Obs.list_dec]
Unnamed_thm [definition, in Obs.decidable_prop]
u1:101 [binder, in Obs.list_tools]
u1:107 [binder, in Obs.list_tools]
u1:306 [binder, in Obs.list_tools]
u1:32 [binder, in Obs.list_dec]
u1:36 [binder, in Obs.list_dec]
u1:95 [binder, in Obs.list_tools]
u2:102 [binder, in Obs.list_tools]
u2:108 [binder, in Obs.list_tools]
u2:307 [binder, in Obs.list_tools]
u2:33 [binder, in Obs.list_dec]
u2:37 [binder, in Obs.list_dec]
u2:96 [binder, in Obs.list_tools]
u:11 [binder, in Obs.sem_obs]
u:13 [binder, in Obs.product]
u:135 [binder, in Obs.laws]
u:138 [binder, in Obs.laws]
u:141 [binder, in Obs.laws]
u:143 [binder, in Obs.list_dec]
u:144 [binder, in Obs.laws]
u:146 [binder, in Obs.list_dec]
u:149 [binder, in Obs.list_dec]
u:150 [binder, in Obs.list_dec]
u:153 [binder, in Obs.list_dec]
u:156 [binder, in Obs.list_dec]
u:159 [binder, in Obs.list_dec]
u:161 [binder, in Obs.list_dec]
u:163 [binder, in Obs.list_dec]
u:165 [binder, in Obs.list_dec]
u:168 [binder, in Obs.list_dec]
u:171 [binder, in Obs.list_dec]
u:174 [binder, in Obs.list_dec]
u:177 [binder, in Obs.list_dec]
u:180 [binder, in Obs.list_dec]
u:183 [binder, in Obs.list_dec]
u:186 [binder, in Obs.list_dec]
u:187 [binder, in Obs.list_dec]
u:189 [binder, in Obs.list_dec]
u:20 [binder, in Obs.anticlique]
u:22 [binder, in Obs.coherence_graph]
u:22 [binder, in Obs.anticlique]
u:25 [binder, in Obs.anticlique]
u:26 [binder, in Obs.fin_sem_obs]
u:304 [binder, in Obs.list_tools]
u:31 [binder, in Obs.product]
u:34 [binder, in Obs.list_tools]
u:4 [binder, in Obs.fin_sem_obs]
u:58 [binder, in Obs.coherence_graph]
u:63 [binder, in Obs.coherence_graph]
u:7 [binder, in Obs.fin_sem_obs]
V
V [abbreviation, in Obs.product]var_clique [lemma, in Obs.laws]
vertex [projection, in Obs.coherence_graph]
V' [definition, in Obs.anticlique]
v':39 [binder, in Obs.list_tools]
v1:103 [binder, in Obs.list_tools]
v1:109 [binder, in Obs.list_tools]
v1:34 [binder, in Obs.list_dec]
v1:38 [binder, in Obs.list_dec]
v1:97 [binder, in Obs.list_tools]
v2:104 [binder, in Obs.list_tools]
v2:110 [binder, in Obs.list_tools]
v2:35 [binder, in Obs.list_dec]
v2:39 [binder, in Obs.list_dec]
v2:98 [binder, in Obs.list_tools]
V:1 [binder, in Obs.anticlique]
v:114 [binder, in Obs.product]
v:117 [binder, in Obs.product]
v:14 [binder, in Obs.product]
v:144 [binder, in Obs.list_dec]
v:147 [binder, in Obs.list_dec]
v:151 [binder, in Obs.list_dec]
v:154 [binder, in Obs.list_dec]
v:157 [binder, in Obs.list_dec]
v:160 [binder, in Obs.list_dec]
v:162 [binder, in Obs.list_dec]
v:164 [binder, in Obs.list_dec]
v:166 [binder, in Obs.list_dec]
v:169 [binder, in Obs.list_dec]
v:172 [binder, in Obs.list_dec]
v:175 [binder, in Obs.list_dec]
v:178 [binder, in Obs.list_dec]
v:181 [binder, in Obs.list_dec]
v:184 [binder, in Obs.list_dec]
v:188 [binder, in Obs.list_dec]
v:190 [binder, in Obs.list_dec]
v:222 [binder, in Obs.product]
v:224 [binder, in Obs.product]
v:226 [binder, in Obs.product]
v:228 [binder, in Obs.product]
v:32 [binder, in Obs.product]
v:33 [binder, in Obs.list_tools]
v:37 [binder, in Obs.list_tools]
v:38 [binder, in Obs.product]
v:42 [binder, in Obs.product]
v:49 [binder, in Obs.product]
v:5 [binder, in Obs.fin_sem_obs]
v:50 [binder, in Obs.product]
v:52 [binder, in Obs.product]
v:56 [binder, in Obs.product]
v:59 [binder, in Obs.coherence_graph]
v:64 [binder, in Obs.coherence_graph]
v:8 [binder, in Obs.fin_sem_obs]
W
weak_excluded_middle [lemma, in Obs.anticlique]w:105 [binder, in Obs.list_tools]
w:112 [binder, in Obs.list_tools]
w:152 [binder, in Obs.list_dec]
w:155 [binder, in Obs.list_dec]
w:158 [binder, in Obs.list_dec]
w:173 [binder, in Obs.list_dec]
w:176 [binder, in Obs.list_dec]
w:179 [binder, in Obs.list_dec]
w:182 [binder, in Obs.list_dec]
w:185 [binder, in Obs.list_dec]
w:99 [binder, in Obs.list_tools]
X
X_dec [lemma, in Obs.decidable_prop]x1:200 [binder, in Obs.list_dec]
x2:201 [binder, in Obs.list_dec]
X:1 [binder, in Obs.decidable_prop]
x:10 [binder, in Obs.sem_obs]
X:102 [binder, in Obs.laws]
X:104 [binder, in Obs.laws]
x:104 [binder, in Obs.list_dec]
X:106 [binder, in Obs.laws]
x:106 [binder, in Obs.list_dec]
x:108 [binder, in Obs.list_dec]
X:109 [binder, in Obs.laws]
x:11 [binder, in Obs.decidable_prop]
X:11 [binder, in Obs.anticlique]
x:110 [binder, in Obs.list_dec]
X:111 [binder, in Obs.laws]
x:111 [binder, in Obs.product]
x:112 [binder, in Obs.list_dec]
X:113 [binder, in Obs.list_tools]
X:114 [binder, in Obs.laws]
x:114 [binder, in Obs.list_dec]
x:115 [binder, in Obs.product]
X:116 [binder, in Obs.list_tools]
X:117 [binder, in Obs.laws]
x:117 [binder, in Obs.list_dec]
x:118 [binder, in Obs.product]
x:12 [binder, in Obs.sem_obs]
x:120 [binder, in Obs.list_dec]
x:122 [binder, in Obs.laws]
X:123 [binder, in Obs.laws]
X:126 [binder, in Obs.laws]
x:129 [binder, in Obs.coherence_graph]
x:13 [binder, in Obs.decidable_prop]
x:131 [binder, in Obs.laws]
X:132 [binder, in Obs.laws]
x:133 [binder, in Obs.coherence_graph]
x:134 [binder, in Obs.product]
x:135 [binder, in Obs.coherence_graph]
x:135 [binder, in Obs.list_dec]
x:137 [binder, in Obs.laws]
x:138 [binder, in Obs.product]
x:139 [binder, in Obs.list_dec]
x:14 [binder, in Obs.fin_sem_obs]
X:14 [binder, in Obs.anticlique]
x:141 [binder, in Obs.coherence_graph]
x:143 [binder, in Obs.laws]
x:144 [binder, in Obs.coherence_graph]
x:147 [binder, in Obs.coherence_graph]
x:15 [binder, in Obs.decidable_prop]
x:15 [binder, in Obs.sem_obs]
x:151 [binder, in Obs.coherence_graph]
x:154 [binder, in Obs.coherence_graph]
x:157 [binder, in Obs.coherence_graph]
x:16 [binder, in Obs.decidable_prop]
x:162 [binder, in Obs.coherence_graph]
x:164 [binder, in Obs.coherence_graph]
x:166 [binder, in Obs.coherence_graph]
x:168 [binder, in Obs.coherence_graph]
x:17 [binder, in Obs.fin_sem_obs]
x:171 [binder, in Obs.coherence_graph]
x:173 [binder, in Obs.coherence_graph]
x:175 [binder, in Obs.coherence_graph]
x:177 [binder, in Obs.coherence_graph]
x:18 [binder, in Obs.decidable_prop]
x:18 [binder, in Obs.sem_obs]
x:182 [binder, in Obs.list_tools]
x:188 [binder, in Obs.list_tools]
x:20 [binder, in Obs.list_dec]
x:202 [binder, in Obs.list_dec]
x:209 [binder, in Obs.list_tools]
x:21 [binder, in Obs.anticlique]
x:211 [binder, in Obs.list_tools]
x:22 [binder, in Obs.decidable_prop]
x:22 [binder, in Obs.sem_obs]
x:225 [binder, in Obs.list_dec]
x:23 [binder, in Obs.coherence_graph]
x:23 [binder, in Obs.fin_sem_obs]
x:24 [binder, in Obs.decidable_prop]
x:24 [binder, in Obs.fin_sem_obs]
x:24 [binder, in Obs.anticlique]
x:25 [binder, in Obs.fin_sem_obs]
x:25 [binder, in Obs.sem_obs]
x:250 [binder, in Obs.list_tools]
x:26 [binder, in Obs.decidable_prop]
x:265 [binder, in Obs.list_tools]
x:27 [binder, in Obs.fin_sem_obs]
x:27 [binder, in Obs.anticlique]
x:28 [binder, in Obs.decidable_prop]
x:28 [binder, in Obs.sem_obs]
x:3 [binder, in Obs.sem_obs]
x:30 [binder, in Obs.fin_sem_obs]
x:305 [binder, in Obs.list_tools]
x:31 [binder, in Obs.fan]
x:31 [binder, in Obs.anticlique]
x:32 [binder, in Obs.decidable_prop]
x:33 [binder, in Obs.fin_sem_obs]
x:34 [binder, in Obs.decidable_prop]
x:34 [binder, in Obs.fan]
x:36 [binder, in Obs.decidable_prop]
x:379 [binder, in Obs.list_tools]
x:38 [binder, in Obs.decidable_prop]
x:38 [binder, in Obs.fan]
x:384 [binder, in Obs.list_tools]
x:389 [binder, in Obs.list_tools]
x:39 [binder, in Obs.coherence_graph]
x:395 [binder, in Obs.list_tools]
x:4 [binder, in Obs.decidable_prop]
X:4 [binder, in Obs.notations]
x:40 [binder, in Obs.fan]
x:400 [binder, in Obs.list_tools]
x:404 [binder, in Obs.list_tools]
x:42 [binder, in Obs.anticlique]
x:47 [binder, in Obs.coherence_graph]
x:48 [binder, in Obs.coherence_graph]
x:48 [binder, in Obs.fan]
x:49 [binder, in Obs.decidable_prop]
x:50 [binder, in Obs.fan]
x:50 [binder, in Obs.anticlique]
X:51 [binder, in Obs.list_dec]
x:54 [binder, in Obs.list_tools]
x:55 [binder, in Obs.list_dec]
x:56 [binder, in Obs.list_dec]
x:61 [binder, in Obs.list_dec]
x:64 [binder, in Obs.list_tools]
x:64 [binder, in Obs.anticlique]
x:65 [binder, in Obs.coherence_graph]
x:67 [binder, in Obs.list_dec]
x:69 [binder, in Obs.list_tools]
X:7 [binder, in Obs.decidable_prop]
x:70 [binder, in Obs.fan]
x:74 [binder, in Obs.list_tools]
x:75 [binder, in Obs.fan]
x:8 [binder, in Obs.sem_obs]
x:81 [binder, in Obs.fan]
x:83 [binder, in Obs.anticlique]
x:84 [binder, in Obs.coherence_graph]
x:87 [binder, in Obs.decidable_prop]
x:89 [binder, in Obs.decidable_prop]
x:9 [binder, in Obs.decidable_prop]
x:9 [binder, in Obs.sem_obs]
X:92 [binder, in Obs.laws]
X:95 [binder, in Obs.laws]
X:97 [binder, in Obs.laws]
X:99 [binder, in Obs.laws]
Y
y:10 [binder, in Obs.decidable_prop]Y:100 [binder, in Obs.laws]
Y:112 [binder, in Obs.laws]
Y:115 [binder, in Obs.laws]
y:115 [binder, in Obs.list_dec]
y:118 [binder, in Obs.list_dec]
y:12 [binder, in Obs.decidable_prop]
y:130 [binder, in Obs.coherence_graph]
y:134 [binder, in Obs.coherence_graph]
y:135 [binder, in Obs.product]
y:136 [binder, in Obs.coherence_graph]
y:139 [binder, in Obs.product]
y:14 [binder, in Obs.decidable_prop]
y:142 [binder, in Obs.coherence_graph]
y:145 [binder, in Obs.coherence_graph]
y:148 [binder, in Obs.coherence_graph]
y:152 [binder, in Obs.coherence_graph]
y:155 [binder, in Obs.coherence_graph]
y:17 [binder, in Obs.decidable_prop]
y:19 [binder, in Obs.decidable_prop]
y:21 [binder, in Obs.fin_sem_obs]
y:21 [binder, in Obs.sem_obs]
y:23 [binder, in Obs.decidable_prop]
y:25 [binder, in Obs.decidable_prop]
y:251 [binder, in Obs.list_tools]
y:27 [binder, in Obs.decidable_prop]
y:29 [binder, in Obs.decidable_prop]
y:29 [binder, in Obs.sem_obs]
y:32 [binder, in Obs.fan]
y:32 [binder, in Obs.anticlique]
y:33 [binder, in Obs.decidable_prop]
y:35 [binder, in Obs.decidable_prop]
y:35 [binder, in Obs.fan]
y:36 [binder, in Obs.fin_sem_obs]
y:37 [binder, in Obs.decidable_prop]
y:39 [binder, in Obs.decidable_prop]
y:40 [binder, in Obs.coherence_graph]
y:42 [binder, in Obs.fan]
y:49 [binder, in Obs.coherence_graph]
y:49 [binder, in Obs.fan]
y:5 [binder, in Obs.decidable_prop]
y:50 [binder, in Obs.decidable_prop]
y:51 [binder, in Obs.fan]
y:62 [binder, in Obs.list_dec]
y:65 [binder, in Obs.anticlique]
y:66 [binder, in Obs.coherence_graph]
y:7 [binder, in Obs.sem_obs]
y:74 [binder, in Obs.fan]
y:85 [binder, in Obs.coherence_graph]
y:88 [binder, in Obs.decidable_prop]
y:90 [binder, in Obs.decidable_prop]
Y:98 [binder, in Obs.laws]
Z
z:143 [binder, in Obs.coherence_graph]z:146 [binder, in Obs.coherence_graph]
z:149 [binder, in Obs.coherence_graph]
z:15 [binder, in Obs.fin_sem_obs]
z:153 [binder, in Obs.coherence_graph]
z:156 [binder, in Obs.coherence_graph]
z:16 [binder, in Obs.fin_sem_obs]
z:22 [binder, in Obs.fin_sem_obs]
z:37 [binder, in Obs.fin_sem_obs]
z:50 [binder, in Obs.coherence_graph]
z:67 [binder, in Obs.coherence_graph]
z:76 [binder, in Obs.product]
z:77 [binder, in Obs.product]
z:77 [binder, in Obs.fan]
z:78 [binder, in Obs.fan]
z:86 [binder, in Obs.coherence_graph]
other
_ ≈ _ [notation, in Obs.list_tools]_ ` [notation, in Obs.list_tools]
_ ⋈ _ [notation, in Obs.list_tools]
_ ⊗ _ [notation, in Obs.list_tools]
_ :> _ [notation, in Obs.list_tools]
_ ∈ _ [notation, in Obs.list_tools]
_ ⊆ _ [notation, in Obs.list_tools]
_ ⊃f _ [notation, in Obs.coherence_graph]
_ ↯↯ _ [notation, in Obs.coherence_graph]
_ @@ _ [notation, in Obs.coherence_graph]
_ ⊃ _ [notation, in Obs.coherence_graph]
_ ↯ _ [notation, in Obs.coherence_graph]
_ ∝ _ [notation, in Obs.coherence_graph]
_ ⋊ _ [notation, in Obs.coherence_graph]
_ ⌣ _ [notation, in Obs.coherence_graph]
_ ⁐ _ [notation, in Obs.coherence_graph]
_ =?= _ [notation, in Obs.decidable_prop]
_ =obs' _ [notation, in Obs.equiv_obs]
_ =obs _ [notation, in Obs.equiv_obs]
_ =ha _ [notation, in Obs.equiv_obs]
_ (+) _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≦ _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≡ _ [notation, in Obs.equiv_obs]
_ ⊨ _ [notation, in Obs.sem_obs]
_ − _ [notation, in Obs.list_dec]
_ ∩ _ [notation, in Obs.list_dec]
_ ⊖ _ [notation, in Obs.list_dec]
_ ∖ _ [notation, in Obs.list_dec]
_ → _ [notation, in Obs.syntax_obs]
_ ⟑ _ [notation, in Obs.syntax_obs]
_ ⟇ _ [notation, in Obs.syntax_obs]
_ ≃ _ [notation, in Obs.notations]
_ ≲ _ [notation, in Obs.notations]
_ ⊨ _ [notation, in Obs.notations]
_ ⊕ _ [notation, in Obs.notations]
_ ∘ _ [notation, in Obs.notations]
! [notation, in Obs.coherence_graph]
$ _ [notation, in Obs.notations]
{{ _ }} [notation, in Obs.list_dec]
⊤o [notation, in Obs.syntax_obs]
⊥o [notation, in Obs.syntax_obs]
⋀ [notation, in Obs.syntax_obs]
⋁ [notation, in Obs.syntax_obs]
⎢ _ ⎥ [notation, in Obs.notations]
⦑ _ ⦒ [notation, in Obs.syntax_obs]
Ω [instance, in Obs.anticlique]
Ω_neg [constructor, in Obs.anticlique]
Ω_top' [constructor, in Obs.anticlique]
Ω_ax [inductive, in Obs.anticlique]
α:104 [binder, in Obs.coherence_graph]
α:106 [binder, in Obs.coherence_graph]
α:109 [binder, in Obs.coherence_graph]
α:112 [binder, in Obs.coherence_graph]
α:119 [binder, in Obs.coherence_graph]
α:12 [binder, in Obs.fan]
α:124 [binder, in Obs.coherence_graph]
α:126 [binder, in Obs.coherence_graph]
α:127 [binder, in Obs.coherence_graph]
α:14 [binder, in Obs.fan]
α:158 [binder, in Obs.coherence_graph]
α:178 [binder, in Obs.coherence_graph]
α:181 [binder, in Obs.coherence_graph]
α:203 [binder, in Obs.product]
α:206 [binder, in Obs.product]
α:209 [binder, in Obs.product]
α:217 [binder, in Obs.product]
α:25 [binder, in Obs.coherence_graph]
α:28 [binder, in Obs.coherence_graph]
α:30 [binder, in Obs.sem_obs]
α:31 [binder, in Obs.coherence_graph]
α:33 [binder, in Obs.coherence_graph]
α:36 [binder, in Obs.coherence_graph]
α:36 [binder, in Obs.sem_obs]
α:37 [binder, in Obs.product]
α:37 [binder, in Obs.anticlique]
α:39 [binder, in Obs.fin_sem_obs]
α:40 [binder, in Obs.anticlique]
α:41 [binder, in Obs.fin_sem_obs]
α:41 [binder, in Obs.product]
α:43 [binder, in Obs.coherence_graph]
α:44 [binder, in Obs.anticlique]
α:45 [binder, in Obs.product]
α:45 [binder, in Obs.anticlique]
α:46 [binder, in Obs.sem_obs]
α:47 [binder, in Obs.anticlique]
α:48 [binder, in Obs.product]
α:48 [binder, in Obs.anticlique]
α:51 [binder, in Obs.sem_obs]
α:53 [binder, in Obs.product]
α:57 [binder, in Obs.product]
α:58 [binder, in Obs.anticlique]
α:60 [binder, in Obs.product]
α:60 [binder, in Obs.anticlique]
α:62 [binder, in Obs.anticlique]
α:63 [binder, in Obs.product]
α:68 [binder, in Obs.product]
α:70 [binder, in Obs.product]
α:72 [binder, in Obs.product]
α:79 [binder, in Obs.product]
α:79 [binder, in Obs.fan]
α:87 [binder, in Obs.anticlique]
α:89 [binder, in Obs.equiv_obs]
α:89 [binder, in Obs.product]
α:90 [binder, in Obs.coherence_graph]
α:92 [binder, in Obs.equiv_obs]
α:93 [binder, in Obs.coherence_graph]
α:94 [binder, in Obs.product]
α:98 [binder, in Obs.coherence_graph]
α:99 [binder, in Obs.coherence_graph]
β:100 [binder, in Obs.product]
β:101 [binder, in Obs.product]
β:105 [binder, in Obs.product]
β:106 [binder, in Obs.product]
β:128 [binder, in Obs.coherence_graph]
β:218 [binder, in Obs.product]
β:242 [binder, in Obs.product]
β:243 [binder, in Obs.product]
β:244 [binder, in Obs.product]
β:245 [binder, in Obs.product]
β:246 [binder, in Obs.product]
β:247 [binder, in Obs.product]
β:248 [binder, in Obs.product]
β:249 [binder, in Obs.product]
β:250 [binder, in Obs.product]
β:251 [binder, in Obs.product]
β:252 [binder, in Obs.product]
β:253 [binder, in Obs.product]
β:37 [binder, in Obs.coherence_graph]
β:44 [binder, in Obs.coherence_graph]
β:49 [binder, in Obs.sem_obs]
β:50 [binder, in Obs.sem_obs]
β:73 [binder, in Obs.product]
β:80 [binder, in Obs.product]
β:93 [binder, in Obs.anticlique]
β:96 [binder, in Obs.product]
β:97 [binder, in Obs.product]
γ:219 [binder, in Obs.product]
γ:74 [binder, in Obs.product]
γ:81 [binder, in Obs.product]
δ:220 [binder, in Obs.product]
ζ [definition, in Obs.anticlique]
ζ_ξ [lemma, in Obs.anticlique]
ζ_empt [lemma, in Obs.anticlique]
ζ_sgl [lemma, in Obs.anticlique]
ζ_None [lemma, in Obs.anticlique]
ζ_Some [lemma, in Obs.anticlique]
ξ [definition, in Obs.anticlique]
ξ_to_Obs__Ω [lemma, in Obs.anticlique]
ξ_ζ [lemma, in Obs.anticlique]
π [definition, in Obs.syntax_obs]
π_proper [instance, in Obs.laws]
π_spec [lemma, in Obs.sem_obs]
τ [definition, in Obs.anticlique]
τ_to_Obs__Ω [lemma, in Obs.anticlique]
τ_impl__Ω [lemma, in Obs.anticlique]
τ_neg__Ω [lemma, in Obs.anticlique]
τ_meet__Ω [lemma, in Obs.anticlique]
τ_join__Ω [lemma, in Obs.anticlique]
τ_proper_inf__Ω [instance, in Obs.anticlique]
τ_ξ [lemma, in Obs.anticlique]
τ_ζ [lemma, in Obs.anticlique]
ϕ:60 [binder, in Obs.decidable_prop]
𝒜 [abbreviation, in Obs.product]
𝒜_complete [lemma, in Obs.product]
𝒜_sound [lemma, in Obs.product]
𝒢 [instance, in Obs.product]
𝒯 [definition, in Obs.product]
𝒱 [inductive, in Obs.product]
𝖠_complete_inf [lemma, in Obs.product]
𝖠:120 [binder, in Obs.product]
𝖠:54 [binder, in Obs.sem_obs]
𝖦:3 [binder, in Obs.product]
𝖳 [abbreviation, in Obs.product]
Notation Index
C
_ ⊗ _ [in Obs.list_tools]D
_ − _ [in Obs.list_dec]_ ∩ _ [in Obs.list_dec]
_ ⊖ _ [in Obs.list_dec]
_ ∖ _ [in Obs.list_dec]
{{ _ }} [in Obs.list_dec]
F
_ @@ _ [in Obs.coherence_graph]_ ↯↯ _ [in Obs.coherence_graph]
! [in Obs.coherence_graph]
_ ⊃f _ [in Obs.coherence_graph]
_ ` [in Obs.list_tools]
M
_ ⋈ _ [in Obs.list_tools]S
_ ≲ _ [in Obs.notations]_ ≃ _ [in Obs.notations]
_ ↯ _ [in Obs.coherence_graph]
_ ⊃ _ [in Obs.coherence_graph]
_ ∝ _ [in Obs.coherence_graph]
_ ⋊ _ [in Obs.coherence_graph]
_ ⌣ _ [in Obs.coherence_graph]
_ ⁐ _ [in Obs.coherence_graph]
_ =obs' _ [in Obs.equiv_obs]
_ =obs _ [in Obs.equiv_obs]
_ =ha _ [in Obs.equiv_obs]
_ (+) _ [in Obs.equiv_obs]
_ ⊢ _ ≦ _ [in Obs.equiv_obs]
_ ⊢ _ ≡ _ [in Obs.equiv_obs]
_ =𝒜 _ [in Obs.product]
_ .{ _ } [in Obs.product]
_ ⇂ _ [in Obs.product]
_ @ _ [in Obs.product]
_ @' _ [in Obs.product]
_ =fan _ [in Obs.fan]
_ =Ω _ [in Obs.anticlique]
A⁺ [in Obs.laws]
⊤' [in Obs.anticlique]
⎣ _ ⎦ [in Obs.fin_sem_obs]
other
_ ≈ _ [in Obs.list_tools]_ ` [in Obs.list_tools]
_ ⋈ _ [in Obs.list_tools]
_ ⊗ _ [in Obs.list_tools]
_ :> _ [in Obs.list_tools]
_ ∈ _ [in Obs.list_tools]
_ ⊆ _ [in Obs.list_tools]
_ ⊃f _ [in Obs.coherence_graph]
_ ↯↯ _ [in Obs.coherence_graph]
_ @@ _ [in Obs.coherence_graph]
_ ⊃ _ [in Obs.coherence_graph]
_ ↯ _ [in Obs.coherence_graph]
_ ∝ _ [in Obs.coherence_graph]
_ ⋊ _ [in Obs.coherence_graph]
_ ⌣ _ [in Obs.coherence_graph]
_ ⁐ _ [in Obs.coherence_graph]
_ =?= _ [in Obs.decidable_prop]
_ =obs' _ [in Obs.equiv_obs]
_ =obs _ [in Obs.equiv_obs]
_ =ha _ [in Obs.equiv_obs]
_ (+) _ [in Obs.equiv_obs]
_ ⊢ _ ≦ _ [in Obs.equiv_obs]
_ ⊢ _ ≡ _ [in Obs.equiv_obs]
_ ⊨ _ [in Obs.sem_obs]
_ − _ [in Obs.list_dec]
_ ∩ _ [in Obs.list_dec]
_ ⊖ _ [in Obs.list_dec]
_ ∖ _ [in Obs.list_dec]
_ → _ [in Obs.syntax_obs]
_ ⟑ _ [in Obs.syntax_obs]
_ ⟇ _ [in Obs.syntax_obs]
_ ≃ _ [in Obs.notations]
_ ≲ _ [in Obs.notations]
_ ⊨ _ [in Obs.notations]
_ ⊕ _ [in Obs.notations]
_ ∘ _ [in Obs.notations]
! [in Obs.coherence_graph]
$ _ [in Obs.notations]
{{ _ }} [in Obs.list_dec]
⊤o [in Obs.syntax_obs]
⊥o [in Obs.syntax_obs]
⋀ [in Obs.syntax_obs]
⋁ [in Obs.syntax_obs]
⎢ _ ⎥ [in Obs.notations]
⦑ _ ⦒ [in Obs.syntax_obs]
Binder Index
A
acc:332 [in Obs.list_tools]acc:362 [in Obs.list_tools]
acc:44 [in Obs.list_dec]
Ax:118 [in Obs.laws]
Ax:127 [in Obs.laws]
a__o:6 [in Obs.anticlique]
A:1 [in Obs.list_tools]
A:1 [in Obs.list_dec]
A:1 [in Obs.notations]
a:10 [in Obs.laws]
A:10 [in Obs.notations]
A:100 [in Obs.list_tools]
a:100 [in Obs.coherence_graph]
a:101 [in Obs.laws]
a:101 [in Obs.list_dec]
a:102 [in Obs.coherence_graph]
a:102 [in Obs.list_dec]
a:103 [in Obs.laws]
a:105 [in Obs.coherence_graph]
a:105 [in Obs.laws]
A:106 [in Obs.list_tools]
a:107 [in Obs.coherence_graph]
a:108 [in Obs.laws]
A:11 [in Obs.list_tools]
a:11 [in Obs.laws]
a:11 [in Obs.equiv_obs]
a:110 [in Obs.coherence_graph]
a:111 [in Obs.list_tools]
a:113 [in Obs.coherence_graph]
a:119 [in Obs.list_tools]
a:12 [in Obs.coherence_graph]
a:12 [in Obs.product]
a:12 [in Obs.anticlique]
A:120 [in Obs.list_tools]
a:120 [in Obs.coherence_graph]
a:123 [in Obs.list_tools]
a:123 [in Obs.list_dec]
A:124 [in Obs.list_tools]
a:125 [in Obs.coherence_graph]
A:128 [in Obs.list_tools]
a:13 [in Obs.fan]
a:131 [in Obs.coherence_graph]
A:136 [in Obs.list_tools]
a:137 [in Obs.coherence_graph]
a:139 [in Obs.coherence_graph]
a:14 [in Obs.laws]
A:14 [in Obs.notations]
a:140 [in Obs.list_tools]
a:140 [in Obs.laws]
A:141 [in Obs.list_tools]
a:142 [in Obs.list_dec]
a:145 [in Obs.list_dec]
a:146 [in Obs.list_tools]
a:146 [in Obs.laws]
A:148 [in Obs.list_tools]
a:148 [in Obs.laws]
a:148 [in Obs.list_dec]
A:15 [in Obs.list_tools]
a:15 [in Obs.coherence_graph]
a:15 [in Obs.equiv_obs]
a:15 [in Obs.fan]
a:15 [in Obs.anticlique]
A:154 [in Obs.list_tools]
A:159 [in Obs.list_tools]
a:159 [in Obs.coherence_graph]
a:16 [in Obs.laws]
a:16 [in Obs.anticlique]
a:160 [in Obs.coherence_graph]
A:167 [in Obs.list_tools]
a:167 [in Obs.list_dec]
a:169 [in Obs.coherence_graph]
a:17 [in Obs.list_tools]
a:17 [in Obs.laws]
a:17 [in Obs.product]
a:17 [in Obs.anticlique]
a:17 [in Obs.notations]
a:170 [in Obs.list_dec]
A:176 [in Obs.list_tools]
a:18 [in Obs.coherence_graph]
a:18 [in Obs.fan]
a:18 [in Obs.list_dec]
A:180 [in Obs.list_tools]
a:182 [in Obs.coherence_graph]
a:183 [in Obs.list_tools]
a:183 [in Obs.coherence_graph]
a:184 [in Obs.coherence_graph]
a:184 [in Obs.product]
A:185 [in Obs.list_tools]
a:185 [in Obs.coherence_graph]
a:186 [in Obs.coherence_graph]
a:188 [in Obs.coherence_graph]
a:189 [in Obs.coherence_graph]
a:19 [in Obs.laws]
a:19 [in Obs.equiv_obs]
a:19 [in Obs.anticlique]
A:191 [in Obs.list_dec]
a:193 [in Obs.list_dec]
a:195 [in Obs.list_tools]
A:195 [in Obs.list_dec]
a:197 [in Obs.list_tools]
A:198 [in Obs.list_tools]
A:2 [in Obs.list_tools]
A:2 [in Obs.laws]
A:2 [in Obs.equiv_obs]
A:20 [in Obs.list_tools]
A:20 [in Obs.decidable_prop]
a:20 [in Obs.product]
a:20 [in Obs.fan]
a:20 [in Obs.notations]
A:201 [in Obs.list_tools]
A:204 [in Obs.list_tools]
A:204 [in Obs.list_dec]
A:206 [in Obs.list_tools]
A:208 [in Obs.list_tools]
a:209 [in Obs.list_dec]
a:21 [in Obs.laws]
a:21 [in Obs.list_dec]
A:210 [in Obs.list_tools]
A:211 [in Obs.list_dec]
A:212 [in Obs.list_tools]
A:216 [in Obs.list_tools]
a:217 [in Obs.list_dec]
A:218 [in Obs.list_dec]
A:219 [in Obs.list_tools]
a:22 [in Obs.list_tools]
a:22 [in Obs.laws]
A:222 [in Obs.list_tools]
A:224 [in Obs.list_tools]
A:224 [in Obs.list_dec]
A:227 [in Obs.list_tools]
A:227 [in Obs.list_dec]
A:229 [in Obs.list_tools]
a:23 [in Obs.equiv_obs]
A:23 [in Obs.sem_obs]
a:23 [in Obs.anticlique]
a:230 [in Obs.product]
A:230 [in Obs.list_dec]
A:232 [in Obs.list_tools]
a:232 [in Obs.product]
a:234 [in Obs.product]
A:236 [in Obs.list_tools]
a:236 [in Obs.product]
A:238 [in Obs.list_tools]
a:238 [in Obs.product]
a:24 [in Obs.coherence_graph]
a:24 [in Obs.laws]
a:24 [in Obs.sem_obs]
a:240 [in Obs.product]
A:241 [in Obs.list_tools]
A:247 [in Obs.list_tools]
A:25 [in Obs.equiv_obs]
a:25 [in Obs.product]
A:252 [in Obs.list_tools]
a:256 [in Obs.list_tools]
A:257 [in Obs.list_tools]
A:26 [in Obs.list_tools]
a:26 [in Obs.laws]
a:26 [in Obs.equiv_obs]
A:26 [in Obs.sem_obs]
a:26 [in Obs.anticlique]
a:261 [in Obs.list_tools]
A:262 [in Obs.list_tools]
A:266 [in Obs.list_tools]
a:27 [in Obs.coherence_graph]
a:27 [in Obs.sem_obs]
a:27 [in Obs.list_dec]
a:271 [in Obs.list_tools]
A:272 [in Obs.list_tools]
a:277 [in Obs.list_tools]
A:278 [in Obs.list_tools]
a:28 [in Obs.list_tools]
A:28 [in Obs.equiv_obs]
A:284 [in Obs.list_tools]
a:286 [in Obs.list_tools]
a:29 [in Obs.laws]
A:29 [in Obs.equiv_obs]
a:29 [in Obs.product]
A:293 [in Obs.list_tools]
a:295 [in Obs.list_tools]
a:30 [in Obs.coherence_graph]
a:30 [in Obs.laws]
A:30 [in Obs.decidable_prop]
A:30 [in Obs.equiv_obs]
A:302 [in Obs.list_tools]
A:308 [in Obs.list_tools]
a:31 [in Obs.laws]
A:31 [in Obs.equiv_obs]
a:31 [in Obs.list_dec]
A:312 [in Obs.list_tools]
A:315 [in Obs.list_tools]
a:316 [in Obs.list_tools]
A:32 [in Obs.list_tools]
a:32 [in Obs.coherence_graph]
a:32 [in Obs.laws]
A:32 [in Obs.equiv_obs]
A:320 [in Obs.list_tools]
A:324 [in Obs.list_tools]
A:327 [in Obs.list_tools]
a:33 [in Obs.laws]
A:33 [in Obs.equiv_obs]
a:331 [in Obs.list_tools]
A:334 [in Obs.list_tools]
a:338 [in Obs.list_tools]
a:34 [in Obs.coherence_graph]
A:34 [in Obs.equiv_obs]
a:34 [in Obs.product]
A:340 [in Obs.list_tools]
A:347 [in Obs.list_tools]
A:35 [in Obs.equiv_obs]
A:351 [in Obs.list_tools]
a:354 [in Obs.list_tools]
A:355 [in Obs.list_tools]
A:358 [in Obs.list_tools]
A:36 [in Obs.list_tools]
a:36 [in Obs.laws]
A:36 [in Obs.equiv_obs]
a:36 [in Obs.fan]
a:361 [in Obs.list_tools]
A:363 [in Obs.list_tools]
A:367 [in Obs.list_tools]
A:37 [in Obs.equiv_obs]
a:37 [in Obs.fan]
A:371 [in Obs.list_tools]
A:375 [in Obs.list_tools]
a:38 [in Obs.list_tools]
a:38 [in Obs.coherence_graph]
a:38 [in Obs.laws]
A:38 [in Obs.equiv_obs]
a:38 [in Obs.anticlique]
A:380 [in Obs.list_tools]
A:385 [in Obs.list_tools]
a:39 [in Obs.product]
A:390 [in Obs.list_tools]
A:396 [in Obs.list_tools]
A:4 [in Obs.list_tools]
a:4 [in Obs.fan]
a:4 [in Obs.anticlique]
A:40 [in Obs.list_tools]
A:40 [in Obs.decidable_prop]
a:40 [in Obs.list_dec]
A:401 [in Obs.list_tools]
A:405 [in Obs.list_tools]
a:409 [in Obs.list_tools]
a:41 [in Obs.coherence_graph]
a:41 [in Obs.laws]
a:41 [in Obs.anticlique]
A:410 [in Obs.list_tools]
a:414 [in Obs.list_tools]
A:416 [in Obs.list_tools]
A:420 [in Obs.list_tools]
a:421 [in Obs.list_tools]
a:428 [in Obs.list_tools]
a:43 [in Obs.list_tools]
a:43 [in Obs.laws]
a:43 [in Obs.product]
a:43 [in Obs.list_dec]
A:44 [in Obs.list_tools]
a:45 [in Obs.coherence_graph]
a:45 [in Obs.laws]
A:450 [in Obs.list_tools]
a:451 [in Obs.list_tools]
A:455 [in Obs.list_tools]
a:46 [in Obs.coherence_graph]
A:46 [in Obs.equiv_obs]
a:46 [in Obs.product]
a:46 [in Obs.list_dec]
a:46 [in Obs.anticlique]
a:47 [in Obs.laws]
A:48 [in Obs.list_tools]
A:48 [in Obs.decidable_prop]
a:49 [in Obs.laws]
a:49 [in Obs.anticlique]
a:5 [in Obs.list_tools]
a:5 [in Obs.laws]
a:5 [in Obs.equiv_obs]
A:51 [in Obs.list_tools]
a:51 [in Obs.coherence_graph]
A:51 [in Obs.equiv_obs]
a:52 [in Obs.laws]
a:53 [in Obs.coherence_graph]
a:54 [in Obs.product]
A:55 [in Obs.list_tools]
a:55 [in Obs.laws]
a:55 [in Obs.sem_obs]
a:55 [in Obs.fan]
a:57 [in Obs.anticlique]
a:58 [in Obs.list_tools]
a:58 [in Obs.laws]
a:58 [in Obs.equiv_obs]
a:58 [in Obs.product]
a:58 [in Obs.fan]
A:59 [in Obs.list_tools]
a:6 [in Obs.equiv_obs]
a:6 [in Obs.fin_sem_obs]
a:60 [in Obs.fan]
a:61 [in Obs.laws]
a:61 [in Obs.equiv_obs]
a:61 [in Obs.product]
a:63 [in Obs.equiv_obs]
a:63 [in Obs.fan]
a:64 [in Obs.laws]
a:64 [in Obs.equiv_obs]
a:64 [in Obs.product]
A:65 [in Obs.list_tools]
a:65 [in Obs.product]
a:65 [in Obs.fan]
a:65 [in Obs.list_dec]
a:66 [in Obs.laws]
a:67 [in Obs.equiv_obs]
a:67 [in Obs.product]
a:67 [in Obs.fan]
a:68 [in Obs.coherence_graph]
a:68 [in Obs.laws]
a:68 [in Obs.fan]
a:69 [in Obs.coherence_graph]
a:69 [in Obs.equiv_obs]
a:69 [in Obs.fan]
a:69 [in Obs.list_dec]
A:7 [in Obs.list_tools]
a:7 [in Obs.coherence_graph]
A:70 [in Obs.list_tools]
a:70 [in Obs.coherence_graph]
a:70 [in Obs.laws]
a:70 [in Obs.equiv_obs]
a:71 [in Obs.coherence_graph]
A:71 [in Obs.decidable_prop]
a:71 [in Obs.list_dec]
a:72 [in Obs.coherence_graph]
a:72 [in Obs.equiv_obs]
a:73 [in Obs.laws]
a:73 [in Obs.list_dec]
a:74 [in Obs.coherence_graph]
a:74 [in Obs.decidable_prop]
a:74 [in Obs.equiv_obs]
a:74 [in Obs.list_dec]
A:75 [in Obs.list_tools]
a:75 [in Obs.decidable_prop]
a:75 [in Obs.equiv_obs]
a:75 [in Obs.list_dec]
a:76 [in Obs.coherence_graph]
a:76 [in Obs.laws]
a:76 [in Obs.decidable_prop]
a:76 [in Obs.anticlique]
A:77 [in Obs.list_tools]
a:77 [in Obs.decidable_prop]
a:77 [in Obs.equiv_obs]
a:77 [in Obs.list_dec]
a:77 [in Obs.anticlique]
a:78 [in Obs.coherence_graph]
A:78 [in Obs.decidable_prop]
a:79 [in Obs.laws]
a:79 [in Obs.equiv_obs]
A:8 [in Obs.list_tools]
a:8 [in Obs.laws]
a:8 [in Obs.equiv_obs]
A:80 [in Obs.list_tools]
a:80 [in Obs.coherence_graph]
a:81 [in Obs.decidable_prop]
a:81 [in Obs.list_dec]
a:82 [in Obs.coherence_graph]
a:82 [in Obs.laws]
a:82 [in Obs.decidable_prop]
a:83 [in Obs.list_tools]
a:83 [in Obs.decidable_prop]
a:83 [in Obs.list_dec]
A:84 [in Obs.list_tools]
a:84 [in Obs.decidable_prop]
a:84 [in Obs.equiv_obs]
a:85 [in Obs.laws]
a:86 [in Obs.laws]
a:86 [in Obs.list_dec]
a:87 [in Obs.laws]
a:88 [in Obs.laws]
A:89 [in Obs.list_tools]
a:89 [in Obs.list_dec]
a:9 [in Obs.anticlique]
a:91 [in Obs.coherence_graph]
a:91 [in Obs.laws]
a:93 [in Obs.equiv_obs]
a:93 [in Obs.list_dec]
A:94 [in Obs.list_tools]
a:94 [in Obs.coherence_graph]
a:94 [in Obs.laws]
a:94 [in Obs.anticlique]
a:95 [in Obs.anticlique]
a:96 [in Obs.coherence_graph]
a:96 [in Obs.anticlique]
a:97 [in Obs.anticlique]
a:98 [in Obs.anticlique]
a:99 [in Obs.anticlique]
B
b0:115 [in Obs.coherence_graph]b0:116 [in Obs.coherence_graph]
b0:117 [in Obs.coherence_graph]
b0:118 [in Obs.coherence_graph]
b0:122 [in Obs.coherence_graph]
b0:123 [in Obs.coherence_graph]
b:10 [in Obs.anticlique]
b:101 [in Obs.coherence_graph]
b:103 [in Obs.coherence_graph]
b:107 [in Obs.laws]
b:108 [in Obs.coherence_graph]
B:11 [in Obs.notations]
b:110 [in Obs.laws]
b:111 [in Obs.coherence_graph]
b:114 [in Obs.coherence_graph]
B:12 [in Obs.list_tools]
b:12 [in Obs.laws]
b:12 [in Obs.equiv_obs]
b:121 [in Obs.coherence_graph]
b:124 [in Obs.list_dec]
b:125 [in Obs.list_dec]
b:126 [in Obs.list_dec]
b:127 [in Obs.list_dec]
b:128 [in Obs.list_dec]
B:129 [in Obs.list_tools]
b:129 [in Obs.list_dec]
b:13 [in Obs.coherence_graph]
b:13 [in Obs.anticlique]
b:130 [in Obs.list_dec]
b:131 [in Obs.list_dec]
b:132 [in Obs.coherence_graph]
b:138 [in Obs.coherence_graph]
b:140 [in Obs.coherence_graph]
b:147 [in Obs.list_tools]
B:149 [in Obs.list_tools]
b:15 [in Obs.laws]
B:15 [in Obs.notations]
B:155 [in Obs.list_tools]
b:16 [in Obs.coherence_graph]
b:16 [in Obs.equiv_obs]
B:160 [in Obs.list_tools]
B:168 [in Obs.list_tools]
B:177 [in Obs.list_tools]
b:18 [in Obs.laws]
b:18 [in Obs.product]
b:18 [in Obs.anticlique]
b:18 [in Obs.notations]
B:181 [in Obs.list_tools]
b:184 [in Obs.list_tools]
b:187 [in Obs.coherence_graph]
b:19 [in Obs.coherence_graph]
b:19 [in Obs.fan]
b:19 [in Obs.list_dec]
b:190 [in Obs.coherence_graph]
b:194 [in Obs.list_dec]
B:196 [in Obs.list_dec]
B:199 [in Obs.list_tools]
b:20 [in Obs.laws]
b:20 [in Obs.equiv_obs]
B:202 [in Obs.list_tools]
B:205 [in Obs.list_dec]
b:21 [in Obs.coherence_graph]
B:21 [in Obs.decidable_prop]
b:21 [in Obs.product]
b:21 [in Obs.fan]
b:21 [in Obs.notations]
b:210 [in Obs.list_dec]
B:212 [in Obs.list_dec]
B:217 [in Obs.list_tools]
B:219 [in Obs.list_dec]
b:22 [in Obs.list_dec]
B:220 [in Obs.list_tools]
b:23 [in Obs.laws]
b:23 [in Obs.notations]
B:230 [in Obs.list_tools]
b:231 [in Obs.product]
b:233 [in Obs.product]
b:235 [in Obs.product]
b:237 [in Obs.product]
b:239 [in Obs.product]
b:24 [in Obs.equiv_obs]
b:24 [in Obs.notations]
b:241 [in Obs.product]
b:25 [in Obs.laws]
b:26 [in Obs.coherence_graph]
b:26 [in Obs.product]
B:267 [in Obs.list_tools]
b:27 [in Obs.laws]
b:27 [in Obs.equiv_obs]
B:273 [in Obs.list_tools]
B:279 [in Obs.list_tools]
B:285 [in Obs.list_tools]
b:29 [in Obs.coherence_graph]
B:294 [in Obs.list_tools]
b:30 [in Obs.product]
B:31 [in Obs.decidable_prop]
B:328 [in Obs.list_tools]
b:33 [in Obs.fan]
b:333 [in Obs.list_tools]
B:335 [in Obs.list_tools]
b:339 [in Obs.list_tools]
b:34 [in Obs.laws]
b:35 [in Obs.coherence_graph]
b:35 [in Obs.product]
b:37 [in Obs.laws]
b:39 [in Obs.laws]
B:39 [in Obs.equiv_obs]
b:39 [in Obs.anticlique]
b:41 [in Obs.list_dec]
b:415 [in Obs.list_tools]
b:42 [in Obs.coherence_graph]
b:42 [in Obs.laws]
b:44 [in Obs.laws]
b:46 [in Obs.laws]
B:47 [in Obs.equiv_obs]
b:48 [in Obs.laws]
b:5 [in Obs.fan]
b:51 [in Obs.laws]
b:52 [in Obs.coherence_graph]
B:52 [in Obs.equiv_obs]
b:53 [in Obs.laws]
b:54 [in Obs.coherence_graph]
b:56 [in Obs.laws]
b:56 [in Obs.sem_obs]
b:56 [in Obs.fan]
b:57 [in Obs.decidable_prop]
b:58 [in Obs.decidable_prop]
b:59 [in Obs.laws]
b:59 [in Obs.equiv_obs]
b:6 [in Obs.laws]
B:60 [in Obs.list_tools]
b:61 [in Obs.fan]
b:62 [in Obs.laws]
b:62 [in Obs.equiv_obs]
b:65 [in Obs.laws]
b:65 [in Obs.equiv_obs]
b:67 [in Obs.laws]
b:68 [in Obs.equiv_obs]
b:68 [in Obs.list_dec]
b:69 [in Obs.laws]
b:7 [in Obs.equiv_obs]
b:71 [in Obs.laws]
b:71 [in Obs.equiv_obs]
b:73 [in Obs.coherence_graph]
b:73 [in Obs.equiv_obs]
b:74 [in Obs.laws]
b:75 [in Obs.coherence_graph]
b:76 [in Obs.equiv_obs]
b:77 [in Obs.coherence_graph]
b:77 [in Obs.laws]
b:78 [in Obs.equiv_obs]
b:79 [in Obs.coherence_graph]
b:8 [in Obs.coherence_graph]
b:80 [in Obs.laws]
b:80 [in Obs.equiv_obs]
b:81 [in Obs.coherence_graph]
b:83 [in Obs.coherence_graph]
b:83 [in Obs.laws]
b:85 [in Obs.equiv_obs]
b:9 [in Obs.laws]
b:9 [in Obs.equiv_obs]
b:9 [in Obs.fin_sem_obs]
b:90 [in Obs.list_dec]
b:92 [in Obs.coherence_graph]
b:93 [in Obs.laws]
b:95 [in Obs.coherence_graph]
b:96 [in Obs.laws]
b:97 [in Obs.coherence_graph]
C
choose_clique_𝖦:7 [in Obs.product]cnf:147 [in Obs.product]
cnf:159 [in Obs.product]
cnf:179 [in Obs.product]
c':57 [in Obs.fan]
c':62 [in Obs.fan]
c':64 [in Obs.fan]
c':66 [in Obs.fan]
c:10 [in Obs.equiv_obs]
c:13 [in Obs.laws]
c:13 [in Obs.equiv_obs]
c:145 [in Obs.list_tools]
C:156 [in Obs.list_tools]
c:166 [in Obs.product]
c:17 [in Obs.equiv_obs]
c:170 [in Obs.product]
c:173 [in Obs.product]
c:175 [in Obs.product]
c:19 [in Obs.notations]
c:21 [in Obs.equiv_obs]
c:22 [in Obs.notations]
C:231 [in Obs.list_tools]
c:28 [in Obs.laws]
c:35 [in Obs.laws]
c:40 [in Obs.laws]
c:50 [in Obs.laws]
c:54 [in Obs.laws]
c:54 [in Obs.fan]
c:57 [in Obs.laws]
c:59 [in Obs.fan]
c:60 [in Obs.laws]
c:60 [in Obs.equiv_obs]
c:63 [in Obs.laws]
c:66 [in Obs.equiv_obs]
c:7 [in Obs.laws]
c:72 [in Obs.laws]
c:75 [in Obs.laws]
c:78 [in Obs.laws]
c:81 [in Obs.laws]
c:81 [in Obs.equiv_obs]
c:84 [in Obs.laws]
c:92 [in Obs.product]
D
decG:147 [in Obs.laws]decG:2 [in Obs.fin_sem_obs]
decG:2 [in Obs.sem_obs]
decG:61 [in Obs.sem_obs]
decG:62 [in Obs.coherence_graph]
decG:7 [in Obs.syntax_obs]
decG:8 [in Obs.fan]
decG:86 [in Obs.equiv_obs]
decG:89 [in Obs.coherence_graph]
decIdx:2 [in Obs.product]
decV:2 [in Obs.anticlique]
dec_A:2 [in Obs.list_dec]
dec𝖦:5 [in Obs.product]
dnf:143 [in Obs.product]
dnf:152 [in Obs.product]
dnf:172 [in Obs.product]
dnf:182 [in Obs.product]
d:14 [in Obs.equiv_obs]
d:168 [in Obs.product]
d:174 [in Obs.product]
d:176 [in Obs.product]
d:18 [in Obs.equiv_obs]
d:22 [in Obs.equiv_obs]
d:52 [in Obs.decidable_prop]
D:8 [in Obs.decidable_prop]
d:93 [in Obs.product]
E
elts:341 [in Obs.list_tools]elts:348 [in Obs.list_tools]
e:346 [in Obs.list_tools]
e:352 [in Obs.list_tools]
e:356 [in Obs.list_tools]
e:5 [in Obs.notations]
F
fanG:3 [in Obs.fin_sem_obs]FanG:9 [in Obs.fan]
f:119 [in Obs.laws]
f:121 [in Obs.list_tools]
f:124 [in Obs.laws]
f:128 [in Obs.laws]
f:130 [in Obs.list_tools]
f:132 [in Obs.list_dec]
f:133 [in Obs.laws]
f:136 [in Obs.list_dec]
f:137 [in Obs.list_tools]
f:14 [in Obs.list_tools]
f:142 [in Obs.list_tools]
f:150 [in Obs.list_tools]
f:199 [in Obs.list_dec]
f:200 [in Obs.list_tools]
f:203 [in Obs.list_tools]
f:205 [in Obs.list_tools]
f:207 [in Obs.list_tools]
f:215 [in Obs.list_dec]
f:218 [in Obs.list_tools]
f:221 [in Obs.list_tools]
f:222 [in Obs.list_dec]
f:223 [in Obs.list_tools]
f:225 [in Obs.list_tools]
f:248 [in Obs.list_tools]
f:253 [in Obs.list_tools]
f:258 [in Obs.list_tools]
f:264 [in Obs.list_tools]
f:268 [in Obs.list_tools]
f:274 [in Obs.list_tools]
f:280 [in Obs.list_tools]
f:359 [in Obs.list_tools]
f:364 [in Obs.list_tools]
f:368 [in Obs.list_tools]
f:372 [in Obs.list_tools]
f:376 [in Obs.list_tools]
f:381 [in Obs.list_tools]
f:386 [in Obs.list_tools]
f:391 [in Obs.list_tools]
f:397 [in Obs.list_tools]
f:402 [in Obs.list_tools]
f:406 [in Obs.list_tools]
f:411 [in Obs.list_tools]
f:418 [in Obs.list_tools]
f:45 [in Obs.list_tools]
f:49 [in Obs.list_tools]
f:52 [in Obs.list_tools]
f:56 [in Obs.list_tools]
f:58 [in Obs.list_dec]
f:60 [in Obs.list_dec]
f:61 [in Obs.list_tools]
f:66 [in Obs.list_tools]
f:71 [in Obs.list_tools]
f:78 [in Obs.list_tools]
G
G:1 [in Obs.laws]G:1 [in Obs.equiv_obs]
G:1 [in Obs.fin_sem_obs]
G:1 [in Obs.sem_obs]
G:1 [in Obs.fan]
G:1 [in Obs.syntax_obs]
g:120 [in Obs.laws]
g:129 [in Obs.laws]
g:254 [in Obs.list_tools]
g:259 [in Obs.list_tools]
g:269 [in Obs.list_tools]
g:275 [in Obs.list_tools]
g:281 [in Obs.list_tools]
g:377 [in Obs.list_tools]
g:382 [in Obs.list_tools]
g:387 [in Obs.list_tools]
g:392 [in Obs.list_tools]
g:398 [in Obs.list_tools]
G:4 [in Obs.syntax_obs]
g:407 [in Obs.list_tools]
g:412 [in Obs.list_tools]
G:5 [in Obs.syntax_obs]
G:55 [in Obs.coherence_graph]
G:6 [in Obs.coherence_graph]
G:6 [in Obs.syntax_obs]
G:60 [in Obs.sem_obs]
G:61 [in Obs.coherence_graph]
g:62 [in Obs.list_tools]
g:67 [in Obs.list_tools]
G:7 [in Obs.fan]
g:72 [in Obs.list_tools]
G:88 [in Obs.coherence_graph]
H
H0:198 [in Obs.list_dec]H0:207 [in Obs.list_dec]
H0:214 [in Obs.list_dec]
H0:221 [in Obs.list_dec]
H:197 [in Obs.list_dec]
H:206 [in Obs.list_dec]
H:213 [in Obs.list_dec]
H:220 [in Obs.list_dec]
h:393 [in Obs.list_tools]
H:53 [in Obs.sem_obs]
H:54 [in Obs.decidable_prop]
H:56 [in Obs.decidable_prop]
H:57 [in Obs.sem_obs]
H:59 [in Obs.sem_obs]
H:61 [in Obs.decidable_prop]
H:9 [in Obs.notations]
I
Idx:1 [in Obs.product]idx:133 [in Obs.product]
idx:137 [in Obs.product]
i:102 [in Obs.product]
i:103 [in Obs.product]
i:104 [in Obs.product]
i:107 [in Obs.product]
i:108 [in Obs.product]
i:109 [in Obs.product]
i:11 [in Obs.product]
i:112 [in Obs.product]
i:119 [in Obs.product]
i:121 [in Obs.product]
i:125 [in Obs.product]
i:130 [in Obs.product]
i:136 [in Obs.product]
i:140 [in Obs.product]
i:141 [in Obs.product]
i:142 [in Obs.product]
I:144 [in Obs.product]
i:146 [in Obs.product]
I:148 [in Obs.product]
i:15 [in Obs.product]
i:150 [in Obs.product]
I:151 [in Obs.product]
i:156 [in Obs.product]
I:158 [in Obs.product]
i:163 [in Obs.product]
I:165 [in Obs.product]
I:167 [in Obs.product]
I:169 [in Obs.product]
I:171 [in Obs.product]
I:177 [in Obs.product]
I:180 [in Obs.product]
i:183 [in Obs.product]
i:19 [in Obs.product]
i:192 [in Obs.product]
i:201 [in Obs.product]
i:202 [in Obs.product]
i:205 [in Obs.product]
i:208 [in Obs.product]
i:212 [in Obs.product]
i:214 [in Obs.product]
i:215 [in Obs.product]
I:216 [in Obs.product]
i:24 [in Obs.product]
i:27 [in Obs.product]
i:33 [in Obs.product]
i:36 [in Obs.product]
i:4 [in Obs.product]
i:40 [in Obs.product]
i:44 [in Obs.product]
i:47 [in Obs.product]
i:51 [in Obs.product]
i:55 [in Obs.product]
i:59 [in Obs.product]
i:6 [in Obs.product]
i:62 [in Obs.product]
i:66 [in Obs.product]
i:69 [in Obs.product]
i:71 [in Obs.product]
i:78 [in Obs.product]
i:8 [in Obs.product]
i:82 [in Obs.product]
i:83 [in Obs.product]
i:87 [in Obs.product]
I:90 [in Obs.product]
i:91 [in Obs.product]
i:95 [in Obs.product]
i:98 [in Obs.product]
i:99 [in Obs.product]
J
j:157 [in Obs.product]j:16 [in Obs.product]
j:164 [in Obs.product]
J:178 [in Obs.product]
J:181 [in Obs.product]
j:221 [in Obs.product]
j:28 [in Obs.product]
j:75 [in Obs.product]
K
k:290 [in Obs.list_tools]k:299 [in Obs.list_tools]
k:325 [in Obs.list_tools]
L
l':42 [in Obs.list_tools]l1:132 [in Obs.list_tools]
l1:161 [in Obs.list_tools]
l1:23 [in Obs.list_dec]
l1:245 [in Obs.list_tools]
l1:25 [in Obs.list_dec]
l1:29 [in Obs.list_dec]
l1:41 [in Obs.decidable_prop]
l1:43 [in Obs.decidable_prop]
l1:431 [in Obs.list_tools]
l1:441 [in Obs.list_tools]
l1:443 [in Obs.list_tools]
l1:445 [in Obs.list_tools]
l1:84 [in Obs.list_dec]
l1:85 [in Obs.list_tools]
l1:90 [in Obs.list_tools]
l1:94 [in Obs.list_dec]
l1:98 [in Obs.list_dec]
l2:133 [in Obs.list_tools]
l2:163 [in Obs.list_tools]
l2:24 [in Obs.list_dec]
l2:246 [in Obs.list_tools]
l2:26 [in Obs.list_dec]
l2:30 [in Obs.list_dec]
l2:42 [in Obs.decidable_prop]
l2:432 [in Obs.list_tools]
l2:44 [in Obs.decidable_prop]
l2:442 [in Obs.list_tools]
l2:444 [in Obs.list_tools]
l2:446 [in Obs.list_tools]
l2:85 [in Obs.list_dec]
l2:86 [in Obs.list_tools]
l2:91 [in Obs.list_tools]
l2:95 [in Obs.list_dec]
l2:99 [in Obs.list_dec]
l3:162 [in Obs.list_tools]
l4:164 [in Obs.list_tools]
l:103 [in Obs.list_dec]
l:105 [in Obs.list_dec]
l:107 [in Obs.list_dec]
l:109 [in Obs.list_dec]
l:11 [in Obs.list_dec]
l:110 [in Obs.product]
l:111 [in Obs.list_dec]
l:113 [in Obs.product]
l:113 [in Obs.list_dec]
l:114 [in Obs.list_tools]
l:116 [in Obs.product]
l:116 [in Obs.list_dec]
l:117 [in Obs.list_tools]
l:119 [in Obs.list_dec]
l:121 [in Obs.laws]
l:121 [in Obs.list_dec]
l:122 [in Obs.list_tools]
l:125 [in Obs.list_tools]
l:125 [in Obs.laws]
L:127 [in Obs.list_tools]
l:13 [in Obs.list_tools]
l:13 [in Obs.list_dec]
l:130 [in Obs.laws]
l:133 [in Obs.list_dec]
l:134 [in Obs.laws]
l:137 [in Obs.list_dec]
l:138 [in Obs.list_tools]
l:141 [in Obs.list_dec]
l:143 [in Obs.list_tools]
l:15 [in Obs.list_dec]
l:151 [in Obs.list_tools]
l:157 [in Obs.list_tools]
l:161 [in Obs.coherence_graph]
l:163 [in Obs.coherence_graph]
l:165 [in Obs.list_tools]
l:165 [in Obs.coherence_graph]
l:167 [in Obs.coherence_graph]
l:17 [in Obs.fan]
l:17 [in Obs.list_dec]
l:170 [in Obs.coherence_graph]
l:172 [in Obs.coherence_graph]
l:174 [in Obs.coherence_graph]
l:176 [in Obs.coherence_graph]
l:178 [in Obs.list_tools]
l:179 [in Obs.coherence_graph]
l:18 [in Obs.list_tools]
l:186 [in Obs.list_tools]
l:19 [in Obs.list_tools]
l:192 [in Obs.list_dec]
l:203 [in Obs.list_dec]
l:213 [in Obs.list_tools]
l:216 [in Obs.list_dec]
L:22 [in Obs.fan]
l:223 [in Obs.list_dec]
l:226 [in Obs.list_dec]
l:228 [in Obs.list_dec]
l:23 [in Obs.list_tools]
l:231 [in Obs.list_dec]
l:233 [in Obs.list_tools]
l:237 [in Obs.list_tools]
l:239 [in Obs.list_tools]
l:242 [in Obs.list_tools]
l:249 [in Obs.list_tools]
l:25 [in Obs.list_tools]
l:255 [in Obs.list_tools]
L:26 [in Obs.fan]
l:260 [in Obs.list_tools]
l:263 [in Obs.list_tools]
l:27 [in Obs.fan]
l:270 [in Obs.list_tools]
l:276 [in Obs.list_tools]
l:28 [in Obs.list_dec]
l:282 [in Obs.list_tools]
l:29 [in Obs.list_tools]
l:3 [in Obs.list_tools]
l:3 [in Obs.list_dec]
l:3 [in Obs.anticlique]
l:309 [in Obs.list_tools]
l:31 [in Obs.list_tools]
l:313 [in Obs.list_tools]
l:318 [in Obs.list_tools]
l:321 [in Obs.list_tools]
l:326 [in Obs.list_tools]
l:329 [in Obs.list_tools]
l:336 [in Obs.list_tools]
l:345 [in Obs.list_tools]
l:35 [in Obs.list_tools]
l:350 [in Obs.list_tools]
l:353 [in Obs.list_tools]
l:357 [in Obs.list_tools]
l:360 [in Obs.list_tools]
l:365 [in Obs.list_tools]
l:369 [in Obs.list_tools]
l:373 [in Obs.list_tools]
l:378 [in Obs.list_tools]
l:383 [in Obs.list_tools]
l:388 [in Obs.list_tools]
l:39 [in Obs.fan]
l:394 [in Obs.list_tools]
l:399 [in Obs.list_tools]
l:403 [in Obs.list_tools]
l:408 [in Obs.list_tools]
l:41 [in Obs.list_tools]
l:41 [in Obs.fan]
l:413 [in Obs.list_tools]
l:419 [in Obs.list_tools]
l:42 [in Obs.list_dec]
l:422 [in Obs.list_tools]
l:425 [in Obs.list_tools]
l:429 [in Obs.list_tools]
l:433 [in Obs.list_tools]
l:435 [in Obs.list_tools]
l:437 [in Obs.list_tools]
l:439 [in Obs.list_tools]
l:447 [in Obs.list_tools]
l:45 [in Obs.list_dec]
l:453 [in Obs.list_tools]
l:456 [in Obs.list_tools]
l:46 [in Obs.list_tools]
l:47 [in Obs.list_dec]
l:48 [in Obs.list_dec]
l:49 [in Obs.list_dec]
l:50 [in Obs.list_tools]
l:50 [in Obs.list_dec]
l:52 [in Obs.list_dec]
l:53 [in Obs.list_tools]
l:53 [in Obs.list_dec]
l:57 [in Obs.list_tools]
l:57 [in Obs.list_dec]
l:59 [in Obs.list_dec]
l:6 [in Obs.list_tools]
l:6 [in Obs.list_dec]
l:63 [in Obs.list_tools]
l:63 [in Obs.list_dec]
l:64 [in Obs.list_dec]
l:66 [in Obs.list_dec]
l:68 [in Obs.list_tools]
l:70 [in Obs.list_dec]
l:72 [in Obs.list_dec]
l:73 [in Obs.list_tools]
l:73 [in Obs.decidable_prop]
l:76 [in Obs.list_tools]
l:76 [in Obs.list_dec]
l:78 [in Obs.list_dec]
l:79 [in Obs.list_tools]
l:80 [in Obs.decidable_prop]
l:82 [in Obs.list_tools]
l:82 [in Obs.list_dec]
l:87 [in Obs.list_dec]
l:88 [in Obs.list_dec]
l:9 [in Obs.list_tools]
l:9 [in Obs.list_dec]
l:91 [in Obs.list_dec]
M
m':319 [in Obs.list_tools]m':323 [in Obs.list_tools]
m':454 [in Obs.list_tools]
m1:134 [in Obs.list_tools]
m1:87 [in Obs.list_tools]
m1:92 [in Obs.list_tools]
m1:96 [in Obs.list_dec]
m2:135 [in Obs.list_tools]
m2:88 [in Obs.list_tools]
m2:93 [in Obs.list_tools]
m2:97 [in Obs.list_dec]
m:10 [in Obs.list_tools]
m:100 [in Obs.list_dec]
m:115 [in Obs.list_tools]
m:118 [in Obs.list_tools]
m:122 [in Obs.list_dec]
m:126 [in Obs.list_tools]
m:131 [in Obs.list_tools]
m:134 [in Obs.list_dec]
m:138 [in Obs.list_dec]
m:139 [in Obs.list_tools]
m:140 [in Obs.list_dec]
m:144 [in Obs.list_tools]
m:152 [in Obs.list_tools]
m:158 [in Obs.list_tools]
m:179 [in Obs.list_tools]
m:180 [in Obs.coherence_graph]
m:187 [in Obs.list_tools]
m:229 [in Obs.list_dec]
m:232 [in Obs.list_dec]
m:234 [in Obs.list_tools]
m:24 [in Obs.list_tools]
m:240 [in Obs.list_tools]
m:243 [in Obs.list_tools]
m:283 [in Obs.list_tools]
m:30 [in Obs.list_tools]
m:314 [in Obs.list_tools]
m:317 [in Obs.list_tools]
m:322 [in Obs.list_tools]
m:366 [in Obs.list_tools]
m:370 [in Obs.list_tools]
m:374 [in Obs.list_tools]
m:4 [in Obs.list_dec]
m:430 [in Obs.list_tools]
m:434 [in Obs.list_tools]
m:436 [in Obs.list_tools]
m:438 [in Obs.list_tools]
m:440 [in Obs.list_tools]
m:448 [in Obs.list_tools]
m:449 [in Obs.list_tools]
m:452 [in Obs.list_tools]
m:457 [in Obs.list_tools]
m:47 [in Obs.list_tools]
m:54 [in Obs.list_dec]
m:7 [in Obs.list_dec]
m:92 [in Obs.list_dec]
N
nc:155 [in Obs.product]nd:162 [in Obs.product]
n:10 [in Obs.list_dec]
n:12 [in Obs.list_dec]
n:14 [in Obs.list_dec]
n:145 [in Obs.product]
n:149 [in Obs.product]
n:153 [in Obs.list_tools]
n:16 [in Obs.list_dec]
n:211 [in Obs.product]
n:213 [in Obs.product]
n:244 [in Obs.list_tools]
n:303 [in Obs.list_tools]
n:342 [in Obs.list_tools]
n:349 [in Obs.list_tools]
n:8 [in Obs.list_dec]
n:91 [in Obs.decidable_prop]
O
o1:13 [in Obs.sem_obs]o1:16 [in Obs.sem_obs]
o1:19 [in Obs.sem_obs]
o1:28 [in Obs.fin_sem_obs]
o1:31 [in Obs.fin_sem_obs]
o1:34 [in Obs.fin_sem_obs]
o2:14 [in Obs.sem_obs]
o2:17 [in Obs.sem_obs]
o2:20 [in Obs.sem_obs]
o2:29 [in Obs.fin_sem_obs]
o2:32 [in Obs.fin_sem_obs]
o2:35 [in Obs.fin_sem_obs]
o:18 [in Obs.fin_sem_obs]
o:28 [in Obs.anticlique]
o:4 [in Obs.sem_obs]
o:55 [in Obs.anticlique]
o:59 [in Obs.anticlique]
o:6 [in Obs.notations]
o:61 [in Obs.anticlique]
o:63 [in Obs.anticlique]
P
p1:63 [in Obs.decidable_prop]p1:65 [in Obs.decidable_prop]
p1:67 [in Obs.decidable_prop]
p1:69 [in Obs.decidable_prop]
p2:64 [in Obs.decidable_prop]
p2:66 [in Obs.decidable_prop]
p2:68 [in Obs.decidable_prop]
p2:70 [in Obs.decidable_prop]
p:113 [in Obs.laws]
p:116 [in Obs.laws]
P:16 [in Obs.list_tools]
p:16 [in Obs.fan]
p:191 [in Obs.product]
P:21 [in Obs.list_tools]
p:235 [in Obs.list_tools]
p:25 [in Obs.fan]
P:27 [in Obs.list_tools]
P:417 [in Obs.list_tools]
P:45 [in Obs.decidable_prop]
p:50 [in Obs.equiv_obs]
p:51 [in Obs.decidable_prop]
p:53 [in Obs.decidable_prop]
p:55 [in Obs.decidable_prop]
p:55 [in Obs.equiv_obs]
p:59 [in Obs.decidable_prop]
p:62 [in Obs.decidable_prop]
p:72 [in Obs.decidable_prop]
p:79 [in Obs.decidable_prop]
P:81 [in Obs.list_tools]
p:85 [in Obs.decidable_prop]
Q
q:86 [in Obs.decidable_prop]R
r:330 [in Obs.list_tools]r:337 [in Obs.list_tools]
S
sat:16 [in Obs.notations]s1:169 [in Obs.list_tools]
s1:174 [in Obs.list_tools]
s1:291 [in Obs.list_tools]
s1:300 [in Obs.list_tools]
s2:170 [in Obs.list_tools]
s2:175 [in Obs.list_tools]
s2:292 [in Obs.list_tools]
s2:301 [in Obs.list_tools]
s3:171 [in Obs.list_tools]
s4:172 [in Obs.list_tools]
s:10 [in Obs.fin_sem_obs]
s:122 [in Obs.product]
s:126 [in Obs.product]
s:13 [in Obs.fin_sem_obs]
s:131 [in Obs.product]
s:136 [in Obs.laws]
s:139 [in Obs.laws]
s:142 [in Obs.laws]
s:145 [in Obs.laws]
s:185 [in Obs.product]
s:188 [in Obs.product]
s:193 [in Obs.product]
s:194 [in Obs.product]
s:195 [in Obs.product]
s:197 [in Obs.product]
s:199 [in Obs.product]
s:204 [in Obs.product]
s:207 [in Obs.product]
s:208 [in Obs.list_dec]
s:210 [in Obs.product]
s:28 [in Obs.fan]
s:3 [in Obs.laws]
s:31 [in Obs.sem_obs]
s:32 [in Obs.sem_obs]
s:34 [in Obs.sem_obs]
s:35 [in Obs.anticlique]
s:37 [in Obs.sem_obs]
s:38 [in Obs.fin_sem_obs]
s:38 [in Obs.sem_obs]
s:40 [in Obs.fin_sem_obs]
s:40 [in Obs.sem_obs]
s:42 [in Obs.equiv_obs]
s:42 [in Obs.fin_sem_obs]
s:42 [in Obs.sem_obs]
s:43 [in Obs.fan]
s:44 [in Obs.equiv_obs]
s:44 [in Obs.sem_obs]
s:44 [in Obs.fan]
s:46 [in Obs.fan]
s:47 [in Obs.sem_obs]
s:48 [in Obs.equiv_obs]
s:51 [in Obs.anticlique]
s:52 [in Obs.sem_obs]
s:52 [in Obs.fan]
s:53 [in Obs.equiv_obs]
s:53 [in Obs.anticlique]
s:66 [in Obs.anticlique]
s:69 [in Obs.anticlique]
s:71 [in Obs.fan]
s:71 [in Obs.anticlique]
s:73 [in Obs.anticlique]
s:74 [in Obs.anticlique]
s:76 [in Obs.fan]
s:78 [in Obs.anticlique]
s:79 [in Obs.anticlique]
s:8 [in Obs.syntax_obs]
s:80 [in Obs.fan]
s:81 [in Obs.anticlique]
s:84 [in Obs.product]
s:84 [in Obs.anticlique]
s:85 [in Obs.anticlique]
s:88 [in Obs.product]
s:88 [in Obs.anticlique]
s:89 [in Obs.laws]
s:89 [in Obs.anticlique]
s:90 [in Obs.laws]
s:90 [in Obs.equiv_obs]
s:91 [in Obs.anticlique]
T
t1:288 [in Obs.list_tools]t1:297 [in Obs.list_tools]
t2:289 [in Obs.list_tools]
t2:298 [in Obs.list_tools]
t:123 [in Obs.product]
t:127 [in Obs.product]
t:132 [in Obs.product]
t:150 [in Obs.coherence_graph]
T:189 [in Obs.list_tools]
T:190 [in Obs.list_tools]
T:191 [in Obs.list_tools]
T:192 [in Obs.list_tools]
T:193 [in Obs.list_tools]
T:194 [in Obs.list_tools]
T:196 [in Obs.list_tools]
t:196 [in Obs.product]
t:198 [in Obs.product]
t:200 [in Obs.product]
T:214 [in Obs.list_tools]
T:215 [in Obs.list_tools]
T:226 [in Obs.list_tools]
T:228 [in Obs.list_tools]
t:287 [in Obs.list_tools]
t:296 [in Obs.list_tools]
t:33 [in Obs.sem_obs]
t:35 [in Obs.sem_obs]
t:36 [in Obs.anticlique]
t:39 [in Obs.sem_obs]
t:4 [in Obs.laws]
t:41 [in Obs.sem_obs]
t:43 [in Obs.equiv_obs]
t:43 [in Obs.fin_sem_obs]
t:43 [in Obs.sem_obs]
t:45 [in Obs.equiv_obs]
t:45 [in Obs.sem_obs]
t:45 [in Obs.fan]
t:47 [in Obs.fan]
t:48 [in Obs.sem_obs]
t:49 [in Obs.equiv_obs]
t:52 [in Obs.anticlique]
t:53 [in Obs.fan]
t:54 [in Obs.equiv_obs]
t:54 [in Obs.anticlique]
t:70 [in Obs.anticlique]
t:72 [in Obs.anticlique]
t:75 [in Obs.anticlique]
t:80 [in Obs.anticlique]
t:82 [in Obs.anticlique]
t:86 [in Obs.anticlique]
t:87 [in Obs.coherence_graph]
t:90 [in Obs.anticlique]
t:91 [in Obs.equiv_obs]
t:92 [in Obs.anticlique]
U
u1:101 [in Obs.list_tools]u1:107 [in Obs.list_tools]
u1:306 [in Obs.list_tools]
u1:32 [in Obs.list_dec]
u1:36 [in Obs.list_dec]
u1:95 [in Obs.list_tools]
u2:102 [in Obs.list_tools]
u2:108 [in Obs.list_tools]
u2:307 [in Obs.list_tools]
u2:33 [in Obs.list_dec]
u2:37 [in Obs.list_dec]
u2:96 [in Obs.list_tools]
u:11 [in Obs.sem_obs]
u:13 [in Obs.product]
u:135 [in Obs.laws]
u:138 [in Obs.laws]
u:141 [in Obs.laws]
u:143 [in Obs.list_dec]
u:144 [in Obs.laws]
u:146 [in Obs.list_dec]
u:149 [in Obs.list_dec]
u:150 [in Obs.list_dec]
u:153 [in Obs.list_dec]
u:156 [in Obs.list_dec]
u:159 [in Obs.list_dec]
u:161 [in Obs.list_dec]
u:163 [in Obs.list_dec]
u:165 [in Obs.list_dec]
u:168 [in Obs.list_dec]
u:171 [in Obs.list_dec]
u:174 [in Obs.list_dec]
u:177 [in Obs.list_dec]
u:180 [in Obs.list_dec]
u:183 [in Obs.list_dec]
u:186 [in Obs.list_dec]
u:187 [in Obs.list_dec]
u:189 [in Obs.list_dec]
u:20 [in Obs.anticlique]
u:22 [in Obs.coherence_graph]
u:22 [in Obs.anticlique]
u:25 [in Obs.anticlique]
u:26 [in Obs.fin_sem_obs]
u:304 [in Obs.list_tools]
u:31 [in Obs.product]
u:34 [in Obs.list_tools]
u:4 [in Obs.fin_sem_obs]
u:58 [in Obs.coherence_graph]
u:63 [in Obs.coherence_graph]
u:7 [in Obs.fin_sem_obs]
V
v':39 [in Obs.list_tools]v1:103 [in Obs.list_tools]
v1:109 [in Obs.list_tools]
v1:34 [in Obs.list_dec]
v1:38 [in Obs.list_dec]
v1:97 [in Obs.list_tools]
v2:104 [in Obs.list_tools]
v2:110 [in Obs.list_tools]
v2:35 [in Obs.list_dec]
v2:39 [in Obs.list_dec]
v2:98 [in Obs.list_tools]
V:1 [in Obs.anticlique]
v:114 [in Obs.product]
v:117 [in Obs.product]
v:14 [in Obs.product]
v:144 [in Obs.list_dec]
v:147 [in Obs.list_dec]
v:151 [in Obs.list_dec]
v:154 [in Obs.list_dec]
v:157 [in Obs.list_dec]
v:160 [in Obs.list_dec]
v:162 [in Obs.list_dec]
v:164 [in Obs.list_dec]
v:166 [in Obs.list_dec]
v:169 [in Obs.list_dec]
v:172 [in Obs.list_dec]
v:175 [in Obs.list_dec]
v:178 [in Obs.list_dec]
v:181 [in Obs.list_dec]
v:184 [in Obs.list_dec]
v:188 [in Obs.list_dec]
v:190 [in Obs.list_dec]
v:222 [in Obs.product]
v:224 [in Obs.product]
v:226 [in Obs.product]
v:228 [in Obs.product]
v:32 [in Obs.product]
v:33 [in Obs.list_tools]
v:37 [in Obs.list_tools]
v:38 [in Obs.product]
v:42 [in Obs.product]
v:49 [in Obs.product]
v:5 [in Obs.fin_sem_obs]
v:50 [in Obs.product]
v:52 [in Obs.product]
v:56 [in Obs.product]
v:59 [in Obs.coherence_graph]
v:64 [in Obs.coherence_graph]
v:8 [in Obs.fin_sem_obs]
W
w:105 [in Obs.list_tools]w:112 [in Obs.list_tools]
w:152 [in Obs.list_dec]
w:155 [in Obs.list_dec]
w:158 [in Obs.list_dec]
w:173 [in Obs.list_dec]
w:176 [in Obs.list_dec]
w:179 [in Obs.list_dec]
w:182 [in Obs.list_dec]
w:185 [in Obs.list_dec]
w:99 [in Obs.list_tools]
X
x1:200 [in Obs.list_dec]x2:201 [in Obs.list_dec]
X:1 [in Obs.decidable_prop]
x:10 [in Obs.sem_obs]
X:102 [in Obs.laws]
X:104 [in Obs.laws]
x:104 [in Obs.list_dec]
X:106 [in Obs.laws]
x:106 [in Obs.list_dec]
x:108 [in Obs.list_dec]
X:109 [in Obs.laws]
x:11 [in Obs.decidable_prop]
X:11 [in Obs.anticlique]
x:110 [in Obs.list_dec]
X:111 [in Obs.laws]
x:111 [in Obs.product]
x:112 [in Obs.list_dec]
X:113 [in Obs.list_tools]
X:114 [in Obs.laws]
x:114 [in Obs.list_dec]
x:115 [in Obs.product]
X:116 [in Obs.list_tools]
X:117 [in Obs.laws]
x:117 [in Obs.list_dec]
x:118 [in Obs.product]
x:12 [in Obs.sem_obs]
x:120 [in Obs.list_dec]
x:122 [in Obs.laws]
X:123 [in Obs.laws]
X:126 [in Obs.laws]
x:129 [in Obs.coherence_graph]
x:13 [in Obs.decidable_prop]
x:131 [in Obs.laws]
X:132 [in Obs.laws]
x:133 [in Obs.coherence_graph]
x:134 [in Obs.product]
x:135 [in Obs.coherence_graph]
x:135 [in Obs.list_dec]
x:137 [in Obs.laws]
x:138 [in Obs.product]
x:139 [in Obs.list_dec]
x:14 [in Obs.fin_sem_obs]
X:14 [in Obs.anticlique]
x:141 [in Obs.coherence_graph]
x:143 [in Obs.laws]
x:144 [in Obs.coherence_graph]
x:147 [in Obs.coherence_graph]
x:15 [in Obs.decidable_prop]
x:15 [in Obs.sem_obs]
x:151 [in Obs.coherence_graph]
x:154 [in Obs.coherence_graph]
x:157 [in Obs.coherence_graph]
x:16 [in Obs.decidable_prop]
x:162 [in Obs.coherence_graph]
x:164 [in Obs.coherence_graph]
x:166 [in Obs.coherence_graph]
x:168 [in Obs.coherence_graph]
x:17 [in Obs.fin_sem_obs]
x:171 [in Obs.coherence_graph]
x:173 [in Obs.coherence_graph]
x:175 [in Obs.coherence_graph]
x:177 [in Obs.coherence_graph]
x:18 [in Obs.decidable_prop]
x:18 [in Obs.sem_obs]
x:182 [in Obs.list_tools]
x:188 [in Obs.list_tools]
x:20 [in Obs.list_dec]
x:202 [in Obs.list_dec]
x:209 [in Obs.list_tools]
x:21 [in Obs.anticlique]
x:211 [in Obs.list_tools]
x:22 [in Obs.decidable_prop]
x:22 [in Obs.sem_obs]
x:225 [in Obs.list_dec]
x:23 [in Obs.coherence_graph]
x:23 [in Obs.fin_sem_obs]
x:24 [in Obs.decidable_prop]
x:24 [in Obs.fin_sem_obs]
x:24 [in Obs.anticlique]
x:25 [in Obs.fin_sem_obs]
x:25 [in Obs.sem_obs]
x:250 [in Obs.list_tools]
x:26 [in Obs.decidable_prop]
x:265 [in Obs.list_tools]
x:27 [in Obs.fin_sem_obs]
x:27 [in Obs.anticlique]
x:28 [in Obs.decidable_prop]
x:28 [in Obs.sem_obs]
x:3 [in Obs.sem_obs]
x:30 [in Obs.fin_sem_obs]
x:305 [in Obs.list_tools]
x:31 [in Obs.fan]
x:31 [in Obs.anticlique]
x:32 [in Obs.decidable_prop]
x:33 [in Obs.fin_sem_obs]
x:34 [in Obs.decidable_prop]
x:34 [in Obs.fan]
x:36 [in Obs.decidable_prop]
x:379 [in Obs.list_tools]
x:38 [in Obs.decidable_prop]
x:38 [in Obs.fan]
x:384 [in Obs.list_tools]
x:389 [in Obs.list_tools]
x:39 [in Obs.coherence_graph]
x:395 [in Obs.list_tools]
x:4 [in Obs.decidable_prop]
X:4 [in Obs.notations]
x:40 [in Obs.fan]
x:400 [in Obs.list_tools]
x:404 [in Obs.list_tools]
x:42 [in Obs.anticlique]
x:47 [in Obs.coherence_graph]
x:48 [in Obs.coherence_graph]
x:48 [in Obs.fan]
x:49 [in Obs.decidable_prop]
x:50 [in Obs.fan]
x:50 [in Obs.anticlique]
X:51 [in Obs.list_dec]
x:54 [in Obs.list_tools]
x:55 [in Obs.list_dec]
x:56 [in Obs.list_dec]
x:61 [in Obs.list_dec]
x:64 [in Obs.list_tools]
x:64 [in Obs.anticlique]
x:65 [in Obs.coherence_graph]
x:67 [in Obs.list_dec]
x:69 [in Obs.list_tools]
X:7 [in Obs.decidable_prop]
x:70 [in Obs.fan]
x:74 [in Obs.list_tools]
x:75 [in Obs.fan]
x:8 [in Obs.sem_obs]
x:81 [in Obs.fan]
x:83 [in Obs.anticlique]
x:84 [in Obs.coherence_graph]
x:87 [in Obs.decidable_prop]
x:89 [in Obs.decidable_prop]
x:9 [in Obs.decidable_prop]
x:9 [in Obs.sem_obs]
X:92 [in Obs.laws]
X:95 [in Obs.laws]
X:97 [in Obs.laws]
X:99 [in Obs.laws]
Y
y:10 [in Obs.decidable_prop]Y:100 [in Obs.laws]
Y:112 [in Obs.laws]
Y:115 [in Obs.laws]
y:115 [in Obs.list_dec]
y:118 [in Obs.list_dec]
y:12 [in Obs.decidable_prop]
y:130 [in Obs.coherence_graph]
y:134 [in Obs.coherence_graph]
y:135 [in Obs.product]
y:136 [in Obs.coherence_graph]
y:139 [in Obs.product]
y:14 [in Obs.decidable_prop]
y:142 [in Obs.coherence_graph]
y:145 [in Obs.coherence_graph]
y:148 [in Obs.coherence_graph]
y:152 [in Obs.coherence_graph]
y:155 [in Obs.coherence_graph]
y:17 [in Obs.decidable_prop]
y:19 [in Obs.decidable_prop]
y:21 [in Obs.fin_sem_obs]
y:21 [in Obs.sem_obs]
y:23 [in Obs.decidable_prop]
y:25 [in Obs.decidable_prop]
y:251 [in Obs.list_tools]
y:27 [in Obs.decidable_prop]
y:29 [in Obs.decidable_prop]
y:29 [in Obs.sem_obs]
y:32 [in Obs.fan]
y:32 [in Obs.anticlique]
y:33 [in Obs.decidable_prop]
y:35 [in Obs.decidable_prop]
y:35 [in Obs.fan]
y:36 [in Obs.fin_sem_obs]
y:37 [in Obs.decidable_prop]
y:39 [in Obs.decidable_prop]
y:40 [in Obs.coherence_graph]
y:42 [in Obs.fan]
y:49 [in Obs.coherence_graph]
y:49 [in Obs.fan]
y:5 [in Obs.decidable_prop]
y:50 [in Obs.decidable_prop]
y:51 [in Obs.fan]
y:62 [in Obs.list_dec]
y:65 [in Obs.anticlique]
y:66 [in Obs.coherence_graph]
y:7 [in Obs.sem_obs]
y:74 [in Obs.fan]
y:85 [in Obs.coherence_graph]
y:88 [in Obs.decidable_prop]
y:90 [in Obs.decidable_prop]
Y:98 [in Obs.laws]
Z
z:143 [in Obs.coherence_graph]z:146 [in Obs.coherence_graph]
z:149 [in Obs.coherence_graph]
z:15 [in Obs.fin_sem_obs]
z:153 [in Obs.coherence_graph]
z:156 [in Obs.coherence_graph]
z:16 [in Obs.fin_sem_obs]
z:22 [in Obs.fin_sem_obs]
z:37 [in Obs.fin_sem_obs]
z:50 [in Obs.coherence_graph]
z:67 [in Obs.coherence_graph]
z:76 [in Obs.product]
z:77 [in Obs.product]
z:77 [in Obs.fan]
z:78 [in Obs.fan]
z:86 [in Obs.coherence_graph]
other
α:104 [in Obs.coherence_graph]α:106 [in Obs.coherence_graph]
α:109 [in Obs.coherence_graph]
α:112 [in Obs.coherence_graph]
α:119 [in Obs.coherence_graph]
α:12 [in Obs.fan]
α:124 [in Obs.coherence_graph]
α:126 [in Obs.coherence_graph]
α:127 [in Obs.coherence_graph]
α:14 [in Obs.fan]
α:158 [in Obs.coherence_graph]
α:178 [in Obs.coherence_graph]
α:181 [in Obs.coherence_graph]
α:203 [in Obs.product]
α:206 [in Obs.product]
α:209 [in Obs.product]
α:217 [in Obs.product]
α:25 [in Obs.coherence_graph]
α:28 [in Obs.coherence_graph]
α:30 [in Obs.sem_obs]
α:31 [in Obs.coherence_graph]
α:33 [in Obs.coherence_graph]
α:36 [in Obs.coherence_graph]
α:36 [in Obs.sem_obs]
α:37 [in Obs.product]
α:37 [in Obs.anticlique]
α:39 [in Obs.fin_sem_obs]
α:40 [in Obs.anticlique]
α:41 [in Obs.fin_sem_obs]
α:41 [in Obs.product]
α:43 [in Obs.coherence_graph]
α:44 [in Obs.anticlique]
α:45 [in Obs.product]
α:45 [in Obs.anticlique]
α:46 [in Obs.sem_obs]
α:47 [in Obs.anticlique]
α:48 [in Obs.product]
α:48 [in Obs.anticlique]
α:51 [in Obs.sem_obs]
α:53 [in Obs.product]
α:57 [in Obs.product]
α:58 [in Obs.anticlique]
α:60 [in Obs.product]
α:60 [in Obs.anticlique]
α:62 [in Obs.anticlique]
α:63 [in Obs.product]
α:68 [in Obs.product]
α:70 [in Obs.product]
α:72 [in Obs.product]
α:79 [in Obs.product]
α:79 [in Obs.fan]
α:87 [in Obs.anticlique]
α:89 [in Obs.equiv_obs]
α:89 [in Obs.product]
α:90 [in Obs.coherence_graph]
α:92 [in Obs.equiv_obs]
α:93 [in Obs.coherence_graph]
α:94 [in Obs.product]
α:98 [in Obs.coherence_graph]
α:99 [in Obs.coherence_graph]
β:100 [in Obs.product]
β:101 [in Obs.product]
β:105 [in Obs.product]
β:106 [in Obs.product]
β:128 [in Obs.coherence_graph]
β:218 [in Obs.product]
β:242 [in Obs.product]
β:243 [in Obs.product]
β:244 [in Obs.product]
β:245 [in Obs.product]
β:246 [in Obs.product]
β:247 [in Obs.product]
β:248 [in Obs.product]
β:249 [in Obs.product]
β:250 [in Obs.product]
β:251 [in Obs.product]
β:252 [in Obs.product]
β:253 [in Obs.product]
β:37 [in Obs.coherence_graph]
β:44 [in Obs.coherence_graph]
β:49 [in Obs.sem_obs]
β:50 [in Obs.sem_obs]
β:73 [in Obs.product]
β:80 [in Obs.product]
β:93 [in Obs.anticlique]
β:96 [in Obs.product]
β:97 [in Obs.product]
γ:219 [in Obs.product]
γ:74 [in Obs.product]
γ:81 [in Obs.product]
δ:220 [in Obs.product]
ϕ:60 [in Obs.decidable_prop]
𝖠:120 [in Obs.product]
𝖠:54 [in Obs.sem_obs]
𝖦:3 [in Obs.product]
Variable Index
C
combine.same_length [in Obs.list_tools]M
mix.same_length [in Obs.list_tools]S
s.infiniteV [in Obs.anticlique]s.𝖠_complete [in Obs.product]
Library Index
A
anticliqueC
coherence_graphD
decidable_propE
equiv_obsF
fanfin_sem_obs
L
lawslist_tools
list_dec
N
notationsP
productS
sem_obssyntax_obs
Lemma Index
A
all_subsets_nodup [in Obs.list_tools]andb_prop_iff [in Obs.decidable_prop]
and_Join [in Obs.laws]
anticlique_choose_clique [in Obs.anticlique]
anticlique_inf_or_cntrex [in Obs.anticlique]
app_comm [in Obs.list_tools]
app_idem [in Obs.list_tools]
app_eq_app_length [in Obs.list_tools]
auxiliary [in Obs.product]
axΩ_sound [in Obs.anticlique]
C
choose_clique_aux [in Obs.product]choose_clique_sat_dec [in Obs.sem_obs]
cliques_at_most_one_elt [in Obs.anticlique]
clique_sat_iff_fsat_proj [in Obs.fin_sem_obs]
cnf_support_incl [in Obs.product]
cnf_to_dnf_equiv [in Obs.product]
cnf_to_dnf_support [in Obs.product]
coh𝒢_sym [in Obs.product]
coh𝒢_refl [in Obs.product]
combine_split [in Obs.list_tools]
combine_app [in Obs.list_tools]
combine_snd [in Obs.list_tools]
combine_fst [in Obs.list_tools]
compat_are_coh [in Obs.coherence_graph]
completeness_anticlique_eq [in Obs.anticlique]
completeness_anticlique [in Obs.anticlique]
complete_inf__Ω [in Obs.anticlique]
Conj_spec [in Obs.fan]
D
decidable_incompatible_with_fcliques [in Obs.coherence_graph]decomposition [in Obs.list_dec]
decomp_unambiguous [in Obs.list_dec]
decomp_unique [in Obs.list_dec]
dec_compat_proj [in Obs.product]
dec_in_proj [in Obs.product]
dec_ssmaller_impl_dec_sequiv [in Obs.sem_obs]
dec_sequiv_impl_dec_ssmaller [in Obs.sem_obs]
dec_ssmaller_impl_dec_fsat [in Obs.sem_obs]
dec_fsat_impl_dec_ssmaller [in Obs.sem_obs]
difference_intersect [in Obs.list_dec]
difference_incl [in Obs.list_dec]
difference_nil [in Obs.list_dec]
difference_inter_l [in Obs.list_dec]
difference_inter_r [in Obs.list_dec]
difference_app_r [in Obs.list_dec]
difference_app_l [in Obs.list_dec]
difference_right_subs [in Obs.list_dec]
difference_spec [in Obs.list_dec]
dnf_support_incl [in Obs.product]
dnf_to_cnf_equiv [in Obs.product]
dnf_to_cnf_support [in Obs.product]
E
empt_max [in Obs.coherence_graph]empt_spec [in Obs.coherence_graph]
eo_Meet_impl [in Obs.laws]
eo_impl_Join [in Obs.laws]
eo_inf_in_Meet [in Obs.laws]
eo_inf_in_Join [in Obs.laws]
eo_top_impl [in Obs.laws]
eo_contradict [in Obs.laws]
eo_eq_bot_iff_inf_bot [in Obs.laws]
eo_eq_top_iff_top_inf [in Obs.laws]
eo_inf_bot [in Obs.laws]
eo_inf_top [in Obs.laws]
eo_impl_distr_left [in Obs.laws]
eo_distr2 [in Obs.laws]
eo_distr1 [in Obs.laws]
eo_curry [in Obs.laws]
eo_heyting [in Obs.laws]
eo_inf_o_impl [in Obs.laws]
eo_impl_mp [in Obs.laws]
eo_inf_impl_concl [in Obs.laws]
eo_inf_impl_right_mon [in Obs.laws]
eo_inf_and_right [in Obs.laws]
eo_inf_and_left [in Obs.laws]
eo_inf_or_right [in Obs.laws]
eo_inf_or_left [in Obs.laws]
eo_inf_and_r [in Obs.laws]
eo_inf_and_l [in Obs.laws]
eo_inf_or_r [in Obs.laws]
eo_inf_or_l [in Obs.laws]
eo_inf_o_and [in Obs.laws]
eo_or_idem [in Obs.laws]
eo_and_idem [in Obs.laws]
eo_or_top [in Obs.laws]
eo_and_bot [in Obs.laws]
eo_impl_distr [in Obs.laws]
eo_impl_concl [in Obs.laws]
eo_impl_premise [in Obs.laws]
eo_tauto [in Obs.laws]
eo_abs2 [in Obs.laws]
eo_abs1 [in Obs.laws]
eo_or_bot [in Obs.laws]
eo_or_comm [in Obs.laws]
eo_or_ass [in Obs.laws]
eo_and_top [in Obs.laws]
eo_and_comm [in Obs.laws]
eo_and_ass [in Obs.laws]
eo_prod_impl [in Obs.product]
eo_sound [in Obs.sem_obs]
eo_ax_complete [in Obs.fan]
eo_inf_dec [in Obs.fan]
eo_inf_complete [in Obs.fan]
eo_fan_clique_neg [in Obs.fan]
eo_Ω_neg [in Obs.anticlique]
eo_Ω_top' [in Obs.anticlique]
equal_list_spec [in Obs.list_dec]
equivalentb_spec [in Obs.list_dec]
eqX_refl [in Obs.decidable_prop]
eqX_false [in Obs.decidable_prop]
eqX_correct [in Obs.decidable_prop]
eq_shuffles [in Obs.list_tools]
eq_obs_inf_obs [in Obs.laws]
eq_axΩ_sound [in Obs.anticlique]
eq𝒱_proj2 [in Obs.product]
eq𝒱_proj1 [in Obs.product]
F
fan_choose_clique [in Obs.fan]FAN_sound [in Obs.fan]
fcic_None [in Obs.coherence_graph]
fcic_Some [in Obs.coherence_graph]
fcliques_coherent [in Obs.coherence_graph]
fcliques_sat_iff_fsat [in Obs.fin_sem_obs]
fcmem_coh [in Obs.coherence_graph]
fc_to_clique_iff [in Obs.coherence_graph]
fc_to_clique_spec [in Obs.coherence_graph]
filter_nil [in Obs.list_tools]
filter_NoDup [in Obs.list_tools]
filter_true [in Obs.list_tools]
filter_ext [in Obs.list_tools]
filter_ext_In [in Obs.list_tools]
filter_map [in Obs.list_tools]
filter_length_lt [in Obs.list_tools]
filter_length_eq [in Obs.list_tools]
filter_length [in Obs.list_tools]
filter_app [in Obs.list_tools]
fincompatible_incompatible [in Obs.coherence_graph]
finsat_spec [in Obs.fan]
fjoins_iff_joins [in Obs.coherence_graph]
flat_map_Join [in Obs.laws]
flat_map_Meet [in Obs.laws]
flip_proj2 [in Obs.list_tools]
flip_proj1 [in Obs.list_tools]
flip_app [in Obs.list_tools]
flip_involutive [in Obs.list_tools]
forallb_ext [in Obs.list_tools]
forallb_ext_In [in Obs.list_tools]
forallb_false_exists [in Obs.list_tools]
forall_existsb [in Obs.list_tools]
fsat_impl [in Obs.fin_sem_obs]
fsat_conj [in Obs.fin_sem_obs]
fsat_disj [in Obs.fin_sem_obs]
fsat_at [in Obs.fin_sem_obs]
fsat_bot [in Obs.fin_sem_obs]
fsat_top [in Obs.fin_sem_obs]
H
HA_A [in Obs.laws]ha_sound [in Obs.sem_obs]
I
impl_Join [in Obs.laws]impl_lst_spec [in Obs.fin_sem_obs]
impl_disj_cliques [in Obs.fan]
impl_disj [in Obs.fan]
impl_cliques [in Obs.fan]
inb_dec [in Obs.list_dec]
inb_false [in Obs.list_dec]
inb_spec [in Obs.list_dec]
inclb_correct [in Obs.list_dec]
incl_cons_disj' [in Obs.list_tools]
incl_cons_disj [in Obs.list_tools]
incl_split [in Obs.list_tools]
incl_app_split [in Obs.list_tools]
incl_app_or [in Obs.list_tools]
incl_nil [in Obs.list_tools]
incl_map [in Obs.list_tools]
incl_sem_iff_incl_fin_sem [in Obs.fin_sem_obs]
incoh_iff_same_component_and_incoh [in Obs.product]
incompatible_or_joins_f [in Obs.coherence_graph]
incompatible_incompat [in Obs.coherence_graph]
incompat_are_incoh [in Obs.coherence_graph]
inf_clique_compat [in Obs.coherence_graph]
inf_axΩ_sound [in Obs.anticlique]
inject_i_incompat [in Obs.product]
inject_i_member [in Obs.product]
insert_spec [in Obs.list_tools]
insert_map [in Obs.list_dec]
interect_nil [in Obs.list_dec]
intersect_incl [in Obs.list_dec]
intersect_meet_l [in Obs.list_dec]
intersect_comm [in Obs.list_dec]
intersect_ass [in Obs.list_dec]
intersect_app_r [in Obs.list_dec]
intersect_app_l [in Obs.list_dec]
intersect_spec [in Obs.list_dec]
In_shuffles [in Obs.list_tools]
In_flip [in Obs.list_tools]
in_concat [in Obs.list_tools]
in_cons_iff [in Obs.list_dec]
In_undup [in Obs.list_dec]
In_dec [in Obs.list_dec]
is_coherent_project_list [in Obs.coherence_graph]
Is_true_iff_eq_true [in Obs.decidable_prop]
Is_true_test [in Obs.decidable_prop]
J
joins_is_meet_f [in Obs.coherence_graph]joins_is_meet [in Obs.coherence_graph]
Join_map_equiv_pointwise [in Obs.laws]
Join_and_Join [in Obs.laws]
Join_app [in Obs.laws]
join_project' [in Obs.product]
join_project [in Obs.product]
L
length_app_tail [in Obs.list_tools]length_app [in Obs.list_tools]
length_sum_filter [in Obs.list_dec]
len_rev_induction [in Obs.list_tools]
len_induction [in Obs.list_tools]
Levi [in Obs.list_tools]
Levi_strict [in Obs.list_tools]
lift_prod_spec [in Obs.list_tools]
lists_of_length_spec [in Obs.list_tools]
M
map_eq_equivalent [in Obs.list_tools]map_ext_in_iff [in Obs.list_tools]
map_bij [in Obs.list_tools]
map_eq_id [in Obs.list_tools]
map_app_inverse [in Obs.list_tools]
map_undup_inj [in Obs.list_dec]
map_undup_id [in Obs.list_dec]
Meet_impl [in Obs.laws]
Meet_map_equiv_pointwise [in Obs.laws]
Meet_or_Meet [in Obs.laws]
Meet_app [in Obs.laws]
Meet_not_and_sgl_in [in Obs.anticlique]
Meet_not_and_sgl_not_in [in Obs.anticlique]
mem_is_sgl [in Obs.anticlique]
mix_app [in Obs.list_tools]
mix_snd [in Obs.list_tools]
mix_fst [in Obs.list_tools]
N
nb_map [in Obs.list_dec]nb_cons_eq [in Obs.list_dec]
nb_cons_neq [in Obs.list_dec]
nb_inv_nil [in Obs.list_dec]
nb_not_In [in Obs.list_dec]
nb_In [in Obs.list_dec]
nb_nil [in Obs.list_dec]
nb_count_occ [in Obs.list_dec]
neg_top'_is_bot [in Obs.anticlique]
neg_neg_axΩ [in Obs.anticlique]
nf_spec [in Obs.fan]
nil_or_last [in Obs.list_tools]
NoDupb_NoDup [in Obs.list_dec]
NoDup_shuffles [in Obs.list_tools]
NoDup_app [in Obs.list_tools]
NoDup_app_inv [in Obs.list_tools]
NoDup_remove_3 [in Obs.list_tools]
NoDup_nb' [in Obs.list_dec]
NoDup_nb [in Obs.list_dec]
NoDup_length [in Obs.list_dec]
NoDup_rev [in Obs.list_dec]
NoDup_undup_eq [in Obs.list_dec]
NoDup_undup [in Obs.list_dec]
normal_form_eq [in Obs.product]
normal_form_sup [in Obs.product]
not_nil_add [in Obs.list_tools]
not_incompatible_is_joins_f [in Obs.coherence_graph]
not_incompatible_is_joins [in Obs.coherence_graph]
O
obs_Join [in Obs.laws]obs_Meet [in Obs.laws]
obs_meet [in Obs.laws]
obs_join [in Obs.laws]
Obs_sound [in Obs.sem_obs]
Obs'_sound [in Obs.sem_obs]
obs𝖦_to_𝒯_sat [in Obs.product]
orb_prop_iff [in Obs.decidable_prop]
or_Meet [in Obs.laws]
P
pad_contents [in Obs.list_tools]pairs_spec [in Obs.list_tools]
product_choose_clique [in Obs.product]
project_project [in Obs.coherence_graph]
project_max [in Obs.coherence_graph]
project_larger [in Obs.coherence_graph]
project_incl [in Obs.coherence_graph]
project_spec [in Obs.coherence_graph]
project_proof [in Obs.coherence_graph]
project_inject [in Obs.product]
project_spec [in Obs.product]
proj_length [in Obs.list_tools]
R
rev_equivalent [in Obs.list_tools]rev_induction [in Obs.list_tools]
rmfst_flip [in Obs.list_dec]
rmfst_app_dec [in Obs.list_dec]
rmfst_comm [in Obs.list_dec]
rmfst_decr [in Obs.list_dec]
rmfst_in [in Obs.list_dec]
rmfst_notin [in Obs.list_dec]
rm_notin [in Obs.list_dec]
rm_equiv [in Obs.list_dec]
rm_In [in Obs.list_dec]
S
satisfies_Meet [in Obs.sem_obs]satisfies_Join [in Obs.sem_obs]
sat_impl [in Obs.sem_obs]
sat_conj [in Obs.sem_obs]
sat_disj [in Obs.sem_obs]
sat_at [in Obs.sem_obs]
sat_bot [in Obs.sem_obs]
sat_top [in Obs.sem_obs]
sat_iff_inf_finsat [in Obs.fan]
sem_bij_to_Obs__Ω [in Obs.anticlique]
sglf_proof [in Obs.coherence_graph]
sgl_spec [in Obs.coherence_graph]
shuffles_length [in Obs.list_tools]
shuffles_nodup [in Obs.list_tools]
shuffles_equiv [in Obs.list_tools]
shuffles_map [in Obs.list_dec]
shuffles_spec [in Obs.list_dec]
singleton_is_coherent [in Obs.coherence_graph]
SizeApp [in Obs.list_tools]
SizeCons [in Obs.list_tools]
SizeLength [in Obs.list_tools]
SizeMap [in Obs.list_tools]
SizeNil [in Obs.list_tools]
sound_τ_sat__Ω [in Obs.anticlique]
split_word [in Obs.list_tools]
split_fst [in Obs.list_tools]
split_snd [in Obs.list_tools]
split_app_unambiguous [in Obs.list_dec]
subsets_NoDup [in Obs.list_tools]
subsets_spec [in Obs.list_tools]
subsets_In [in Obs.list_tools]
sum_filter [in Obs.list_tools]
sum_lt [in Obs.list_tools]
sum_le [in Obs.list_tools]
sum_zero_in [in Obs.list_tools]
sum_add_distr [in Obs.list_tools]
sum_add [in Obs.list_tools]
sum_ext_In [in Obs.list_tools]
sum_ext [in Obs.list_tools]
sum_incr [in Obs.list_tools]
sum_eq_ND [in Obs.list_tools]
sum_incl_ND [in Obs.list_tools]
sum_app [in Obs.list_tools]
sum_incr_0_right [in Obs.list_dec]
sum_incr_0_left [in Obs.list_dec]
support_dominates_sem [in Obs.fin_sem_obs]
T
test_spec [in Obs.decidable_prop]test_Is_true [in Obs.decidable_prop]
test_reflect [in Obs.decidable_prop]
top'_or_neg [in Obs.anticlique]
top'_not_a [in Obs.anticlique]
top'_a [in Obs.anticlique]
U
undup_equivalent [in Obs.list_dec]undup_length [in Obs.list_dec]
V
var_clique [in Obs.laws]W
weak_excluded_middle [in Obs.anticlique]X
X_dec [in Obs.decidable_prop]other
ζ_ξ [in Obs.anticlique]ζ_empt [in Obs.anticlique]
ζ_sgl [in Obs.anticlique]
ζ_None [in Obs.anticlique]
ζ_Some [in Obs.anticlique]
ξ_to_Obs__Ω [in Obs.anticlique]
ξ_ζ [in Obs.anticlique]
π_spec [in Obs.sem_obs]
τ_to_Obs__Ω [in Obs.anticlique]
τ_impl__Ω [in Obs.anticlique]
τ_neg__Ω [in Obs.anticlique]
τ_meet__Ω [in Obs.anticlique]
τ_join__Ω [in Obs.anticlique]
τ_ξ [in Obs.anticlique]
τ_ζ [in Obs.anticlique]
𝒜_complete [in Obs.product]
𝒜_sound [in Obs.product]
𝖠_complete_inf [in Obs.product]
Constructor Index
C
coh_ij [in Obs.product]coh_i [in Obs.product]
D
dec_prop [in Obs.decidable_prop]E
eo_ax [in Obs.equiv_obs]eo_impl [in Obs.equiv_obs]
eo_and [in Obs.equiv_obs]
eo_or [in Obs.equiv_obs]
eo_trans [in Obs.equiv_obs]
eo_sym [in Obs.equiv_obs]
eo_re [in Obs.equiv_obs]
F
fan_clique_neg [in Obs.fan]H
ha_impl_distr [in Obs.equiv_obs]ha_impl_concl [in Obs.equiv_obs]
ha_impl_premise [in Obs.equiv_obs]
ha_tauto [in Obs.equiv_obs]
ha_abs2 [in Obs.equiv_obs]
ha_abs1 [in Obs.equiv_obs]
ha_or_bot [in Obs.equiv_obs]
ha_or_comm [in Obs.equiv_obs]
ha_or_ass [in Obs.equiv_obs]
ha_and_top [in Obs.equiv_obs]
ha_and_comm [in Obs.equiv_obs]
ha_and_ass [in Obs.equiv_obs]
J
jleft [in Obs.equiv_obs]jright [in Obs.equiv_obs]
N
node [in Obs.product]O
obs_clique_obs [in Obs.equiv_obs]obs_clique_impl [in Obs.equiv_obs]
obs_incoh [in Obs.equiv_obs]
o_impl [in Obs.syntax_obs]
o_and [in Obs.syntax_obs]
o_or [in Obs.syntax_obs]
o_obs [in Obs.syntax_obs]
o_false [in Obs.syntax_obs]
o_true [in Obs.syntax_obs]
P
prod_impl [in Obs.product]prod_idx [in Obs.product]
S
satisfies [in Obs.notations]size [in Obs.notations]
other
Ω_neg [in Obs.anticlique]Ω_top' [in Obs.anticlique]
Projection Index
A
an [in Obs.fan]an_spec [in Obs.fan]
C
coh [in Obs.coherence_graph]coh_sym [in Obs.coherence_graph]
coh_refl [in Obs.coherence_graph]
D
decidable_vertex [in Obs.coherence_graph]decidale_coh [in Obs.coherence_graph]
dec_prop [in Obs.decidable_prop]
E
eqX [in Obs.decidable_prop]eqX_eq [in Obs.decidable_prop]
I
incompat [in Obs.coherence_graph]incompat_None [in Obs.coherence_graph]
incompat_Some [in Obs.coherence_graph]
M
member [in Obs.coherence_graph]members_are_coh [in Obs.coherence_graph]
S
satisfies [in Obs.notations]size [in Obs.notations]
V
vertex [in Obs.coherence_graph]Inductive Index
C
coh𝒢 [in Obs.product]D
DecidableProp [in Obs.decidable_prop]E
equiv_Obs [in Obs.equiv_obs]F
fan_ax [in Obs.fan]H
ha_ax [in Obs.equiv_obs]J
join [in Obs.equiv_obs]O
observation [in Obs.syntax_obs]obs_ax [in Obs.equiv_obs]
obs'_ax [in Obs.equiv_obs]
P
prod_ax [in Obs.product]S
Satisfaction [in Obs.notations]Size [in Obs.notations]
other
Ω_ax [in Obs.anticlique]𝒱 [in Obs.product]
Instance Index
A
anticlique_dec_inf [in Obs.anticlique]Ax_impl_eq [in Obs.equiv_obs]
B
Boolean [in Obs.decidable_prop]C
cnf_support_proper [in Obs.product]cnf_support_proper_incl [in Obs.product]
compat_dec [in Obs.coherence_graph]
D
DecidableProp_equiv_prop [in Obs.decidable_prop]DecidableProp_exists_bnd [in Obs.decidable_prop]
DecidableProp_forall_bnd [in Obs.decidable_prop]
DecidableProp_iff [in Obs.decidable_prop]
DecidableProp_impl [in Obs.decidable_prop]
DecidableProp_disj [in Obs.decidable_prop]
DecidableProp_conj [in Obs.decidable_prop]
DecidableProp_neg [in Obs.decidable_prop]
DecidableProp_Eq [in Obs.decidable_prop]
DecidableProp_Equiv [in Obs.list_dec]
DecidableProp_Incl [in Obs.list_dec]
DecidableProp_In [in Obs.list_dec]
decidable_incompatible_f [in Obs.coherence_graph]
decidable_is_coherent [in Obs.coherence_graph]
decidable_incoh [in Obs.coherence_graph]
dec_option [in Obs.decidable_prop]
dec_sum [in Obs.decidable_prop]
dec_prod [in Obs.decidable_prop]
dec_list [in Obs.list_dec]
dec_sat [in Obs.anticlique]
dec_inf__Ω [in Obs.anticlique]
decΩ [in Obs.anticlique]
dec𝒢 [in Obs.product]
difference_proper_inf [in Obs.list_dec]
difference_proper [in Obs.list_dec]
dnf_support_proper [in Obs.product]
dnf_support_proper_incl [in Obs.product]
E
equivalent_lift_prod_Proper [in Obs.list_tools]equivalent_flat_map_Proper [in Obs.list_tools]
equivalent_rev_Proper [in Obs.list_tools]
equivalent_cons_Proper [in Obs.list_tools]
equivalent_app_Proper [in Obs.list_tools]
equivalent_Equivalence [in Obs.list_tools]
equiv_obs_equiv [in Obs.equiv_obs]
F
FAN_Obs [in Obs.fan]fc_to_clique_proper_eq [in Obs.coherence_graph]
fc_to_clique_proper [in Obs.coherence_graph]
filter_equivalent_Proper [in Obs.list_tools]
filter_incl_Proper [in Obs.list_tools]
fincompatible_eq [in Obs.coherence_graph]
fincompatible_inf [in Obs.coherence_graph]
finSat [in Obs.fin_sem_obs]
fjoins_proper [in Obs.coherence_graph]
I
incl_lift_prod_Proper [in Obs.list_tools]incl_flat_map_Proper [in Obs.list_tools]
incl_rev_Proper [in Obs.list_tools]
incl_cons_Proper [in Obs.list_tools]
incl_app_Proper [in Obs.list_tools]
incl_PartialOrder [in Obs.list_tools]
incl_PreOrder [in Obs.list_tools]
incoh_sym [in Obs.coherence_graph]
incoh_irrefl [in Obs.coherence_graph]
incompatible_eq [in Obs.coherence_graph]
incompatible_inf [in Obs.coherence_graph]
incompat_dec [in Obs.coherence_graph]
inf_obs_partialorder [in Obs.laws]
inf_obs_preorder [in Obs.laws]
intersect_proper [in Obs.list_dec]
intersect_proper_incl [in Obs.list_dec]
In_equivalent_Proper [in Obs.list_tools]
In_incl_Proper [in Obs.list_tools]
irrefl_fincompatible [in Obs.coherence_graph]
irrefl_incompatible [in Obs.coherence_graph]
Is_true_dec [in Obs.decidable_prop]
J
joins_proper [in Obs.coherence_graph]Join_equiv [in Obs.laws]
Join_monotone [in Obs.laws]
join_proper_right [in Obs.equiv_obs]
join_proper_left [in Obs.equiv_obs]
L
le_plus_Proper [in Obs.list_tools]lt_plus_Proper [in Obs.list_tools]
M
map_equivalent_Proper [in Obs.list_tools]map_incl_Proper [in Obs.list_tools]
Meet_equiv [in Obs.laws]
Meet_monotone [in Obs.laws]
N
NatNum [in Obs.decidable_prop]O
obs𝖦_to_𝒯_proper_inf [in Obs.product]obs𝖦_to_𝒯_proper [in Obs.product]
o_impl_inf [in Obs.laws]
o_and_inf [in Obs.laws]
o_or_inf [in Obs.laws]
o_impl_equiv [in Obs.equiv_obs]
o_or_equiv [in Obs.equiv_obs]
o_and_equiv [in Obs.equiv_obs]
P
PartialOrder_subrelation [in Obs.notations]product_sat_dec [in Obs.product]
project_proper_inf [in Obs.coherence_graph]
project_proper [in Obs.coherence_graph]
R
rm_incl_Proper [in Obs.list_dec]rm_equivalent_Proper [in Obs.list_dec]
S
satClique [in Obs.coherence_graph]satisfies_inf [in Obs.sem_obs]
satisfies_inf [in Obs.notations]
satisfies_proper [in Obs.notations]
satObs [in Obs.sem_obs]
satObs_proper [in Obs.sem_obs]
sat__Ω [in Obs.anticlique]
sequiv_Equiv [in Obs.notations]
SizeList [in Obs.list_tools]
ssmaller_PartialOrder [in Obs.notations]
ssmaller_PreOrder [in Obs.notations]
sym_fincompatible [in Obs.coherence_graph]
sym_incompatible [in Obs.coherence_graph]
U
undup_equivalent_Proper [in Obs.list_dec]undup_incl_Proper [in Obs.list_dec]
other
Ω [in Obs.anticlique]π_proper [in Obs.laws]
τ_proper_inf__Ω [in Obs.anticlique]
𝒢 [in Obs.product]
Section Index
C
combine [in Obs.list_tools]D
decidable [in Obs.decidable_prop]decidable_graph [in Obs.coherence_graph]
dec_list [in Obs.list_dec]
F
finite_cliques [in Obs.coherence_graph]flip [in Obs.list_tools]
M
mix [in Obs.list_tools]S
s [in Obs.coherence_graph]s [in Obs.laws]
s [in Obs.equiv_obs]
s [in Obs.fin_sem_obs]
s [in Obs.product]
s [in Obs.sem_obs]
s [in Obs.fan]
s [in Obs.anticlique]
SemEquiv [in Obs.notations]
shuffle [in Obs.list_tools]
Abbreviation Index
A
axΩ [in Obs.anticlique]E
eq_fcliques [in Obs.coherence_graph]F
FAN [in Obs.fan]I
inf_fcliques [in Obs.coherence_graph]inf_fcliques [in Obs.coherence_graph]
inf_cliques [in Obs.coherence_graph]
inf_cliques [in Obs.coherence_graph]
N
nb [in Obs.list_dec]nb [in Obs.list_dec]
O
O [in Obs.equiv_obs]Obs [in Obs.equiv_obs]
Obs' [in Obs.equiv_obs]
P
prj1 [in Obs.list_tools]prj2 [in Obs.list_tools]
S
sgl [in Obs.coherence_graph]sgl [in Obs.coherence_graph]
V
V [in Obs.product]other
𝒜 [in Obs.product]𝖳 [in Obs.product]
Definition Index
A
atTop [in Obs.product]C
choose_clique [in Obs.sem_obs]cnf_to_dnf [in Obs.product]
cnf_support [in Obs.product]
Conj [in Obs.fan]
conj_interp [in Obs.product]
D
difference [in Obs.list_dec]disj_interp [in Obs.product]
dnf_to_cnf [in Obs.product]
dnf_support [in Obs.product]
E
empt [in Obs.coherence_graph]equal_list [in Obs.list_dec]
equivalent [in Obs.list_tools]
equivalentb [in Obs.list_dec]
eq𝒱 [in Obs.product]
F
fcic [in Obs.coherence_graph]fcliques [in Obs.coherence_graph]
fcmem [in Obs.coherence_graph]
fc_to_clique [in Obs.coherence_graph]
fincompatible [in Obs.coherence_graph]
finsat [in Obs.fan]
fjoins [in Obs.coherence_graph]
flip [in Obs.list_tools]
I
impl_lst [in Obs.fin_sem_obs]inb [in Obs.list_dec]
inclb [in Obs.list_dec]
incoh [in Obs.coherence_graph]
incompatible [in Obs.coherence_graph]
incompat_project [in Obs.product]
incompat_inject [in Obs.product]
inf_obs [in Obs.equiv_obs]
inf__Ω [in Obs.anticlique]
inject [in Obs.product]
insert [in Obs.list_tools]
intersect [in Obs.list_dec]
is_coherent [in Obs.coherence_graph]
J
Join [in Obs.syntax_obs]joins [in Obs.coherence_graph]
join__f [in Obs.fan]
L
lift_prod [in Obs.list_tools]lists_of_length [in Obs.list_tools]
M
mapNF [in Obs.product]Meet [in Obs.syntax_obs]
mix [in Obs.list_tools]
N
NF [in Obs.product]nf [in Obs.fan]
NoDupb [in Obs.list_dec]
normal_form [in Obs.product]
O
Obs__Ω [in Obs.anticlique]obs𝖦_to_𝒯 [in Obs.product]
P
pad [in Obs.list_tools]pairs [in Obs.list_tools]
project [in Obs.coherence_graph]
project [in Obs.product]
project_list [in Obs.coherence_graph]
R
rm [in Obs.list_dec]rmfst [in Obs.list_dec]
S
sequiv [in Obs.notations]sgl__f [in Obs.coherence_graph]
shuffles [in Obs.list_tools]
ssmaller [in Obs.notations]
subsets [in Obs.list_tools]
sum [in Obs.list_tools]
sup [in Obs.product]
support [in Obs.fin_sem_obs]
T
termVect [in Obs.product]test [in Obs.decidable_prop]
to_Obs__Ω [in Obs.anticlique]
U
undup [in Obs.list_dec]Unnamed_thm [in Obs.decidable_prop]
V
V' [in Obs.anticlique]other
ζ [in Obs.anticlique]ξ [in Obs.anticlique]
π [in Obs.syntax_obs]
τ [in Obs.anticlique]
𝒯 [in Obs.product]
Record Index
C
clique [in Obs.coherence_graph]D
DecidableGraph [in Obs.coherence_graph]DecidableProp [in Obs.decidable_prop]
decidable_set [in Obs.decidable_prop]
F
FanGraph [in Obs.fan]G
Graph [in Obs.coherence_graph]S
Satisfaction [in Obs.notations]Size [in Obs.notations]
| 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 | (2452 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 | (81 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 | (1680 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (13 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 | (366 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 | (41 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 | (18 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 | (14 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 | (115 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) |
| 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 | (19 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 | (76 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 | (8 entries) |
This page has been generated by coqdoc