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

comparison filter.agda @ 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
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