# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1699446954 -32400
# Node ID a60132983557f39f3d1d9eee068cf90bb4e5188e
# Parent  af8f630b7e6083ab5734ea14489f93042312a75d
...

diff -r af8f630b7e60 -r a60132983557 a01/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a02/agda-install.ind
diff -r af8f630b7e60 -r a60132983557 a02/agda.ind
diff -r af8f630b7e60 -r a60132983557 a02/agda/dag.agda
diff -r af8f630b7e60 -r a60132983557 a02/agda/data1.agda
--- a/a02/agda/data1.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/agda/data1.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -28,20 +28,20 @@
 open _∧_
 
 ex3' : {A B : Set} → ( A ∨ B ) →   A ∧ B   -- this is wrong
-ex3' = ?
+ex3' (case1 x) = ?
+ex3' (case2 x) = ?
 
 ex4' : {A B : Set} → ( A ∧ B ) →   A ∨ B   
-ex4' ab = case1 (proj1 ab )
+ex4' ⟪ a , b ⟫ = ?
 
 --- 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 (case1 a→c) ab = a→c (proj1 ab)
-ex5 (case2 b→c) ab = b→c (proj2 ab)
+ex5 = ?
 
 data ⊥ : Set where
 
-⊥-elim : {A : Set } -> ⊥ -> A
-⊥-elim = {!!}
+⊥-elim : {A : Set } →  ⊥ →  A
+⊥-elim ()
 
 ¬_ : Set → Set
 ¬ A = A → ⊥
@@ -76,6 +76,36 @@
     problem2 = {!!}
 
 
+data Nat : Set where
+  zero : Nat
+  suc  : Nat →  Nat
+
+one : Nat
+one = suc zero
+
+five : Nat
+five = suc (suc (suc (suc (suc zero))))
+
+add : ( a b : Nat ) → Nat
+add zero x = x
+add (suc x) y = suc ( add x y )
+
+data _≡_ {A : Set } : ( x y : A ) → Set where
+  refl : {x : A} → x ≡ x
+
+test11 : add one five ≡ suc five
+test11 = refl
+
+mul : ( a b : Nat ) → Nat
+mul zero x = zero
+mul (suc x) y = add y (mul x y)
+
+ex6 : Nat
+ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
+
+ex7 : mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) ≡  suc (suc (suc (suc (suc (suc zero)))))
+ex7 = refl
+
 data Three : Set where
   t1 : Three
   t2 : Three
@@ -95,27 +125,24 @@
    r2 : 3Ring t2 t3
    r3 : 3Ring t3 t1
 
-data Nat : Set where
-  zero : Nat
-  suc  : Nat →  Nat
-
-add : ( a b : Nat ) → Nat
-add zero x = x
-add (suc x) y = suc ( add x y )
-
-mul : ( a b : Nat ) → Nat
-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
 
-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 )
 
 lemma : ¬ (dag 3Ring )
-lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 )))
+lemma r = ?
+
+--   t1 → t2 → t3
+--
+data 3Line : (dom cod : Three) → Set where
+   line1 : 3Line t1 t2
+   line2 : 3Line t2 t3
+
+lemma1 : dag 3Line
+lemma1 = ?
+
+
+
diff -r af8f630b7e60 -r a60132983557 a02/agda/equality.agda
--- a/a02/agda/equality.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/agda/equality.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,26 +1,26 @@
 module equality where
 
 
-data _==_ {A : Set } : A → A → Set where
-   refl :  {x : A} → x == x
+data _≡_ {A : Set } : A → A → Set where
+   refl :  {x : A} → x ≡ x
 
-ex1 : {A : Set} {x : A } → x == x
+ex1 : {A : Set} {x : A } → x ≡ x
 ex1  = ?
 
-ex2 : {A : Set} {x y : A } → x == y → y == x
+ex2 : {A : Set} {x y : A } → x ≡ y → y ≡ x
 ex2 = ?
 
-ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
+ex3 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
 ex3 = {!!}
 
-ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
+ex4 : {A B : Set} {x y : A } { f : A → B } →   x ≡ y → f x ≡ f y
 ex4 = {!!}
 
-subst : {A : Set } → { x y : A } → ( f : A → Set ) → x == y → f x → f y
+subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
 subst {A} {x} {y} f refl fx = fx
 
--- ex5 :   {A : Set} {x y z : A } →  x == y → y == z → x == z
--- ex5 {A} {x} {y} {z} x==y y==z = subst (λ refl  → {!!} ) x==y {!!}
+-- ex5 :   {A : Set} {x y z : A } →  x ≡ y → y ≡ z → x ≡ z
+-- ex5 {A} {x} {y} {z} x≡y y≡z = subst (λ refl  → {!!} ) x≡y {!!}
 
 
 
diff -r af8f630b7e60 -r a60132983557 a02/agda/lambda.agda
diff -r af8f630b7e60 -r a60132983557 a02/agda/level1.agda
diff -r af8f630b7e60 -r a60132983557 a02/agda/list.agda
diff -r af8f630b7e60 -r a60132983557 a02/agda/logic.agda
--- a/a02/agda/logic.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/agda/logic.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module logic where
 
 open import Level
diff -r af8f630b7e60 -r a60132983557 a02/agda/practice-logic.agda
diff -r af8f630b7e60 -r a60132983557 a02/agda/practice-nat.agda
--- a/a02/agda/practice-nat.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/agda/practice-nat.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 module practice-nat where
 
 open import Data.Nat 
@@ -6,24 +7,29 @@
 open import Relation.Binary.PropositionalEquality hiding (_⇔_)
 open import logic
 
+-- data _<=_ : ℕ → ℕ → Set where
+--  z<=n : {x : ℕ} → zero <= x
+--  s<=s : {x y : ℕ} → x <= y → suc x <= suc y
+
 -- hint : it has two inputs, use recursion
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
-nat-<> = {!!}  
+nat-<>   (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
 -- hint : use recursion
 nat-<≡ : { x : ℕ } → x < x → ⊥
-nat-<≡ = {!!}
+nat-<≡ (s≤s x<x) = nat-<≡ x<x
 
 -- hint : use refl and recursion
 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
-nat-≡< = {!!}
+nat-≡< refl (s≤s x<y) = nat-≡< refl x<y
 
 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
-¬a≤a = {!!}
+¬a≤a (s≤s lt) = ¬a≤a lt
 
 -- hint : make case with la first
-a<sa : {la : ℕ} → la < suc la 
-a<sa = {!!}
+a<sa : {i : ℕ} → i < suc i 
+a<sa {zero} = s≤s z≤n
+a<sa {suc i} =  s≤s a<sa 
 
 -- hint  : ¬ has an input, use recursion
 =→¬< : {x : ℕ  } → ¬ ( x < x )
diff -r af8f630b7e60 -r a60132983557 a02/agda/record1.agda
diff -r af8f630b7e60 -r a60132983557 a02/lecture.ind
--- a/a02/lecture.ind	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/lecture.ind	Wed Nov 08 21:35:54 2023 +0900
@@ -22,6 +22,7 @@
 
 論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。
 
+この章の内容は基本的には Girad 先生の Proofs and Typesに書いてある内容です。
 
 --あらすじ
 
@@ -162,7 +163,7 @@
 
 record によって  
 
-   record _∧_ A B : Set
+   record _∧_ A B : Set where
      field
          π1 : A
          π2 : B
@@ -177,7 +178,7 @@
 
 とかける。(Haskell では (∧) を使う)
 
-は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。
+は、型Aと型Bから作るデータ構造である。オブジェクトあるいは構造体だと思って良い。
 
    record { π1 = x ; π2 = y }    
 
diff -r af8f630b7e60 -r a60132983557 a02/reduction.ind
diff -r af8f630b7e60 -r a60132983557 a02/unification.ind
diff -r af8f630b7e60 -r a60132983557 a03/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a04/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a05/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a06/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a07/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a08/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a09/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a10/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a11/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a12/lecture.ind
diff -r af8f630b7e60 -r a60132983557 a13/lecture.ind
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/LICENSE
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/README.md
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/automaton-in-agda.agda-lib
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/automaton-in-agda.agda-pkg
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -371,6 +371,10 @@
 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
 
+--
+-- fin→ is in finiteFunc.agda
+--      we excludeit becauase it uses f-extensionarity
+
 open import Data.List
 
 open FiniteSet
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/flcagl.agda
--- a/automaton-in-agda/src/flcagl.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/flcagl.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,6 +1,35 @@
 {-# OPTIONS --cubical-compatible #-}
+{-# OPTIONS --sized-types #-}
 
-{-# OPTIONS --sized-types #-}
+--
+-- induction
+--      data aaa where
+--          aend : aaa
+--          bb : (y : aaa) → aaa
+--          cc : (y : aaa) → aaa
+--
+--   (x : aaa) → bb → cc → aend
+--     induction : ( P : aaa → Set ) → (x : aaa) → P x
+--     induction P aend = ?
+--     induction P (bb y) = ? where
+--           lemma : P y
+--           lemma = induction P y 
+--     induction P (cc y) = ?
+--         
+--        ∙ 
+--       / \
+--      bb  cc
+--     /
+--    aend
+
+--
+-- coinduction
+--      record  AAA : Set where
+--        field
+--          bb : (y : AAA) 
+--          cc : (y : AAA) 
+
+
 open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
 module flcagl
@@ -11,6 +40,7 @@
 -- open import Data.Maybe
 open import Level renaming ( zero to Zero ; suc to succ )
 open import Size 
+open import Data.Empty
 
 module List where
 
@@ -50,6 +80,14 @@
         ν (trie f) = f []
         δ (trie f) a = trie (λ as → f (a ∷ as))
 
+        -- trie' : ∀{i}  (f : List i A → Bool) → Lang i
+        -- trie' {i} f = record { 
+        --     ν = f []
+        --   ; δ = λ {j} a → lem {j} a   -- we cannot write in this way
+        --   } where
+        --      lem :  {j : Size< i} → A → Lang j 
+        --      lem {j} a = trie' (λ as → f (a ∷ as))
+
         ∅ : ∀{i} → Lang i 
         ν ∅ = false
         δ ∅ x = ∅
@@ -78,6 +116,33 @@
         ν (k · l) = ν k ∧ ν l
         δ (k · l) x = let k′l =  δ k x  · l in if ν k then k′l ∪ δ l x else k′l
 
+        _+_ : ∀{i}  (k l : Lang i) → Lang i
+        ν (k + l) = ν k ∧ ν l
+        δ (k + l) x with ν k
+        ... | false = δ k x  + l 
+        ... | true  = (δ k x  + l )  ∪ δ l x 
+
+        language : { Σ : Set } → Set
+        language {Σ}  = List ∞ Σ → Bool
+
+        split : {Σ : Set} → {i : Size } → (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
+
+        LtoSplit : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ true →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true
+        LtoSplit x y [] xy with ν x | ν y
+        ... | true | true = refl
+        LtoSplit x y (h ∷ z) xy = ?
+
+        SplitoL : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ false →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false
+        SplitoL x y [] xy with ν x | ν y 
+        ... | false | false = refl
+        ... | false | true = ?
+        ... | true | false = ?
+        SplitoL x y (h ∷ z) xy = ?
+
+
         _*_ : ∀{i} (k l : Lang i )  → Lang i
         ν (k * l) = ν k ∧ ν l
         δ (_*_ {i} k  l) {j} x =
@@ -476,9 +541,9 @@
 Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x ))
 Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 
 
-nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
-Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa  {!!}
-Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 
+-- nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
+-- Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa  {!!}
+-- Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 
 
 -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
 -- Lang.ν (nlang' nfa s) = DA.ν nfa  s
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/logic.agda
--- a/automaton-in-agda/src/logic.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/logic.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -58,7 +58,7 @@
 false \/ false = false
 _ \/ _ = true
 
-not_ : Bool → Bool 
+not : Bool → Bool 
 not true = false
 not false = true 
 
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/nfa.agda
--- a/automaton-in-agda/src/nfa.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/nfa.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+-- {-# OPTIONS --allow-unsolved-metas #-}
 module nfa where
 
 -- open import Level renaming ( suc to succ ; zero to Zero )
@@ -54,6 +55,12 @@
     →  ( Qs : Q → Bool )  → (s : Σ ) → ( Q → Bool )
 Nmoves {Q} { Σ} M exists  Qs  s  = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
 
+--
+--  Q is finiteSet
+--  so we have 
+--     exists : ( P : Q → Bool ) → Bool
+--  which checks if there is a q in Q such that P q is true
+
 Naccept : { Q : Set } { Σ : Set  } 
     → NAutomaton Q  Σ
     → (exists : ( Q → Bool ) → Bool)
@@ -61,45 +68,22 @@
 Naccept M exists sb []  = exists ( λ q → sb q /\ Nend M q )
 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q →  exists ( λ qn → (sb qn /\ ( Nδ M qn i q )  ))) t
 
-{-# TERMINATING #-}
-NtraceDepth : { Q : Set } { Σ : Set  } 
-    → NAutomaton Q  Σ
-    → (Nstart : Q → Bool) → (all-states : List Q ) → List  Σ → List (List ( Σ ∧ Q ))
-NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
-    ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
-    ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
-    ndepth1 q i [] is t t1 = t1
-    ndepth1 q i (x ∷ qns) is t t1 =  ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
-    ndepth [] sb is t t1 =  t1
-    ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
-    ... | true =  ndepth qs sb [] t ( t  ∷ t1 )
-    ... | false =  ndepth qs sb [] t t1
-    ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 
-    ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
-    ... | false = ndepth qs sb (i ∷ is) t t1
-
-NtraceDepth1 : { Q : Set } { Σ : Set  } 
-    → NAutomaton Q  Σ
-    → (Nstart : Q → Bool) → (all-states : List Q ) → List  Σ → Bool ∧ List (List ( Σ ∧ Q ))
-NtraceDepth1 {Q} {Σ} M sb all is = ndepth all sb is [] [] where
-    exists : (Q → Bool) → Bool 
-    exists p = exists1 all where
-        exists1 : List Q → Bool 
-        exists1 [] = false
-        exists1 (q ∷ qs) with p q
-        ... | true = true
-        ... | false = exists1 qs
-    ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (Bool ∧ List ( Σ ∧ Q )  ) → Bool ∧  List (List ( Σ ∧ Q )  )
-    ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( Bool ∧ List ( Σ ∧ Q )) →  List ( Bool ∧ List ( Σ ∧ Q ))
-    ndepth1 q i [] is t t1 = t1
-    ndepth1 q i (x ∷ qns) is t t1 =  ? -- ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
-    ndepth [] sb is t t1 =  ? -- ⟪ exists (λ q → Nend M q /\ sb q)  ? ⟫
-    ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
-    ... | true =  ndepth qs sb [] t ( ?  ∷ t1 )
-    ... | false =  ndepth qs sb [] t t1
-    ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 
-    ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
-    ... | false = ndepth qs sb (i ∷ is) t t1
+-- {-# TERMINATING #-}
+-- NtraceDepth : { Q : Set } { Σ : Set  } 
+--     → NAutomaton Q  Σ
+--     → (Nstart : Q → Bool) → (all-states : List Q ) → List  Σ → List (List ( Σ ∧ Q ))
+-- NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
+--     ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
+--     ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
+--     ndepth1 q i [] is t t1 = t1
+--     ndepth1 q i (x ∷ qns) is t t1 =  ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
+--     ndepth [] sb is t t1 =  t1
+--     ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
+--     ... | true =  ndepth qs sb [] t ( t  ∷ t1 )
+--     ... | false =  ndepth qs sb [] t t1
+--     ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 
+--     ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
+--     ... | false = ndepth qs sb (i ∷ is) t t1
 
 -- trace in state set
 --
@@ -156,9 +140,9 @@
 t-1 : List ( List States1 )
 t-1 = Ntrace am2 LStates1  existsS1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )  -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ []
 t-2 = Ntrace am2 LStates1 existsS1  start1 ( i0  ∷ i1  ∷ i0  ∷ [] )  -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ []
-t-3 = NtraceDepth am2 start1 LStates1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
-t-4 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
-t-5 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1 ∷ [] ) 
+-- t-3 = NtraceDepth am2 start1 LStates1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
+-- t-4 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
+-- t-5 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1 ∷ [] ) 
 
 transition4 : States1  → In2  → States1 → Bool
 transition4 sr i0 sr = true
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/regular-concat.agda
--- a/automaton-in-agda/src/regular-concat.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/regular-concat.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,4 +1,10 @@
-module regular-concat where
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import finiteSet
+open import logic
+-- open import finiteFunc  -- we can prove fin→ , but it is unsafe 
+
+module regular-concat (fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool )) where
 
 open import Level renaming ( suc to Suc ; zero to Zero )
 open import Data.List 
@@ -10,18 +16,17 @@
 -- open import Data.Maybe
 open import  Relation.Nullary
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
-open import logic
 open import nat
 open import automaton
 open import regular-language 
 
 open import nfa
 open import sbconst2
-open import finiteSet
 open import finiteSetUtil
 
 open Automaton
 open FiniteSet
+open Split
 
 open RegularLanguage
 
@@ -56,93 +61,10 @@
        finf : FiniteSet (states A ∨ states B → Bool ) 
        finf = fin→ fin 
        
--- closed-in-concat' :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
--- closed-in-concat' {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
---     closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
---     closed-in-concat→ = {!!}
---     closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
---     closed-in-concat← = {!!}
-
-record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
-    field
-        sp0 : List Σ
-        sp1 : List Σ
-        sp-concat : sp0 ++ sp1 ≡ x
-        prop0 : A sp0 ≡ true
-        prop1 : B sp1 ≡ true
-
-open Split
-
-list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
-list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
-list-empty++ [] (x ∷ y) ()
-list-empty++ (x ∷ x₁) y ()
-
 open _∧_
 
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 
-c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
-   → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
-   → split (λ t1 → A (h ∷ t1)) B t ≡ true
-c-split-lemma {Σ} A B h t eq p = sym ( begin
-      true
-  ≡⟨  sym eq  ⟩
-      split A B (h ∷ t ) 
-  ≡⟨⟩
-      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
-  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩
-      false \/ split (λ t1 → A (h ∷ t1)) B t
-  ≡⟨ bool-or-1 refl ⟩
-      split (λ t1 → A (h ∷ t1)) B t
-  ∎ ) where
-     open ≡-Reasoning 
-     lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false
-     lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A )
-     lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B )
-
-split→AB :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
-split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true 
-split→AB {Σ} A B [] eq | yes eqa | yes eqb = 
-    record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
-split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
-split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
-split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
-... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
-... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
-... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
-split→AB {Σ} A B (h ∷ t ) eq  | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
-... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
-
-AB→split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
-AB→split {Σ} A B [] [] eqa eqb = begin
-       split A B [] 
-     ≡⟨⟩
-       A [] /\ B []
-     ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
-      true
-     ∎  where open ≡-Reasoning
-AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
-      split A B (h ∷ y )
-     ≡⟨⟩
-      A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
-     ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
-      true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
-     ≡⟨⟩
-      true \/ split (λ t1 → A (h ∷ t1)) B y
-     ≡⟨⟩
-      true
-     ∎  where open ≡-Reasoning
-AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
-       split A B ((h ∷ t) ++ y)  
-     ≡⟨⟩
-       A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
-     ≡⟨ cong ( λ k →  A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
-       A [] /\ B (h ∷ t ++ y) \/ true
-     ≡⟨ bool-or-3 ⟩
-      true
-     ∎  where open ≡-Reasoning
-
 open NAutomaton
 open import Data.List.Properties
 
@@ -204,28 +126,38 @@
           → (qa : states A )  → (  (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
     contain-A [] nq fn qa cond with found← finab fn  -- at this stage, A and B must be satisfied with [] (ab-case cond forces it)
-    ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
-    ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
-    ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S)))
+    ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S))
+    ... | case1 qa' | refl = lemma11 where
+       lemma12 : found-q S ≡ case1 qa →  aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ Concat-NFA.nend A B (found-q S)
+       lemma12 refl = refl
+       lemma11 : aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true
+       lemma11 = trans (lemma12 eq) ( bool-∧→tt-1 (found-p S) )
+    ... | case2 qb  |  ab  = ⊥-elim ( ab (lemma11 eq) ) where 
+       lemma11 : found-q S ≡ case2 qb → aend (automaton B) qb ≡ true
+       lemma11 refl = bool-∧→tt-1 (found-p S)
     contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
     ... | yes eq = bool-or-41 eq  -- found A ++ B all end
     ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion
        --- prove ab-case condition (we haven't checked but case2 b may happen)
        lemma11 :  (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
        lemma11 (case1 qa')  ex with found← finab ex 
-       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
-       ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (found-p S) ))  -- continued A case
-       ... | case2 qb | record { eq = refl } | nb with  bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false
-       ... | ()   
+       ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
+       ... | case1 qa2 | refl = sym ( equal→refl (afin A) (lemma12 eq) ) where -- continued A case
+           lemma12 : found-q S ≡ case1 qa2 → equal? (afin A) (δ (automaton A) qa2 h) qa' ≡ true  
+           lemma12 refl = bool-∧→tt-1 (found-p S) 
+       ... | case2 qb | nb = ⊥-elim (¬-bool refl ((lemma12 eq)) )  where --  δnfa (case2 q) i (case1 q₁) is false
+           lemma12 :  found-q S ≡ case2 qb → false ≡ true 
+           lemma12 refl = bool-∧→tt-1 (found-p S) 
        lemma11 (case2 qb)  ex with found← finab ex 
-       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
-       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail
-           lemma13 :  accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
-           lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb  
-       lemma11 (case2 qb)  ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S)
-       ... | eee = contra-position lemma12 ne where -- starting B case should fail
-           lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
-           lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )
+       ... | S with found-q S in eq | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
+       lemma11 (case2 qb)  ex | S | case2 qb' | nb = contra-position (lemma13 eq) nb where -- continued B case should fail
+           lemma13 :  found-q S ≡ case2 qb' → accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
+           lemma13 refl fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb  
+       lemma11 (case2 qb)  ex | S | case1 qa | refl with bool-∧→tt-1 (found-p S)
+       ... | eee = contra-position (lemma12 eq) ne where -- starting B case should fail
+           lemma12 : found-q S ≡ case1 qa  →  
+                accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
+           lemma12 refl fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )
 
     lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
     lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where 
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/regular-language.agda
--- a/automaton-in-agda/src/regular-language.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -53,6 +53,19 @@
 Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
 Star {Σ} x y = repeat x y
 
+-- We have to prove definitions of Concat and Star are equivalent to the set theoretic definitions
+
+-- 1.  A ∪ B = { x | x ∈ A \/ x ∈ B }
+-- 2.  A ∘ B = { x | ∃ y ∈ A, z ∈ B, x = y ++ z }
+-- 3.  A* = { x | ∃ n ∈ ℕ, y1, y2, ..., yn ∈ A, x = y1 ++ y2 ++ ... ++ yn }
+
+-- lemma-Union : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) → Union A B x ≡ ( A x \/ B x )
+-- lemma-Union = ?
+
+-- lemma-Concat : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) 
+--    → Concat A B x ≡ ( ∃ λ y → ∃ λ z → A y /\ B z /\ x ≡ y ++ z )
+-- lemma-Concat = ?
+
 open import automaton-ex
 
 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
@@ -119,3 +132,84 @@
    lemma1 [] qa qb = refl
    lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
 
+
+       
+record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
+    field
+        sp0 sp1 : List Σ
+        sp-concat : sp0 ++ sp1 ≡ x
+        prop0 : A sp0 ≡ true
+        prop1 : B sp1 ≡ true
+
+open Split
+
+list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
+list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
+list-empty++ [] (x ∷ y) ()
+list-empty++ (x ∷ x₁) y ()
+
+open _∧_
+
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+
+c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
+   → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
+   → split (λ t1 → A (h ∷ t1)) B t ≡ true
+c-split-lemma {Σ} A B h t eq p = sym ( begin
+      true
+  ≡⟨  sym eq  ⟩
+      split A B (h ∷ t ) 
+  ≡⟨⟩
+      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
+  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩
+      false \/ split (λ t1 → A (h ∷ t1)) B t
+  ≡⟨ bool-or-1 refl ⟩
+      split (λ t1 → A (h ∷ t1)) B t
+  ∎ ) where
+     open ≡-Reasoning 
+     lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false
+     lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A )
+     lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B )
+
+split→AB :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
+split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true 
+split→AB {Σ} A B [] eq | yes eqa | yes eqb = 
+    record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
+split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
+split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
+split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
+... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
+... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
+... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
+split→AB {Σ} A B (h ∷ t ) eq  | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
+... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
+
+AB→split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
+AB→split {Σ} A B [] [] eqa eqb = begin
+       split A B [] 
+     ≡⟨⟩
+       A [] /\ B []
+     ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
+      true
+     ∎  where open ≡-Reasoning
+AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
+      split A B (h ∷ y )
+     ≡⟨⟩
+      A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
+     ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
+      true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
+     ≡⟨⟩
+      true \/ split (λ t1 → A (h ∷ t1)) B y
+     ≡⟨⟩
+      true
+     ∎  where open ≡-Reasoning
+AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
+       split A B ((h ∷ t) ++ y)  
+     ≡⟨⟩
+       A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
+     ≡⟨ cong ( λ k →  A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
+       A [] /\ B (h ∷ t ++ y) \/ true
+     ≡⟨ bool-or-3 ⟩
+      true
+     ∎  where open ≡-Reasoning
+
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/root2.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -197,8 +197,24 @@
       d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
       Rational.i r * Rational.i r  ∎ where open ≡-Reasoning
 
+-- data _≤_ : (i j : ℕ) → Set where
+--    z≤n : {n : ℕ} → zero ≤ n
+--    s≤s : {i j : ℕ} → i ≤ j → (suc i) ≤ (suc j)
+
 *<-2 : {x y z : ℕ} → z > 0  → x < y → z * x < z * y   
-*<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y
+*<-2 {zero} {suc y} {suc z} (s≤s z>0) x<y = begin
+   suc (z * zero) ≡⟨ cong suc (*-comm z _) ⟩ 
+   suc (zero * z) ≡⟨ refl ⟩ 
+   suc zero ≤⟨ s≤s z≤n ⟩ 
+   suc (y + z * suc y) ∎ where open ≤-Reasoning
+*<-2 {x} {y} {suc zero} (s≤s z>0) x<y = begin
+   suc (x + zero) ≡⟨ cong suc (+-comm x _) ⟩
+   suc x  ≤⟨ x<y ⟩
+   y  ≡⟨ +-comm zero _ ⟩
+   y + zero  ∎ where open ≤-Reasoning
+*<-2 {x} {y} {suc (suc z)} (s≤s z>0) x<y = begin
+   suc (x + (x + z * x))  <⟨ +-mono-≤-< x<y (*<-2 {x} {y} {suc z} (s≤s z≤n) x<y) ⟩
+   y + (y + z * y)  ∎ where open ≤-Reasoning
 
 r15 : {p : ℕ} → p > 1 → p < p * p
 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )
diff -r af8f630b7e60 -r a60132983557 automaton-in-agda/src/sbconst2.agda
--- a/automaton-in-agda/src/sbconst2.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/sbconst2.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,4 +1,4 @@
--- {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module sbconst2 where
 
diff -r af8f630b7e60 -r a60132983557 exercise/001.ind
diff -r af8f630b7e60 -r a60132983557 exercise/002.ind
diff -r af8f630b7e60 -r a60132983557 exercise/003.ind
diff -r af8f630b7e60 -r a60132983557 exercise/004.ind
diff -r af8f630b7e60 -r a60132983557 exercise/005.ind