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

comparison src/zorn.agda @ 767:6c87cb98abf2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
spi <= u
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 25 Jul 2022 22:27:15 +0900
parents e1c6c32efe01
children 67c7d4b43844
comparison
equal deleted inserted replaced
766:e1c6c32efe01 767:6c87cb98abf2
638 ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 638 ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
639 → SUP A (uchain f mf ay) 639 → SUP A (uchain f mf ay)
640 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) 640 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay)
641 641
642 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ 642 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
643 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = csupf ; fcy<sup = ? 643 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
644 ; csupf = λ {z} → csupf {z} ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 )
644 ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where 645 ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
645 spi = & (SUP.sup (ysup f mf ay)) 646 spi = & (SUP.sup (ysup f mf ay))
646 isupf : Ordinal → Ordinal 647 isupf : Ordinal → Ordinal
647 isupf z = spi 648 isupf z with trio< z spi
649 ... | tri< a ¬b ¬c = y
650 ... | tri≈ ¬a b ¬c = spi
651 ... | tri> ¬a ¬b c = spi
648 sp = ysup f mf ay 652 sp = ysup f mf ay
653 asi = SUP.A∋maximal sp
649 cy : odef (UnionCF A f mf ay isupf o∅) y 654 cy : odef (UnionCF A f mf ay isupf o∅) y
650 cy = ⟪ ay , ch-init (init ay) ⟫ 655 cy = ⟪ ay , ch-init (init ay) ⟫
651 y<sup : * y ≤ SUP.sup (ysup f mf ay) 656 y<sup : * y ≤ SUP.sup (ysup f mf ay)
652 y<sup = SUP.x<sup (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay)) 657 y<sup = SUP.x<sup (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay))
653 isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z 658 isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
654 isy {z} ⟪ az , uz ⟫ with uz 659 isy {z} ⟪ az , uz ⟫ with uz
655 ... | ch-init fc = s≤fc y f mf fc 660 ... | ch-init fc = s≤fc y f mf fc
656 ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup) (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc ) 661 ... | ch-is-sup u is-sup fc = ?
657 inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a) 662 inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
658 inext {a} ua with (proj2 ua) 663 inext {a} ua with (proj2 ua)
659 ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-init (fsuc _ fc ) ⟫ 664 ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-init (fsuc _ fc ) ⟫
660 ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-is-sup u (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫ 665 ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-is-sup u (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫
661 itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 666 itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅)
662 itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 667 itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
663 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 668 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
664 uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb) 669 uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)
665 670
666 csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z) 671 csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z)
667 csupf {z} = ? 672 csupf {z} = uz00 where
673 -- = ? where -- ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where
674 uz03 : {z : Ordinal } → FClosure A f y z → (z ≡ spi) ∨ (z << spi)
675 uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc )
676 ... | case1 eq = case1 ( begin
677 z ≡⟨ sym &iso ⟩
678 & (* z) ≡⟨ cong (&) eq ⟩
679 spi ∎ ) where open ≡-Reasoning
680 ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
681 uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
682 uz04 {s} {z} s<spi fcz = ?
683 -- uz02 : ChainP A f mf ay isupf spi spi
684 -- uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = ? }
685 uz00 : odef (UnionCF A f mf ay isupf o∅) (isupf z)
686 uz00 with trio< z spi
687 ... | tri< a ¬b ¬c = ?
688 ... | tri≈ ¬a b ¬c = ?
689 ... | tri> ¬a ¬b c = ?
690
668 691
669 -- 692 --
670 -- create all ZChains under o< x 693 -- create all ZChains under o< x
671 -- 694 --
672 695