# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595334778 -32400
# Node ID c3a0fb13e2676cd30fc2b0fdcd63f6b0ca016b15
# Parent  d2cb5278e46d9ea615e7604b4dfda8167fa52fc6
...

diff -r d2cb5278e46d -r c3a0fb13e267 filter.agda
--- a/filter.agda	Tue Jul 21 14:34:27 2020 +0900
+++ b/filter.agda	Tue Jul 21 21:32:58 2020 +0900
@@ -359,29 +359,49 @@
 _3↑_ : (Nat → Two) → Nat → List Three
 f 3↑ x = ↑app f x [] 
 
-listn : Nat → List Nat
-listn 0 = []
-listn (Suc n) = n ∷ listn n
+3↑22 : (f : Nat → Two) (i j : Nat) → List Three
+3↑22 f Zero j = []
+3↑22 f (Suc i) j with f i
+3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j)
+3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j)
+
+3↑2 : (Nat → Two) → Nat → List Three
+3↑2 f i = 3↑22 f i 0 
 
-rev : {A : Set} → List A → List A
-rev {A} x = rev1 x [] where
-    rev1 : List A → List A → List A
-    rev1 [] y = y
-    rev1 (h ∷ x) y = rev1 x (h ∷ y)
+lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t))
+lemma10 s t eq = eq 
+lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t))
+lemma11 s t eq = eq
+lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
+lemma12 s t eq = eq
+lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
+lemma13 s t eq = eq
+lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
+lemma14 s t eq = eq
 
-Lmap : {A B : Set} → (A → B ) → List A → List B
-Lmap f [] = []
-Lmap f (h ∷ t) = f h ∷ Lmap f t
-
-3↑1 : (Nat → Two) → Nat → List Three
-3↑1 f i with f i
-... | i0 = Lmap (λ x → j0) (rev ( listn i ))
-... | i1 = Lmap (λ x → j1) (rev ( listn i ))
-
-3↑<1 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑1 f x)  3⊆ (3↑1 f y)
-3↑<1 {f} {x} {y} x<y  = lemma (rev ( listn x )) where
-     lemma : (z : List Nat ) → {!!}
-     lemma = {!!}
+3↑<2 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x)  3⊆ (3↑2 f y)
+3↑<2 {f} {x} {y} x<y  = lemma x 0 y x<y (3↑22 f x 0)  (3↑22 f y 0) where
+    lemma :  (i j y : Nat) → i ≤ y → (s t : List Three) → s  3⊆  t
+    lemma Zero j y z≤n [] [] = refl
+    lemma Zero j y z≤n [] (x ∷ t) = 3⊆-[] {x ∷ t}
+    lemma Zero j y z≤n (x ∷ s) [] = {!!}
+    lemma Zero j y z≤n (j0 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
+    lemma Zero j y z≤n (j0 ∷ s) (j1 ∷ t) = {!!}
+    lemma Zero j y z≤n (j0 ∷ s) (j2 ∷ t) = {!!}
+    lemma Zero j y z≤n (j1 ∷ s) (j0 ∷ t) = {!!}
+    lemma Zero j y z≤n (j1 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
+    lemma Zero j y z≤n (j1 ∷ s) (j2 ∷ t) = {!!}
+    lemma Zero j y z≤n (j2 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
+    lemma Zero j y z≤n (j2 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
+    lemma Zero j y z≤n (j2 ∷ s) (j2 ∷ t) = lemma Zero j y z≤n s t
+    lemma (Suc i) j (Suc y) (s≤s i<y) [] t = 3⊆-[] {t}
+    lemma (Suc i) j (Suc y) (s≤s i<y) (x ∷ s) [] = {!!}
+    lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j0 ∷ t) = {!!}
+    lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j1 ∷ t) = {!!}
+    lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j2 ∷ t) = {!!}
+    lemma (Suc i) j (Suc y) (s≤s i<y) (j1 ∷ s) (x1 ∷ t) = {!!}
+    lemma (Suc i) j (Suc y) (s≤s i<y) (j2 ∷ s) (x1 ∷ t) = {!!}
+    -- with lemma i j y i<y s t 
 
 
 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x)  3⊆ (f 3↑ y)