Mercurial > hg > Members > kono > Proof > galois
changeset 84:7e36bd8916a9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 26 Aug 2020 23:53:40 +0900 |
| parents | f2edc816740b |
| children | 2d79a2c06c6c |
| files | sym5.agda |
| diffstat | 1 files changed, 76 insertions(+), 68 deletions(-) [+] |
line wrap: on
line diff
--- a/sym5.agda Wed Aug 26 19:53:24 2020 +0900 +++ b/sym5.agda Wed Aug 26 23:53:40 2020 +0900 @@ -22,9 +22,12 @@ open import Data.List hiding ( [_] ) open import nat open import fin +open import logic + +open _∧_ ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) -¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where +¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (proj1 (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) )) where -- -- dba 1320 d → b → a → d @@ -71,87 +74,92 @@ abc= : abc i<3 j<4 =p= [ dba (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , aec (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] 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 ∷ []) ∷ 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 ∷ ∷ []) ∷ - ∷ plist ( abc (n≤ 1) (n≤ 0) ) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ - ∷ plist ( abc (n≤ 1) (n≤ 1) ) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ - ∷ plist ( abc (n≤ 1) (n≤ 2) ) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ - ∷ plist ( abc (n≤ 1) (n≤ 3) ) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ - ∷ plist ( abc (n≤ 1) (n≤ 4) ) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ - ∷ plist ( abc (n≤ 2) (n≤ 0) ) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ - ∷ plist ( abc (n≤ 2) (n≤ 1) ) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ - ∷ plist ( abc (n≤ 2) (n≤ 2) ) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ - ∷ plist ( abc (n≤ 2) (n≤ 3) ) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ - ∷ plist ( abc (n≤ 2) (n≤ 4) ) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ - ∷ plist ( abc (n≤ 3) (n≤ 0) ) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ - ∷ plist ( abc (n≤ 3) (n≤ 1) ) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ - ∷ plist ( abc (n≤ 3) (n≤ 2) ) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ - ∷ plist ( abc (n≤ 3) (n≤ 3) ) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ - ∷ plist ( abc (n≤ 3) (n≤ 4) ) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ [] + -- a b c d e + t1 = (plist ( abc (n≤ 0) (n≤ 0) ) ++ ( 0 ∷ 0 ∷ [])) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ cde no 4 on top + -- ∷ (plist ( abc (n≤ 0) (n≤ 1) ) ++ ( 0 ∷ 1 ∷ [])) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 0) (n≤ 2) ) ++ ( 0 ∷ 2 ∷ [])) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 0) (n≤ 3) ) ++ ( 0 ∷ 3 ∷ [])) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ 120 : aec + -- ∷ (plist ( abc (n≤ 0) (n≤ 4) ) ++ ( 0 ∷ 4 ∷ [])) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ 342 : dba, (open c, put 1st) + ∷ (plist ( abc (n≤ 1) (n≤ 0) ) ++ ( 1 ∷ 0 ∷ [])) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ + ∷ (plist ( abc (n≤ 1) (n≤ 1) ) ++ ( 1 ∷ 1 ∷ [])) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 1) (n≤ 2) ) ++ ( 1 ∷ 2 ∷ [])) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 1) (n≤ 3) ) ++ ( 1 ∷ 3 ∷ [])) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 1) (n≤ 4) ) ++ ( 1 ∷ 4 ∷ [])) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ 120 dba , 340 : dba + -- ∷ (plist ( abc (n≤ 2) (n≤ 0) ) ++ ( 2 ∷ 0 ∷ [])) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ 342 : aec (open b, put 2nd) + -- ∷ (plist ( abc (n≤ 2) (n≤ 1) ) ++ ( 2 ∷ 1 ∷ [])) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 2) (n≤ 2) ) ++ ( 2 ∷ 2 ∷ [])) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ 340 : aec -- 1 3 3 4 + -- ∷ (plist ( abc (n≤ 2) (n≤ 3) ) ++ ( 2 ∷ 3 ∷ [])) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 2) (n≤ 4) ) ++ ( 2 ∷ 4 ∷ [])) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 3) (n≤ 0) ) ++ ( 3 ∷ 0 ∷ [])) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 3) (n≤ 1) ) ++ ( 3 ∷ 1 ∷ [])) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 3) (n≤ 2) ) ++ ( 3 ∷ 2 ∷ [])) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 3) (n≤ 3) ) ++ ( 3 ∷ 3 ∷ [])) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ + -- ∷ (plist ( abc (n≤ 3) (n≤ 4) ) ++ ( 3 ∷ 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 ∷ ∷ ∷ []) ∷ [] - ∷ [] + t8 : ( i : Fin 4 ) → (j : Fin 5) → List ( List ℕ ) + t8 i j = ((plist [ dba (n≤ 0) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] ) ++ (8 ∷ 0 ∷ 0 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 0) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 1 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 0) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 2 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 0) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 3 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 0) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 4 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 1) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 0 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 1) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 1 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 1) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 2 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 1) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 3 ∷ [] )) -- + ∷ ((plist ( [ dba (n≤ 1) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 4 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 2) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 0 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 2) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 1 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 2) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 2 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 2) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 3 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 2) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 4 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 3) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 0 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 3) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 1 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 3) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 2 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 3) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 4 ∷ [] )) + ∷ ((plist ( [ dba (n≤ 3) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 4 ∷ [] )) + ∷ [] + t88 = t1 ++ t8 (# 3) (# 1) + ++ t8 (# 3) (# 2) + ++ t8 (# 3) (# 3) + ++ t8 (# 3) (# 4) --- 1 ∷ 2 ∷ 0 ∷ ∷ ∷ [] abc -- abc (n≤ 3) (n≤ 4) --- 3 ∷ 0 ∷ ∷ 1 ∷ ∷ [] dba - dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 2) + dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 4) --- 4 ∷ ∷ 0 ∷ ∷ 2 ∷ [] aec - aec99 = ins2 (pinv 3rot) (n≤ 1) (n≤ 4) + aec99 = ins2 (pinv 3rot) (n≤ 0) (n≤ 3) tt1 = plist dba99 ∷ plist (pinv dba99) ∷ [] tt2 = plist aec99 ∷ plist (pinv aec99) ∷ [] tt5 = plist [ dba99 , aec99 ] -- =p= abc - 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= = {!!} } - triple z≤n (s≤s z≤n) = {!!} - triple z≤n (s≤s (s≤s z≤n)) = {!!} - triple z≤n (s≤s (s≤s (s≤s z≤n))) = {!!} - triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!} - triple (s≤s z≤n) z≤n = {!!} - triple (s≤s z≤n) (s≤s z≤n) = {!!} - triple (s≤s z≤n) (s≤s (s≤s z≤n)) = {!!} - triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = {!!} - triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!} - triple (s≤s (s≤s z≤n)) z≤n = {!!} - triple (s≤s (s≤s z≤n)) (s≤s z≤n) = {!!} - triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = {!!} - triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = {!!} - triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!} - triple (s≤s (s≤s (s≤s z≤n))) z≤n = {!!} - triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = {!!} - triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = {!!} - triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = {!!} + triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + 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 } + 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 } + 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 } + triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } triple (s≤s (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 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } - dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 ) - dervie-any-3rot 0 i<3 j<4 = lift tt + dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) + → deriving n (abc i<3 j<4 ) ∧ deriving n (dba i<3 j<4 ) ∧ deriving n (aec i<3 j<4 ) + dervie-any-3rot 0 i<3 j<4 = ⟪ lift tt , ⟪ lift tt , lift tt ⟫ ⟫ dervie-any-3rot (suc i) i<3 j<4 = {!!} -- ccong {deriving i} ( abc= (triple i<3 j<4 ) ) ( -- comm {deriving i} {dba} {aec}