Mercurial > hg > Members > kono > Proof > galois

changeset 165:16ad3c7aa287

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
should be a = a'
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Nov 2020 08:33:06 +0900
parents 85bf5c283469
children 0f3cb18beebf
files FLutil.agda
diffstat 1 files changed, 10 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Mon Nov 23 03:24:28 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 08:33:06 2020 +0900
@@ -234,24 +234,26 @@
 ∀FList zero = record { ∀list = f0 ∷# [] ; x∈∀list = af1 } where
     af1 : (x : FL zero) → Any  (_≡_ x) (cons f0 [] (Level.lift tt))
     af1 f0 = here refl
-∀FList (suc n) = record { ∀list = af4 n ≤-refl (∀FListP.∀list af0) [] fmax (Level.lift tt)
-       ; x∈∀list = λ x → af2 x  ( af4 n ≤-refl (∀FListP.∀list af0) [] fmax (Level.lift tt)) } where
+∀FList (suc n) = record { ∀list = af4 n ≤-refl (∀FListP.∀list af0) [] fmax {!!} (Level.lift tt)
+       ; x∈∀list = λ x → af2 x  ( af4 n ≤-refl (∀FListP.∀list af0) [] fmax {!!} (Level.lift tt)) } where
     af0 : ∀FListP n
     af0 = ∀FList n
     af3 : (w : Fin (suc n)) (x y : FL n) → Level.Lift Level.zero (True (x f<? y )) → (w :: x ) f< (w :: y )
     af3 w x y (Level.lift z) with x f<? y
     ... | yes x<y = f<t x<y
     af4  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n))
-        → (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1 →  FList (suc n)
-    af4 zero i<n [] y1 a fr = y1
-    af4 zero (s≤s i<n) (cons a' y x) y1 a fr =
-      af4 zero 0<s y (cons (zero :: a') y1 (af41 a fr {!!})) a' ({!!} , af41 a fr {!!} ) where 
+        → (a : FL n) → fresh (FL n) ⌊ _f<?_ ⌋ a y 
+        → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1 →  FList (suc n)
+    af4 zero i<n [] y1 a fr0 fr = y1
+    af4 zero (s≤s i<n) (cons a' y x) y1 a (lift a<a' , q) fr =
+      af4 zero 0<s y (cons (zero :: a') y1 (af41 a fr {!!})) a' {!!} ({!!} , af41 a fr {!!} ) where 
        af41 : (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) y1 → a' f< a  → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a') y1
        af41 a fr lt = ttf (f<t lt) y1 fr
-    af4 (suc i) (s≤s i<n) [] y1 a fr = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1 fmax (af42 fr) where
+    af4 (suc i) (s≤s i<n) [] y1 a fr0 fr = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1 fmax {!!} (af42 fr) where
        af42 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) y1 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (≤-trans i<n a≤sa) :: fmax) y1
        af42 = {!!}
-    af4 (suc i) (s≤s i<n) (cons a' y x) y1 a fr = af4 (suc i) (s≤s i<n) y (cons (fromℕ< (s≤s i<n) :: a') y1 {!!}) a' ({!!} , {!!} ) where -- 
+    af4 (suc i) (s≤s i<n) (cons a' y x) y1 a (lift a<a' , q) fr =
+      af4 (suc i) (s≤s i<n) y (cons (fromℕ< (s≤s i<n) :: a') y1 {!!}) a' {!!} ({!!} , {!!} ) where -- 
        af43 : (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) y1 → a' f< a
           → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a') y1
        af43 a fr lt = ttf (f<t lt) y1 fr