Mercurial > hg > Members > kono > Proof > galois

changeset 65:aeb6b588db01

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Aug 2020 14:20:51 +0900
parents 537903b159ef
children 442873eaf80b
files Putil.agda
diffstat 1 files changed, 11 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Mon Aug 24 12:55:38 2020 +0900
+++ b/Putil.agda	Mon Aug 24 14:20:51 2020 +0900
@@ -282,6 +282,17 @@
 -- FL←iso {0} perm = record { peq = λ () }
 -- FL←iso {suc n} perm = {!!}
 
+∀-FL : {n : ℕ } → Fin n → List (FL n)
+∀-FL  x  = ∀-FL1 x  where
+    ∀-FL2 : { n : ℕ } → Fin (suc n) → List (FL n)  → List (FL (suc n)) → List (FL (suc n))
+    ∀-FL2 zero [] t = t
+    ∀-FL2 zero (x ∷ fls) t = ∀-FL2 zero fls (( zero :: x )  ∷ t ) 
+    ∀-FL2 (suc x) [] t = t
+    ∀-FL2 (suc x) (y ∷ fls) t = ∀-FL2 (suc x) fls (( (suc x) :: y )  ∷ t ) 
+    ∀-FL1 : {n : ℕ } → (Fin n) →  List (FL n) 
+    ∀-FL1 zero    = []
+    ∀-FL1 (suc x) =  ∀-FL2 (suc x) ( ∀-FL1 x) []
+
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where
    lem1 : {i n : ℕ } → i ≤ n → i < suc n