Mercurial > hg > Members > atton > agda > systemT
comparison int.agda @ 5:a3cf5cb2b7d3
Auto proof sum-assoc
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 May 2014 14:52:44 +0900 |
parents | 6b1230883bfa |
children | db4c6d435f23 |
comparison
equal
deleted
inserted
replaced
4:6b1230883bfa | 5:a3cf5cb2b7d3 |
---|---|
31 ≡⟨ sym (cong S (left-increment m n)) ⟩ | 31 ≡⟨ sym (cong S (left-increment m n)) ⟩ |
32 S ((S m) + n) | 32 S ((S m) + n) |
33 ≡⟨ refl ⟩ | 33 ≡⟨ refl ⟩ |
34 (S m) + (S n) | 34 (S m) + (S n) |
35 ∎ | 35 ∎ |
36 | |
37 sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z | |
38 sum-assoc O O O = refl | |
39 sum-assoc O O (S z) = cong S (sum-assoc O O z) | |
40 sum-assoc O (S y) O = refl | |
41 sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z) | |
42 sum-assoc (S x) O O = refl | |
43 sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z) | |
44 sum-assoc (S x) (S y) O = refl | |
45 sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z) |