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

changeset 790:201b66da4e69

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove unnesesary part in SZ1 the second TransFinite induction for is-max
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Aug 2022 02:50:13 +0900
parents a08c456d49d0
children f4450bc95699
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Aug 03 01:49:34 2022 +0900
+++ b/src/zorn.agda	Wed Aug 03 02:50:13 2022 +0900
@@ -527,37 +527,20 @@
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
-           is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f )
-           ... | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
-           ... | case2  ¬fy<x  = m01 where
-                 px<x : px o< x
-                 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
-                 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-                 m01 with trio< b px    --- px  < b < x
-                 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
-                 ... | tri< b<px ¬b ¬c = chain-mono1 x (ordtrans px<x <-osuc ) m04 where
-                    m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
-                    m03 with proj2 ua
-                    ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-                    ... | ch-is-sup u u≤x is-sup fc with osuc-≡< u≤x
-                    ... | case1 u=x = ?    -- u is sup of chain px, b is also a sup becasue it has no prev , so a = b
-                    ... | case2 u<x = ⟪ proj1 ua , ch-is-sup u (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x) is-sup fc ⟫
-                    m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
-                    m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
-                         (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x (ordtrans px<x <-osuc) lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
-                    b<A : b o< & A
-                    b<A = z09 ab
-                    m05 : b ≡ ZChain.supf zc b
-                    m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
+           is-max {a} {b} ua b<x ab (case2 is-sup) a<b 
+             = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
+              b<A : b o< & A
+              b<A = z09 ab
+              m05 : b ≡ ZChain.supf zc b
+              m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x (osucc b<x) uz )  }  )
-                    m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
-                    m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
-                    m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
+              m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
+              m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
+              m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
-                    m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
-                    m06 : ChainP A f mf ay (ZChain.supf zc) b 
-                    m06 = record {  fcy<sup = m08  ; order = m09 } 
+              m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
+              m06 : ChainP A f mf ay (ZChain.supf zc) b 
+              m06 = record {  fcy<sup = m08  ; order = m09 } 
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -566,21 +549,20 @@
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-           ... | case2 y<b = chain-mono1 x (osucc b<x) m04 where
-                 m09 : b o< & A
-                 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-                 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-                 m07 {z} fc = ZChain.fcy<sup zc m09 fc
-                 m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
+           ... | case2 y<b = chain-mono1 x (osucc b<x) 
+             ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫ where
+              m09 : b o< & A
+              m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
+              m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
+              m07 {z} fc = ZChain.fcy<sup zc m09 fc
+              m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
                        → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
-                 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
-                 m05 : b ≡ ZChain.supf zc b
-                 m05 = sym (ZChain.sup=u zc ab m09
+              m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
+              m05 : b ≡ ZChain.supf zc b
+              m05 = sym (ZChain.sup=u zc ab m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x (osucc b<x) lt )} )   -- ZChain on x
-                 m06 : ChainP A f mf ay (ZChain.supf zc) b 
-                 m06 = record { fcy<sup = m07 ;  order = m08 }
-                 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫
+              m06 : ChainP A f mf ay (ZChain.supf zc) b 
+              m06 = record { fcy<sup = m07 ;  order = m08 }
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function