Mercurial > hg > Members > kono > Proof > galois

changeset 110:cb3281e83229

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FL iso done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 01 Sep 2020 20:41:38 +0900
parents 5d60a060453c
children d3da6e2c0d90
files Putil.agda
diffstat 1 files changed, 4 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Tue Sep 01 20:00:24 2020 +0900
+++ b/Putil.agda	Tue Sep 01 20:41:38 2020 +0900
@@ -642,17 +642,13 @@
         FL→perm ( perm→FL perm  ) ⟨$⟩ʳ q
      ≡⟨⟩
         (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )))  ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ) ) ⟨$⟩ʳ q
-     ≡⟨  peq (presp (pprep-cong (FL←iso _ ) ) prefl ) q  ⟩
+     ≡⟨  peq (presp {suc n} {_} {_} {pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))} (pprep-cong {n} {FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ))} (FL←iso _ ) ) prefl ) q  ⟩
          (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))   ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
-     ≡⟨  peq (passoc _ _ _  ) q ⟩
-         (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))) ⟨$⟩ʳ ((  pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q )
-     ≡⟨ peq (shrink-iso2 (p=0 perm)) ((pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q) ⟩
+     ≡⟨ peq (presp {suc n} {pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))} {perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))} {pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )} (shrink-iso2 (p=0 perm)) prefl) q  ⟩
          ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
-     ≡⟨ peq (passoc _ _ _ ) q ⟩
-         (perm ∘ₚ (flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )))  ⟨$⟩ʳ q 
-     ≡⟨ {!!}  ⟩
+     ≡⟨ peq (presp {suc n} {perm} {_} {flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))} {pid} prefl record { peq = λ q → inverseʳ (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) }) q  ⟩
         ( perm ∘ₚ pid ) ⟨$⟩ʳ q
-     ≡⟨ {!!}  ⟩
+     ≡⟨⟩
         perm ⟨$⟩ʳ q
      ∎  ) }