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

comparison zf-in-agda.html @ 338:bca043423554

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 Sun, 12 Jul 2020 12:32:42 +0900
parents 197e0b3d39dc
children 5e22b23ee3fd
comparison
equal deleted inserted replaced
337:de2c472bcbcd 338:bca043423554
96 <p> 96 <p>
97 It has some amount of difficulty and self circulating discussion. 97 It has some amount of difficulty and self circulating discussion.
98 <p> 98 <p>
99 I'm planning to do it in my old age, but I'm enough age now. 99 I'm planning to do it in my old age, but I'm enough age now.
100 <p> 100 <p>
101 This is done during from May to September. 101 if you familier with Agda, you can skip to <a href="#set-theory">
102 there
103 </a>
102 <p> 104 <p>
103 105
104 <hr/> 106 <hr/>
105 <h2><a name="content004">Agda and Intuitionistic Logic </a></h2> 107 <h2><a name="content004">Agda and Intuitionistic Logic </a></h2>
106 Curry Howard Isomorphism 108 Curry Howard Isomorphism
373 Writing some type in a module argument is the same as postulating a type, but 375 Writing some type in a module argument is the same as postulating a type, but
374 postulate can be written the middle of a proof. 376 postulate can be written the middle of a proof.
375 <p> 377 <p>
376 postulate can be constructive. 378 postulate can be constructive.
377 <p> 379 <p>
378 postulate can be inconsistent, which result everything has a proof. 380 postulate can be inconsistent, which result everything has a proof. Actualy this assumption
381 doesnot work for Ordinals, we discuss this later.
379 <p> 382 <p>
380 383
381 <hr/> 384 <hr/>
382 <h2><a name="content015"> A ∨ B</a></h2> 385 <h2><a name="content015"> A ∨ B</a></h2>
383 386
584 587
585 <hr/> 588 <hr/>
586 <h2><a name="content023">Classical story of ZF Set Theory</a></h2> 589 <h2><a name="content023">Classical story of ZF Set Theory</a></h2>
587 590
588 <p> 591 <p>
592 <a name="set-theory">
589 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads 593 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
590 a relative consistency proof of the Set Theory. 594 a relative consistency proof of the Set Theory.
591 Ordinal number is used in the flow. 595 Ordinal number is used in the flow.
592 <p> 596 <p>
593 In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD). 597 In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
645 → ∀ (x : ord) → ψ x 649 → ∀ (x : ord) → ψ x
646 650
647 </pre> 651 </pre>
648 652
649 <hr/> 653 <hr/>
650 <h2><a name="content026">Concrete Ordinals</a></h2> 654 <h2><a name="content026">Concrete Ordinals or Countable Ordinals</a></h2>
651 655
652 <p> 656 <p>
653 We can define a list like structure with level, which is a kind of two dimensional infinite array. 657 We can define a list like structure with level, which is a kind of two dimensional infinite array.
654 <p> 658 <p>
655 659
740 This operation can be performed within a ZF Set theory. Classical Set Theory assumes 744 This operation can be performed within a ZF Set theory. Classical Set Theory assumes
741 ZF, so this kind of thing is allowed. 745 ZF, so this kind of thing is allowed.
742 <p> 746 <p>
743 But in our case, we have no ZF theory, so we are going to use Ordinals. 747 But in our case, we have no ZF theory, so we are going to use Ordinals.
744 <p> 748 <p>
749 The idea is to use an ordinal as a pointer to a record which defines a Set.
750 If the recored defines a series of Ordinals which is a pointer to the Set. This record looks like a Set.
751 <p>
745 752
746 <hr/> 753 <hr/>
747 <h2><a name="content032">Ordinal Definable Set</a></h2> 754 <h2><a name="content032">Ordinal Definable Set</a></h2>
748 We can define a sbuset of Ordinals using predicates. What is a subset? 755 We can define a sbuset of Ordinals using predicates. What is a subset?
749 <p> 756 <p>
763 </pre> 770 </pre>
764 Ordinals itself is not a set in a ZF Set theory but a class. In OD, 771 Ordinals itself is not a set in a ZF Set theory but a class. In OD,
765 <p> 772 <p>
766 773
767 <pre> 774 <pre>
768 record { def = λ x → true } 775 data One : Set n where
769 776 OneObj : One
770 </pre> 777 record { def = λ x → One }
771 means Ordinals itself, so ODs are larger than a notion of ZF Set Theory, 778
772 but we don't care about it. 779 </pre>
773 <p> 780 means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set.
774 781 You can say OD is a class in ZF Set Theory term.
775 <hr/> 782 <p>
776 <h2><a name="content033">∋ in OD</a></h2> 783
777 OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping 784 <hr/>
778 <p> 785 <h2><a name="content033">OD is not ZF Set</a></h2>
779 786 If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like
780 <pre> 787 a Set. The idea is to use an ordinal as a pointer to OD.
781 od→ord : OD → Ordinal 788 Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like
782 789 <p>
783 </pre> 790
784 we may check an OD is an element of the OD using def. 791 <pre>
792 ¬OD-order : ( od→ord : OD → Ordinal )
793 → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y) → ⊥
794 ¬OD-order od→ord ord→od c&lt;→o&lt; = ?
795
796 </pre>
797 Actualy we can prove this contrdction, so we need some restrctions on OD.
798 <p>
799 This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself.
800 <p>
801
802 <hr/>
803 <h2><a name="content034"> HOD : Hereditarily Ordinal Definable</a></h2>
804 What we need is a bounded OD, the containment is limited by an ordinal.
805 <p>
806
807 <pre>
808 record HOD : Set (suc n) where
809 field
810 od : OD
811 odmax : Ordinal
812 &lt;odmax : {y : Ordinal} → def od y → y o&lt; odmax
813
814 </pre>
815 In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
816 <p>
817
818 <pre>
819 HOD = { x | TC x ⊆ OD }
820
821 </pre>
822 TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD.
823 <p>
824
825 <hr/>
826 <h2><a name="content035">1 to 1 mapping between an HOD and an Ordinal</a></h2>
827 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
828 <p>
829
830 <pre>
831 od→ord : HOD → Ordinal
832 ord→od : Ordinal → HOD
833 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x
834 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
835
836 </pre>
837 we can check an HOD is an element of the OD using def.
785 <p> 838 <p>
786 A ∋ x can be define as follows. 839 A ∋ x can be define as follows.
787 <p> 840 <p>
788 841
789 <pre> 842 <pre>
790 _∋_ : ( A x : OD ) → Set n 843 _∋_ : ( A x : HOD ) → Set n
791 _∋_ A x = def A ( od→ord x ) 844 _∋_ A x = def (od A) ( od→ord x )
792 845
793 </pre> 846 </pre>
794 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then 847 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
795 <p> 848 <p>
796 849
797 <pre> 850 <pre>
798 A x = def A ( od→ord x ) = ψ (od→ord x) 851 A x = def A ( od→ord x ) = ψ (od→ord x)
799
800 </pre>
801
802 <hr/>
803 <h2><a name="content034">1 to 1 mapping between an OD and an Ordinal</a></h2>
804
805 <p>
806
807 <pre>
808 od→ord : OD → Ordinal
809 ord→od : Ordinal → OD
810 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
811 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
812 852
813 </pre> 853 </pre>
814 They say the existing of the mappings can be proved in Classical Set Theory, but we 854 They say the existing of the mappings can be proved in Classical Set Theory, but we
815 simply assumes these non constructively. 855 simply assumes these non constructively.
816 <p> 856 <p>
817 We use postulate, it may contains additional restrictions which are not clear now. It look like the mapping should be a subset of Ordinals, but we don't explicitly
818 state it.
819 <p>
820 <img src="fig/ord-od-mapping.svg"> 857 <img src="fig/ord-od-mapping.svg">
821 858
822 <p> 859 <p>
823 860
824 <hr/> 861 <hr/>
825 <h2><a name="content035">Order preserving in the mapping of OD and Ordinal</a></h2> 862 <h2><a name="content036">Order preserving in the mapping of OD and Ordinal</a></h2>
826 Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ). 863 Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ).
827 <p> 864 <p>
828 865
829 <pre> 866 <pre>
830 def y ( od→ord x ) 867 def (od y) ( od→ord x )
831 868
832 </pre> 869 </pre>
833 An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements 870 An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements
834 have to be smaller than the corresponding ordinal of the containing OD. 871 have to be smaller than the corresponding ordinal of the containing OD.
835 <p> 872 We also assumes subset is always smaller. This is necessary to make a limit of Power Set.
836 873 <p>
837 <pre> 874
838 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y 875 <pre>
839 876 c&lt;→o&lt; : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y
840 </pre> 877 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; osuc (od→ord z)
841 This is also said to be provable in classical Set Theory, but we simply assumes it. 878
842 <p> 879 </pre>
843 OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋relation. This means the reverse order preservation, 880 If wa assumes reverse order preservation,
844 <p> 881 <p>
845 882
846 <pre> 883 <pre>
847 o&lt;→c&lt; : {n : Level} {x y : Ordinal } → x o&lt; y → def (ord→od y) x 884 o&lt;→c&lt; : {n : Level} {x y : Ordinal } → x o&lt; y → def (ord→od y) x
848 885
849 </pre> 886 </pre>
850 is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in 887 ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
851 the model.
852 <p> 888 <p>
853 <img src="fig/ODandOrdinals.svg"> 889 <img src="fig/ODandOrdinals.svg">
854 890
855 <p> 891 <p>
856 892
857 <hr/> 893 <hr/>
858 <h2><a name="content036">ISO</a></h2>
859 It also requires isomorphisms,
860 <p>
861
862 <pre>
863 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
864 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
865
866 </pre>
867
868 <hr/>
869 <h2><a name="content037">Various Sets</a></h2> 894 <h2><a name="content037">Various Sets</a></h2>
870
871 <p>
872 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. 895 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
873 <p> 896 <p>
874 897
875 <pre> 898 <pre>
876 Ordinal / things satisfies axiom of Ordinal / extension of natural number 899 Ordinal / things satisfies axiom of Ordinal / extension of natural number
877 V / hierarchical construction of Set from φ 900 V / hierarchical construction of Set from φ
878 L / hierarchical predicate definable construction of Set from φ 901 L / hierarchical predicate definable construction of Set from φ
902 HOD / Hereditarily Ordinal Definable
879 OD / equational formula on Ordinals 903 OD / equational formula on Ordinals
880 Agda Set / Type / it also has a level 904 Agda Set / Type / it also has a level
881 905
882 </pre> 906 </pre>
883 907
965 <h2><a name="content041">pair in OD</a></h2> 989 <h2><a name="content041">pair in OD</a></h2>
966 OD is an equation on Ordinals, we can simply write axiom of pair in the OD. 990 OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
967 <p> 991 <p>
968 992
969 <pre> 993 <pre>
970 _,_ : OD → OD → OD 994 _,_ : HOD → HOD → HOD
971 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } 995 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = ? ; &lt;odmax = ? }
972 996
973 </pre> 997 </pre>
998 It is easy to find out odmax from odmax of x and y.
999 <p>
974 ≡ is an equality of λ terms, but please not that this is equality on Ordinals. 1000 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
975 <p> 1001 <p>
976 1002
977 <hr/> 1003 <hr/>
978 <h2><a name="content042">Validity of Axiom of Pair</a></h2> 1004 <h2><a name="content042">Validity of Axiom of Pair</a></h2>
1047 field 1073 field
1048 eq→ : ∀ { x : Ordinal } → def a x → def b x 1074 eq→ : ∀ { x : Ordinal } → def a x → def b x
1049 eq← : ∀ { x : Ordinal } → def b x → def a x 1075 eq← : ∀ { x : Ordinal } → def b x → def a x
1050 1076
1051 </pre> 1077 </pre>
1052 Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B. 1078 Actually, (z : HOD) → (A ∋ z) ⇔ (B ∋ z) implies od A == od B.
1053 <p> 1079 <p>
1054 1080
1055 <pre> 1081 <pre>
1056 extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 1082 extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → od A == od B
1057 eq→ (extensionality0 {A} {B} eq ) {x} d = ? 1083 eq→ (extensionality0 {A} {B} eq ) {x} d = ?
1058 eq← (extensionality0 {A} {B} eq ) {x} d = ? 1084 eq← (extensionality0 {A} {B} eq ) {x} d = ?
1059 1085
1060 </pre> 1086 </pre>
1061 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) . 1087 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
1062 <p> 1088 <p>
1063 Actual proof is rather complicated. 1089 Actual proof is rather complicated.
1064 <p> 1090 <p>
1065 1091
1066 <pre> 1092 <pre>
1067 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 1093 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
1068 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 1094 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
1069 1095
1070 </pre> 1096 </pre>
1071 where 1097 where
1072 <p> 1098 <p>
1073 1099
1074 <pre> 1100 <pre>
1075 def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x 1101 odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y → (def A (od y) → def (od B) y) → def (od A) x → def (od B) x
1076 def-iso refl t = t 1102 odef-iso refl t = t
1077 1103
1078 </pre> 1104 </pre>
1079 1105
1080 <hr/> 1106 <hr/>
1081 <h2><a name="content044">Validity of Axiom of Extensionality</a></h2> 1107 <h2><a name="content044">Validity of Axiom of Extensionality</a></h2>
1082 1108
1083 <p> 1109 <p>
1084 If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes 1110 If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes
1085 <p> 1111 <p>
1086 1112
1087 <pre> 1113 <pre>
1088 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 1114 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
1089 1115
1090 </pre> 1116 </pre>
1091 Using this, we have 1117 Using this, we have
1092 <p> 1118 <p>
1093 1119
1094 <pre> 1120 <pre>
1095 extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) 1121 extensionality : {A B w : HOD } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
1096 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d 1122 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
1097 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 1123 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
1098 1124
1099 </pre> 1125 </pre>
1100 This assumption means we may have an equivalence set on any predicates.
1101 <p>
1102 1126
1103 <hr/> 1127 <hr/>
1104 <h2><a name="content045">Non constructive assumptions so far</a></h2> 1128 <h2><a name="content045">Non constructive assumptions so far</a></h2>
1105 We have correspondence between OD and Ordinals and one directional order preserving. 1129
1106 <p> 1130 <p>
1107 We also have equality assumption. 1131
1108 <p> 1132 <pre>
1109 1133 od→ord : HOD → Ordinal
1110 <pre> 1134 ord→od : Ordinal → HOD
1111 od→ord : OD → Ordinal 1135 c&lt;→o&lt; : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y
1112 ord→od : Ordinal → OD 1136 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; osuc (od→ord z)
1113 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x 1137 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x
1114 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 1138 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
1115 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y 1139 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y
1116 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 1140 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
1141 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 ψ
1117 1142
1118 </pre> 1143 </pre>
1119 1144
1120 <hr/> 1145 <hr/>
1121 <h2><a name="content046">Axiom which have negation form</a></h2> 1146 <h2><a name="content046">Axiom which have negation form</a></h2>
1599 <li><a href="#content021"> Can we do math in this way?</a> 1624 <li><a href="#content021"> Can we do math in this way?</a>
1600 <li><a href="#content022"> Things which Agda cannot prove</a> 1625 <li><a href="#content022"> Things which Agda cannot prove</a>
1601 <li><a href="#content023"> Classical story of ZF Set Theory</a> 1626 <li><a href="#content023"> Classical story of ZF Set Theory</a>
1602 <li><a href="#content024"> Ordinals</a> 1627 <li><a href="#content024"> Ordinals</a>
1603 <li><a href="#content025"> Axiom of Ordinals</a> 1628 <li><a href="#content025"> Axiom of Ordinals</a>
1604 <li><a href="#content026"> Concrete Ordinals</a> 1629 <li><a href="#content026"> Concrete Ordinals or Countable Ordinals</a>
1605 <li><a href="#content027"> Model of Ordinals</a> 1630 <li><a href="#content027"> Model of Ordinals</a>
1606 <li><a href="#content028"> Debugging axioms using Model</a> 1631 <li><a href="#content028"> Debugging axioms using Model</a>
1607 <li><a href="#content029"> Countable Ordinals can contains uncountable set?</a> 1632 <li><a href="#content029"> Countable Ordinals can contains uncountable set?</a>
1608 <li><a href="#content030"> What is Set</a> 1633 <li><a href="#content030"> What is Set</a>
1609 <li><a href="#content031"> We don't ask the contents of Set. It can be anything.</a> 1634 <li><a href="#content031"> We don't ask the contents of Set. It can be anything.</a>
1610 <li><a href="#content032"> Ordinal Definable Set</a> 1635 <li><a href="#content032"> Ordinal Definable Set</a>
1611 <li><a href="#content033"> ∋ in OD</a> 1636 <li><a href="#content033"> OD is not ZF Set</a>
1612 <li><a href="#content034"> 1 to 1 mapping between an OD and an Ordinal</a> 1637 <li><a href="#content034"> HOD : Hereditarily Ordinal Definable</a>
1613 <li><a href="#content035"> Order preserving in the mapping of OD and Ordinal</a> 1638 <li><a href="#content035"> 1 to 1 mapping between an HOD and an Ordinal</a>
1614 <li><a href="#content036"> ISO</a> 1639 <li><a href="#content036"> Order preserving in the mapping of OD and Ordinal</a>
1615 <li><a href="#content037"> Various Sets</a> 1640 <li><a href="#content037"> Various Sets</a>
1616 <li><a href="#content038"> Fixes on ZF to intuitionistic logic</a> 1641 <li><a href="#content038"> Fixes on ZF to intuitionistic logic</a>
1617 <li><a href="#content039"> Pure logical axioms</a> 1642 <li><a href="#content039"> Pure logical axioms</a>
1618 <li><a href="#content040"> Axiom of Pair</a> 1643 <li><a href="#content040"> Axiom of Pair</a>
1619 <li><a href="#content041"> pair in OD</a> 1644 <li><a href="#content041"> pair in OD</a>
1636 <li><a href="#content058"> Filter</a> 1661 <li><a href="#content058"> Filter</a>
1637 <li><a href="#content059"> Programming Mathematics</a> 1662 <li><a href="#content059"> Programming Mathematics</a>
1638 <li><a href="#content060"> link</a> 1663 <li><a href="#content060"> link</a>
1639 </ol> 1664 </ol>
1640 1665
1641 <hr/> Shinji KONO / Sat May 9 16:41:10 2020 1666 <hr/> Shinji KONO / Tue Jul 7 15:44:35 2020
1642 </body></html> 1667 </body></html>