Members/atton/delta_monad: agda/delta.agda annotate

annotate agda/delta.agda @ 60:73bb981cb1c6

Expand pattern-matches...

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Sat, 22 Nov 2014 18:31:33 +0900
parents	46b15f368905
children	0f308ddd6136

rev	line source
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	1 open import list
28 6e6d646d7722 Split basic functions to file Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 27 diff changeset	2 open import basic
29 e0ba1bf564dd Apply level to some functions Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 28 diff changeset	3
e0ba1bf564dd Apply level to some functions Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 28 diff changeset	4 open import Level
27 742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	5 open import Relation.Binary.PropositionalEquality
742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	6 open ≡-Reasoning
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	7
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	8 module delta where
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	9
54 9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	10
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	11 data Delta {l : Level} (A : Set l) : (Set (suc l)) where
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	12 mono : A -> Delta A
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	13 delta : A -> Delta A -> Delta A
54 9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	14
9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	15 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	16 deltaAppend (mono x) d = delta x d
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	17 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
54 9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	18
9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	19 headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	20 headDelta (mono x) = mono x
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	21 headDelta (delta x _) = mono x
54 9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	22
9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	23 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	24 tailDelta (mono x) = mono x
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	25 tailDelta (delta _ d) = d
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	26
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	27
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	28 -- Functor
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	29 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	30 fmap f (mono x) = mono (f x)
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	31 fmap f (delta x d) = delta (f x) (fmap f d)
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	32
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	33
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	34
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	35 -- Monad (Category)
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	36 eta : {l : Level} {A : Set l} -> A -> Delta A
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	37 eta x = mono x
27 742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	38
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	39 bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	40 bind (mono x) f = f x
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	41 bind (delta x d) f = deltaAppend (headDelta (f x)) (bind d (tailDelta ∙ f))
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	42
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	43 -- can not apply id. because different Level
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	44 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	45 mu d = bind d id
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	46
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	47
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	48 returnS : {l : Level} {A : Set l} -> A -> Delta A
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	49 returnS x = mono x
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	50
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	51 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	52 returnSS x y = deltaAppend (returnS x) (returnS y)
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	53
33 0bc402f970b3 Proof Monad-law 1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 32 diff changeset	54
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	55 -- Monad (Haskell)
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	56 return : {l : Level} {A : Set l} -> A -> Delta A
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	57 return = eta
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	58
41 23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	59 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	60 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	61 (mono x) >>= f = f x
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	62 (delta x d) >>= f = deltaAppend (headDelta (f x)) (d >>= (tailDelta ∙ f))
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	63
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	64
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	65
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	66 -- proofs
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	67
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	68
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	69 -- Functor-laws
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	70
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	71 -- Functor-law-1 : T(id) = id'
55 9c8c09334e32 Redefine Delta for infinite changes in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 54 diff changeset	72 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	73 functor-law-1 (mono x) = refl
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	74 functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	75
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	76 -- Functor-law-2 : T(f . g) = T(f) . T(g)
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	77 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
55 9c8c09334e32 Redefine Delta for infinite changes in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 54 diff changeset	78 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
9c8c09334e32 Redefine Delta for infinite changes in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 54 diff changeset	79 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	80 functor-law-2 f g (mono x) = refl
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	81 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	82
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	83
56 bfb6be9a689d Trying redefine monad-laws-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 55 diff changeset	84
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	85 -- Monad-laws (Category)
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	86
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	87 -- monad-law-1 : join . fmap join = join . join
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	88 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	89 monad-law-1 (mono d) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	90 monad-law-1 (delta (mono (mono x)) (mono (mono (mono x₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	91 monad-law-1 (delta (mono (delta x x₁)) (mono (mono (mono x₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	92 monad-law-1 (delta (delta (mono x) (mono x₁)) (mono (mono (mono x₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	93 monad-law-1 (delta (delta (delta x x₁) (mono x₂)) (mono (mono (mono x₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	94 monad-law-1 (delta (delta (mono x) (delta (mono x₁) x₂)) (mono (mono (mono x₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	95 monad-law-1 (delta (delta (delta x x₁) (delta (mono x₂) x₃)) (mono (mono (mono x₄)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	96 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (mono (mono x₃)))) (mono (mono (mono x₄)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	97 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (mono x₃)) (mono (mono x₄)))) (mono (mono (mono x₅)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	98 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (mono x₃))) (mono (mono x₄)))) (mono (mono (mono x₅)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	99 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (mono x₄))) (mono (mono x₅)))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	100 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (mono x₄)))) (mono (mono x₅)))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	101 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (mono (mono x₆)))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	102 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))) (mono (mono x₆)))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	103 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (mono (mono x₇)))) (mono (mono (mono x₈)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	104 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ x₆))))) (mono (mono x₇)))) (mono (mono (mono x₈)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	105 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ x₇))))) (mono (mono x₈)))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	106 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (mono (delta x₃ (mono x₄))))) (mono (mono (mono x₅)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	107 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (mono x₃)) (mono (delta x₄ (mono x₅))))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	108 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ x₃)) (mono (delta x₄ (mono x₅))))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	109 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ x₄)) (mono (delta x₅ (mono x₆))))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	110 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (mono (delta x₃ (delta x₄ (mono x₅)))))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	111 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (mono x₃)) (mono (delta x₄ (delta x₅ (mono x₆)))))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	112 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (mono x₃))) (mono (delta x₄ (delta x₅ (mono x₆)))))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	113 monad-law-1 (delta (delta (delta x (mono x₁)) (delta (delta x₂ (delta x₃ (mono x₄))) (mono (delta x₅ (delta x₆ (mono x₇)))))) (mono (mono (mono x₈)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	114 monad-law-1 (delta (delta (delta x (delta x₁ x₂)) (delta (delta x₃ (delta x₄ (mono x₅))) (mono (delta x₆ (delta x₇ (mono x₈)))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	115 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (mono x₄)))) (mono (delta x₅ (delta x₆ (mono x₇)))))) (mono (mono (mono x₈)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	116 monad-law-1 (delta (delta (delta x (mono x₁)) (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (mono (delta x₆ (delta x₇ (mono x₈)))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	117 monad-law-1 (delta (delta (delta x (delta x₁ x₂)) (delta (delta x₃ (delta x₄ (delta x₅ (mono x₆)))) (mono (delta x₇ (delta x₈ (mono x₉)))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	118 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))) (mono (delta x₆ (delta x₇ (mono x₈)))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	119 monad-law-1 (delta (delta (delta x (mono x₁)) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (mono (delta x₇ (delta x₈ (mono x₉)))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	120 monad-law-1 (delta (delta (delta x (delta x₁ x₂)) (delta (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇))))) (mono (delta x₈ (delta x₉ (mono x₁₀)))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	121 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆)))))) (mono (delta x₇ (delta x₈ (mono x₉)))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	122 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (mono (delta x₈ (delta x₉ (mono x₁₀)))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	123 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇))))))) (mono (delta x₈ (delta x₉ (mono x₁₀)))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	124 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (mono (delta x₉ (delta x₁₀ (mono x₁₁)))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	125 -- x (Delta A)... x7
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	126 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ x₈))))))) (mono (delta x₉ (delta x₁₀ (mono x₁₁)))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	127 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ x₉))))))) (mono (delta x₁₀ (delta x₁₁ (mono x₁₂)))))) (mono (mono (mono x₁₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	128 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (mono (delta x₃ (delta x₄ (delta x₅ (mono x₆))))))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	129 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (mono x₃)) (mono (delta x₄ (delta x₅ (delta x₆ (mono x₇))))))) (mono (mono (mono x₈)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	130 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (mono x₃))) (mono (delta x₄ (delta x₅ (delta x₆ (mono x₇))))))) (mono (mono (mono x₈)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	131 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (mono x₄))) (mono (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	132 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (mono x₄)))) (mono (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	133 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (mono (delta x₆ (delta x₇ (delta x₈ (mono x₉))))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	134 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))) (mono (delta x₆ (delta x₇ (delta x₈ (mono x₉))))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	135 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (mono (delta x₇ (delta x₈ (delta x₉ (mono x₁₀))))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	136 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆)))))) (mono (delta x₇ (delta x₈ (delta x₉ (mono x₁₀))))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	137 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (mono (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁))))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	138 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇))))))) (mono (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁))))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	139 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (mono (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂))))))) (mono (mono (mono x₁₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	140 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ x₈))))))) (mono (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂))))))) (mono (mono (mono x₁₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	141 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ x₉))))))) (mono (delta x₁₀ (delta x₁₁ (delta x₁₂ (mono x₁₃))))))) (mono (mono (mono x₁₄)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	142 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (mono (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))))) (mono (mono (mono x₈)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	143 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (mono x₃)) (mono (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈)))))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	144 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (mono x₃))) (mono (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈)))))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	145 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (mono x₄))) (mono (delta x₅ (delta x₆ (delta x₇ (delta x₈ (mono x₉)))))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	146 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (mono x₄)))) (mono (delta x₅ (delta x₆ (delta x₇ (delta x₈ (mono x₉)))))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	147 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (mono (delta x₆ (delta x₇ (delta x₈ (delta x₉ (mono x₁₀)))))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	148 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))) (mono (delta x₆ (delta x₇ (delta x₈ (delta x₉ (mono x₁₀)))))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	149 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (mono (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁)))))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	150 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆)))))) (mono (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁)))))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	151 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (mono (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂)))))))) (mono (mono (mono x₁₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	152 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇))))))) (mono (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂)))))))) (mono (mono (mono x₁₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	153 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (mono (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (mono x₁₃)))))))) (mono (mono (mono x₁₄)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	154 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ x₈))))))) (mono (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (mono x₁₃)))))))) (mono (mono (mono x₁₄)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	155 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ x₉))))))) (mono (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (mono x₁₄)))))))) (mono (mono (mono x₁₅)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	156 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (mono (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ x₈)))))))) (mono (mono (mono x₉)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	157 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (mono x₃)) (mono (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ x₉)))))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	158 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (mono x₃))) (mono (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ x₉)))))))) (mono (mono (mono x₁₀)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	159 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (mono x₄))) (mono (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ x₁₀)))))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	160 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (mono x₄)))) (mono (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ x₁₀)))))))) (mono (mono (mono x₁₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	161 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (mono (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ x₁₁)))))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	162 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))) (mono (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ x₁₁)))))))) (mono (mono (mono x₁₂)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	163 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (mono (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ x₁₂)))))))) (mono (mono (mono x₁₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	164 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆)))))) (mono (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ x₁₂)))))))) (mono (mono (mono x₁₃)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	165 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (mono (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ x₁₃)))))))) (mono (mono (mono x₁₄)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	166 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇))))))) (mono (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ x₁₃)))))))) (mono (mono (mono x₁₄)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	167 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (mono (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ x₁₄)))))))) (mono (mono (mono x₁₅)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	168 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ x₈))))))) (mono (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ x₁₄)))))))) (mono (mono (mono x₁₅)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	169 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ x₉))))))) (mono (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ x₁₅)))))))) (mono (mono (mono x₁₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	170 -- 0, 2
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	171 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (delta (mono x₃) (mono (mono x₄))))) (mono (mono (mono x₅)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	172 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (delta (mono x₃) (mono (delta x₄ (mono x₅)))))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	173 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (delta (mono x₃) (mono (delta x₄ (delta x₅ x₆)))))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	174 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (delta (mono x₃) (delta x₄ (mono x₅))))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	175 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (delta (mono x₃) (delta x₄ (delta x₅ x₆))))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	176 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (delta (delta x₃ x₄) (mono x₅)))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	177 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (mono x₂)) (delta (delta x₃ x₄) (delta x₅ x₆)))) (mono (mono (mono x₇)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	178 monad-law-1 (delta (delta (mono x) (delta (delta x₁ (delta x₂ x₃)) (delta x₄ x₅))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	179 monad-law-1 (delta (delta (delta x x₁) (delta (delta x₂ x₃) (delta x₄ x₅))) (mono (mono (mono x₆)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	180 monad-law-1 (delta (mono x) (mono (mono (delta x₁ d)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	181 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (mono (mono (delta x₂ (mono x₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	182 monad-law-1 (delta (delta (delta x x₁) (mono (mono x₂))) (mono (mono (delta x₃ (mono x₄))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	183 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (mono (mono (delta x₃ (mono x₄))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	184 monad-law-1 (delta (delta (delta x x₁) (mono (delta x₂ (mono x₃)))) (mono (mono (delta x₄ (mono x₅))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	185 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ x₃)))) (mono (mono (delta x₄ (mono x₅))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	186 monad-law-1 (delta (delta (delta x x₁) (mono (delta x₂ (delta x₃ x₄)))) (mono (mono (delta x₅ (mono x₆))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	187 monad-law-1 (delta (delta (mono x) (mono x₁)) (mono (mono (delta x₂ (delta x₃ d))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	188 monad-law-1 (delta (delta (delta x x₁) (mono x₂)) (mono (mono (delta x₃ (delta x₄ d))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	189 monad-law-1 (delta (delta (mono x) (delta x₁ (mono x₂))) (mono (mono (delta x₃ d)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	190 monad-law-1 (delta (delta (delta x x₁) (delta x₂ (mono x₃))) (mono (mono (delta x₄ d)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	191 monad-law-1 (delta (delta (mono x) (delta x₁ (delta x₂ x₃))) (mono (mono (delta x₄ d)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	192 monad-law-1 (delta (delta (delta x x₁) (delta x₂ (delta x₃ x₄))) (mono (mono (delta x₅ d)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	193 monad-law-1 (delta (mono (mono x)) (mono (delta (mono x₁) d₁))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	194 monad-law-1 (delta (mono (mono x)) (mono (delta (delta x₁ d) d₁))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	195 monad-law-1 (delta (mono (delta x (mono x₁))) (mono (delta (mono x₂) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	196 monad-law-1 (delta (mono (delta x (mono x₁))) (mono (delta (delta x₂ d) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	197 monad-law-1 (delta (mono (delta x (delta x₁ x₂))) (mono (delta (mono x₃) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	198 monad-law-1 (delta (mono (delta x (delta x₁ x₂))) (mono (delta (delta x₃ d) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	199 monad-law-1 (delta (mono (delta x x₁)) (mono (delta (mono x₂) (delta d₁ (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	200 monad-law-1 (delta (mono (delta x x₁)) (mono (delta (delta x₂ d) (delta d₁ (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	201 monad-law-1 (delta (mono (delta x x₁)) (mono (delta (mono x₂) (delta d₁ (delta d₂ (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	202 monad-law-1 (delta (mono (delta x x₁)) (mono (delta (delta x₂ d) (delta d₁ (delta d₂ (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	203 monad-law-1 (delta (mono (delta x (mono x₁))) (mono (delta (mono x₂) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	204 monad-law-1 (delta (mono (delta x (mono x₁))) (mono (delta (delta x₂ d) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	205 monad-law-1 (delta (mono (delta x (delta x₁ (mono x₂)))) (mono (delta (mono x₃) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	206 monad-law-1 (delta (mono (delta x (delta x₁ (mono x₂)))) (mono (delta (delta x₃ d) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	207 monad-law-1 (delta (mono (delta x (delta x₁ (delta x₂ (mono x₃))))) (mono (delta (mono x₄) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	208 monad-law-1 (delta (mono (delta x (delta x₁ (delta x₂ (mono x₃))))) (mono (delta (delta x₄ d) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	209 monad-law-1 (delta (mono (delta x (delta x₁ (delta x₂ (delta x₃ x₄))))) (mono (delta (mono x₅) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	210 monad-law-1 (delta (mono (delta x (delta x₁ (delta x₂ (delta x₃ x₄))))) (mono (delta (delta x₅ d) (delta d₁ (delta d₂ (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	211 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (mono (delta (mono x₂) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	212 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (mono (delta (delta x₂ d) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	213 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (mono (delta (mono x₃) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	214 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (mono (delta (delta x₃ d) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	215 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (mono (delta (mono x₄) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	216 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (mono (delta (delta x₄ d) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	217 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (mono x₄)))))) (mono (delta (mono x₅) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	218 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (mono x₄)))))) (mono (delta (delta x₅ d) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	219 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ x₅)))))) (mono (delta (mono x₆) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	220 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ x₅)))))) (mono (delta (delta x₆ d) (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	221 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (mono (delta (mono x₂) (delta d₁ (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	222 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (mono (delta (delta x₂ d) (delta d₁ (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	223 monad-law-1 (delta (delta (mono x) (mono (delta x₁ x₂))) (mono (delta (mono x₃) (delta d₁ (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	224 monad-law-1 (delta (delta (mono x) (mono (delta x₁ x₂))) (mono (delta (delta x₃ d) (delta d₁ (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	225 monad-law-1 (delta (delta (mono x) (mono x₁)) (mono (delta (mono x₂) (delta d₁ (delta d₂ d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	226 monad-law-1 (delta (delta (mono x) (mono x₁)) (mono (delta (delta x₂ d) (delta d₁ (delta d₂ d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	227 monad-law-1 (delta (delta (mono x) (delta x₁ x₂)) (mono (delta (mono x₃) d₁))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	228 monad-law-1 (delta (delta (mono x) (delta x₁ x₂)) (mono (delta (delta x₃ d) d₁))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	229 monad-law-1 (delta (delta (delta x x₁) x₂) (mono (delta (mono x₃) d₁))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	230 monad-law-1 (delta (delta (delta x x₁) x₂) (mono (delta (delta x₃ d) d₁))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	231 --
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	232 monad-law-1 (delta (mono x) (delta (mono (mono x₁)) (mono (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	233 monad-law-1 (delta (delta (mono x) (mono x₁)) (delta (mono (mono x₂)) (mono (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	234 monad-law-1 (delta (delta (delta x x₁) (mono x₂)) (delta (mono (mono x₃)) (mono (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	235 monad-law-1 (delta (delta (mono x) (delta x₁ x₂)) (delta (mono (mono x₃)) (mono (mono d₁)))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	236 monad-law-1 (delta (delta (delta x x₁) (delta x₂ x₃)) (delta (mono (mono x₄)) (mono (mono d₁)))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	237 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (mono x₂) (mono d₂))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	238 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (mono x₂) (delta (mono x₃) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	239 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (mono x₂) (delta (delta x₃ (mono x₄)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	240 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (mono x₂) (delta (delta x₃ (delta x₄ d₂)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	241 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (mono x₃)) (mono d₂))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	242 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (mono x₃)) (delta (mono x₄) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	243 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (mono x₃)) (delta (delta x₄ (mono x₅)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	244 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (mono x₃)) (delta (delta x₄ (delta x₅ d₂)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	245 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (mono x₄))) (mono d₂))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	246 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (mono x₄))) (delta (mono x₅) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	247 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (mono x₄))) (delta (delta x₅ (mono x₆)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	248 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (mono x₄))) (delta (delta x₅ (delta x₆ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	249 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	250 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (delta (mono x₆) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	251 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (delta (delta x₆ (mono x₇)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	252 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (mono x₅)))) (delta (delta x₆ (delta x₇ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	253 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	254 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (delta (mono x₇) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	255 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (delta (delta x₇ (mono x₈)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	256 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆))))) (delta (delta x₇ (delta x₈ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	257 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	258 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (mono x₈) (mono (mono x₉))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	259 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (mono x₉)) (mono (mono x₁₀))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	260 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (delta x₉ d₂)) (mono (mono x₁₀))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	261 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (mono x₈) (mono (delta x₉ d₃))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	262 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (mono x₉)) (mono (delta x₁₀ (mono x₁₁)))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	263 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (delta x₉ d₂)) (mono (delta x₁₀ (mono x₁₁)))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	264 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (mono x₉)) (mono (delta x₁₀ (delta x₁₁ d₃)))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	265 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (delta x₉ d₂)) (mono (delta x₁₀ (delta x₁₁ d₃)))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	266 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (mono x₈) (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	267 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (mono x₉)) (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	268 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (mono x₇)))))) (delta (delta x₈ (delta x₉ d₂)) (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	269 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	270 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (mono x₉) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	271 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (mono x₁₀)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	272 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (delta x₁₀ d₂)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	273 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (mono x₁₀)) (delta d₃ (mono d₄))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	274 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (delta x₁₀ d₂)) (delta d₃ (mono d₄))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	275 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (mono x₁₀)) (delta (mono x₁₁) (delta (mono x₁₂) (mono (mono x₁₃))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	276 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (delta x₁₀ d₂)) (delta (mono x₁₁) (delta (mono x₁₂) (mono (mono x₁₃))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	277 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (mono x₁₀)) (delta (delta x₁₁ d₃) (delta (mono x₁₂) (mono (mono x₁₃))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	278 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (delta x₁₀ d₂)) (delta (delta x₁₁ d₃) (delta (mono x₁₂) (mono (mono x₁₃))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	279 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (mono x₁₀)) (delta d₃ (delta (delta x₁₁ d₄) (mono (mono x₁₂))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	280 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (delta x₁₀ d₂)) (delta d₃ (delta (delta x₁₁ d₄) (mono (mono x₁₂))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	281 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (mono x₁₀)) (delta d₃ (delta d₄ (mono (delta x₁₁ d₅))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	282 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (delta x₁₀ d₂)) (delta d₃ (delta d₄ (mono (delta x₁₁ d₅))))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	283 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (mono x₁₀)) (delta d₃ (delta d₄ (delta d₅ d₆)))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	284 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (mono x₈))))))) (delta (delta x₉ (delta x₁₀ d₂)) (delta d₃ (delta d₄ (delta d₅ d₆)))))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	285 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (mono x₉)))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	286 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (mono x₉)))))))) (delta (mono x₁₀) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	287 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (mono x₉)))))))) (delta (delta x₁₀ (mono x₁₁)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	288 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (mono x₉)))))))) (delta (delta x₁₀ (delta x₁₁ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	289 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (mono x₁₀))))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	290 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (mono x₁₀))))))))) (delta (mono x₁₁) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	291 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (mono x₁₀))))))))) (delta (delta x₁₁ (mono x₁₂)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	292 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (mono x₁₀))))))))) (delta (delta x₁₁ (delta x₁₂ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	293 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁)))))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	294 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁)))))))))) (delta (mono x₁₂) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	295 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁)))))))))) (delta (delta x₁₂ (mono x₁₃)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	296 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (mono x₁₁)))))))))) (delta (delta x₁₂ (delta x₁₃ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	297 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂))))))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	298 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂))))))))))) (delta (mono x₁₃) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	299 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂))))))))))) (delta (delta x₁₃ (mono x₁₄)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	300 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (mono x₁₂))))))))))) (delta (delta x₁₃ (delta x₁₄ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	301 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (mono x₁₃)))))))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	302 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (mono x₁₃)))))))))))) (delta (mono x₁₄) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	303 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (mono x₁₃)))))))))))) (delta (delta x₁₄ (mono x₁₅)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	304 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (mono x₁₃)))))))))))) (delta (delta x₁₄ (delta x₁₅ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	305 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (mono x₁₄))))))))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	306 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (mono x₁₄))))))))))))) (delta (mono x₁₅) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	307 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (mono x₁₄))))))))))))) (delta (delta x₁₅ (mono x₁₆)) d₃))))) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	308 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (mono x₁₄))))))))))))) (delta (delta x₁₅ (delta x₁₆ d₂)) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	309 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ d₁))))))))))))) (mono d₂))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	310 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ d₁))))))))))))) (delta (mono x₁₅) d₃))))) = refl
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	311 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (mono x₁₅)))))))))))))) (delta (delta x₁₆ (mono x₁₇)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	312 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (mono x₁₅)))))))))))))) (delta (delta x₁₆ (delta x₁₇ d₂)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	313 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ (mono x₁₆))))))))))))))) (delta (delta x₁₇ (mono x₁₈)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	314 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ (mono x₁₆))))))))))))))) (delta (delta x₁₇ (delta x₁₈ d₂)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	315 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ (delta x₁₆ (mono x₁₇)))))))))))))))) (delta (delta x₁₈ (mono x₁₉)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	316 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ (delta x₁₆ (mono x₁₇)))))))))))))))) (delta (delta x₁₈ (delta x₁₉ d₂)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	317 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ (delta x₁₆ (delta x₁₇ d₁)))))))))))))))) (delta (delta x₁₈ (mono x₁₉)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	318 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ (delta x₁₆ (delta x₁₇ d₁)))))))))))))))) (delta (delta x₁₈ (delta x₁₉ d₂)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	319 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (mono x₁₅)))))))))))))) (delta (delta x₁₆ (mono x₁₇)) (delta (mono x₁₈) d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	320 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (mono x₁₅)))))))))))))) (delta (delta x₁₆ (delta x₁₇ d₂)) (delta (mono x₁₈) d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	321 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (mono x₁₅)))))))))))))) (delta (delta x₁₆ (mono x₁₇)) (delta (delta x₁₈ d₃) d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	322 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (mono x₁₅)))))))))))))) (delta (delta x₁₆ (delta x₁₇ d₂)) (delta (delta x₁₈ d₃) d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	323 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ d₁)))))))))))))) (delta (delta x₁₆ (mono x₁₇)) (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	324 monad-law-1 (delta (mono (mono x)) (delta (mono (mono x₁)) (mono (delta (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ (delta x₇ (delta x₈ (delta x₉ (delta x₁₀ (delta x₁₁ (delta x₁₂ (delta x₁₃ (delta x₁₄ (delta x₁₅ d₁)))))))))))))) (delta (delta x₁₆ (delta x₁₇ d₂)) (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	325 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (mono x₃) (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	326 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (mono x₃) (delta (mono x₄) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	327 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (mono x₃) (delta (delta x₄ (mono x₅)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	328 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (mono x₃) (delta (delta x₄ (delta x₅ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	329 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ d₁) (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	330 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (mono x₅) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	331 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (delta x₅ (mono x₆)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	332 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (delta x₅ (delta x₆ d₂)) (mono d₃)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	333 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (delta x₅ (mono x₆)) (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	334 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (delta x₅ (delta x₆ d₂)) (delta d₃ d₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	335 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (delta x₄ (mono x₅))) (delta (mono x₆) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	336 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (delta x₄ (mono x₅))) (delta (delta x₆ (mono x₇)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	337 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (delta x₄ (mono x₅))) (delta (delta x₆ (delta x₇ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	338 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (delta x₄ (delta x₅ d₁))) (delta (mono x₆) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	339 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (delta x₄ (delta x₅ d₁))) (delta (delta x₆ (mono x₇)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	340 monad-law-1 (delta (mono (delta x x₁)) (delta (mono (mono x₂)) (mono (delta (delta x₃ (delta x₄ (delta x₅ d₁))) (delta (delta x₆ (delta x₇ d₂)) d₃))))) = refl
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	341 --
60 73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	342 monad-law-1 (delta (delta (mono x) (mono x₁)) (delta (mono (mono x₂)) (mono (delta (mono x₃) (mono (mono x₄)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	343 monad-law-1 (delta (delta (delta x x₁) (mono x₂)) (delta (mono (mono x₃)) (mono (delta (mono x₄) (mono (mono x₅)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	344 monad-law-1 (delta (delta (mono x) (delta x₁ (mono x₂))) (delta (mono (mono x₃)) (mono (delta (mono x₄) (mono (mono x₅)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	345 monad-law-1 (delta (delta (delta x x₁) (delta x₂ (mono x₃))) (delta (mono (mono x₄)) (mono (delta (mono x₅) (mono (mono x₆)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	346 monad-law-1 (delta (delta (mono x) (delta x₁ (delta x₂ x₃))) (delta (mono (mono x₄)) (mono (delta (mono x₅) (mono (mono x₆)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	347 monad-law-1 (delta (delta (delta x x₁) (delta x₂ (delta x₃ x₄))) (delta (mono (mono x₅)) (mono (delta (mono x₆) (mono (mono x₇)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	348 monad-law-1 (delta (delta (mono x) x₁) (delta (mono (mono x₂)) (mono (delta (mono x₃) (mono (delta x₄ d₂)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	349 monad-law-1 (delta (delta (delta x x₁) x₂) (delta (mono (mono x₃)) (mono (delta (mono x₄) (mono (delta x₅ d₂)))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	350 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (delta (mono (mono x₂)) (mono (delta (mono x₃) (delta (mono x₄) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	351 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (delta (mono (mono x₂)) (mono (delta (mono x₃) (delta (delta x₄ (mono x₅)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	352 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (delta (mono (mono x₂)) (mono (delta (mono x₃) (delta (delta x₄ (delta x₅ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	353 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (mono x₅) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	354 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (delta x₅ (mono x₆)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	355 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (delta x₅ (delta x₆ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	356 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (mono x₅) (delta (mono x₆) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	357 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (mono x₅) (delta (delta x₆ (mono x₇)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	358 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (mono x₅) (delta (delta x₆ (delta x₇ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	359 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (mono x₄)))))) (delta (mono (mono x₅)) (mono (delta (mono x₆) (delta (mono x₇) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	360 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (mono x₄)))))) (delta (mono (mono x₅)) (mono (delta (mono x₆) (delta (delta x₇ (mono x₈)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	361 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (mono x₄)))))) (delta (mono (mono x₅)) (mono (delta (mono x₆) (delta (delta x₇ (delta x₈ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	362 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))))) (delta (mono (mono x₆)) (mono (delta (mono x₇) (delta (mono x₈) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	363 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))))) (delta (mono (mono x₆)) (mono (delta (mono x₇) (delta (delta x₈ (mono x₉)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	364 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (mono x₅))))))) (delta (mono (mono x₆)) (mono (delta (mono x₇) (delta (delta x₈ (delta x₉ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	365 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆)))))))) (delta (mono (mono x₇)) (mono (delta (mono x₈) (delta (mono x₉) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	366 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆)))))))) (delta (mono (mono x₇)) (mono (delta (mono x₈) (delta (delta x₉ (mono x₁₀)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	367 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (mono x₆)))))))) (delta (mono (mono x₇)) (mono (delta (mono x₈) (delta (delta x₉ (delta x₁₀ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	368 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ x₇)))))))) (delta (mono (mono x₈)) (mono (delta (mono x₉) (delta (mono x₁₀) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	369 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ x₇)))))))) (delta (mono (mono x₈)) (mono (delta (mono x₉) (delta (delta x₁₀ (mono x₁₁)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	370 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ (delta x₅ (delta x₆ x₇)))))))) (delta (mono (mono x₈)) (mono (delta (mono x₉) (delta (delta x₁₀ (delta x₁₁ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	371 monad-law-1 (delta (delta (mono x) (delta x₁ x₂)) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (mono x₅) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	372 monad-law-1 (delta (delta (mono x) (delta x₁ x₂)) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (delta x₅ (mono x₆)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	373 monad-law-1 (delta (delta (mono x) (delta x₁ x₂)) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (delta x₅ (delta x₆ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	374 monad-law-1 (delta (delta (delta x x₁) x₂) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (mono x₅) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	375 monad-law-1 (delta (delta (delta x x₁) x₂) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (delta x₅ (mono x₆)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	376 monad-law-1 (delta (delta (delta x x₁) x₂) (delta (mono (mono x₃)) (mono (delta (mono x₄) (delta (delta x₅ (delta x₆ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	377 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	378 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (mono x₅) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	379 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (delta x₅ (mono x₆)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	380 monad-law-1 (delta (delta (mono x) (mono (mono x₁))) (delta (mono (mono x₂)) (mono (delta (delta x₃ (mono x₄)) (delta (delta x₅ (delta x₆ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	381 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (delta (mono (mono x₃)) (mono (delta (delta x₄ (mono x₅)) (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	382 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (delta (mono (mono x₃)) (mono (delta (delta x₄ (mono x₅)) (delta (mono x₆) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	383 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (delta (mono (mono x₃)) (mono (delta (delta x₄ (mono x₅)) (delta (delta x₆ (mono x₇)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	384 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (mono x₂)))) (delta (mono (mono x₃)) (mono (delta (delta x₄ (mono x₅)) (delta (delta x₆ (delta x₇ d₂)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	385 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (delta x₅ (mono x₆)) (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	386 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (delta x₅ (mono x₆)) (delta (mono x₇) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	387 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (delta x₅ (mono x₆)) (delta (delta x₇ (mono x₈)) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	388 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (delta x₅ (mono x₆)) (delta (delta x₇ (delta x₈ (mono x₉))) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	389 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (mono x₃))))) (delta (mono (mono x₄)) (mono (delta (delta x₅ (mono x₆)) (delta (delta x₇ (delta x₈ (delta x₉ d₂))) d₃))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	390 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (mono x₄)))))) (delta (mono (mono x₅)) (mono (delta (delta x₆ (mono x₇)) (mono d₂))))) = refl
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	391 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (mono x₄)))))) (delta (mono (mono x₅)) (mono (delta (delta x₆ (mono x₇)) (delta d₂ d₃))))) = {!!}
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	392 monad-law-1 (delta (delta (mono x) (mono (delta x₁ (delta x₂ (delta x₃ (delta x₄ x₅)))))) (delta (mono (mono x₆)) (mono (delta (delta x₇ (mono x₈)) d₂)))) = {!!}
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	393 monad-law-1 (delta (delta (mono x) (delta x₁ x₂)) (delta (mono (mono x₃)) (mono (delta (delta x₄ (mono x₅)) d₂)))) = {!!}
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	394 monad-law-1 (delta (delta (delta x x₁) x₂) (delta (mono (mono x₃)) (mono (delta (delta x₄ (mono x₅)) d₂)))) = {!!}
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	395 monad-law-1 (delta (delta x x₁) (delta (mono (mono x₂)) (mono (delta (delta x₃ (delta x₄ d₁)) d₂)))) = {!!}
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	396 --
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	397 monad-law-1 (delta x (delta (mono (mono x₁)) (delta d₁ d₂))) = {!!}
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	398 monad-law-1 (delta x (delta (mono (delta x₁ d)) d₁)) = {!!}
73bb981cb1c6 Expand pattern-matches... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 59 diff changeset	399 monad-law-1 (delta x (delta (delta d d₁) d₂)) = {!!}
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	400
29 e0ba1bf564dd Apply level to some functions Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 28 diff changeset	401
34 b7c4e6276bcf Proof Monad-law-2-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 33 diff changeset	402
56 bfb6be9a689d Trying redefine monad-laws-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 55 diff changeset	403 {-
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	404 -- monad-law-2-2 : join . return = id
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	405 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s
35 c5cdbedc68ad Proof Monad-law-2-2 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 34 diff changeset	406 monad-law-2-2 (similar lx x ly y) = refl
c5cdbedc68ad Proof Monad-law-2-2 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 34 diff changeset	407
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	408 -- monad-law-3 : return . f = fmap f . return
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	409 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x
36 169ec60fcd36 Proof Monad-law-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 35 diff changeset	410 monad-law-3 f x = refl
27 742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	411
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	412 -- monad-law-4 : join . fmap (fmap f) = fmap f . join
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	413 monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (s : Delta (Delta A)) ->
36 169ec60fcd36 Proof Monad-law-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 35 diff changeset	414 (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	415 monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	416
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	417
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	418 -- Monad-laws (Haskell)
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	419 -- monad-law-h-1 : return a >>= k = k a
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	420 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	421 (a : A) -> (k : A -> (Delta B)) ->
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	422 (return a >>= k) ≡ (k a)
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	423 monad-law-h-1 a k = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	424
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	425
40 a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	426
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	427 -- monad-law-h-2 : m >>= return = m
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	428 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= return) ≡ m
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	429 monad-law-h-2 (mono x) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	430 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d)
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	431
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	432
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	433
41 23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	434
23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	435 -- monad-law-h-3 : m >>= (\x -> k x >>= h) = (m >>= k) >>= h
23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	436 monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	437 (m : Delta A) -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) ->
41 23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	438 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	439 monad-law-h-3 (mono x) k h = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	440 monad-law-h-3 (delta x d) k h = begin
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	441 (delta x d) >>= (\x -> k x >>= h)
42 1df4f9d88025 Proof Monad-law-3 (haskell) Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 41 diff changeset	442 ≡⟨ refl ⟩
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	443 -- (delta x d) >>= f = deltaAppend (headDelta (f x)) (d >>= (tailDelta ∙ f))
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	444 deltaAppend (headDelta ((\x -> k x >>= h) x)) (d >>= (tailDelta ∙ (\x -> k x >>= h)))
42 1df4f9d88025 Proof Monad-law-3 (haskell) Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 41 diff changeset	445 ≡⟨ refl ⟩
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	446 deltaAppend (headDelta (k x >>= h)) (d >>= (tailDelta ∙ (\x -> k x >>= h)))
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	447 ≡⟨ {!!} ⟩
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	448 ((delta x d) >>= k) >>= h
41 23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	449 ∎
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	450 -}

Mercurial > hg > Members > atton > delta_monad

annotate agda/delta.agda @ 60:73bb981cb1c6