# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598439204 -32400
# Node ID f2edc816740b44ca12b67d53d73399f3ac7805ff
# Parent  fcb9e29d189424825bc636b3c0137f60122d9a5d
...

diff -r fcb9e29d1894 -r f2edc816740b fin.agda
--- a/fin.agda	Wed Aug 26 19:21:42 2020 +0900
+++ b/fin.agda	Wed Aug 26 19:53:24 2020 +0900
@@ -2,7 +2,7 @@
 
 module fin where
 
-open import Data.Fin hiding (_<_)
+open import Data.Fin hiding (_<_ ; _≤_ )
 open import Data.Nat
 open import logic
 open import nat
@@ -22,6 +22,10 @@
 fin<n {_} {zero} = s≤s z≤n
 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
 
+fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
+fin≤n {_} zero = z≤n
+fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)
+
 pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0  → Data.Nat.pred (toℕ f) < n
 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
 pred<n {suc n} {suc f} (s≤s z≤n) = fin<n
diff -r fcb9e29d1894 -r f2edc816740b sym5.agda
--- a/sym5.agda	Wed Aug 26 19:21:42 2020 +0900
+++ b/sym5.agda	Wed Aug 26 19:53:24 2020 +0900
@@ -62,10 +62,6 @@
      aec : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
      aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4
 
-     fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
-     fin≤n {_} zero = z≤n
-     fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)
-
      record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where
        field 
          dba0<3 : Fin 4
@@ -77,7 +73,7 @@
      open Triple
      --                                    d   e   a   b   c
      t1 = plist ( abc (n≤ 0) (n≤ 0) )  -- (  ∷   ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷    no 4 on top
-       ∷  plist ( abc (n≤ 0) (n≤ 1) )  -- (  ∷   ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ 
+        ∷  plist ( abc (n≤ 0) (n≤ 1) )  -- (  ∷   ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷    342 043 312
        ∷  plist ( abc (n≤ 0) (n≤ 2) )  -- (3 ∷   ∷   ∷ 4 ∷ 0 ∷ []) ∷
        ∷  plist ( abc (n≤ 0) (n≤ 3) )  -- (2 ∷   ∷ 4 ∷   ∷ 0 ∷ []) ∷   
        ∷  plist ( abc (n≤ 0) (n≤ 4) )  -- (2 ∷   ∷ 3 ∷ 0 ∷   ∷ []) ∷  
@@ -98,28 +94,37 @@
        ∷  plist ( abc (n≤ 3) (n≤ 4) )  -- (1 ∷ 2 ∷ 0 ∷   ∷   ∷ []) ∷ []
        ∷ []
 
+     td = plist ( dba (n≤ 0) (n≤ 0) ) -- (  ∷   ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 0) (n≤ 1) ) -- (  ∷   ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 0) (n≤ 2) ) -- (4 ∷   ∷   ∷ 0 ∷ 3 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 0) (n≤ 3) ) -- (4 ∷   ∷ 0 ∷   ∷ 2 ∷ []) ∷                                
+       ∷  plist ( dba (n≤ 0) (n≤ 4) ) -- (3 ∷   ∷ 0 ∷ 2 ∷   ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 1) (n≤ 0) ) -- (  ∷ 4 ∷   ∷ 1 ∷ 3 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 1) (n≤ 1) ) -- (  ∷ 4 ∷   ∷ 1 ∷ 3 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 1) (n≤ 2) ) -- (4 ∷   ∷   ∷ 0 ∷ 3 ∷ []) ∷                                
+       ∷  plist ( dba (n≤ 1) (n≤ 3) ) -- (4 ∷ 0 ∷   ∷   ∷ 1 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 1) (n≤ 4) ) -- (3 ∷ 0 ∷   ∷ 1 ∷   ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 2) (n≤ 0) ) -- (  ∷ 4 ∷ 1 ∷   ∷ 2 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 2) (n≤ 1) ) -- (  ∷ 4 ∷ 1 ∷   ∷ 2 ∷ []) ∷                                
+       ∷  plist ( dba (n≤ 2) (n≤ 2) ) -- (4 ∷   ∷ 0 ∷   ∷ 2 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 2) (n≤ 3) ) -- (4 ∷ 0 ∷   ∷   ∷ 1 ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 2) (n≤ 4) ) -- (2 ∷ 0 ∷ 1 ∷   ∷   ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 3) (n≤ 0) ) -- (  ∷ 3 ∷ 1 ∷ 2 ∷   ∷ []) ∷                                
+       ∷  plist ( dba (n≤ 3) (n≤ 1) ) -- (  ∷ 3 ∷ 1 ∷ 2 ∷   ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 3) (n≤ 2) ) -- (3 ∷   ∷ 0 ∷ 2 ∷   ∷ []) ∷                               
+       ∷  plist ( dba (n≤ 3) (n≤ 3) ) -- (3 ∷ 0 ∷   ∷ 1 ∷   ∷ []) ∷ 
+       ∷  plist ( dba (n≤ 3) (n≤ 4) ) -- (2 ∷ 0 ∷ 1 ∷   ∷   ∷ []) ∷ [] 
+       ∷ []
+
 
      --- 1 ∷ 2 ∷ 0 ∷   ∷   ∷ []      abc    --  abc (n≤ 3) (n≤ 4)
      --- 3 ∷ 0 ∷   ∷ 1 ∷   ∷ []      dba
-     dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 4)
+     dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 2)
      --- 4 ∷   ∷ 0 ∷   ∷ 2 ∷ []      aec
-     aec99 = ins2 (pinv 3rot) (n≤ 0) (n≤ 3)
+     aec99 = ins2 (pinv 3rot) (n≤ 1) (n≤ 4)
      tt1 = plist dba99 ∷ plist (pinv dba99) ∷ []
      tt2 = plist aec99 ∷ plist (pinv aec99) ∷ []
      tt5 = plist  [ dba99 , aec99  ]  -- =p=  abc  
-     tt6 : [ dba99 , aec99  ]  =p=  abc (n≤ 3) (n≤ 4)
-     tt6 = record { peq = λ q → lll q } where
-        lll : (q : Fin 5) →  ([ dba99 , aec99 ] ⟨$⟩ʳ q) ≡ (abc (n≤ 3) (n≤ 4) ⟨$⟩ʳ q)
-        lll zero = refl
-        lll (suc zero) = refl
-        lll (suc (suc zero)) = refl
-        lll (suc (suc (suc zero))) = refl
-        lll (suc (suc (suc (suc zero)))) = refl
-     tt8  = plist ( dba (fin<n  {3} {# 0}) (fin<n  {4} {# 3}))
-     tt9  : fin<n  {4} {# 3} ≡ n≤ 4
-     tt9  = refl
-     tta  : fin≤n  {3} (# 1) ≡ n≤ 1
-     tta  = refl
 
      triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4
      triple z≤n z≤n = record { dba0<3 = {!!} ; dba1<4 = {!!} ; aec0<3 = {!!} ; aec1<4 = {!!} ; abc= = {!!} }