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

comparison src/bijection.agda @ 1324:1eefc6600354

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 Sun, 11 Jun 2023 18:49:13 +0900
parents 95f6216499d7
children 8b909deb840e
comparison
equal deleted inserted replaced
1323:95f6216499d7 1324:1eefc6600354
694 694
695 fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < fla-max n 695 fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < fla-max n
696 fla-max< zero n i≤n = ? 696 fla-max< zero n i≤n = ?
697 fla-max< (suc i) n i≤n = ? 697 fla-max< (suc i) n i≤n = ?
698 698
699 record FLany (n m : ℕ ) : Set where 699 fla0 : (i n : ℕ ) → i < suc n → FList (fla-max n)
700 fla0 zero n lt = FLinsert fl0 [] where
701 fl0 : FL (fla-max n )
702 fl0 = ca<n zero (fla-max< zero n 0<s )
703 fla0 (suc i) n (s≤s lt) = FLinsert fl0 fl1 where
704 fl0 : FL (fla-max n )
705 fl0 = ca<n (suc i) (fla-max< (suc i) n ? )
706 fl1 = fla0 i n (≤-trans refl-≤s (s≤s lt))
707 fla : (n : ℕ) → FList (fla-max n)
708 fla n = fla0 n n a<sa
709
710 record FLany (n : ℕ ) : Set where
700 field 711 field
701 flist : FList (fla-max n) 712 flist : FList (fla-max n)
702 flany : (i : ℕ) → (i<n : i < suc m ) → (m≤n : suc m < suc n) → Any ( ca<n i (fla-max< i n (<-trans i<n m≤n ) ) ≡_) flist 713 flany : (i : ℕ) → (i<n : i < suc n ) → Any ( ca<n i (fla-max< i n i<n ) ≡_) flist
703 714
704 fla : (n : ℕ) → FLany n n 715 flany : (n : ℕ) → FLany n
705 fla n = fla0 n a<sa where 716 flany n = record { flist = fla0 n n a<sa ; flany = ? } where
706 fla0 : (i : ℕ ) → i < suc n → FLany n i 717 flany0 : (i : ℕ) → (i<n : i < suc n ) → Any ( ca<n i (fla-max< i n i<n ) ≡_) (fla0 i n i<n)
707 fla0 zero lt = record { flist = FLinsert fl0 [] ; flany = fl1 } where 718 flany0 zero i<n = fl1 where
708 fl0 : FL (fla-max n ) 719 fl0 = ca<n zero (fla-max< zero n 0<s )
709 fl0 = ca<n zero (fla-max< zero n 0<s ) 720 fl1 = x∈FLins fl0 []
710 fl1 : (i : ℕ) (i<n : i < 1) (m≤n : 1 < suc n) → Any (_≡_ (ca<n i (fla-max< i n (<-trans i<n m≤n)))) (FLinsert fl0 []) 721 flany0 (suc i) (s≤s i<n) = fl3 where
711 fl1 zero (s≤s z≤n) lt = x∈FLins fl0 [] 722 fl0 : FL (fla-max n )
712 fla0 (suc i) (s≤s lt) = record { flist = FLinsert fl0 fl1 ; flany = fl2 } where 723 fl0 = ca<n (suc i) (fla-max< (suc i) n ? )
713 fl0 : FL (fla-max n ) 724 fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n))
714 fl0 = ca<n i (fla-max< i n (≤-trans lt refl-≤s ) ) 725 fl3 = x∈FLins fl0 fl1
715 fl1 = FLany.flist ( fla0 i (≤-trans refl-≤s (s≤s lt)) ) 726 fl4 : Any ( ca<n i (fla-max< i n (≤-trans refl-≤s (s≤s i<n)) ) ≡_) (fla0 i n (≤-trans refl-≤s (s≤s i<n)))
716 fl3 = x∈FLins fl0 fl1 727 fl4 = flany0 i (≤-trans refl-≤s (s≤s i<n))
717 fl4 = FLany.flany (fla0 i (≤-trans refl-≤s (s≤s lt))) 728
718 fl2 : (j : ℕ) (i<n : j < suc (suc i)) (m≤n : suc (suc i) < suc n)
719 → Any (_≡_ (ca<n j (fla-max< j n (<-trans i<n m≤n)))) (FLinsert fl0 fl1)
720 fl2 j i<n m≤n with ≤-∨ i<n
721 ... | case1 eq = ?
722 ... | case2 lt = ? -- fl4 ? ? ? -- FLany.flany ( fla0 i ? ) j ? ?
723 729
724 lem02 : (n : ℕ) → maxAC n 730 lem02 : (n : ℕ) → maxAC n
725 lem02 n = lem03 n where 731 lem02 n = lem03 n where
726 lem03 : (i : ℕ) → maxAC i 732 lem03 : (i : ℕ) → maxAC i
727 lem03 i = lem10 i where 733 lem03 i = lem10 i where