Mercurial > hg > Members > kono > Proof > galois
changeset 64:537903b159ef
postulate
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Aug 2020 12:55:38 +0900 |
| parents | d730fb6eea89 |
| children | aeb6b588db01 |
| files | Putil.agda |
| diffstat | 1 files changed, 4 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Mon Aug 24 12:47:31 2020 +0900 +++ b/Putil.agda Mon Aug 24 12:55:38 2020 +0900 @@ -251,12 +251,13 @@ -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) )) ∷ [] -postulate - p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 +-- postulate +-- p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 perm→FL : {n : ℕ } → Permutation n n → FL n perm→FL {zero} perm = f0 -perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) +perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) +-- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) -- t5 = plist t4 ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 3 ) )) t5 = plist (t4) ∷ plist (flip t4)