Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.agda @ 384:171a3d587d6e
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 |
comparison
equal
deleted
inserted
replaced
383:5994f10d9bfd | 384:171a3d587d6e |
---|---|
348 3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h | 348 3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h |
349 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | 349 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h |
350 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | 350 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h |
351 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | 351 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h |
352 | 352 |
353 ↑app :(Nat → Two) → Nat → List Three → List Three | |
354 ↑app f Zero y = y | |
355 ↑app f (Suc x) y with f x | |
356 ... | i0 = ↑app f x (j0 ∷ y ) | |
357 ... | i1 = ↑app f x (j1 ∷ y ) | |
358 | |
359 _3↑_ : (Nat → Two) → Nat → List Three | |
360 f 3↑ x = ↑app f x [] | |
361 | |
362 lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t)) | |
363 lemma10 s t eq = eq | |
364 lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t)) | |
365 lemma11 s t eq = eq | |
366 | |
367 3↑22 : (f : Nat → Two) (i j : Nat) → List Three | 353 3↑22 : (f : Nat → Two) (i j : Nat) → List Three |
368 3↑22 f Zero j = [] | 354 3↑22 f Zero j = [] |
369 3↑22 f (Suc i) j with f i | 355 3↑22 f (Suc i) j with f j |
370 3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j) | 356 3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j) |
371 3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j) | 357 3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j) |
372 | 358 |
373 3↑2 : (Nat → Two) → Nat → List Three | 359 _3↑_ : (Nat → Two) → Nat → List Three |
374 3↑2 f i = 3↑22 f i 0 | 360 _3↑_ f i = 3↑22 f i 0 |
375 | 361 |
376 3↑<22 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x) 3⊆ (3↑2 f y) | 362 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x) 3⊆ (_3↑_ f y) |
377 3↑<22 {f} {x} {y} x<y = lemma x y 0 x<y where | 363 3↑< {f} {x} {y} x<y = lemma x y 0 x<y where |
378 lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i ) | 364 lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i ) |
379 lemma 0 y i z≤n with f i | 365 lemma 0 y i z≤n with f i |
380 lemma Zero Zero i z≤n | i0 = refl | 366 lemma Zero Zero i z≤n | i0 = refl |
381 lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i} | 367 lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i} |
382 lemma Zero Zero i z≤n | i1 = refl | 368 lemma Zero Zero i z≤n | i1 = refl |
383 lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i} | 369 lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i} |
384 lemma (Suc x) (Suc y) i (s≤s x<y) with f i | 3↑22 f (Suc y) i | 370 lemma (Suc x) (Suc y) i (s≤s x<y) with f i |
385 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 | t = {!!} where | 371 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y |
386 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 | t = {!!} | 372 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y |
387 lemma1 : {x i : Nat} → f x ≡ i0 → 3↑22 f (Suc x) i ≡ j0 ∷ 3↑22 f x (Suc i) | |
388 lemma1 {x} {i} eq = {!!} | |
389 | 373 |
390 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t)) | 374 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t)) |
391 lemma12 s t eq = eq | 375 lemma12 s t eq = eq |
392 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t)) | 376 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t)) |
393 lemma13 s t eq = eq | 377 lemma13 s t eq = eq |
394 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t)) | 378 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t)) |
395 lemma14 s t eq = eq | 379 lemma14 s t eq = eq |
396 | |
397 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y) | |
398 3↑< {f} {x} {y} x<y = {!!} | |
399 | 380 |
400 record Finite3 (p : List Three ) : Set where | 381 record Finite3 (p : List Three ) : Set where |
401 field | 382 field |
402 3-max : Nat | 383 3-max : Nat |
403 3-func : Nat → Two | 384 3-func : Nat → Two |