Mercurial > hg > Members > kono > Proof > galois
changeset 113:d8a21c5db0e0
sym5 done but agda won'y stop
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 02 Sep 2020 18:55:15 +0900 |
| parents | 43731a549950 |
| children | eb1dcba4752e |
| files | sym5.agda |
| diffstat | 1 files changed, 104 insertions(+), 104 deletions(-) [+] |
line wrap: on
line diff
--- a/sym5.agda Wed Sep 02 11:29:04 2020 +0900 +++ b/sym5.agda Wed Sep 02 18:55:15 2020 +0900 @@ -26,7 +26,6 @@ open _∧_ -{-# TERMINATING #-} ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (proj1 (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) )) where @@ -35,8 +34,8 @@ -- (dba)⁻¹ 3021 a → b → d → a -- aec 21430 -- (aec)⁻¹ 41032 --- (abd)(cea)(dba)(aec) --- +-- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc +-- so commutator always contains abc, dba and aec open ≡-Reasoning @@ -61,43 +60,19 @@ ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) - 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 - 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 )} - (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl + -- 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 + -- 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 )} + -- (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl open _=p=_ - -- ins2distr : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → ins2 (x ∘ₚ y) i<3 j<4 =p= (ins2 x i<3 j<4 ∘ₚ ins2 y i<3 j<4) - -- ins2distr {i} {j} {x} {y} {i<3} {j<4} = record { peq = λ q → - -- ins2 (x ∘ₚ y) i<3 j<4 ⟨$⟩ʳ q - -- ≡⟨⟩ - -- ((save2 i<3 j<4 ∘ₚ (pprep (pprep (x ∘ₚ y)))) ∘ₚ flip (save2 i<3 j<4 )) ⟨$⟩ʳ q - -- ≡⟨ peq ( presp prefl ( presp (ptrans (pprep-cong pprep-dist) pprep-dist ) prefl )) q ⟩ - -- (((save2 i<3 j<4 ∘ₚ (pprep (pprep x))) ∘ₚ (pprep (pprep y))) ∘ₚ flip (save2 i<3 j<4 )) ⟨$⟩ʳ q - -- ≡⟨ peq (presp prefl (presp (psym ( record { peq = λ q → inverseˡ (save2 i<3 j<4) } )) prefl )) q ⟩ - -- (((save2 i<3 j<4 ∘ₚ (pprep (pprep x))) ∘ₚ ((flip (save2 i<3 j<4 ) ∘ₚ - -- save2 i<3 j<4 ) ∘ₚ (pprep (pprep y)))) ∘ₚ flip (save2 i<3 j<4 )) ⟨$⟩ʳ q - -- ≡⟨⟩ - -- (((save2 i<3 j<4 ∘ₚ (pprep (pprep x))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ - -- ((save2 i<3 j<4 ∘ₚ (pprep (pprep y))) ∘ₚ flip (save2 i<3 j<4 ))) ⟨$⟩ʳ q - -- ≡⟨⟩ - -- (ins2 x i<3 j<4 ∘ₚ ins2 y i<3 j<4) ⟨$⟩ʳ q - -- ∎ } abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 abc i<3 j<4 = ins2 3rot i<3 j<4 - dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4 aec : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4 - -- abc→dba : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p= dba i<3 j<4 -- abc ⁻¹ - -- abc→dba i<3 j<4 = psym ins2distr - -- dba→aec : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p= aec i<3 j<4 -- dba ⁻¹ - -- dba→aec i<3 j<4 = psym ins2distr - -- aec→abc : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p= abc i<3 j<4 -- aec ⁻¹ - -- aec→abc i<3 j<4 = psym ins2distr - record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where field dba0<3 : Fin 4 @@ -133,94 +108,119 @@ _⁻¹ : {n : ℕ } ( x : Permutation n n) → Permutation n n _⁻¹ = pinv - -- abc0 = abc z≤n z≤n -- _ _ * * * - -- dba0 = dba z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) -- _ * * * _ - -- aec0 = aec (s≤s (s≤s z≤n)) z≤n -- _ * * _ * + -- 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 ℕ) + -- tt5 i j z w x y rot t with is-=p= (ins2 rot (fin≤n i) (fin≤n j)) + -- [ ins2 (rot ∘ₚ rot) (fin≤n z) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n w) ] + -- ... | yes _ = ( toℕ i ∷ toℕ j ∷ 9 ∷ toℕ z ∷ toℕ x ∷ toℕ y ∷ toℕ w ∷ [] ) ∷ t + -- ... | no _ = t - -- abc1 = abc (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) -- _ * * * _ - -- dba1 = dba z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) -- _ * * * _ - -- aec1 = aec z≤n (s≤s z≤n) + -- open import Relation.Binary.Definitions - -- t0 = plist abc0 ∷ plist dba0 ∷ plist aec0 ∷ plist [ dba0 , aec0 ] ∷ [] - -- t1 = plist aec0 ∷ plist abc0 ∷ plist dba0 ∷ plist [ aec1 , abc1 ⁻¹ ] ∷ [] - -- tt0 : (i : Fin 4) (j : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) - -- tt0 i j x y rot = - -- plist (ins2 rot (fin≤n i) (fin≤n j)) ∷ - -- plist [ ins2 (rot ∘ₚ rot) (fin≤n i) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n j) ] ∷ [] - - tt5 : (i : Fin 4) (j : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) → List (List ℕ) - tt5 i j x y rot t with is-=p= (ins2 rot (fin≤n i) (fin≤n j)) - [ ins2 (rot ∘ₚ rot) (fin≤n i) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n j) ] - ... | yes _ = ( toℕ x ∷ toℕ y ∷ [] ) ∷ t - ... | no _ = t - - open import Relation.Binary.Definitions + -- tt2 : (i : Fin 4) (j : Fin 5) → (rot : Permutation 3 3 ) → List (List ℕ) + -- tt2 i j rot = tt3 (# 4) (# 3) (# 3) (# 4) [] where + -- tt3 : (w : Fin 5) (z : Fin 4) (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ) + -- tt3 zero zero zero zero t = ( tt5 i j zero zero zero zero rot [] ) ++ t + -- tt3 (suc w) zero zero zero t = tt3 (fin+1 w) (# 3) (# 3) (# 4) ((tt5 i j zero (suc w) zero zero rot [] ) ++ t) + -- tt3 w z zero (suc y) t = tt3 w z (# 3) (fin+1 y) ((tt5 i j z w (suc y) zero rot [] ) ++ t) + -- tt3 w z (suc x) y t = tt3 w z (fin+1 x) y ((tt5 i j z w y (suc x) rot [] ) ++ t) + -- tt3 w (suc z) zero zero t = tt3 w (fin+1 z) (# 3) (# 4) ((tt5 i j (suc z) w zero zero rot [] ) ++ t) - tt2 : (i : Fin 4) (j : Fin 5) → (rot : Permutation 3 3 ) → List (List ℕ) - tt2 i j rot = tt3 (# 3) (# 4) [] where - tt3 : (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ) - tt3 zero zero t = t - tt3 zero (suc y) t = tt3 (# 3) (fin+1 y) (( tt5 i j (suc y) zero rot [] ) ++ t) - tt3 (suc x) y t = tt3 (fin+1 x) y (( tt5 i j y (suc x) rot [] ) ++ t) - - -- tt1 = tt0 (# 0) (# 0) (# 4) (# 2) 3rot ∷ - -- tt0 (# 0) (# 1) (# 4) (# 2) 3rot ∷ - -- tt0 (# 0) (# 2) (# 0) (# 3) 3rot ∷ + -- tt4 : List (List (List ℕ)) + -- tt4 = tt2 (# 0) (# 0) (pinv 3rot) ∷ + -- tt2 (# 1) (# 0) (pinv 3rot) ∷ + -- tt2 (# 2) (# 0) (pinv 3rot) ∷ + -- tt2 (# 3) (# 0) (pinv 3rot) ∷ + -- tt2 (# 0) (# 1) (pinv 3rot) ∷ + -- tt2 (# 1) (# 1) (pinv 3rot) ∷ + -- tt2 (# 2) (# 1) (pinv 3rot) ∷ + -- tt2 (# 3) (# 1) (pinv 3rot) ∷ + -- tt2 (# 0) (# 2) (pinv 3rot) ∷ + -- tt2 (# 1) (# 2) (pinv 3rot) ∷ + -- tt2 (# 2) (# 2) (pinv 3rot) ∷ + -- tt2 (# 3) (# 2) (pinv 3rot) ∷ + -- tt2 (# 0) (# 3) (pinv 3rot) ∷ + -- tt2 (# 1) (# 3) (pinv 3rot) ∷ + -- tt2 (# 2) (# 3) (pinv 3rot) ∷ + -- tt2 (# 3) (# 3) (pinv 3rot) ∷ + -- tt2 (# 0) (# 4) (pinv 3rot) ∷ + -- tt2 (# 1) (# 4) (pinv 3rot) ∷ + -- tt2 (# 2) (# 4) (pinv 3rot) ∷ + -- tt2 (# 3) (# 4) (pinv 3rot) ∷ -- [] - tt4 = tt2 (# 0) (# 0) (3rot ∘ₚ 3rot ) ∷ - tt2 (# 1) (# 0) (3rot ∘ₚ 3rot ) ∷ - tt2 (# 2) (# 0) (3rot ∘ₚ 3rot ) ∷ - tt2 (# 3) (# 0) (3rot ∘ₚ 3rot ) ∷ - tt2 (# 0) (# 1) (3rot ∘ₚ 3rot ) ∷ - [] - - - --- 1 = [ 2 , -1 ] = ((dba ⁻¹ ∘ₚ aec ⁻¹ ) ∘ₚ dba ) ∘ₚ aec ) = -1 1 2 -1 = 1 - --- dba = abc ∘ₚ 2 = [ 1 , -1 ] = ((aec ⁻¹ ∘ₚ abc ⁻¹ ) ∘ₚ aec ) ∘ₚ dab ) = 1 2 -1 1 2 - --- aec = dba ∘ₚ -1 = [ 1 , 2 ] = ((abc ⁻¹ ∘ₚ dba ⁻¹ ) ∘ₚ abc ) ∘ₚ dba ) = 2 1 1 2 - open Triple dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) - dba-triple = {!!} - -- dba-triple z≤n z≤n = {!!} -- record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ {!!} } + dba-triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + 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 } + 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 } + 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 } + dba-triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + 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 } + dba-triple (s≤s (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 } + aec-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (pinv 3rot ) - aec-triple = {!!} - -- aec-triple z≤n z≤n = {!!} -- record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ {!!} } + aec-triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + aec-triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + aec-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 } + aec-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 } + aec-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 } + aec-triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-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 } + aec-triple (s≤s (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 } + 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 = {!!} -- ⟪ d0 , ⟪ d1 , d2 ⟫ ⟫ where - -- tc : Triple i<3 j<4 3rot - -- tc = triple i<3 j<4 - -- abc0 = abc i<3 j<4 - -- b<3 = fin≤n {3} (dba0<3 tc) - -- b<4 = fin≤n {4} (dba1<4 tc) - -- dba0 = dba b<3 b<4 - -- c<3 = fin≤n {3} (aec0<3 tc) - -- c<4 = fin≤n {4} (aec1<4 tc) - -- aec0 = aec c<3 c<4 - -- d0 : deriving (suc i) (abc i<3 j<4) - -- d0 = - -- ccong {deriving i} ( psym (abc= tc )) ( - -- comm {deriving i} {dba0} {aec0} - -- (proj1 (proj2 ( dervie-any-3rot i b<3 b<4))) - -- (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 )))) - -- d1 : deriving (suc i) (dba i<3 j<4) - -- d1 = - -- ccong {deriving i} ( psym {!!}) ( -- dba i<3 j<4 =p= [ aec0 , abc0 ] -- dba= : dba b<3 b<4 =p= [ aec0 , abc0 ] is not enough... - -- comm {deriving i} {aec0} {abc0} - -- (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 ))) - -- (proj1 ( dervie-any-3rot i i<3 j<4 ))) - -- d2 : deriving (suc i) (aec i<3 j<4) - -- d2 = - -- ccong {deriving i} ( psym {!!}) ( - -- comm {deriving i} {abc0} {dba0} - -- (proj1 ( dervie-any-3rot i i<3 j<4 )) - -- (proj1 (proj2 ( dervie-any-3rot i b<3 b<4 ) ))) + dervie-any-3rot (suc i) i<3 j<4 = ⟪ d0 , ⟪ d1 , d2 ⟫ ⟫ where + tc : Triple i<3 j<4 3rot + tc = triple i<3 j<4 + d0 : deriving (suc i) (abc i<3 j<4) + d0 = ccong {deriving i} ( psym (abc= tc)) ( + comm {deriving i} {dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))} {aec (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))} + (proj1 (proj2 ( dervie-any-3rot i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))))) + (proj2 (proj2 ( dervie-any-3rot i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)))))) + tdba = dba-triple i<3 j<4 + d1 : deriving (suc i) (dba i<3 j<4) + d1 = ccong {deriving i} ( psym (abc= tdba )) ( + comm {deriving i} {aec (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))} {abc (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))} + (proj2 (proj2 ( dervie-any-3rot i (fin≤n {3} (dba0<3 tdba) (fin≤n {4} (dba1<4 tdba) ))))) + (proj1 ( dervie-any-3rot i (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba) )))) + taec = aec-triple i<3 j<4 + d2 : deriving (suc i) (aec i<3 j<4) + d2 = ccong {deriving i} ( psym (abc= (aec-triple i<3 j<4) )) ( + comm {deriving i} {abc (fin≤n {3} (dba0<3 taec)) (fin≤n {4} (dba1<4 taec) )} {dba (fin≤n {3} (aec0<3 taec)) (fin≤n {4} (aec1<4 taec))} + (proj1 ( dervie-any-3rot i (fin≤n {3} (dba0<3 taec) (fin≤n {4} (dba1<4 taec) )))) + (proj1 (proj2 ( dervie-any-3rot i (fin≤n {3} (aec0<3 taec) (fin≤n {4} (aec1<4 taec))))))) open _=p=_ counter-example : ¬ (abc 0<3 0<4 =p= pid )