Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 384:171a3d587d6e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Three List / Filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Jul 2020 00:20:33 +0900
parents 5994f10d9bfd
children edbf7459a85f
files filter.agda
diffstat 1 files changed, 8 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/filter.agda	Tue Jul 21 23:40:38 2020 +0900
+++ b/filter.agda	Wed Jul 22 00:20:33 2020 +0900
@@ -350,42 +350,26 @@
 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
 
-↑app :(Nat → Two) → Nat → List Three  → List Three 
-↑app f Zero y = y
-↑app f (Suc x) y with f x
-... | i0 = ↑app f x (j0 ∷ y )
-... | i1 = ↑app f x (j1 ∷ y )
-
-_3↑_ : (Nat → Two) → Nat → List Three
-f 3↑ x = ↑app f x [] 
-
-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
-
 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 with f j
 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 
+_3↑_ : (Nat → Two) → Nat → List Three
+_3↑_ f i = 3↑22 f i 0 
 
-3↑<22 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x)  3⊆ (3↑2 f y)
-3↑<22 {f} {x} {y} x<y = lemma x y 0 x<y where
+3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x)  3⊆ (_3↑_ f y)
+3↑< {f} {x} {y} x<y = lemma x y 0 x<y where
      lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
      lemma 0 y i z≤n with f i
      lemma Zero Zero i z≤n | i0 = refl
      lemma Zero (Suc y) i z≤n | i0 = 3⊆-[]  {3↑22 f (Suc y) i}
      lemma Zero Zero i z≤n | i1 = refl
      lemma Zero (Suc y) i z≤n | i1 = 3⊆-[]  {3↑22 f (Suc y) i}
-     lemma (Suc x) (Suc y) i (s≤s x<y) with f i  | 3↑22 f (Suc y) i
-     lemma (Suc x) (Suc y) i (s≤s x<y) | i0 | t = {!!}  where
-     lemma (Suc x) (Suc y) i (s≤s x<y) | i1 | t = {!!}
-     lemma1 : {x i : Nat} → f x ≡ i0 → 3↑22 f (Suc x) i ≡ j0 ∷ 3↑22 f x (Suc i)
-     lemma1 {x} {i} eq = {!!}
+     lemma (Suc x) (Suc y) i (s≤s x<y) with f i  
+     lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y 
+     lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y 
 
 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
 lemma12 s t eq = eq
@@ -394,9 +378,6 @@
 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
 lemma14 s t eq = eq
 
-3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x)  3⊆ (f 3↑ y)
-3↑< {f} {x} {y} x<y = {!!} 
-
 record Finite3 (p : List Three ) : Set  where
    field
      3-max :  Nat