Members/kono/Proof/galois: FL.agda comparison

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 10 Sep 2020 20:55:19 +0900
parents	35c0b6878863
children	029a7885fe57

comparison

equal deleted inserted replaced

-:35c0b6878863
+:435159e2897a
 FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf a x lt y  x₁)
 ... | inj₂ (case1 eq) = cons a y x₁
 FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
 ... | [] | ()
 ... | cons a₁ t x₂ | e = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
-FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) = ttf2 a a₁ x (FLinsert x (cons a₁ y x₂)) where
+FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) with FLinsert x (cons a₁ y x₂)
-ttf2 : {n : ℕ } → (a a₁ x : FL (suc n))  → ( y : FList {suc n} ) → FList {suc n}
+... | [] = cons a (cons x ( cons a₁ [] (Level.lift tt) ) {!!} ) {!!}
-ttf2 a a₁ x [] = cons a (cons x ( cons a₁ [] (Level.lift tt) ) {!!} ) {!!}
+... | cons a₂ t x₁ = cons a ( cons a₂ t x₁) ( Level.lift (fromWitness (ttf2 {!!} {!!})) , ( ttf a₂ a (ttf2 {!!} {!!} ) t x₁ )) where
-ttf2 a a₁ x (cons a₂ t x₁) = cons a ( cons a₂ t x₁) ( {!!} , ( ttf x a ? t {!!}) )
+ttf2 :  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t → a f< a₂
+ttf2 = {!!}
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1

Mercurial > hg > Members > kono > Proof > galois