Mercurial > hg > Members > kono > Proof > galois

changeset 163:d3d2083643d6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Nov 2020 02:35:37 +0900
parents 57d475583f74
children 85bf5c283469
files FLutil.agda
diffstat 1 files changed, 7 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Mon Nov 23 00:48:18 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 02:35:37 2020 +0900
@@ -234,24 +234,21 @@
 ∀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) []
+∀FList (suc n) = record { ∀list = af4 n ≤-refl (∀FListP.∀list af0) [] 
        ; x∈∀list = λ x → af2 x  ( af4 n ≤-refl (∀FListP.∀list af0) [] ) } 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
-    af4r : (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
-    af4r zero i<n y [] a = Level.lift tt
-    af4r zero i<n y (cons a₁ y1 x) a = {!!} , af4r zero i<n y y1 a 
-    af4r (suc i) i<n y [] a = Level.lift tt
-    af4r (suc i) i<n y (cons a₁ y1 x) a = {!!} , af4r (suc i) i<n y y1 a 
+    af4r  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n))
+         → (a : FL n) →  fresh (FL (n)) ⌊ _f<?_ ⌋ a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1
+    af4r = {!!}
     af4  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n)) →  FList (suc n)
     af4 zero i<n [] y1 = y1
-    af4 (suc i) (s≤s i<n) [] y1 = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1
-    af4 zero (s≤s i<n) (cons a y x) y1 = af4 zero 0<s y (cons (fromℕ< (s≤s i<n) :: a) y1 (af4r zero (s≤s i<n) y y1 a))
-    af4 (suc i) (s≤s i<n) (cons a y x) y1 = af4 i (≤-trans i<n a≤sa) y (cons (fromℕ< (s≤s i<n) :: a) y1 (af4r (suc i) (s≤s i<n) y y1 a))
+    af4 zero (s≤s i<n) (cons a' y x) y1 = af4 zero 0<s y (cons (zero :: a') y1 (af4r zero 0<s y y1 a' x))
+    af4 (suc i) (s≤s i<n) [] y1 = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1 
+    af4 (suc i) (s≤s i<n) (cons a' y x) y1 = af4 (suc i) (s≤s i<n) y (cons (fromℕ< (s≤s i<n) :: a') y1 (af4r (suc i) (s≤s i<n) y y1 a' x))
     af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y
     af2 = {!!}