Mercurial > hg > Members > kono > Proof > category
annotate system-t.agda @ 681:bd8f7346f252
fix Product and pullback
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Nov 2017 17:12:08 +0900 |
| parents | af321e38ecee |
| children |
| rev | line source |
|---|---|
| 315 | 1 module system-t where |
| 2 open import Relation.Binary.PropositionalEquality | |
| 3 | |
| 4 record _×_ ( U : Set ) ( V : Set ) : Set where | |
| 5 field | |
| 6 π1 : U | |
| 7 π2 : V | |
| 8 | |
| 346 | 9 <_,_> : {U V : Set} → U → V → U × V |
| 315 | 10 < u , v > = record {π1 = u ; π2 = v } |
| 11 | |
| 12 open _×_ | |
| 13 | |
| 14 postulate U : Set | |
| 15 postulate V : Set | |
| 16 | |
| 17 postulate v : V | |
| 18 postulate u : U | |
| 19 | |
| 346 | 20 f : U → V |
| 21 f = λ u → v | |
| 315 | 22 |
| 23 | |
| 24 UV : Set | |
| 25 UV = U × V | |
| 26 | |
| 27 uv : U × V | |
| 28 uv = < u , v > | |
| 29 | |
| 30 lemma01 : π1 < u , v > ≡ u | |
| 31 lemma01 = refl | |
| 32 | |
| 33 lemma02 : π2 < u , v > ≡ v | |
| 34 lemma02 = refl | |
| 35 | |
| 36 lemma03 : (uv : U × V ) → < π1 uv , π2 uv > ≡ uv | |
| 37 lemma03 uv = refl | |
| 38 | |
| 39 lemma04 : (λ x → f x ) u ≡ f u | |
| 40 lemma04 = refl | |
| 41 | |
| 42 lemma05 : (λ x → f x ) ≡ f | |
| 43 lemma05 = refl | |
| 44 | |
| 45 nn = λ (x : U ) → u | |
| 46 n1 = λ ( x : U ) → f x | |
| 47 | |
| 48 data Bool : Set where | |
| 49 T : Bool | |
| 50 F : Bool | |
| 51 | |
| 346 | 52 D : { U : Set } → U → U → Bool → U |
| 315 | 53 D u v T = u |
| 54 D u v F = v | |
| 55 | |
| 56 data Int : Set where | |
| 57 zero : Int | |
| 58 S : Int → Int | |
| 59 | |
| 346 | 60 pred : Int → Int |
| 315 | 61 pred zero = zero |
| 62 pred (S t) = t | |
| 63 | |
| 346 | 64 R : { U : Set } → U → ( U → Int → U ) → Int → U |
| 315 | 65 R u v zero = u |
| 66 R u v ( S t ) = v (R u v t) t | |
| 67 | |
| 346 | 68 null : Int → Bool |
| 315 | 69 null zero = T |
| 70 null (S _) = F | |
| 71 | |
| 346 | 72 It : { T : Set } → T → (T → T) → Int → T |
| 315 | 73 It u v zero = u |
| 74 It u v ( S t ) = v (It u v t ) | |
| 75 | |
| 346 | 76 R' : { T : Set } → T → ( T → Int → T ) → Int → T |
| 315 | 77 R' u v t = π1 ( It ( < u , zero > ) (λ x → < v (π1 x) (π2 x) , S (π2 x) > ) t ) |
| 78 | |
| 346 | 79 sum : Int → Int → Int |
| 80 sum x y = R y ( λ z → λ w → S z ) x | |
| 315 | 81 |
|
605
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
82 sum2 : Int → Int → Int |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
83 sum2 zero x = x |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
84 sum2 (S x) y = S ( sum2 x y ) |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
85 |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
86 cong1 : { x y : Int } -> ( f : Int -> Int ) -> x ≡ y -> f x ≡ f y |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
87 cong1 {x} {.x} f refl = refl |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
88 |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
89 lemma1 : ( x y : Int ) → sum x y ≡ sum2 x y |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
90 lemma1 zero y = refl |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
91 lemma1 (S x) y = cong1 ( λ z -> S z ) ( lemma1 x y ) |
|
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
92 |
| 346 | 93 mul : Int → Int → Int |
| 94 mul x y = R zero ( λ z → λ w → sum y z ) x | |
| 315 | 95 |
| 346 | 96 sum' : Int → Int → Int |
| 97 sum' x y = R' y ( λ z → λ w → S z ) x | |
| 315 | 98 |
| 346 | 99 mul' : Int → Int → Int |
| 100 mul' x y = R' zero ( λ z → λ w → sum y z ) x | |
| 315 | 101 |
| 346 | 102 fact : Int → Int |
| 103 fact n = R (S zero) (λ z → λ w → mul (S w) z ) n | |
| 315 | 104 |
| 346 | 105 fact' : Int → Int |
| 106 fact' n = R' (S zero) (λ z → λ w → mul (S w) z ) n | |
| 315 | 107 |
| 108 f3 = fact (S (S (S zero))) | |
| 109 f3' = fact' (S (S (S zero))) | |
| 110 | |
| 111 lemma21 : f3 ≡ f3' | |
| 112 lemma21 = refl | |
| 113 | |
| 346 | 114 lemma07 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → |
| 315 | 115 (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t )) ≡ t |
| 116 lemma07 u v zero = refl | |
| 346 | 117 lemma07 u v (S t) = cong ( λ x → S x ) ( lemma07 u v t ) |
| 315 | 118 |
| 346 | 119 lemma06 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → ( (R u v t) ≡ (R' u v t )) |
| 315 | 120 lemma06 u v zero = refl |
| 346 | 121 lemma06 u v (S t) = trans ( cong ( λ x → v x t ) ( lemma06 u v t ) ) |
| 122 ( cong ( λ y → v (R' u v t) y ) (sym ( lemma07 u v t ) ) ) | |
| 315 | 123 |
| 346 | 124 lemma08 : ( n m : Int ) → ( sum' n m ≡ sum n m ) |
| 315 | 125 lemma08 zero _ = refl |
| 346 | 126 lemma08 (S t) y = cong ( λ x → S x ) ( lemma08 t y ) |
| 315 | 127 |
| 346 | 128 lemma09 : ( n m : Int ) → ( mul' n m ≡ mul n m ) |
| 315 | 129 lemma09 zero _ = refl |
| 346 | 130 lemma09 (S t) y = cong ( λ x → sum y x) ( lemma09 t y ) |
| 315 | 131 |
| 346 | 132 lemma10 : ( n : Int ) → ( fact n ≡ fact n ) |
| 315 | 133 lemma10 zero = refl |
| 346 | 134 lemma10 (S t) = cong ( λ x → mul (S t) x ) ( lemma10 t ) |
| 315 | 135 |
| 346 | 136 lemma11 : ( n : Int ) → ( fact n ≡ fact' n ) |
| 137 lemma11 n = lemma06 (S zero) (λ z → λ w → mul (S w) z ) n | |
| 315 | 138 |
| 346 | 139 lemma06' : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → ( (R u v t) ≡ (R' u v t )) |
| 315 | 140 lemma06' u v zero = refl |
| 141 lemma06' u v (S t) = let open ≡-Reasoning in | |
| 142 begin | |
| 143 R u v (S t) | |
| 144 ≡⟨⟩ | |
| 145 v (R u v t) t | |
| 346 | 146 ≡⟨ cong (λ x → v x t ) ( lemma06' u v t ) ⟩ |
| 315 | 147 v (R' u v t) t |
| 346 | 148 ≡⟨ cong (λ x → v (R' u v t) x ) ( sym ( lemma07 u v t )) ⟩ |
| 315 | 149 v (R' u v t) (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t)) |
| 150 ≡⟨⟩ | |
| 151 R' u v (S t) | |
| 152 ∎ | |
| 153 | |
| 154 | |
| 346 | 155 sum1 : (x y : Int) → sum x (S y) ≡ S (sum x y ) |
| 156 sum1 zero y = refl | |
| 157 sum1 (S x) y = cong (λ x → S x ) (sum1 x y ) | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
158 |
| 346 | 159 sum-sym : (x y : Int) → sum x y ≡ sum y x |
| 160 sum-sym zero zero = refl | |
| 161 sum-sym zero (S t) = cong (λ x → S x )( sum-sym zero t) | |
| 162 sum-sym (S t) zero = cong (λ x → S x ) ( sum-sym t zero ) | |
| 163 sum-sym (S t) (S t') = let open ≡-Reasoning in | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
164 begin |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
165 sum (S t) (S t') |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
166 ≡⟨⟩ |
| 339 | 167 S (sum t (S t')) |
| 346 | 168 ≡⟨ cong ( λ x → S x ) ( sum1 t t') ⟩ |
| 339 | 169 S ( S (sum t t')) |
| 346 | 170 ≡⟨ cong ( λ x → S (S x ) ) ( sum-sym t t') ⟩ |
| 339 | 171 S ( S (sum t' t)) |
| 346 | 172 ≡⟨ sym ( cong ( λ x → S x ) ( sum1 t' t)) ⟩ |
| 339 | 173 S (sum t' (S t)) |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
174 ≡⟨⟩ |
| 346 | 175 R (S t) ( λ z → λ w → S z ) (S t') |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
176 ≡⟨⟩ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
177 sum (S t') (S t) |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
178 ∎ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
179 |
| 346 | 180 sum-assoc : (x y z : Int) → sum x (sum y z ) ≡ sum (sum x y) z |
| 181 sum-assoc zero y z = refl | |
| 182 sum-assoc (S x) y z = let open ≡-Reasoning in | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
183 begin |
| 339 | 184 sum (S x) ( sum y z ) |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
185 ≡⟨⟩ |
| 339 | 186 S ( sum x ( sum y z ) ) |
| 346 | 187 ≡⟨ cong (λ x → S x ) ( sum-assoc x y z) ⟩ |
| 339 | 188 S ( sum (sum x y) z ) |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
189 ≡⟨⟩ |
| 339 | 190 sum (S ( sum x y)) z |
| 191 ≡⟨⟩ | |
| 192 sum (sum (S x) y) z | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
193 ∎ |
| 315 | 194 |
| 346 | 195 mul-distr1 : (x y : Int) → mul x (S y) ≡ sum x ( mul x y ) |
| 196 mul-distr1 zero y = refl | |
| 197 mul-distr1 (S x) y = let open ≡-Reasoning in | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
198 begin |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
199 mul (S x) (S y) |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
200 ≡⟨⟩ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
201 sum (S y) (mul x (S y)) |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
202 ≡⟨⟩ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
203 S (sum y (mul x (S y) )) |
| 346 | 204 ≡⟨ cong (λ t → S ( sum y t )) (mul-distr1 x y ) ⟩ |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
205 S (sum y (sum x (mul x y))) |
| 346 | 206 ≡⟨ cong (λ x → S x ) ( |
| 339 | 207 begin |
| 208 sum y (sum x (mul x y)) | |
| 346 | 209 ≡⟨ sum-assoc y x (mul x y) ⟩ |
| 339 | 210 sum (sum y x) (mul x y) |
| 346 | 211 ≡⟨ cong (λ t → sum t (mul x y)) (sum-sym y x ) ⟩ |
| 339 | 212 sum (sum x y) (mul x y) |
| 346 | 213 ≡⟨ sym ( sum-assoc x y (mul x y)) ⟩ |
| 339 | 214 sum x (sum y (mul x y)) |
| 215 ∎ | |
| 216 ) ⟩ | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
217 S (sum x (sum y (mul x y) )) |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
218 ≡⟨⟩ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
219 S (sum x (mul (S x) y ) ) |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
220 ≡⟨⟩ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
221 sum (S x) (mul (S x) y) |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
222 ∎ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
223 |
| 346 | 224 mul-sym0 : (x : Int) → mul zero x ≡ mul x zero |
| 225 mul-sym0 zero = refl | |
| 226 mul-sym0 (S x) = mul-sym0 x | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
227 |
| 346 | 228 mul-sym : (x y : Int) → mul x y ≡ mul y x |
| 229 mul-sym zero x = mul-sym0 x | |
| 230 mul-sym (S x) y = let open ≡-Reasoning in | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
231 begin |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
232 mul (S x) y |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
233 ≡⟨⟩ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
234 sum y (mul x y ) |
| 346 | 235 ≡⟨ cong ( λ x → sum y x ) (mul-sym x y ) ⟩ |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
236 sum y (mul y x) |
| 346 | 237 ≡⟨ sym ( mul-distr1 y x ) ⟩ |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
238 mul y (S x) |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
239 ∎ |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
240 |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
241 |
| 346 | 242 mul-ditr : (y z w : Int) → sum (mul y z) ( mul w z ) ≡ mul (sum y w) z |
| 243 mul-ditr y zero w = let open ≡-Reasoning in | |
| 339 | 244 begin |
| 245 sum (mul y zero) ( mul w zero ) | |
| 346 | 246 ≡⟨ cong ( λ t → sum (mul y zero ) t ) (mul-sym w zero ) ⟩ |
| 339 | 247 sum (mul y zero ) ( mul zero w ) |
| 346 | 248 ≡⟨ cong ( λ t → sum t zero ) (mul-sym y zero ) ⟩ |
| 339 | 249 sum zero zero |
| 250 ≡⟨⟩ | |
| 251 mul zero (sum y w) | |
| 346 | 252 ≡⟨ mul-sym0 (sum y w) ⟩ |
| 339 | 253 mul (sum y w) zero |
| 254 ∎ | |
| 346 | 255 mul-ditr y (S z) w = let open ≡-Reasoning in |
| 339 | 256 begin |
| 257 sum (mul y (S z)) ( mul w (S z) ) | |
| 346 | 258 ≡⟨ cong ( λ t → sum t ( mul w (S z ))) (mul-distr1 y z) ⟩ |
| 339 | 259 sum ( sum y ( mul y z)) ( mul w (S z) ) |
| 346 | 260 ≡⟨ cong ( λ t → sum ( sum y ( mul y z)) t ) (mul-distr1 w z) ⟩ |
| 339 | 261 sum ( sum y ( mul y z)) ( sum w ( mul w z) ) |
| 346 | 262 ≡⟨ sym ( sum-assoc y (mul y z ) ( sum w ( mul w z) ) ) ⟩ |
| 339 | 263 sum y ( sum ( mul y z) ( sum w ( mul w z) )) |
| 346 | 264 ≡⟨ cong ( λ t → sum y t) (sum-sym ( mul y z) ( sum w ( mul w z) )) ⟩ |
| 339 | 265 sum y ( sum ( sum w ( mul w z) )( mul y z)) |
| 346 | 266 ≡⟨ sym ( cong ( λ t → sum y t) (sum-assoc w (mul w z) (mul y z )) ) ⟩ |
| 339 | 267 sum y ( sum w (sum ( mul w z) ( mul y z)) ) |
| 346 | 268 ≡⟨ cong ( λ t → sum y (sum w t) ) ( sum-sym (mul w z) (mul y z )) ⟩ |
| 339 | 269 sum y ( sum w (sum ( mul y z) ( mul w z)) ) |
| 346 | 270 ≡⟨ cong ( λ t → sum y (sum w t) ) ( mul-ditr y z w ) ⟩ |
| 339 | 271 sum y ( sum w (mul (sum y w) z) ) |
| 346 | 272 ≡⟨ sum-assoc y w (mul (sum y w) z) ⟩ |
| 339 | 273 sum (sum y w) ( mul (sum y w) z ) |
| 346 | 274 ≡⟨ sym ( mul-distr1 (sum y w) z ) ⟩ |
| 339 | 275 mul (sum y w) (S z) |
| 276 ∎ | |
| 277 | |
| 278 | |
| 346 | 279 mul-assoc : (x y z : Int) → mul x (mul y z ) ≡ mul (mul x y) z |
| 280 mul-assoc zero y z = refl | |
| 281 mul-assoc (S x) y z = let open ≡-Reasoning in | |
| 339 | 282 begin |
| 283 mul (S x) (mul y z ) | |
| 284 ≡⟨⟩ | |
| 285 sum (mul y z) ( mul x ( mul y z ) ) | |
| 346 | 286 ≡⟨ cong (λ t → sum (mul y z) t ) (mul-assoc x y z ) ⟩ |
| 339 | 287 sum (mul y z) ( mul ( mul x y) z ) |
| 346 | 288 ≡⟨ mul-ditr y z (mul x y) ⟩ |
| 339 | 289 mul (sum y (mul x y)) z |
| 290 ≡⟨⟩ | |
| 291 mul (mul (S x) y) z | |
| 292 ∎ | |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
293 |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
294 |
|
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
295 |
| 339 | 296 |