Mercurial > hg > Members > kono > Proof > galois

annotate sym5.agda @ 135:4e2d272b4bcc

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 Tue, 08 Sep 2020 12:29:58 +0900
parents 019b98d398ee
children 59d12d02dfa8
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level hiding ( suc ; zero )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Algebra
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
3 module sym5 where
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Symmetric
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
6 open import Data.Unit using (⊤ ; tt )
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
8 open import Function hiding (flip)
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
10 open import Data.Nat.Properties
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Nullary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Data.Empty
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Data.Product
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import Gutil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import Putil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Solvable using (solvable)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 open import Relation.Binary.PropositionalEquality hiding ( [_] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
20 open import Data.Fin hiding (_<_ ; _≤_ ; lift )
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
21 open import Data.Fin.Permutation hiding (_∘ₚ_)
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
22
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
23 infixr 200 _∘ₚ_
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
24 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
25
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
26 open import Data.List hiding ( [_] )
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
27 open import nat
77
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
28 open import fin
84
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
29 open import logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
30
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
31 open _∧_
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
115
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
34 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
35
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
36 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
37 -- dba 1320 d → b → a → d
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
38 -- (dba)⁻¹ 3021 a → b → d → a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
39 -- aec 21430
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
40 -- (aec)⁻¹ 41032
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
41 -- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
42 -- so commutator always contains abc, dba and aec
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
43
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
44 open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
45
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
46 open solvable
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
47 open Solvable ( Symmetric 5)
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
48 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
49 end5 x der = end sol x der
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
50
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
51 0<4 : 0 < 4
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
52 0<4 = s≤s z≤n
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
53
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
54 0<3 : 0 < 3
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
55 0<3 = s≤s z≤n
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
56
79
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
57 --- 1 ∷ 2 ∷ 0 ∷ [] abc
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
58 3rot : Permutation 3 3
79
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
59 3rot = pid {3} ∘ₚ pins (n≤ 2)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
60
85
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
61 save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
62 save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
63
79
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
64 ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
85
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
65 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 )
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
66
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
67 ins2cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → ins2 x i<3 j<4 =p= ins2 y i<3 j<4
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
68 ins2cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )}
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
69 (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
70
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
71 open _=p=_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
72
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
73 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
79
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
74 abc i<3 j<4 = ins2 3rot i<3 j<4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
75 dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
76 dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
77
87
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
78 record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
77
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
79 field
82
fcb9e29d1894 ... pleq worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
80 dba0<3 : Fin 4
fcb9e29d1894 ... pleq worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
81 dba1<4 : Fin 5
fcb9e29d1894 ... pleq worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
82 aec0<3 : Fin 4
fcb9e29d1894 ... pleq worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
83 aec1<4 : Fin 5
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
84 abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
83
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 82
diff changeset
85
85
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
86 open Triple
87
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
87 triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot
84
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
88 triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
89 triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
90 triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
91 triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
92 triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
93 triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
94 triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
95 triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
96 triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
97 triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
98 triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
99 triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
100 triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
101 triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
102 triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
103 triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
104 triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
105 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
106 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
80
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 79
diff changeset
107 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =
84
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 83
diff changeset
108 record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
109
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
110 _⁻¹ : {n : ℕ } ( x : Permutation n n) → Permutation n n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
111 _⁻¹ = pinv
79
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
112
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
113 -- tt5 : (i : Fin 4) (j : Fin 5) → (z : Fin 4) → (w : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) → List (List ℕ)
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
114 -- tt5 i j z w x y rot t with is-=p= (ins2 rot (fin≤n i) (fin≤n j))
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
115 -- [ ins2 (rot ∘ₚ rot) (fin≤n z) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n w) ]
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
116 -- ... | yes _ = ( toℕ i ∷ toℕ j ∷ 9 ∷ toℕ z ∷ toℕ x ∷ toℕ y ∷ toℕ w ∷ [] ) ∷ t
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
117 -- ... | no _ = t
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
118
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
119 -- open import Relation.Binary.Definitions
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
120
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
121 -- tt2 : (i : Fin 4) (j : Fin 5) → (rot : Permutation 3 3 ) → List (List ℕ)
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
122 -- tt2 i j rot = tt3 (# 4) (# 3) (# 3) (# 4) [] where
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
123 -- tt3 : (w : Fin 5) (z : Fin 4) (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ)
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
124 -- tt3 zero zero zero zero t = ( tt5 i j zero zero zero zero rot [] ) ++ t
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
125 -- tt3 (suc w) zero zero zero t = tt3 (fin+1 w) (# 3) (# 3) (# 4) ((tt5 i j zero (suc w) zero zero rot [] ) ++ t)
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
126 -- tt3 w z zero (suc y) t = tt3 w z (# 3) (fin+1 y) ((tt5 i j z w (suc y) zero rot [] ) ++ t)
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
127 -- tt3 w z (suc x) y t = tt3 w z (fin+1 x) y ((tt5 i j z w y (suc x) rot [] ) ++ t)
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
128 -- tt3 w (suc z) zero zero t = tt3 w (fin+1 z) (# 3) (# 4) ((tt5 i j (suc z) w zero zero rot [] ) ++ t)
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
129
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
130 -- tt4 : List (List (List ℕ))
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
131 -- tt4 = tt2 (# 0) (# 0) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
132 -- tt2 (# 1) (# 0) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
133 -- tt2 (# 2) (# 0) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
134 -- tt2 (# 3) (# 0) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
135 -- tt2 (# 0) (# 1) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
136 -- tt2 (# 1) (# 1) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
137 -- tt2 (# 2) (# 1) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
138 -- tt2 (# 3) (# 1) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
139 -- tt2 (# 0) (# 2) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
140 -- tt2 (# 1) (# 2) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
141 -- tt2 (# 2) (# 2) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
142 -- tt2 (# 3) (# 2) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
143 -- tt2 (# 0) (# 3) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
144 -- tt2 (# 1) (# 3) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
145 -- tt2 (# 2) (# 3) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
146 -- tt2 (# 3) (# 3) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
147 -- tt2 (# 0) (# 4) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
148 -- tt2 (# 1) (# 4) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
149 -- tt2 (# 2) (# 4) (pinv 3rot) ∷
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
150 -- tt2 (# 3) (# 4) (pinv 3rot) ∷
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
151 -- []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
152
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
153 open Triple
87
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
154 dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot )
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
155 dba-triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
156 dba-triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
157 dba-triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
158 dba-triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
159 dba-triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
160 dba-triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
161 dba-triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
162 dba-triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
163 dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
164 dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
165 dba-triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
166 dba-triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
167 dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
168 dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
169 dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
170 dba-triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
171 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
172 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
173 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
174 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
175 record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
176
115
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
177 -3=33 : pinv 3rot =p= (3rot ∘ₚ 3rot )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
178 -3=33 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
179
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
180 4=1 : (3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot ) =p= 3rot
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
181 4=1 = pleq _ _ refl
87
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
182
114
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
183 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
184 → deriving n (abc i<3 j<4 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
185 dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
186 → deriving n (dba i<3 j<4 )
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
187
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
188 commd : {n : ℕ } → (f g : Permutation 5 5)
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
189 → deriving n f
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
190 → deriving n g
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
191 → Commutator (deriving n) [ f , g ]
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
192 commd {n} f g df dg = comm {deriving n} {f} {g} df dg
114
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
193
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
194 dervie-any-3rot0 0 i<3 j<4 = lift tt
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
195 dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
196 tc = triple i<3 j<4
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
197 dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
198 aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
117
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
199 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
200 -- abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
201 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
202 ceq' : ins2 3rot i<3 j<4 =p= [ ins2 (3rot ∘ₚ 3rot) (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) , ins2 (3rot ∘ₚ 3rot) (fin≤n {3} (aec0<3 tc )) (fin≤n {4} (aec1<4 tc)) ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
203 ceq' = abc= tc
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
204 ceq : abc i<3 j<4 =p= [ dba0 , aec0 ]
118
019b98d398ee sym5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
205 ceq = record { peq = peq (abc= tc) }
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
206 df = dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
207 dg = dervie-any-3rot1 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
114
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
208
115
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
209 dervie-any-3rot1 0 i<3 j<4 = lift tt
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
210 dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong {deriving n} ( psym ceq ) (commd aec0 abc0 df dg ) where
113
d8a21c5db0e0 sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
211 tdba = dba-triple i<3 j<4
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
212 aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
213 abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
214 ceq : dba i<3 j<4 =p= [ aec0 , abc0 ]
118
019b98d398ee sym5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
215 ceq = record { peq = peq (abc= tdba) }
116
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
216 df : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
217 df = deriving-subst (psym (ins2cong {toℕ (dba0<3 (dba-triple i<3 j<4))} {toℕ (dba1<4 (dba-triple i<3 j<4))} 4=1 ))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
218 (dervie-any-3rot0 n (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
219 dg : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
220 dg = deriving-subst (psym (ins2cong {toℕ (aec0<3 (dba-triple i<3 j<4))} {toℕ (aec1<4 (dba-triple i<3 j<4))} 4=1 ))
6022d00a0690 check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
221 (dervie-any-3rot0 n (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)))
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
222
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
223 open _=p=_
77
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
224 counter-example : ¬ (abc 0<3 0<4 =p= pid )
85
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
225 counter-example eq with ←pleq _ _ eq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
226 ... | ()
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
227
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
228