Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff BAlgbra.agda @ 423:9984cdd88da3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Aug 2020 18:05:23 +0900 |
| parents | 44a484f17f26 |
| children | cc7909f86841 |
line wrap: on
line diff
--- a/BAlgbra.agda Sat Aug 01 11:06:29 2020 +0900 +++ b/BAlgbra.agda Sat Aug 01 18:05:23 2020 +0900 @@ -94,9 +94,9 @@ x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c +-sym : {a b : L } → a + b ≡ b + a -sym : {a b : L } → a x b ≡ b x a - -aab : {a b : L } → a + ( a x b ) ≡ a + +-aab : {a b : L } → a + ( a x b ) ≡ a x-aab : {a b : L } → a x ( a + b ) ≡ a - -dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c ) + +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c ) x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c ) a+0 : {a : L } → a + b0 ≡ a ax1 : {a : L } → a x b1 ≡ a