Home | Intuitionistic Logic Explorer Theorem List (p. 120 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phimullem 11901* | Lemma for phimul 11902. (Contributed by Mario Carneiro, 24-Feb-2014.) |
..^ ..^ ..^ ..^ ..^ | ||
Theorem | phimul 11902 | The Euler function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.) |
Theorem | hashgcdlem 11903* | A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
..^ ..^ | ||
Theorem | hashgcdeq 11904* | Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
♯ ..^ | ||
Theorem | oddennn 11905 | There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.) |
Theorem | evenennn 11906 | There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.) |
Theorem | xpnnen 11907 | The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) |
Theorem | xpomen 11908 | The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.) |
Theorem | xpct 11909 | The cartesian product of two sets dominated by is dominated by . (Contributed by Thierry Arnoux, 24-Sep-2017.) |
Theorem | unennn 11910 | The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.) |
Theorem | znnen 11911 | The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.) |
Theorem | ennnfonelemdc 11912* | Lemma for ennnfone 11938. A direct consequence of fidcenumlemrk 6842. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID DECID | ||
Theorem | ennnfonelemk 11913* | Lemma for ennnfone 11938. (Contributed by Jim Kingdon, 15-Jul-2023.) |
Theorem | ennnfonelemj0 11914* | Lemma for ennnfone 11938. Initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemjn 11915* | Lemma for ennnfone 11938. Non-initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemg 11916* | Lemma for ennnfone 11938. Closure for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemh 11917* | Lemma for ennnfone 11938. (Contributed by Jim Kingdon, 8-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem0 11918* | Lemma for ennnfone 11938. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemp1 11919* | Lemma for ennnfone 11938. Value of at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem1 11920* | Lemma for ennnfone 11938. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemom 11921* | Lemma for ennnfone 11938. yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhdmp1 11922* | Lemma for ennnfone 11938. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemss 11923* | Lemma for ennnfone 11938. We only add elements to as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfoneleminc 11924* | Lemma for ennnfone 11938. We only add elements to as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemkh 11925* | Lemma for ennnfone 11938. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhf1o 11926* | Lemma for ennnfone 11938. Each of the functions in is one to one and onto an image of . (Contributed by Jim Kingdon, 17-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemex 11927* | Lemma for ennnfone 11938. Extending the sequence to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhom 11928* | Lemma for ennnfone 11938. The sequences in increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemrnh 11929* | Lemma for ennnfone 11938. A consequence of ennnfonelemss 11923. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemfun 11930* | Lemma for ennnfone 11938. is a function. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemf1 11931* | Lemma for ennnfone 11938. is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemrn 11932* | Lemma for ennnfone 11938. is onto . (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemdm 11933* | Lemma for ennnfone 11938. The function is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemen 11934* | Lemma for ennnfone 11938. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemnn0 11935* | Lemma for ennnfone 11938. A version of ennnfonelemen 11934 expressed in terms of instead of . (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID frec | ||
Theorem | ennnfonelemr 11936* | Lemma for ennnfone 11938. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfonelemim 11937* | Lemma for ennnfone 11938. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfone 11938* | A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that is countable (that's the part, as seen in theorems like ctm 6994), infinite (that's the part about being able to find an element of distinct from any mapping of a natural number via ), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | exmidunben 11939* | If any unbounded set of positive integers is equinumerous to , then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.) |
Omni EXMID | ||
Theorem | ctinfomlemom 11940* | Lemma for ctinfom 11941. Converting between and . (Contributed by Jim Kingdon, 10-Aug-2023.) |
frec | ||
Theorem | ctinfom 11941* | A condition for a set being countably infinite. Restates ennnfone 11938 in terms of and function image. Like ennnfone 11938 the condition can be summarized as being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | inffinp1 11942* | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | ctinf 11943* | A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | qnnen 11944 | The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.) |
Theorem | enctlem 11945* | Lemma for enct 11946. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | enct 11946* | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | ctiunctlemu1st 11947* | Lemma for ctiunct 11953. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemu2nd 11948* | Lemma for ctiunct 11953. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemuom 11949 | Lemma for ctiunct 11953. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemudc 11950* | Lemma for ctiunct 11953. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID DECID | ||
Theorem | ctiunctlemf 11951* | Lemma for ctiunct 11953. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemfo 11952* | Lemma for ctiunct 11953. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunct 11953* |
A sequence of enumerations gives an enumeration of the union. We refer
to "sequence of enumerations" rather than "countably many
countable
sets" because the hypothesis provides more than countability for
each
: it refers to together with the
which enumerates it.
The "countably many countable sets" version could be expressed as ⊔ and countable choice would be needed to derive the current hypothesis from that. Compare with the case of two sets instead of countably many, as seen at unct 11954, in which case we express countability using . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 11908) and using the first number to map to an element of and the second number to map to an element of B(x) . In this way we are able to map to every element of . Although it would be possible to work directly with countability expressed as ⊔ , we instead use functions from subsets of the natural numbers via ctssdccl 6996 and ctssdc 6998. (Contributed by Jim Kingdon, 31-Oct-2023.) |
⊔ ⊔ ⊔ | ||
Theorem | unct 11954* | The union of two countable sets is countable. (Contributed by Jim Kingdon, 1-Nov-2023.) |
⊔ ⊔ ⊔ | ||
An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of . The function's argument is the index of a structure component (such as for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 11983 and strslfv 12003. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an is a via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-ress 11967. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization. | ||
Syntax | cstr 11955 | Extend class notation with the class of structures with components numbered below . |
Struct | ||
Syntax | cnx 11956 | Extend class notation with the structure component index extractor. |
Syntax | csts 11957 | Set components of a structure. |
sSet | ||
Syntax | cslot 11958 | Extend class notation with the slot function. |
Slot | ||
Syntax | cbs 11959 | Extend class notation with the class of all base set extractors. |
Syntax | cress 11960 | Extend class notation with the extensible structure builder restriction operator. |
↾s | ||
Definition | df-struct 11961* |
Define a structure with components in . This is
not a
requirement for groups, posets, etc., but it is a useful assumption for
component extraction theorems.
As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set to be extensible structures. Because of 0nelfun 5141, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11972: Struct . Allowing an extensible structure to contain the empty set ensures that expressions like are structures without asserting or implying that , , and are sets (if or is a proper class, then , see opprc 3726). (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Definition | df-ndx 11962 | Define the structure component index extractor. See theorem ndxarg 11982 to understand its purpose. The restriction to ensures that is a set. The restriction to some set is necessary since is a proper class. In principle, we could have chosen or (if we revise all structure component definitions such as df-base 11965) another set such as the set of finite ordinals (df-iom 4505). (Contributed by NM, 4-Sep-2011.) |
Definition | df-slot 11963* |
Define the slot extractor for extensible structures. The class
Slot is a
function whose argument can be any set, although it is
meaningful only if that set is a member of an extensible structure (such
as a partially ordered set or a group).
Note that Slot is implemented as "evaluation at ". That is, Slot is defined to be , where will typically be a small nonzero natural number. Each extensible structure is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. The special "structure" , defined as the identity function restricted to , can be used to extract the number from a slot, since Slot (see ndxarg 11982). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression in theorems and proofs instead of its value 1). The class Slot cannot be defined as because each Slot is a function on the proper class so is itself a proper class, and the values of functions are sets (fvex 5441). It is necessary to allow proper classes as values of Slot since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.) |
Slot | ||
Theorem | sloteq 11964 | Equality theorem for the Slot construction. The converse holds if (or ) is a set. (Contributed by BJ, 27-Dec-2021.) |
Slot Slot | ||
Definition | df-base 11965 | Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Slot | ||
Definition | df-sets 11966* | Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 11967 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.) |
sSet | ||
Definition | df-ress 11967* |
Define a multifunction restriction operator for extensible structures,
which can be used to turn statements about rings into statements about
subrings, modules into submodules, etc. This definition knows nothing
about individual structures and merely truncates the set while
leaving operators alone; individual kinds of structures will need to
handle this behavior, by ignoring operators' values outside the range,
defining a function using the base set and applying that, or explicitly
truncating the slot before use.
(Credit for this operator goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) |
↾s sSet | ||
Theorem | brstruct 11968 | The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | isstruct2im 11969 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | isstruct2r 11970 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | structex 11971 | A structure is a set. (Contributed by AV, 10-Nov-2021.) |
Struct | ||
Theorem | structn0fun 11972 | A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.) |
Struct | ||
Theorem | isstructim 11973 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | isstructr 11974 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | structcnvcnv 11975 | Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | structfung 11976 | The converse of the converse of a structure is a function. Closed form of structfun 11977. (Contributed by AV, 12-Nov-2021.) |
Struct | ||
Theorem | structfun 11977 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.) |
Struct | ||
Theorem | structfn 11978 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | strnfvnd 11979 | Deduction version of strnfvn 11980. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
Theorem | strnfvn 11980 |
Value of a structure component extractor . Normally, is a
defined constant symbol such as (df-base 11965) and is a
fixed integer such as . is a
structure, i.e. a specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 12003. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.) |
Slot | ||
Theorem | strfvssn 11981 | A structure component extractor produces a value which is contained in a set dependent on , but not . This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
Theorem | ndxarg 11982 | Get the numeric argument from a defined structure component extractor such as df-base 11965. (Contributed by Mario Carneiro, 6-Oct-2013.) |
Slot | ||
Theorem | ndxid 11983 |
A structure component extractor is defined by its own index. This
theorem, together with strslfv 12003 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the in df-base 11965, making it easier to change
should the need arise.
(Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.) |
Slot Slot | ||
Theorem | ndxslid 11984 | A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 12003. (Contributed by Jim Kingdon, 29-Jan-2023.) |
Slot Slot | ||
Theorem | slotslfn 11985 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.) |
Slot | ||
Theorem | slotex 11986 | Existence of slot value. A corollary of slotslfn 11985. (Contributed by Jim Kingdon, 12-Feb-2023.) |
Slot | ||
Theorem | strndxid 11987 | The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.) |
Slot | ||
Theorem | reldmsets 11988 | The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
sSet | ||
Theorem | setsvalg 11989 | Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
sSet | ||
Theorem | setsvala 11990 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.) |
sSet | ||
Theorem | setsex 11991 | Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.) |
sSet | ||
Theorem | strsetsid 11992 | Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot Struct sSet | ||
Theorem | fvsetsid 11993 | The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.) |
sSet | ||
Theorem | setsfun 11994 | A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021.) |
sSet | ||
Theorem | setsfun0 11995 | A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun 11994 is useful for proofs based on isstruct2r 11970 which requires for to be an extensible structure. (Contributed by AV, 7-Jun-2021.) |
sSet | ||
Theorem | setsn0fun 11996 | The value of the structure replacement function (without the empty set) is a function if the structure (without the empty set) is a function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
Struct sSet | ||
Theorem | setsresg 11997 | The structure replacement function does not affect the value of away from . (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
sSet | ||
Theorem | setsabsd 11998 | Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
sSet sSet sSet | ||
Theorem | setscom 11999 | Component-setting is commutative when the x-values are different. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
sSet sSet sSet sSet | ||
Theorem | strslfvd 12000 | Deduction version of strslfv 12003. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |