Mercurial > hg > Members > kono > Proof > galois

changeset 181:7423f0fc124a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... almost ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Nov 2020 08:58:12 +0900
parents d631469259f2
children eb94265d2a39
files FLutil.agda
diffstat 1 files changed, 7 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Thu Nov 26 08:10:06 2020 +0900
+++ b/FLutil.agda	Thu Nov 26 08:58:12 2020 +0900
@@ -234,22 +234,20 @@
 Ffresh0 : {n : ℕ } → (i<n : zero < suc n) → (a : FL n) → (x z : FList n )
     →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) (Flist zero i<n x z)
 Ffresh1 : {n : ℕ } → (i : ℕ) → (i<n : i < suc n) → 0 < i → (a : FL n) → (x z : FList n )
-    →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (Flist i i<n x z)
+     →  (a₂ : FL (suc n)) (t : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t 
+     →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) t
 Flist zero i<n [] _ = []
 Flist zero i<n (cons a x xr) z  = cons ( zero :: a ) (Flist zero i<n x z ) (Ffresh0 i<n a x z xr)
 Flist (suc i) (s≤s i<n) [] z  = Flist i (<-trans i<n a<sa) z z 
-Flist (suc i) i<n (cons a x xr) z  = cons ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z ) (Ffresh1 (suc i) i<n 0<s a x z xr)
+Flist (suc i) (s≤s i<n) (cons a [] xr) z = cons ((fromℕ< (s≤s i<n)) :: a) (Flist i (<-trans i<n a<sa) z z)  {!!}
+Flist (suc i) (s≤s i<n) (cons a (cons a₁ x x₁) xr) z with Flist (suc i) (s≤s i<n) x z 
+... | [] = cons ((fromℕ< (s≤s i<n)) :: a) [] (Level.lift tt)
+... | cons a₂ t x₂ = cons ((fromℕ< (s≤s i<n)) :: a) t (Ffresh1 (suc i) (s≤s i<n) 0<s a x z a₂ t x₂ ?)
 Ffresh0 i<n a [] z xr = Level.lift tt
 Ffresh0 i<n a (cons a₁ x x₁) z (lift a<a₁ , ar) = Fr0 , Ffresh0 i<n a x z ar where
    Fr0 : ⌊ _f<?_ ⌋ (zero :: a) (zero :: a₁)
    Fr0 = Level.lift (fromWitness (f<t (toWitness a<a₁)))
-Ffresh1 zero i<n () a [] z xr 
-Ffresh1 (suc i) (s≤s i<n) a _ [] z (Level.lift tt) with Flist i (<-trans i<n a<sa) z z 
-... | [] = Level.lift tt
-... | cons a₁ t x = {!!} , ttf {!!} t x
-Ffresh1 zero i<n () a (cons a₁ x xr) z (a<a₁ , ar) 
-Ffresh1 {n} (suc i) i<n _ a (cons a₁ x xr) z (a<a₁ , ar) with Ffresh1 {n} (suc i) i<n 0<s a x z ar  --  (suc (fromℕ< (≤-pred i<n)) :: a) (Flist (suc i) i<n x z)
-... | t = {!!} -- (suc (fromℕ< (≤-pred i<n)) :: a) (Flist (suc i) i<n (cons a₁ x xr) z)
+Ffresh1 = {!!}
 
 ∀Flist : {n : ℕ } → FL n → FList n
 ∀Flist {zero} f0 = f0 ∷# []