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

changeset 760:0dc7999b1d50

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 Mon, 25 Jul 2022 06:41:40 +0900
parents 944f50265914
children 9307f895891c
files src/zorn.agda
diffstat 1 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jul 24 19:01:24 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 06:41:40 2022 +0900
@@ -368,6 +368,8 @@
      <-irr0 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
      z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
+     z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
+     z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
      s : HOD
      s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
      as : A ∋ * ( & s  )
@@ -473,11 +475,17 @@
                     ... | ch-is-sup u u≤x is-sup fc with trio< u px
                     ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup fc ⟫ -- u o< osuc x
                     ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup fc ⟫
-                    ... | tri> ¬a ¬b c = ?   -- u = x
+                    ... | tri> ¬a ¬b c = ?   -- u = x → u = sup →  (b o< x →  b  < a ) → ⊥  
                     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-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) ? (subst (λ k → FClosure A f k b) ? (init ab)) ⟫  -- b = px case,  u = px  u< osuc x 
+                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
+                    m06 : ChainP A f mf ay (ZChain.supf zc) b b
+                    m06 = ?
+                    m05 : b ≡ ZChain.supf zc b
+                    m05 = sym ( ZChain.sup=u zc {b} {ab} (z09 ab) 
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
+                    -- b = px case,  u = px  u< osuc x 
         ... | 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) →