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

comparison filter.agda @ 383:5994f10d9bfd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Jul 2020 23:40:38 +0900
parents c3a0fb13e267
children 171a3d587d6e
comparison
equal deleted inserted replaced
382:c3a0fb13e267 383:5994f10d9bfd
357 ... | i1 = ↑app f x (j1 ∷ y ) 357 ... | i1 = ↑app f x (j1 ∷ y )
358 358
359 _3↑_ : (Nat → Two) → Nat → List Three 359 _3↑_ : (Nat → Two) → Nat → List Three
360 f 3↑ x = ↑app f x [] 360 f 3↑ x = ↑app f x []
361 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
362 3↑22 : (f : Nat → Two) (i j : Nat) → List Three 367 3↑22 : (f : Nat → Two) (i j : Nat) → List Three
363 3↑22 f Zero j = [] 368 3↑22 f Zero j = []
364 3↑22 f (Suc i) j with f i 369 3↑22 f (Suc i) j with f i
365 3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j) 370 3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j)
366 3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j) 371 3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j)
367 372
368 3↑2 : (Nat → Two) → Nat → List Three 373 3↑2 : (Nat → Two) → Nat → List Three
369 3↑2 f i = 3↑22 f i 0 374 3↑2 f i = 3↑22 f i 0
370 375
371 lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t)) 376 3↑<22 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x) 3⊆ (3↑2 f y)
372 lemma10 s t eq = eq 377 3↑<22 {f} {x} {y} x<y = lemma x y 0 x<y where
373 lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t)) 378 lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
374 lemma11 s t eq = eq 379 lemma 0 y i z≤n with f i
380 lemma Zero Zero i z≤n | i0 = refl
381 lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i}
382 lemma Zero Zero i z≤n | i1 = refl
383 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
385 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 | t = {!!} where
386 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 | t = {!!}
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
375 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t)) 390 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
376 lemma12 s t eq = eq 391 lemma12 s t eq = eq
377 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t)) 392 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
378 lemma13 s t eq = eq 393 lemma13 s t eq = eq
379 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t)) 394 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
380 lemma14 s t eq = eq 395 lemma14 s t eq = eq
381 396
382 3↑<2 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x) 3⊆ (3↑2 f y)
383 3↑<2 {f} {x} {y} x<y = lemma x 0 y x<y (3↑22 f x 0) (3↑22 f y 0) where
384 lemma : (i j y : Nat) → i ≤ y → (s t : List Three) → s 3⊆ t
385 lemma Zero j y z≤n [] [] = refl
386 lemma Zero j y z≤n [] (x ∷ t) = 3⊆-[] {x ∷ t}
387 lemma Zero j y z≤n (x ∷ s) [] = {!!}
388 lemma Zero j y z≤n (j0 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
389 lemma Zero j y z≤n (j0 ∷ s) (j1 ∷ t) = {!!}
390 lemma Zero j y z≤n (j0 ∷ s) (j2 ∷ t) = {!!}
391 lemma Zero j y z≤n (j1 ∷ s) (j0 ∷ t) = {!!}
392 lemma Zero j y z≤n (j1 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
393 lemma Zero j y z≤n (j1 ∷ s) (j2 ∷ t) = {!!}
394 lemma Zero j y z≤n (j2 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
395 lemma Zero j y z≤n (j2 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
396 lemma Zero j y z≤n (j2 ∷ s) (j2 ∷ t) = lemma Zero j y z≤n s t
397 lemma (Suc i) j (Suc y) (s≤s i<y) [] t = 3⊆-[] {t}
398 lemma (Suc i) j (Suc y) (s≤s i<y) (x ∷ s) [] = {!!}
399 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j0 ∷ t) = {!!}
400 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j1 ∷ t) = {!!}
401 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j2 ∷ t) = {!!}
402 lemma (Suc i) j (Suc y) (s≤s i<y) (j1 ∷ s) (x1 ∷ t) = {!!}
403 lemma (Suc i) j (Suc y) (s≤s i<y) (j2 ∷ s) (x1 ∷ t) = {!!}
404 -- with lemma i j y i<y s t
405
406
407 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y) 397 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y)
408 3↑< {f} {x} {y} x<y = {!!} where 398 3↑< {f} {x} {y} x<y = {!!}
409 lemma0 : (i : Nat) → (y : List Three ) → ( ↑app f (Suc i) y ≡ ↑app f i (j0 ∷ y)) ∨ ( ↑app f (Suc i) y ≡ ↑app f i (j1 ∷ y))
410 lemma0 i y with f i
411 lemma0 i y | i0 = case1 refl
412 lemma0 i y | i1 = case2 refl
413 lemma : (i : Nat) → (f 3↑ i) 3⊆ (f 3↑ Suc i)
414 lemma i with f i
415 lemma i | i0 = {!!}
416 lemma i | i1 = {!!}
417 399
418 record Finite3 (p : List Three ) : Set where 400 record Finite3 (p : List Three ) : Set where
419 field 401 field
420 3-max : Nat 402 3-max : Nat
421 3-func : Nat → Two 403 3-func : Nat → Two