| 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 | (385 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 | (6 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 | (264 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 | (24 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 | (1 entry) |
| 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 | (36 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 | (21 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 | (3 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 | (2 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 | (5 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 | (20 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 | (3 entries) |
Global Index
A
Abstract [section, in baf.backandforth]Abstract.find [variable, in baf.backandforth]
Abstract.find_iso [variable, in baf.backandforth]
Abstract.iso [variable, in baf.backandforth]
Abstract.iso_rev [variable, in baf.backandforth]
Abstract.iso_eq [variable, in baf.backandforth]
Abstract.RX [variable, in baf.backandforth]
Abstract.RY [variable, in baf.backandforth]
Abstract.srev [variable, in baf.backandforth]
Abstract.srev_invol [variable, in baf.backandforth]
Abstract.structure [variable, in baf.backandforth]
Abstract.SXY [variable, in baf.backandforth]
Abstract.X [variable, in baf.backandforth]
Abstract.Y [variable, in baf.backandforth]
a':211 [binder, in baf.backandforth]
a':219 [binder, in baf.backandforth]
a:194 [binder, in baf.backandforth]
a:199 [binder, in baf.backandforth]
a:204 [binder, in baf.backandforth]
a:209 [binder, in baf.backandforth]
a:217 [binder, in baf.backandforth]
a:22 [binder, in baf.backandforth]
a:224 [binder, in baf.backandforth]
a:227 [binder, in baf.backandforth]
a:229 [binder, in baf.backandforth]
a:233 [binder, in baf.backandforth]
a:27 [binder, in baf.backandforth]
a:33 [binder, in baf.backandforth]
a:40 [binder, in baf.backandforth]
a:46 [binder, in baf.backandforth]
B
Back [definition, in baf.backandforth]backandforth [library]
back_and_forth [lemma, in baf.backandforth]
back_forth [lemma, in baf.backandforth]
bireduction [record, in baf.backandforth]
b:196 [binder, in baf.backandforth]
b:200 [binder, in baf.backandforth]
b:205 [binder, in baf.backandforth]
b:23 [binder, in baf.backandforth]
b:235 [binder, in baf.backandforth]
b:28 [binder, in baf.backandforth]
b:41 [binder, in baf.backandforth]
C
Cantor [lemma, in baf.backandforth]CantorStep [section, in baf.backandforth]
CantorStep.A [variable, in baf.backandforth]
CantorStep.B [variable, in baf.backandforth]
_ <B _ [notation, in baf.backandforth]
_ <A _ [notation, in baf.backandforth]
Cantor_Bernstein [lemma, in baf.backandforth]
correspondence [definition, in baf.backandforth]
correspondence_remove [lemma, in baf.backandforth]
countable_discrete [instance, in baf.backandforth]
c:195 [binder, in baf.backandforth]
c:201 [binder, in baf.backandforth]
c:206 [binder, in baf.backandforth]
c:212 [binder, in baf.backandforth]
c:214 [binder, in baf.backandforth]
c:220 [binder, in baf.backandforth]
c:222 [binder, in baf.backandforth]
c:234 [binder, in baf.backandforth]
C:287 [binder, in baf.backandforth]
C:313 [binder, in baf.backandforth]
C:314 [binder, in baf.backandforth]
C:319 [binder, in baf.backandforth]
C:322 [binder, in baf.backandforth]
C:324 [binder, in baf.backandforth]
D
discrete [definition, in baf.backandforth]discrete_prod [lemma, in baf.backandforth]
discrete_indec [lemma, in baf.backandforth]
dom [abbreviation, in baf.backandforth]
dom_el [lemma, in baf.backandforth]
double_flip [lemma, in baf.backandforth]
dulo [record, in baf.backandforth]
dulo_disc [lemma, in baf.backandforth]
d:197 [binder, in baf.backandforth]
d:202 [binder, in baf.backandforth]
d:207 [binder, in baf.backandforth]
d:213 [binder, in baf.backandforth]
d:215 [binder, in baf.backandforth]
d:221 [binder, in baf.backandforth]
d:223 [binder, in baf.backandforth]
d:236 [binder, in baf.backandforth]
E
eX [projection, in baf.backandforth]eY [projection, in baf.backandforth]
F
f [projection, in baf.backandforth]flip [abbreviation, in baf.backandforth]
flip_tiso [lemma, in baf.backandforth]
flip_el [lemma, in baf.backandforth]
Forth [definition, in baf.backandforth]
forth_back [lemma, in baf.backandforth]
forth_iso [lemma, in baf.backandforth]
f_red [projection, in baf.backandforth]
f_inj [projection, in baf.backandforth]
f':110 [binder, in baf.backandforth]
f:105 [binder, in baf.backandforth]
f:109 [binder, in baf.backandforth]
f:115 [binder, in baf.backandforth]
f:120 [binder, in baf.backandforth]
F:148 [binder, in baf.backandforth]
F:152 [binder, in baf.backandforth]
f:193 [binder, in baf.backandforth]
f:198 [binder, in baf.backandforth]
f:203 [binder, in baf.backandforth]
f:208 [binder, in baf.backandforth]
f:21 [binder, in baf.backandforth]
f:216 [binder, in baf.backandforth]
f:225 [binder, in baf.backandforth]
f:226 [binder, in baf.backandforth]
f:228 [binder, in baf.backandforth]
f:230 [binder, in baf.backandforth]
f:232 [binder, in baf.backandforth]
f:237 [binder, in baf.backandforth]
f:238 [binder, in baf.backandforth]
F:246 [binder, in baf.backandforth]
f:252 [binder, in baf.backandforth]
f:259 [binder, in baf.backandforth]
f:26 [binder, in baf.backandforth]
f:32 [binder, in baf.backandforth]
F:331 [binder, in baf.backandforth]
f:337 [binder, in baf.backandforth]
F:339 [binder, in baf.backandforth]
f:39 [binder, in baf.backandforth]
f:45 [binder, in baf.backandforth]
f:50 [binder, in baf.backandforth]
f:55 [binder, in baf.backandforth]
f:86 [binder, in baf.backandforth]
f:97 [binder, in baf.backandforth]
G
g [projection, in baf.backandforth]gamma [definition, in baf.backandforth]
gamma_spec [lemma, in baf.backandforth]
g_red [projection, in baf.backandforth]
g_inj [projection, in baf.backandforth]
G:149 [binder, in baf.backandforth]
G:153 [binder, in baf.backandforth]
G:247 [binder, in baf.backandforth]
G:332 [binder, in baf.backandforth]
g:338 [binder, in baf.backandforth]
G:340 [binder, in baf.backandforth]
H
HIR [projection, in baf.backandforth]I
I [projection, in baf.backandforth]im [definition, in baf.backandforth]
im_none [lemma, in baf.backandforth]
im_some [lemma, in baf.backandforth]
incl_tiso [lemma, in baf.backandforth]
inj [definition, in baf.backandforth]
inverse [definition, in baf.backandforth]
K
k:137 [binder, in baf.backandforth]L
L [definition, in baf.backandforth]L_iso [lemma, in baf.backandforth]
L_cum [lemma, in baf.backandforth]
L_sur [lemma, in baf.backandforth]
L_tot [lemma, in baf.backandforth]
L_tiso [lemma, in baf.backandforth]
L:16 [binder, in baf.backandforth]
L:284 [binder, in baf.backandforth]
M
matches [definition, in baf.backandforth]matches_down [lemma, in baf.backandforth]
max_im [definition, in baf.backandforth]
max:218 [binder, in baf.backandforth]
min_im [definition, in baf.backandforth]
min:210 [binder, in baf.backandforth]
morph [definition, in baf.backandforth]
morph_morph' [lemma, in baf.backandforth]
morph' [definition, in baf.backandforth]
mstep [definition, in baf.backandforth]
Myhill [lemma, in baf.backandforth]
MyhillStep [section, in baf.backandforth]
MyhillStep.eX [variable, in baf.backandforth]
MyhillStep.eY [variable, in baf.backandforth]
MyhillStep.f [variable, in baf.backandforth]
MyhillStep.f_red [variable, in baf.backandforth]
MyhillStep.inj_f [variable, in baf.backandforth]
MyhillStep.p [variable, in baf.backandforth]
MyhillStep.q [variable, in baf.backandforth]
MyhillStep.X [variable, in baf.backandforth]
MyhillStep.Y [variable, in baf.backandforth]
N
n':141 [binder, in baf.backandforth]n:116 [binder, in baf.backandforth]
n:126 [binder, in baf.backandforth]
n:129 [binder, in baf.backandforth]
n:136 [binder, in baf.backandforth]
n:138 [binder, in baf.backandforth]
O
OA:191 [binder, in baf.backandforth]OB:192 [binder, in baf.backandforth]
OX:180 [binder, in baf.backandforth]
OX:184 [binder, in baf.backandforth]
OX:188 [binder, in baf.backandforth]
OX:242 [binder, in baf.backandforth]
OY:243 [binder, in baf.backandforth]
P
p [projection, in baf.backandforth]partner [definition, in baf.backandforth]
partner_matches [lemma, in baf.backandforth]
partner_ran [lemma, in baf.backandforth]
pi1 [abbreviation, in baf.backandforth]
pi2 [abbreviation, in baf.backandforth]
point [projection, in baf.backandforth]
p:257 [binder, in baf.backandforth]
p:47 [binder, in baf.backandforth]
Q
q [projection, in baf.backandforth]q:258 [binder, in baf.backandforth]
R
R [projection, in baf.backandforth]ran [abbreviation, in baf.backandforth]
ran_compute [lemma, in baf.backandforth]
ran_el [lemma, in baf.backandforth]
reduction [definition, in baf.backandforth]
rel [projection, in baf.backandforth]
rel_dec [lemma, in baf.backandforth]
rel_asym [lemma, in baf.backandforth]
rel_dense [projection, in baf.backandforth]
rel_down [projection, in baf.backandforth]
rel_up [projection, in baf.backandforth]
rel_trich [projection, in baf.backandforth]
rel_trans [projection, in baf.backandforth]
rel_irref [projection, in baf.backandforth]
retract [record, in baf.backandforth]
retract_discrete [instance, in baf.backandforth]
RX:102 [binder, in baf.backandforth]
RX:113 [binder, in baf.backandforth]
RX:244 [binder, in baf.backandforth]
RX:329 [binder, in baf.backandforth]
RX:335 [binder, in baf.backandforth]
RY:245 [binder, in baf.backandforth]
RY:330 [binder, in baf.backandforth]
RY:336 [binder, in baf.backandforth]
S
step [definition, in baf.backandforth]step_corr [lemma, in baf.backandforth]
step_morph [lemma, in baf.backandforth]
step_morph' [lemma, in baf.backandforth]
step_tiso [lemma, in baf.backandforth]
SXY:328 [binder, in baf.backandforth]
S:103 [binder, in baf.backandforth]
S:108 [binder, in baf.backandforth]
S:114 [binder, in baf.backandforth]
S:119 [binder, in baf.backandforth]
S:62 [binder, in baf.backandforth]
S:69 [binder, in baf.backandforth]
S:77 [binder, in baf.backandforth]
S:85 [binder, in baf.backandforth]
S:96 [binder, in baf.backandforth]
T
table [definition, in baf.backandforth]tiso [definition, in baf.backandforth]
X
X_dec:44 [binder, in baf.backandforth]X_dec:38 [binder, in baf.backandforth]
X_dec:31 [binder, in baf.backandforth]
x':142 [binder, in baf.backandforth]
x':145 [binder, in baf.backandforth]
x':155 [binder, in baf.backandforth]
x':249 [binder, in baf.backandforth]
x':254 [binder, in baf.backandforth]
x':316 [binder, in baf.backandforth]
x':71 [binder, in baf.backandforth]
x':79 [binder, in baf.backandforth]
x':88 [binder, in baf.backandforth]
X:1 [binder, in baf.backandforth]
X:100 [binder, in baf.backandforth]
x:104 [binder, in baf.backandforth]
X:106 [binder, in baf.backandforth]
X:11 [binder, in baf.backandforth]
X:111 [binder, in baf.backandforth]
X:117 [binder, in baf.backandforth]
X:13 [binder, in baf.backandforth]
x:130 [binder, in baf.backandforth]
x:133 [binder, in baf.backandforth]
x:134 [binder, in baf.backandforth]
x:139 [binder, in baf.backandforth]
X:14 [binder, in baf.backandforth]
x:144 [binder, in baf.backandforth]
x:146 [binder, in baf.backandforth]
x:15 [binder, in baf.backandforth]
x:150 [binder, in baf.backandforth]
x:154 [binder, in baf.backandforth]
X:156 [binder, in baf.backandforth]
x:160 [binder, in baf.backandforth]
x:162 [binder, in baf.backandforth]
x:166 [binder, in baf.backandforth]
x:169 [binder, in baf.backandforth]
X:17 [binder, in baf.backandforth]
x:172 [binder, in baf.backandforth]
x:175 [binder, in baf.backandforth]
X:179 [binder, in baf.backandforth]
x:181 [binder, in baf.backandforth]
X:183 [binder, in baf.backandforth]
x:185 [binder, in baf.backandforth]
X:187 [binder, in baf.backandforth]
X:19 [binder, in baf.backandforth]
x:231 [binder, in baf.backandforth]
x:239 [binder, in baf.backandforth]
X:24 [binder, in baf.backandforth]
X:240 [binder, in baf.backandforth]
x:248 [binder, in baf.backandforth]
X:250 [binder, in baf.backandforth]
x:253 [binder, in baf.backandforth]
X:255 [binder, in baf.backandforth]
x:260 [binder, in baf.backandforth]
X:261 [binder, in baf.backandforth]
x:285 [binder, in baf.backandforth]
x:286 [binder, in baf.backandforth]
X:29 [binder, in baf.backandforth]
x:312 [binder, in baf.backandforth]
x:315 [binder, in baf.backandforth]
x:320 [binder, in baf.backandforth]
x:323 [binder, in baf.backandforth]
x:325 [binder, in baf.backandforth]
X:326 [binder, in baf.backandforth]
X:333 [binder, in baf.backandforth]
X:36 [binder, in baf.backandforth]
X:42 [binder, in baf.backandforth]
X:48 [binder, in baf.backandforth]
x:51 [binder, in baf.backandforth]
X:53 [binder, in baf.backandforth]
X:57 [binder, in baf.backandforth]
x:6 [binder, in baf.backandforth]
X:60 [binder, in baf.backandforth]
X:64 [binder, in baf.backandforth]
X:67 [binder, in baf.backandforth]
x:70 [binder, in baf.backandforth]
X:75 [binder, in baf.backandforth]
x:78 [binder, in baf.backandforth]
X:8 [binder, in baf.backandforth]
X:83 [binder, in baf.backandforth]
x:87 [binder, in baf.backandforth]
x:9 [binder, in baf.backandforth]
X:91 [binder, in baf.backandforth]
X:94 [binder, in baf.backandforth]
x:98 [binder, in baf.backandforth]
Y
y':143 [binder, in baf.backandforth]y':318 [binder, in baf.backandforth]
y':73 [binder, in baf.backandforth]
y':81 [binder, in baf.backandforth]
y':90 [binder, in baf.backandforth]
y:10 [binder, in baf.backandforth]
Y:101 [binder, in baf.backandforth]
Y:107 [binder, in baf.backandforth]
Y:112 [binder, in baf.backandforth]
Y:118 [binder, in baf.backandforth]
Y:12 [binder, in baf.backandforth]
y:131 [binder, in baf.backandforth]
y:132 [binder, in baf.backandforth]
y:135 [binder, in baf.backandforth]
y:140 [binder, in baf.backandforth]
y:147 [binder, in baf.backandforth]
y:151 [binder, in baf.backandforth]
y:163 [binder, in baf.backandforth]
y:167 [binder, in baf.backandforth]
y:170 [binder, in baf.backandforth]
y:173 [binder, in baf.backandforth]
y:176 [binder, in baf.backandforth]
Y:18 [binder, in baf.backandforth]
y:182 [binder, in baf.backandforth]
y:186 [binder, in baf.backandforth]
Y:2 [binder, in baf.backandforth]
Y:20 [binder, in baf.backandforth]
Y:241 [binder, in baf.backandforth]
Y:25 [binder, in baf.backandforth]
Y:251 [binder, in baf.backandforth]
Y:256 [binder, in baf.backandforth]
Y:262 [binder, in baf.backandforth]
y:283 [binder, in baf.backandforth]
Y:30 [binder, in baf.backandforth]
y:317 [binder, in baf.backandforth]
y:321 [binder, in baf.backandforth]
Y:327 [binder, in baf.backandforth]
Y:334 [binder, in baf.backandforth]
Y:37 [binder, in baf.backandforth]
Y:43 [binder, in baf.backandforth]
Y:49 [binder, in baf.backandforth]
y:52 [binder, in baf.backandforth]
Y:54 [binder, in baf.backandforth]
Y:58 [binder, in baf.backandforth]
Y:61 [binder, in baf.backandforth]
Y:65 [binder, in baf.backandforth]
Y:68 [binder, in baf.backandforth]
y:72 [binder, in baf.backandforth]
Y:76 [binder, in baf.backandforth]
y:80 [binder, in baf.backandforth]
Y:84 [binder, in baf.backandforth]
y:89 [binder, in baf.backandforth]
Y:92 [binder, in baf.backandforth]
Y:95 [binder, in baf.backandforth]
Z
z:164 [binder, in baf.backandforth]z:177 [binder, in baf.backandforth]
other
_ < _ [notation, in baf.backandforth]_ <<= _ [notation, in baf.backandforth]
_ nel _ [notation, in baf.backandforth]
_ el _ [notation, in baf.backandforth]
Notation Index
C
_ <B _ [in baf.backandforth]_ <A _ [in baf.backandforth]
other
_ < _ [in baf.backandforth]_ <<= _ [in baf.backandforth]
_ nel _ [in baf.backandforth]
_ el _ [in baf.backandforth]
Binder Index
A
a':211 [in baf.backandforth]a':219 [in baf.backandforth]
a:194 [in baf.backandforth]
a:199 [in baf.backandforth]
a:204 [in baf.backandforth]
a:209 [in baf.backandforth]
a:217 [in baf.backandforth]
a:22 [in baf.backandforth]
a:224 [in baf.backandforth]
a:227 [in baf.backandforth]
a:229 [in baf.backandforth]
a:233 [in baf.backandforth]
a:27 [in baf.backandforth]
a:33 [in baf.backandforth]
a:40 [in baf.backandforth]
a:46 [in baf.backandforth]
B
b:196 [in baf.backandforth]b:200 [in baf.backandforth]
b:205 [in baf.backandforth]
b:23 [in baf.backandforth]
b:235 [in baf.backandforth]
b:28 [in baf.backandforth]
b:41 [in baf.backandforth]
C
c:195 [in baf.backandforth]c:201 [in baf.backandforth]
c:206 [in baf.backandforth]
c:212 [in baf.backandforth]
c:214 [in baf.backandforth]
c:220 [in baf.backandforth]
c:222 [in baf.backandforth]
c:234 [in baf.backandforth]
C:287 [in baf.backandforth]
C:313 [in baf.backandforth]
C:314 [in baf.backandforth]
C:319 [in baf.backandforth]
C:322 [in baf.backandforth]
C:324 [in baf.backandforth]
D
d:197 [in baf.backandforth]d:202 [in baf.backandforth]
d:207 [in baf.backandforth]
d:213 [in baf.backandforth]
d:215 [in baf.backandforth]
d:221 [in baf.backandforth]
d:223 [in baf.backandforth]
d:236 [in baf.backandforth]
F
f':110 [in baf.backandforth]f:105 [in baf.backandforth]
f:109 [in baf.backandforth]
f:115 [in baf.backandforth]
f:120 [in baf.backandforth]
F:148 [in baf.backandforth]
F:152 [in baf.backandforth]
f:193 [in baf.backandforth]
f:198 [in baf.backandforth]
f:203 [in baf.backandforth]
f:208 [in baf.backandforth]
f:21 [in baf.backandforth]
f:216 [in baf.backandforth]
f:225 [in baf.backandforth]
f:226 [in baf.backandforth]
f:228 [in baf.backandforth]
f:230 [in baf.backandforth]
f:232 [in baf.backandforth]
f:237 [in baf.backandforth]
f:238 [in baf.backandforth]
F:246 [in baf.backandforth]
f:252 [in baf.backandforth]
f:259 [in baf.backandforth]
f:26 [in baf.backandforth]
f:32 [in baf.backandforth]
F:331 [in baf.backandforth]
f:337 [in baf.backandforth]
F:339 [in baf.backandforth]
f:39 [in baf.backandforth]
f:45 [in baf.backandforth]
f:50 [in baf.backandforth]
f:55 [in baf.backandforth]
f:86 [in baf.backandforth]
f:97 [in baf.backandforth]
G
G:149 [in baf.backandforth]G:153 [in baf.backandforth]
G:247 [in baf.backandforth]
G:332 [in baf.backandforth]
g:338 [in baf.backandforth]
G:340 [in baf.backandforth]
K
k:137 [in baf.backandforth]L
L:16 [in baf.backandforth]L:284 [in baf.backandforth]
M
max:218 [in baf.backandforth]min:210 [in baf.backandforth]
N
n':141 [in baf.backandforth]n:116 [in baf.backandforth]
n:126 [in baf.backandforth]
n:129 [in baf.backandforth]
n:136 [in baf.backandforth]
n:138 [in baf.backandforth]
O
OA:191 [in baf.backandforth]OB:192 [in baf.backandforth]
OX:180 [in baf.backandforth]
OX:184 [in baf.backandforth]
OX:188 [in baf.backandforth]
OX:242 [in baf.backandforth]
OY:243 [in baf.backandforth]
P
p:257 [in baf.backandforth]p:47 [in baf.backandforth]
Q
q:258 [in baf.backandforth]R
RX:102 [in baf.backandforth]RX:113 [in baf.backandforth]
RX:244 [in baf.backandforth]
RX:329 [in baf.backandforth]
RX:335 [in baf.backandforth]
RY:245 [in baf.backandforth]
RY:330 [in baf.backandforth]
RY:336 [in baf.backandforth]
S
SXY:328 [in baf.backandforth]S:103 [in baf.backandforth]
S:108 [in baf.backandforth]
S:114 [in baf.backandforth]
S:119 [in baf.backandforth]
S:62 [in baf.backandforth]
S:69 [in baf.backandforth]
S:77 [in baf.backandforth]
S:85 [in baf.backandforth]
S:96 [in baf.backandforth]
X
X_dec:44 [in baf.backandforth]X_dec:38 [in baf.backandforth]
X_dec:31 [in baf.backandforth]
x':142 [in baf.backandforth]
x':145 [in baf.backandforth]
x':155 [in baf.backandforth]
x':249 [in baf.backandforth]
x':254 [in baf.backandforth]
x':316 [in baf.backandforth]
x':71 [in baf.backandforth]
x':79 [in baf.backandforth]
x':88 [in baf.backandforth]
X:1 [in baf.backandforth]
X:100 [in baf.backandforth]
x:104 [in baf.backandforth]
X:106 [in baf.backandforth]
X:11 [in baf.backandforth]
X:111 [in baf.backandforth]
X:117 [in baf.backandforth]
X:13 [in baf.backandforth]
x:130 [in baf.backandforth]
x:133 [in baf.backandforth]
x:134 [in baf.backandforth]
x:139 [in baf.backandforth]
X:14 [in baf.backandforth]
x:144 [in baf.backandforth]
x:146 [in baf.backandforth]
x:15 [in baf.backandforth]
x:150 [in baf.backandforth]
x:154 [in baf.backandforth]
X:156 [in baf.backandforth]
x:160 [in baf.backandforth]
x:162 [in baf.backandforth]
x:166 [in baf.backandforth]
x:169 [in baf.backandforth]
X:17 [in baf.backandforth]
x:172 [in baf.backandforth]
x:175 [in baf.backandforth]
X:179 [in baf.backandforth]
x:181 [in baf.backandforth]
X:183 [in baf.backandforth]
x:185 [in baf.backandforth]
X:187 [in baf.backandforth]
X:19 [in baf.backandforth]
x:231 [in baf.backandforth]
x:239 [in baf.backandforth]
X:24 [in baf.backandforth]
X:240 [in baf.backandforth]
x:248 [in baf.backandforth]
X:250 [in baf.backandforth]
x:253 [in baf.backandforth]
X:255 [in baf.backandforth]
x:260 [in baf.backandforth]
X:261 [in baf.backandforth]
x:285 [in baf.backandforth]
x:286 [in baf.backandforth]
X:29 [in baf.backandforth]
x:312 [in baf.backandforth]
x:315 [in baf.backandforth]
x:320 [in baf.backandforth]
x:323 [in baf.backandforth]
x:325 [in baf.backandforth]
X:326 [in baf.backandforth]
X:333 [in baf.backandforth]
X:36 [in baf.backandforth]
X:42 [in baf.backandforth]
X:48 [in baf.backandforth]
x:51 [in baf.backandforth]
X:53 [in baf.backandforth]
X:57 [in baf.backandforth]
x:6 [in baf.backandforth]
X:60 [in baf.backandforth]
X:64 [in baf.backandforth]
X:67 [in baf.backandforth]
x:70 [in baf.backandforth]
X:75 [in baf.backandforth]
x:78 [in baf.backandforth]
X:8 [in baf.backandforth]
X:83 [in baf.backandforth]
x:87 [in baf.backandforth]
x:9 [in baf.backandforth]
X:91 [in baf.backandforth]
X:94 [in baf.backandforth]
x:98 [in baf.backandforth]
Y
y':143 [in baf.backandforth]y':318 [in baf.backandforth]
y':73 [in baf.backandforth]
y':81 [in baf.backandforth]
y':90 [in baf.backandforth]
y:10 [in baf.backandforth]
Y:101 [in baf.backandforth]
Y:107 [in baf.backandforth]
Y:112 [in baf.backandforth]
Y:118 [in baf.backandforth]
Y:12 [in baf.backandforth]
y:131 [in baf.backandforth]
y:132 [in baf.backandforth]
y:135 [in baf.backandforth]
y:140 [in baf.backandforth]
y:147 [in baf.backandforth]
y:151 [in baf.backandforth]
y:163 [in baf.backandforth]
y:167 [in baf.backandforth]
y:170 [in baf.backandforth]
y:173 [in baf.backandforth]
y:176 [in baf.backandforth]
Y:18 [in baf.backandforth]
y:182 [in baf.backandforth]
y:186 [in baf.backandforth]
Y:2 [in baf.backandforth]
Y:20 [in baf.backandforth]
Y:241 [in baf.backandforth]
Y:25 [in baf.backandforth]
Y:251 [in baf.backandforth]
Y:256 [in baf.backandforth]
Y:262 [in baf.backandforth]
y:283 [in baf.backandforth]
Y:30 [in baf.backandforth]
y:317 [in baf.backandforth]
y:321 [in baf.backandforth]
Y:327 [in baf.backandforth]
Y:334 [in baf.backandforth]
Y:37 [in baf.backandforth]
Y:43 [in baf.backandforth]
Y:49 [in baf.backandforth]
y:52 [in baf.backandforth]
Y:54 [in baf.backandforth]
Y:58 [in baf.backandforth]
Y:61 [in baf.backandforth]
Y:65 [in baf.backandforth]
Y:68 [in baf.backandforth]
y:72 [in baf.backandforth]
Y:76 [in baf.backandforth]
y:80 [in baf.backandforth]
Y:84 [in baf.backandforth]
y:89 [in baf.backandforth]
Y:92 [in baf.backandforth]
Y:95 [in baf.backandforth]
Z
z:164 [in baf.backandforth]z:177 [in baf.backandforth]
Variable Index
A
Abstract.find [in baf.backandforth]Abstract.find_iso [in baf.backandforth]
Abstract.iso [in baf.backandforth]
Abstract.iso_rev [in baf.backandforth]
Abstract.iso_eq [in baf.backandforth]
Abstract.RX [in baf.backandforth]
Abstract.RY [in baf.backandforth]
Abstract.srev [in baf.backandforth]
Abstract.srev_invol [in baf.backandforth]
Abstract.structure [in baf.backandforth]
Abstract.SXY [in baf.backandforth]
Abstract.X [in baf.backandforth]
Abstract.Y [in baf.backandforth]
C
CantorStep.A [in baf.backandforth]CantorStep.B [in baf.backandforth]
M
MyhillStep.eX [in baf.backandforth]MyhillStep.eY [in baf.backandforth]
MyhillStep.f [in baf.backandforth]
MyhillStep.f_red [in baf.backandforth]
MyhillStep.inj_f [in baf.backandforth]
MyhillStep.p [in baf.backandforth]
MyhillStep.q [in baf.backandforth]
MyhillStep.X [in baf.backandforth]
MyhillStep.Y [in baf.backandforth]
Library Index
B
backandforthLemma Index
B
back_and_forth [in baf.backandforth]back_forth [in baf.backandforth]
C
Cantor [in baf.backandforth]Cantor_Bernstein [in baf.backandforth]
correspondence_remove [in baf.backandforth]
D
discrete_prod [in baf.backandforth]discrete_indec [in baf.backandforth]
dom_el [in baf.backandforth]
double_flip [in baf.backandforth]
dulo_disc [in baf.backandforth]
F
flip_tiso [in baf.backandforth]flip_el [in baf.backandforth]
forth_back [in baf.backandforth]
forth_iso [in baf.backandforth]
G
gamma_spec [in baf.backandforth]I
im_none [in baf.backandforth]im_some [in baf.backandforth]
incl_tiso [in baf.backandforth]
L
L_iso [in baf.backandforth]L_cum [in baf.backandforth]
L_sur [in baf.backandforth]
L_tot [in baf.backandforth]
L_tiso [in baf.backandforth]
M
matches_down [in baf.backandforth]morph_morph' [in baf.backandforth]
Myhill [in baf.backandforth]
P
partner_matches [in baf.backandforth]partner_ran [in baf.backandforth]
R
ran_compute [in baf.backandforth]ran_el [in baf.backandforth]
rel_dec [in baf.backandforth]
rel_asym [in baf.backandforth]
S
step_corr [in baf.backandforth]step_morph [in baf.backandforth]
step_morph' [in baf.backandforth]
step_tiso [in baf.backandforth]
Projection Index
E
eX [in baf.backandforth]eY [in baf.backandforth]
F
f [in baf.backandforth]f_red [in baf.backandforth]
f_inj [in baf.backandforth]
G
g [in baf.backandforth]g_red [in baf.backandforth]
g_inj [in baf.backandforth]
H
HIR [in baf.backandforth]I
I [in baf.backandforth]P
p [in baf.backandforth]point [in baf.backandforth]
Q
q [in baf.backandforth]R
R [in baf.backandforth]rel [in baf.backandforth]
rel_dense [in baf.backandforth]
rel_down [in baf.backandforth]
rel_up [in baf.backandforth]
rel_trich [in baf.backandforth]
rel_trans [in baf.backandforth]
rel_irref [in baf.backandforth]
Section Index
A
Abstract [in baf.backandforth]C
CantorStep [in baf.backandforth]M
MyhillStep [in baf.backandforth]Instance Index
C
countable_discrete [in baf.backandforth]R
retract_discrete [in baf.backandforth]Abbreviation Index
D
dom [in baf.backandforth]F
flip [in baf.backandforth]P
pi1 [in baf.backandforth]pi2 [in baf.backandforth]
R
ran [in baf.backandforth]Definition Index
B
Back [in baf.backandforth]C
correspondence [in baf.backandforth]D
discrete [in baf.backandforth]F
Forth [in baf.backandforth]G
gamma [in baf.backandforth]I
im [in baf.backandforth]inj [in baf.backandforth]
inverse [in baf.backandforth]
L
L [in baf.backandforth]M
matches [in baf.backandforth]max_im [in baf.backandforth]
min_im [in baf.backandforth]
morph [in baf.backandforth]
morph' [in baf.backandforth]
mstep [in baf.backandforth]
P
partner [in baf.backandforth]R
reduction [in baf.backandforth]S
step [in baf.backandforth]T
table [in baf.backandforth]tiso [in baf.backandforth]
Record Index
B
bireduction [in baf.backandforth]D
dulo [in baf.backandforth]R
retract [in baf.backandforth]| 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 | (385 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 | (6 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 | (264 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 | (24 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 | (1 entry) |
| 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 | (36 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 | (21 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 | (3 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 | (2 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 | (5 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 | (20 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 | (3 entries) |