Mercurial > hg > Members > kono > Proof > galois
changeset 175:0394bc762a49
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Nov 2020 06:15:09 +0900 |
| parents | 8e8238b26ee7 |
| children | cf7622b185a6 |
| files | FLutil.agda |
| diffstat | 1 files changed, 11 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/FLutil.agda Tue Nov 24 15:59:42 2020 +0900 +++ b/FLutil.agda Wed Nov 25 06:15:09 2020 +0900 @@ -246,12 +246,15 @@ fr9 : FList 3 fr9 = ∀Flist fmax -∀Flist' : (n : ℕ ) → FList n -∀Flist' n = ∀Flist0' n n FL0 {!!} where - ∀Flist0' : (i j : ℕ) → (x : FL n) → x f< fmax → FList n - ∀Flist0' zero zero x _ = [] - ∀Flist0' zero (suc j) x lt = ∀Flist0' j j fmax {!!} - ∀Flist0' (suc i) j x lt = cons (fsuc x lt) (∀Flist0' i j (fsuc x lt) {!!} ) {!!} +∀F1 : {n : ℕ } → FL (suc n) → Fin n → FList (suc n) → FList (suc n) +∀F1 _ _ [] L = L +∀F1 y (cons x t xr) L = ∀F1 y t (cons (fin+1 y :: x) L ? ) + +∀Flist' : (n : ℕ ) → FL n → FList n → FList n +∀Flist' zero f0 L = L +∀Flist' (suc n) (zero :: y) L = ∀F1 zero (∀Flist' n []) L +∀Flist' (suc n) (suc x :: y) L = + ∀Flist' (suc n) (x :: y) ( ∀F1 (suc x) ( ∀Flist' n y []) L ) -- open import Size -- @@ -269,8 +272,8 @@ open import Data.List.Fresh.Relation.Unary.Any open import Data.List.Fresh.Relation.Unary.All -AnyFList' : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) (∀Flist' n) -AnyFList' 0 f0 = ? +AnyFList' : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) {!!} -- (∀Flist' n fmax) +AnyFList' 0 f0 = {!!} AnyFList' (suc n) (x :: y) = {!!} x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs)