Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison zf-in-agda.html @ 361:4cbcf71b09c4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Jul 2020 16:33:30 +0900
parents 5e22b23ee3fd
children f7d66c84bc26
comparison
equal deleted inserted replaced
360:2a8a51375e49 361:4cbcf71b09c4
938 Agda Set / Type / it also has a level 938 Agda Set / Type / it also has a level
939 939
940 </pre> 940 </pre>
941 941
942 <hr/> 942 <hr/>
943 <h2><a name="content039">Fixes on ZF to intuitionistic logic</a></h2> 943 <h2><a name="content039">Fixing ZF axom to fit intuitionistic logic</a></h2>
944 944
945 <p> 945 <p>
946 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define 946 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
947 ZF axioms in Agda. 947 ZF axioms in Agda.
948 <p> 948 <p>
1203 1203
1204 </pre> 1204 </pre>
1205 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which 1205 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which
1206 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal. 1206 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal.
1207 <p> 1207 <p>
1208
1209 <hr/>
1210 <h2><a name="content048">HOD Ordrinal mapping</a></h2>
1211 We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger.
1212 The address of HOD can be larger at least it have to be larger than the content's address.
1213 We only have a relative ordering such as
1214 <p>
1215
1216 <pre>
1217 pair-xx&lt;xy : {x y : HOD} → od→ord (x , x) o&lt; osuc (od→ord (x , y) )
1218 pair&lt;y : {x y : HOD } → y ∋ x → od→ord (x , x) o&lt; osuc (od→ord y)
1219
1220 </pre>
1221 Basicaly, we cannot know the concrete address of HOD other than empty set.
1222 <p>
1223 <img src="fig/address-of-HOD.svg">
1224
1225 <p>
1226
1227 <hr/>
1228 <h2><a name="content049">Possible restriction on HOD</a></h2>
1208 We need some restriction on the HOD-Ordinal mapping. Simple one is this. 1229 We need some restriction on the HOD-Ordinal mapping. Simple one is this.
1209 <p> 1230 <p>
1210 1231
1211 <pre> 1232 <pre>
1212 ωmax : Ordinal 1233 ωmax : Ordinal
1227 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. 1248 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound.
1228 This is the reason of necessity of Axiom of infinite. 1249 This is the reason of necessity of Axiom of infinite.
1229 <p> 1250 <p>
1230 1251
1231 <hr/> 1252 <hr/>
1232 <h2><a name="content048">increment pase of address of HOD</a></h2> 1253 <h2><a name="content050">increment pase of address of HOD</a></h2>
1233 The address of HOD may have obvious bound, but it is defined in a relative way. 1254 Assuming, hod-ord&lt; , we have
1234 <p>
1235
1236 <pre>
1237 pair-xx&lt;xy : {x y : HOD} → od→ord (x , x) o&lt; osuc (od→ord (x , y) )
1238 pair&lt;y : {x y : HOD } → y ∋ x → od→ord (x , x) o&lt; osuc (od→ord y)
1239
1240 </pre>
1241 Basicaly, we cannot know the concrete address of HOD other than empty set.
1242 <p>
1243 Assuming, previous assuption, we have
1244 <p> 1255 <p>
1245 1256
1246 <pre> 1257 <pre>
1247 pair-ord&lt; : {x : HOD } → ( {y : HOD } → od→ord y o&lt; next (odmax y) ) → od→ord ( x , x ) o&lt; next (od→ord x) 1258 pair-ord&lt; : {x : HOD } → ( {y : HOD } → od→ord y o&lt; next (odmax y) ) → od→ord ( x , x ) o&lt; next (od→ord x)
1248 pair-ord&lt; {x} ho&lt; = subst (λ k → od→ord (x , x) o&lt; k ) lemmab0 lemmab1 where 1259 pair-ord&lt; {x} ho&lt; = subst (λ k → od→ord (x , x) o&lt; k ) lemmab0 lemmab1 where
1249 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x) 1260 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
1250 1261
1251 </pre> 1262 </pre>
1252 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. 1263 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove
1253 <p> 1264 <p>
1265
1266 <pre>
1267 infinite-bound : ({x : HOD} → od→ord x o&lt; next (odmax x)) → {y : Ordinal} → infinite-d y → y o&lt; next o∅
1268
1269 </pre>
1254 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x), c&lt;→o&lt; can be drived from ⊆→o≤ . 1270 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x), c&lt;→o&lt; can be drived from ⊆→o≤ .
1255 <p> 1271 <p>
1256 1272
1257 <pre> 1273 <pre>
1258 ⊆→o≤→c&lt;→o&lt; : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) 1274 ⊆→o≤→c&lt;→o&lt; : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
1260 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y 1276 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y
1261 1277
1262 </pre> 1278 </pre>
1263 1279
1264 <hr/> 1280 <hr/>
1265 <h2><a name="content049">Non constructive assumptions so far</a></h2> 1281 <h2><a name="content051">Non constructive assumptions so far</a></h2>
1266 1282
1267 <p> 1283 <p>
1268 1284
1269 <pre> 1285 <pre>
1270 od→ord : HOD → Ordinal 1286 od→ord : HOD → Ordinal
1278 sup-o&lt; : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o&lt; sup-o A ψ 1294 sup-o&lt; : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o&lt; sup-o A ψ
1279 1295
1280 </pre> 1296 </pre>
1281 1297
1282 <hr/> 1298 <hr/>
1283 <h2><a name="content050">Axiom which have negation form</a></h2> 1299 <h2><a name="content052">Axiom which have negation form</a></h2>
1284 1300
1285 <p> 1301 <p>
1286 1302
1287 <pre> 1303 <pre>
1288 Union, Selection 1304 Union, Selection
1302 </pre> 1318 </pre>
1303 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. 1319 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
1304 <p> 1320 <p>
1305 1321
1306 <hr/> 1322 <hr/>
1307 <h2><a name="content051">Union </a></h2> 1323 <h2><a name="content053">Union </a></h2>
1308 The original form of the Axiom of Union is 1324 The original form of the Axiom of Union is
1309 <p> 1325 <p>
1310 1326
1311 <pre> 1327 <pre>
1312 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) 1328 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
1357 </pre> 1373 </pre>
1358 which checks existence using contra-position. 1374 which checks existence using contra-position.
1359 <p> 1375 <p>
1360 1376
1361 <hr/> 1377 <hr/>
1362 <h2><a name="content052">Axiom of replacement</a></h2> 1378 <h2><a name="content054">Axiom of replacement</a></h2>
1363 We can replace the elements of a set by a function and it becomes a set. From the book, 1379 We can replace the elements of a set by a function and it becomes a set. From the book,
1364 <p> 1380 <p>
1365 1381
1366 <pre> 1382 <pre>
1367 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 1383 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
1408 <p> 1424 <p>
1409 Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship. 1425 Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship.
1410 <p> 1426 <p>
1411 1427
1412 <hr/> 1428 <hr/>
1413 <h2><a name="content053">Validity of Power Set Axiom</a></h2> 1429 <h2><a name="content055">Validity of Power Set Axiom</a></h2>
1414 The original Power Set Axiom is this. 1430 The original Power Set Axiom is this.
1415 <p> 1431 <p>
1416 1432
1417 <pre> 1433 <pre>
1418 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) 1434 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
1501 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 1517 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
1502 1518
1503 </pre> 1519 </pre>
1504 1520
1505 <hr/> 1521 <hr/>
1506 <h2><a name="content054">Axiom of regularity, Axiom of choice, ε-induction</a></h2> 1522 <h2><a name="content056">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
1507 1523
1508 <p> 1524 <p>
1509 Axiom of regularity requires non self intersectable elements (which is called minimum), if we 1525 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
1510 replace it by a function, it becomes a choice function. It makes axiom of choice valid. 1526 replace it by a function, it becomes a choice function. It makes axiom of choice valid.
1511 <p> 1527 <p>
1548 </pre> 1564 </pre>
1549 It does not requires ∅ ∉ X . 1565 It does not requires ∅ ∉ X .
1550 <p> 1566 <p>
1551 1567
1552 <hr/> 1568 <hr/>
1553 <h2><a name="content055">Axiom of choice and Law of Excluded Middle</a></h2> 1569 <h2><a name="content057">Axiom of choice and Law of Excluded Middle</a></h2>
1554 In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, 1570 In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
1555 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, 1571 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
1556 but it requires law of the exclude middle. 1572 but it requires law of the exclude middle.
1557 <p> 1573 <p>
1558 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can 1574 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
1568 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice 1584 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
1569 and Law of Excluded Middle is equivalent in our mode. 1585 and Law of Excluded Middle is equivalent in our mode.
1570 <p> 1586 <p>
1571 1587
1572 <hr/> 1588 <hr/>
1573 <h2><a name="content056">Relation-ship among ZF axiom</a></h2> 1589 <h2><a name="content058">Relation-ship among ZF axiom</a></h2>
1574 <img src="fig/axiom-dependency.svg"> 1590 <img src="fig/axiom-dependency.svg">
1575 1591
1576 <p> 1592 <p>
1577 1593
1578 <hr/> 1594 <hr/>
1579 <h2><a name="content057">Non constructive assumption in our model</a></h2> 1595 <h2><a name="content059">Non constructive assumption in our model</a></h2>
1580 mapping between HOD and Ordinals 1596 mapping between HOD and Ordinals
1581 <p> 1597 <p>
1582 1598
1583 <pre> 1599 <pre>
1584 od→ord : HOD → Ordinal 1600 od→ord : HOD → Ordinal
1620 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) 1636 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) )
1621 1637
1622 </pre> 1638 </pre>
1623 1639
1624 <hr/> 1640 <hr/>
1625 <h2><a name="content058">So it this correct?</a></h2> 1641 <h2><a name="content060">So it this correct?</a></h2>
1626 1642
1627 <p> 1643 <p>
1628 Our axiom are syntactically the same in the text book, but negations are slightly different. 1644 Our axiom are syntactically the same in the text book, but negations are slightly different.
1629 <p> 1645 <p>
1630 If we assumes excluded middle, these are exactly same. 1646 If we assumes excluded middle, these are exactly same.
1640 <p> 1656 <p>
1641 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. 1657 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
1642 <p> 1658 <p>
1643 1659
1644 <hr/> 1660 <hr/>
1645 <h2><a name="content059">How to use Agda Set Theory</a></h2> 1661 <h2><a name="content061">How to use Agda Set Theory</a></h2>
1646 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be 1662 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
1647 postulated or assuming law of excluded middle. 1663 postulated or assuming law of excluded middle.
1648 <p> 1664 <p>
1649 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check 1665 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
1650 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. 1666 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
1651 <p> 1667 <p>
1652 ZF record itself is not necessary, for example, topology theory without ZF can be possible. 1668 ZF record itself is not necessary, for example, topology theory without ZF can be possible.
1653 <p> 1669 <p>
1654 1670
1655 <hr/> 1671 <hr/>
1656 <h2><a name="content060">Topos and Set Theory</a></h2> 1672 <h2><a name="content062">Topos and Set Theory</a></h2>
1657 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a 1673 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
1658 sub-object classifier. 1674 sub-object classifier.
1659 <p> 1675 <p>
1660 Topos itself is model of intuitionistic logic. 1676 Topos itself is model of intuitionistic logic.
1661 <p> 1677 <p>
1669 <p> 1685 <p>
1670 Our Agda model is a proof theoretic version of it. 1686 Our Agda model is a proof theoretic version of it.
1671 <p> 1687 <p>
1672 1688
1673 <hr/> 1689 <hr/>
1674 <h2><a name="content061">Cardinal number and Continuum hypothesis</a></h2> 1690 <h2><a name="content063">Cardinal number and Continuum hypothesis</a></h2>
1675 Axiom of choice is required to define cardinal number 1691 Axiom of choice is required to define cardinal number
1676 <p> 1692 <p>
1677 definition of cardinal number is not yet done 1693 definition of cardinal number is not yet done
1678 <p> 1694 <p>
1679 definition of filter is not yet done 1695 definition of filter is not yet done
1687 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) 1703 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
1688 1704
1689 </pre> 1705 </pre>
1690 1706
1691 <hr/> 1707 <hr/>
1692 <h2><a name="content062">Filter</a></h2> 1708 <h2><a name="content064">Filter</a></h2>
1693 1709
1694 <p> 1710 <p>
1695 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number 1711 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
1696 is depends on axiom of choice. 1712 is depends on axiom of choice.
1697 <p> 1713 <p>
1710 <p> 1726 <p>
1711 This may be simpler than classical forcing theory ( not yet done). 1727 This may be simpler than classical forcing theory ( not yet done).
1712 <p> 1728 <p>
1713 1729
1714 <hr/> 1730 <hr/>
1715 <h2><a name="content063">Programming Mathematics</a></h2> 1731 <h2><a name="content065">Programming Mathematics</a></h2>
1716 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical 1732 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
1717 structure are 1733 structure are
1718 <p> 1734 <p>
1719 1735
1720 <pre> 1736 <pre>
1735 </pre> 1751 </pre>
1736 are proved in Agda. 1752 are proved in Agda.
1737 <p> 1753 <p>
1738 1754
1739 <hr/> 1755 <hr/>
1740 <h2><a name="content064">link</a></h2> 1756 <h2><a name="content066">link</a></h2>
1741 Summer school of foundation of mathematics (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/</a> 1757 Summer school of foundation of mathematics (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/</a>
1742 <p> 1758 <p>
1743 Foundation of axiomatic set theory (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf 1759 Foundation of axiomatic set theory (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf
1744 </a> 1760 </a>
1745 <p> 1761 <p>
1794 <li><a href="#content034"> OD is not ZF Set</a> 1810 <li><a href="#content034"> OD is not ZF Set</a>
1795 <li><a href="#content035"> HOD : Hereditarily Ordinal Definable</a> 1811 <li><a href="#content035"> HOD : Hereditarily Ordinal Definable</a>
1796 <li><a href="#content036"> 1 to 1 mapping between an HOD and an Ordinal</a> 1812 <li><a href="#content036"> 1 to 1 mapping between an HOD and an Ordinal</a>
1797 <li><a href="#content037"> Order preserving in the mapping of OD and Ordinal</a> 1813 <li><a href="#content037"> Order preserving in the mapping of OD and Ordinal</a>
1798 <li><a href="#content038"> Various Sets</a> 1814 <li><a href="#content038"> Various Sets</a>
1799 <li><a href="#content039"> Fixes on ZF to intuitionistic logic</a> 1815 <li><a href="#content039"> Fixing ZF axom to fit intuitionistic logic</a>
1800 <li><a href="#content040"> Pure logical axioms</a> 1816 <li><a href="#content040"> Pure logical axioms</a>
1801 <li><a href="#content041"> Axiom of Pair</a> 1817 <li><a href="#content041"> Axiom of Pair</a>
1802 <li><a href="#content042"> pair in OD</a> 1818 <li><a href="#content042"> pair in OD</a>
1803 <li><a href="#content043"> Validity of Axiom of Pair</a> 1819 <li><a href="#content043"> Validity of Axiom of Pair</a>
1804 <li><a href="#content044"> Equality of OD and Axiom of Extensionality </a> 1820 <li><a href="#content044"> Equality of OD and Axiom of Extensionality </a>
1805 <li><a href="#content045"> Validity of Axiom of Extensionality</a> 1821 <li><a href="#content045"> Validity of Axiom of Extensionality</a>
1806 <li><a href="#content046"> Axiom of infinity</a> 1822 <li><a href="#content046"> Axiom of infinity</a>
1807 <li><a href="#content047"> ω in HOD</a> 1823 <li><a href="#content047"> ω in HOD</a>
1808 <li><a href="#content048"> increment pase of address of HOD</a> 1824 <li><a href="#content048"> HOD Ordrinal mapping</a>
1809 <li><a href="#content049"> Non constructive assumptions so far</a> 1825 <li><a href="#content049"> Possible restriction on HOD</a>
1810 <li><a href="#content050"> Axiom which have negation form</a> 1826 <li><a href="#content050"> increment pase of address of HOD</a>
1811 <li><a href="#content051"> Union </a> 1827 <li><a href="#content051"> Non constructive assumptions so far</a>
1812 <li><a href="#content052"> Axiom of replacement</a> 1828 <li><a href="#content052"> Axiom which have negation form</a>
1813 <li><a href="#content053"> Validity of Power Set Axiom</a> 1829 <li><a href="#content053"> Union </a>
1814 <li><a href="#content054"> Axiom of regularity, Axiom of choice, ε-induction</a> 1830 <li><a href="#content054"> Axiom of replacement</a>
1815 <li><a href="#content055"> Axiom of choice and Law of Excluded Middle</a> 1831 <li><a href="#content055"> Validity of Power Set Axiom</a>
1816 <li><a href="#content056"> Relation-ship among ZF axiom</a> 1832 <li><a href="#content056"> Axiom of regularity, Axiom of choice, ε-induction</a>
1817 <li><a href="#content057"> Non constructive assumption in our model</a> 1833 <li><a href="#content057"> Axiom of choice and Law of Excluded Middle</a>
1818 <li><a href="#content058"> So it this correct?</a> 1834 <li><a href="#content058"> Relation-ship among ZF axiom</a>
1819 <li><a href="#content059"> How to use Agda Set Theory</a> 1835 <li><a href="#content059"> Non constructive assumption in our model</a>
1820 <li><a href="#content060"> Topos and Set Theory</a> 1836 <li><a href="#content060"> So it this correct?</a>
1821 <li><a href="#content061"> Cardinal number and Continuum hypothesis</a> 1837 <li><a href="#content061"> How to use Agda Set Theory</a>
1822 <li><a href="#content062"> Filter</a> 1838 <li><a href="#content062"> Topos and Set Theory</a>
1823 <li><a href="#content063"> Programming Mathematics</a> 1839 <li><a href="#content063"> Cardinal number and Continuum hypothesis</a>
1824 <li><a href="#content064"> link</a> 1840 <li><a href="#content064"> Filter</a>
1841 <li><a href="#content065"> Programming Mathematics</a>
1842 <li><a href="#content066"> link</a>
1825 </ol> 1843 </ol>
1826 1844
1827 <hr/> Shinji KONO / Tue Jul 14 15:02:38 2020 1845 <hr/> Shinji KONO / Fri Jul 17 13:42:02 2020
1828 </body></html> 1846 </body></html>