Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
14-Sep-2024 | nnpredlt 4582 | The predecessor (see nnpredcl 4581) of a nonzero natural number is less than (see df-iord 4326) that number. (Contributed by Jim Kingdon, 14-Sep-2024.) |
13-Sep-2024 | nninfisollemeq 7069 | Lemma for nninfisol 7070. The case where is a successor and and are equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
13-Sep-2024 | nninfisollemne 7068 | Lemma for nninfisol 7070. A case where is a successor and and are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
13-Sep-2024 | nninfisollem0 7067 | Lemma for nninfisol 7070. The case where is zero. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
12-Sep-2024 | nninfisol 7070 | Finite elements of ℕ_{∞} are isolated. That is, given a natural number and any element of ℕ_{∞}, it is decidable whether the natural number (when converted to an element of ℕ_{∞}) is equal to the given element of ℕ_{∞}. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence to decide whether it is equal to (in fact, you only need to look at two elements and tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.) |
ℕ_{∞} DECID | ||
7-Sep-2024 | eulerthlemfi 12091 | Lemma for eulerth 12096. The set is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.) |
..^ | ||
7-Sep-2024 | modqexp 10537 | Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.) |
5-Sep-2024 | eulerthlemh 12094 | Lemma for eulerth 12096. A permutation of . (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlemth 12095 | Lemma for eulerth 12096. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlema 12093 | Lemma for eulerth 12096. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlemrprm 12092 | Lemma for eulerth 12096. and are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
30-Aug-2024 | fprodap0f 11526 | A finite product of terms apart from zero is apart from zero. A version of fprodap0 11511 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.) |
# # | ||
28-Aug-2024 | fprodrec 11519 | The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.) |
# | ||
26-Aug-2024 | exmidontri2or 7172 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
26-Aug-2024 | exmidontri 7168 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
26-Aug-2024 | ontri2orexmidim 4530 | Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4529. (Contributed by Jim Kingdon, 26-Aug-2024.) |
DECID | ||
26-Aug-2024 | ontriexmidim 4480 | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4479. (Contributed by Jim Kingdon, 26-Aug-2024.) |
DECID | ||
25-Aug-2024 | onntri2or 7175 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
25-Aug-2024 | onntri3or 7174 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
25-Aug-2024 | csbcow 3042 | Composition law for chained substitutions into a class. Version of csbco 3041 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvreuvw 2686 | Version of cbvreuv 2682 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvrexvw 2685 | Version of cbvrexv 2681 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvralvw 2684 | Version of cbvralv 2680 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvabw 2280 | Version of cbvab 2281 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | nfsbv 1927 | If is not free in , it is not free in when is distinct from and . Version of nfsb 1926 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on . (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvexvw 1900 | Change bound variable. See cbvexv 1898 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvalvw 1899 | Change bound variable. See cbvalv 1897 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | nfal 1556 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1490. (Revised by Gino Giotto, 25-Aug-2024.) |
24-Aug-2024 | gcdcomd 11849 | The operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
17-Aug-2024 | fprodcl2lem 11495 | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.) |
16-Aug-2024 | if0ab 13351 |
Expression of a conditional class as a class abstraction when the False
alternative is the empty class: in that case, the conditional class is
the extension, in the True alternative, of the condition.
Remark: a consequence which could be formalized is the inclusion and therefore, using elpwg 3551, , from which fmelpw1o 13352 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.) |
16-Aug-2024 | fprodunsn 11494 | Multiply in an additional term in a finite product. See also fprodsplitsn 11523 which is the same but with a hypothesis in place of the distinct variable condition between and . (Contributed by Jim Kingdon, 16-Aug-2024.) |
15-Aug-2024 | bj-charfundcALT 13355 | Alternate proof of bj-charfundc 13354. It was expected to be much shorter since it uses bj-charfun 13353 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
DECID | ||
15-Aug-2024 | bj-charfun 13353 | Properties of the characteristic function on the class of the class . (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | fmelpw1o 13352 |
With a formula
one can associate an element of ,
which
can therefore be thought of as the set of "truth values" (but
recall that
there are no other genuine truth values than and , by
nndc 837, which translate to and respectively by iftrue 3510
and iffalse 3513, giving pwtrufal 13540).
As proved in if0ab 13351, the associated element of is the extension, in , of the formula . (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | cnstab 8514 | Equality of complex numbers is stable. Stability here means as defined at df-stab 817. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.) |
STAB | ||
15-Aug-2024 | subap0d 8513 | Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.) |
# # | ||
15-Aug-2024 | ifexd 4443 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwun 4442 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwund 4441 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwung 4440 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifidss 3520 | A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifssun 3519 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
12-Aug-2024 | exmidontriimlem2 7151 | Lemma for exmidontriim 7154. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
12-Aug-2024 | exmidontriimlem1 7150 | Lemma for exmidontriim 7154. A variation of r19.30dc 2604. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
11-Aug-2024 | nndc 837 |
Double negation of decidability of a formula. Intuitionistic logic
refutes the negation of decidability (but does not prove decidability) of
any formula.
This should not trick the reader into thinking that EXMID is provable in intuitionistic logic. Indeed, if we could quantify over formula metavariables, then generalizing nnexmid 836 over would give " DECID ", but EXMID is "DECID ", so proving EXMID would amount to proving " DECID ", which is not implied by the above theorem. Indeed, the converse of nnal 1629 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of , like we do in our definition of EXMID (df-exmid 4156): then, we can prove DECID but we cannot prove DECID because the converse of nnral 2447 does not hold. Actually, EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying EXMID and noncontradiction holds (pm3.24 683). (Contributed by BJ, 9-Oct-2019.) Add explanation on non-provability of EXMID. (Revised by BJ, 11-Aug-2024.) |
DECID | ||
10-Aug-2024 | exmidontriim 7154 | Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | exmidontriimlem4 7153 | Lemma for exmidontriim 7154. The induction step for the induction on . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | exmidontriimlem3 7152 | Lemma for exmidontriim 7154. What we get to do based on induction on both and . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | nnnninf2 7064 | Canonical embedding of into ℕ_{∞}. (Contributed by BJ, 10-Aug-2024.) |
ℕ_{∞} | ||
10-Aug-2024 | infnninf 7061 | The point at infinity in ℕ_{∞} is the constant sequence equal to . Note that with our encoding of functions, that constant function can also be expressed as , as fconstmpt 4632 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.) |
ℕ_{∞} | ||
9-Aug-2024 | ss1o0el1o 6854 | Reformulation of ss1o0el1 4158 using instead of . (Contributed by BJ, 9-Aug-2024.) |
9-Aug-2024 | pw1dc0el 6853 | Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.) |
EXMID DECID | ||
9-Aug-2024 | ss1o0el1 4158 | A subclass of contains the empty set if and only if it equals . (Contributed by BJ and Jim Kingdon, 9-Aug-2024.) |
8-Aug-2024 | pw1dc1 6855 | If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.) |
EXMID DECID | ||
7-Aug-2024 | pw1fin 6852 | Excluded middle is equivalent to the power set of being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.) |
EXMID | ||
7-Aug-2024 | elomssom 4563 | A natural number ordinal is, as a set, included in the set of natural number ordinals. (Contributed by NM, 21-Jun-1998.) Extract this result from the previous proof of elnn 4564. (Revised by BJ, 7-Aug-2024.) |
6-Aug-2024 | bj-charfunbi 13357 |
In an ambient set , if
membership in is
stable, then it is
decidable if and only if has a characteristic function.
This characterization can be applied to singletons when the set has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.) |
STAB DECID | ||
6-Aug-2024 | bj-charfunr 13356 |
If a class has a
"weak" characteristic function on a class ,
then negated membership in is decidable (in other words,
membership in
is testable) in .
The hypothesis imposes that be a set. As usual, it could be formulated as to deal with general classes, but that extra generality would not make the theorem much more useful. The theorem would still hold if the codomain of were any class with testable equality to the point where is sent. (Contributed by BJ, 6-Aug-2024.) |
DECID | ||
6-Aug-2024 | bj-charfundc 13354 | Properties of the characteristic function on the class of the class , provided membership in is decidable in . (Contributed by BJ, 6-Aug-2024.) |
DECID | ||
6-Aug-2024 | prodssdc 11479 | Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.) |
# DECID DECID | ||
5-Aug-2024 | fnmptd 13350 | The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | funmptd 13349 |
The maps-to notation defines a function (deduction form).
Note: one should similarly prove a deduction form of funopab4 5206, then prove funmptd 13349 from it, and then prove funmpt 5207 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | 2ssom 13348 | The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | bj-dcfal 13298 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
DECID | ||
5-Aug-2024 | bj-dctru 13296 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
DECID | ||
5-Aug-2024 | bj-stfal 13288 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
STAB | ||
5-Aug-2024 | bj-sttru 13286 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
STAB | ||
5-Aug-2024 | prod1dc 11476 | Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.) |
DECID | ||
2-Aug-2024 | onntri52 7173 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri24 7171 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
2-Aug-2024 | onntri45 7170 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri51 7169 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri13 7167 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
2-Aug-2024 | onntri35 7166 |
Double negated ordinal trichotomy.
There are five equivalent statements: (1) , (2) , (3) , (4) , and (5) EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7167), (3) implies (5) (onntri35 7166), (5) implies (1) (onntri51 7169), (2) implies (4) (onntri24 7171), (4) implies (5) (onntri45 7170), and (5) implies (2) (onntri52 7173). Another way of stating this is that EXMID is equivalent to trichotomy, either the or the form, as shown in exmidontri 7168 and exmidontri2or 7172, respectively. Thus EXMID is equivalent to (1) or (2). In addition, EXMID is equivalent to (3) by onntri3or 7174 and (4) by onntri2or 7175. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
1-Aug-2024 | nnral 2447 | The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1629. (Contributed by Jim Kingdon, 1-Aug-2024.) |
31-Jul-2024 | 3nsssucpw1 7165 | Negated excluded middle implies that is not a subset of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
31-Jul-2024 | sucpw1nss3 7164 | Negated excluded middle implies that the successor of the power set of is not a subset of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
30-Jul-2024 | 3nelsucpw1 7163 | Three is not an element of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | sucpw1nel3 7162 | The successor of the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | sucpw1ne3 7161 | Negated excluded middle implies that the successor of the power set of is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
30-Jul-2024 | pw1nel3 7160 | Negated excluded middle implies that the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
30-Jul-2024 | pw1ne3 7159 | The power set of is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | pw1ne1 7158 | The power set of is not one. (Contributed by Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | pw1ne0 7157 | The power set of is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.) |
29-Jul-2024 | pw1on 7155 | The power set of is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.) |
28-Jul-2024 | exmidpweq 6851 | Excluded middle is equivalent to the power set of being . (Contributed by Jim Kingdon, 28-Jul-2024.) |
EXMID | ||
27-Jul-2024 | dcapnconstALT 13603 | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13602 by means of dceqnconst 13601. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
DECID # | ||
27-Jul-2024 | reap0 13600 | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
DECID # | ||
26-Jul-2024 | nconstwlpolemgt0 13605 | Lemma for nconstwlpo 13607. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
26-Jul-2024 | nconstwlpolem0 13604 | Lemma for nconstwlpo 13607. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
24-Jul-2024 | tridceq 13598 | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13585 and redcwlpo 13597). Thus, this is an analytic analogue to lpowlpo 7105. (Contributed by Jim Kingdon, 24-Jul-2024.) |
DECID | ||
24-Jul-2024 | iswomni0 13593 | Weak omniscience stated in terms of equality with . Like iswomninn 13592 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.) |
WOmni DECID | ||
24-Jul-2024 | lpowlpo 7105 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7104. There is an analogue in terms of analytic omniscience principles at tridceq 13598. (Contributed by Jim Kingdon, 24-Jul-2024.) |
Omni WOmni | ||
23-Jul-2024 | nconstwlpolem 13606 | Lemma for nconstwlpo 13607. (Contributed by Jim Kingdon, 23-Jul-2024.) |
23-Jul-2024 | dceqnconst 13601 | Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 13597 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.) |
DECID | ||
23-Jul-2024 | redc0 13599 | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
DECID DECID | ||
23-Jul-2024 | canth 5775 | No set is equinumerous to its power set (Cantor's theorem), i.e., no function can map onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1480 if you want the form .) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.) |
22-Jul-2024 | nconstwlpo 13607 | Existence of a certain non-constant function from reals to integers implies WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.) |
WOmni | ||
15-Jul-2024 | fprodseq 11473 | The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.) |
Copyright terms: Public domain | W3C HTML validation [external] |