# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668588190 -32400
# Node ID 407684f806e40718dcf9ee9c5e3f21fb591367a4
# Parent  ba0ae5de62d1d4bd406e36ed48fff075f7f6db97
...

diff -r ba0ae5de62d1 -r 407684f806e4 a02/agda-install.ind
--- a/a02/agda-install.ind	Tue Jan 25 09:11:01 2022 +0900
+++ b/a02/agda-install.ind	Wed Nov 16 17:43:10 2022 +0900
@@ -11,7 +11,7 @@
 
 install 先がどこかは、
 
-    /usr/local/Cellar/agda/2.6.1/lib/agda
+    /opt/homebrew/Cellar/agda/
 
 などになるので、
 
@@ -21,10 +21,10 @@
 
 defaults の中には
 
-   standard-library
+    /opt/homebrew/Cellar/agda/2.6.2.2/lib/agda/standard-library.agda-lib 
 
 libraries の中には
-    /usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib
+    /opt/homebrew/Cellar/agda/2.6.2.2/lib/agda/standard-library.agda-lib 
 
 --VS-code
 
@@ -72,7 +72,18 @@
 
 --vim
 
-<a ref="https://github.com/derekelkins/agda-vim"> agda-vim</a>
+neovim で、
+
+<a href="https://github.com/shinji-kono/nvim-agda"> nvim-agda </a>
 
 が使えます。
 
+--document
+
+Agda のライブラリの説明をみていくと良い
+
+ /opt/homebrew/Cellar/agda/2.6.2.2/lib/agda/README/Data/Nat.agda
+
+
+
+
diff -r ba0ae5de62d1 -r 407684f806e4 a02/agda/dag.agda
--- a/a02/agda/dag.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/a02/agda/dag.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -7,14 +7,14 @@
 --         f1
 
 
-data  TwoObject   : Set  where
-       t0 : TwoObject
-       t1 : TwoObject
+data  TwoObject   : Set  where     -- vertex
+    t0 : TwoObject
+    t1 : TwoObject
 
 
-data TwoArrow  : TwoObject → TwoObject → Set  where
-       f0 :  TwoArrow t0 t1
-       f1 :  TwoArrow t0 t1
+data TwoArrow  : TwoObject → TwoObject → Set  where  -- edge
+    f0 :  TwoArrow t0 t1
+    f1 :  TwoArrow t0 t1
 
 
 --         r0
@@ -24,25 +24,34 @@
 --         r1
 
 data Circle  : TwoObject → TwoObject → Set  where
-       r0 :  Circle t0 t1
-       r1 :  Circle t1 t0
+    r0 :  Circle t0 t1
+    r1 :  Circle t1 t0
 
-data ⊥ : Set where
+--
+-- Definition of ⊥ and ¬  in agda
+--
 
-⊥-elim : {A : Set } -> ⊥ -> A
-⊥-elim ()
+data ⊥ : Set where              -- data with no consutructor
 
-¬_ : Set → Set
+⊥-elim : {A : Set } → ⊥ →  A    -- function with no possible input
+⊥-elim ()                       --   no constructor
+
+¬_ : Set → Set                  -- A won't happen (This is a type, not an imlemetation )
 ¬ A = A → ⊥
 
 data Bool  : Set  where
-       true :  Bool
-       false :  Bool
+    true :  Bool
+    false :  Bool
 
 data connected { V : Set } ( E : V → V → Set ) ( x y : V ) : Set  where
-    direct :   E x y → connected E x y 
+    direct :     E x y → connected E x y 
     indirect :  { z : V  } → E x z  →  connected {V} E z y → connected E x y
 
+-- this is similar to the List
+data List ( A : Set ) : Set where
+    nil : List A
+    cons : A → List A →  List A
+
 lemma1 : connected TwoArrow t0 t1
 lemma1 =  {!!}
 
@@ -54,22 +63,37 @@
 -- lemma2 (indirect () (indirect _ _ ))
 
 lemma3 : connected Circle t0 t0
-lemma3 = {!!}
+lemma3 = ?
+
+-- decidabity
 
 data Dec (P : Set) : Set where
    yes :   P → Dec P
    no  : ¬ P → Dec P
 
-reachable :  { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
+reachable :  { V : Set } ( E : V → V → Set ) ( x y : V ) → Set
 reachable {V} E x y = Dec ( connected {V} E x y )
 
-dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+dag :  { V : Set } ( E : V → V → Set ) →  Set
 dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
 
+-- dag {V} E =  ∀ (n : V)  →   connected E n n → ⊥
+
 lemma4 : dag TwoArrow
-lemma4 = {!!}
+lemma4 = ?
 
 lemma5 :  ¬ ( dag Circle )
-lemma5 x = ⊥-elim {!!}
+lemma5 x = ?
 
-
+-- record Finite ( A : Set ) : Set where
+--    field
+--       a : ?
+-- 
+-- record FiniteE {A : Set} ( E : A → A → Set ) : Set where
+--    field
+--       a : ?
+-- 
+-- lemma6 : ( V : Set ) ( E : V → V → Set ) → Finite V → FiniteE E → ( x y : V ) → reachable E x y
+-- lemma6 = ?
+-- 
+-- 
diff -r ba0ae5de62d1 -r 407684f806e4 a02/agda/data1.agda
--- a/a02/agda/data1.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/a02/agda/data1.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -7,7 +7,7 @@
 ex1 : {A B : Set} → A → ( A ∨ B ) 
 ex1  a = case1 a
 
-ex2 : {A B : Set} → B → ( A ∨ B ) 
+ex2 : {A B : Set} → ( B → ( A ∨ B ) )
 ex2 = λ b → case2 b
 
 ex3 : {A B : Set} → ( A ∨ A ) → A 
@@ -15,9 +15,12 @@
 ex3 (case2 x) = x
 
 ex4 : {A B C : Set} →  A ∨ ( B ∨ C ) → ( A ∨  B ) ∨ C 
-ex4 = {!!}
+ex4 (case1 a) = case1 (case1 a )
+ex4 (case2 (case1 b)) = case1 (case2 b)
+ex4 (case2 (case2 c)) = case2 c
 
 record _∧_ A B : Set where
+  constructor  ⟪_,_⟫
   field
      proj1 : A
      proj2 : B
@@ -25,14 +28,15 @@
 open _∧_
 
 ex3' : {A B : Set} → ( A ∨ B ) →   A ∧ B   -- this is wrong
-ex3' = {!!}
+ex3' = ?
 
 ex4' : {A B : Set} → ( A ∧ B ) →   A ∨ B   
-ex4' = {!!}
+ex4' ab = case1 (proj1 ab )
 
 --- ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∨  B ) → C ) is wrong
 ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∧  B ) → C )
-ex5 = {!!}
+ex5 (case1 a→c) ab = a→c (proj1 ab)
+ex5 (case2 b→c) ab = b→c (proj2 ab)
 
 data ⊥ : Set where
 
@@ -81,6 +85,10 @@
 
 infixl 110 _∨_ 
 
+--         t1
+--        /  \ r1
+--      t3 ←  t2
+--         r2
 
 data 3Ring : (dom cod : Three) → Set where
    r1 : 3Ring t1 t2
@@ -96,14 +104,12 @@
 add (suc x) y = suc ( add x y )
 
 mul : ( a b : Nat ) → Nat
-mul zero x = {!!}
-mul (suc x) y = {!!}
+mul zero x = zero
+mul (suc x) y = add y (mul x y)
 
 ex6 : Nat
 ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
 
-
-
 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
    direct :   E x y -> connected E x y
    indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y
diff -r ba0ae5de62d1 -r 407684f806e4 a02/agda/equality.agda
--- a/a02/agda/equality.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/a02/agda/equality.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -5,10 +5,10 @@
    refl :  {x : A} → x == x
 
 ex1 : {A : Set} {x : A } → x == x
-ex1  = {!!}
+ex1  = ?
 
 ex2 : {A : Set} {x y : A } → x == y → y == x
-ex2 = {!!}
+ex2 = ?
 
 ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
 ex3 = {!!}
diff -r ba0ae5de62d1 -r 407684f806e4 a02/agda/lambda.agda
--- a/a02/agda/lambda.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/a02/agda/lambda.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -18,18 +18,24 @@
 A→A' x = x
 
 lemma2 : (A : Set ) →  A → A   --  これは  A → ( A  → A ) とは違う
-lemma2 = {!!}
+lemma2 = ?
+
+lemma3 : {A B : Set } → B → ( A → B )  -- {} implicit variable
+lemma3  b = λ _ → b    -- _ anonymous variable
 
-λ-intro : {A B : Set } → A →  B → ( A → B )  -- {} implicit variable
-λ-intro  _ b = λ _ → b    -- _ anonymous variable
-
--- λ-intro {A} {B} a b = λ a → b    
+-- λ-intro 
+--
+--    a :  A
+--     :              f : A → B
+--    b :  B 
+--  ------------- f
+--    A → B
 
 --   λ-elim
 --
---      A     A → B
---   ----------------- λ-elim 
---          B
+--     a : A     f : A → B
+--   ------------------------ λ-elim 
+--          f a :  B      
 
 →elim : A → ( A → B ) → B
 →elim a f = f a 
diff -r ba0ae5de62d1 -r 407684f806e4 a02/agda/logic.agda
--- a/a02/agda/logic.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/a02/agda/logic.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -19,6 +19,14 @@
    case1 : A → A ∨ B
    case2 : B → A ∨ B
 
+-- data ⊥ : Set where
+
+-- ⊥-elim : {n : Level} {A : Set n } → ⊥ → A
+--⊥-elim ()
+
+-- ¬_ : {n : Level } → Set n → Set n
+-- ¬ A = A → ⊥
+
 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
diff -r ba0ae5de62d1 -r 407684f806e4 a02/lecture.ind
--- a/a02/lecture.ind	Tue Jan 25 09:11:01 2022 +0900
+++ b/a02/lecture.ind	Wed Nov 16 17:43:10 2022 +0900
@@ -121,6 +121,10 @@
 
 <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html"> Unicode入力 </a>
 
+--Agda introduction
+
+<a href="https://gitlab.ie.u-ryukyu.ac.jp/teacher/kono/agda-introduction"> Agda introduction </a>
+
 --重要
 
     空白が入らないものは一単語になる (A→A は一単語、A → A とは別)
@@ -423,3 +427,18 @@
 
 
 
+---問題2.3 sum type の問題
+
+問題2.9 まで
+
+<a href=""> </a> <!--- Exercise 2.3 --->
+<a href=""> </a> <!--- Exercise 2.4 --->
+<a href=""> </a> <!--- Exercise 2.5 --->
+<a href=""> </a> <!--- Exercise 2.6 --->
+<a href=""> </a> <!--- Exercise 2.7 --->
+<a href=""> </a> <!--- Exercise 2.8 --->
+<a href=""> </a> <!--- Exercise 2.9 --->
+<a href=""> </a> <!--- Exercise 2.8 --->
+<a href=""> </a> <!--- Exercise 2.9 --->
+
+
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/automaton-ex.agda
--- a/automaton-in-agda/src/automaton-ex.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/automaton-ex.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -30,8 +30,9 @@
 transitionQ q3 i1 = q2
 
 aendQ : StatesQ → Bool
+aendQ q1 = false
 aendQ q2 = true
-aendQ _ = false
+aendQ q3 = false
 
 a1 : Automaton StatesQ In2
 a1 = record {
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/derive.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -165,13 +165,13 @@
 --
 -- if (Derivative r is finite,  regex→automaton is finite
 --
-drive-is-finite : (r : Regex   Σ) → FiniteSet (Derivative r) 
-drive-is-finite ε = {!!}
-drive-is-finite φ = {!!}
-drive-is-finite (r *) = {!!} where
-   d1 :  FiniteSet (Derivative r )
-   d1 = drive-is-finite r
-drive-is-finite (r & r₁) = {!!}
-drive-is-finite (r || r₁) = {!!}
-drive-is-finite < x > = {!!}
-
+-- drive-is-finite : (r : Regex   Σ) → FiniteSet (Derivative r) 
+-- drive-is-finite ε = {!!}
+-- drive-is-finite φ = {!!}
+-- drive-is-finite (r *) = {!!} where
+--    d1 :  FiniteSet (Derivative r )
+--    d1 = drive-is-finite r
+-- drive-is-finite (r & r₁) = {!!}
+-- drive-is-finite (r || r₁) = {!!}
+-- drive-is-finite < x > = {!!}
+-- 
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -103,7 +103,7 @@
 
 iso-fin : {A B : Set} → FiniteSet A  → Bijection A B → FiniteSet B 
 iso-fin {A} {B}  fin iso = record {
-   Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f )
+       Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f )
      ; F←Q = λ b → FiniteSet.F←Q fin (fun← iso b )
      ; finiso→ = finiso→ 
      ; finiso← = finiso← 
@@ -131,10 +131,10 @@
 
 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 
 fin-∨1 {B} fb =  record {
-   Q←F = Q←F
- ; F←Q =  F←Q
- ; finiso→ = finiso→
- ; finiso← = finiso←
+       Q←F = Q←F
+     ; F←Q =  F←Q
+     ; finiso→ = finiso→
+     ; finiso← = finiso←
    }  where
    b = FiniteSet.finite fb
    Q←F : Fin (suc b) → One ∨ B
@@ -502,6 +502,14 @@
 -- there is a duplicate element in finite list
 --
 
+--
+-- How about this?
+--      get list of Q
+--      remove one element for each Q from list
+--      there must be remaining list > 1
+--      theses are duplicates
+--      actualy it is duplicate
+
 phase2 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
 phase2 finq q [] = false
 phase2 finq q (x ∷ qs) with equal? finq q x
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/omega-automaton.agda
--- a/automaton-in-agda/src/omega-automaton.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/omega-automaton.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -72,6 +72,11 @@
      δ Ω' (ω-run Ω' q s n) (s n) ≡⟨⟩
      ω-run Ω' q s (suc n) ∎  where open ≡-Reasoning
 
+--
+-- <> [] p → ¬ [] <> ¬ p
+--
+
+
 B→M : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
 B→M {Q} {Σ} Ω S q b m = ¬-bool bm04 bm02 where
    q1 : Q
@@ -90,6 +95,9 @@
      not (aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b)))))) ≡⟨ cong (λ k → not k ) bm03  ⟩
      false ∎  where open ≡-Reasoning
 
+--
+-- [] <> p → ¬ <> [] ¬ p
+--
 
 M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
 M→B {Q} {Σ} Ω S q m b = ¬-bool bm04 bm02 where
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/puzzle.agda
--- a/automaton-in-agda/src/puzzle.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/puzzle.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -15,13 +15,13 @@
   open import Relation.Nullary
   open import Data.Empty
 
-  postulate 
+  postulate   -- the law of exclude middle
      lem : (a : Set) → a ∨ ( ¬ a )
 
   record PetResearch ( Cat Dog Goat Rabbit : Set ) : Set where
      field
-        fact1 : ( Cat ∨ Dog ) → ¬ Goat
-        fact2 : ¬ Cat →  ( Dog ∨ Rabbit )
+        fact1 :  Cat ∨ Dog  → ¬ Goat
+        fact2 : ¬ Cat →   Dog ∨ Rabbit 
         fact3 : ¬ ( Cat ∨ Goat ) →  Rabbit
 
   module tmp ( Cat Dog Goat Rabbit : Set ) (p :  PetResearch  Cat Dog Goat Rabbit ) where
@@ -31,7 +31,7 @@
     problem0 : Cat ∨ Dog ∨ Goat ∨ Rabbit
     problem0 with lem Cat | lem Goat
     ... | case1 c | g = case1 c
-    ... | c | case1 g = case2 ( case2 ( case1 g ) )
+    ... | case2 ¬c | case1 g = case2 ( case2 ( case1 g ) )
     ... | case2 ¬c | case2 ¬g  = case2 ( case2 ( case2 ( fact3 p lemma1 ))) where
         lemma1 : ¬ ( Cat ∨ Goat )
         lemma1 (case1 c) = ¬c c
@@ -71,7 +71,7 @@
 
   _=>_ :  Bool → Bool → Bool
   _ => true = true
-  false => _ = true
+  false => false = true
   true => false = false
 
   ¬_ : Bool → Bool
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/regex1.agda
--- a/automaton-in-agda/src/regex1.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/regex1.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -2,7 +2,7 @@
 module regex1 where
 
 open import Level renaming ( suc to succ ; zero to Zero )
-open import Data.Fin
+open import Data.Fin hiding ( pred )
 open import Data.Nat hiding ( _≟_ )
 open import Data.List hiding ( any ;  [_] )
 -- import Data.Bool using ( Bool ; true ; false ; _∧_ )
@@ -35,18 +35,43 @@
 open import nfa
 
 --    former ++ later  ≡ x
-split : {Σ : Set} → ((former : List Σ) → Bool) → ((later :  List Σ) → Bool) → (x : List Σ ) → Bool
+split : {Σ : Set} → (x : List Σ → Bool) → (y :  List Σ → Bool) → (z : List Σ ) → Bool
 split x y  [] = x [] /\ y []
 split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
   split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
--- tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] )
--- tt1 P Q = ?
+---   ( a ∷ b ∷ c ∷ [] )
+--
+---     former ( a ∷ b ∷ c ∷ [] ) ∧ later []
+--- ∨ ( former ( a ∷ b ∷ [] ) ∧ later (c ∷ [] ) )
+--- ∨ ( former ( a ∷ [] ) ∧ later (b ∷ c ∷ [] ) )
+--- ∨ ( former ( [] ) ∧ later (a ∷ b ∷ c ∷ [] ) )
+
+tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] ) ≡ ?
+tt1 P Q = ?
+
+-- {-# TERMINATING #-}
+-- repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
+-- repeat x [] = true
+-- repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
 
-{-# TERMINATING #-}
-repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
-repeat x [] = true
-repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
+repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
+repeat {Σ} x [] = true
+repeat {Σ} x (h ∷ y) = repeat2 [] (h ∷ y) where
+    repeat2 : (pre y : List Σ ) → Bool
+    repeat2 pre [] = false
+    repeat2 pre (h ∷ y) = 
+       (x (pre ++ (h ∷ [])) /\ repeat x y )
+       \/ repeat2 (pre ++ (h ∷ [])) y 
+
+test-AB→repeat1 : {Σ : Set} → {A : List In → Bool} → repeat A  ( a ∷ b ∷ c ∷ [] ) ≡  
+    A (a ∷ []) /\ (
+           (A (b ∷ [])     /\ (A (c ∷ []) /\ true \/ false) )
+        \/ (A (b ∷ c ∷ []) /\ true \/ false))
+    \/ A (a ∷ b ∷ []) /\ (A (c ∷ []) /\ true \/ false) 
+    \/ A (a ∷ b ∷ c ∷ []) /\ true \/ false
+test-AB→repeat1 {_} {A}  = refl
+
 
 -- Meaning of regular expression
 
@@ -84,6 +109,9 @@
 test-regex : regular-language r1' cmpi ( a ∷ [] ) ≡ false
 test-regex = refl
 
+-- test-regex2 : regular-language r2 cmpi ( b ∷ c ∷ a ∷ b ∷ [] ) ≡ false
+-- test-regex2 = refl
+
 test-regex1 : regular-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true
 test-regex1 = refl
 
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/regular-language.agda
--- a/automaton-in-agda/src/regular-language.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -21,10 +21,9 @@
 language-L {Σ} = List (List Σ)
 
 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
-Union {Σ} A B x = (A x ) \/ (B x)
+Union {Σ} A B x = A x  \/ B x
 
-split : {Σ : Set} → (List Σ → Bool)
-      → ( List Σ → Bool) → List Σ → Bool
+split : {Σ : Set} → (x y : language {Σ} ) → language {Σ}
 split x y  [] = x [] /\ y []
 split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
   split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -47,6 +47,12 @@
 ... | case1 dn = dn
 ... | case2 dm = dm
 
+-- divdable-n*m : { n m k : ℕ } → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k n
+-- divdable-n*m = ?
+
+-- 2^2 : { n k : ℕ } → 1 < n → Dividable 2 ( n * n ) → Dividable 2 n
+-- 2^2 = ?
+
 -- p * n * n ≡ m * m means (m/n)^2 = p
 -- rational m/n requires m and n is comprime each other which contradicts the condition
 
diff -r ba0ae5de62d1 -r 407684f806e4 automaton-in-agda/src/temporal-logic.agda
--- a/automaton-in-agda/src/temporal-logic.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/temporal-logic.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -101,6 +101,11 @@
     _q\/_ :  QPTL V → QPTL  V → QPTL  V
     _q/\_ :  QPTL V → QPTL  V → QPTL  V
 
+--
+--  ∃ p ( <> p → ? )
+--
+
+
 {-# TERMINATING #-}
 SQP1 : { V : Set } → ((x y : V) → Dec ( x ≡ y))   → QPTL V → V  → Bool → QPTL V
 SQP1 {V} dec (qt x) v t = qt x
diff -r ba0ae5de62d1 -r 407684f806e4 index.ind
--- a/index.ind	Tue Jan 25 09:11:01 2022 +0900
+++ b/index.ind	Wed Nov 16 17:43:10 2022 +0900
@@ -35,8 +35,7 @@
 
 --Agdaの記述
 
-<a href="agda/index.html"> 2020  </a><br>
-<a href="agda-2.6.2/index.html"> 2019  </a>
+<a href="https://github.com/shinji-kono/automaton-in-agda"> github  </a><br>
 
 -- 評価方法