--- a/agda/chap0.agda	Wed Oct 16 23:16:27 2019 +0900
+++ b/agda/chap0.agda	Thu Oct 17 15:11:39 2019 +0900
@@ -2,7 +2,7 @@
 
 open import Data.List
 open import Data.Nat hiding (_⊔_)
-open import Data.Integer hiding (_⊔_ ;  _≟_ ; _+_ )
+-- open import Data.Integer hiding (_⊔_ ;  _≟_ ; _+_ )
 open import Data.Product
 
 A : List ℕ
@@ -44,6 +44,14 @@
 
 open import Data.Nat.DivMod
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat.Properties
+
+-- _%_ : ℕ → ℕ → ℕ
+-- _%_ a b with <-cmp a b
+-- _%_ a b | tri< a₁ ¬b ¬c = a
+-- _%_ a b | tri≈ ¬a b₁ ¬c = 0
+-- _%_ a b | tri> ¬a ¬b c = _%_ (a - b) b
 
 _≡7_ : ℕ → ℕ → Set
 n ≡7 m = (n % 7) ≡ (m % 7 )
@@ -143,11 +151,47 @@
 dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
 dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
 
+open import Function
+
+lemma4 : ¬ ( dag ( edge graph012a)  )
+lemma4 neg = neg 1 $ indirect 2 refl $ indirect 3 refl $ indirect 4 refl $ indirect 5 refl $ direct refl 
+
 dgree : List ( ℕ × ℕ ) → ℕ → ℕ 
 dgree [] _ = 0
-dgree ((e , e1) ∷ t)  e0 with e0 ≟ e | e0 ≟ e1
+dgree ((e , e1) ∷ t) e0 with e0 ≟ e | e0 ≟ e1
 dgree ((e , e1) ∷ t) e0 | yes _ | _ = 1 + (dgree t e0)
 dgree ((e , e1) ∷ t) e0 | _ | yes p = 1 + (dgree t e0)
 dgree ((e , e1) ∷ t) e0 | no _ | no _ = dgree t e0
 
+dgree-c : {t : Set} → List ( ℕ × ℕ ) → ℕ → (ℕ → t)  → t 
+dgree-c {t} [] e0 next = next 0
+dgree-c {t} ((e , e1) ∷ tail ) e0 next with e0 ≟ e | e0 ≟ e1
+... | yes _ | _ = dgree-c tail e0 ( λ n → next (n + 1 ))
+... | _ | yes _ = dgree-c tail e0 ( λ n → next (n + 1 ))
+... | no _ | no _ = dgree-c tail e0 next
+
 lemma6 = dgree list012a 2
+lemma7 = dgree-c list012a 2 ( λ n → n )
+
+even2 : (n : ℕ ) → n % 2 ≡ 0 → (n + 2) % 2 ≡ 0 
+even2 0 refl = refl
+even2 1 () 
+even2 (suc (suc n)) eq = trans ([a+n]%n≡a%n n _) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
+
+sum-of-dgree : ( g : List ( ℕ × ℕ )) → ℕ
+sum-of-dgree [] = 0
+sum-of-dgree ((e , e1) ∷ t) = 2 + sum-of-dgree t
+
+dgree-even : ( g : List ( ℕ × ℕ )) → sum-of-dgree g % 2 ≡ 0
+dgree-even [] = refl
+dgree-even ((e , e1) ∷ t) with dgree-even t
+... | s = subst (λ k → k % 2 ≡ 0 ) (sym lemma)( even2 (sum-of-dgree t) s ) where
+   lemma : sum-of-dgree ((e , e1) ∷ t) ≡ sum-of-dgree t + 2
+   lemma = begin
+         sum-of-dgree ((e , e1) ∷ t)
+      ≡⟨⟩
+         2 + sum-of-dgree t 
+      ≡⟨ +-comm 2 _ ⟩
+         sum-of-dgree t + 2
+     ∎ where open ≡-Reasoning
+