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

comparison src/zorn.agda @ 771:7679fef53073

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, 26 Jul 2022 03:37:25 +0900
parents 798d8b8c36b1
children 068cba4ee934
comparison
equal deleted inserted replaced
770:798d8b8c36b1 771:7679fef53073
628 → SUP A (uchain f mf ay) 628 → SUP A (uchain f mf ay)
629 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) 629 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay)
630 630
631 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ 631 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
632 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy 632 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
633 ; csupf = λ {z} → csupf {z} ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 ) 633 ; csupf = λ {z} → csupf {z} ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 ) ; supf-mono = λ _ → o≤-refl
634 ; 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 634 ; 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
635 spi = & (SUP.sup (ysup f mf ay)) 635 spi = & (SUP.sup (ysup f mf ay))
636 isupf : Ordinal → Ordinal 636 isupf : Ordinal → Ordinal
637 isupf z = spi 637 isupf z = spi
638 sp = ysup f mf ay 638 sp = ysup f mf ay
791 ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z) 791 ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
792 zc12 = ZChain.csupf ozc {z} 792 zc12 = ZChain.csupf ozc {z}
793 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z) 793 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
794 zc11 with zc12 794 zc11 with zc12
795 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 795 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
796 ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup z 796 ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , z13 fc is-sup ⟫ where
797 zc14 (subst (λ k → FClosure A f k (ZChain.supf ozc z)) (sym eq1) (init az)) ⟫ where 797 z13 : FClosure A f (ZChain.supf ozc u ) (ZChain.supf ozc z ) → ChainP A f mf ay (ZChain.supf ozc) u (ZChain.supf ozc z )
798 zc14 : ChainP A f mf ay psupf z (ZChain.supf ozc z) 798 → UChain A f mf ay psupf x (ZChain.supf ozc z )
799 zc14 = ? 799 z13 fc is-sup = ?
800
801 -- ch-is-sup z
802 -- zc14 (subst (λ k → FClosure A f k (ZChain.supf ozc z)) (sym eq1) (init az)) ⟫ where
803 -- zc14 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
804 -- zc14 = record { csupz = ? ; supfu=u = ? ; fcy<sup = ? ; order = ? } where
805 -- csupz : FClosure A f (psupf z) (ZChain.supf ozc z)
806 -- csupz = ?
807
800 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc15 808 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc15
801 (subst (λ k → FClosure A f k spu) zc17 (init (SUP.A∋maximal usup))) ⟫ where 809 (subst (λ k → FClosure A f k spu) zc17 (init (SUP.A∋maximal usup))) ⟫ where
802 zc15 : ChainP A f mf ay psupf x spu 810 zc15 : ChainP A f mf ay psupf x spu
803 zc15 = ? 811 zc15 = ?
804 zc17 : spu ≡ psupf x 812 zc17 : spu ≡ psupf x