Mercurial > hg > Members > kono > Proof > galois
changeset 62:a66f773330b4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Aug 2020 12:41:57 +0900 |
| parents | c16749815259 |
| children | d730fb6eea89 |
| files | Putil.agda |
| diffstat | 1 files changed, 4 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Mon Aug 24 12:04:25 2020 +0900 +++ b/Putil.agda Mon Aug 24 12:41:57 2020 +0900 @@ -61,22 +61,22 @@ p→ : Fin (suc (suc n)) → Fin (suc (suc n)) p→ zero = suc zero p→ (suc zero) = zero - p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) + p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) p← : Fin (suc (suc n)) → Fin (suc (suc n)) p← zero = suc zero p← (suc zero) = zero - p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) + p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x piso← zero = refl piso← (suc zero) = refl - piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) + piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x piso→ zero = refl piso→ (suc zero) = refl - piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) + piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) -- enumeration @@ -92,7 +92,6 @@ -- -- psawpim (inseert swap at position m ) --- not easy to write directory beacause left-inverse-of may contains Fin relations -- psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) )