HomeTheorem List (p. 1 of 10)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 1 of 10) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
We start by internalizing five standard logical connectives: {ganai}, {ge}, {go}, {ga}, and {gonai}. We will use these connectives to provide a basic logical framework for defining selbri and proving bridi. | ||
Before logic, we must define some basic elements of syntax: bridi, selbri, and sumti. We will also embrace some experimental concepts not named in the baseline valsi, but exposed in the baseline grammar: prenexes and bridi-tails. | ||
| Syntax | tsb 1 | Any selbri is a valid brirebla. |
| brirebla bu'a | ||
| Syntax | tss 2 | Any brirebla can have an additional trailing sumti. |
| brirebla bo'a ko'a | ||
| Syntax | btb 3 | Build a bridi from a sumti and brirebla. |
| bridi ko'a bo'a | ||
| Theorem | bu 4 | Normal form for unary selbri. (Contributed by la korvo, 14-Aug-2023.) |
| bridi ko'a bu'a | ||
| Theorem | bb 5 | Normal form for binary selbri. (Contributed by la korvo, 14-Aug-2023.) |
| bridi ko'a bu'a ko'e | ||
| Theorem | bt 6 | Normal form for ternary selbri. (Contributed by la korvo, 14-Aug-2023.) |
| bridi ko'a bu'a ko'e ko'i | ||
| Theorem | bq 7 | Normal form for quaternary selbri. (Contributed by la korvo, 19-Mar-2024.) |
| bridi ko'a bu'a ko'e ko'i ko'o | ||
| Theorem | bp 8 | Normal form for quinary selbri. To avoid conflict with bq 7 this syntax is "bp" for "bridi pentad". (Contributed by la korvo, 22-Jun-2024.) |
| bridi ko'a bu'a ko'e ko'i ko'o ko'u | ||
We start with the most fundamental connective, {ganai}, which denotes implication. We will build combinators from the SK basis, which is universal over parametric combinators. This gives us both an enormous degree of flexibility, because we may build any well-typed combinator, as well as confidence in correctness, because the SK basis is well-studied. We also require a single inference-building rule, ax-mp 10. In terms of category theory, {ganai broda gi brode} is an arrow in a syntactic category of equivalence classes of bridi, and the bridi {broda} and {brode} are objects. Note that, since we are using metavariables to denote bridi, we automatically denote equivalence classes. | ||
| Syntax | bgan 9 | If {broda} and {brode} are bridi, then so is {ganai broda gi brode}. In terms of category theory, our category of bridi is closed. |
| bridi ganai broda gi brode | ||
| Axiom | ax-mp 10 | Because {ganai} encodes a syllogism, it may be eliminated by modus ponens. In terms of categorical logic, {broda} implies {brode} and {broda} is assumed. |
⊢ broda  ⊢ ganai
broda gi brode  ⊢ brode | ||
| Axiom | ax-k 11 | The principle of simplification. Known as the constant combinator, or K, in combinator calculus. |
| ⊢ ganai broda gi ganai brode gi broda | ||
| Theorem | ki 12 | Inference form of ax-k 11 (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ broda ⊢ ganai
brode gi broda | ||
| Theorem | mpki 13 | Discharge a proven antecedent and replace it with another one. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ broda ⊢ ganai
broda gi brode ⊢ ganai
brodi gi brode | ||
| Theorem | kii 14 | Inference form of ki 12 (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ broda ⊢ brode ⊢ broda | ||
| Axiom | ax-s 15 | Frege's axiom. Known as the S combinator in combinator calculus. |
| ⊢ ganai ganai broda gi ganai brode gi brodi gi ganai ganai broda gi brode gi ganai broda gi brodi | ||
| Theorem | si 16 | Inference form of ax-s 15 (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
ganai broda gi brode gi ganai broda gi brodi | ||
| Theorem | mpd 17 | Deductive form of ax-mp 10 (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi ganai brode gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | id 18 | The principle of identity. This is distantly related to, but not the same as, the identity relation df-du 215. In terms of category theory, this proves that identity arrows exist. (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ ganai broda gi broda | ||
| Theorem | idd 19 | Deduction form of id 18 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi brode | ||
| Theorem | syl 20 | The quintessential syllogism. This inference is a standard workhorse for producing deductive forms. In terms of category theory, it composes arrows. (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
brode gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | sd 21 | Deductive form of ax-s 15 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ⊢ ganai
broda gi ganai
ganai brode gi brodi gi ganai brode gi brodo | ||
| Theorem | mpdd 22 | Nested form of mpd 17 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
broda gi ganai brode gi ganai brodi gi brodo ⊢ ganai
broda gi ganai brode gi brodo | ||
| Theorem | sylcom 23 | A syllogism which shuffles antecedents. (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
brode gi ganai brodi gi brodo ⊢ ganai
broda gi ganai brode gi brodo | ||
| Theorem | syl6 24 | A syllogism replacing consequents. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
brodi gi brodo ⊢ ganai
broda gi ganai brode gi brodo | ||
| Theorem | syl6c 25 | A contractive variant of syl6 24 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
broda gi ganai brode gi brodo ⊢ ganai
brodi gi ganai brodo gi brodu ⊢ ganai
broda gi ganai brode gi brodu | ||
| Theorem | kd 26 | Deductive form of ax-k 11 (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi ganai brodi gi brode | ||
| Theorem | syl5com 27 | A syllogism which shuffles antecedents. (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
brodi gi ganai brode gi brodo ⊢ ganai
broda gi ganai brodi gi brodo | ||
| Theorem | ganai-swap12 28 | Naturally swap the first and second antecedents in an internalized inference. (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
brode gi ganai broda gi brodi | ||
| Theorem | mpc 29 | A closed version of ax-mp 10 (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi ganai ganai broda gi brode gi brode | ||
| Theorem | syl5 30 | A syllogism which shuffles antecedents. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
brodi gi ganai brode gi brodo ⊢ ganai
brodi gi ganai broda gi brodo | ||
| Theorem | syl2im 31 | Replace two antecedents in parallel. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
brodi gi brodo ⊢ ganai
brode gi ganai brodo gi brodu ⊢ ganai
broda gi ganai brodi gi brodu | ||
| Theorem | ganai-abs 32 | Absorb a redundant antecedent. (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi ganai broda gi brode ⊢ ganai
broda gi brode | ||
| Theorem | sylc 33 | A contracting syllogism. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi brodi ⊢ ganai
brode gi ganai brodi gi brodo ⊢ ganai
broda gi brodo | ||
| Theorem | mpi 34 | A nested modus ponens. (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ broda ⊢ ganai
brode gi ganai broda gi brodi ⊢ ganai
brode gi brodi | ||
| Theorem | mp2 35 | Double modus ponens. (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ broda ⊢ brode ⊢ ganai
broda gi ganai brode gi brodi ⊢ brodi | ||
| Theorem | imim2d 36 | A deduction. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
broda gi ganai
ganai brodo gi brode gi ganai brodo gi brodi | ||
| Theorem | imim2 37 | A closed syllogism. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai ganai broda gi brode gi ganai ganai brodi gi broda gi ganai brodi gi brode | ||
| Theorem | syldd 38 | Deduction form of syld (future) (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ⊢ ganai
broda gi ganai brode gi ganai brodo gi brodu ⊢ ganai
broda gi ganai brode gi ganai brodi gi brodu | ||
| Theorem | syl5d 39 | Deduction form of syl5 30 (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
broda gi ganai brodo gi ganai brodi gi brodu ⊢ ganai
broda gi ganai brodo gi ganai brode gi brodu | ||
| Theorem | syl9 40 | A syllogism. (Contributed by la korvo, 1-Jan-2025.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
brodo gi ganai brodi gi brodu ⊢ ganai
broda gi ganai brodo gi ganai brode gi brodu | ||
| Theorem | ganai-swap23 41 | Naturally swap the second and third antecedents in an internalized inference. (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ⊢ ganai
broda gi ganai brodi gi ganai brode gi brodo | ||
| Syntax | bge 42 |
|
| bridi ge broda gi brode | ||
| Axiom | ax-ge-le 43 | Elimination of {ge} on the left. Curry of the left-hand projection. |
| ⊢ ganai ge broda gi brode gi broda | ||
| Axiom | ax-ge-re 44 |
Elimination of {ge} on the right. Curry of the right-hand
projection.
|
| ⊢ ganai ge broda gi brode gi brode | ||
| Axiom | ax-ge-in 45 | Introduction of {ge}. Curry of the I combinator. |
| ⊢ ganai broda gi ganai brode gi ge broda gi brode | ||
| Theorem | ge-lei 46 | Inference form of ax-ge-le 43 (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ ge broda gi brode ⊢ broda | ||
| Theorem | ge-led 47 | Deductive form of ax-ge-le 43 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ge brode gi brodi ⊢ ganai
broda gi brode | ||
| Theorem | ge-rei 48 | Inference form of ax-ge-re 44 (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ ge broda gi brode ⊢ brode | ||
| Theorem | ge-red 49 | Deductive form of ax-ge-re 44 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ge brode gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | ge-ini 50 | Inference form of ax-ge-in 45 (Contributed by la korvo, 27-Jul-2023.) |
| ⊢ broda ⊢ brode ⊢ ge
broda gi brode | ||
| Theorem | ge-ganai 51 | Conjunction implies implication. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ganai ge broda gi brode gi ganai broda gi brode | ||
| Theorem | ge-in-swap12 52 | ax-ge-in 45 with swapped antecedents. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi ge brode gi broda | ||
| Theorem | cur 53 | The natural curry (or "import") for any well-formed statement. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
ge broda gi brode gi brodi | ||
| Theorem | uncur 54 | The natural uncurry (or "export") for any well-formed statement. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai
ge broda gi brode gi brodi ⊢ ganai
broda gi ganai brode gi brodi | ||
| Theorem | jca 55 | "Join Consequents with AND". (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi brodi ⊢ ganai
broda gi ge brode gi brodi | ||
| Theorem | syl2anc 56 | A contracting syllogism. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi brodi ⊢ ganai
ge brode gi brodi gi brodo ⊢ ganai
broda gi brodo | ||
| Theorem | mpancom 57 | A variant of mpan 58 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
ge brode gi broda gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | mpan 58 | An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ broda ⊢ ganai
ge broda gi brode gi brodi ⊢ ganai
brode gi brodi | ||
| Theorem | mp2an 59 | An inference eliminating a conjunction from the antecedent. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ broda ⊢ brode ⊢ ganai
ge broda gi brode gi brodi ⊢ brodi | ||
| Syntax | bgo 60 | If {broda} and {brode} are bridi, then so is {go broda gi brode}. |
| bridi go broda gi brode | ||
| Definition | df-go 61 | Definition of {go} in terms of {ganai} and {ge}. This is the standard definition of the biconditional connective in higher-order intuitionistic logic. This can be justified intuitionistically; see theorem df-bi along with bijust from [ILE] p. 0. |
| ⊢ ge ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda gi ganai ge ganai broda gi brode gi ganai brode gi broda gi go broda gi brode | ||
| Theorem | goli 62 | Inference form of left side of df-go 61 (Contributed by la korvo, 29-Jul-2023.) |
| ⊢ go broda gi brode ⊢ ge
ganai broda gi brode gi ganai brode gi broda | ||
| Theorem | go-ganai 63 | Biconditional implication may be weakened to unidirectional implication. Category-theoretically, this theorem embeds the core of Loj. Inference form of left side of goli 62. (Contributed by la korvo, 17-Jul-2023.) (Shortened by la korvo, 29-Jul-2023.) |
| ⊢ go broda gi brode ⊢ ganai
broda gi brode | ||
| Theorem | gori 64 | Inference form of right side of df-go 61 (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ge
ganai broda gi brode gi ganai brode gi broda ⊢ go
broda gi brode | ||
| Theorem | iso 65 | Inference form of right side of gori 64 (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
brode gi broda ⊢ go
broda gi brode | ||
| Theorem | bi1 66 | Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai go broda gi brode gi ganai broda gi brode | ||
| Theorem | bi2 67 | Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai go broda gi brode gi ganai brode gi broda | ||
| Theorem | bi3 68 | Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai ganai broda gi brode gi ganai ganai brode gi broda gi go broda gi brode | ||
| Theorem | go-ganaid 69 | Deduction form of go-ganai 63 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi go brode gi brodi ⊢ ganai
broda gi ganai brode gi brodi | ||
| Theorem | isodd 70 | Double deduction form of iso 65 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi ganai brodi gi brodo ⊢ ganai
broda gi ganai brode gi ganai brodo gi brodi ⊢ ganai
broda gi ganai brode gi go brodi gi brodo | ||
| Theorem | isod-lem 71 | Lemma for isod 72 known as theorem impbid21d in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
| Theorem | isod 72 | Deduction form of iso 65 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ganai brode gi brodi ⊢ ganai
broda gi ganai brodi gi brode ⊢ ganai
broda gi go brode gi brodi | ||
| Theorem | go-id 73 | {go} is reflexive. (Contributed by la korvo, 30-Jul-2023.) |
| ⊢ go broda gi broda | ||
| Theorem | go-com-lem 74 | Lemma: {go} commutes in one direction. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai go broda gi brode gi go brode gi broda | ||
| Theorem | go-com 75 | {go} commutes. (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ go go broda gi brode gi go brode gi broda | ||
| Theorem | go-comi 76 | Inference form of go-com 75 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ go broda gi brode ⊢ go
brode gi broda | ||
| Axiom | ax-go-trans 77 | {go} is transitive. |
| ⊢ go broda gi brode ⊢ go
brode gi brodi ⊢ go
broda gi brodi | ||
| Theorem | go-syl 78 | {go} admits composition. (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ go broda gi brode ⊢ go
brode gi brodi ⊢ go
broda gi brodi | ||
| Theorem | bi 79 | Like modus ponens ax-mp 10 but for biconditionals. (Contributed by la korvo, 16-Jul-2023.) |
| ⊢ broda ⊢ go
broda gi brode ⊢ brode | ||
| Theorem | bi-rev 80 | Modus ponens in the other direction. (Contributed by la korvo, 16-Jul-2023.) |
| ⊢ broda ⊢ go
brode gi broda ⊢ brode | ||
| Theorem | bi-rev-syl 81 | The right-hand side of a {go} may also be weakened to a {ganai}. (Contributed by la korvo, 10-Jul-2023.) |
| ⊢ go broda gi brode ⊢ ganai
brode gi broda | ||
| Theorem | sylbi 82 | Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ go broda gi brode ⊢ ganai
brode gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | sylib 83 | Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ganai broda gi brode ⊢ go
brode gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | sylibr 84 | Apply a definition to a consequent. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ganai broda gi brode ⊢ go
brodi gi brode ⊢ ganai
broda gi brodi | ||
| Theorem | sylanbrc 85 | Deductive unpacking of a definition with conjoined components. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi brodi ⊢ go
brodo gi ge brode gi brodi ⊢ ganai
broda gi brodo | ||
| Theorem | syl5bi 86 | Replace a nested antecedent using a biconditional. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ go broda gi brode ⊢ ganai
brodi gi ganai brode gi brodo ⊢ ganai
brodi gi ganai broda gi brodo | ||
Unlike the other four connectives, {ganai} is not symmetric. As a result, Lojban's grammar admits both a left-to-right and right-to-left version of each connective for implication. | ||
| Syntax | sjnaa 87 |
|
| sumti ko'a na.a ko'e | ||
| Definition | df-na.a 88 | Definition of {na.a} in terms of {ganai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
| ⊢ go ko'a na.a ko'e bo'a gi ganai ko'a bo'a gi ko'e bo'a | ||
| Theorem | naai 89 | Inference form of df-na.a 88 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ko'a na.a ko'e
bo'a ⊢
ganai ko'a bo'a gi ko'e
bo'a | ||
| Theorem | naaii 90 | Inference form of df-na.a 88 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ko'a na.a ko'e
bo'a ⊢ ko'a bo'a ⊢ ko'e bo'a | ||
| Theorem | naari 91 | Reverse inference form of df-na.a 88 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ganai ko'a bo'a gi
ko'e bo'a ⊢ ko'a na.a ko'e
bo'a | ||
| Theorem | na.a-refl 92 | {na.a} is reflexive over any brirebla. (Contributed by la korvo, 14-Aug-2024.) |
| ⊢ ko'a na.a ko'a bo'a | ||
| Syntax | sjanai 93 |
|
| sumti ko'a .anai ko'e | ||
| Definition | df-anai 94 | Definition of {.anai} in terms of {ganai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
| ⊢ go ko'e .anai ko'a bo'a gi ganai ko'a bo'a gi ko'e bo'a | ||
| Theorem | anaii 95 | Inference form of df-anai 94 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'e .anai ko'a
bo'a ⊢
ganai ko'a bo'a gi ko'e
bo'a | ||
| Theorem | anaiii 96 | Inference form of df-anai 94 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'e .anai ko'a
bo'a ⊢ ko'a bo'a ⊢ ko'e bo'a | ||
| Theorem | anairi 97 | Reverse inference form of df-anai 94 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ganai ko'a bo'a gi
ko'e bo'a ⊢ ko'e .anai ko'a
bo'a | ||
| Syntax | sbnaja 98* |
|
| selbri bu'a naja bu'e | ||
| Definition | df-naja 99* | Definition of {naja} in terms of {ganai}. By analogy with example 12.2-5 of [CLL] p. 14. |
| ⊢ go ko'a bu'a naja bu'e ko'e gi ganai ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
| Theorem | najai 100* | Inference form of df-naja 99 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ko'a bu'a naja
bu'e ko'e ⊢ ganai
ko'a bu'a ko'e gi ko'a
bu'e ko'e | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |