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

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

(28 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

(12 entries)

---

Global Index

A

acquintance_1 [lemma, in AMM11262.ascii_format.example1]
acquintance_2 [lemma, in AMM11262.ascii_format.example2]
acquintance_1 [lemma, in AMM11262.unicode_format.utf_example1]
acquintance_2 [lemma, in AMM11262.unicode_format.utf_example2]
AMM11262 [lemma, in AMM11262.unicode_format.utf_AMM11262]
AMM11262 [lemma, in AMM11262.ascii_format.AMM11262]
AMM11262 [library]

E

example_three_inhabitants [section, in AMM11262.ascii_format.example1]
example_five_inhabitants [section, in AMM11262.ascii_format.example2]
_ ℛ₁ _ [notation, in AMM11262.unicode_format.utf_example1]
example_three_inhabitants [section, in AMM11262.unicode_format.utf_example1]
_ ℛ₂ _ [notation, in AMM11262.unicode_format.utf_example2]
example_five_inhabitants [section, in AMM11262.unicode_format.utf_example2]
example1 [library]
example2 [library]
extendible_to_n [lemma, in AMM11262.unicode_format.utf_AMM11262]
extendible_by_one [lemma, in AMM11262.unicode_format.utf_AMM11262]
extendible_to_n [lemma, in AMM11262.ascii_format.AMM11262]
extendible_by_one [lemma, in AMM11262.ascii_format.AMM11262]

F

familiarity_1_extensional [lemma, in AMM11262.ascii_format.example1]
familiarity_1_sym [lemma, in AMM11262.ascii_format.example1]
familiarity_1 [definition, in AMM11262.ascii_format.example1]
familiarity_2_extensional [lemma, in AMM11262.ascii_format.example2]
familiarity_2_sym [lemma, in AMM11262.ascii_format.example2]
familiarity_2 [definition, in AMM11262.ascii_format.example2]
familiarity₁ [definition, in AMM11262.unicode_format.utf_example1]
familiarity₁_extensional [lemma, in AMM11262.unicode_format.utf_example1]
familiarity₁_sym [lemma, in AMM11262.unicode_format.utf_example1]
familiarity₂ [definition, in AMM11262.unicode_format.utf_example2]
familiarity₂_extensional [lemma, in AMM11262.unicode_format.utf_example2]
familiarity₂_sym [lemma, in AMM11262.unicode_format.utf_example2]

G

GeneralProperties [module, in AMM11262.unicode_format.utf_AMM11262]
GeneralProperties [module, in AMM11262.ascii_format.AMM11262]

I

inductive_invariant [lemma, in AMM11262.unicode_format.utf_AMM11262]
inductive_invariant [lemma, in AMM11262.ascii_format.AMM11262]

N

NatSet [module, in AMM11262.unicode_format.utf_AMM11262]
NatSet [module, in AMM11262.ascii_format.AMM11262]

P

population_1 [lemma, in AMM11262.ascii_format.example1]
population_2 [lemma, in AMM11262.ascii_format.example2]
population₁ [lemma, in AMM11262.unicode_format.utf_example1]
population₂ [lemma, in AMM11262.unicode_format.utf_example2]
problem_knows_not_refl.property [variable, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.knows_extensional [variable, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.knows_sym [variable, in AMM11262.unicode_format.utf_AMM11262]
_ ℛ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.knows [variable, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.cardinality [variable, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.n [variable, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.town [variable, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl [section, in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.property [variable, in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.knows_extensional [variable, in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.knows_sym [variable, in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.knows [variable, in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.cardinality [variable, in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.n [variable, in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.town [variable, in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl [section, in AMM11262.ascii_format.AMM11262]

S

social_citizen_1 [definition, in AMM11262.ascii_format.example1]
social_citizen_2 [definition, in AMM11262.ascii_format.example2]
social_citizen_1 [definition, in AMM11262.unicode_format.utf_example1]
social_citizen_2 [definition, in AMM11262.unicode_format.utf_example2]
subsets_1 [lemma, in AMM11262.ascii_format.example1]
subsets_2 [lemma, in AMM11262.ascii_format.example2]
subsets_1 [lemma, in AMM11262.unicode_format.utf_example1]
subsets_2 [lemma, in AMM11262.unicode_format.utf_example2]

T

town_1 [definition, in AMM11262.ascii_format.example1]
town_2 [definition, in AMM11262.ascii_format.example2]
town_1 [definition, in AMM11262.unicode_format.utf_example1]
town_2 [definition, in AMM11262.unicode_format.utf_example2]

U

utf_AMM11262 [library]
utf_example1 [library]
utf_example2 [library]

other

_ ≤ _ (nat_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
ℕ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
_ × _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
∃ _ , _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
_ \/ _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ∨ _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ∧ _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
¬ _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
∀ _ _ _ , _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
∀ _ _ , _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
∀ _ , _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ⇒ _ (type_scope) [notation, in AMM11262.unicode_format.utf_AMM11262]
_ \ { _ } [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ∪ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ∩ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ≡ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
_ \ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ⊆ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ∈ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
_ ≐ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
_ [=] _ [notation, in AMM11262.ascii_format.AMM11262]
_ ++ _ [notation, in AMM11262.ascii_format.AMM11262]
{ _ } ∪ _ [notation, in AMM11262.unicode_format.utf_AMM11262]
| _ | [notation, in AMM11262.unicode_format.utf_AMM11262]
∅ [notation, in AMM11262.unicode_format.utf_AMM11262]

---

Notation Index

E

_ ℛ₁ _ [in AMM11262.unicode_format.utf_example1]
_ ℛ₂ _ [in AMM11262.unicode_format.utf_example2]

P

_ ℛ _ [in AMM11262.unicode_format.utf_AMM11262]

other

_ ≤ _ (nat_scope) [in AMM11262.unicode_format.utf_AMM11262]
ℕ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
_ × _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
∃ _ , _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
_ \/ _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
_ ∨ _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
_ ∧ _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
¬ _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
∀ _ _ _ , _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
∀ _ _ , _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
∀ _ , _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
_ ⇒ _ (type_scope) [in AMM11262.unicode_format.utf_AMM11262]
_ \ { _ } [in AMM11262.unicode_format.utf_AMM11262]
_ ∪ _ [in AMM11262.unicode_format.utf_AMM11262]
_ ∩ _ [in AMM11262.unicode_format.utf_AMM11262]
_ ≡ _ [in AMM11262.unicode_format.utf_AMM11262]
_ \ _ [in AMM11262.unicode_format.utf_AMM11262]
_ ⊆ _ [in AMM11262.unicode_format.utf_AMM11262]
_ ∈ _ [in AMM11262.unicode_format.utf_AMM11262]
_ ≐ _ [in AMM11262.unicode_format.utf_AMM11262]
_ [=] _ [in AMM11262.ascii_format.AMM11262]
_ ++ _ [in AMM11262.ascii_format.AMM11262]
{ _ } ∪ _ [in AMM11262.unicode_format.utf_AMM11262]
| _ | [in AMM11262.unicode_format.utf_AMM11262]
∅ [in AMM11262.unicode_format.utf_AMM11262]

---

Module Index

G

GeneralProperties [in AMM11262.unicode_format.utf_AMM11262]
GeneralProperties [in AMM11262.ascii_format.AMM11262]

N

NatSet [in AMM11262.unicode_format.utf_AMM11262]
NatSet [in AMM11262.ascii_format.AMM11262]

---

Variable Index

P

problem_knows_not_refl.property [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.knows_extensional [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.knows_sym [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.knows [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.cardinality [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.n [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.town [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl.property [in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.knows_extensional [in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.knows_sym [in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.knows [in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.cardinality [in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.n [in AMM11262.ascii_format.AMM11262]
problem_knows_not_refl.town [in AMM11262.ascii_format.AMM11262]

---

Library Index

A

AMM11262

E

example1
example2

U

utf_AMM11262
utf_example1
utf_example2

---

Lemma Index

A

acquintance_1 [in AMM11262.ascii_format.example1]
acquintance_2 [in AMM11262.ascii_format.example2]
acquintance_1 [in AMM11262.unicode_format.utf_example1]
acquintance_2 [in AMM11262.unicode_format.utf_example2]
AMM11262 [in AMM11262.unicode_format.utf_AMM11262]
AMM11262 [in AMM11262.ascii_format.AMM11262]

E

extendible_to_n [in AMM11262.unicode_format.utf_AMM11262]
extendible_by_one [in AMM11262.unicode_format.utf_AMM11262]
extendible_to_n [in AMM11262.ascii_format.AMM11262]
extendible_by_one [in AMM11262.ascii_format.AMM11262]

F

familiarity_1_extensional [in AMM11262.ascii_format.example1]
familiarity_1_sym [in AMM11262.ascii_format.example1]
familiarity_2_extensional [in AMM11262.ascii_format.example2]
familiarity_2_sym [in AMM11262.ascii_format.example2]
familiarity₁_extensional [in AMM11262.unicode_format.utf_example1]
familiarity₁_sym [in AMM11262.unicode_format.utf_example1]
familiarity₂_extensional [in AMM11262.unicode_format.utf_example2]
familiarity₂_sym [in AMM11262.unicode_format.utf_example2]

I

inductive_invariant [in AMM11262.unicode_format.utf_AMM11262]
inductive_invariant [in AMM11262.ascii_format.AMM11262]

P

population_1 [in AMM11262.ascii_format.example1]
population_2 [in AMM11262.ascii_format.example2]
population₁ [in AMM11262.unicode_format.utf_example1]
population₂ [in AMM11262.unicode_format.utf_example2]

S

subsets_1 [in AMM11262.ascii_format.example1]
subsets_2 [in AMM11262.ascii_format.example2]
subsets_1 [in AMM11262.unicode_format.utf_example1]
subsets_2 [in AMM11262.unicode_format.utf_example2]

---

Section Index

E

example_three_inhabitants [in AMM11262.ascii_format.example1]
example_five_inhabitants [in AMM11262.ascii_format.example2]
example_three_inhabitants [in AMM11262.unicode_format.utf_example1]
example_five_inhabitants [in AMM11262.unicode_format.utf_example2]

P

problem_knows_not_refl [in AMM11262.unicode_format.utf_AMM11262]
problem_knows_not_refl [in AMM11262.ascii_format.AMM11262]

---

Definition Index

F

familiarity_1 [in AMM11262.ascii_format.example1]
familiarity_2 [in AMM11262.ascii_format.example2]
familiarity₁ [in AMM11262.unicode_format.utf_example1]
familiarity₂ [in AMM11262.unicode_format.utf_example2]

S

social_citizen_1 [in AMM11262.ascii_format.example1]
social_citizen_2 [in AMM11262.ascii_format.example2]
social_citizen_1 [in AMM11262.unicode_format.utf_example1]
social_citizen_2 [in AMM11262.unicode_format.utf_example2]

T

town_1 [in AMM11262.ascii_format.example1]
town_2 [in AMM11262.ascii_format.example2]
town_1 [in AMM11262.unicode_format.utf_example1]
town_2 [in AMM11262.unicode_format.utf_example2]

---

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

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

(28 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

(12 entries)