# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695429532 -32400
# Node ID 42eeb9f299eb40a3db030c521746591fae861f41
# Parent  558c33f7f8e05f226a75bf0bea0e81b2e6b92fff
...

diff -r 558c33f7f8e0 -r 42eeb9f299eb src/Putil.agda
--- a/src/Putil.agda	Fri Sep 22 08:22:56 2023 +0900
+++ b/src/Putil.agda	Sat Sep 23 09:38:52 2023 +0900
@@ -442,6 +442,24 @@
    pswap-dist1 (suc zero) = refl
    pswap-dist1 (suc (suc q)) =  cong ( λ k → suc (suc k) ) refl
 
+p11 : {n : ℕ } → (y : Fin (suc n)) → 0 < toℕ y → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
+p11 {.(suc _)} zero () (s≤s z≤n)
+p11 {suc n} (suc zero) 0<y (s≤s z≤n) = refl
+p11 {suc n} (suc (suc y)) 0<y y<n = p13 where
+  p14 : toℕ (suc y) < suc n
+  p14 = y<n
+  sy<n : Data.Nat.pred (toℕ (suc y)) < n
+  sy<n = px≤py ( begin 
+     suc (suc (toℕ y))  ≡⟨ refl ⟩
+     suc (toℕ (suc y))  ≤⟨ p14 ⟩
+     suc n  ∎ ) where open ≤-Reasoning 
+  p12 : suc (fromℕ< sy<n ) ≡ suc y 
+  p12 = p11 (suc y) (s≤s z≤n) sy<n
+  p16 : fromℕ< y<n ≡ suc (fromℕ< sy<n)
+  p16 = lemma10 refl 
+  p13 : suc (fromℕ< y<n) ≡ suc (suc y)
+  p13 = cong suc (trans p16 p12  )
+
 shlem→ : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
 shlem→ perm p0=0 x px=0 = begin
           x                                  ≡⟨ sym ( inverseʳ perm ) ⟩
@@ -498,25 +516,8 @@
    p← x | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
    p← x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c)
 
-   p11 : {n : ℕ } → (y : Fin (suc n)) → 0 < toℕ y → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
-   p11 {.(suc _)} zero () (s≤s z≤n)
-   p11 {suc n} (suc zero) 0<y (s≤s z≤n) = refl
-   p11 {suc n} (suc (suc y)) 0<y y<n = p13 where
-      p14 : toℕ (suc y) < suc n
-      p14 = y<n
-      sy<n : Data.Nat.pred (toℕ (suc y)) < n
-      sy<n = px≤py ( begin 
-         suc (suc (toℕ y))  ≡⟨ refl ⟩
-         suc (toℕ (suc y))  ≤⟨ p14 ⟩
-         suc n  ∎ ) where open ≤-Reasoning 
-      p12 : suc (fromℕ< sy<n ) ≡ suc y 
-      p12 = p11 (suc y) (s≤s z≤n) sy<n
-      p16 : fromℕ< y<n ≡ suc (fromℕ< sy<n)
-      p16 = lemma10 refl 
-      p13 : suc (fromℕ< y<n) ≡ suc (suc y)
-      p13 = cong suc (trans p16 p12  )
-
    --  using "with" something binded in ≡ is prohibited
+   --  with perm ⟨$⟩ʳ (suc q) in e generates w != Inverse.to perm (suc q) of type Fin (suc n)  error
    piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
    piso← x = p02 _ _ refl refl  where
       p02 : (y z : Fin n) → p← x ≡ y → p→ y ≡ z → z ≡ x
@@ -564,7 +565,24 @@
              x ∎  
 
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
-shrink-iso {n} {perm} = record { peq = λ q → ? } 
+shrink-iso {n} {perm} = record { peq = λ q → s001 q } where
+    s001 : (x : Fin n) → shrink (pprep perm) refl ⟨$⟩ʳ x ≡ perm ⟨$⟩ʳ x
+    s001 zero with <-fcmp (suc (perm ⟨$⟩ʳ zero)) (# 0) 
+    ... | tri> ¬a ¬b c = s002 where
+        s002 :  fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡ perm ⟨$⟩ʳ zero
+        s002 = begin
+            fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
+            fromℕ< fin<n  ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ zero) fin<n ⟩ 
+            perm ⟨$⟩ʳ zero ∎ where
+               open ≡-Reasoning
+    s001 (suc x) with <-fcmp (suc (perm ⟨$⟩ʳ (suc x))) (# 0) 
+    ... | tri> ¬a ¬b c = s002 where
+        s002 :  fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡ perm ⟨$⟩ʳ (suc x)
+        s002 = begin
+            fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
+            fromℕ< fin<n  ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ (suc x)) fin<n ⟩ 
+            perm ⟨$⟩ʳ (suc x) ∎ where
+               open ≡-Reasoning
 
 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
    → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= perm
@@ -578,10 +596,7 @@
          perm ⟨$⟩ʳ zero
        ∎ where
           open ≡-Reasoning 
-    s001 = ?
-    -- s001 (suc q) with perm ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ perm ) (suc q) 
-    -- ... | zero | record {eq = e}  = ⊥-elim (sh1 perm p=0 {q} e)
-    -- ... | suc t | e = refl
+    s001 (suc q) = ?
 
 
 shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)}